全局协议在会面同步下的研究：从可实现性到类型检查
Global Protocols under Rendezvous Synchrony: From Realizability to Type Checking
AI总结：
本文研究了通过会面同步通信的分布式过程的全局协议规范，证明了同步可实现性问题的可判定性，并提出了一种支持局部混合选择的类型系统。
摘要：
全局协议规范是自顶向下的验证方法的起点，为合成保证分布式实现正确性的局部规范提供了蓝图。在本工作中，我们研究了针对通过会面同步通信的分布式过程的全局协议规范。我们获得了同步可实现性问题的积极结果：(a) 在传递并发字母表上，全局协议的可实现性在协议大小上为2-EXPTIME，在字母表大小上为3-EXPTIME；(b) 对于无歧义表示其轨迹语言的全局协议，可实现性在EXPTIME内可判定。无歧义的全局协议涵盖了先前工作中研究的有向和发送者驱动选择协议的片段。此外，我们的归约得出结论，同步验证问题可以以相同的复杂度解决，其中候选实现作为输入的一部分。最后，我们证明了一个否定结果，即一般情况下同步可实现性是不可判定的。我们还提出了一种类型系统，用于检查pi演算过程 against 以同步通信状态机形式的局部规范。我们的类型系统是第一个支持在会话交错和委托存在下具有局部混合选择的过程的。
英文摘要：
Global protocol specifications are the starting point of top-down verification methodologies, and serve as a blueprint for synthesizing local specifications that guarantee the correctness of distributed implementations. In this work, we study global protocol specifications targeting distributed processes that communicate via rendezvous synchrony. We obtain the following positive results for the synchronous realizability problem: (a) realizability is decidable for global protocols over a transitive concurrency alphabet in 2-EXPTIME in the size of the protocol, and in 3-EXPTIME in the size of the alphabet, and (b) realizability is decidable in EXPTIME for global protocols that unambiguously represent their trace language. Unambiguous global protocols encompass fragments of directed and sender-driven choice protocols studied in prior work. Further, our reductions admit the corollary that the synchronous verification problem is solvable with the same complexity, where a candidate realization is included as part of the input. We then prove a negative result stating that synchronous realizability is undecidable in general. Finally, we propose a type system to check pi-calculus processes against local specifications in the form of synchronous communicating state machines. Our type system is the first to support processes with local mixed choice in the presence of session interleaving and~delegation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
