一句话：提出带 provenance 标注的新操作语义，解除 psi-calculi 对信道对称传递的限制并保持双相似代数性质。
Psi-calculi 是为显式融合演算、应用 pi 演算和 spi 演算等提供统一代数与同余性质的参数化进程演算框架，但其通信信道必须满足对称性与传递性。本文提出一种新的操作语义，通过为迁移标注 provenance（描述其作用域与来源信道）来解除该限制，并简化若干证明。作者机器化验证了新扩展的保守性，以及强、弱双相似性的标准代数与同余性质仍然成立；还证明了与 reduction semantics 和 barbed bisimulation 的对应关系，并展示如何捕捉先前超出 psi-calculi 范围的带预序 pi 演算，以及在很强质量标准下编码 mixed choice。
Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Mechanised proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework. A limitation of psi-calculi is that communication channels must be symmetric and transitive. In this paper, we give a new operational semantics to psi-calculi that allows us to lift these restrictions and simplify some of the proofs. The key technical innovation is to annotate transitions with a provenance -- a description of the scope and channel they originate from. We give mechanised proofs that our extension is conservative, and that the standard algebraic and congruence properties of strong and weak bisimilarity are maintained. We show correspondence with a reduction semantics and barbed bisimulation. We show how a pi-calculus with preorders that was previously beyond the scope of psi-calculi can be captured, and how to encode mixed choice under very strong quality criteria.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1909-06692,
title = {Psi-Calculi Revisited: Connectivity and Compositionality},
author = {Johannes Åman Pohjola},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 4},
year = {2020},
doi = {10.23638/lmcs-16(4:16)2020}
}