A theory of bisimulation for the π-calculus |
| |
Authors: | Davide Sangiorgi |
| |
Affiliation: | (1) INRIA, 2004, route des Lucioles, B.P. 93, F-06902 Sophia Antipolis Cedex, France, FR |
| |
Abstract: | We study a new formulation of bisimulation for the π-calculus MPW92], which we have called open bisimulation (∼). In contrast with the previously known bisimilarity equivalences, ∼ is preserved by allπ-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 π-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 the π-calculus, the issues developed may be relevant to value-passing calculi in general.
Received: June 11, 1993/November 28, 1994 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|