一句话：对带无限状态与数据的符号通信协议，给出可实现性的精确语义刻画、检查算法及复杂度结果。
本文研究涉及多个参与者的符号通信协议的可实现性问题。此类协议用依赖精化谓词描述无限状态和数据值；可实现性要求全局协议规范存在分布、异步的参与者实现，既无死锁又与规范行为一致。作者通过精确的语义刻画统一解释了看似不同的不可实现性来源，将可实现性归约为限制到各参与者上的全局协议(余)可达性，并据此给出首个可靠且相对完备的符号协议可实现性检查算法。对有限协议，显式表示下该问题是 co-NP完全的，符号表示下是 PSPACE 完全的；显式有限片段还涵盖已研究的多方会话类型片段，将其上界从 PSPACE 收紧到 co-NP。
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.
@article{paperbot3156,
title = {Characterizing Implementability of Global Protocols with Infinite States and Data},
author = {Elaine Li and Felix Stutz and Thomas Wies and Damien Zufferey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720493}
}