Automating the Analysis of Quantitative Automata with QuAK

Traditional system behavior analysis categorizes system behaviors as correct or incorrect. However, modern systems require more nuanced approaches to address performance and robustness criteria. Quantitative automata generalize boolean \(\omega \)-automata by adding rational-valued weights to their transitions and using value functions (instead of acceptance conditions) that accumulate infinite weight sequences into single values. Common value functions include \({\textsf{Inf}}\), \({\textsf{Sup}}\), \({\textsf{LimInf}}\), and \({\textsf{LimSup}}\) (respectively generalizing safety, reachability, co-Büchi and Büchi acceptance conditions), as well as \({\textsf{DSum}}\) (discounted sum), \({\textsf{LimInfAvg}}\), and \({\textsf{LimSupAvg}}\) (limit average a.k.a. mean payoff).

Decision problems for boolean automata extend naturally to quantitative automata. For example, a quantitative automaton \(\mathcal {A}\) is nonempty with respect to a rational number v iff \(\mathcal {A}\) maps some infinite word w to a value at least v [13]. These problems are closely related to game theory [21] and enable reasoning about quantitative system aspects. Although quantitative automata have been extensively studied from a theoretical perspective [4‐6, 8, 16, 24‐26, 34, 35] and these works could significantly impact their practical verification, until recently, there was no general software tool for their analysis.

Quantitative Automata Kit (QuAK) [11] is the first general tool for quantitative automata analysis. It currently supports several automaton types (\({\textsf{Inf}}\), \({\textsf{Sup}}\), \({\textsf{LimInf}}\), \({\textsf{LimSup}}\), \({\textsf{LimInfAvg}}\), \({\textsf{LimSupAvg}}\)) and provides decision procedures for fundamental problems such as emptiness, universality, inclusion, and safety.

We present an improved version of QuAK: (i) the safety-liveness decompositions are extended to handle nondeterministic automata, and (ii) the inclusion and top value algorithms are extended with capabilities to return a witness—an ultimately periodic word explaining the algorithm’s output. For checking inclusion, i.e., whether \(\mathcal {A}(w) \le \mathcal {B}(w)\) for all words w, the witness \(\hat{w}\) is a word such that \(\mathcal {A}(\hat{w}) > \mathcal {B}(\hat{w})\). For computing top value, i.e., \(\top _{\mathcal {A}} = \sup _{w \in \varSigma ^\omega } \mathcal {A}(w)\), the witness \(\widehat{w}\) is a word such that \(\mathcal {A}(\hat{w}) = \top _{\mathcal {A}}\). Since all the other procedures are reduced to either inclusion checking or top value computation, these extensions significantly improve QuAK’s informativeness for analyzing quantitative automata.

Several approaches extend system modeling beyond boolean aspects. One uses multi-valued truth domains [9, 15], while another relies on weighted automata [36], where numerical weights are assigned to transitions and accumulated via semiring operations. Tools such as Vaucanson [32], Vcsn [18], and Awali [31] support weighted automata analysis. Other approaches address digital-analog interactions [1, 2, 22], with tools like UPPAAL [30] and HyTech [23]. Signal temporal logic [33] allows reasoning about specification satisfaction degrees, as implemented in Breach [19], S-TaLiRo [3], and RTAMT [37]. Probabilistic verification handles uncertainties, as implemented in PRISM [29] and STORM [17].

Let \(\varSigma \) be a finite alphabet of letters. We denote by \(\varSigma ^*\) (resp. \(\varSigma ^\omega \)) the set of all finite (resp. infinite) words over \(\varSigma \). For \(w \in \varSigma ^\omega \) and \(u \in \varSigma ^*\), we write \(u \prec w\) when u is a prefix of w. A value domain \(\mathbb {D} \) is a nontrivial complete lattice. A quantitative property is a total function \(\varPhi : \varSigma ^\omega \rightarrow \mathbb {D} \).

