Semantic equivalences (and preorders) for concurrent systems are used as criteria for determining whether implementations (say of a protocol) meet specifications. The choice of a suitable equivalence (or preorder) can be motivated by means of a testing scenario. Such a scenario associates to every system a set of `observable' properties. These properties should be the ones that are important in the given application. Now the equivalence should be such that two processes are related only if they have the same observable behaviour (and for preorders the observable properties of the one should be included in those of the other). But this still leaves us with an abundance of suitable equivalences to choose from. Here one is faced with two opposite strategies.
One strategy is to choose the unique equivalence that relates two systems if and only if they have the same observable behaviour. This equivalence is said to be fully abstract with respect to the selected testing scenario. The advantage of a fully abstract equivalence is that it never fails to identify two processes if they have the same observable behaviour. For this reason it may be the best choice if the testing scenario is known and fixed once and forever. In practice however, there appears to be doubt and difference of opinion concerning the observable behaviour of systems. Moreover, what is observable may depend on the nature of the systems on which the concept will be applied and the context in which they will be operating. A big disadvantage of equivalences that are fully abstract with respect to non-stable notions of observability is that whenever a verification is carried out using a such an equivalence, and one decides that the context in which the verified system will be working is such that actually a little bit more can be observed that what was originally accounted for, the verification has to be completely redone. Moreover, the correctness of the investigated systems keeps depending on the completeness of the underlying testing scenario.
The opposite strategy is based on a concept of `internal structure' of processes. The internal structure of a process should be such that for any reasonable notion of observability you can imagine, if two processes have the same internal structure they surely have the same observable behaviour. According to this strategy a suitable equivalence should respect the internal structure of processes: if two processes are equivalent they must have the same internal structure. Preferably the equivalence should be `fully abstract' with respect to this structure: processes with a different internal structure should be distinguished. This to maximize the applicability of the notion. A disadvantage of this strategy is that the selected equivalence may fail to identify two processes with the same observable behaviour merely because they have a different internal structure. But the advantage is that verifications (of the equivalence of two processes) based on this strategy automatically count as verifications in any equivalence that is fully abstract with respect to a testing scenario, and keep being valid if the insight in what is observable changes. Moreover, when applying such an equivalence all bothersome considerations about observability can be skipped.
In models of concurrency that abstract from divergence, true concurrency, real-time behaviour and stochastic aspects of systems, and represent actions by uninterpreted symbols, it appears that the internal structure of processes can be formalized as their branching structure. This makes branching bisimulation equivalence a preferred tool for verifications. The internal structure strategy recommends to try a verification first in branching bisimulation semantics, and only when this fails move to a coarser equivalence that still seems appropriate for the given application. In this move to a coarser equivalence it would still be recommendable to minimize the amount of water (linear time) in the wine. But of course in situations where the appropriate testing scenario is beyond doubt, the full abstraction strategy is recommendable, and would rarely yield so fine a semantics as branching bisimulation.
One could argue that the strict branching structure would be an even better formalization of the internal structure of processes. This would make tree equivalence a preferred option. Although this argument by itself has some merit, the use of tree semantics has serious drawbacks. To name a few, the standard operational and denotational semantics of CCS-like system description languages do not coincide module tree equivalence, and deciding tree equivalence of regular processes has a higher complexity than deciding branching bisimulation equivalence. But most importantly, whereas in many verifications the specification and implementation are actually branching bisimulation equivalent, it rarely occurs that they are tree equivalent.
Another counterargument could be that there is an equivalence coarser
than branching bisimulation that, although not respecting the
branching structure of processes, respects their internal structure to
a sufficient degree to guarantee that any reasonable testing scenario
yields an equivalence that is at least as coarse. The most likely
candidates for such an equivalence are weak bisimulation or, as
argued in the absence of silent moves in BLOOM, ISTRAEL & MEYER [2], ready simulation. However, in VAN GLABBEEK [6] I present a testing scenario for branching
bisimulation that is arguably only twice as contrived as that of weak
bisimulation. Moreover, I argue that in the presence of silent moves
the case for ready simulation is not so compelling as in the
-free situation, and present a situation in which a more
discriminating equivalence is called for.
In models of concurrency that do not abstract from true concurrency etc. the internal structure of a process may include more than just its branching structure. The argument presented here can just as well be used to prefer causality respecting semantics for instance.