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:

- The equivalence is abstract in the sense that it
satisfies at least
**atx=ax**(Milner's first**t**-law). - It is a congruence for the operators of CCS and CSP.
- 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.

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.