Characterizing Implementability of Global Protocols with Infinite States and Data
Elaine Li, Felix Stutz, Thomas Wies, Damien Zufferey
TL;DR
The paper addresses the implementability of highly expressive asynchronous global protocols with infinite states and data by introducing Global Communicating Labeled Transition Systems (GCLTS) and a semantic, per-participant reachability framework. It develops a sound and relatively complete symbolic algorithm that reduces implementability to (co)reachability and encodes the problem in the $\mu$CLP$ framework, enabling practical verification across finite and symbolic fragments. It establishes complexity results: implementability is co-NP-complete for explicit finite protocols and PSPACE-complete for symbolic or symbolic-finite fragments, with a corollary tightening the known bound for global types. The approach unifies disparate non-implementability phenomena under a single semantic lens and provides a canonical implementation-based synthesis pathway, with broad implications for MSTs, HMSCs, and choreographic programming in asynchronous settings.
Abstract
We study the implementability problem for an expressive class of symbolic communication protocols involving multiple participants. Our symbolic protocols describe infinite states and data values using dependent refinement predicates. Implementability asks whether a global protocol specification admits a distributed, asynchronous implementation, namely one for each participant, that is deadlock-free and exhibits the same behavior as the specification. We provide a unified explanation of seemingly disparate sources of non-implementability through a precise semantic characterization of implementability for infinite protocols. Our characterization reduces the problem of implementability to (co)reachability in the global protocol restricted to each participant. This compositional reduction yields the first sound and relatively complete algorithm for checking implementability of symbolic protocols. We use our characterization to show that for finite protocols, implementability is co-NP-complete for explicit representations and PSPACE-complete for symbolic representations. The finite, explicit fragment subsumes a previously studied fragment of multiparty session types for which our characterization yields a co-NP decision procedure, tightening a prior PSPACE upper bound.