Divide and Congruence II: From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity

Abstract

Earlier we presented a method to decompose modal formulas for processes with the internal action $\tau$, and congruence formats for branching and $\eta$-bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. In this follow-up paper the decomposition method is enhanced to deal with modal characterisations that contain a modality $⟨\epsilon ⟩⟨a⟩\varphi$, to derive congruence formats for delay and weak bisimilarity.

An extended abstract of this paper appeared in Proc. LICS'16. With Definition 20.4b(i) as formulated originally [v1], Proposition 5 does not hold. A corrected Definition 20.4b appears in this revision [v2]

Cited by in corpus (5)

• Logical Characterization of Bisimulation Metrics
• Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence
• SOS-based Modal Decomposition on Nondeterministic Probabilistic Processes
• Up-to Techniques for Branching Bisimilarity
• The Way We Were: Structural Operational Semantics Research in Perspective