Executable behaviour and the π-calculus (extended abstract)

Bas Luttik, F. Yang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)
2 Downloads (Pure)


In Proceedings ICE 2015, arXiv:1508.04595. arXiv admin note: substantial text overlap with arXiv:1410.4512 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.
Original languageEnglish
Title of host publication8th Interaction and Concurrency Experience (ICE 2015, Grenoble, France, June 4-5, 2015)
EditorsS. Knight, I. Lanese, A. Lluch Lafuente, H. Torres Vieira
Publication statusPublished - 2015

Publication series

NameElectronic Proceedings in Theoretical Computer Science
ISSN (Print)2075-2180


Dive into the research topics of 'Executable behaviour and the π-calculus (extended abstract)'. Together they form a unique fingerprint.

Cite this