next up previous
Next: Complexity Up: Conclusion Previous: `Eventually' and CTL*

There are practical applications in which weak bisimulation poses a problem that can be solved by moving to branching bisimulation. No applications have been found in which the reverse holds.

The extra identifications made in weak bisimulation semantics on top of branching bisimulation semantics can be cumbersome in certain applications of the theory. An example concerns the work of JONSSON & PARROW (1993), mentioned in the introduction. On the other hand we are not aware of a single application where weak bisimulation semantics can be successfully applied, but the extra distinctions made in branching bisimulation semantics pose a problem.

In BOUALI (1992) an example is given were weak bisimulation semantics works better than branching bisimulation semantics. The example concerns the minimization of PETERSON's mutual exclusion algorithm (1981). Here minimization means finding an equivalent process that is as small as possible. In branching bisimulation semantics this yields a process with 17 states, whereas in weak bisimulation semantics a process with only 14 states is obtained. (In fact, using the quasi-branching bisimulation mentioned in sections 6 and 7 would bring the number of states to 14 already.) It should be noted however, that weak bisimulation is still far from optimal for this purpose. Coupled simulation, proposed by PARROW & SJÖDIN (1992), is a generalization of bisimulation semantics to a setting with silent moves that is coarser than weak bisimulation. It is completely axiomatized by the laws of weak bisimulation together with t(tx+y)=tx+y. Minimization of Peterson's algorithm in coupled simulation semantics would yield a process with no more than 9 states, and using failure semantics (BROOKES, HOARE & ROSCOE (1984), DE NICOLA & HENNESSY (1984)) would bring it down to 4.

We conjecture that this is illustrative for a general tendency. Coupled simulation has distinct advantages over weak (and branching) bisimulation in applications were the latter notions are too fine. Examples of such applications can be found in PARROW & SJÖDIN (1992) and VAN GLABBEEK & VAANDRAGER (1993). However, whenever weak bisimulation performs better than branching bisimulation, it turns out to be the case that neither of the two notions are really suitable, and coupled simulation, or an even coarser equivalence, is called for.



next up previous
Next: Complexity Up: Conclusion Previous: `Eventually' and CTL*

Rob van Glabbeek