We study quantitative automata, which define a subset of quantitative properties on totally-ordered value domains. Formally, a nondeterministic quantitative automaton (or simply an automaton) is a tuple \(\mathcal {A}= (\varSigma ,Q,s,\delta )\) where \(\varSigma \) is a finite alphabet, Q is a finite nonempty set of states, \(s \in Q\) is the initial state, and \(\delta :Q \times \varSigma \rightarrow 2^{\mathbb {Q} \times Q}\) is a finite transition function over weight-state pairs [13]. A transition is a tuple \((q, \sigma , x, q') \in Q \times \varSigma \times \mathbb {Q} \times Q\) such that \((x,q') \in \delta (q,\sigma )\), denoted \(q\xrightarrow []{\sigma :x}q'\). The weight of a transition \(t = (q, \sigma , x, q')\) is denoted by \(\gamma (t) = x\). An automaton \(\mathcal {A}\) is deterministic when \(|\delta (q,a)| = 1\) for every \(q \in Q\) and \(a \in \varSigma \), and it is total (a.k.a. complete) when \(|\delta (q,a)| \ge 1\) for every \(q \in Q\) and \(a \in \varSigma \). We require quantitative automata to be total.

A run of \(\mathcal {A}\) on an infinite word \(w = a_0 a_1 \ldots \) is an infinite sequence \(\rho = q_0\xrightarrow []{a_0:x_0}q_1\xrightarrow []{a_1:x_1}q_2\ldots \) of transitions where \(q_0 = s\) and \((x_i, q_{i+1}) \in \delta (q_i, a_i)\) for each integer \(i \ge 0\). Since each transition has a weight, a run \(\rho = t_0 t_1 \ldots \) produces an infinite sequence \(\gamma (\rho ) = \gamma (t_0) \gamma (t_1) \ldots \) of weights. A value function \({\textsf{Val}}: \mathbb {Q} ^\omega \rightarrow \mathbb {R} \) maps infinite weight sequences to real values. A \({\textsf{Val}}\)-automaton is a quantitative automaton equipped with the value function \({\textsf{Val}}\), i.e., where each run \(\rho \) is mapped to the value obtained by applying \({\textsf{Val}}\) to its weight sequence \(\gamma (\rho )\). Given a \({\textsf{Val}}\)-automaton \(\mathcal {A}\), the value of an infinite word w is \(\mathcal {A}(w) = \sup \{{\textsf{Val}}(\gamma (\rho )) \;|\;\rho \text { is a run of } \mathcal {A}\text { on } w\}\). The top value of an automaton \(\mathcal {A}\) is \(\top _{\mathcal {A}} = \sup _{w \in \varSigma ^\omega } \mathcal {A}(w)\), and its bottom value is \(\bot _{\mathcal {A}} = \inf _{w \in \varSigma ^\omega } \mathcal {A}(w)\). We consider the below value functions over an infinite sequence \(x = x_0 x_1 \ldots \) of rational weights.

The automaton \(\mathcal {A}\) in Figure 1 shows a \({\textsf{LimInfAvg}}\) automaton modeling the long-term average power consumption of a device with two operating modes.

Quantitative Automata Problems We describe the standard decision problems of quantitative automata as well as the problems related to their safety and liveness. The complexity results are summarized in Table 1.

An automaton \(\mathcal {A}\) is nonempty (resp. universal) with respect to a threshold \(v \in \mathbb {Q} \) iff \(\mathcal {A}(w) \ge v\) for some (resp. all) \(w \in \varSigma ^\omega \). Nonemptiness (resp. universality) is closely related to computing an automaton’s top value (resp. bottom value): \(\mathcal {A}\) is nonempty (resp. universal) with respect to \(v \in \mathbb {Q} \) iff \(\top _{\mathcal {A}} \ge v\) (resp. \(\bot _{\mathcal {A}} \ge v\)). An automaton \(\mathcal {A}\) is included in (resp. equivalent to) an automaton \(\mathcal {B}\) iff \(\mathcal {A}(w) \le \mathcal {B}(w)\) (resp. \(\mathcal {A}(w) = \mathcal {B}(w)\)) for all \(w \in \varSigma ^\omega \). An automaton \(\mathcal {A}\) is constant iff there exists \(c \in \mathbb {R} \) such that \(\mathcal {A}(w) = c\) for all \(w \in \varSigma ^\omega \). This problem is closely related to safety and liveness of quantitative automata, as we discuss below.

