Multiparty session types (MSTs) are an efficient approach to verifying (asynchronous) communication protocols. In this work, we consider MST frameworks with a projection operator, i.e. a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant. Existing projection operators trade efficiency for completeness. Our work provides the first projection operator that is sound, complete, and efficient. Our approach to 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 asynchronous MST implementability is PSPACE-complete. Our prototype implementation demonstrates the effectiveness of our approach and handles global types not supported by previous work without sacrificing performance.

This is joint work with Elaine Li (New York University), Thomas Wies (New York University), and Damien Zufferey (Sonar Source) and appeared in the proceedings of the 35th International Conference on Computer Aided Verification (CAV 2023).