Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity
Authors
DATA61
Vrije Universiteit Amsterdam
UNSW Sydney
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.
BibTeX Entry
@article{vanGlabbeek_Fokkink_17, publisher = {Elsevier}, doi = {https://doi.org/10.1016/j.ic.2017.10.003}, month = dec, journal = {Information and Computation}, paperurl = {https://ts.data61.csiro.au/publications/csiro_full_text/vanGlabbeek_Fokkink_17.pdf}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, year = {2017}, issn = {0890-5401}, editor = {{Meyer, Roland \& Nestmann, Uwe}}, keywords = {Structural Operational Semantics Congruence formats Modal logic Weak bisimilarity}, volume = {257}, title = {Divide and Congruence {II}: From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity}, pages = {79-113}, author = {van Glabbeek, Rob and Fokkink, Wan}, date = {2017-12-19}, address = {Berlin, Germany} }