论文标题
验证的复杂性和阈值自动机的合成
Complexity of Verification and Synthesis of Threshold Automata
论文作者
论文摘要
阈值自动机是一种形式主义，用于建模和分析耐故障分布式算法，该算法最近由Konnov，Veith和Widder引入，描述了由固定但任意数量的过程执行的协议。我们对阈值自动机的验证和合成问题的复杂性进行了首次系统研究。我们证明，覆盖性，可及性，安全性和livesice问题是NP的完整问题，并且有限的合成问题为$σ_P^2 $完整。我们结果的关键是将阈值自动机的可达性关系作为存在的前爆发公式的新颖表征。该表征还导致了新的验证和合成算法。我们报告实施，并提供实验结果。
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 $Σ_p^2$ 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.
