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

TL;DR

This paper introduces AMP, a comprehensive automata-theoretic framework for specifying, projecting, and type-checking multiparty protocols, enhancing expressivity and robustness over existing session type frameworks.

Contribution

It presents a new formalism for global protocols, a type system for session-typed pi-calculus, and a complete projection method for a broad class of protocols, improving expressivity and robustness.

Findings

PSPACE projection for 'tame' PSMs is sound and complete.

AMP significantly improves expressivity over existing frameworks.

The framework offers a robust, backwards-compatible backend for multiparty session types.

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 $\pi$-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).