In this paper we introduced a new semantic equivalence for concurrent systems that we called branching bisimulation equivalence. We compared branching bisimulation with the coarser notion of weak bisimulation equivalence and two intermediate notions. Our main motivation for introducing branching bisimulation is that it preserves the branching structure of processes. Although we believe that this has been demonstrated in Sections 1 and 3, this paper does not contain a formal definition of the `branching structure' of a process. Such a definition will be offered in VAN GLABBEEK (1993c).
Here we would like to stress that this feature of branching bisimulation is of more than philosophical interest. Actually, we think that of all the equivalences in the linear time - branching time spectrum, branching bisimulation is most suited for verifying the correctness of concurrent systems in applications were the final word on what exactly is observable behaviour has not been pronounced. Below we list our arguments.