Quantitative Language Automata

Our main contribution is the definition and systematic study of QLAs within a three-dimensional framework of aggregator functions (run, word, and language aggregators), which supports the specification and verification of quantitative hyperproperties over nonprobabilistic and probabilistic language generators.

Section 2 presents our definitional framework and Section 3 gives several examples of QLAs for specifying quantitative hyperproperties. Section 4 introduces the QLA evaluation, nonemptiness, and universality problems that we study. Section 5 focuses on the evaluation problem of QLAs with word and language aggregators $\mathrm{𝖨𝗇𝖿}$, $\mathrm{𝖲𝗎𝗉}$, or $𝔼$, and Section 6 on the nonemptiness and universality problems of these. Section 7 switches the focus to QLAs with word and language aggregators $\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿}$ and $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$. Section 8 concludes with potential research directions. We summarize our decidability and complexity results in Table 1. We provide proof sketches in the main text; the details are available in the full version.

To present a comprehensive picture, we overcome several technical challenges: First, for the evaluation problem (Section 5), we demonstrate that the value of an $\omega$-regular language $L$ may not be realized (i) by a lasso word in $L$ for limit-average (a.k.a. mean-payoff) QLAs and (ii) by any word in $L$ for discounted-sum QLAs. Although the evaluation problem for these automata is not always solvable, for its solvable cases we resolve these issues by proving that (i) in the limit-average case, the value of $L$ can still be computed by analyzing strongly connected components even if it is not realized by a lasso word, and (ii) in the discounted-sum case, the value of $L$ matches the value of its safety closure $L^{\prime }$ and is realized by some word in $L^{\prime }$. These results yield PTime algorithms for the evaluation of these QLAs. We complement these results with hardness proofs via reductions from universality problems of the underlying QWAs.

Second, for nonemptiness and universality (Section 6), we examine the behavior of common QWA classes regarding the greatest lower bound of their values – their so-called bottom values [4]. We show (i) discounted-sum QWAs always have a word achieving their bottom value, and (ii) the bottom value of limit-superior-average QWAs can be approximated by lasso words, contrasting sharply with limit-inferior-average QWAs [12]. This enables us to establish the hardness of nonemptiness and universality for certain classes of QLAs. Moreover, we prove that for most classes of QLAs the unrestricted versions of nonemptiness and universality coincide with their finite-state restrictions, indicating a finite-model property.

Third, for QLAs using $\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿}$ and $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$ as word and language aggregators (Section 7), we study values realized by infinitely many runs of a word and infinitely many words of a given language. Using combinatorial arguments, we characterize structural patterns in $\omega$-automata that precisely capture when a value is infinitely realizable with the run aggregators $\mathrm{𝖨𝗇𝖿}$, $\mathrm{𝖲𝗎𝗉}$, $\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿}$, and $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$.

Our work builds on quantitative languages and quantitative word automata [12, 10], as well as on games with quantitative objectives [14]. There have been other definitions of quantitative hyperproperties [16, 28, 31].

While our motivations align, QLAs in their current form and the formalisms of [16, 28] are orthogonal. In [16, 28], a quantitative hyperproperty is based on counting the number of executions that appear in a given relation. Therefore, these formalisms cannot express, e.g., the worst-case server uptime, which QLAs can (see Section 3). Similarly, QLAs with the aggregators we considered cannot express properties that can only be defined using counting or cardinality constraints.

In [31], the authors provide a predicate-transformer theory for reasoning on finite executions of imperative programs. Their formalism can define quantitative hyperproperties that can be expressed as functions from a set or distribution of values at a program’s final state to a single value, which is closer to our view compared to [16, 28]. For example, it can express the maximal value of a variable $x$ given the value of variable $y$ upon termination (akin to QLAs) or the variance of a random variable. However, it cannot express long-run aggregates such as limit superior or limit averages. Conversely, QLAs cannot express variances with the current aggregators, since it requires combining two expectations at the language-aggregator level. To the best of our knowledge, our work is the first to define quantitative hyperproperties as functions from sets or distributions of infinite words to quantitative values, and therefore the first to study the specification and verification of such properties through automata.

