Coefficient Synthesis for Threshold Automata

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.