Complete Multiparty Session Type Projection with Automata

TL;DR

This paper introduces a novel automata-based projection operator for multiparty session types that is sound, complete, efficient, and capable of handling more complex protocols than previous methods.

Contribution

It presents the first projection operator that combines automata-theoretic synthesis with succinct implementability checks, improving efficiency and applicability.

Findings

The new projection operator is sound, complete, and efficient.

MST implementability is shown to be in PSPACE, improving over previous EXPSPACE bounds.

A prototype implementation demonstrates practical effectiveness on complex global types.

Abstract

Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine. Existing projection operators are syntactic in nature, and trade efficiency for completeness. We present the first projection operator that is sound, complete, and efficient. Our projection separates synthesis from checking implementability. For synthesis, we use a simple automata-theoretic construction; for checking implementability, we present succinct conditions that summarize insights into the property of implementability. We use these conditions to show that MST implementability is in PSPACE. This improves upon a previous decision procedure that is in EXPSPACE and applies to a smaller class of MSTs. We demonstrate the effectiveness of our approach using a prototype implementation, which handles global types not supported by previous work without sacrificing performance.