Skip to main content
CSIRO Logo Data 61 logo

Lean and full congruence formats for recursion

Authors

Rob van Glabbeek

DATA61

UNSW Sydney

Abstract

In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions. I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.

BibTeX Entry

  @inproceedings{vanGlabbeek_17_2,
    author           = {van Glabbeek, Rob},
    doi              = {https://doi.org/10.1109/LICS.2017.8005142},
    month            = aug,
    date             = {2017-8-18},
    year             = {2017},
    keywords         = {Structural Operational Semantics Congruence formats Recursion Bisimulation},
    title            = {Lean and Full Congruence Formats for Recursion},
    address          = {Reykjavik, Iceland},
    numpages         = {11 p.},
    booktitle        = {Proceedings of the 32nd Annual IEEE Symposium on Logic in Computer Science},
    paperurl         = {https://ts.data61.csiro.au/publications/csiro_full_text//vanGlabbeek_17_2.pdf},
    publisher        = {ACM/IEEE}
  }

Download