Abstract:
We study three notions of bisimulation equivalence for concurrent processes. Bisimulation equivalences are based on an operational interpretation of processes as labelled transition systems, and constitute the strongest notion of equivalence one may adopt for such systems: two systems are equivalent if and only if they have the same step-by-step behaviour.

We focus first on Milner's notion of weak bisimulation (also known as observational equivalence) and propose an alternative formulation for it. More specifically, we show that Milner's notion may be redefined as abstraction homomorphism. We use our characterisation to derive a complete set of reduction rules for observational equivalence on finite processes. We also show how abstraction homomorphisms may be extended to labelled event structures: however we do not consider the possibility of unobservable events here.

We look then for notions of bisimulation which account for the concurrent aspects of processes. Traditional transition systems - evolving via successive elementary actions - only provide an interleaving semantics for concurrency. We suggest two generalisations of the notion of transition system: distributed transition systems, obtained by generalising the residual of a transition, and pomset transiton systems, obtained by extending the notion of action labelling a transition (an action being now a partially ordered multiset). For the latter we find a corresponding notion of bisimulation on labelled event structures.

Based on these new kinds of transitions, we obtain two bisimulation equivalences - one stronger than the other - which are both more discriminating than Milner's equivalence. For both of them we present an algebraic characterisation on finite processes, in the form of a complete set of axioms.