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

TL;DR

This paper extends a decomposition method for modal formulas to include modalities with internal actions, enabling the derivation of congruence formats for delay and weak bisimilarity in process semantics.

Contribution

It enhances the previous decomposition technique to handle more complex modal characterizations involving internal actions, facilitating congruence results for delay and weak bisimilarity.

Findings

Decomposition method now handles modalities with internal actions.

Derived congruence formats for delay and weak bisimilarity.

Ensured modal formulas remain within the characterization during decomposition.

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 $\langle\epsilon\rangle\langle a\rangle\phi$, to derive congruence formats for delay and weak bisimilarity.