Journal of the ACM Bibliography

Rocco De Nicola and Frits Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458-487, March 1995. [BibTeX entry]

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

Selected references


  • Journal of the ACM homepage
  • Bibliography top level
  • Journal of the ACM Author Index
  • Search the HBP database