The most popular method for establishing bisimilarities
among processes is to exhibit bisimulation relations. By definition,
[Rscr ] is a bisimulation relation if [Rscr ] progresses to
[Rscr ] itself, i.e., pairs of processes in [Rscr ]
can match each other's actions and their derivatives are again in
[Rscr ].
We study generalisations of the method aimed at reducing the size of
the relations to be
exhibited and hence relieving the proof work needed to establish bisimilarity
results. We
allow a relation [Rscr ] to progress to a different relation [Fscr ] ([Rscr ]),
where
[Fscr ] is a function on relations. Functions that can be safely used in
this way
(i.e., such that if [Rscr ] progresses to [Fscr ] ([Rscr ]), then
[Rscr ]
only includes pairs of bisimilar processes) are sound. We give
a simple
condition that ensures soundness. We show that the class of sound functions
contains
non-trivial functions and we study the closure properties of the class
with respect to 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 π-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 that justifies the adoption of a simple
form of prefix-guarded
replication as the only form of replication in the π-calculus.
