Realisability and Complementability of Multiparty Session Types

TL;DR

This paper investigates the properties of multiparty session types, focusing on their realisability and complementability, and provides algorithms and constructions to determine and achieve these properties in message-passing systems.

Contribution

It establishes the relationship between realisability and complementability of global types and introduces an algorithm to decide realisability in p2p communication models.

Findings

Realisability with p2p implies realisability with synchronous communication.

Synchronous realisability implies the existence of a complementary global type.

An algorithm is provided to decide realisability of complementable global types.

Abstract

Multiparty session types (MPST) are a type-based approach for specifying message-passing distributed systems. They rely on the notion of global type specifying the global behaviour and local types, which are the projections of the global behaviour onto each local participant. An essential property of global types is realisability, i.e., whether the composition of the local behaviours conforms to those specified by the global type. We explore how realisability of MPST relates to their complementability, i.e., whether there exists a global type that describes the complementary behaviour of the original global type. First, we show that if a global type is realisable with p2p communications, then it is realisable with synchronous communications. Second, we show that if a global type is realisable in the synchronous model, then it is complementable, in the sense that there exists a global type that describes the complementary behaviour of the original global type. Third, we give an algorithm to decide whether a complementable global type, given with an explicit complement, is realisable in p2p. As a side contribution, we propose a complementation construction for global types with sender-driven choice, and more generally commutation-deterministic, with a linear blowup in the size of the global type.