Three logics for branching bisimulation
- 4 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 118-129
- https://doi.org/10.1109/lics.1990.113739
Abstract
Three temporal logics are introduced which induce on labeled transition systems the same identifications as branching bisimulation. The first is an extension of Hennessy-Milner logic with a kind of unit operator. The second is another extension of Hennessy-Milner logic which exploits the power of backward modalities. The third is CTL* with the next-time operator interpreted over all paths, not just over maximal ones. A relevant side effect of the last characterization is that it sets a bridge between the state- and event-based approaches to the semantics of concurrent systems.Keywords
This publication has 8 references indexed in Scilit:
- An efficient algorithm for branching bisimulation and stuttering equivalencePublished by Springer Nature ,2005
- Compositional model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Using the axiomatic presentation of behavioural equivalences for manipulating CCS specificationsPublished by Springer Nature ,1990
- Characterizing finite Kripke structures in propositional temporal logicTheoretical Computer Science, 1988
- Extensional equivalences for transition systemsActa Informatica, 1987
- “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