Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Impact of the Communication Model on Realisability

Cinzia Di Giusto, Etienne Lozes, Pascal Urso

TL;DR

This paper develops a parameterised framework for realisability and subtyping of Multiparty Session Types (MPST) across diverse communication models, representing global protocols as MSC-based automata and projecting to CFSMs. A key theoretical insight is that subtyping is model-agnostic, while realisability depends on the communication model; the authors introduce complementability to bridge complexity gaps and enable reductions to synchronous realisability. They prove decidability results, obtaining PSPACE bounds for synchronous realisability and EXPSPACE bounds for causally closed asynchronous models, with subtyping decidable in NLOGSPACE given explicit complements. Complementation by duality and by renunciation for sender-driven choices provide practical methods to obtain complements for several classes of global types. Overall, the work delivers a unified, semantically-grounded treatment of realisability across models and lays foundations for scalable verification tools in MPST-enabled distributed systems.

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.

On the Impact of the Communication Model on Realisability

TL;DR

This paper develops a parameterised framework for realisability and subtyping of Multiparty Session Types (MPST) across diverse communication models, representing global protocols as MSC-based automata and projecting to CFSMs. A key theoretical insight is that subtyping is model-agnostic, while realisability depends on the communication model; the authors introduce complementability to bridge complexity gaps and enable reductions to synchronous realisability. They prove decidability results, obtaining PSPACE bounds for synchronous realisability and EXPSPACE bounds for causally closed asynchronous models, with subtyping decidable in NLOGSPACE given explicit complements. Complementation by duality and by renunciation for sender-driven choices provide practical methods to obtain complements for several classes of global types. Overall, the work delivers a unified, semantically-grounded treatment of realisability across models and lays foundations for scalable verification tools in MPST-enabled distributed systems.

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.

Paper Structure

This paper contains 24 sections, 27 theorems, 26 equations, 12 figures.

Table of Contents

  1. Introduction
  2. Global Types as Automata for Real-World Protocols
  3. Beyond P2P Semantics: the Need for General Communication Models
  4. Subtyping: Protocol Flexibility and Safe Refinement
  5. Contributions
  6. Preliminaries
  7. Automata
  8. Executions
  9. Communication Models
  10. Message Sequence Charts
  11. Happens-before relation and linearisations
  12. Communicating finite state machines
  13. Global Types
  14. Realisability
  15. Subtyping
  16. ...and 9 more sections

Key Result

Lemma 2.15

Let $e$ be an execution and $M=\mathsf{msc}(e)$. Then $e$ is an execution of $\mathsf{p2p}$ if and only if for any two send events $s_1=!m_1^{p\to q}$ and $s_2=!m_2^{p\to q}$ in $\mathsf{events}_S(e)$, with $s_1 \mathrel{\preceq_{M}^{}} s_2$, one of the two holds:

Figures (12)

  • Figure 1: The MQTT global type
  • Figure 2: A subtype of the MQTT global type and its representation as an automaton.
  • Figure 3: The two interactions specified by $\mathsf{G}_2$, and another unspecified interaction that happens in the projected system in the p2p semantics
  • Figure 4: Hierarchy of communication models, both as sets of executions and as sets of MSCs.
  • Figure 5: Examples of MSCs for various communication models. The sender of a message is at the origin of the arrow and the receiver at the destination. Unmatched send events are depicted with dashed arrows.
  • ...and 7 more figures

Theorems & Definitions (105)

  • Definition 2.1: Execution
  • Definition 2.2: Communication model
  • Definition 2.3: $\mathsf{bag}$
  • Definition 2.4: $\mathsf{synch}$
  • Definition 2.5: $\mathsf{p2p}$
  • Definition 2.6: MSC
  • Example 2.7
  • Definition 2.8: Happens-before relation
  • Definition 2.9: Linearisation
  • Example 2.10
  • ...and 95 more