AbstractIn 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 CCS-terms branching bisimulation congruence can be completely axiomatized by the single axiom scheme
a.(\tau.(y + z) + y) = a.(y + z)
(where a ranges over all actions) and the usual laws 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.
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory; F.1.2 [Computation by Abstract Devices]: Modes of Computation; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages
Additional Key Words and Phrases: Abstraction, action refinement, bisimulation, branching time, concurrency, process algebra, semantic equivalence
Selected papers that cite this one
- Luca Aceto, Rob van Glabbeek, Wan Fokkink, and Anna Ingólfsdóttir. Axiomatizing prefix iteration with silent steps. Information and Computation, 127(1):26-40, 25 May 1996.
- J. C. M. Baeten and J. A. Bergstra. Process algebra with propositional signals. Theoretical Computer Science, 177(2):381-405, 15 May 1997.
- Pedro R. D'Argenio and Chris Verhoef. A general conservative extension theorem in process algebras with inequalities. Theoretical Computer Science, 177(2):351-380, 15 May 1997.
- Andrew M. Pitts and Joshua R. X. Ross. Process calculus based upon evaluation to committed form. Theoretical Computer Science, 195(2):155-182, 30 March 1998.
Selected references
- J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Control, 60(1-3):109-137, January/February/March 1984.
- Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. Journal of the ACM, 42(1):232-268, January 1995.
- S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560-599, July 1984.
- Søren Christensen, Hans Hüttel, and Colin Stirling. Bisimulation equivalence is decidable for all context-free processes. Information and Computation, 121(2):143-148, September 1995.
- Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, January 1985.
- Bengt Jonsson and Joachim Parrow. Deciding bisimulation equivalences for a class of Non-Finite-State programs. Information and Computation, 107(2):272-302, December 1993.
- Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86(1):43-68, May 1990.
- Rocco De Nicola and Frits Vaandrager. Three logics for branching bisimulation (extended abstract). In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 118-129, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.
- Rocco De Nicola and Frits Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458-487, March 1995.
- W. C. Rounds and S. D. Brookes. Possible futures, acceptances, refusals, and communicating processes. In 22nd Annual Symposium on Foundations of Computer Science, pages 140-149, Nashville, Tennessee, 28-30 October 1981. IEEE.
- Irek Ulidowski. Equivalences on observable processes. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 148-159, Santa Cruz, California, 22-25 June 1992. IEEE Computer Society Press.
- D. J. Walker. Bisimulation and divergence. Information and Computation, 85(2):202-241, April 1990.