Three logics for branching bisimulation
- 1 March 1995
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 42 (2), 458-487
- https://doi.org/10.1145/201019.201032
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.Keywords
This publication has 14 references indexed in Scilit:
- Translations between modal logics of reactive systemsTheoretical Computer Science, 1995
- An action-based framework for veryfying logical and behavioural properties of concurrent systemsComputer Networks and ISDN Systems, 1993
- Characterizing finite Kripke structures in propositional temporal logicTheoretical Computer Science, 1988
- Extensional equivalences for transition systemsActa Informatica, 1987
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- “Sometimes” and “not never” revisitedJournal of the ACM, 1986
- The power of the future perfect in program logicsInformation and Control, 1985
- Algebraic laws for nondeterminism and concurrencyJournal of the ACM, 1985
- Results on the propositional μ-calculusTheoretical Computer Science, 1983
- Propositional dynamic logic of looping and converse is elementarily decidableInformation and Control, 1982