Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols

Felix Stutz, Emanuele D'Osualdo

TL;DR

AMP advances top-down protocol design by coupling expressive global specifications (PSMs) with local realizations (CSMs) in a decoupled framework that preserves modular verification. It shows that PSMs can encode all global types and HMSCs, while enabling richer global patterns through bounded cores and a closure under asynchronous reordering. The authors establish a complete, PSPACE projection for a broad class of PSMs (Tame PSMs) and prove that removing the sender-driven constraint yields undecidability, thereby balancing expressivity with decidability. A CSM-based session-type system provides soundness (subject reduction, safety, and progress under practical restrictions) and supports backward compatibility with MSTs, enabling existing MST tools to flow into the AMP backend. The work also introduces channel-participant encodings and a formal workflow for leveraging this framework in tooling, aiming to unify global and local protocol theories under a practical, robust automata-theoretic foundation.

Abstract

We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a $π$-calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, called "tame", for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection).

An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols

TL;DR

AMP advances top-down protocol design by coupling expressive global specifications (PSMs) with local realizations (CSMs) in a decoupled framework that preserves modular verification. It shows that PSMs can encode all global types and HMSCs, while enabling richer global patterns through bounded cores and a closure under asynchronous reordering. The authors establish a complete, PSPACE projection for a broad class of PSMs (Tame PSMs) and prove that removing the sender-driven constraint yields undecidability, thereby balancing expressivity with decidability. A CSM-based session-type system provides soundness (subject reduction, safety, and progress under practical restrictions) and supports backward compatibility with MSTs, enabling existing MST tools to flow into the AMP backend. The work also introduces channel-participant encodings and a formal workflow for leveraging this framework in tooling, aiming to unify global and local protocol theories under a practical, robust automata-theoretic foundation.

Abstract

We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a -calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, called "tame", for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection).

Paper Structure

This paper contains 12 sections, 1 theorem, 2 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Expressivity of AMP.
  3. Decoupling of AMP.
  4. Robustness of AMP.
  5. Contributions.
  6. Motivation and Key Ideas
  7. Global Specifications via Protocol State Machines
  8. From Global to Local Specifications: Projection
  9. Processes and Typing
  10. Automata-based Protocol Specifications
  11. State Machines and Protocol Languages
  12. A language-theoretic view of protocols.

Key Result

lemma thmcounterlemma

For any CSM $\{\!\!\{A_{\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{p}}}}\}\!\!\}_{{\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{p}}}} \in \mathcal{P}}$, $\mathcal{L}(\{\!\!\{A_{\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{p}}}}\}\!\!\}_{{\color{roleColor}\boldsymbol{{

Figures (6)

  • Figure 1: The components of top-down frameworks.
  • Figure 2: Example global type.
  • Figure 3: A protocol as an HMSC.
  • Figure 4: A PSM encoding for the protocol of \ref{['fig:example1-mst']}.
  • Figure 5: A protocol not expressible as an HMSC. Transitions labelled with ${\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{p}}}}{\to}{\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{q}}}} {:} m$ should be interpreted as emitting the sequence ${\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{p}}}}\mathbin{\color{send}\triangleright}{\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{q}}}}!m \cdot {\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{q}}}}\mathbin{\color{recv}\triangleleft}{\color{roleColor}\boldsymbol{{\color{roleColor}\mathtt{p}}}}?m$.
  • ...and 1 more figures

Theorems & Definitions (6)

  • definition thmcounterdefinition: State machines
  • definition thmcounterdefinition: FIFO Language
  • definition thmcounterdefinition: Communicating state machines
  • definition thmcounterdefinition: Projections and Projectability
  • definition thmcounterdefinition
  • lemma thmcounterlemma: DBLP:conf/concur/MajumdarMSZ21