Three Logics for Branching Bisimulation (Extended Abstract)
Rocco De Nicola, Frits Vaandrager · Logic in Computer Science · 1990
Three temporal logics are introduced which induce on labelled transition systems the same identifications as branching bisimulation. The first is an extension of Hennessy-Milner Logic with a kind of “until” operator. The second is another extension of Hennessy-Milner Logic which exploits the power of backward modalities. The third is CTL* without 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.