### Branching time and abstraction in bisimulation semanticsBranching time and abstraction in bisimulation semantics

Access Restriction
Subscribed

 Author van Glabbeek, Rob J. ♦ Weijland, W. Peter Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©1996 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Subject Keyword Abstraction ♦ Action refinement ♦ Bisimulation ♦ Branching time ♦ Concurrency ♦ Process algebra semantic equivalence Abstract In comparative concurrency semantics, one usually distinguishes between linear time and branching time semantic equivalences. Milner's notion of observatin 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 axion scheme: $\textit{a.(τ.(y+z)+y)=a.(y+z)}$ (where $\textit{a}$ ranges over all actions) and the usual loaws 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. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 1996-05-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 43 Issue Number 3 Page Count 46 Starting Page 555 Ending Page 600

#### Open content in new tab

Source: ACM Digital Library