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.

翻译：阈值自动机是一种用于建模容错分布式算法的形式化方法。其主要特征在于阈值守卫的概念，该概念允许我们将接收到的消息数量与不同类型进程的总数进行比较。本文研究了阈值自动机的系数综合问题：给定一个阈值自动机草图（其中阈值守卫的某些常数未指定）以及描述一系列不良行为的违规条件，我们的目标是综合出一组常数，当将其代入草图时，所得到的阈值自动机不会表现出这些不良行为。我们的主要结果表明，即使违规条件由覆盖性属性给出且底层草图是无环的，该问题仍然是不可判定的。随后，我们考虑了有界系数综合问题，其中还提供了待综合常数的界限。尽管已知该问题对于覆盖性属性属于多项式层次结构的第二层，但现有算法需要将可达关系以指数规模编码为存在性普雷斯伯格算术。本文中，我们给出了该关系的多项式规模编码。同时，我们针对覆盖性属性为该问题提供了紧致的复杂度下界。最后，受文献中出现的基准测试启发，我们还研究了一类特殊的阈值自动机，并证明了在此情况下问题的复杂度会降低。