阈值自动机的系数合成
摘要：阈值自动机是一种用于建模容错分布式算法的形式化方法。阈值自动机的主要特点是阈值守卫的概念，它允许我们比较接收到的消息数量与不同类型的进程的总数。在本文中，我们考虑阈值自动机的系数合成问题。该问题给定了一个阈值自动机的草图（其中阈值守卫中的常数未指定）和一个规范，我们希望合成一组常数，将其插入到草图中，以得到满足规范的阈值自动机。我们的主要结果是，即使规范是可覆盖性规范并且底层草图是非循环的，这个问题也是不可判定的。
作者：A. R. Balasubramanian
论文ID：2304.08917
分类：Distributed, Parallel, and Cluster Computing
分类简称：cs.DC
提交时间：2023-04-19