10.23638/LMCS-17(1:14)2021
Luttik, Bas
Bas
Luttik
Yang, Fei
Fei
Yang
The $\pi$-Calculus is Behaviourally Complete and Orbit-Finitely
Executable
episciences.org
2021
Computer Science - Logic in Computer Science
contact@episciences.org
episciences.org
2020-01-23T09:00:22+01:00
2021-02-10T08:10:29+01:00
2021-02-10
eng
Journal article
https://lmcs.episciences.org/6047
arXiv:1410.4512
1860-5974
PDF
1
Logical Methods in Computer Science ; Volume 17, Issue 1 ; 1860-5974
Reactive Turing machines extend classical Turing machines with a facility to
model observable interactive behaviour. We call a behaviour (finitely)
executable if, and only if, it is equivalent to the behaviour of a (finite)
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 every finitely 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 finitely executable up to divergence-preserving
branching bisimilarity. We shall prove, however, that if the finiteness
requirement on reactive Turing machines and the associated notion of
executability is relaxed to orbit-finiteness, then the $\pi$-calculus is
executable up to (divergence-insensitive) branching bisimilarity.
Comment: arXiv admin note: text overlap with arXiv:1508.04850