通信自动机中的多方兼容性：全局会话类型的刻画与综合
Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types
摘要：
多方会话类型是一种类型系统，它通过对分布式对等点之间的交互进行全局规范来保证分布式对等点的安全性和活性。为了构建一个全球性的规范，从一组分布式的不受控制的行为，本文探讨了充分刻画多方会话类型的通信自动机方面的问题。我们配备了全球和本地会话类型的标记转换系统（LTS），忠实地代表通过无界缓冲通道的异步通信。使用两个LTS之间的等价性，我们确定了一类通信自动机，完全对应于投影的本地类型。我们展示了一个算法来合成一个全局类型的通信自动机的集合。我们的研究结果的关键属性是多方兼容性的概念，非平凡地扩展二元会话类型的对偶条件。
英文摘要：
Multiparty session types are a type system that can ensure the safety and liveness of distributed peers via the global specification of their interactions. To construct a global specification from a set of distributed uncontrolled behaviours, this paper explores the problem of fully characterising multiparty session types in terms of communicating automata. We equip global and local session types with labelled transition systems (LTSs) that faithfully represent asynchronous communications through unbounded buffered channels. Using the equivalence between the two LTSs, we identify a class of communicating automata that exactly correspond to the projected local types. We exhibit an algorithm to synthesise a global type from a collection of communicating automata. The key property of our findings is the notion of multiparty compatibility which non-trivially extends the duality condition for binary session types.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
