## Bisimulations for Concurrency

**I. Castellani**
*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. **Ph.D. Thesis - Price
£7.00**

*LFCS report ECS-LFCS-88-51 (also published as
CST-51-88)*

Previous |

Index |

Next