Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine. Existing projection operators are syntactic in nature, and trade efficiency for completeness. We present the first projection operator that is sound, complete, and efficient. Our projection separates synthesis from checking implementability. For synthesis, we use a simple automata-theoretic construction; for checking implementability, we present succinct conditions that summarize insights into the property of implementability. We use these conditions to show that MST implementability is PSPACE-complete. This improves upon a previous decision procedure that is in EXPSPACE and applies to a smaller class of MSTs. We demonstrate the effectiveness of our approach using a prototype implementation, which handles global types not supported by previous work without sacrificing performance.

翻译：多方会话类型（MSTs）是一种基于类型的方法，用于验证通信协议。MSTs的核心是投影算子：一个部分函数，将表示为全局类型的协议映射到每个参与者的正确性构造实现，这些实现表示为通信状态机。现有的投影算子本质上是语法性的，并且在完备性上牺牲了效率。我们提出了首个既可靠、完备又高效的投影算子。我们的投影将综合与可实施性检查分离开来。对于综合，我们使用简单的自动机理论构造；对于可实施性检查，我们提出了简洁的条件，总结了对可实施性属性的深刻见解。利用这些条件，我们证明了MST可实施性是PSPACE完全的。这改进了先前属于EXPSPACE且仅适用于较小类别MST的判定过程。我们通过原型实现展示了方法的有效性，该实现能够处理先前工作不支持且不牺牲性能的全局类型。