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.