Skip to main content


Lean and full congruence formats for recursion


Rob van Glabbeek




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

    author           = {van Glabbeek, Robert},
    month            = jun,
    year             = {2017},
    keywords         = {structural operational semantics, congruence formats, recursion, bisimulation.},
    title            = {Lean and Full Congruence Formats for Recursion},
    booktitle        = {Proceedings 32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017)},
    address          = {Reykjavik, Iceland}


Served by Apache on Linux on seL4.