A weighted labeled transition system is a tuple $𝒯=(\mathrm{\Sigma },Q,s,\delta ,d)$, where: $\mathrm{\Sigma }$ is a finite alphabet, $Q$ is a finite nonempty set of states, $s\in Q$ is the initial state, $\delta :Q\times \mathrm{\Sigma }\to 2^{\mathbb{Q}\times Q}$ is a finite transition function over weight-state pairs, and $d:Q\times \mathrm{\Sigma }\times \mathbb{Q}\times Q\to [0,1]$ is a probability distribution such that for all $q\in Q$ and $a\in \mathrm{\Sigma }$, (i) $d(q,a,x,q^{\prime })>0$ iff $(x,q^{\prime })\in \delta (q,a)$, and (ii) ${\sum }_{(x,q^{\prime })\in \delta (q,a)}d(q,a,x,q^{\prime })=1$. Given a transition system $𝒯$, the dual of $𝒯$ is a copy of $𝒯$ with the weights multiplied by $-1$.

A transition is a tuple $(q,\sigma ,x,q^{\prime })\in Q\times \mathrm{\Sigma }\times \mathbb{Q}\times Q$ such that $(x,q^{\prime })\in \delta (q,\sigma )$, denoted $q\stackrel{\sigma :x}{\to }{q}^{\prime }$. Given a transition $t=q\stackrel{\sigma :x}{\to }{q}^{\prime }$, we denote its weight by $\gamma (t)=x$. We say that $𝒯$ is complete (a.k.a. total) iff $|\delta (q,a)|\ge 1$ for every $q\in Q$ and $a\in \mathrm{\Sigma }$, and deterministic iff $|\delta (q,a)|=1$ for every $q\in Q$ and $a\in \mathrm{\Sigma }$. Throughout the paper, we assume that weighted labeled transition systems are complete.

Although weighted labeled transition systems are probabilistic by definition, they can be viewed as nondeterministic by considering only the support of $d$, i.e., treating all transitions with positive probability as nondeterministic transitions.

A run of $𝒯$ is an infinite sequence $\rho =q_0\stackrel{{\sigma }_0:x_0}{\to }{q}_1\stackrel{{\sigma }_1:x_1}{\to }\mathrm{\dots }$ of transitions such that $q_0=s$ and $(x_i,q_{i+1})\in \delta (q_i,{\sigma }_i)$ for all $i\ge 0$. We write $\gamma (\rho )$ for the corresponding infinite sequence $x_0{x}_1\mathrm{\dots }$ of rational weights. Given a word $w\in {\mathrm{\Sigma }}^{\omega }$, we denote by $R(𝒯,w)$ the set of runs of $w$ over $𝒯$. Let $\rho =t_0{t}_1\mathrm{\dots }$ be a run and $r=t_0{t}_1\mathrm{\dots }{t}_n$ be a finite prefix of $\rho$. The probability of $r$ is ${\prod }_{i=0}^{n}d(t_i)$. For each infinite word $w$, we define ${\mu }_{𝒯,w}$ as the unique probability measure over Borel sets of infinite runs of $𝒯$ over $w$, induced by the transition probabilities $d$.

A quantitative word automaton (QWA) [12] is a tuple $𝒜=(g,f,𝒯)$ where $𝒯$ is a complete weighted labeled transition system, $f$ is a run aggregator, and $g$ is a word aggregator. Given a word $w$, a transition system $𝒯$, and a run aggregator $f$, we define an $\overline{ℝ}$-multiset $M_{w,𝒯,f}$ such that for every $x\in \overline{ℝ}$ the value $M_{w,𝒯,f}(x)$ equals the number of runs $\rho$ of $𝒯$ over $w$ such that $f(\gamma (\rho ))=x$. For all $x\in \text{supp}(M_{w,𝒯,f})$ we define $\mu (x)={\mu }_{𝒯,w}(\{\rho \in R(𝒯,w)|f(\gamma (\rho ))=x\})$. We let $𝒜(w)=g(M_{w,𝒯,f})$ for all $w\in {\mathrm{\Sigma }}^{\omega }$ and write $𝔼$ for ${𝔼}_{\mu }$ when $\mu$ is clear from the context.