Quantitative safety generalizes the boolean view by considering membership hypotheses in the form of lower bound queries: a property is safe iff every wrong membership hypothesis has a finite witness for the violation. Formally, a quantitative property \(\varPhi : \varSigma ^\omega \rightarrow \mathbb {D} \) is safe iff for every \(w \in \varSigma ^\omega \) and \(v \in \mathbb {D} \) with \(\varPhi (w) \not \ge v\), there exists a finite prefix \(u \prec w\) such that \(\sup _{w' \in \varSigma ^\omega } \varPhi (u w') \not \ge v\) [25]. Moreover, an automaton \(\mathcal {A}\) is safe iff the quantitative property defined by \(\mathcal {A}\) is safe. Given a quantitative property \(\varPhi : \varSigma ^\omega \rightarrow \mathbb {D} \), its safety closure is defined as \({ SafetyCl}(\varPhi )(w) = \inf _{u \prec w} \sup _{w' \in \varSigma ^\omega } \varPhi (u w')\) and is the least safety property that bounds \(\varPhi \) from above [25]. As expected, a property \(\varPhi \) is safe iff \(\varPhi (w) = { SafetyCl}(\varPhi )(w)\) for all \(w \in \varSigma ^\omega \), and we can compute the safety closure of an automaton \(\mathcal {A}\)—the automaton \({ SafetyCl}(\mathcal {A})\) that expresses the safety closure of the property defined by \(\mathcal {A}\). While this characterization is useful for some classes of quantitative automata, the equivalence problem is undecidable for \({\textsf{LimInfAvg}}\) and \({\textsf{LimSupAvg}}\) automata. For these, the safety problem is still decidable by a reduction to their constant-function problem [6].

Quantitative liveness extends the membership-based view: a quantitative property \(\varPhi : \varSigma ^\omega \rightarrow \mathbb {D} \) is live iff for every word (whose value is less than \(\top = \sup \mathbb {D} \)) there exists a wrong membership hypothesis without a finite witness for the violation. Formally, a quantitative property \(\varPhi : \varSigma ^\omega \rightarrow \mathbb {D} \) is live iff for all \(w \in \varSigma ^\omega \), if \(\varPhi (w) < \top \), then there exists a value \(v \in \mathbb {D} \) such that \(\varPhi (w) \not \ge v\) and for all prefixes \(u \prec w\), we have \(\sup _{w' \in \varSigma ^\omega } \varPhi (uw') \ge v\) [25]. Moreover, an automaton \(\mathcal {A}\) is live iff the quantitative property defined by \(\mathcal {A}\) is live. For the common classes of quantitative automata, deciding liveness reduces to the constant-function problem: an automaton \(\mathcal {A}\) is live iff \({ SafetyCl}(\mathcal {A})\) is constant [6]. Just like every boolean property is the intersection of its safety closure and a liveness property, every quantitative property is the pointwise minimum of its safety closure and a liveness property [25]. Recently, it was proved that all the common classes of automata can be decomposed into its safety closure and a liveness property [7]. Consider the automaton \(\mathcal {A}\), its safety closure \(\mathcal {B}\), and its liveness part \(\mathcal {C}\) as defined in Figure 1. In \(\mathcal {B}\), each strongly connected component (SCC) of \(\mathcal {A}\) is assigned the highest value achievable within the component, representing the greatest among the lower bound hypotheses that cannot be refuted by any finite prefix. The liveness part \(\mathcal {C}\) consists of three components: the upper part is a copy of \(\mathcal {A}\) (ensuring \(\mathcal {C}\) can have runs with the same value as \(\mathcal {A}\)); the middle part contains a \(\top _{\mathcal {A}}\)-weighted copy of the highest-valued cycle in each SCC (enabling \(\mathcal {C}\) to achieve high-valued runs when \(\mathcal {A}\) and \(\mathcal {B}\) agree); and the lower part includes a sink state looping with the lowest weight of \(\mathcal {A}\) (allowing \(\mathcal {C}\) to “escape” the middle part and realize a value using the upper part).

