Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation

Abstract. We present a method for decomposing modal formulas for processes with the internal action o /. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra. We use this decomposition method to derive congruence formats for branching and rooted branching bisimulation equivalence. 1 Introduction Structural operational semantics [20] provides process algebras and specificationlanguages with an interpretation. It generates a labelled transition system, in which states are the closed terms over a (single-sorted, first-order) signature, andtransitions between states may be supplied with labels. The transitions between states are obtained from a transition system specification, which consists of aset of proof rules called transition rules. Labelled transition systems can be distinguished from each other by a widerange of behavioural equivalences, based on e.g. branching structure or decorated versions of execution sequences. Van Glabbeek [11] classified equivalences forprocesses that take into account the internal actio