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 the constants in the threshold guards left unspecified) and a specification and we want to synthesize a set of constants which when plugged into the sketch, gives a threshold automaton satisfying the specification. Our main result is that this problem is undecidable, even when the specification is a coverability specification and the underlying sketch is acyclic.

翻译：阈值自动机是一种用于对容错分布式算法进行建模的形式化方法。阈值自动机的主要特征是阈值守卫的概念，该机制允许将接收到的消息数量与不同类型进程的总数进行比较。本文研究阈值自动机的系数综合问题，即给定一个阈值自动机草图（其中阈值守卫中的常数未指定）与一个规约，我们需要综合出一组常数，将其代入草图后得到满足该规约的阈值自动机。我们的主要结论是：即便规约为覆盖性规约且底层草图是无环结构，该问题仍不可判定。