阈值自动机验证与综合的复杂性
计算机科学中的逻辑
2025-12-02 v2 分布式、并行与集群计算
摘要
阈值自动机是 Konnov、Veith 和 Widder 近期提出的用于建模和分析容错分布式算法的形式化方法，描述由固定但任意数量进程执行的协议。我们首次对阈值自动机的验证与综合问题的复杂性进行系统研究。我们证明覆盖性、可达性、安全性与活性问题均为 NP 完全，而有界综合问题为 完全。我们结果的关键在于将阈值自动机的可达关系刻画为存在 Presburger 公式的新表征。该表征也导出了新的验证与综合算法。我们报告了实现，并提供了实验结果。
引用
@article{arxiv.2007.06248,
title = {Complexity of Verification and Synthesis of Threshold Automata},
author = {A. R. Balasubramanian and Javier Esparza and Marijana Lazic},
journal= {arXiv preprint arXiv:2007.06248},
year = {2025}
}
备注
Accepted at ATVA20; Code available at https://github.com/arbalan96/thr_aut_SMT