Rob J. van Glabbeek
W. Peter Weijland
Skip Abstract Section
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: a.(τ.(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.
- ABRAMSKY, S. 1987. Observation equivalence as a testing equivalence. Theoret. Comput. Sci. 53, 225-241. Google Scholar
- 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.)Google Scholar
- AKK~r~MAN, G. J. AND BAETEN, J. C.M. 1991. Term rewriting analysis in process algebra. CW1 Quarterly 4, 4, 257-267.Google Scholar
- BAETF.N, j. C. M., BERGSTRA, J. A. AND Kl.or', J.W. 1987a. On the consistency of Koomen's fair abstraction rule. Theoret. Comput. Sci. 51, 1/2, 129-176. Google Scholar
- BAETEN, J. C. M., BERGSTRA, J. A., AND KLOP, J.W. 1987b. Ready-trace semantics for concrete prt~cess algebra with the priority operator. Comput. J. 30, 6, 498-506. Google Scholar
- BAETEN, J. C. M. AND VAN GABBEEK, R.J. 1987. Another look at abstraction in process algebra, in Proceedings of ICALP 87 (Karlsruhe, Germany). Th. Ottman, ed. Lecture Notes in Computer Science. vol. 267. Springer-Verlag, New York, pp. 84-94. Google Scholar
- BAETEN, J. C. M. AND WEIJLAND, W. P. 1990. Process Algebra. In Cambridge Tracts in ?heoretical Computer Science, vol. 18. Cambridge University Press, Cambridge, England. Google Scholar
- BASTi~N, T. 1996. Branching bisimulation is an equivalence indeed! Inf. Proc. Lett. to appear. Google Scholar
- BERGSTRA, J. A. AND KI,OP, J.W. 1984. Process algebra for synchronous communication. Inf. Cont.60, 1-3, 109- i 37.Google Scholar
- BERGSTRA, J. A. AND KLOP, J.W. 1985. Algebra of communicating processes with abstraction. Theoret. Comput. ScL 37, 1, 77-121.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- BLOOM, B. 1995. Structural operational semantics for weak bisimulations. Theoret. Comput. Sci. 146, 25-68. Google Scholar
- BLOOM, B., ISTRAIL, S., AND MEYER, A.R. 1995. Bisimulation can't be traced. J. ACM 42, 1 (Jan.), 232-268. Google Scholar
- Bouhta, A. 1992. Weak and branching bisimulation in FCTOOL. Rapports de Recherche No. 1575. INRIA, Sophia Antipolis, Valbonne Cedex, France.Google Scholar
- BROOKES, S. D., HOARE, C. A. R., AND ROSCOE, A.W. 1984. A theory of communicating sequential processes. ,1. ACM 31, 3 (July), 560-599. Google Scholar
- BROWNE, M. C., CLARKE, E. M., AND GROMaERG, O. 1988. Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59, 1/2, 115-131. Google Scholar
- CASTELLANO, L., DE MICHEUS, G., AND POMELLO, L. 1987. Concurrency vs Interleaving: An instructive example. Bull. EA TCS 31, 12-15.Google Scholar
- CHERIEF, F. 1992. Contributions ~ la s6mantique du parali61isme- Bisimulations pour le raffinement et le vrai paralMlisme. Ph.D. dissertation. Univ. Grenoble, Grenoble, France.Google Scholar
- CHERIEF, F. AND SCHNOEBELEN, Pn. 1991. r-Bisimulations and full abstraction for refinement of actions. Inf. Proc. Lett. 40, 219-222.Google Scholar
- CHRISTENSEN, S., H(SrlTEL, H., AND STIRLING, C. 1995. Bisimulation equivalence is decidable for all context-free processes, inf. Comput. 121(2), 143-148. Google Scholar
- CLARKE, E. M. AND EMERSON, E, A. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings o.f the Workshop on Logics of Programs D. Kozen, ed. (Yorktown Heights, N.Y.) Lecture Notes in Computer Science, vol 131. Springer- Verlag, New York, pp. 52-71. Google Scholar
- DARONDEAU, PH. AND DEGANO, P. 1989. About semantic action refinement. Fundamenta Informaticae XIE, 221-234. Google Scholar
- 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.Google Scholar
- DE NICOLA, R. AND HENNESS~, M. 1984. Testing equivalence for processes. Theoret. Comput. Sci. 34, 83-133.Google Scholar
- DE NICOLA, R., INVERARDI, P., AND NESl, M. 1990a. Using axiomatic presentation of behavioural equivalences for manipulating CCS specifications. In Automatic Verification Methods for Finite State Systems, J. Sifakis, ed. Lecture Notes in Computer Science, vol. 407. Springer- Verlag, New York, pp. 54-67. Google Scholar
- DE N~COLA, R., MONTANARI, U., AND VAANDRAGER, F.W. 1990b. Back and forth bisimulations. In Proceedings of CONCUR 90, J. C. M. Baeten and J. W. Klop, eds. (Amsterdam, The Netherlands, Lecture Notes in Computer Science, vol. 458. Springer-Verlag, New York, pp. 152-165. Google Scholar
- DE NICOLA, R. AND VAANDRAGER, F.W. 1990. Action versus state based logics for transition systems. In Proceedings of the Semantics of Systems of Concurrent Processes, I. Guessarian, ed. (La Roche Posay, France). Lecture Notes in Computer Science, vol. 469, Springer-Verlag, New York, pp. 407-419. Google Scholar
- DE NtCOLA, R. AND VAANORAGER, F. W. 1995. Three logics for branching bisimulation. J. ACM 42, 2, 458-487. Google Scholar
- DEVILLERS, R. 1992. Maximality preserving bisimulation. Theoret. Comput. Sci. 102, 165-183. Google Scholar
- EMERSON, E. A. AND HALPERN, J.Y. 1986. 'Sometimes' and 'Not Never' revisited: on branching time versus linear time temporal logic. J. ACM 33, 1 (Jan.) 151-178. Google Scholar
- GaAF, S. AND SIFAKIS, J. 1987. Readiness semantics for regular processes with silent actions. In Proceedings of ICALP 87, Th. Ottman, ed. (Karlsruhe, Germany) Lecture Notes in Computer Science, vol. 267. Springer-Verlag, New York, pp. 115-125. Google Scholar
- GROOTE, J. F. Aa'qD Ht,vlq~L, H. 1994. Undecidable equivalences for basic process algebra. Inf. Comput. 115, 2, 354-371. Google Scholar
- GROOTE, J. F. ANO VAANDRAGER, F.W. 1990. An efficient algorithm for branching bisimulation and stuttering equivalence. In Proceedings of ICALP 90. M. S. Paterson, ed. (Warwick, R. I.). Lecture Notes in Computer Science, vol. 443, Springer-Verlag, New York, pp. 626-638. Google Scholar
- HENNESSY, M. AND MILNER, R. 1980. On observing nondeterminism and concurrency. In Proceedings ICALP 80, J. W. de Bakker and J. van Leeuwen, eds. Lecture Notes in Computer Science, vol. 85. Springer-Verlag, New York, 299-309 (a preliminary version of Hennessy and Milner { 1985 }). Google Scholar
- HENNESSY, M. AND MILNER, R. 1985. Algebraic laws for nondeterminism and concurrency. J. ACM 32. 1, 137-161. Google Scholar
- HENNESSY, M. AND PLO'rKaN, G.D. 1980. A term model for CCS. In Proceedings of MFCS 80 (P. Dembifiski, ed.). Lecture Notes in Computer Science, vol. 88. Springer-Verlag, New York, pp. 261-274. Google Scholar
- 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.Google Scholar
- HOARE, C. A.R. 1985. Communicating sequentialprocesses. Prentice-Hall, London, England. Google Scholar
- JONSSON, B. ANO PARROW, J. 1993. Deciding bisimulation equivalences for a class of nonfinite-state programs. Inf. Comput. 107, 272-302. Google Scholar
- KANEI.I.AKIS, P. C. AND SMOLKA, S.A. 1990. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86, 43-68. Google Scholar
- LAMPORT, L. 1983. What good is temporal logic? Inf. Proc. 83, 657-668.Google Scholar
- LAMPORT, L. 1986. On interprocess communication. Part 1: Basic formalism. Dist. Comput. 1, 2, 77- 85.Google Scholar
- LAROUSSINIE, F., PINCHINAT, S., AND SCHNOEBELEN, PH. 1995. Translations between modal logics of reactive systems. Theoret. Comput. ScL 140, 1, 53-71. Google Scholar
- MII.NER, R. 1980. A calculus of communication systems. In Lecture Notes in Computer Science, vol. 92. Springer-Verlag, New York.Google Scholar
- MILNER, R. 1981. A modal characterisation of observable machine-behaviour. In Proceedings CAAP 81, G. Astesiano and C. B6hm, eds. Lecture Notes in Computer Science, vol. 112. Springer-Verlag, New York, pp. 25-34. Google Scholar
- MILNER, R. 1983. Calculi for synchrony and asynchrony. Theoret. Cornput. Sci. 25, 267-310.Google Scholar
- MII.NER, R. 1985. Lectures on a calculus for communicating systems. In Proceedings of the Seminar on Concurrency, S. D. Brookes, A. W. Roscoe, and G. Winskel, eds. Lecture Notes in Computer Science, vol. 97. Springer-Verlag, New York, pp. 197-220. Google Scholar
- MII_NER, R. 1989. Communication and concurrency. Prentice Hall, London, England. Google Scholar
- OIDEROG, E.-R. AND HOARE, C. A.R. 1986. Specification-oriented semantics for communicating processes. Acta Inf. 23, 9-66. Google Scholar
- PARK, D. M.R. 1981. Concurrency and automata on infinite sequences. In Proceedings of the 5th GI Conference P. Deussen, ed. Lecture Notes in Computer Science, vol. 104. Springer-Verlag, New York, pp. 167-183. Google Scholar
- PARROW, J. AND SJ~DIN, P. 1992. Multiway synchronization verified with coupled simulation. In Proceedings of CONCUR '92 W. R. Cleaveland, ed. (Stony Brook, NY). Lecture Notes in Computer Science, vol. 630. Springer-Verlag, New York, pp. 518-533. Google Scholar
- PI.~TERSON, G. L. 1981. Myths about the mutual exclusion problem. Inf. Proc. Lett. 12, 3, 115--116.Google Scholar
- PI-IlIA,IPS, I. C.C. 1987. Refusal testing. Theoret. Comput. Sci. 50, 241-284. Google Scholar
- P.~ut-:t.I, A. 1985. Linear and branching structures in the semantics and logics of reactive systems. In Proceedingsof the 12th ICALP, W. Brauer, ed. (Nafplion, Greece). Lecture Notes in Computer Science, vol. 194. Springer-Verlag, New York, pp. 15-32. Google Scholar
- POMEI.t.O, L. 1986. Some equivalence notions for concurrent systems. An overview, in Ad- ~,ances in Petri Nets 1985 G. Rozenberg, ed. Lecture Notes in Computer Science, vol. 222. Springer-Verlag, New York, pp. 381-400. Google Scholar
- PRATT, V.R. 1986. Modeling concurrency with partial orders. Int. J. Para. Prog. 15, 1, 33-71. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- VAN BENTHEM, J., VAN EIJCK, J., AND STEBLETSOVA, V. 1994. Modal logic, transition systems and processes, j. Logic Comput. 4, 5, 811-855.Google Scholar
- VAN GLABBEEK, R.J. 1990a. Comparative concurrency semantics and refinement of actions. Ph.D. dissertation. Free University, Amsterdam, The Netherlands.Google Scholar
- VAN GLABBEEK, R.J. 1990b. The linear time-branching time spectrum. In Proceedings of CONCUR '90 J. C. M. Baeten and J. W. Klop, eds. (Amsterdam, The Netherlands) Lecture Notes in Computer Science, vol. 458. Springer-Verlag, New York, pp. 278-297. Google Scholar
- VAN GLABBEEK, R.J. 1993a. A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In Proc. MFCS 1993, A. M. Borzyszkowski and S. Sokolowski, eds. (Gdansk, Poland). Lecture Notes in Computer Science, vol. 711. Springer-Verlag, New York, pp. 473-484. Google Scholar
- VAN GLABBEEK, R.J. 1993b. The linear time-branching time spectrum II. Preliminary version available from Boole.stanford.edu; extended abstract in Proceedings of CONCUR "93. E. Best, ed. (Hildesheim, Germany). Lecture Notes in Computer Science, vol. 715. Springer-Verlag, New York, pp. 66-81, Google Scholar
- 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.Google Scholar
- VAN GLABBEEK, R. J. AND GOLTZ, U. 1990. Refinement of actions in causality based models. In Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, eds. (Mook, The Netherlands), Lecture Notes in Computer Science, vol. 430. Springer-Verlag, New York, pp. 267-300. Google Scholar
- VAN GLABBEEK, R. J. AND VAANDRAGER, F.W. 1993. Modular specification of process algebras. Theoret. Comput. Sci., vol. 113, 2, 293-348. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- VAN GLABBEEK, R. J. AND WELILAND, W.P. 1991, Branching time and abstraction in bisimulation semantics. Rep. CS-R9120. CWl, Amsterdam, The Netherlands.Google Scholar
- WALKER, D.J. 1990. Bisimulation and divergence. Inf. Comput. 85, 2, 202-241. Google Scholar
- WEULANO, W.P. 1989. Synchrony and asynchrony in process algebra. Ph.D. dissertation. Univ. Amsterdam, The Netherlands.Google Scholar
Index Terms
- Branching time and abstraction in bisimulation semantics
Recommendations
Branching bisimulation for probabilistic systems: characteristics and decidability
Expressiveness in concurrencyWe address the concept of abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model of Hansson. In particular, we define the notion of branching bisimilarity and study its ...
Branching time and orthogonal bisimulation equivalence
We propose a refinement of branching bisimulation equivalence that we call orthogonal bisimulation equivalence. Typically, internal activity (the performance of τ-steps) may be compressed, but not completely discarded. Hence, a process with τ-steps ...
Bisimulation on speed: a unified approach
Two process-algebraic approaches have been developed for comparing two bisimulation-equivalent processes with respect to speed: the one of Moller/Tofts equips actions with lower time bounds, while the other by Lüttgen/Vogler considers upper time bounds ...
Comments