On the Impact of the Communication Model on Realisability

TL;DR

This paper investigates how different communication models affect the realisability of global specifications in Multiparty Session Types, providing a unified framework and decision procedures for various models.

Contribution

It introduces a unified framework for analyzing realisability across multiple communication models and develops decision procedures with complexity analyses.

Findings

Communication model does not affect subtyping.

Realisability is impacted by the communication model.

Decision procedures vary in complexity from NLOGSPACE to EXPSPACE.

Abstract

Multiparty Session Types (MPST) provide a type-theoretic foundation for specifying and verifying communication protocols in distributed systems. MPST rely on the notion of global type which specifies the global behaviour and local types, which are the projections of the global behaviour onto each local participant. A central notion in MPST is realisability - whether local implementations derived from a global specification correctly realise the intended protocol under a given communication model. While realisability has been extensively studied under peer-to-peer semantics, it remains poorly understood in alternative communication models such as bag-based, causally ordered, or synchronous communications. In this paper, we develop a unified framework for reasoning about realisability and subtyping across a spectrum of communication models. We show that the communication model does not impact the notion of subtyping, but that it impacts the notion of realisability. We introduce several decision procedures for subtyping checking and realisability checking with complexities ranging from NLOGSPACE to EXPSPACE depending on the assumptions made on the global types, in particular depending on their complementability and the size of a given complement.