标题： 可实现性与互补性多参与方会话类型 显示英文标题

标题： Realisability and Complementability of Multiparty Session Types

摘要： 多方会话类型（MPST）是一种基于类型的用于指定消息传递分布式系统的方案。 它们依赖于全局类型的概念，全局类型指定了全局行为，而局部类型是将全局行为投影到每个本地参与者的产物。 全局类型的一个基本属性是可实现性，即局部行为的组合是否符合全局类型所指定的行为。 我们探讨了MPST的可实现性如何与其互补性相关，即是否存在一个全局类型来描述原始全局类型的互补行为。 首先，我们证明如果一个全局类型在点对点通信中是可实现的，那么它在同步通信中也是可实现的。 其次，我们证明如果一个全局类型在同步模型中是可实现的，那么它是互补的，即存在一个全局类型来描述原始全局类型的互补行为。 第三，我们给出一个算法，用于判断一个带有显式互补的互补全局类型是否在点对点通信中是可实现的。 该算法在全局类型及其互补的大小上是PSPACE复杂度的。 作为一项附加贡献，我们提出了一个针对发送方驱动选择的全局类型的互补构造，其大小在全局类型的大小上呈线性增长。 显示英文摘要

摘要： Multiparty session types (MPST) are a type-based approach for specifying message-passing distributed systems. They rely on the notion of global type specifying the global behaviour and local types, which are the projections of the global behaviour onto each local participant. An essential property of global types is realisability, i.e., whether the composition of the local behaviours conforms to those specified by the global type. We explore how realisability of MPST relates to their complementability, i.e., whether there exists a global type that describes the complementary behaviour of the original global type. First, we show that if a global type is realisable with p2p communications, then it is realisable with synchronous communications. Second, we show that if a global type is realisable in the synchronous model, then it is complementable, in the sense that there exists a global type that describes the complementary behaviour of the original global type. Third, we give an algorithm to decide whether a complementable global type, given with an explicit complement, is realisable in p2p. The algorithm is PSPACE in the size of the global type and its complement. As a side contribution, we propose a complementation construction for global types with sender-driven choice with a linear blowup in the size of the global type.