Extensions of Standard Weak Bisimulation Machinery: Finite-state General Processes, Refinable Actions, Maximal-progress and Time

We present our work on extending the standard machinery for weak bisimulation to deal with: finite-state processes of calculi with a full signature, including static operators like parallel; semantic action refinement and ST bisimulation; maximal-progress, i.e. priority of standard actions over unprioritized actions; representation of time: discrete real-time and Markovian stochastic time. For every such topic we show that it is possible to resort simply to weak bisimulation and that we can exploit this to obtain, via modifications to the standard machinery: finite-stateness of semantic models when static operators are not replicable by recursion, as for CCS with the standard semantics, thus yielding decidability of equivalence; structural operational semantics for terms; a complete axiomatization for finite-state processes via a modification of the standard theory of standard equation sets and of the normal-form derivation procedure.