• People
• Events
• Research

On the Bisimulation Proof Method

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.