A QWA is nondeterministic when its word aggregator is $\mathrm{𝖲𝗎𝗉}$, and universal when $\mathrm{𝖨𝗇𝖿}$. The top value of a word automaton $𝒜$ is ${\top }_{𝒜}={sup}_{w\in {\mathrm{\Sigma }}^{\omega }}𝒜(w)$, and its bottom value is ${\perp }_{𝒜}={inf}_{w\in {\mathrm{\Sigma }}^{\omega }}𝒜(w)$. We say that ${\top }_{𝒜}$ (resp. ${\perp }_{𝒜}$) is achievable iff there exists a word $w$ with $𝒜(w)={\top }_{𝒜}$ (resp. $𝒜(w)={\perp }_{𝒜}$). Given a word automaton $𝒜=(g,f,𝒯)$ its dual is $\widehat{𝒜}=(\widehat{g},\widehat{f},\widehat{𝒯})$ where $\widehat{g}$, $\widehat{f}$, and $\widehat{𝒯}$ are the duals of $g$, $f$, and $𝒯$, respectively. For a QWA $𝒜=(g,f,𝒯)$ and a word $w$, if $M_{w,𝒯,f}(x)$ is finite for all $x\in \overline{ℝ}$, then we let $𝒜(w)={\top }_{𝒜}$ when $g=\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿}$ and $𝒜(w)={\perp }_{𝒜}$ when $g=\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$.

Boolean word automata are a special case of QWAs with weights in $\{0,1\}$ and $f\in \{\mathrm{𝖨𝗇𝖿},\mathrm{𝖲𝗎𝗉},\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿},\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}\}$. In particular, a nondeterministic Büchi automaton is a boolean word automaton with $g=\mathrm{𝖲𝗎𝗉}$ and $f=\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$. Given a boolean word automaton $ℬ$, we write $L(ℬ)=\{w\in {\mathrm{\Sigma }}^{\omega }|ℬ(w)=1\}$ for its language.

A language generator is a function $G:2^{{\mathrm{\Sigma }}^{\omega }}\to [0,1]$. A language generator $G$ is nonprobabilistic iff there is a language $L_G\subseteq {\mathrm{\Sigma }}^{\omega }$ such that $G(L_G)=1$ and $G(L)=0$ for every other language $L\ne L_G$. A nonprobabilistic language generator $G$ is nonempty iff $L_G\ne \mathrm{\varnothing }$. A language generator $G$ is probabilistic iff it defines a probability measure ${\mu }_G$ over ${\mathrm{\Sigma }}^{\omega }$. A nonprobabilistic quantitative hyperproperty (resp. probabilistic quantitative hyperproperty) is a total function from the set of all nonprobabilistic (resp. probabilistic) language generators to a value domain $𝔻$.

A language aggregator is a function $h:{\overline{\mathbb{N}}}^{\overline{ℝ}}\to \overline{ℝ}$ that accumulates a multiset of values obtained from a set of words into a single value. We consider the language aggregators $\mathrm{𝖨𝗇𝖿}$, $\mathrm{𝖲𝗎𝗉}$, $\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿}$, $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$, and ${𝔼}_{\mu }$, which are defined the same as for the word aggregators above.

