Three logics for branching bisimulation

ABSTRACT

Three temporal logics are introduced that induce on labeled transition systems the same identifications as branching bisimulation, a behavioral equivalence that aims at ignoring invisible transitions while preserving the branching structure of systems. The first logic is an extension of Hennessy-Milner Logic with an “until” operator. The second one is another extension of Hennessy-Milner Logic, which exploits the power of backward modalities. The third logic is CTL* without the next-time operator. A relevant side-effect of the last characterization is that it sets a bridge between the state- and action-based approaches to the semantics of concurrent systems.

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: ~AKKERMAN, G. J., AND BAETEN, J. C. M. 1990. Term rewriting analysis in process algebra. ~Report P9006. Programming Research Group, Univ. Amsterdam, Amsterdam, the Netherlands.
• 3: J. C. M. Baeten, Applications of process algebra, Cambridge University Press, New York, NY, 1990
• 4: J. C. M. Baeten , W. P. Weijland, Process algebra, Cambridge University Press, New York, NY, 1991
• 5: B. Bloom , S. Istrail , A. R. Meyer, Bisimulation can't be traced, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.229-239, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73580]
• 6: Jeroen van de. Lagemaat , Jeroen Van De Lagemaat , Tommaso Bolognesi , Chris Vissers, LOTOSphere: Software Development with Lotos, Kluwer Academic Publishers, Norwell, MA, 1995
• 7: 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 ]
• 8: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 9: E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
• 10: R. Cleaveland , J. Parrow , B. Steffen, The concurrency workbench, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.24-37, February 1990, Grenoble, France
• 11: Philippe Darondeau , Pierpaolo Degano, About semantic action refinement, Fundamenta Informaticae, v.14 n.2, p.221-234, Feb. 1991
• 12: ~DE BAKKER, J., DE ROEVER, W. P., AND ROZENBERG, G. EDS. 1989. Linear time, branching time ~and partial order in logics and models for concurrency. In Lecture Notes in Computer Science, ~vol. 354, Springer-Verlag, New York.
• 13: R De Nicola, Extensional equivalence for transition systems, Acta Informatica, v.24 n.2, p.211-237, April 1987
• 14: R. De Nicola , A. Fantechi , S. Gnesi , G. Ristori, An action-based framework for verifying logical and behavioural properties of concurrent systems, Computer Networks and ISDN Systems, v.25 n.7, p.761-778, Feb. 1993 [doi>10.1016/0169-7552(93)90047-8]
• 15: 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
• 16: 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
• 17: 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
• 18: ~DE NICOLA, R., AND VAANDRAGER, F. W. 1990b. Three logics for branching bisimulation ~(Extended Abstract). In Proceedings of the 5th Annual Symposium on Logzc zn Computer Scie~zce ~(LICS). IEEE Computer Society Press, New York, pp. 118 129.
• 19: 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]
• 20: E. A Emerson , Chin L Lei, Model Checking Under Generalized Fairness Constraints, University of Texas at Austin, Austin, TX, 1984
• 21: E. Allen Emerson , Jai Srinivasan, Branching time temporal logic, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, p.123-172, May 30-June 03, 1988
• 22: 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
• 23: ~VAN GLABBEEK, R. J. 1990. Comparative concurrency semantics and refinement of actions. ~Ph.D. dissertation, Free University, Amsterdam, The Netherlands.
• 24: ~VAN GLABBEEK, R. J., AND WEIJLAND, W. P. 1989/1991. Branching time and abstraction in ~bisimulation semantics (extended abstract). In Information Processing '89, G. X. Ritter, ed. ~North Holland, Amsterdam, The Netherlands, pp. 613-618. Full paper appeared as CWI ~Report CS-R9120, Amsterdam 1991.
• 25: ~VAN GLABBEEK, R. J., AND WEIJLAND, W. P. 1989. Refinement in branching time semantics. In ~Proceedings of the AMAST Conference. IOWA pp. 197-201.
• 26: 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]
• 27: Matthew Hennessy , Colin Stirling, The power of the future perfect in program logics, Information and Control, v.67 n.1-3, p.23-52, Oct./Nov./Dec. 1986 [doi>10.1016/S0019-9958(85)80025-5]
• 28: B. Jonsson , A. H. Khan , J. Parrow, Implementing a model checking algorithm by adapting existing automated tools, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.179-188, February 1990, Grenoble, France
• 29: Henri Korver, Computing Distinguishing Formulas for Branching Bisimulation, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.13-23, July 01-04, 1991
• 30: Maciej Koutny, Axiom system induced by CTL* Logic, Fundamenta Informaticae, v.14 n.2, p.235-253, Feb. 1991
• 31: ~KOZEN, D. 1983. Results on the propositional mu-calculus. Theoret. Comput. Sci., 27, 333-354.
• 32: 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
• 33: Orna Lichtenstein , Amir Pnueli , Lenore D. Zuck, The Glory of the Past, Proceedings of the Conference on Logic of Programs, p.196-218, June 17-19, 1985
• 34: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 35: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 36: 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
• 37: ~OL~, E. E. 1992. An efficient implementation of branching bisimulation and distinguishing ~formulae. Master Thesis. Programming Research Group. Univ. Amsterdam, Amsterdam, The ~Netherlands.
• 38: ~PRATT, V. 1981. A decidable mu-calculus. In Proceedings of the 22nd Symposium on Foundations ~of Computer Science. IEEE Computer Society Press, New York, pp. 421-427.
• 39: Colin Stirling, Temporal logics for CCS, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, p.660-672, May 30-June 03, 1988
• 40: Colin Stirling, Modal and temporal logics, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 41: ~STREET, R. S. 1982. Propositional dynamic logic of looping and converse is elementarily ~decidable. Inf. Cont. 54, 121-141.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Theory, Verification

Keywords:
CTL*, Hennessy-Milner logic, Kripke structures, backward modalities, branching bisimulation equivalence, concurrency, doubly labeled transition systems, labeled transition systems, reactive systems, semantics, stuttering equivalence, until operations