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.

翻译：全局协议规范是自顶向下验证方法的起点，并作为合成局部规范的蓝图，以保证分布式实现的正确性。在本工作中，我们研究针对通过会聚同步进行通信的分布式进程的全局协议规范。对于同步可实现性问题，我们获得了以下积极结果：(a) 对于在传递并发字母表上的全局协议，可实现性是可判定的，其复杂度在协议规模上为2-EXPTIME，在字母表规模上为3-EXPTIME；(b) 对于能明确表示其迹语言的全局协议，可实现性在EXPTIME内可判定。明确的全局协议涵盖了先前工作中研究的定向和发送者驱动选择协议的片段。此外，我们的归约允许一个推论：同步验证问题可以用相同的复杂度解决，其中候选实现作为输入的一部分。接着，我们证明了一个负面结果：一般而言，同步可实现性是不可判定的。最后，我们提出一个类型系统，用于根据以同步通信状态机形式给出的局部规范来检查π演算进程。我们的类型系统是首个在存在会话交错和委托的情况下，支持具有局部混合选择的进程的系统。