next up previous
Next: Introduction Up: Reference

Branching Time and Abstraction in Bisimulation Semantics

Rob van Glabbeek & Peter Weijland
Centrum voor Wiskunde en Informatica
Postbus 94079, 1090 GB Amsterdam, The Netherlands

Original December 1990; Updated January 1996

Abstract: In comparative concurrency semantics one usually distinguishes between linear time and branching time semantic equivalences. Milner's notion of observation equivalence is often mentioned as the standard example of a branching time equivalence. In this paper we investigate whether observation equivalence really does respect the branching structure of processes, and find that in the presence of the unobservable action t of CCS this is not the case.

Therefore the notion of branching bisimulation equivalence is introduced which strongly preserves the branching structure of processes, in the sense that it preserves computations together with the potentials in all intermediate states that are passed through, even if silent moves are involved. On closed CCS-terms branching bisimulation congruence can be completely axiomatized by the single axiom scheme:

a.(t.(y + z) + y) = a.(y + z)

(where a ranges over all actions) and the usual laws for strong congruence.

We also establish that for sequential processes observation equivalence is not preserved under refinement of actions, whereas branching bisimulation is.

For a large class of processes it turns out that branching bisimulation and observation equivalence are the same. As far as we know, all protocols that have been verified in the setting of observation equivalence happen to fit in this class, and hence are also valid in the stronger setting of branching bisimulation equivalence.

Key words & phrases: Concurrency, process algebra, semantic equivalences, abstraction, bisimulation, branching time, action refinement.
1980 Mathematics Subject Classification: 68B10, 68C01, 68D25, 68F20
1985 Mathematics Subject Classification: 68Q55, 68Q45, 68Q10, 68N15
1987 CR Categories: F.3.2, F.4.3, F.1.2, D.3.1.

Version management: An extended abstract of this paper appeared as VAN GLABBEEK & WEIJLAND(1989a). The sections on branching and abstraction, congruence and axioms partly appeared in WEIJLAND (1989), and the section on refinement as VAN GLABBEEK & WEIJLAND (1989b). The full paper first appeared as Chapter III of VAN GLABBEEK (1990a) and in a slightly extended form as VAN GLABBEEK & WEIJLAND (1990). An updated and further extended version appears in the second edition of VAN GLABBEEK (1990a). A further updated version, but lacking an historical note, a digression about deadlock and termination in BPA, CCS and ACP, and complete axiomatizations also for BPA and ACP, appeared in the Journal of the ACM 43(3), 1996, pp. 555-600. This hypertext document displays part of this last version. A PDF-file of the entire document is available for JACM subscribers from the ACM portal.
Support: The research of the authors was supported by ESPRIT project 432 (METEOR). The first author was also supported by Sonderforschungsbereich 342 of the TU München, by the ESPRIT Basic Research Action 3148 (DEMON) and by ONR under grant number N00014-92-J-1974; the second author by ESPRIT project 3006 (CONCUR). This paper was finalized when the first author was employed at the Technical University of Munich and updated when he was employed at Stanford University. The current (1996) affiliations of the authors are:
R.J. van Glabbeek, Computer Science Department, Stanford University, Stanford, California 94305, USA.
W.P. Weijland, PTT Telecom, Postbus 30150, 2500 GD Den Haag, The Netherlands. Acknowledgement: We thank the JACM referees for their many insightful suggestions.
next up previous
Next: Introduction Up: Reference

Rob van Glabbeek