Journal of the Association for Computing Machinery, Vol. 43, No. 3, May 1996, pp. 555–600.

Branching Time and Abstraction in Bisimulation Semantics

ROB J. VAN GLABBEEK

AND

W. PETER WEIJLAND

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 τ 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.(τ.(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.

Categories and Subject Descriptors. D.3.1 [Programming Languages]: Formal Definitions and Theory; F.1.2 [Computation by Abstract Devices]: Modes of Computation; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages

Additional Key words and Phrases. Abstraction, action refinement, bisimulation, branching time, concurrency, process algebra, semantic equivalence

Copyright 1996 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.