Multiparty session types (MSTs) provide efficient means to specify and verify asynchronous message-passing systems. For a global type, which specifies all interactions between roles in a system, the implementability problem asks whether there are local specifications for all roles such that their composition is deadlock-free and generates precisely the specified executions. Decidability of the implementability problem is an open question. We answer it positively for global types with generalised choice, which allow a sender to send to different receivers and a receiver to receive from different senders upon branching. To achieve this, we generalise results from the domain of high-level message sequence charts (HMSCs). This connection also allows us to comprehensively investigate how HMSC techniques can be adapted to the MST setting. This comprises techniques to make the problem algorithmically more tractable as well as a variant of implementability that may open new design space for MSTs. Inspired by potential performance benefits, we introduce a generalisation of the implementability problem that we, unfortunately, prove to be undecidable.

翻译：多参与者会话类型（MSTs）为指定并验证异步消息传递系统提供了高效手段。对于规定系统中所有角色间交互的全局类型而言，可实现性问题询问是否存在所有角色的局部规范，使得这些规范的组合无死锁且精确生成指定的执行过程。该问题的可判定性一直是一个开放问题。我们针对具有广义选择（允许发送者在分支时向不同接收者发送消息，接收者从不同发送者接收消息）的全局类型给出了肯定答案。为此，我们推广了高层消息序列图（HMSCs）领域的研究成果。这一联系使我们能够全面探讨如何将HMSC技术适配至MST场景，涵盖使问题在算法上更易处理的技术，以及可能为MST开辟新设计空间的可实现性变体。受潜在性能优势启发，我们引入了一种可实现性问题的推广形式，但遗憾地证明其不可判定。