关于pi-演算中的层次通信拓扑
On Hierarchical Communication Topologies in the pi-calculus
摘要：
本文研究π-项的通信拓扑所满足的形状不变量，以及这些不变量的自动推理。π-项P是层次的，如果存在有限森林T，使得从P可达的每个项的通信拓扑满足T形不变量。我们设计了一个静态分析，通过一个新的类型系统，享有决策推理证明一个术语层次。类型系统的可靠性证明采用了π演算反应的非标准观点。层次项的可覆盖性问题是可判定的。这是证明了每一个层次的长期是深度有界的，在文献中已知的不可判定的属性。因此，我们得到一个有表现力的静态片段的π演算可判定的安全验证问题。
英文摘要：
This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T-shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of π-calculus reactions. The coverability problem for hierarchical terms is decidable. This is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the π-calculus with decidable safety verification problems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
