QuAK：定量自动机工具包
QuAK: Quantitative Automata Kit
AI总结：
本文介绍了首个定量自动机自动化分析工具QuAK，支持多种自动机类型的判定、极值计算、安全-活性分解及行为监控，并通过实验验证了其有效性。
摘要：
系统行为传统上通过正确性的二元分类来评估，这不足以处理涉及系统和执行定量方面的性质。定量自动机提供了一种更细致的方法，通过结合加权转移和推广接受条件的值函数，将每次执行映射到一个实数。在本文中，我们介绍了QuAK，这是首个旨在自动化分析定量自动机的工具。QuAK目前支持多种定量自动机类型，包括Inf、Sup、LimInf、LimSup、LimInfAvg和LimSupAvg自动机，并实现了针对空性、普遍性、包含、等价等问题，以及检查自动机是否安全、活或常数的判定程序。此外，QuAK能够在可能时计算极值，构建安全-活性分解，并监控系统行为。我们通过专注于包含、常数函数检查和监控问题的实验，展示了QuAK的有效性。
英文摘要：
System behaviors are traditionally evaluated through binary classifications of correctness, which do not suffice for properties involving quantitative aspects of systems and executions. Quantitative automata offer a more nuanced approach, mapping each execution to a real number by incorporating weighted transitions and value functions generalizing acceptance conditions. In this paper, we introduce QuAK, the first tool designed to automate the analysis of quantitative automata. QuAK currently supports a variety of quantitative automaton types, including Inf, Sup, LimInf, LimSup, LimInfAvg, and LimSupAvg automata, and implements decision procedures for problems such as emptiness, universality, inclusion, equivalence, as well as for checking whether an automaton is safe, live, or constant. Additionally, QuAK is able to compute extremal values when possible, construct safety-liveness decompositions, and monitor system behaviors. We demonstrate the effectiveness of QuAK through experiments focusing on the inclusion, constant-function check, and monitoring problems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
