TY - GEN
T1 - Complete Multiparty Session Type Projection with Automata
AU - Li, Elaine
AU - Stutz, Felix
AU - Wies, Thomas
AU - Zufferey, Damien
N1 - Publisher Copyright:
© 2023, The Author(s).
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - Communicating state machines
KW - Deadlock freedom
KW - Multiparty session types
KW - Protocol fidelity
KW - Protocol verification
UR - http://www.scopus.com/inward/record.url?scp=85169430094&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85169430094&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-37709-9_17
DO - 10.1007/978-3-031-37709-9_17
M3 - Conference contribution
AN - SCOPUS:85169430094
SN - 9783031377082
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 350
EP - 373
BT - Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings
A2 - Enea, Constantin
A2 - Lal, Akash
PB - Springer Science and Business Media Deutschland GmbH
T2 - 35th International Conference on Computer Aided Verification, CAV 2023
Y2 - 17 July 2023 through 22 July 2023
ER -