π-演算在行为上是完备的且轨道有限可执行的
The $π$-Calculus is Behaviourally Complete and Orbit-Finitely Executable
AI总结：
本文研究π-演算与反应式图灵机的关系，证明在轨道有限放宽下π-演算是可执行的，并指出有限可执行性的局限。
摘要：
反应式图灵机扩展了经典图灵机，增加了建模可观察交互行为的能力。我们称一个行为（有限）可执行，当且仅当它与一个（有限）反应式图灵机的行为等价。本文研究可执行行为与可在π-演算中指定的行为之间的关系。我们证明，每个有限可执行行为都可以在π-演算中指定，直至保持发散的枝点双相似。然而，反过来并不成立，这是由于反应式图灵机模型的（预期）限制。也就是说，π-演算允许指定在保持发散的枝点双相似下不是有限可执行的行为。但我们将证明，如果反应式图灵机的有限性要求及相关可执行性概念放宽为轨道有限性，则π-演算在（对发散不敏感的）枝点双相似下是可执行的。
英文摘要：
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 $π$-calculus. We establish that every finitely 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 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 $π$-calculus is executable up to (divergence-insensitive) branching bisimilarity.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
