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