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 PTIME decision procedure, improving upon a prior PSPACE upper bound.

翻译：本研究探讨一类涉及多参与方的符号通信协议的可实现性问题。该符号协议利用依赖精化谓词描述无限状态与数据值。可实现性询问全局协议规范是否允许分布式异步实现，即为每个参与方提供无死锁且行为与规范一致的实现。通过对无限协议可实现性的精确语义刻画，我们为看似分散的非可实现性来源提供了统一解释。该刻画将可实现性问题简化为全局协议在各参与方受限下的（共）可达性问题。这一组合归约产生了首个用于检验符号协议可实现性的可靠且相对完备的算法。我们运用该特征刻画证明：对于有限协议，显式表示下的可实现性为co-NP完全问题，符号表示下为PSPACE完全问题。有限显式片段包含先前研究的多方会话类型片段，我们的特征刻画为此提供了PTIME判定过程，改进了原有的PSPACE上界。