TACO：阈值自动机验证工具套件
分布式、并行与集群计算
2026-05-08 v1
摘要
我们提出 TACO，一个用于开发和自动验证面向阈值的容错分布算法的工具套件。该工具套件实现了来自文献中已知不同可判定片段的三种模型检查阈值自动机的方法，以及两套超越这些可判定片段的半判决程序。此外，TACO 是一个模块化、可扩展且文档完善的框架，用于开发阈值自动机的算法和工具。我们介绍了重要功能，概述了所实现算法的概览，并对其性能进行了实验评估。
引用
@article{arxiv.2605.06118,
title = {TACO: A Toolsuite for the Verification of Threshold Automata},
author = {Paul Eichler and Tom Baumeister and Mouhammad Sakr and Mahboubeh Kalateh Dowlati and Marcus Völp and Swen Jacobs},
journal= {arXiv preprint arXiv:2605.06118},
year = {2026}
}
备注
Extended Version of CAV 2026 paper