Branching Time and Abstraction in Bisimulation Semantics (extended abstract)

R.J. van Glabbeek, W.P. Weijland

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 tau 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 terms, branching bisimulation can be completely axiomatized by the two laws:

x;tau = x
x;((tau;(y+z))+y) = x;(y+z).


For a large class of processes it turns out that branching bisimulation and observation equivalence are the same. All protocols known to the authors 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.
Original languageEnglish
Title of host publicationInformation Processing 89, 11th World Computer Congress, San Francisco 1989
EditorsG.X. Ritter
PublisherNorth-Holland Publishing Company
Pages613-618
Number of pages6
Publication statusPublished - 1 Sept 1989
EventThe IFIP 11th World Computer Congress, 1989 - San Francisco, United States
Duration: 28 Aug 19891 Sept 1989
Conference number: 11

Conference

ConferenceThe IFIP 11th World Computer Congress, 1989
Country/TerritoryUnited States
CitySan Francisco
Period28/08/891/09/89

Fingerprint

Dive into the research topics of 'Branching Time and Abstraction in Bisimulation Semantics (extended abstract)'. Together they form a unique fingerprint.

Cite this