Structural operational semantics for weak bisimulations

AbstractIn this study, we present rule formats for four main notions of bisimulation with silent moves. Weak bisimulation is a congruence for any process algebra defined by WB cool rules; we have similar results for rooted weak bisimulation (Milner's “observational congruence”), branching bisimulation, and rooted branching bisimulation. The theorems stating that, say, observational congruence is an appropriate notion of equality for CCS are corollaries of the results of this paper. We also give sufficient conditions under which equational axiom systems can be generated from operational rules. Indeed, many equational axiom systems appearing in the literature are instances of this general theory