Compositional Interface Refinement Through Subtyping in Probabilistic Session Types

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 modeling becomes increasingly important for scalable verification. Therefore, we propose using refinement through subtyping to facilitate the modularity needed for compositional verification. We present a probabilistic extension for MPST with a novel, flexible subtyping system which allows one channel (the interface) to be substituted by several channels (the refinement). Our subtyping is very 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, which offers greater flexibility in communication choices.