阈值自动机的系数合成

阈值自动机是一种用于建模容错分布式算法的形式化方法。阈值自动机的主要特征是阈值守卫的概念，它允许我们将接收到的消息数量与不同类型进程的总数进行比较。在本文中，我们考虑阈值自动机的系数合成问题，其中给定一个阈值自动机的草图（阈值守卫中的某些常数未指定）以及一个描述一组不良行为的违例。然后我们希望合成一组常数，将其代入草图后得到的阈值自动机不具有这些不良行为。我们的主要结果是该问题不可判定，即使违例由可覆盖性性质给出且底层草图是无环的。接着我们考虑有界系数合成问题，其中还提供了待合成常数的上界。尽管已知该问题对于可覆盖性性质处于多项式层级第二层，但该问题的算法涉及将可达关系以指数大小编码到存在 Presburger 算术中。在本文中，我们给出了该关系的多项式大小编码。我们还针对可覆盖性性质给出了该问题的紧复杂度下界。最后，受文献中出现的基准启发，我们还考虑了一类特殊的阈值自动机并证明在此情况下复杂度降低。