Executable Behaviour and the π-Calculus (extended abstract)

Bas Luttik
(Eindhoven University of Technology)
Fei Yang
(Eindhoven University of Technology)

Reactive Turing machines extend classical Turing machines with a facility to model observable interactive behaviour. We call a behaviour executable if, and only if, it is behaviourally equivalent to the behaviour of a reactive Turing machine. In this paper, we study the relationship between executable behaviour and behaviour that can be specified in the pi-calculus. We establish that all executable behaviour can be specified in the pi-calculus up to divergence-preserving branching bisimilarity. The converse, however, is not true due to (intended) limitations of the model of reactive Turing machines. That is, the pi-calculus allows the specification of behaviour that is not executable up to divergence-preserving branching bisimilarity. Motivated by an intuitive understanding of executability, we then consider a restriction on the operational semantics of the pi-calculus that does associate with every pi-term executable behaviour, at least up to the version of branching bisimilarity that does not require the preservation of divergence.

In Sophia Knight, Ivan Lanese, Alberto Lluch Lafuente and Hugo Torres Vieira: Proceedings 8th Interaction and Concurrency Experience (ICE 2015), Grenoble, France, 4-5th June 2015, Electronic Proceedings in Theoretical Computer Science 189, pp. 37–52.
Published: 19th August 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.189.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org