skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Characterizing Implementability of Global Protocols with Infinite States and Data
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.  more » « less
Award ID(s):
2304758
PAR ID:
10642067
Author(s) / Creator(s):
; ; ;
Publisher / Repository:
Association for Computing Machinery (ACM)
Date Published:
Journal Name:
Proceedings of the ACM on Programming Languages
Volume:
9
Issue:
OOPSLA1
ISSN:
2475-1421
Format(s):
Medium: X Size: p. 1434-1463
Size(s):
p. 1434-1463
Sponsoring Org:
National Science Foundation
More Like this
  1. ; (, Schloss Dagstuhl – Leibniz-Zentrum für Informatik)
    Forster, Yannick; Keller, Chantal (Ed.)
    Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models. 
    more » « less
  2. (, Information processing letters)
    Using the notion of visibility representations, our paper establishes a new property of instances of the Nondeterministic Constraint Logic (NCL) problem (a PSPACE-complete problem that is very convenient to prove the PSPACE-hardness of reversible games with pushing blocks). Direct use of this property introduces an explosion in the number of gadgets needed to show PSPACE-hardness, but we show how to bring that number from 32 down to only three in the general case, and down to two in our specific case! We propose it as a step towards a broader and more general framework for studying games with irreversible gravity, and use this connection to guide an indirect polynomial-time many-one reduction from the NCL problem to the Hanano Puzzle—which is NP-hard—to prove it is PSPACE-complete. 
    more » « less
  3. (, Proceedings of the 25th International Conference on Descriptional Complexity of Formal Systems)
    Using the notion of visibility representations, our paper establishes a new property of in- stances of the Nondeterministic Constraint Logic (NCL) problem (a PSPACE-complete problem that is very convenient to prove the PSPACE-hardness of reversible games with pushing blocks). Direct use of this property introduces an explosion in the number of gadgets needed to show PSPACE-hardness, but we show how to bring that number from 32 down to only three in general, and down to two in a specific case! We propose it as a step towards a broader and more general framework for studying games with irreversible gravity, and use this connection to guide an indirect polynomial-time many-one reduction from the NCL problem to the Hanano Puzzle—which is NP-hard—to prove it is in fact PSPACE-complete. 
    more » « less
  4. ; (, Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning)
    The problems of verification and realizability are two central themes in the analysis of reactive systems. When multiagent systems are considered, these problems have natural analogues of existence (nonemptiness) of pure-strategy Nash equilibria and verification of pure-strategy Nash equilibria. Recently, this body of work has begun to include finite-horizon temporal goals. With finite-horizon temporal goals, there is a natural hierarchy of goal representation, ranging from deterministic finite automata (DFA), to nondeterministic finite automata (NFA), and to alternating finite automata (AFA), with a worst-case exponential gap between each successive representation. Previous works showed that the realizability problem with DFA goals was PSPACE-complete, while the realizability problem with temporal logic goals is in 2EXPTIME. In this work, we study both the realizability and the verification problems with respect to various goal representations. We first show that the realizability problem with NFA goals is EXPTIME-complete and with AFA goals is 2EXPTIME-complete, thus establishing strict complexity gaps between realizability with respect to DFA, NFA, and AFA goals. We then contrast these complexity gaps with the complexity of the verification problem, where we show that verification with respect to DFAs, NFA, and AFA goals is PSPACE-complete. 
    more » « less
  5. ; ; ; (, Springer Nature Switzerland)
    Abstract We presentSprout, the first sound and complete implementability checker for symbolic multiparty protocols.Sproutsupports protocols with dependent refinements on message values, loop memory, and multiparty communication with generalized, sender-driven choice.Sproutchecks implementability via an optimized, sound and complete reduction to the fixpoint logic$$\mu $$ μ CLP, and usesMuValas a backend solver for$$\mu $$ μ CLP instances. We evaluateSprouton an extended benchmark suite of implementable and non-implementable examples, and show thatSproutoutperforms its competititors in terms of expressivity and precision, and provides competitive runtime performance.Sproutadditionally provides support for verifying custom functional correctness properties beyond implementability. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email