   Next: Compositionality Up: Conclusion Previous: No coarser semantics

#### In abstract interleaving semantics no finer notion of bisimulation is suitable.

This leaves us with the question whether a finer equivalence than branching bisimulation might be more or equally suitable. In the absence of silent moves the only candidate appears to be tree equivalence (VAN GLABBEEK (1993c)), as even finer equivalences, such as graph isomorphism, are clearly useless from the point of view of practical applications. But tree semantics has the disadvantage that the standard operational and denotational interpretations of CCS-like system description languages do not coincide. Moreover the operational interpretation is not compositional, and the most plausible fix requires an upgrade of the underlying graph model into a multigraph model (allowing more than one equally labelled edges between two nodes).

Thus it is more tempting to search for generalizations of bisimulation equivalence to a setting with silent moves that are finer than branching bisimulation. Such generalizations undoubtedly exists. But in many application we are interested in three useful properties:

1. The equivalence is abstract in the sense that it satisfies at least atx=ax (Milner's first t-law).
2. It is a congruence for the operators of CCS and CSP.
3. The merge or parallel composition satisfies the expansion theorem of MILNER (1980, 1983, 1985, 1989), i.e. interleaving semantics is employed, and also the other laws of strong bisimulation are satisfied.
In such circumstances branching bisimulation on finite closed terms is completely axiomatized by the first t-law (atx=ax) and the laws of strong bisimulation, and hence is the finest congruence possible (VAN GLABBEEK (1993a)).

Returning to tree equivalence, a similar argument as above applies: all recursion-free closed instances of the law a(t(y+z)+y)=a(y+z) are derivable from atx=ax and the laws for (strong) tree equivalence (which are the laws of strong bisimulation without x+x=x). Thus, in applications where properties 1-3 above are desired, a `weak' version of tree congruence would be needed, that satisfies a(t(y+z)+y)=a(y+z). Such a weak tree-congruence would not have the intuitive appeal of strong tree equivalence, and does not appear to have any advantages over branching bisimulation congruence.   Next: Compositionality Up: Conclusion Previous: No coarser semantics

Rob van Glabbeek