Executable Behaviour and the pi-Calculus

B. Luttik, F. Yang

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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
DOIs
Publication statusPublished - 2015

Fingerprint

Turing machines
Semantics
Specifications

Bibliographical note

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

Cite this

@article{57213f0a050a42b380ca8f919e173797,
title = "Executable Behaviour and the pi-Calculus",
abstract = "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.",
author = "B. Luttik and F. Yang",
note = "PT: J; NR: 19; TC: 0; J9: ELECTRON PROC THEOR; PG: 16; GA: CZ8GW; UT: WOS:000367339200004",
year = "2015",
doi = "10.4204/EPTCS.189.5",
language = "English",
pages = "37--52",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",
number = "189",

}

Executable Behaviour and the pi-Calculus. / Luttik, B.; Yang, F.

In: Electronic Proceedings in Theoretical Computer Science, No. 189, 2015, p. 37-52.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Executable Behaviour and the pi-Calculus

AU - Luttik, B.

AU - Yang, F.

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

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.4204/EPTCS.189.5

DO - 10.4204/EPTCS.189.5

M3 - Article

SP - 37

EP - 52

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

IS - 189

ER -