A quantitative language automaton (QLA) is a pair $𝔸=(h,𝒜)$ where $𝒜=(g,f,𝒯)$ is a QWA and $h$ is a language aggregator. Consider a language generator $G$ and a QWA $𝒜$. If $G$ is nonprobabilistic (resp. probabilistic), we define $M_{G,𝒜}$ as an $\overline{ℝ}$-multiset such that for every $x\in \overline{ℝ}$ the value $M_{G,𝒜}(x)$ equals the number of words $w$ in $L_G\subseteq {\mathrm{\Sigma }}^{\omega }$ (resp. in ${\mathrm{\Sigma }}^{\omega }$) such that $𝒜(w)=x$. Moreover, if $G$ is probabilistic, we additionally let $\mu (x)={\mu }_G(\{w\in {\mathrm{\Sigma }}^{\omega }|𝒜(w)=x\})$. Then, we let $𝔸(G)=h(M_{G,𝒜})$ for every language generator $G$ where $\mu$ is as above. We write $𝔼$ for ${𝔼}_{\mu }$ when $\mu$ is clear from the context.

Below, we assume the input to a QLA is a nonprobabilistic (resp. probabilistic) language generator when $h\ne 𝔼$ (resp. $h=𝔼$). We write $L$ to denote a nonprobabilistic language generator, and $\mu$ to denote a probabilistic one.

The top value of a QLA $𝔸$, denoted ${\top }_{𝔸}$, is the supremum of the values $𝔸(G)$ over all inputs $G$, and its bottom value, denoted ${\perp }_{𝔸}$, is the infimum. For a QLA $𝔸=(h,𝒜)$ and a nonprobabilistic language generator $L$, if $M_{L,𝒜}(x)=0$ for all $x\in \overline{ℝ}$ (i.e., when $L=\mathrm{\varnothing }$), then we let $𝔸(L)={\top }_{𝔸}$ when $h=\mathrm{𝖨𝗇𝖿}$ and $𝔸(L)={\perp }_{𝔸}$ when $h=\mathrm{𝖲𝗎𝗉}$. Similarly, if $M_{L,𝒜}(x)$ is finite for all $x\in \overline{ℝ}$, then we let $𝔸(L)={\top }_{𝔸}$ when $h=\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿}$ and $𝔸(L)={\perp }_{𝔸}$ when $h=\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$.

Given a QLA $𝔸=(h,𝒜)$ its dual is $\widehat{𝔸}=(\widehat{h},\widehat{𝒜})$ where $\widehat{h}$ and $\widehat{𝒜}$ are the duals of $h$ and $𝒜$.

QWAs can model performance metrics for individual executions. Let $\mathrm{\Sigma }=\{\text{on},\text{off}\}$ be a finite alphabet of observations modeling a server’s activity. Consider the weighted labeled transition system ${𝒯}_{\text{up}}$ given in Figure 1, and let ${𝒜}_{\text{up}}=(g,f,{𝒯}_{\text{up}})$ be a QWA where $g=\mathrm{𝖲𝗎𝗉}$ and $f=\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿𝖠𝗏𝗀}$. The automaton ${𝒜}_{\text{up}}$ maps each infinite word $w$ to the long-run ratio of on, i.e., the average uptime of the execution modeled by $w$. For example, if $w=\text{on}\cdot {(\text{on}\cdot \text{off})}^{\omega }$, we have $𝒜(w)=0.5$.

