Branching Time and Abstraction in Bisimulation Semantics

ROB J. VAN GLABBEEK AND W. PETER WEIJLAND
Centturn (war Wiskunde en Informatica, Amsterdam, The Netherlands

JACM 1996

Branching time and abstraction in bisimulation semantics.pdf

Abstract.

   In comparative concurrency semantics, one usually distinguishes between linear time
and branching time semantic equivalences. Milner’s notion of ohsen~ation equirlalence 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 7 of CCS this is not the case.
Therefore, the notion of branching hisimulation 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 KS-terms branching bisimulation congruence can be completely axiomatized
by the single axiom scheme:
a.(7.(y + z) + y) = a.(y + z)
(where a ranges over all actions) and the usual laws for strong congruence.
WC 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 hisimulation equivalence.