Executable Behaviour and the pi-Calculus

B. Luttik, F. Yang

Research output: Contribution to JournalArticleAcademicpeer-review


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 πcalculus. We establish that all executable behaviour can be specified in the π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 π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 πcalculus that does associate with every π-term executable behaviour, at least up to the version of branching bisimilarity that does not require the preservation of divergence.
Original languageEnglish
Pages (from-to)37-52
JournalElectronic Proceedings in Theoretical Computer Science
Issue number189
Publication statusPublished - 2015

Bibliographical note

PT: J; NR: 19; TC: 0; J9: ELECTRON PROC THEOR; PG: 16; GA: CZ8GW; UT: WOS:000367339200004


Dive into the research topics of 'Executable Behaviour and the pi-Calculus'. Together they form a unique fingerprint.

Cite this