Quantitative Language Automata

Abstract

A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA A obtains a mean payoff, and every word w is assigned the maximal mean payoff obtained by nondeterministic runs of A over w. We introduce quantitative language automata (QLAs) that define functions from language generators (i.e., implementations) to values, where a language generator can be nonprobabilistic, defining a set of infinite words, or probabilistic, defining a probability measure over infinite words. A QLA consists of a QWA and a language aggregator. For example, given a QWA A, the infimum aggregator maps each language L to the greatest lower bound assigned by A to any word in L. For boolean value sets, QWAs capture trace properties, and QLAs capture hyperproperties. For more general value sets, QLAs serve as a specification language for a generalization of hyperproperties, called quantitative hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty assigns a value to each set (resp. distribution) G of traces, e.g., the minimal (resp. expected) average response time exhibited by the traces in G (resp. by traces sampled according to G). We give several examples of quantitative hyperproperties and investigate three paradigmatic problems for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem, given a QLA AA and an implementation G, we ask for the value that AA assigns to G. In the nonemptiness (resp. universality) problem, given a QLA AA, a threshold k, and a comparison in {>, >=} we ask whether AA assigns a value meeting the threshold to some (resp. every) language. We provide a comprehensive picture of decidability and complexity for these problems for QLAs with common aggregators as well as their restrictions to omega-regular languages and distributions generated by finite Markov chains.

Figures (2)

• Figure 1: Weighted labeled transition systems $\mathcal{T}\xspace_{\text{up}}$, $\mathcal{T}\xspace_{\text{sim}}$, $\mathcal{T}\xspace_{\text{com}}$, and $\mathcal{T}\xspace_{\text{sta}}$ can be used to specify QWAs and QLAs with various aggregators, as demonstrated in \ref{['sec:applications']}. Transitions are marked with $\sigma : p : x$, where $\sigma$ denotes a letter, $p$ the transition probability (dropped when $p=1$), and $x$ the transition weight. The Markov chain $\mathcal{M}\xspace$ is a language generator with parameters $0 \leq p,q \leq 1$ (its transitions are not weighted, and those with probability 0 are not shown). In $\mathcal{T}\xspace_{\text{sta}}$, the three initial arrows are shorthand for the three admissible initial positions.
• Figure 2: The pattern used in \ref{['characterize:words:fixed']} witnessing word-level infiniteness. From $q_I$, the automaton reaches $q_1$, may iterate the loop labeled $v_1$, then moves to $q_2$ via $u_1u_2$, and may iterate the loop labeled $v_2$ at $q_2$, where $u_0,u_1,u_2,v_1,v_2 \in \Sigma^+$, $|u_1| = |v_1|$, and $u_1 \neq v_1$. Consequently, the words $u_0(v_1)^i u_1u_2(v_2)^\omega$, for $i \in \mathbb{N}\xspace$, are pairwise distinct, and each admits a run that visits $q_2$ infinitely often.

Theorems & Definitions (101)

• Proposition 2.1
• proof
• Proposition 2.2
• proof
• Remark 4.1
• Proposition 4.2
• proof
• Proposition 4.3
• proof
• Proposition 4.4