Branching Bisimilarity is an Equivalence indeed!

This note presents a detailed proof of a result in the theory of concurrency semantics that is already considered folklore, namely that branching bisimilarity is an equivalence relation. The ``simple proof,'' which in the literature is always assumed to exist, is shown to be incorrect. The proof in this note is based on the notion of a semi-branching bisimulation taken from [2]. Branching bisimilarity can equivalently be defined in terms of semi-branching bisimulations; the results suggest that such a definition is more intuitive than the original definition of [1].
  1. R.J. van Glabbeek and W.P. Weijland. Branching Time and Abstraction in Bisimulation Semantics (extended abstract). In G.X. Ritter, editor, Information Processing 89: Proceedings of the IFIP 11th. World Computer Congress, pages 613-618, San Fransisco, CA, USA, August/September 1989. Elsevier Science Publishers B.V., North-Holland, The Netherlands, 1989.

  2. R.J. van Glabbeek and W.P. Weijland. Branching Time and Abstraction in Bisimulation Semantics. Report CS-R9120, Centre for Mathematics and Computer Science, CWI, Amsterdam, The Netherlands, 1991. A revised version with a corrected equivalence proof has appeared in the Journal of the ACM, 43(3):555-600, 1996.

(postscript / pdf version of the complete paper)

Back to the list of publications.