$pi$-演算在行为上是完备且轨道有限可执行的
摘要：反应式图灵机通过一种模拟可观察的互动行为的机制扩展了经典图灵机。我们将一个行为称为(有限)可执行的，当且仅当它等价于一个(有限)反应式图灵机的行为。本文研究了可执行行为与能够在π-演算中规范的行为之间的关系。我们证明了每个有限可执行行为都可以在π-演算中通过保持发散性的分支相似性指定。然而，由于(有意的)反应式图灵机模型的局限性，反之则不成立。也就是说，π-演算允许规范的行为存在在不保持有限可执行性的分支相似性上。然而，我们将证明，如果对反应式图灵机的有限性要求以及相关的可执行性概念放宽为轨道有限性，则π-演算可在(发散不敏感的)分支相似性上可执行。
作者：Bas Luttik and Fei Yang
论文ID：1410.4512
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22