A theory of bisimulation for the \(\pi\)-calculus
type: Item
instance of: scholarly article
title: A theory of bisimulation for the \(\pi\)-calculus
zbMATH Open document ID: 0835.68072
author: Davide Sangiorgi
published in: Acta Informatica
publication date: 1995-11-15T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68Q10
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 814152
zbMATH Keywords: bisimulation
zbMATH Keywords: \(pi\)-calculus
zbMATH Keywords: axiomatisation
zbMATH Keywords: completeness proof
zbMATH Keywords: transition system
zbMATH Keywords: automated-verfication
zbMATH Keywords: completeness proofs
zbMATH Keywords: automated-verification
MaRDI profile type: Publication
Wikidata QID: Q56019903
full work available at URL: s002360050036
OpenAlex ID: W2027689693
cites work: Algebra of communicating processes with abstraction
cites work: Q4282583
cites work: A proof system for communicating processes with value-passing
cites work: Q4431382
cites work: Calculi for synchrony and asynchrony
cites work: Q3992568
cites work: Q4260379
cites work: Functions as processes
cites work: A calculus of mobile processes. I
cites work: Q4018066
DOI: 10.1007/S002360050036
description: scientific article; zbMATH DE number 814152