Complexity of Verification and Synthesis of Threshold Automata

TL;DR

The paper analyzes the complexity of verification and synthesis for threshold automata, a model for parameterized fault-tolerant distributed protocols. It introduces an existential Presburger arithmetic characterization of the reachability relation, enabling NP membership for reachability and parameterized reachability, and provides a model-checking approach for ELTLFT. It establishes NP-completeness for coverability, reachability, safety, and liveness, and proves $\Sigma_p^2$-completeness for the bounded synthesis problem, with further results tying synthesis for sane guards to the same complexity. An implemented tool using Z3 demonstrates favorable performance compared to ByMC on large benchmarks. Overall, the work offers a principled, scalable framework for verifying and synthesizing threshold-based distributed algorithms across varying system sizes.

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 $Σ_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.

Figures (2)

• Figure 1: Pseudocode of a reliable broadcast protocol from ST87:abc for a correct process $i$, where $n$ and $t$ denote the number of processes, and an upper bound on the number of faulty processes. The protocol satisfies its specification (if $\mathit{myval}_i=1$ for every correct process $i$, then eventually $\mathit{accept}_j=\mathit{true}$ for some correct process $j$) if $t < n/3$.
• Figure 2: Threshold automaton modeling the body of the loop in the protocol from Fig. \ref{['fig:st']}. Symbols $\gamma_1, \gamma_2$ stand for the threshold guards $x \ge (t+1) - f$ and $x \ge (n-t) - f$, where $n$ and $t$ are as in Fig. \ref{['fig:st']}, and $f$ is the actual number of faulty processes. The shared variable $x$ models the number of ECHO messages sent by correct processes. Processes with $\mathit{myval}_i=b$ (line 1) start in location $\ell_b$ (in green). Rules $r_1$ and $r_2$ model sending ECHO at lines 7 and 12. The self-loop rules $sl_1,\ldots, sl_3$ are stuttering steps.