The crucial difference between branching bisimulation and weak bisimulation is that the first one better takes into account the intermediate states of two equivalent processes as they progress through a computation. As argued already by HENNESSY & MILNER (1980) on the occasion of the introduction of the first version of observation equivalence, it is useful to do so, "because different intermediate states can be exploited in different program contexts to produce different overall behaviour". Here we present an example of a program context that exploits the different intermediate states of two observation equivalent (i.e. weakly bisimilar) processes to produce different overall behaviour. It is a context (operator) that allows a process (its argument) to proceed normally, but in addition can report that the process is ready to perform a visible action, without actually doing it. Thus the states of this context are the same as the states of its argument, and the transitions are the transitions of its argument, together with a transition labelled "can do a," from a state to itself, whenever the argument can do an a from that state. Observe that the processes a0+tb0 and a0+tb0+b0 displayed in Figure 7 are weakly bisimilar.
FIGURE 7. An operator exploiting different intermediate states of weakly bisimilar processes.
They are even delay bisimilar, but not branching bisimilar. After placing them in the described context (the results are displayed below them) they are no longer weakly bisimilar. In fact they even have different traces, as only the second one has a trace "can do b" followed by "a". In BLOOM (1995) a class of operators is given for which rooted branching bisimulation equivalence is a congruence. He also presents a class of operators for which rooted weak bisimulation equivalence is a congruence. The latter class is a subclass of the former, and the operator described above falls in the difference. Also all abstract equivalences in the linear time - branching time spectrum that are situated between trace equivalence and delay bisimulation (and including these) fail to be congruences for this operator. On the other hand, we know of no useful operator for which some abstract equivalence in the linear time - branching time spectrum is a congruence, but rooted branching bisimulation is not.