Complete Multiparty Session Type Projection with Automata
summary
Claims a sound, complete, and practical projection operator for asynchronous multiparty session types, implemented by translating global types to automata and projecting to candidate communicating state machines, then checking two succinct annotations (send validity and receive validity). Proves implementability is PSPACE-complete, builds a prototype that verifies global types previous tools could not, and reports similar-order runtimes (about a twofold overhead) while producing deadlock-free implementations when checks pass.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:43Global types and visuals
- 2:08Local specs and state machines
- 3:10Implementability problem
- 5:18Soundness and completeness
- 8:08Sender-driven choice challenges
- 10:56Previous work limitations
- 12:00Two-phase implementability
- 14:07Send validity role
- 15:54Receive validity and messages
- 18:00Two conditions sufficiency
- 19:06Complexity and evaluation
- 19:49Additional properties
- 20:11Covered implementable space
- 20:33Q&A