QLAs can model system-wide performance metrics. Let ${𝔸}_{\text{up}}=(h,{𝒜}_{\text{up}})$. Setting $h=\mathrm{𝖨𝗇𝖿}$ tunes ${𝔸}_{\text{up}}$ to map any given language $L$, capturing the implementation of a server, to the worst-case uptime over all the executions allowed by the implementation, i.e., ${𝔸}_{\text{up}}(L)={inf}_{w\in L}{𝒜}_{\text{up}}(w)$. For example, let $U=\{{\text{on}}^n{\text{off}}^k|n>k\ge 0\}$ and consider the language $L=\{u_1{u}_2\mathrm{\dots }|\forall i:u_i\in U\}$ of server executions where each block of on’s is followed by a strictly shorter block of off’s. Although for every $u\in U$ there are strictly more on’s than off’s, we have $w=s_1{s}_2\mathrm{\dots }\in L$ where $s_i={\text{on}}^i{\text{off}}^{i-1}\in U$ for each $i\ge 1$, thus ${𝔸}_{\text{up}}(L)=0.5$. In particular, notice that the value of ${𝔸}_{\text{up}}(L)$ cannot be achieved by any ultimately periodic word in $L$; we will later show that this may happen even for $\omega$-regular languages (Proposition 5.2). As another example of using QLAs to specify quantitative hyperproperties, setting $h=\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿}$ tunes ${𝔸}_{\text{up}}$ to express the “almost” worst-case uptime by considering only the uptime values realized by infinitely many executions. For example, let $L={\mathrm{\Sigma }}^{\ast }{\text{on}}^{\omega }\cup \{{({\text{on}}^n\text{off})}^{\omega }|n\ge 0\}$. The part ${\mathrm{\Sigma }}^{\ast }{\text{on}}^{\omega }$ yields infinitely many executions with uptime 1, while each ${({\text{on}}^n\text{off})}^{\omega }$ with uptime $\frac{n}{n+1}$ appears only once. Thus, even though the infimum over $L$ is 0, only uptime 1 occurs infinitely often, so $𝔸(L)=1$.

QWAs can specify the distance of individual executions to a desired boolean trace property. Let $\mathrm{\Sigma }=\{\text{req},\text{gra},\text{idle}\}$ be a finite alphabet of observations modeling a server receiving requests and issuing grants, and consider the boolean safety property $P$ requiring that no two requests are simultaneously open (i.e., there is a gra between every two req’s). Consider the transition system ${𝒯}_{\text{sim}}$ given in Figure 1, and let ${𝒜}_{\text{sim}}=(g,f,{𝒯}_{\text{sim}})$ be a QWA where $f={\mathrm{𝖣𝖲𝗎𝗆}}_{0.5}$ and $g\in \{\mathrm{𝖨𝗇𝖿},\mathrm{𝖲𝗎𝗉}\}$ (the choice of $g$ does not matter since ${𝒯}_{\text{sim}}$ is deterministic). The automaton ${𝒜}_{\text{sim}}$ maps each infinite word $w$ to the smallest Cantor distance between $w$ and some word $w^{\prime }\in P$, i.e., ${𝒜}_{\text{sim}}(w)={inf}_{w^{\prime }\in P}d(w,w^{\prime })$. For example, if $w=\text{req}\cdot \text{idle}\cdot {\text{req}}^{\omega }$, we have $𝒜(w)=0.25$.

QLAs can specify the distance of systems to a desired boolean trace property. Let ${𝔸}_{\text{sim}}=(h,{𝒜}_{\text{sim}})$. Setting $h=\mathrm{𝖲𝗎𝗉}$ tunes ${𝔸}_{\text{sim}}$ to map any given language $L$, representing a server implementation, to the worst-case distance from $L$ to $P$. In other words, ${𝔸}_{\text{sim}}(L)={sup}_{w\in L}{inf}_{w^{\prime }\in P}d(w,w^{\prime })$ where $d$ denotes the Cantor distance. For example, if $L={\mathrm{\Sigma }}^{\ast }{\text{req}}^2{\mathrm{\Sigma }}^{\omega }$, then ${𝔸}_{\text{sim}}(L)=0.5$. Setting $h=\mathrm{𝖨𝗇𝖿}$ tunes ${𝔸}_{\text{sim}}$ to map each language to the best-case distance from $L$ to $P$. For example, if $L$ is as above, the value of $L$ would be 0 although all the words in $L$ violate $P$. This is because for every $i\ge 0$ the word $w_i={\text{idle}}^i{\text{req}}^2{\text{idle}}^{\omega }$ belongs to $L$ and $\underset{i\to \mathrm{\infty }}{lim}{𝔸}_{\text{sim}}(w_i)=0$, highlight a challenge for the evaluation of discounted-sum QLAs: the value of $L$ may not be realized by any word in $L$, even if $L$ is omega-regular. Setting $h=𝔼$ tunes ${𝔸}_{\text{sim}}$ to map each language to the average-case distance to $P$. For example, consider the Markov chain $ℳ$ from Figure 1. The expected value can be computed by solving the corresponding system of linear equations, resulting in ${𝔸}_{\text{sim}}({\mu }_{ℳ})=\frac{2pq}{2+p(1+q)}$.

