next up previous
Next: No coarser semantics Up: Conclusion Previous: Conclusion

Verifications in branching bisimulation semantics are sound independent of your notion of observable behaviour.

In applications where the notion of observable behaviour is clear, the most suitable equivalence is usually the one which is fully abstract with respect to this notion of observable behaviour, i.e. identifies two processes if and only if their observable behaviour is the same. However, if there is no clarity on what is observable, a verification in a fully abstract semantics w.r.t. any notion of observability needs to be redone every time one discovers that a little bit more can be observed than what was originally accounted for. Moreover, the soundness of the verification depends crucially on the right estimation of what can be observed. A verification (of the equivalence of two processes) in a semantics that preserves the internal structure of processes, on the other hand, does not depend on considerations of observability (as long as it is clear that no more can be observable than this internal structure), and is automatically valid in any semantics that is fully abstract w.r.t. some notion of observable behaviour. Now for the simple kind of processes that are the subject of this paper, the best formalization of the internal structure of a process appears to be its branching structure. (However, for more complex systems the internal structure may involve more, e.g. the causal structure of processes.)


Rob van Glabbeek