## A Theory of Bisimulation for the Pi-Calculus

**Davide Sangiorgi**
*Abstract:* We study a new formulation of bisimulation for
the pi-calculus, which we have called *open bisimulation* (~).
In contrast with the previously known bisimilarity equivalences, ~
is preserved by *all* pi-calculus operators, including input
prefix. The differences among all these equivalences already appear
in the sublanguage without name restrictions: Here the definition
of ~ can be factorised into a ``standard'' part which, modulo the
different syntax of actions, is the CCS bisimulation, and a part
specific to the pi-calculus, which requires name instantiation.
Attractive features of ~ are: a simple axiomatisation (of the
finite terms), with a completeness proof which leads to the
construction of *minimal canonical representatives* for the
equivalence classes of ~; an ``efficient'' characterisation, based
on a modified transition system. This characterisation seems
promising for the development of automated-verification tools and
also shows the call-by-need flavour of ~. Although in the paper we
stick to pi-calculus, the issues developed may be relevant to
value-passing calculi in general.

*LFCS report ECS-LFCS-93-270,
June 1993.*

This report has now been published in *Acta Informatica*,
1996.

Previous |

Index |

Next