QuAK：自动化量化自动机分析

量化自动机模型超越布尔值系统的方面：每个执行映射到一个实数，通过引入加权转换和值函数来实现，这些值函数概括了布尔 $\omega$-自动机的接受条件。尽管量化自动机在系统分析方面取得了理论进展，但直到最近，才开发了第一个全面的量化自动机软件工具（量化自动机套件，QuAK）。QuAK实现了解决标准决策问题的算法，如空性和普遍性，以及量化自动机的安全性和活性构造。我们 present了QuAK的架构，这反映了所有这些问题都归约为检查两个量化自动机之间的包含关系或计算自动机可实现的最高值——即其所谓的顶部值。我们通过扩展这两个算法以返回结果的同时返回最终周期词证明算法输出的 witness，以及实现一个可以处理非确定性自动机的新的安全-活性分解算法，使QuAK更加信息丰富且更具能力。