QuAK is written in C++ using the standard library, and the source code is available online [10]. It can be used both as a C++ library and a stand-alone tool through the command-line interface – see our project repository for instructions. For \({\textsf{Inf}}\), \({\textsf{Sup}}\), \({\textsf{LimInf}}\), \({\textsf{LimSup}}\), \({\textsf{LimInfAvg}}\), and \({\textsf{LimSupAvg}}\) automata, QuAK implements the operations listed in Table 1 and a monitoring procedure where the monitor maintains the maximal and minimal possible values or a running average. The problems handled in QuAK reduce to either the inclusion problem or the top value computation, as shown in Figure 2. For the details of these reductions, we refer the reader to [7, 11, 13].

We improve over QuAK’s initial version [11] in two ways. First, a safety-liveness decomposition for nondeterministic automata is implemented, following a new result that provides a decomposition for nondeterministic automata with prefix-independent value functions, namely, \({\textsf{LimInf}}\), \({\textsf{LimSup}}\), \({\textsf{LimInfAvg}}\), and \({\textsf{LimSupAvg}}\) automata [7, Thm. 9.5]. Second, the inclusion-checking and the top-value computation algorithms are extended with an option to return a witness (for negative instance of inclusion and all instances of top value). Since all other problems reduce to these two (see Figure 2), the ability to generate witnesses makes QuAK more informative for analyzing quantitative automata. Inclusion checking, a central component of QuAK, is implemented using an antichain-based algorithm, extending FORKLIFT for Büchi automata [20], with details and performance benefits discussed in [11]. As this algorithm systematically searches for counterexamples, it inherently supports witness construction for negative instances. Top value computation is based on graph-theoretic algorithms [13], with witness generation achieved via backtracking pointers. These improvements, along with other features of QuAK, were validated through unit testing, random testing, and cross-validation with existing implementations.

QuAK reads and constructs automata from text files. Each automaton is represented as a list of transitions of the format a : v, q -> p which encodes a transition from state q to state p with letter a and weight v. The initial state of the input automaton is the source state of the first transition in its text file.

Recall the nondeterministic limit-average automaton \(\mathcal {A}\) and its safety-liveness decomposition from Figure 1. The first three lines of the code snippet in Figure 3 construct the automata \(\mathcal {A}\), \(\mathcal {B}\), and \(\mathcal {C}\) as presented in Figure 1. The nonemptiness check returns false, and witEmpt points to an array storing \(u = \textit{hi}\) and \(v = \textit{hi}\) as \(\top _{\mathcal {A}} = \mathcal {A}(\textit{hi}^\omega ) = 6\). Similarly, the safety check returns false and witSafe points to an array storing \(u = v = \textit{lo}\) as \(\mathcal {B}(\textit{lo}^\omega ) = 4\) and \(\mathcal {A}(\textit{lo}^\omega ) = 2\).

We presented an improved version of QuAK, our software tool for automating quantitative automata analysis, which extends the functionality introduced in [11]. Future work aims to improve the tool’s scalability and applicability while exploring more efficient verification methods. One promising avenue is the development of symbolic approaches to efficiently manage large state spaces. Another key direction involves extending the tool to support additional formalisms, such as various types of discounted-sum automata [4], mean-payoff automaton expressions [12], and nested quantitative automata [14]. In parallel with these efforts, developing novel verification methods specifically tailored to the safety fragments of expressive quantitative formalisms presents an exciting research direction.