Complete Multiparty Session Type Projection with Automata

Elaine Li, Felix Stutz, Thomas Wies, Damien Zufferey

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 PSPACE-complete. 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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 35th International Conference, CAV 2023, Proceedings
EditorsConstantin Enea, Akash Lal
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages24
ISBN (Print)9783031377082
StatePublished - 2023
Event35th International Conference on Computer Aided Verification, CAV 2023 - Paris, France
Duration: Jul 17 2023Jul 22 2023

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13966 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference35th International Conference on Computer Aided Verification, CAV 2023


  • Communicating state machines
  • Deadlock freedom
  • Multiparty session types
  • Protocol fidelity
  • Protocol verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Complete Multiparty Session Type Projection with Automata'. Together they form a unique fingerprint.

Cite this