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 sender-driven choice, which allow a sender to send to different receivers upon branching and a receiver to receive from different senders. 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开辟新设计空间的可实现性变体。受潜在性能优势启发，我们引入了一种可实现性问题的推广形式，但令人遗憾的是，我们证明该推广形式是不可判定的。