Abstract
Earlier we presented a method to decompose modal formulas for processes with the internal action τ, and congruence formats for branching and η-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 〈ϵ〉〈a〉φ, to derive congruence formats for delay and weak bisimilarity.
Original language | English |
---|---|
Pages (from-to) | 79-113 |
Number of pages | 35 |
Journal | Information and Computation |
Volume | 257 |
DOIs | |
Publication status | Published - 1 Dec 2017 |
Externally published | Yes |
Keywords
- Congruence formats
- Modal characterisation
- Structural operational semantics
- Weak bisimilarity