QWAs can express stability constraints of individual executions. Let $\mathrm{\Sigma }=\{\text{l},\text{r},\text{i}\}$ be a finite alphabet representing robot movements – left, right, and idle – on a one-dimensional finite grid. An execution is $\epsilon$-stable, for some $\epsilon \ge 0$, if there exists $0\le \delta \le \epsilon$ such that whenever the system starts within a $\delta$-ball around the origin, it remains indefinitely within an $\epsilon$-ball around the origin. For a fixed $\delta \ge 0$, QWAs can express the most permissive $\epsilon$ associated with each execution. Consider the weighted labeled transition system ${𝒯}_{\text{sta}}$ given in Figure 1, and let ${𝒜}_{\text{sta}}=(\mathrm{𝖲𝗎𝗉},\mathrm{𝖲𝗎𝗉},{𝒯}_{\text{sta}})$. The automaton captures the scenario where $\delta =1$, meaning the robot starts at most one step away from the origin. Transition weights indicate distances from the origin, and a run’s value is the maximal distance reached. Thus, the automaton’s value on a word is the worst-case distance (or most permissive $\epsilon$) over all initial positions. For instance, the word $w={(\text{l}\cdot \text{r})}^{\omega }$ has three runs with values 1, 1, and 2, so ${𝒜}_{\text{sta}}(w)=2$.

QLAs can express stability constraints of systems. Let ${𝔸}_{\text{sta}}=(h,{𝒜}_{\text{sta}})$. If $h=\mathrm{𝖲𝗎𝗉}$, then given a language $L$ modeling the robot’s behavior, the automaton ${𝔸}_{\text{sta}}$ maps $L$ to least upper bound of the set of per-execution $\epsilon$ values obtained from $L$ and ${𝒜}_{\text{sta}}$. In other words, ${𝔸}_{\text{sta}}(L)={\mathrm{𝖲𝗎𝗉}}_{w\in L}{𝔸}_{\text{sta}}(w)$ is the smallest $\epsilon$ ensuring all executions in $L$ are $\epsilon$-stable with $\delta =1$. Alternatively, if $h=\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$, then ${𝔸}_{\text{sta}}(L)$ captures the smallest $\epsilon$ such that infinitely many executions are $\epsilon$-stable for $\delta =1$, allowing to discard “outlier” values achieved only by finitely many executions.

Probabilistic QWAs can specify the expected cost of individual executions. Let $\mathrm{\Sigma }=\{\text{send},\text{ack}\}$ be an alphabet modeling a communication channel. Consider the transition system ${𝒯}_{\text{com}}$ given in Figure 1, and let ${𝒜}_{\text{com}}=(𝔼,\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉},{𝒯}_{\text{com}})$ be a probabilistic QWA. Each run of the automaton is mapped to a long-term maximal cost, i.e., $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$ of the corresponding weight sequence. Then, each infinite word is mapped to the expected value over the distribution of its runs. For example, considering $w={(\text{send}\cdot \text{ack})}^{\omega }$ gives us ${𝒜}_{\text{com}}(w)=5$ because the set of runs with a $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}$ value 5 (i.e., those in which the high-cost cycle occurs infinitely often) has probability 1.

QLAs can specify the aggregate cost of a communication channel. Let ${𝔸}_{\text{com}}=(h,{𝒜}_{\text{com}})$. If $h=𝔼$, the QLA ${𝔸}_{\text{com}}$ specifies the expected cost of the underlying probabilistic model of a communication channel. Consider a Markov chain defining a uniform probability measure $\mu$ over the alphabet $\mathrm{\Sigma }=\{\text{send},\text{ack}\}$. Then, $𝔸(\mu )=1.05$ which can be computed by analyzing the product of the Markov chain defining $\mu$ and the underlying word automaton ${𝒜}_{\text{com}}$.

