Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is Σ^2_p complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results.
%0 Journal Article
%1 journals/corr/abs-2007-06248
%A Balasubramanian, A. R.
%A Esparza, Javier
%A Lazic, Marijana
%D 2020
%J CoRR
%K informal
%T Complexity of Verification and Synthesis of Threshold Automata.
%V abs/2007.06248
%X Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is Σ^2_p complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results.
@article{journals/corr/abs-2007-06248,
abstract = {Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is Σ^2_p complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results. },
added-at = {2020-10-01T16:13:26.000+0200},
author = {Balasubramanian, A. R. and Esparza, Javier and Lazic, Marijana},
biburl = {https://www.bibsonomy.org/bibtex/26df6582bf1a4a2052b9cd262c1ee0ef5/paves},
ee = {https://arxiv.org/abs/2007.06248},
interhash = {eef129d507b67284d7adf165ed39aa6e},
intrahash = {6df6582bf1a4a2052b9cd262c1ee0ef5},
journal = {CoRR},
keywords = {informal},
note = {https://arxiv.org/abs/2007.06248},
timestamp = {2023-09-24T19:43:27.000+0200},
title = {Complexity of Verification and Synthesis of Threshold Automata.},
volume = {abs/2007.06248},
year = 2020
}