## On the Bisimulation Proof Method

**Davide Sangiorgi**
*Abstract:* The most popular method for establishing
*bisimilarity* results is to exhibit bisimulation relations.
By definition, *R* is a bisimulation relation if *R*
*progresses* to *R* itself, i.e. pairs of processes in
*R* can match each other's actions and their derivatives are
again in *R*.

We study generalisations of the method aimed at reducing the
size of the relations to exhibit and hence relieving the proof work
needed to establish bisimilarity results. We allow a relation
*R* to progress to a different relation *F (R)*, where
*F* is a function on relations. Functions which can be safely
used in this way (i.e. such that if *R* progresses to
*F(R)*, then *R* only includes pairs of bisimilar
processes) are *sound*. We give a simple condition which
ensures soundness. We show that the class of sound functions
contains non-trivial functions and we prove closure properties of
the class w.r.t. various important function constructors, like
composition, union and iteration. These properties allow us to
construct sophisticated sound functions - and hence sophisticated
proof techniques for bisimilarity - from simpler ones.

The usefulness of our proof techniques is supported by various
non-trivial examples, drawn from the process algebras CCS and
*pi*-calculus. They include the proof of the unique solution
of equations and the proof of a few properties of the replication
operator. Among these, there is a novel result which justifies the
adoption of a simple form of prefix-guarded replication as the only
form of replication in the *pi*-calculus.

*LFCS report ECS-LFCS-94-299,
August 1994.*

Previous |

Index |

Next