Trustworthy Systems

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

Authors

Wan Fokkink and Rob van Glabbeek

Free University of Amsterdam

NICTA

UNSW

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

  @techreport{Fokkink_Glabbeek_16:tr,
    address          = {Sydney, Australia},
    author           = {Fokkink, Wan and van Glabbeek, Robert},
    institution      = {NICTA},
    issn             = {1833-9646-9351},
    keywords         = {structural operational semantics, congruence formats, weak bisimilarity, modal characterisation},
    month            = apr,
    number           = {9351},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9351.pdf},
    title            = {Divide and Congruence {II}: From Decomposition of Modal Formulas to Preservation of Delay and Weak
                        Bisimilarity},
    year             = {2016}
  }

Download