Automating the Analysis of Quantitative Automata with QuAK

TL;DR

The paper addresses the need for practical tooling for quantitative automata, extending beyond boolean semantics by using real-valued weights and diverse value functions. It presents QuAK, the first general-purpose tool for quantitative automata, with reductions that express core problems as inclusion checks or top-value computations, and it introduces a safety-liveness decomposition for nondeterministic automata along with witness-enabled solutions. The authors implement antichain-based inclusion and graph-based top-value algorithms, enable witness generation for negative inclusions and top-value outputs, and provide a usable C++ library and CLI that reads automata from text. This work enhances the practical verification of quantitative properties and points to scalable, symbolic, and multi-formalism extensions for future research and tooling improvements.

Abstract

Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize acceptance conditions of boolean $ω$-automata. Despite the theoretical advances in systems analysis through quantitative automata, the first comprehensive software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was developed only recently. QuAK implements algorithms for solving standard decision problems, e.g., emptiness and universality, as well as constructions for safety and liveness of quantitative automata. We present the architecture of QuAK, which reflects that all of these problems reduce to either checking inclusion between two quantitative automata or computing the highest value achievable by an automaton -- its so-called top value. We improve QuAK by extending these two algorithms with an option to return, alongside their results, an ultimately periodic word witnessing the algorithm's output, as well as implementing a new safety-liveness decomposition algorithm that can handle nondeterministic automata, making QuAK more informative and capable.

Figures (3)

• Figure 1: A nondeterministic ${\mathsf{LimInfAvg}}$-automaton $\mathcal{A}$ over the alphabet $\Sigma = \{\textit{hi}, \textit{lo}\}$, modeling the power consumption of a device where starting with high-power mode is not reversible, its safety closure $\mathcal{B}$, and its liveness component $\mathcal{C}$ in a corresponding decomposition boker2024safetylivenessquantitativeproperties.
• Figure 2: Reductions of quantitative automata problems in QuAK. The subscript b stands for basic (i.e., ${\mathsf{Val}} \in \{{\mathsf{Inf}}, {\mathsf{Sup}}, {\mathsf{LimInf}}, {\mathsf{LimSup}}\}$), la for limit-average (i.e., ${\mathsf{Val}} \in \{{\mathsf{LimInfAvg}}, {\mathsf{LimSupAvg}}\}$), d for deterministic, and nd for nondeterministic. For example, checking safety of limit-average automata (safety$_\textit{la}$) reduces to their constant-function problem, which reduces to universality of ${\mathsf{LimInf}}$ automata.
• Figure 3: An example usage of QuAK as a C++ library. The functions isNonEmpty and isSafe now take an additional (optional) parameter for storing the stem and the period of the ultimately periodic word witnessing the algorithms' outputs.