Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore the implementability problem for symbolic communication protocols involving multiple participants in this 13-minute conference presentation from OOPSLA 2025. Delve into an expressive class of symbolic protocols that describe infinite states and data values using dependent refinement predicates, where implementability determines whether a global protocol specification can admit a distributed, asynchronous implementation that remains deadlock-free while exhibiting the same behavior as the specification. Learn about a unified semantic characterization that explains various sources of non-implementability through a compositional reduction approach, transforming the implementability problem into (co)reachability analysis within the global protocol restricted to each participant. Discover the first sound and relatively complete algorithm for checking implementability of symbolic protocols, along with complexity results showing that implementability is co-NP-complete for explicit representations and PSPACE-complete for symbolic representations in finite protocols. Understand how this characterization applies to multiparty session types, providing a co-NP decision procedure that tightens previous PSPACE upper bounds for finite, explicit protocol fragments.