Let us first consider QLAs whose underlying word automata are nondeterministic, i.e., those where the word aggregator is $g=\mathrm{𝖲𝗎𝗉}$. We show that the nonemptiness problems for such QLAs can be solved efficiently, independently of the choice of the remaining aggregators or additional restrictions on the problem. Intuitively, this is because their top values coincide with those of the underlying QWAs (Proposition 2.1), which are achievable by lasso words and can be computed efficiently.

We turn our attention to QLAs whose underlying word automata are universal, i.e., those where the word aggregator is $g=\mathrm{𝖨𝗇𝖿}$. For run aggregators $f\in \{\mathrm{𝖨𝗇𝖿}$, $\mathrm{𝖲𝗎𝗉}$, $\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿}$, $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉}\}$, we show that computing the automaton’s top value suffices, which can be done in PSpace when $g=\mathrm{𝖨𝗇𝖿}$.

Next, we focus on QLAs with the limit-average run aggregators. We first show that the bottom value of nondeterministic $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉𝖠𝗏𝗀}$ QWAs (dually, top value of universal $\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿𝖠𝗏𝗀}$ QWAs) can be approximated arbitrarily closely by lasso words. This is in stark contrast with nondeterministic $\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿𝖠𝗏𝗀}$ QWAs, where an automaton may be lasso-word universal for some threshold $k$ while there exist non-lasso words with values below $k$ [12, Lem. 4]. The intuition behind this is that for $\mathrm{𝖫𝗂𝗆𝖲𝗎𝗉𝖠𝗏𝗀}$, if $𝒜(w)=k$ for some word $w$ and value $k$, then for any $\epsilon >0$, there exists a length $\mathrm{\ell }$ such that the average value of any run prefix on $w$ of length at least $\mathrm{\ell }$ is below $k+\epsilon$, which does not hold in general for $\mathrm{𝖫𝗂𝗆𝖨𝗇𝖿𝖠𝗏𝗀}$. Consequently, we can find two distant-enough occurrences of the same state and pump the low-average segment between them to obtain a lasso whose overall value stays under the threshold.

In general, all variants of the nonemptiness problem for universal limit-average QWAs (dually, universality for the nondeterministic ones) are undecidable [14, 9, 20]. Combining these with our approximability result above, we obtain the following.

Now, we consider QLAs with the discounted-sum run aggregators. We show that the bottom value of nondeterministic $\mathrm{𝖣𝖲𝗎𝗆}$ QWAs (dually, top value of universal $\mathrm{𝖣𝖲𝗎𝗆}$ QWAs) is achievable. At a high level, we repeatedly extend a finite prefix with a letter that does not increase the current infimum over continuation values. In the limit, this process results in an infinite word whose sequence of prefix infima converges to the automaton’s bottom value. Since discounted-sum automata are co-safe in the quantitative sense [18, 4, 5], i.e., the value of every infinite word equals the limit of its prefix infima, this constructed word attains exactly the bottom value.

By combining the achievability result above with Proposition 4.2, we obtain a concise proof to establish that the nonemptiness problem for QLAs whose underlying QWAs are universal $\mathrm{𝖣𝖲𝗎𝗆}$ QWAs is at least as hard as the universality problem for nondeterministic $\mathrm{𝖣𝖲𝗎𝗆}$ QWAs, which is a long-standing open problem [12, 6].

Let us now focus on QLAs whose underlying QWA is probabilistic, i.e., where $g=𝔼$. We show that several variants of the nonemptiness problem for probabilistic QWAs are undecidable by building on the undecidability results of probabilistic word automata [26].

Finally, putting together the above undecidability result with Propositions 4.2 and 4.3, we show the undecidability of the nonemptiness problem for QLAs whose underlying QWA is probabilistic.