一句话：证明π演算可规范所有有限可执行行为，并在轨道有限松弛下与反应式图灵机行为等价。
论文研究可执行行为与π演算可规范行为之间的关系。可执行行为指与（有限）反应式图灵机行为等价的行为；反应式图灵机在经典图灵机上增加可观察交互行为建模。作者以保持发散的分支双相似性作为等价判定，证明每个有限可执行行为都可由π演算规范到该等价意义下，但反之不成立：π演算能刻画某些并非有限可执行的行为。随后将反应式图灵机及可执行性的有限性要求松弛为轨道有限性，证明π演算在该松弛下（对发散不敏感的分支双相似性）是可执行的。
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
@article{paperbot1337,
title = {The $\pi$-Calculus is Behaviourally Complete and Orbit-Finitely Executable},
author = {Bas Luttik and Fei Yang},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:14)2021}
}