Asynchronous global protocols, precisely

Book section

Asynchronous multiparty session types are a type-based framework that ensures the compatibility of components in a distributed system by specifying a global protocol. Each component can be independently developed and refined locally, before being integrated into a larger system, leading to higher quality distributed software. This paper studies the interplay between global protocols and an asynchronous refinement relation, precise asynchronous multiparty subtyping. This subtyping relation locally optimises asynchronous messaging, enabling a permutation of two actions in a component while still preserving the safety and liveness of the overall composed system. In this paper, we first define the asynchronous association between a global protocol and a set of local (optimised) specifications. We then prove the soundness and completeness of the operational correspondence of this asynchronous association. We demonstrate that the association acts as an invariant to provide type soundness, deadlock-freedom and liveness of a collection of components optimised from the end-point projections of a given global protocol.

Authors: Pischke, K; Yoshida, N

• Publication status: Published
• Publisher: Springer
• Host title: Components Operationally: Reversibility and System Engineering Essays Dedicated to Jean-Bernard Stefani on the Occasion of His 65th Birthday
• Series: Lecture Notes in Computer Science
• Series number: 16065
• Publication date: 2025-10-19
• Acceptance date: 2025-10-19
• Event title: Components Operationally: Reversibility and System Engineering
• Event website: https://link.springer.com/chapter/10.1007/978-3-031-99717-4_7
• DOI: 10.1007/978-3-031-99717-4_7
• EISSN: 1611-3349
• ISSN: 0302-9743
• EISBN: 9783031997174
• ISBN: 9783031997167
• Language: English
• Keywords: convention theory; modularity; formal languages and automata theory; standardization; control structures and microprogramming; standards