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:
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.