A theory of bisimulation for the \(\pi\)-calculus (Q1901699)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A theory of bisimulation for the \(\pi\)-calculus |
scientific article |
Statements
A theory of bisimulation for the \(\pi\)-calculus (English)
0 references
15 November 1995
0 references
We study a new formulation of bisimulation for the \(\pi\)-calculus [\textit{R. Milner, J. Parrow} and \textit{D. Walker} (1989)], which we have called open bisimulation (\(\sim\)). In contrast with the previously known bisimilarity equivalences, \(\sim\) is preserved by all \(\pi\)-calculus operators, including input prefix. The differences among all these equivalences already appear in te sublanguage without name restrictions: Here the definition of \(\sim\) 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 \(\sim\) are: A simple axiomatisation (of the finite terms), with a completeness proofs which leads to the construction of minimal canonical representatives for the equivalence classes of \(\sim\); 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 \(\sim\). Although in the paper we stick to the \(\pi\)- calculus, the issues developed may be relevant to value-passing calculi in general.
0 references
bisimulation
0 references
\(pi\)-calculus
0 references
axiomatisation
0 references
completeness proof
0 references
transition system
0 references
automated-verfication
0 references
completeness proofs
0 references
automated-verification
0 references