Skip to main content

Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity

Authors

Rob van Glabbeek and Wan Fokkink

DATA61

Vrije Universiteit Amsterdam

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              = {10.1016/j.ic.2017.10.003},
    date             = {2017-12-19},
    author           = {van Glabbeek, Rob and Fokkink, Wan},
    series           = {Leibniz International Proceedings in Informatics (LIPIcs)},
    journal          = {Information and Computation},
    issn             = {0890-5401},
    month            = dec,
    volume           = {257},
    editor           = {{Meyer, Roland \& Nestmann, Uwe}},
    year             = {2017},
    keywords         = {structural operational semantics congruence formats modal logic weak bisimilarity},
    title            = {Divide and Congruence {II}: From Decomposition of Modal Formulas to Preservation of Delay and Weak
                        Bisimilarity},
    pages            = {79-113},
    address          = {Berlin, Germany}
  }

Download

Served by Apache on Linux on seL4.