2025/09/12 by Paula Blechschmidt, Blechschmidt, Paula
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Natural Language Processing Techniques #Speech Recognition and Synthesis
paper · pdf · doi:10.48550/arxiv.2509.16228
openalex publication_date 2025/09/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Multiparty session types (MPST) are a robust typing framework that ensures safe and deadlock-free communication within distributed protocols. As these protocols grow in complexity, compositional modelling becomes increasingly important to scalably verify their behaviour. Therefore, we propose using a refinement-based subtyping approach to facilitate the modularity needed for compositional verification. Subtyping in classic MPST systems inherently represents a notion of refinement: A larger type may be safely substituted by a smaller, refined type. The aim of this thesis is to significantly extend this concept and discover just how flexible and expressive subtyping relations can be. We present a probabilistic extension for MPST, the probabilistic mixed choice multiparty session pi-calculus, with a novel, flexible subtyping system which allows one channel (the interface) to be substituted by several channels (the refinement). Our subtyping is remarkably expressive; any selection of well-typed channels as the refinement has a corresponding interface in a single channel type. To facilitate this generality, we base our system on a powerful variant of MPST, mixed choice multiparty session types (MCMP), which offers greater flexibility in communication choices. We establish soundness of the probabilistic mixed choice multiparty session system through several key results. In particular, we prove subject reduction, error-freedom and deadlock-freedom, ensuring that well-typed processes are well-behaved. This work demonstrates subtyping to possess great previously untapped potential for stepwise refinement and compositional verification. The presented framework enables highly expressive, compositional, and verifiable modelling of probabilistic distributed communication.