Compositional Interface Refinement Through Subtyping in Probabilistic Session Types

Abstract

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.