A complete axiomatization for branching bisimulation congruence of finite-state behaviours

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

This paper offers a complete inference system for branching bisimulation congruence on a basic sublanguage of CCS for representing regular processes with silent moves. Moreover, complete axiomatizations are provided for the guarded expressions in this language, representing the divergence-free processes, and for the recursion-free expressions, representing the finite processes. Furthermore it is argued that in abstract interleaving semantics (at least for finite processes) branching bisimulation congruence is the finest reasonable congruence possible. The argument is that for closed recursion-free process expressions, in the presence of some standard process algebra operations like partially synchronous parallel composition and relabelling, branching bisimulation congruence is completely axiomatized by the usual axioms for strong congruence together with Milner's first τ-law aτ X=aX.

Original languageEnglish
Title of host publicationMathematical Foundations of Computer Science 1993: 18th International Symposium, MFCS’93, Gdańsk, Poland, August 30–September 3, 1993 Proceedings
EditorsA.M. Borzyszkowski, S Sokołowski
Number of pages12
ISBN (Electronic)978-3-540-47927-7
ISBN (Print)978-3-540-57182-7
Publication statusPublished - 18 Aug 1993

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'A complete axiomatization for branching bisimulation congruence of finite-state behaviours'. Together they form a unique fingerprint.

Cite this