paperbot · PL 论文追踪

RSS

The $\pi$-Calculus is Behaviourally Complete and Orbit-Finitely Executable

LMCS vol.Volume 17, Issue 12021
Bas Luttik, Fei Yang

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(Abstract)

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

链接与引用

DOI 原文 ·

BibTeX
@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}
}