Coefficient Synthesis for Threshold Automata

TL;DR

This paper considers the coefficient synthesis problem for threshold automata, and provides a tight complexity lower bound for this problem against coverability properties, and considers a special class of threshold automata and proves that the complexity decreases in this case.

Abstract

Threshold automata are a formalism for modeling fault-tolerant distributed algorithms. The main feature of threshold automata is the notion of a threshold guard, which allows us to compare the number of received messages with the total number of different types of processes. In this paper, we consider the coefficient synthesis problem for threshold automata, in which we are given a sketch of a threshold automaton (with some of the constants in the threshold guards left unspecified) and a violation describing a collection of undesirable behaviors. We then want to synthesize a set of constants which when plugged into the sketch, gives a threshold automaton that does not have the undesirable behaviors. Our main result is that this problem is undecidable, even when the violation is given by a coverability property and the underlying sketch is acyclic. We then consider the bounded coefficient synthesis problem, in which a bound on the constants to be synthesized is also provided. Though this problem is known to be in the second level of the polynomial hierarchy for coverability properties, the algorithm for this problem involves an exponential-sized encoding of the reachability relation into existential Presburger arithmetic. In this paper, we give a polynomial-sized encoding for this relation. We also provide a tight complexity lower bound for this problem against coverability properties. Finally, motivated by benchmarks appearing from the literature, we also consider a special class of threshold automata and prove that the complexity decreases in this case.

Figures (6)

• 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=0$ for every correct process $i$, then no correct process sets its $\mathit{accept}$ variable to $\mathit{true}$) if $t < n/3$.
• Figure 2: Threshold automaton from ELTLFT 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.
• Figure 5: Example sketch for the second phase
• Figure 6: Example sketch for the third phase
• Figure 7: Sketch for formula \ref{['eq:example']}

Theorems & Definitions (28)

• Example 2.1
• Example 2.2
• Remark 2.3
• Example 2.4
• Theorem 3.1
• Remark 3.2
• Remark 3.3
• Remark 3.4
• Remark 3.5
• Remark 3.6