Deciding Subtyping for Asynchronous Multiparty Sessions
Elaine Li, Felix Stutz, Thomas Wies
TL;DR
This work develops the first precise subtyping framework for asynchronous multiparty session types implemented by unrestricted communicating state machines, tying subtyping to CSM refinement. It introduces a state-decoration based set of conditions $C_1$ and $C_2$ that ensure deadlock freedom and subprotocol fidelity, enabling safe substitution and refinement with respect to a global type $\mathbf{G}$. By relating MST subtyping to CSM refinement and leveraging a subset-construction like approach, the authors establish polynomial-time decidability for Protocol Verification and a tractable restricted form of Protocol Refinement, while showing general refinement is PSPACE-hard. The approach supports sender-driven global types and enables robust verification/refinement beyond prior restricted local-type models, with practical implications for safe protocol optimization and implementation synthesis.
Abstract
Multiparty session types (MSTs) are a type-based approach to verifying communication protocols, represented as global types in the framework. We present a precise subtyping relation for asynchronous MSTs with communicating state machines (CSMs) as implementation model. We address two problems: when can a local implementation safely substitute another, and when does an arbitrary CSM implement a global type? We define safety with respect to a given global type, in terms of subprotocol fidelity and deadlock freedom. Our implementation model subsumes existing work which considers local types with restricted choice. We exploit the connection between MST subtyping and refinement to formulate concise conditions that are directly checkable on the candidate implementations, and use them to show that both problems are decidable in polynomial time.