Branching time and abstraction in bisimulation semantics

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 &tgr; 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: a.(&tgr;.(y+z)+y)=a.(y+z) (where 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.

REFERENCES

• 1: S. Abramsky, Observation equivalence as a testing equivalence, Theoretical Computer Science, v.53 n.2-3, p.225-241, Aug. 1987 [doi>10.1016/0304-3975(87)90065-X]
• 2: AcF.xo, L., FOKKING, W. J., VAN GI.ABBEEK, R. J., AND ING6LFSD6TTIR, A. 1995. Axiomatizing prcfix iteration with silent steps. BRICS Research Report RS-95-56. Department of Mathematics and Computer Science. Aalborg Univ., Aalborg, Denmark. (Inf. Comput., to appear.)
• 3: AKK~r~MAN, G. J. AND BAETEN, J. C.M. 1991. Term rewriting analysis in process algebra. CW1 Quarterly 4, 4, 257-267.
• 4: J. C. M. Baeten , J. A. Bergstra , J. W. Klop, On the consistency of Koomen's fair abstraction rule, Theoretical Computer Science, v.51 n.1-2, p.129-176, March 31, 1987 [doi>10.1016/0304-3975(87)90052-1]
• 5: J. C. M. Baeten , J. A. Bergstra, Ready-trace semantics for concrete process algebra with the priority operator, The Computer Journal, v.30 n.6, p.498-506, Dec. 1987
• 6: J. C. M. Baeten , R. J. van Glabbeek, Another look at abstraction in process algebra, 14th International Colloquium on Automata, languages and programming, p.84-94, July 1987, Karlsruhe, Germany
• 7: J. C. M. Baeten , W. P. Weijland, Process algebra, Cambridge University Press, New York, NY, 1991
• 8: Twan Basten, Branching bisimilarity is an equivalence indeed!, Information Processing Letters, v.58 n.3, p.141-147, May 13, 1996 [doi>10.1016/0020-0190(96)00034-8]
• 9: BERGSTRA, J. A. AND KI,OP, J.W. 1984. Process algebra for synchronous communication. Inf. Cont..60, 1-3, 109- i 37.
• 10: BERGSTRA, J. A. AND KLOP, J.W. 1985. Algebra of communicating processes with abstraction. Theoret. Comput. ScL 37, 1, 77-121.
• 11: BERGSTRA, J. A. AND KLOP, J.W. 1988. A complete inference system for regular processes with silent moves. In Proceedings of the Logic Colloquium 1986, F. R. Drake and J. K. Truss, eds. Hull, North Holland, Amsterdam, The Netherlands, pp. 21-81.
• 12: BERGSTRA, J. A., KLOP, J. W., AND OLDEROG, E.-R. 1987. Failures without chaos: A new process semantics for fair abstraction. In Formal Description of Programming Concepts-Ill. Proceedings of the 3rd IFIP WG 2.2 Working Conference. M. Wirsing, ed. (Ebberup, Denmark). North Holland, pp. 77-103.
• 13: Bard Bloom, Structural operational semantics for weak bisimulations, Theoretical Computer Science, v.146 n.1-2, p.25-68, July 24, 1995 [doi>10.1016/0304-3975(94)00152-9]
• 14: Bard Bloom , Sorin Istrail , Albert R. Meyer, Bisimulation can't be traced, Journal of the ACM (JACM), v.42 n.1, p.232-268, Jan. 1995 [doi>10.1145/200836.200876]
• 15: Bouhta, A. 1992. Weak and branching bisimulation in FCTOOL. Rapports de Recherche No. 1575. INRIA, Sophia Antipolis, Valbonne Cedex, France.
• 16: S. D. Brookes , C. A. R. Hoare , A. W. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM (JACM), v.31 n.3, p.560-599, July 1984 [doi>10.1145/828.833]
• 17: M. C. Browne , E. M. Clarke , O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science, v.59 n.1-2, p.115-131, July 1988 [doi>10.1016/0304-3975(88)90098-9]
• 18: CASTELLANO, L., DE MICHEUS, G., AND POMELLO, L. 1987. Concurrency vs Interleaving: An instructive example. Bull. EA TCS 31, 12-15.
• 19: CHERIEF, F. 1992. Contributions ~ la s6mantique du parali61isme- Bisimulations pour le raffinement et le vrai paralMlisme. Ph.D. dissertation. Univ. Grenoble, Grenoble, France.
• 20: CHERIEF, F. AND SCHNOEBELEN, Pn. 1991. r-Bisimulations and full abstraction for refinement of actions. Inf. Proc. Lett. 40, 219-222.
• 21: Søren Christensen , Hans Hüttel , Colin Stirling, Bisimulation equivalence is decidable for all context-free processes, Information and Computation, v.121 n.2, p.143-148, Sept. 1995 [doi>10.1006/inco.1995.1129]
• 22: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 23: Philippe Darondeau , Pierpaolo Degano, About semantic action refinement, Fundamenta Informaticae, v.14 n.2, p.221-234, Feb. 1991
• 24: DE BAKKER, J. W., BERGSTRA, J. A., KLOP, j. W., AND MEIJER, J.-J. CH. 1984. Linear time and branching time semantics for recursion with merge. Theoret. Comput. Sci. 34, 135-156.
• 25: DE NICOLA, R. AND HENNESS~, M. 1984. Testing equivalence for processes. Theoret. Comput. Sci. 34, 83-133.
• 26: R. De Nicola , P. Inverardi , M. Nesi, Using the axiomatic presentation of behavioural equivalences for manipulating CCS specifications, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.54-67, February 1990, Grenoble, France
• 27: Rocco De Nicola , Ugo Montanari , Frits Vaandrager, Back and forth bisimulations, Proceedings on Theories of concurrency : unification and extension: unification and extension, p.152-165, September 1990, Amsterdam, The Netherlands
• 28: Rocco De Nicola , Frits Vaandrager, Action versus state based logics for transition systems, Proceedings of the LITP spring school on theoretical computer science on Semantics of systems of concurrent processes, p.407-419, November 1990, La Roche Posay, France
• 29: Rocco De Nicola , Frits Vaandrager, Three logics for branching bisimulation, Journal of the ACM (JACM), v.42 n.2, p.458-487, March 1995 [doi>10.1145/201019.201032]
• 30: Raymond Devillers, Maximality preserving bisimulation, Theoretical Computer Science, v.102 n.1, p.165-183, 3 Aug. 1992 [doi>10.1016/0304-3975(92)90298-T]
• 31: E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
• 32: S. Graf , J. Sifakis, Readiness semantics for regular processes with silent actions, 14th International Colloquium on Automata, languages and programming, p.115-125, July 1987, Karlsruhe, Germany
• 33: Jan Friso Groote , Hans Hüttel, Undecidable equivalences for basic process algebra, Information and Computation, v.115 n.2, p.354-371, Dec. 1994 [doi>10.1006/inco.1994.1101]
• 34: Jan Friso Groote , Frits Vaandrager, An efficient algorithm for branching bisimulation and stuttering equivalence, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.626-638, July 1990, Warwick University, England
• 35: Matthew Hennessy , Robin Milner, On Observing Nondeterminism and Concurrency, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.299-309, July 14-18, 1980
• 36: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 37: Matthew Hennessy , Gordon D. Plotkin, A Term Model for CCS, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, p.261-274, September 01-05, 1980
• 38: HOARE, C. A. R. 1980. Communicating sequential processes. In On the construction of programs, R. McKeag and A. M. Macnaghten, eds. Cambridge University Press, Cambridge, England, pp. 229-254.
• 39: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 40: Bengt Jonsson , Joachim Parrow, Deciding bisimulation equivalences for a class of non-finite-state programs, Information and Computation, v.107 n.2, p.272-302, Dec. 1993 [doi>10.1006/inco.1993.1069]
• 41: Paris C. Kanellakis , Scott A. Smolka, CCS expressions finite state processes, and three problems of equivalence, Information and Computation, v.86 n.1, p.43-68, May 1990 [doi>10.1016/0890-5401(90)90025-D]
• 42: LAMPORT, L. 1983. What good is temporal logic? Inf. Proc. 83, 657-668.
• 43: LAMPORT, L. 1986. On interprocess communication. Part 1: Basic formalism. Dist. Comput. 1, 2, 77- 85.
• 44: F. Laroussinie , S. Pinchinat , Ph. Schnoebelen, Translations between modal logics of reactive systems, Theoretical Computer Science, v.140 n.1, p.53-71, March 20, 1995
• 45: MII.NER, R. 1980. A calculus of communication systems. In Lecture Notes in Computer Science, vol. 92. Springer-Verlag, New York.
• 46: Robin Milner, A Modal Characterisation of Observable Machine-Behaviour, Proceedings of the 6th Colloquium on Trees in Algebra and Programming, p.25-34, March 05-07, 1981
• 47: MILNER, R. 1983. Calculi for synchrony and asynchrony. Theoret. Cornput. Sci. 25, 267-310.
• 48: Robin Milner, Lectures on a Calculus for Communicating Systems, Seminar on Concurrency, Carnegie-Mellon University, p.197-220, July 09-11, 1984
• 49: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 50: E R Olderog , C A R Hoare, Specification-oriented semantics for communicating processes, Acta Informatica, v.23 n.1, p.9-66, April 1986 [doi>10.1007/BF00268075]
• 51: David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
• 52: Joachim Parrow , Peter Sjödin, Multiway Synchrinizaton Verified with Coupled Simulation, Proceedings of the Third International Conference on Concurrency Theory, p.518-533, August 24-27, 1992
• 53: PI.~TERSON, G. L. 1981. Myths about the mutual exclusion problem. Inf. Proc. Lett. 12, 3, 115--116.
• 54: I. Phillips, Refusal testing, Theoretical Computer Science, v.50 n.3, p.241-284, Feb. 1987 [doi>10.1016/0304-3975(87)90117-4]
• 55: Amir Pnueli, Linear and Branching Structures in the Semantics and Logics of Reactive Systems, Proceedings of the 12th Colloquium on Automata, Languages and Programming, p.15-32, July 15-19, 1985
• 56: Lucia Pomello, Some equivalence notions for concurrent systems. An overview, Advances in Petri Nets 1985, covers the 6th European Workshop on Applications and Theory in Petri Nets-selected papers, p.381-400, June 01, 1985
• 57: Vaughan Pratt, Modeling concurrency with partial orders, International Journal of Parallel Programming, v.15 n.1, p.33-71, Feb. 1986 [doi>10.1007/BF01379149]
• 58: ROt;ND, W. C. AND BROOKES, S.D. 1981. Possible futures, acceptances, refusals and communicating processes. In Proceedings 22nd Annual Symposium on Foundations of Computer Science (Nashville, Tenn.). IEEE, New York, pp. 140-149.
• 59: Ut.IDOWSKI, !. 1992. Equivalences on observable processes. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICS '92) (Santa Cruz, Calif.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 148-159.
• 60: VAN BENTHEM, J., VAN EIJCK, J., AND STEBLETSOVA, V. 1994. Modal logic, transition systems and processes, j. Logic Comput. 4, 5, 811-855.
• 61: VAN GLABBEEK, R.J. 1990a. Comparative concurrency semantics and refinement of actions. Ph.D. dissertation. Free University, Amsterdam, The Netherlands.
• 62: R. J. van Glabbeek, The linear time-branching time spectrum (extended abstract), Proceedings on Theories of concurrency : unification and extension: unification and extension, p.278-297, September 1990, Amsterdam, The Netherlands
• 63: Rob J. van Glabbeek, A Complete Axiomatization for Branching Bisimulation Congruence of Finite-State Behaviours, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.473-484, August 30-September 03, 1993
• 64: Rob J. van Glabbeek, The Linear Time - Branching Time Spectrum II, Proceedings of the 4th International Conference on Concurrency Theory, p.66-81, August 23-26, 1993
• 65: VAN GLABBEEK, R.J. 1994. What is branching time and why to use it? Report No. STAN-CS- 93-1486. Stanford University, available from Boole.stanford.edu. In the Concurrency Column, M. Nielsen, Ed. Bull. EA TCS 53, 190-198.
• 66: R. van Glabbeek , U. Goltz, Refinement of actions in causality based models, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.267-300, May 1990, Mook, The Netherlands
• 67: Rob van Glabbeek , Frits Vaandrager, Modular specification of process algebras, Theoretical Computer Science, v.113 n.2, p.293-348, June 7, 1993 [doi>10.1016/0304-3975(93)90006-F]
• 68: VAN GLABBEEK, R. J. AND WEIJLAND, W.P. 1989a. Branching time and abstraction in bisimulation semantics (extended abstract), Information Processing 89. In Proceedings of the IFIP llth World Computer Congress, G. X. Ritter, ed. (San Francisco, Calif.). North Holland, Amsterdam, The Netherlands, pp. 613-618.
• 69: VAN GLABBEEK, R. J. AND WEIJLAND, W.P. 1989b. Refinement in branching time semantics. Rep. CS-R8922. Centrum voor Wiskunde en lnformatica, Amsterdam, and Proceedings of AMAST Conference. Univ. Iowa, Iowa City, Ia. pp. 197-201.
• 70: VAN GLABBEEK, R. J. AND WELILAND, W.P. 1991, Branching time and abstraction in bisimulation semantics. Rep. CS-R9120. CWl, Amsterdam, The Netherlands.
• 71: D. J. Walker, Bisimulation and divergence, Information and Computation, v.85 n.2, p.202-241, April 1990 [doi>10.1016/0890-5401(90)90048-M]
• 72: WEULANO, W.P. 1989. Synchrony and asynchrony in process algebra. Ph.D. dissertation. Univ. Amsterdam, The Netherlands.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
  F.3 LOGICS AND MEANINGS OF PROGRAMS
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Languages, Theory

Keywords:
abstraction, action refinement, bisimulation, branching time, concurrency, process algebra semantic equivalence