Trustworthy Systems

Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity

Authors

Wan Fokkink, Rob van Glabbeek and Paulien de Wind

Free University of Amsterdam

NICTA

UNSW

Abstract

We present a method for decomposing modal formulas for processes with the internal action τ. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra. We use this decomposition method to derive congruence formats for two weak and rooted weak semantics: branching and η-bisimilarity.

BibTeX Entry

  @article{Fokkink_GW_12,
    author           = {Fokkink, Wan and van Glabbeek, Robert and de Wind, Paulien},
    issn             = {0890-5401},
    journal          = {Information and Computation},
    keywords         = {concurrency, structural operational semantics, compositionality, congruence, branching bisimulation,
                        modal logic, modal decomposition.},
    month            = may,
    number           = { },
    pages            = {59--85},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4930.pdf},
    title            = {Divide and Congruence: From Decomposition of Modal Formulas to Preservation of Branching and
                        {\η}-Bisimilarity},
    volume           = {214},
    year             = {2012}
  }

Download