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.
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 language | English |
---|---|
Title of host publication | Information Processing 89, 11th World Computer Congress, San Francisco 1989 |
Editors | G.X. Ritter |
Publisher | North-Holland Publishing Company |
Pages | 613-618 |
Number of pages | 6 |
Publication status | Published - 1 Sept 1989 |
Event | The IFIP 11th World Computer Congress, 1989 - San Francisco, United States Duration: 28 Aug 1989 → 1 Sept 1989 Conference number: 11 |
Conference
Conference | The IFIP 11th World Computer Congress, 1989 |
---|---|
Country/Territory | United States |
City | San Francisco |
Period | 28/08/89 → 1/09/89 |