Branching Time and Abstraction in Bisimulation Semantics (Extended 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. The paper investigates whether observation equivalence really does respect the branching structure of processes, and finds 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. For a large class of processes it turns out that branching bisimulation and observation equivalence are the same.