next up previous
Next: No finer notion of bisimulation Up: Conclusion Previous: Verifications in branching bisimulation semantics are sound

No coarser semantics (like weak bisimulation) has this property.

The previous argument says that branching bisimulation equivalence (or congruence) is suited for applications in which there is no certainty on what constitutes observable behaviour. However, it does not show that it is the only such notion. It could be that there exists a coarser equivalence that still preserves the upperbound on observable behaviour. In fact the name observation equivalence suggest that weak (or delay?) bisimulation equivalence is the coarsest equivalence with this property. This argument is enforced by Milner's testing scenario for observation equivalence, presented in MILNER (1980) and (1981). However, the testing scenario briefly sketched Section 8 and elaborated in VAN GLABBEEK (1993b) shows (together with the previous argument) that in fact branching bisimulation represents the limit of observable behaviour, and hence no coarser equivalence shares the advantage mentioned in the previous argument.

Of course one could argue that the testing scenario of Section 8 is not very realistic. However, the same can be said of the testing scenario for weak bisimulation, and the question of what is a realistic testing scenario is exactly the one that we want to avoid.

For those readers that believe that some variant of ready simulation equivalence represents the limit of observable behaviour and is therefore the right notion (cf. BLOOM, ISTRAIL & MEYER (1995) and ULIDOWSKI (1992)) we refer to the lifeness argument in VAN GLABBEEK (1993b).



next up previous
Next: No finer notion of bisimulation Up: Conclusion Previous: Verifications in branching bisimulation semantics are sound

Rob van Glabbeek