next up previous
Next: Tool for analysing weak bisimulation Up: Conclusion Previous: Better term rewrite properties

And it has a nice characterization as back-and-forth bisimulation.

Branching bisimulation equivalence has a nice characterization as weak back-and-forth bisimulation (see the end of Section 8). No matter whether the weak, delay, eta or branching mode is selected, if it is required that moves in the one process can be simulated by the other, not only when going forward but also when going back in history, these modified notions all coincide with branching bisimulation (DE NICOLA, MONTANARI & VAANDRAGER (1990)).

This argument is balanced however by a nice characterization of weak bisimulation of which there is no analogy for branching bisimulation. Namely if (root-unwound) process graphs are saturated by adding an edge s --t-> s' whenever there is a path
s ===> --a-> ===>s' (cf. Definition 4.8) and by adding a t-loop in every state except the root, then two graphs are weakly equivalent iff their saturated graphs are strongly equivalent.

Rob van Glabbeek