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. rvg@cs.stanford.edu.
W.P. Weijland, PTT Telecom, Postbus 30150, 2500 GD Den Haag, The
Netherlands. w.p.weijland@bd.telecom.ptt.nl.
Acknowledgement: We thank the JACM referees for their many insightful
suggestions.
Next: Introduction
Up: Reference
Rob van Glabbeek