next up previous
Next: Practical applications Up: Conclusion Previous: Compositionality

Branching bisimulation equivalence is the only known equivalence in the linear time - branching time spectrum that supports an `eventually' operator as part of a temporal logic on transition systems. It even supports all the operators of CTL* and corresponds with stuttering equivalence of kripke structures.

As mentioned in the introduction, weak bisimulation semantics is not adequate for a modal logic with eventually operator. From the examples in the introduction one can see that the problem originates from the circumstance that weak bisimulation equivalence does not preserve the branching structure of processes. They also apply to all other semantic equivalences that do not preserve branching, and indeed one can easily prove that such an operator would cause no problems in branching bisimulation semantics, at least not in the variant with explicit divergence. In fact, a much stronger result has been proved by DE NICOLA & VAANDRAGER (1990a).

The Computation Tree Logic CTL* (EMERSON & HALPERN (1986)) is a very powerful logic, combining both branching time and linear time operators. It is a generalization of CTL (CLARKE & EMERSON (1981)), that contains only branching time operators. CTL* is interpreted on Kripke structures (directed graphs of which the nodes are labelled with sets of atomic propositions). DE NICOLA & VAANDRAGER (1990a) established a translation from process graphs to Kripke structures, so that CTL* can also be regarded as a logic on process graphs. In fact, in DE NICOLA & VAANDRAGER (1990b) they introduced a counterpart ACTL* of CTL* on process graphs and supplied translations in both directions. One of the operators of CTL/CTL*, the nexttime operator X, makes it possible to see when an (invisible) action takes place, and is therefore incompatible with abstraction. This operator was also criticized by LAMPORT (1983). BROWNE, CLARKE & GRÜMBERG (1988) found that CTL without X and CTL* without X induce the same equivalence on Kripke structures, which they characterized as stuttering equivalence. In DE NICOLA & VAANDRAGER (1990a) branching bisimulation, after being translated to Kripke structures, is shown to coincide with stuttering equivalence. (To be precise, they consider two variants of CTL*, that correspond to two variants of stuttering equivalence and two variants of branching bisimulation, namely divergence blind branching bisimulation (our notion with fair abstraction) and divergence sensitive branching bisimulation (defined as branching bisimulation with explicit divergence as in Section 7, but also considering endnodes to be divergent). The stuttering equivalence of BROWNE, CLARKE & GRÜMBERG (1988) is the divergence sensitive variant.) Hence (divergence sensitive) branching bisimulation is adequate for CTL*-X. Since the eventually operator of GRAF & SIFAKIS (1987) can be expressed in CTL*, this implies that it causes no problems in branching bisimulation semantics.



next up previous
Next: Practical applications Up: Conclusion Previous: Compositionality

Rob van Glabbeek