Journal of the ACM Bibliography

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. Copyright 1995 by ACM, Inc.

The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.

Preliminary version

A 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.

Shortcuts: