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.

翻译：多方会话类型（MST）是一种基于类型的通信协议验证方法。其核心是投影算子：一个偏函数，将全局类型表示的协议映射为每位参与者可正确构造的实现，并以通信状态机的形式呈现。现有投影算子本质上基于语法规则，且以牺牲完备性为代价换取效率。我们提出了首个兼具可靠性、完备性与高效性的投影算子。该投影将合成过程与可实施性检查相分离：合成本身采用简洁的自动机理论构造，而可实施性检查则通过提炼可实施性性质的紧凑条件实现。基于这些条件，我们证明了MST可实施性问题为PSPACE完全问题。这较之于此前仅适用于更小MST类别且复杂度为EXPSPACE的判定过程有显著提升。我们通过原型实现验证了本方法的有效性——该实现能在不牺牲性能的前提下处理先前方法无法支持的全局类型。