AbstractThree 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. Copyright 1995 by ACM, Inc.
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Preliminary versionA preliminary version of these results was presented in: 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.
Categories and Subject Descriptors: F.1.1 [Computation by Abstract Devices]: Models of Computation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs
General Terms: Theory, verification
Additional Key Words and Phrases: Backward modalities, branching bisimulation equivalence, concurrency, CTL*, doubly labeled transition systems, Hennessy-Milner logic, Kripke structures, labeled transition systems, reactive systems, semantics, stuttering equivalence, until operations
Selected papers that cite this one
- Twan Basten. Branching bisimilarity is an equivalence indeed! Information Processing Letters, 58(3):141-147, 13 May 1996.
- Rob J. van Glabbeek and W. Peter Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, May 1996.
- Nancy Lynch and Frits Vaandrager. Forward and backward simulations: I. Untimed systems. Information and Computation, 121(2):214-233, September 1995.
Selected references
- E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 353-362, Asilomar Conference Center, Pacific Grove, California, 5-8 June 1989. IEEE Computer Society Press.
- E. Allen Emerson and Joseph Y. Halpern. ``Sometimes'' and ``not never'' revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151-178, January 1986.
- Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, January 1985.
- Matthew Hennessy and Colin Stirling. The power of the future perfect in program logics. Information and Control, 67(1-3):23-52, October/November/December 1985.
- 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.
- V. R. Pratt. A decidable mu-calculus: Preliminary report. In 22nd Annual Symposium on Foundations of Computer Science, pages 421-427, Nashville, Tennessee, 28-30 October 1981. IEEE.
- Robert S. Streett. Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control, 54(1/2):121-141, July/August 1982.