异步多方会话类型可实现性是可判定的——来自消息序列图的经验教训
Asynchronous Multiparty Session Type Implementability is Decidable -- Lessons Learned from Message Sequence Charts
AI总结：
该研究解决了具有发送方驱动选择的异步多方会话类型可实现性的可判定性开放问题，通过推广高级消息序列图的结论给出肯定答案，同时研究了相关技术适配并证明了一类推广的可实现性问题不可判定。
摘要：
多方会话类型（MSTs）为规范和验证异步消息传递系统提供了高效手段。对于规定系统中各角色间所有交互的全局类型，可实现性问题旨在探究是否存在所有角色的局部规范，使得它们的组合无死锁且能精确生成规定的执行序列。该可实现性问题的可判定性一直是一个开放问题。我们针对具有发送方驱动选择的全局类型给出了肯定答案，这类全局类型允许发送方在分支时向不同接收方发送消息，也允许接收方从不同发送方接收消息。为实现这一结果，我们推广了高级消息序列图（HMSCs）领域的相关结论。这一关联还使我们能够全面研究如何将HMSC技术适配到MST场景中，其中包括提升该问题算法可处理性的技术，以及一种可能为MST开辟新设计空间的可实现性变体。受潜在性能优势的启发，我们引入了可实现性问题的一种推广形式，但遗憾的是，我们证明了该问题是不可判定的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
