An earlier version of this paper has appeared at FoSSaCS 2018 [6]

# Comparator automata in quantitative verification

Suguman Bansal  Rice University, Houston, TX-77005, USA<EMAIL_ADDRESS>,
Swarat Chaudhuri  Rice University, Houston, TX-77005, USA<EMAIL_ADDRESS>and
Moshe Y. Vardi  Rice University, Houston, TX-77005, USA<EMAIL_ADDRESS>
###### Abstract.

The notion of comparison between system runs is fundamental in formal
verification. This concept is implicitly present in the verification of
qualitative systems, and is more pronounced in the verification of
quantitative systems. In this work, we identify a novel mode of comparison in
quantitative systems: the online comparison of the aggregate values of two
sequences of quantitative weights. This notion is embodied by comparator
automata (comparators, in short), a new class of automata that read two
infinite sequences of weights synchronously and relate their aggregate values.

We show that aggregate functions that can be represented with Büchi automaton
result in comparators that are finite-state and accept by the Büchi condition
as well. Such $\omega$-regular comparators further lead to generic algorithms
for a number of well-studied problems, including the quantitative inclusion
and winning strategies in quantitative graph games with incomplete
information, as well as related non-decision problems, such as obtaining a
finite representation of all counterexamples in the quantitative inclusion
problem.

We study comparators for two aggregate functions: discounted-sum and limit-
average. We prove that the discounted-sum comparator is $\omega$-regular iff
the discount-factor is an integer. Not every aggregate function, however, has
an $\omega$-regular comparator. Specifically, we show that the language of
sequence-pairs for which limit-average aggregates exist is neither
$\omega$-regular nor $\omega$-context-free. Given this result, we introduce
the notion of prefix-average as a relaxation of limit-average aggregation, and
show that it admits $\omega$-context-free comparators.

###### Key words and phrases:

Comparator automata, aggregate functions, discounted-sum, limit-average,
quantitative inclusion, PSPACE-complete, $\omega$-regular, integer discount-
factor

##  1\. Introduction

Many classic questions in formal methods can be seen as involving comparisons
between different system runs or inputs. Consider the problem of verifying if
a system $S$ satisfies a linear-time temporal property $P$. Traditionally,
this problem is phrased language-theoretically: $S$ and $P$ are interpreted as
sets of (infinite) words, and $S$ is determined to satisfy $P$ if $S\subseteq
P$. The problem, however, can also be framed in terms of a comparison between
words in $S$ and $P$. Suppose a word $w$ is assigned a weight of 1 if it
belongs to the language of the system or property, and 0 otherwise. Then
determining if $S\subseteq P$ amounts to checking whether the weight of every
word in $S$ is less than or equal to its weight in $P$ [5].

The need for such a formulation is clearer in quantitative systems, in which
every run of a word is associated with a sequence of (rational-valued)
weights. The weight of a run is given by aggregate function
$f:\mathbb{Q}^{\omega}\rightarrow\mathbb{R}$, which returns the real-valued
aggregate value of the run’s weight sequence. The weight of a word is given by
the supremum or infimum of the weight of all its runs. Common examples of
aggregate functions include discounted-sum and limit-average.

In a well-studied class of problems involving quantitative systems, the
objective is to check if the aggregate value of words of a system exceed a
constant threshold value [15, 16, 17]. This is a natural generalization of
emptiness problems in qualitative systems. Known solutions to the problem
involve arithmetic reasoning via linear programming and graph algorithms such
as negative-weight cycle detection, computation of maximum weight of cycles
etc [4, 19].

A more general notion of comparison relates aggregate values of two weight
sequences. Such a notion arises in the quantitative inclusion problem for
weighted automata [1], where the goal is to determine whether the weight of
words in one weighted automaton is less than that in another. Here it is
necessary to compare the aggregate value along runs between the two automata.
Approaches based on arithmetic reasoning do not, however, generalize to
solving such problems. In fact, the known solution to discounted-sum inclusion
with integer discount-factor combines linear programming with a specialized
subset-construction-based determinization step, rendering an EXPTIME algorithm
[4, 7]. Yet, this approach does not match the PSPACE lower bound for
discounted-sum inclusion.

In this paper, we present an automata-theoretic formulation of this form of
comparison between weighted sequences. Specifically, we introduce comparator
automata (_comparators_ , in short), a class of automata that read pairs of
infinite weight sequences synchronously, and compare their aggregate values in
an online manner. While comparisons between weight sequences happen implicitly
in prior approaches to quantitative systems, comparator automata make these
comparisons explicit. We show that this has many benefits, including generic
algorithms for a large class of quantitative reasoning problems, as well as a
direct solution to the problem of discounted-sum inclusion that also closes
its complexity gap.

A comparator for aggregate function $f$ for relation $R$ is an automaton that
accepts a pair $(A,B)$ of sequences of bounded rational numbers iff $f(A)$ $R$
$f(B)$, where $R$ is an inequality relation ($>$, $<$, $\geq$, $\leq$, $\neq$)
or the equality relation $=$. A comparator could be finite-state or (pushdown)
infinite-state. This paper studies such comparators.

A comparator is $\omega$-regular if it is finite-state and accepts by the
Büchi condition. We relate $\omega$-regular comparators to $\omega$-regular
aggregate functions [13], and show that $\omega$-regular aggregate-functions
entail $\omega$-regular comparators. However, the other direction is still
open: Does an $\omega$-regular comparator for an aggregate function and a
relation imply that the aggregate function is also $\omega$-regular?
Furthermore, we show that $\omega$-regular comparators lead to generic
algorithms for a number of well-studied problems including the quantitative
inclusion problem, and in showing existence of winning strategies in
incomplete-information quantitative games. Our algorithm yields PSPACE-
completeness of quantitative inclusion when the $\omega$-regular comparator is
provided. The same algorithm extends to obtaining finite-state representations
of counterexample words in inclusion.

Next, we show that the discounted-sum aggregation function admits an
$\omega$-regular comparator for all relations $R$ iff the discount-factor
$d>1$ is an integer. We use this result to prove that discounted-sum aggregate
function for discount-factor $d>1$ is $\omega$-regular iff $d$ is an integer.
Furthermore, we use properties of $\omega$-regular comparators to conclude
that the discounted-sum inclusion is PSPACE-complete, hence resolving the
complexity gap.

Finally, we investigate the limit-average comparator. Since limit-average is
only defined for sequences in which the average of prefixes converge, limit-
average comparison is not well-defined. We show that even a Büchi pushdown
automaton cannot separate sequences for which limit-average exists from those
for which it does not. Hence, we introduce the novel notion of prefix-average
comparison as a relaxation of limit-average comparison. We show that the
prefix-average comparator admits a comparator that is $\omega$-context-free,
i.e., given by a Büchi pushdown automaton, and we discuss the utility of this
characterization.

This paper is organized as follows: Preliminaries are given in § 2. Comparator
automata is formally defined in § 3. The connections between $\omega$-regular
aggregate functions and $\omega$-regular comparators is discussed in Section
3.1. Generic algorithms for $\omega$-regular comparators are discussed in §
3.2-3.3. § 4 discusses discounted-sum aggregate function and its comparators
with non-integer rational discount-factors (§ 4.1) and integer discount-
factors (§ 4.2). The construction and properties of prefix-average comparator
are given in § 5, respectively. We conclude with future directions in § 6.

###  1.1. Related work

The notion of comparison has been widely studied in quantitative settings.
Here we mention only a few of them. Such aggregate-function based notions
appear in weighted automata [1, 18], quantitative games including mean-payoff
and energy games [17], discounted-payoff games [3, 4], in systems regulating
cost, memory consumption, power consumption, verification of quantitative
temporal properties [15, 16], and others. Common solution approaches include
graph algorithms such as weight of cycles or presence of cycle [19], linear-
programming-based approaches, fixed-point-based approaches [9], and the like.
The choice of approach for a problem typically depends on the underlying
aggregate function. In contrast, in this work we present an automata-theoretic
approach that unifies solution approaches to problems on different aggregate
functions. We identify a class of aggregate functions, ones that have an
$\omega$-regular comparator, and present generic algorithms for some of these
problems.

While work on finite-representations of counterexamples and witnesses in the
qualitative setting is known [5], we are not aware of such work in the
quantitative verification domain. This work can be interpreted as automata-
theoretic arithmetic, which has been explored in regular real analysis [13].

##  2\. Preliminaries

[Büchi automaton [21]]

A (finite-state) Büchi automaton is a tuple $\mathcal{A}=(\mathit{S}$,
$\Sigma$, $\delta$, ${\mathit{Init}}$, $\mathcal{F})$, where $\mathit{S}$ is a
finite set of states, $\Sigma$ is a finite input alphabet,
$\delta\subseteq(\mathit{S}\times\Sigma\times\mathit{S})$ is the transition
relation, ${\mathit{Init}}\subseteq\mathit{S}$ is the set of initial states,
and $\mathcal{F}\subseteq\mathit{S}$ is the set of accepting states [21] . A
Büchi automaton is deterministic if for all states $s$ and inputs $a$,
$|\\{s^{\prime}|(s,a,s^{\prime})\in\delta\textrm{ for some
$s^{\prime}$}\\}|\leq 1$ and $|{\mathit{Init}}|=1$. Otherwise, it is
nondeterministic. A Büchi automaton is complete if for all states $s$ and
inputs $a$, $|\\{s^{\prime}|(s,a,s^{\prime})\in\delta\textrm{ for some
$s^{\prime}$}\\}|\geq 1$. For a word $w=w_{0}w_{1}\dots\in\Sigma^{\omega}$, a
run $\rho$ of $w$ is a sequence of states $s_{0}s_{1}\dots$ s.t.
$s_{0}\in{\mathit{Init}}$, and $\tau_{i}=(s_{i},w_{i},s_{i+1})\in\delta$ for
all $i$. Let $\mathit{inf}(\rho)$ denote the set of states that occur
infinitely often in run ${\rho}$. A run $\rho$ is an accepting run if
$\mathit{inf}(\rho)\cap\mathcal{F}\neq\emptyset$. A word $w$ is an accepting
word if it has an accepting run. Büchi automata are closed under set-theoretic
union, intersection, and complementation [21]. Languages accepted by these
automata are called $\omega$-regular languages.

#### Reals over $\omega$-words [13]

Given an integer base $\beta\geq 2$, its digit set is
$\mathsf{Digit}(\beta)=\\{0,\dots,\beta-1\\}$. Let $x\in\mathbb{R}$, then
there exist unique words
$\mathsf{Int}(x,\beta)=z_{0}z_{1}\dots\in\mathsf{Digit}(\beta)^{*}\cdot
0^{\omega}$ and
$\mathsf{Frac}(x,\beta)=f_{0}f_{1}\dots\notin\mathsf{Digit}(\beta)^{*}\cdot(\beta-1)^{\omega}$
such that $|x|=\Sigma_{i=0}^{\infty}\beta^{i}\cdot
z_{i}+\Sigma_{i=0}^{\infty}\frac{f_{i}}{\beta^{i}}$. Thus, $z_{i}$ and $f_{i}$
are respectively the $i$-th least significant digit in the base $\beta$
representation of the integer part of $x$, and the $i$-th most significant
digit in the base $\beta$ representation of the fractional part of $x$. Then,
a real-number $x\in\mathbb{R}$ in base $\beta$ is represented by
$\mathsf{rep}(x,\beta)=\mathsf{sign}\cdot(\mathsf{Int}(x,\beta),\mathsf{Frac}(x,\beta))$,
where $\mathsf{sign}=+$ if $x\geq 0$, $\mathsf{sign}=-$ if $x<0$, and
$(\mathsf{Int}(x,\beta),\mathsf{Frac}(x,\beta))$ is the interleaved word of
$\mathsf{Int}(x,\beta)$ and $\mathsf{Frac}(x,\beta)$. Clearly,
$x=\mathsf{sign}\cdot|x|=\mathsf{sign}\cdot(\Sigma_{i=0}^{\infty}\beta^{i}\cdot
z_{i}+\Sigma_{i=0}^{\infty}\frac{f_{i}}{\beta^{i}})$. For all integer
$\beta\geq 2$, we denote the alphabet of representation of real-numbers in
base $\beta$ by $\mathsf{AlphaRep}(\beta)$. We adopt the definitions of
function automata and regular functions [13] w.r.t. aggregate functions as
follows: [Aggregate function automaton, $\omega$-Regular aggregate function]
Let $\Sigma$ be a finite set, and $\beta\geq 2$ be an integer-valued base. A
Büchi automaton $\mathcal{A}$ over alphabet
$\Sigma\times\mathsf{AlphaRep}(\beta)$ is an aggregate function automata of
type $\Sigma^{\omega}\rightarrow\mathbb{R}$ if the following conditions hold:

  * •

For all $A\in\Sigma^{\omega}$, there exists at most one $x\in\mathbb{R}$ such
that $(A,\mathsf{rep}(x,\beta))\in\mathcal{L}(\mathcal{A})$, and

  * •

For all $A\in\Sigma^{\omega}$, there exists an $x\in\mathbb{R}$ such that
$(A,\mathsf{rep}(x,\beta))\in\mathcal{L}(\mathcal{A})$

$\Sigma$ and $\mathsf{AlphaRep}(\beta)$ are the input and output alphabets,
respectively. An aggregate function $f:\Sigma^{\omega}\rightarrow\mathbb{R}$
is $\omega$-regular under integer base $\beta\geq 2$ if there exists an
aggregate function automaton $\mathcal{A}$ over alphabet
$\Sigma\times\mathsf{AlphaRep}(\beta)$ such that for all sequences
$A\in\Sigma^{\omega}$ and $x\in\mathbb{R}$, $f(A)=x$ iff
$(A,\mathsf{rep}(x,\beta))\in L(\mathcal{A})$.

[Weighted $\omega$-automaton [11, 20]] A weighted automaton over infinite
words is a tuple $\mathcal{A}=(\mathcal{M},\gamma,f)$, where
$\mathcal{M}=(\mathit{S},\Sigma,\delta,{\mathit{Init}},\mathit{S})$ is a Büchi
automaton with all states as accepting, $\gamma:\delta\rightarrow\mathbb{Q}$
is a weight function, and $f:\mathbb{Q}\rightarrow\mathbb{R}$ is the aggregate
function [11, 20]. Words and runs in weighted automata are defined as they are
in Büchi automata. The weight-sequence of run $\rho=s_{0}s_{1}\dots$ of word
$w=w_{0}w_{1}\dots$ is given by $wt_{\rho}=n_{0}n_{1}n_{2}\dots$ where
$n_{i}=\gamma(s_{i},w_{i},s_{i+1})$ for all $i$. The weight of a run $\rho$,
denoted by $f(\rho)$, is given by $f(wt_{\rho})$. Here the weight of a word
$w\in\Sigma^{\omega}$ in weighted automata is defined as
$wt_{\mathcal{A}}(w)=sup\\{f(\rho)|\rho$ is a run of $w$ in $\mathcal{A}\\}$.
In general, weight of a word can also be defined as the infimum of the weight
of all its runs. By convention, if a word $w\notin\mathcal{L}(\mathcal{M})$
its weight $wt_{\mathcal{A}}(w)=-\infty$.

[Quantitative inclusion] Let $P$ and $Q$ be weighted $\omega$-automata with
the same aggregate function $f$. The strict quantitative inclusion problem,
denoted by $P\subset_{f}Q$, asks whether for all words $w\in\Sigma^{\omega}$,
$wt_{P}(w)<wt_{Q}(w)$. The non-strict quantitative inclusion problem, denoted
by $P\subseteq_{f}Q$, asks whether for all words $w\in\Sigma^{\omega}$,
$wt_{P}(w)\leq wt_{Q}(w)$.

Quantitative inclusion, strict and non-strict, is PSPACE-complete for limsup
and liminf [11], and undecidable for limit-average [17]. For discounted-sum
with integer discount-factor it is in EXPTIME [7, 11], and decidability is
unknown for rational discount-factors

[Incomplete-information quantitative games] An incomplete-information
quantitative game is a tuple
$\mathcal{G}=(S,s_{\mathcal{I}},\mathit{O},\Sigma,\delta,\gamma,f)$, where
$S$, $\mathit{O}$, $\Sigma$ are sets of states, observations, and actions,
respectively, $s_{\mathcal{I}}\in S$ is the initial state, $\delta\subseteq
S\times\Sigma\times S$ is the transition relation,
$\gamma:S\rightarrow\mathbb{N}\times\mathbb{N}$ is the weight function, and
$f:\mathbb{N}^{\omega}\rightarrow\mathbb{R}$ is the aggregate function. The
transition relation $\delta$ is complete, i.e., for all states $p$ and actions
$a$, there exists a state $q$ s.t. $(p,a,q)\in\delta$. A play $\rho$ is a
sequence $s_{0}a_{0}s_{1}a_{1}\dots$, where
$\tau_{i}=(s_{i},a_{i},s_{i+1})\in\delta$. The observation of state $s$ is
denoted by $\mathit{O}(s)\in\mathit{O}$. The observed play $o_{\rho}$ of
$\rho$ is the sequence $o_{0}a_{0}o_{1}aa_{1}\dots$, where
$o_{i}=\mathit{O}(s_{i})$. Player $P_{0}$ has incomplete information about the
game $\mathcal{G}$; it only perceives the observation play $o_{\rho}$. Player
$P_{1}$ receives full information and witnesses play $\rho$. Plays begin in
the initial state $s_{0}=s_{\mathcal{I}}$. For $i\geq 0$, Player $P_{0}$
selects action $a_{i}$. Next, player $P_{1}$ selects the state $s_{i+1}$, such
that $(s_{i},a_{i},s_{i+1})\in\delta$. The weight of state $s$ is the pair of
payoffs $\gamma(s)=(\gamma(s)_{0},\gamma(s)_{1})$. The weight sequence
$wt_{i}$ of player $P_{i}$ along $\rho$ is given by
$\gamma(s_{0})_{i}\gamma(s_{1})_{i}\dots$, and its payoff from $\rho$ is given
by $f(wt_{i})$ for aggregate function $f$, denoted by $f(\rho_{i})$, for
simplicity. A play on which a player receives a greater payoff is said to be a
winning play for the player. A strategy for player $P_{0}$ is given by a
function $\alpha:\mathit{O}^{*}\rightarrow\Sigma$ since it only sees
observations. Player $P_{0}$ follows strategy $\alpha$ if for all $i$,
$a_{i}=\alpha(o_{0}\dots o_{i})$. A strategy $\alpha$ is said to be a winning
strategy for player $P_{0}$ if all plays following $\alpha$ are winning plays
for $P_{0}$.

[Büchi pushdown automaton [14]] A _Büchi pushdown automaton (Büchi PDA)_ is a
tuple
$\mathcal{A}=(\mathit{S},\Sigma,\Gamma,\delta,{\mathit{Init}},Z_{0},\mathcal{F})$,
where $\mathit{S}$, $\Sigma$, $\Gamma$, and $\mathcal{F}$ are finite sets of
states, input alphabet, pushdown alphabet and accepting states, respectively.
$\delta\subseteq(\mathit{S}\times\Gamma\times(\Sigma\cup\\{\epsilon\\})\times\mathit{S}\times\Gamma)$
is the transition relation, ${\mathit{Init}}\subseteq\mathit{S}$ is a set of
initial states, $Z_{0}\in\Gamma$ is the start symbol. A _run_ $\rho$ on a word
$w=w_{0}w_{1}\dots\in\Sigma^{\omega}$ of a Büchi PDA $\mathcal{A}$ is a
sequence of configurations $(s_{0},\gamma_{0}),(s_{1},\gamma_{1})\dots$
satisfying (1) $s_{0}\in{\mathit{Init}}$, $\gamma_{0}=Z_{0}$, and (2)
($s_{i},\gamma_{i},w_{i},s_{i+1},\gamma_{i+1})\in\delta$ for all $i$. Büchi
PDA consists of a stack, elements of which are the tokens $\Gamma$, and
initial element $Z_{0}$. Transitions push or pop token(s) to/from the top of
the stack. Let $\mathit{inf}(\rho)$ be the set of states that occur infinitely
often in state sequence $s_{0}s_{1}\dots$ of run $\rho$. A run $\rho$ is an
accepting run in Büchi PDA if
$\mathit{inf}(\rho)\cap\mathcal{F}\neq\emptyset$. A word $w$ is an accepting
word if it has an accepting run. Languages accepted by Büchi PDA are called
$\omega$-context-free languages ($\omega$-CFL).

#### Notation

For an infinite sequence $A=(a_{0},a_{1},\dots)$, $A[i]$ denotes its $i$-th
element, and $A[n,m]$ denotes the finite word $A[n]A[n+1]\dots A[m]$. Abusing
notation, we write $w\in\mathcal{A}$ and $\rho\in\mathcal{A}$ if $w$ and
$\rho$ are an accepting word and an accepting run of $\mathcal{A}$
respectively. An infinite weight-sequence is bounded if the absolute value of
all of its elements are bounded by a fixed number.

For missing proofs and constructions, refer to the supplementary material.

##  3\. Comparator automata

Comparator automata (often abbreviated as comparators) are a class of automata
that can read pairs of weight sequences synchronously and establish an
equality or inequality relationship between these sequences. Formally, we
define: [Comparator automata] Let $\Sigma$ be a finite set of rational
numbers, and $f:\mathbb{Q}^{\omega}\rightarrow\mathbb{R}$ denote an aggregate
function. A comparator automaton for aggregate function $f$ with inequality or
equality relation $R\in\\{\leq,<,\geq,>,=,\neq\\}$ is an automaton over the
alphabet $\Sigma\times\Sigma$ that accepts a pair $(A,B)$ of (infinite) weight
sequences iff $f(A)$ $R$ $f(B)$. From now on, unless mentioned otherwise, we
assume that all weight sequences are bounded, natural-number sequences. The
boundedness assumption is justified since the set of weights forming the
alphabet of a comparator is bounded. For all aggregate functions considered in
this paper, the result of comparison of weight sequences is preserved by a
uniform linear transformation that converts rational-valued weights into
natural numbers; justifying the natural number assumption.

When the comparator for an aggregate function and a relation is a Büchi
automaton, we call it an $\omega$-regular comparator. Likewise, when the
comparator is a Büchi pushdown automaton, we call it an $\omega$-context-free
comparator. Due to closure properties of Büchi automata, if the comparator for
an aggregate function for any one inequality is $\omega$-regular for all
equality and inequality relations, then the comparator for the function for
all inequality and equality relations also $\omega$-regular. Later, we see
that discounted-sum comparator is $\omega$-regular (§ 4) and prefix-average
comparator with $\geq$ (or $\leq$) is $\omega$-context-free (§ 5).

#### Limsup comparator

$s$start$f_{k}$$s_{k}$$(*,*)$$(k,\leq k)$$(k,\leq k)$$(\leq k-1,\leq k)$$(\leq
k-1,\leq k)$$(k,\leq k)$ Figure 1. State $f_{k}$ is an accepting state.
Automaton $\mathcal{A}_{k}$ accepts $(A,B)$ iff $\mathsf{LimSup(A)}=k$,
$\mathsf{LimSup(B)}\leq k$. $*$ denotes $\\{0,1\dots\mu\\}$, $\leq m$ denotes
$\\{0,1\dots,m\\}$

We explain comparators through an example. The limit supremum (limsup, in
short) of a bounded, integer sequence $A$, denoted by $\mathsf{LimSup(A)}$, is
the largest integer that appears infinitely often in $A$. The limsup
comparator for relation $\geq$ is a Büchi automaton that accepts the pair
$(A,B)$ of sequences iff $\mathsf{LimSup(A)}\geq\mathsf{LimSup(B)}$.

The working of the limsup comparator for relation $\geq$ is based on non-
deterministically guessing the limsup of sequences $A$ and $B$, and then
verifying that $\mathsf{LimSup(A)}\geq\mathsf{LimSup(B)}$. Büchi automaton
$\mathcal{A}_{k}$ (Fig. 1) illustrates the basic building block of the limsup
comparator for relation $\geq$. Automaton $\mathcal{A}_{k}$ accepts pair
$(A,B)$ of number sequences iff $\mathsf{LimSup(A)}=k$, and
$\mathsf{LimSup(B)}\leq k$, for integer $k$. (Lemma 1).

######  Lemma 1.

Let $A$ and $B$ be non-negative integer sequences bounded by $\mu$. Büchi
automaton $\mathcal{A}_{k}$ (Fig. 1) accepts $(A,B)$ iff
$\mathsf{LimSup(A)}=k$, and $\mathsf{LimSup(A)}\geq\mathsf{LimSup(B)}$.

######  Proof 3.1.

Let $(A,B)$ have an accepting run in $\mathcal{A}_{k}$. We show that
$\mathsf{LimSup(A)}=k\geq\mathsf{LimSup(B)}$. The accepting run visits state
$f_{k}$ infinitely often. Note that all incoming transitions to accepting
state $f_{k}$ occur on alphabet $(k,\leq k)$ while all transitions between
states $f_{k}$ and $s_{k}$ occur on alphabet $(\leq k,\leq k)$, where $\leq k$
denotes the set $\\{0,1,\dots k\\}$. So, the integer $k$ must appear
infinitely often in $A$ and all elements occurring infinitely often in $A$ and
$B$ are less than or equal to $k$. Therefore, if $(A,B)$ is accepted by
$\mathcal{A}_{k}$ then $\mathsf{LimSup(A)}=k$, and $\mathsf{LimSup(B)}\leq k$,
and $\mathsf{LimSup(A)}\geq\mathsf{LimSup(B)}$.

Conversely, let $\mathsf{LimSup(A)}=k>\mathsf{LimSup(B)}$. We prove that
$(A,B)$ is accepted by $\mathcal{A}_{k}$. For an integer sequence $A$ when
$\mathsf{LimSup(A)}=k$ integers greater than $k$ can occur only a finite
number of times in $A$. Let $l_{A}$ denote the index of the last occurrence of
an integer greater than $k$ in $A$. Similarly, since $\mathsf{LimSup(B)}\leq
k$, let $l_{B}$ be index of the last occurrence of an integer greater than
$k$. Therefore, for sequences $A$ and $B$ integers greater than $k$ will not
occur beyond index $l=\mathit{max}(l_{A},l_{B})$. Büchi automaton
$\mathcal{A}_{k}$ (Fig. 1) non-deterministically determines $l$. On reading
the $l$-th element of input word $(A,B)$, the run of $(A,B)$ exits the start
state $s$ and shifts to accepting state $f_{k}$. Note that all runs beginning
at state $f_{k}$ occur on alphabet $(a,b)$ where $a,b\leq k$. Therefore,
$(A,B)$ can continue its infinite run even after transitioning to $f_{k}$. To
ensure that this is an accepting run, the run must visit accepting state
$f_{k}$ infinitely often. But this must be the case, since $k$ occurs
infinitely often in $A$, and all transitions on $(k,b)$, for all $b\leq k$,
transition into state $f_{k}$. Hence, for all integer sequences $A$,$B$
bounded by $\mu$, if $\mathsf{LimSup(A)}=k$, and
$\mathsf{LimSup(A)}\geq\mathsf{LimSup(B)}$, the automaton accepts $(A,B)$.

######  Theorem 2.

Let $\mu>0$ be an integer upper bound, and $\geq$ be the inequality relation.
The limsup comparator with relation $\geq$ accepting pair of bounded-sequence
$(A,B)$ iff $\mathsf{LimSup((A))}\geq\mathsf{LimSup(B)}$ is $\omega$-regular.

######  Proof 3.2.

The union of Büchi automata $\mathcal{A}_{k}$ (Fig 1, Lemma 1) for
$k\in\\{0,1,\dots\mu\\}$, when $\mu$ is the upper bound results in the limsup
comparator for relation $\geq$.

Due to closure properties of Büchi automata, this implies that limsup
comparator for all inequalities and equality relation is also
$\omega$-regular. The limit infimum (liminf, in short) of an integer sequence
is the smallest integer that appears infinitely often in it; its comparator
has a similar construction to the limsup comparator. One can further prove
that the limsup and liminf aggregate functions are also $\omega$-regular
aggregate functions.

###  3.1. $\omega$-Regular aggregate functions

This section draws out the relationship between $\omega$-regular aggregate
functions and $\omega$-regular comparators. We begin with showing that
$\omega$-regular aggregate functions entails $\omega$-regular comaparators for
the aggregate function.

######  Theorem 3.

Let $\mu>0$ be the upper-bound on weight sequences, and $\beta\geq 2$ be the
integer base. Let $f:\\{0,1,\dots,\mu\\}^{\omega}\rightarrow\mathbb{R}$ be an
aggregate function. If aggregate function $f$ is $\omega$-regular under base
$\beta$, then its comparator for all inequality and equality relations is also
$\omega$-regular.

######  Proof 3.3.

We show that if an aggregate function is $\omega$-regular under base $\beta$,
then its comparator for relation $>$ is $\omega$-regular. By closure
properties of $\omega$-regular comparators, this implies that comparators of
the aggregate function are $\omega$-regular for all inequality and equality
relations.

But first we prove that for a given integer base $\beta\geq 2$ there exists an
automaton $\mathcal{A}_{\beta}$ such that for all $a,b\in\mathbb{R}$,
$\mathcal{A}_{\beta}$ accepts $(\mathsf{rep}(a,\beta),\mathsf{rep}(b,\beta))$
iff $a>b$. Let $a,b\in\mathbb{R}$, and $\beta>2$ be an integer base. Let
$\mathsf{rep}(a,\beta)=\mathsf{sign}_{a}\cdot(\mathsf{Int}(a,\beta),\mathsf{Frac}(a,\beta))$
and
$\mathsf{rep}(b,\beta)=\mathsf{sign}_{b}\cdot(\mathsf{Int}(b,\beta),\mathsf{Frac}(b,\beta))$.
Then, the following statements can be proven using simple evaluation from
definitions:

  * •

When $\mathsf{sign}_{a}=+$ and $\mathsf{sign}_{b}=-$. Then $a>b$.

  * •

When $\mathsf{sign}_{a}=\mathsf{sign}_{b}=+$

    * –

If $\mathsf{Int}(a,\beta)\neq\mathsf{Int}(b,\beta)$: Since
$\mathsf{Int}(a,\beta)$ and $\mathsf{Int}(b,\beta)$ eventually only see digit
$0$ i.e. they are necessarily identical eventually, there exists an index $i$
such that it is the last position where $\mathsf{Int}(a,\beta)$ and
$\mathsf{Int}(b,\beta)$ differ. If
$\mathsf{Int}(a,\beta)[i]>\mathsf{Int}(b,\beta)[i]$, then $a>b$. If
$\mathsf{Int}(a,\beta)[i]<\mathsf{Int}(b,\beta)[i]$, then $a<b$.

    * –

If $\mathsf{Int}(a,\beta)=\mathsf{Int}(b,\beta)$ but
$\mathsf{Frac}(a,\beta)\neq\mathsf{Frac}(b,\beta)$: Let $i$ be the first index
where $\mathsf{Frac}(a,\beta)$ and $\mathsf{Frac}(b,\beta)$ differ. If
$\mathsf{Frac}(a,\beta)[i]>\mathsf{Frac}(b,\beta)[i]$ then $a>b$. If
$\mathsf{Frac}(a,\beta)[i]<\mathsf{Frac}(b,\beta)[i]$ then $a<b$.

    * –

Finally, if $\mathsf{Int}(a,\beta)=\mathsf{Int}(b,\beta)$ and
$\mathsf{Frac}(a,\beta)=\mathsf{Frac}(b,\beta)$: Then $a=b$.

  * •

When $\mathsf{sign}_{a}=\mathsf{sign}_{b}=-$

    * –

If $\mathsf{Int}(a,\beta)\neq\mathsf{Int}(b,\beta)$: Since
$\mathsf{Int}(a,\beta)$ and $\mathsf{Int}(b,\beta)$ eventually only see digit
$0$ i.e. they are necessarily identical eventually. Therefore, there exists an
index $i$ such that it is the last position where $\mathsf{Int}(a,\beta)$ and
$\mathsf{Int}(b,\beta)$ differ. If
$\mathsf{Int}(a,\beta)[i]>\mathsf{Int}(b,\beta)[i]$, then $a<b$. If
$\mathsf{Int}(a,\beta)[i]<\mathsf{Int}(b,\beta)[i]$, then $a>b$.

    * –

If $\mathsf{Int}(a,\beta)=\mathsf{Int}(b,\beta)$ but
$\mathsf{Frac}(a,\beta)\neq\mathsf{Frac}(b,\beta)$: Let $i$ be the first index
where $\mathsf{Frac}(a,\beta)$ and $\mathsf{Frac}(b,\beta)$ differ. If
$\mathsf{Frac}(a,\beta)[i]>\mathsf{Frac}(b,\beta)[i]$ then $a<b$. If
$\mathsf{Frac}(a,\beta)[i]<\mathsf{Frac}(b,\beta)[i]$ then $a>b$.

    * –

Finally, if $\mathsf{Int}(a,\beta)=\mathsf{Int}(b,\beta)$ and
$\mathsf{Frac}(a,\beta)=\mathsf{Frac}(b,\beta)$: Then $a=b$.

  * •

When $\mathsf{sign}_{a}=-$ and $\mathsf{sign}_{b}=+$. Then $a<b$.

Since the conditions given above are exhaustive and mutually exclusive, we
conclude that for all $a,b\in\mathbb{R}$ and integer base $\beta\geq 2$, let
$\mathsf{rep}(a,\beta)=\mathsf{sign}_{a}\cdot(\mathsf{Int}(a,\beta),\mathsf{Frac}(a,\beta))$
and
$\mathsf{rep}(b,\beta)=\mathsf{sign}_{b}\cdot(\mathsf{Int}(b,\beta),\mathsf{Frac}(b,\beta))$.
Then $a>b$ iff one of the following conditions occurs:

  1. (1)

$\mathsf{sign}_{a}=+$ and $\mathsf{sign}_{b}=-$.

  2. (2)

$\mathsf{sign}_{a}=\mathsf{sign}_{b}=+$,
$\mathsf{Int}(a,\beta)\neq\mathsf{Int}(b,\beta)$, and
$\mathsf{Int}(a,\beta)[i]>\mathsf{Int}(b,\beta)[i]$ when $i$ is the last index
where $\mathsf{Int}(a,\beta)$ and $\mathsf{Int}(b,\beta)$ differ.

  3. (3)

$\mathsf{sign}_{a}=\mathsf{sign}_{b}=+$,
$\mathsf{Int}(a,\beta)=\mathsf{Int}(b,\beta)$,
$\mathsf{Frac}(a,\beta)\neq\mathsf{Frac}(b,\beta)$, and
$\mathsf{Int}(a,\beta)[i]>\mathsf{Int}(b,\beta)[i]$ when $i$ is the first
index where $\mathsf{Frac}(a,\beta)$ and $\mathsf{Frac}(b,\beta)$ differ.

  4. (4)

$\mathsf{sign}_{a}=\mathsf{sign}_{b}=+$,
$\mathsf{Int}(a,\beta)\neq\mathsf{Int}(b,\beta)$, and
$\mathsf{Int}(a,\beta)[i]<\mathsf{Int}(b,\beta)[i]$ when $i$ is the last index
where $\mathsf{Int}(a,\beta)$ and $\mathsf{Int}(b,\beta)$ differ.

  5. (5)

$\mathsf{sign}_{a}=\mathsf{sign}_{b}=+$,
$\mathsf{Int}(a,\beta)=\mathsf{Int}(b,\beta)$,
$\mathsf{Frac}(a,\beta)\neq\mathsf{Frac}(b,\beta)$, and
$\mathsf{Int}(a,\beta)[i]<\mathsf{Int}(b,\beta)[i]$ when $i$ is the first
index where $\mathsf{Frac}(a,\beta)$ and $\mathsf{Frac}(b,\beta)$ differ.

Note that each of these five condition can be easily expressed by a Büchi
automaton over alphabet $\mathsf{AlphaRep(\beta)}$ for an integer $\beta\geq
2$. For an integer $\beta\geq 2$, the union of all these Büchi automata will
result in a Büchi automaton $\mathcal{A}_{\beta}$ such that for all
$a,b\in\mathbb{R}$ and $A=\mathsf{rep}(a,\beta)$ and
$B=\mathsf{rep}(b,\beta)$, $a>b$ iff interleaved word
$(A,B)\in\mathcal{L}(\mathcal{A}_{\beta})$.

Now we come to the main part of the proof. Let
$f:\Sigma^{\omega}\rightarrow\mathbb{R}$ be an $\omega$-regular aggregate
function with aggregate function automata $\mathcal{A}_{f}$. We will construct
an $\omega$-regular comparator for $f$ with relation $>$. Note that $(X,Y)$ is
present in the comparator iff $(X,M),(Y,N)\in\mathcal{A}_{f}$ for
$M,N\in\mathsf{AlphaRep}(\beta)^{\omega}$ and $(M,N)\in\mathcal{A}_{\beta}$,
for $\mathcal{A}_{\beta}$ as described above. Since $\mathcal{A}_{f}$ and
$\mathcal{A}_{\beta}$ are both Büchi automata, the comparator for function $f$
with relation $>$ is also a Büchi auotmaton. Therefore, the comparator for
aggregate function $f$ with relation $>$ is $\omega$-regular.

The converse direction of whether $\omega$-regular comparator for an aggregate
function $f$ for all inequality or equality relations will entail
$\omega$-regular functions under an integer base $\beta\geq 0$ is trickier.
For all aggregate functions considered in this paper, we see that whenever the
comparator is $\omega$-regular, the aggregate function is $\omega$-regular as
well. However, the proofs for this have been done on a case-by-cass basis, and
we do not have an algorithmic procedure to derive a function (Büchi) automaton
from its $\omega$-regular comparator. We also do not have an example of an
aggregate function for which the comparator is $\omega$-regular but the
function is not. Therefore, we arrive at the following conjecture:

######  Conjecture 4.

Let $\mu>0$ be the upper-bound on weight sequences, and $\beta\geq 2$ be the
integer base. Let $f:\\{0,1,\dots,\mu\\}^{\omega}\rightarrow\mathbb{R}$ be an
aggregate function. If the comparator for an aggregate function $f$ is
$\omega$-regular for all inequality and equality relations, then its aggregate
function is also $\omega$-regular under base $\beta$.

###  3.2. Quantitative inclusion

The aggregate function or comparator of a quantitative inclusion problem refer
to the aggregate function or comparator of the associated aggregate function.
This section presents a generic algorithm (Algorithm 1) to solve quantitative
inlcusion between $\omega$-weighted automata $P$ and $Q$ with
$\omega$-comparators. This section focusses on the non-strict quantitative
inclusion. $\mathsf{InclusionReg}$ (Algorithm 1) is an algorithm for
quantitative inclusion between weighted $\omega$-automata $P$ and $Q$ with
$\omega$-regular comparator $\mathcal{A}_{f}$ for relation $\geq$.
$\mathsf{InclusionReg}$ takes $P$,$Q$ and $\mathcal{A}_{f}$ as input, and
returns $\mathsf{True}$ iff $P\subseteq_{f}Q$. The results for strict
quantitative inclusion are similar. We use the following motivating example to
explain steps of Algorithm 1.

#### Motivating example

$p_{1}$start$p_{2}$$a,1$$a,1$ Figure 2. Weighted automaton $P$

$q_{1}$start$q_{2}$$a,0$$a,2$$a,1$ Figure 3. Weighted automaton $Q$

Let weighted $\omega$-automata $P$ and $Q$ be as illustrated in Fig. 3-3 with
the limsup aggregate function. The word $w=a^{\omega}$ has one run
$\rho^{P}_{1}=p_{1}p_{2}^{\omega}$ with weight sequence
$wt^{P}_{1}=1^{\omega}$ in $P$ and two runs $\rho^{Q}_{1}=q_{1}q_{2}^{\omega}$
with weight sequence $wt^{Q}_{1}=0,1^{\omega}$ and run
$\rho^{Q}_{2}=q_{1}q_{2}^{\omega}$ with weight sequence
$wt^{Q}_{2}=2,1^{\omega}$. Clearly, $wt_{P}(w)\leq wt_{Q}(w$). Therefore
$P\subseteq_{f}Q$. From Theorem 2 we know that the limsup comparator
$\mathcal{A}_{\mathsf{LS}}^{\leq}$ for $\leq$ is $\omega$-regular.

We use Algorithm 1 to show that $P\subseteq_{f}Q$ using its $\omega$-regular
comparator for $\leq$. Intuitively, the algorithm must be able to identify
that for run $\rho^{P}_{1}$ of $w$ in $P$, there exists a run $\rho^{Q}_{2}$
in $Q$ s.t. $(wt^{P}_{1},wt^{Q}_{2})$ is accepted by the limsup comparator for
$\leq$.

#### Key ideas

A run $\rho_{P}$ in $P$ on word $w\in\Sigma^{\omega}$ is said to be dominated
w.r.t $P\subseteq_{f}Q$ if there exists a run $\rho_{Q}$ in $Q$ on the same
word $w$ such that $wt_{P}(\rho_{P})\leq wt_{Q}(\rho_{Q})$. $P\subseteq_{f}Q$
holds if for every run $\rho_{P}$ in $P$ is dominated w.r.t.
$P\subseteq_{f}Q$.

$\mathsf{InclusionReg}$ constructs Büchi automaton $\mathit{Dom}$ that
consists of exactly the domianted runs of $P$ w.r.t $P\subseteq_{f}Q$.
$\mathsf{InclusionReg}$ returns $\mathsf{True}$ iff $\mathit{Dom}$ contains
all runs of $P$. To obtain $\mathit{Dom}$, it constructs Büchi automaton
$\mathit{DomProof}$ that accepts word $(\rho_{P},\rho_{Q})$ iff $\rho_{P}$ and
$\rho_{Q}$ are runs of the same word in $P$ and $Q$ respectively, and
$wt_{P}(\rho_{P})\leq wt_{Q}(\rho_{Q})$ i.e. if $w_{P}$ and $w_{Q}$ are weight
sequence of $\rho_{P}$ and $\rho_{Q}$, respectively, then $(w_{P},w_{Q})$ is
present in the $\omega$-regular comparator $\mathcal{A}_{f}^{\leq}$ for
aggregate function $f$ with relation $\leq$. The projection of
$\mathit{DomProof}$ on runs of $P$ results in $\mathit{Dom}$.

Algorithm 1 $\mathsf{InclusionReg}(P,Q,\mathcal{A}_{f})$, Is
$P\subseteq_{f}Q$?

1: Input:  Weighted automata $P$, $Q$, and $\omega$-regular comparator
$\mathcal{A}_{f}$ (Inequality $\leq$)

2: Output:  $\mathsf{True}$ if $P\subseteq_{f}Q$, $\mathsf{False}$ otherwise

3: $\hat{P}\leftarrow\mathsf{AugmentWtAndLabel}(P)$

4: $\hat{Q}\leftarrow\mathsf{AugmentWtAndLabel}(Q)$

5: $\hat{P}\times\hat{Q}\leftarrow\mathsf{MakeProduct}(\hat{P},\hat{Q})$

6:
$\mathit{DomProof}\leftarrow\mathsf{Intersect}(\hat{P}\times\hat{Q},\mathcal{A}_{\succeq})$

7: $\mathit{Dom}\leftarrow\mathsf{FirstProject}(\mathit{DomProof})$

8: return $\hat{P}\equiv\mathit{Dom}$

#### Algorithm details

For sake a simplicity, we assume that every word present in $P$ is also
present in $Q$ i.e. $P\subseteq Q$ (qualitative inclusion).
$\mathsf{InclusionReg}$ has three steps: (a). $\mathsf{UniqueId}$ (Lines 3-4):
Enables unique identification of runs in $P$ and $Q$ through labels. (b).
$\mathsf{Compare}$ (Lines 5-7): Compares weight of runs in $P$ with weight of
runs in $Q$, and constructs $\mathit{Dom}$. (c). $\mathsf{DimEnsure}$ (Line
8): Ensures if all runs of $P$ are diminished.

  1. (1)

$\mathsf{UniqueId}$: $\mathsf{AugmentWtAndLabel}$ transforms weighted
$\omega$-automaton $\mathcal{A}$ into Büchi automaton $\hat{\mathcal{A}}$ by
converting transition $\tau=(s,a,t)$ with weight $\gamma(\tau)$ in
$\mathcal{A}$ to transition $\hat{\tau}=(s,(a,\gamma(\tau),l),t)$ in
$\hat{\mathcal{A}}$, where $l$ is a unique label assigned to transition
$\tau$. The word
$\hat{\rho}=(a_{0},n_{0},l_{0})(a_{1},n_{1},l_{1})\dots\in\hat{A}$ iff run
$\rho\in\mathcal{A}$ on word $a_{0}a_{1}\dots$ with weight sequence
$n_{0}n_{1}\dots$. Labels ensure bijection between runs in $\mathcal{A}$ and
words in $\hat{\mathcal{A}}$. Words of $\hat{A}$ have a single run in
$\hat{A}$. Hence, transformation of weighted $\omega$-automata $P$ and $Q$ to
Büchi automata $\hat{P}$ and $\hat{Q}$ enables disambiguation between runs of
$P$ and $Q$ (Line 3-4).

The corresponding $\hat{A}$ for weighted $\omega$-automata $P$ and $Q$ from
Figure 3\- 3 are given in Figure 6\- 6 respectively.

$p_{1}$start$p_{2}$$(a,1,1)$$(a,1,2)$ Figure 4. $\hat{P}$

$q_{1}$start$q_{2}$$(a,0,1)$$(a,2,2)$$(a,1,3)$ Figure 5. $\hat{Q}$

$p_{1},q_{1}$start$p_{2},q_{2}$$(a,1,1,0,1)$$(a,1,1,2,2)$$(a,1,2,1,3)$ Figure
6. $\hat{P}\times\hat{Q}$

  2. (2)

$\mathsf{Compare}$: The output of this step is the Büchi automaton
$\mathit{Dom}$, that contains the word ${\hat{\rho}}\in\hat{P}$ iff $\rho$ is
a dominated run in $P$ w.r.t $P\subseteq_{f}Q$ (Lines 5-7).

$\mathsf{MakeProduct}(\hat{P},\hat{Q})$ constructs $\hat{P}\times\hat{Q}$ s.t.
word $(\hat{\rho_{P}},\hat{\rho_{Q}})\in\hat{P}\times\hat{Q}$ iff $\rho_{P}$
and $\rho_{Q}$ are runs of the same word in $P$ and $Q$ respectively (Line 5).
Concretely, for transition
$\hat{\tau_{\mathcal{A}}}=(s_{\mathcal{A}},(a,n_{\mathcal{A}},l_{\mathcal{A}}),t_{\mathcal{A}})$
in automaton $\mathcal{A}$, where $\mathcal{A}\in\\{\hat{P},\hat{Q}\\}$,
transition
$\hat{\tau_{P}}\times\hat{\tau_{Q}}=((s_{P},s_{Q}),(a,n_{P},l_{P},n_{Q},l_{Q}),(t_{P},t_{Q}))$
is in $\hat{P}\times\hat{Q}$, as shown in Figure 6.

$\mathsf{Intersect}$ intersects the weight components of
$\hat{P}\times\hat{Q}$ with comparator $\mathcal{A}_{f}^{\leq}$ (Line 6). The
resulting automaton $\mathit{DomProof}$ accepts word
$(\hat{\rho_{P}},\hat{\rho_{Q}})$ iff $f(\rho_{P})\leq f(\rho_{Q})$, and
$\rho_{P}$ and $\rho_{Q}$ are runs on the same word in $P$ and $Q$
respectively. The result of $\mathsf{Intersect}$ between
$\hat{P}\times\hat{Q}$ with the limsup comparator
$\mathcal{A}_{\mathsf{LS}}^{\leq}$ for relation $\leq$ (Figure 9) is given in
Figure 9.

The projection of $\mathit{DomProof}$ on the words of $\hat{P}$ returns
$\mathit{Dom}$ which contains the word $\hat{\rho_{P}}$ iff $\rho_{P}$ is a
dominated run in $P$ w.r.t $P\subseteq_{f}Q$ (Line 7), as shown in Figure 9.

$s_{1}$start$s_{2}$$s_{3}$$(1,2)$$(1,0)$$(1,1)$$(1,1)$ Figure 7. Snippet of
limsup comparator $\mathcal{A}_{\mathsf{LS}}^{\leq}$ for relation $\leq$

$s_{1}$start$s_{2}$$(a,1,1,2,2)$$(a,1,2,1,3)$ Figure 8. $\mathsf{Intersect}$

$p_{1}$start$p_{2}$$(a,1,1)$$(a,1,2)$ Figure 9. $\mathit{Dom}$

  3. (3)

$\mathsf{DimEnsure}$: $P\subseteq_{f}Q$ iff $\hat{P}\equiv\mathit{Dom}$
(qualitative equivalence) since $\hat{P}$ consists of all runs of $P$ and
$\mathit{Dom}$ consists of all domianted runs w.r.t $P\subseteq_{f}Q$ (Line
8).

######  Lemma 5.

Büchi automaton $\mathit{Dom}$ consists of all domianted runs in $P$ w.r.t
$P\subseteq_{f}Q$.

######  Proof 3.4.

Let $\mathcal{A}_{f}^{\leq}$ be the comparator for $\omega$-regular aggregate
function $f$ and relation $\leq$ s.t. $\mathcal{A}_{f}$ accepts $(A,B)$ iff
$f(A)\leq f(B)$. A run $\rho$ over word $w$ with weight sequence $wt$ in $P$
(or $Q$) is represented by the unique word $\hat{\rho}=(w,wt,l)$ in $\hat{P}$
(or $\hat{Q}$) where $l$ is the unique label sequence associated with each run
in $P$ (or $Q$). Since every label on each transition is separate, $\hat{P}$
and $\hat{Q}$ are deterministic automata. Now, $\hat{P}\times\hat{Q}$ is
constructed by ensuring that two transitions are combined in the product only
if their alphabet is the same. Therefore if
$(w,wt_{1},l_{1},wt_{2},l_{2})\in\hat{P}\times\hat{Q}$, then
$\hat{\rho}=(w,wt_{1},l_{1})\in\hat{P}$,
$\hat{\sigma}=(w,wt_{2},l_{2})\in\hat{Q}$. Hence, there exist runs $\rho$ and
$\sigma$ with weight sequences $wt_{1}$ and $wt_{2}$ in $P$ and $Q$,
respectively. Next, $\hat{P}\times\hat{Q}$ is intersected over the weight
sequences with $\omega$-regular comparator $\mathcal{A}_{f}^{\leq}$ for
aggregate function $f$ and relation $\leq$. Therefore
$(w,wt_{1},l_{1},wt_{2},l_{2})\in\mathit{DomProof}$ iff $f(wt_{1})\leq
f(wt_{2})$. Therefore runs $\rho$ in $P$ and $\sigma$ in $Q$ are runs on the
same word s.t. aggregate weight in $P$ is less than or equal to that of
$\sigma$ in $Q$. Therefore $\mathit{Dom}$ constitutes of these $\hat{\rho}$.
Therefore $\mathit{Dom}$ consists of $\hat{\rho}$ only if $\rho$ is a
dominated run in $P$ w.r.t $P\subseteq_{f}Q$.

Every step of the algorithm has a two-way implication, hence it is also true
that every dominated run in $P$ w.r.t $P\subseteq_{f}Q$ is present in
$\mathit{Dom}$.

######  Lemma 6.

Given weighted $\omega$-automata $P$ and $Q$ and their $\omega$-regular
comparator $\mathcal{A}_{f}^{\leq}$ for aggregate function $f$ and relation
$\leq$. $\mathsf{InclusionReg}(P,Q,\mathcal{A}_{f})$ returns $\mathsf{True}$
iff $P\subseteq_{f}Q$.

######  Proof 3.5.

$\hat{P}$ consists of all runs of $P$. $\mathit{Dom}$ consists of all
dominated run in $P$ w.r.t $P\subseteq_{f}Q$. $P\subseteq_{f}Q$ iff every run
of $P$ is dominated w.r.t $P\subseteq_{f}Q$. Therefore $P\subseteq_{f}Q$ is
given by whether $\hat{P}\equiv\mathit{Dom}$, where $\equiv$ denotes
qualitative equivalence.

Algorithm $\mathsf{InclusionReg}$ is adapted for strict quantitative inclusion
$P\subset_{f}Q$ by repeating the same procedure with $\omega$-regular
comparator $\mathcal{A}_{f}^{<}$ for aggregate function $f$ and relation $<$.
Here, a run $\rho_{P}$ in $P$ on word $w\in\Sigma^{\omega}$ is said to be
dominated w.r.t $P\subset_{f}Q$ if there exists a run $\rho_{Q}$ in $Q$ on the
same word $w$ such that $wt_{P}(\rho_{P})<wt_{Q}(\rho_{Q})$. Similarly for
quantitative equivalence $P\equiv_{f}Q$.

We give the complexity analysis of quantitative-inclusion with
$\omega$-regular comparators.

######  Theorem 7.

Let $P$ and $Q$ be weighted $\omega$-automata and $\mathcal{A}_{f}$ be an
$\omega$-regular comparator. Quantitative inclusion problem, quantitative
strict-inclusion problem, and quantitative equivalence problem for
$\omega$-regular aggregate function $f$ is $\mathsf{PSPACE}$-complete.

######  Proof 3.6.

All operations in $\mathsf{InclusionReg}$ until Line 7 are polytime operations
in the size of weighted $\omega$-automata $P$, $Q$ and comparator
$\mathcal{A}_{f}$. Hence, $\mathit{Dom}$ is polynomial in size of $P$, $Q$ and
$\mathcal{A}_{f}$. Line 8 solves a $\mathsf{PSPACE}$-complete problem.
Therefore, the quantitative inclusion for $\omega$-regular aggregate function
$f$ is in $\mathsf{PSPACE}$ in size of the inputs $P$, $Q$, and
$\mathcal{A}_{f}$.

The $\mathsf{PSPACE}$-hardness of the quantitative inclusion is established
via reduction from the qualitative inclusion problem, which is
$\mathsf{PSPACE}$-complete. The formal reduction is as follows: Let $P$ and
$Q$ be Büchi automata (with all states as accepting states). Reduce $P$, $Q$
to weighted automata $\overline{P}$, $\overline{Q}$ by assigning a weight of 1
to each transition. Since all runs in $\overline{P}$, $\overline{Q}$ have the
same weight sequence, weight of all words in $\overline{P}$ and $\overline{Q}$
is the same for any function $f$. It is easy to see $P\subseteq Q$
(qualitative inclusion) iff $\overline{P}\subseteq_{f}\overline{Q}$
(quantitative inclusion).

Theorem 7 extends to weighted $\omega$-automata when weight of words is the
infimum of weight of runs. The key idea for $P\subseteq_{f}Q$ here is to
ensure that for every run $\rho_{Q}$ in $Q$ there exists a run on the same
word in $\rho_{P}$ in $P$ s.t. $f(\rho_{P})\leq f(\rho_{Q})$.

#### Representation of counterexamples

When $P\nsubseteq_{f}Q$, there exists word(s) $w\in\Sigma^{*}$ s.t
$wt_{P}(w)>wt_{Q}(w)$. Such a word $w$ is said to be a counterexample word.
Previously, finite-state representations of counterexamples have been useful
in verification and synthesis in qualitative systems [5], and could be useful
in quantitative settings as well. However, we are not aware of procedures for
such representations in the quantitative settings. Here we show that a trivial
extension of $\mathsf{InclusionReg}$ yields Büchi automata-representations for
all counterexamples of the quantitative inclusion problem for $\omega$-regular
functions.

######  Theorem 8.

All counterexamples of the quantitative inclusion problem for an
$\omega$-regular aggregate function can be expressed by a Büchi automaton.

######  Proof 3.7.

For word $w$ to be a counterexample, it must contain a run in $P$ that is not
dominated. Clearly, all non-dominated runs of $P$ w.r.t to the quantitative
inclusion are members of $\hat{P}\setminus\mathit{Dom}$. The counterexamples
words can be obtained from $\hat{P}\setminus\mathit{Dom}$ by modifying its
alphabet to the alphabet of $P$ by dropping transition weights and their
unique labels.

###  3.3. Incomplete-information quantitative games

Given an incomplete-information quantitative game
$\mathcal{G}=(S,s_{\mathcal{I}},\mathit{O},\Sigma,\delta,\gamma,f)$, our
objective is to determine if player $P_{0}$ has a winning strategy
$\alpha:\mathit{O}^{*}\rightarrow\Sigma$ for $\omega$-regular aggregate
function $f$. We assume we are given the $\omega$-regular comparator
$\mathcal{A}_{f}$ for function $f$. Note that a function $A^{*}\rightarrow B$
can be treated like a $B$-labeled $A$-tree, and vice-versa. Hence, we proceed
by finding a $\Sigma$-labeled $\mathit{O}$-tree – the winning strategy tree.
Every branch of a winning strategy-tree is an observed play $o_{\rho}$ of
$\mathcal{G}$ for which every actual play $\rho$ is a winning play for
$P_{0}$.

We first consider all game trees of $\mathcal{G}$ by interpreting
$\mathcal{G}$ as a tree-automaton over $\Sigma$-labeled $S$-trees. Nodes $n\in
S^{*}$ of the game-tree correspond to states in $S$ and labeled by actions in
$\Sigma$ taken by player $P_{0}$. Thus, the root node $\varepsilon$
corresponds to $s_{\mathcal{I}}$, and a node $s_{i_{0}},\ldots,s_{i_{k}}$
corresponds to the state $s_{i_{k}}$ reached via
$s_{\mathcal{I}},s_{i_{0}},\ldots,s_{i_{k-1}}$. Consider now a node $x$
corresponding to state $s$ and labeled by an action $\sigma$. Then $x$ has
children $xs_{1},\ldots xs_{n}$, for every $s_{i}\in S$. If
$s_{i}\in\delta(s,\sigma)$, then we call $xs_{i}$ a _valid_ child, otherwise
we call it an _invalid_ child. Branches that contain invalid children
correspond to invalid plays.

A game-tree $\tau$ is a winning tree for player $P_{0}$ if every branch of
$\tau$ is either a winning play for $P_{0}$ or an invalid play of
$\mathcal{G}$. One can check, using an automata, if a play is invalid by the
presence of invalid children. Furthermore, the winning condition for $P_{0}$
can be expressed by the $\omega$-regular comparator $\mathcal{A}_{f}$ that
accepts $(A,B)$ iff $f(A)>f(B)$. To use the comparator $\mathcal{A}_{f}$, it
is determinized to parity automaton $D_{f}$. Thus, a product of game
$\mathcal{G}$ with $D_{f}$ is a deterministic parity tree-automaton accepting
precisely winning-trees for player $P_{0}$.

Winning trees for player $P_{0}$ are $\Sigma$-labeled $S$-trees. We need to
convert them to $\Sigma$-labeled $\mathit{O}$-trees. Recall that every state
has a unique observation. We can simulate these $\Sigma$-labeled $S$-trees on
strategy trees using the technique of thinning states $S$ to observations
$\mathit{O}$ [kupferman2000synthesis]. The resulting alternating parity tree
automaton $\mathcal{M}$ will accept a $\Sigma$-labeled $\mathit{O}$-tree
$\tau_{o}$ iff for all actual game-tree $\tau$ of $\tau_{o}$, $\tau$ is a
winning-tree for $P_{0}$ with respect to the strategy $\tau_{o}$. The problem
of existence of winning-strategy for $P_{0}$ is then reduced to non-emptiness
checking of $\mathcal{M}$.

######  Theorem 9.

Given an incomplete-information quantitative game $\mathcal{G}$ and
$\omega$-regular comparator $\mathcal{A}_{f}$ for the aggregate function $f$,
the complexity of determining whether $P_{0}$ has a winning strategy is
exponential in ${|\mathcal{G}|\cdot|D_{f}|}$, where
$|D_{f}|=|\mathcal{A}_{f}|^{O(|\mathcal{A}_{f}|)}$.

Since, $D_{f}$ is the deterministic parity automaton equivalent to
$A_{f},|D_{f}|=|\mathcal{A}_{f}|^{O(|\mathcal{A}_{f}|)}$. The thinning
operation is linear in size of $|\mathcal{G}\times D_{f}|$, therefore
$|\mathcal{M}|=|\mathcal{G}|\cdot|D_{f}|$. Non-emptiness checking of
alternating parity tree automata is exponential. Therefore, our procedure is
doubly exponential in size of the comparator and exponential in size of the
game. The question of tighter bounds is open.

##  4\. Discounted-sum comparator

The discounted-sum of an infinite sequence $A$ with discount-factor $d>1$,
denoted by $\mathit{DS}({A},{d})$, is defined as
$\Sigma_{i=0}^{\infty}A[i]/d^{i}$, and the discounted-sum of a finite sequence
$A$ is $\Sigma_{i=0}^{|A|-1}A[i]/d^{i}$. The discounted-sum comparator (DS-
comparator, in short) for discount-factor $d$ and relation R, denoted by
$\mathcal{A}_{d}^{R}$, accepts a pair $(A,B)$ of (infinite length) weight
sequences iff $\mathit{DS}({A},{d})$ $R$ $\mathit{DS}({B},{d})$. We
investigate properties of the DS-comparator, and show that the DS-comparator
is $\omega$-regular iff the discount-factor $d>1$ is an integer. We also show
that the discounted-sum aggregate function is $\omega$-regular iff the
discount-factor is an integer. Finally, we show the repercussions of the above
results on quantitative inclusion with discounted-sum aggregate function (DS-
inclusion, in short). Section 4.1 and Section 4.2 deal with the non-integer
rational discount-factors and integer discount-factors, respectively.

###  4.1. Non-integer, rational discount-factor

For a weighted $\omega$-automaton $\mathcal{A}$ and a real number
$r\in\mathbb{R}$, the cut-point language of $\mathcal{A}$ w.r.t. $r$ is
defined as $L^{\geq r}=\\{w\in L(\mathcal{A})|wt_{\mathcal{A}}(w)\geq r\\}$
[10]. When the discount factor is a rational value $1<d<2$, it is known that
not all deterministic weighted $\omega$-automaton with discounted-sum
aggregate function (DS-automaton, in short) have an $\omega$-regular cut-point
language for an $r\in\mathbb{R}$ [10]. In this section, we extended this
result to to all non-integer, rational discount-factors $d>1$. Finally, we use
the extension to show that DS-comparator for non-integer, rational discount-
factors $d>1$ is not $\omega$-regular. Consequently, also proving that
discounted-sum is not an $\omega$-regular aggregate function when its
discount-factor is a non-integer rational number.

Note that the result on cut-point languages from [10] has motivated the proof
for impossibility of determinization of weighted $\omega$-automata with
discounted-sum aggregate function with non-integer discount-factors [7].
However, the direct link with cut-point languages is unclear. Here, we give a
simpler extension of the proof in [10] to generalize it to all non-integer
rational discount-factors.

######  Theorem 10.

For all non-integer, rational discount-factor $d>1$, there exists a
deterministic discounted-sum automata $\mathcal{A}$ and rational value
$r\in\mathbb{R}$ for which its cut-point language is not $\omega$-regular.

######  Proof 4.1.

Since the proof for $1<d<2$ has been presented in [10], we skip that case.

The proof presented here extends the earlier result on $1<d<2$ from [10] to
all non-integer, rational discount factors $d>1$.

Let $d>2$ be a non-integer, rational discount-factor. Define deterministic
discounted-sum automata $\mathcal{A}$ over the alphabet $\\{0,1,\dots,\lceil
d\rceil-1\\}$ such that the weight of transitions on alphabet
$n\in\\{0,1,\dots,\lceil d\rceil-1\\}$ is $n$. Therefore, weight of word
$w\in\mathcal{A}$ is $\mathit{DS}({w},{d})$. Consider its cut-point language
$L^{\geq(\lceil d\rceil-1)}$. We say a finite-length word $w$ is ambiguous iff
$\lceil d\rceil-1-\frac{1}{d^{|w|-1}}\cdot\frac{\lceil d\rceil-1}{d-1}\leq
DS(w,d)<\lceil d\rceil-1$. Intuitively, a finite word $w$ is ambiguous if it
can be extended into infinite words in $\mathcal{A}$ such that some extensions
lie in $L^{\geq(\lceil d\rceil-1)}$ and some do not. Clearly, the finite word
$w=\lceil d\rceil-2$ is ambiguous. Note that when $d>2$ is non-integer,
rational valued, then $\frac{\lceil d\rceil-1}{d-1}>1$, so word $\lceil
d\rceil-2$ falls within the range for ambiguity. We claim that if finite word
$w$ is ambiguous, then either $w\cdot(\lceil d\rceil-2)$ or $w\cdot(\lceil
d\rceil-1)$ is ambiguous. To prove ambiguity, we need to show that $\lceil
d\rceil-1-\frac{1}{d^{|w|}}\cdot\frac{\lceil
d\rceil-1}{d-1}\leq\mathit{DS}({w\cdot(\lceil d\rceil-k)},{d})<\lceil
d\rceil-1$, for $k\in\\{1,2\\}$. Note, $\mathit{DS}({w\cdot(\lceil
d\rceil-2)},{d})=\mathit{DS}({w},{d})+\frac{1}{d^{|w|}}\cdot(\lceil
d\rceil-2)$, and $\mathit{DS}({w\cdot(\lceil
d\rceil-1)},{d})=\mathit{DS}({w},{d})+\frac{1}{d^{|w|}}\cdot(\lceil
d\rceil-1)$. Simplifying the expressions for $w\cdot(\lceil d\rceil-1)$ and
$w\cdot(\lceil d\rceil-2)$, we need to prove either $\lceil
d\rceil-1-\frac{1}{d^{|w|+1}}\cdot\frac{\lceil
d\rceil-1}{d-1}\leq\mathit{DS}({w},{d})<\lceil
d\rceil-1-\frac{1}{d^{|w|}}\cdot(\lceil d\rceil-1)$ or $\lceil
d\rceil-1-\frac{1}{d^{|w|}}\cdot\frac{\lceil
d\rceil-1}{d-1}-\frac{1}{d^{|w|}}\cdot(\lceil
d\rceil-2)\leq\mathit{DS}({w},{d})<\lceil
d\rceil-1-\frac{1}{d^{|w|}}\cdot(\lceil d\rceil-2)$. Now, this is true if
$\lceil d\rceil-1-\frac{1}{d^{|w|}}\cdot\frac{\lceil
d\rceil-1}{d-1}-\frac{1}{d^{|w|}}\cdot(\lceil d\rceil-2)<\lceil
d\rceil-1-\frac{1}{d^{|w|}}\cdot(\lceil d\rceil-1)$ which is equivalent $d>2$
is a is non-integer, rational discount-factor. Therefore, every ambiguous
finite word can be extended to another ambiguous word. This means there exists
an infinite word $w^{\geq}$ such that $\mathit{DS}({w^{\geq}},{d})=\lceil
d\rceil-1$ and all finite prefixes of $w^{\geq}$ are ambiguous.

Let us assume that the language $L^{\geq(\lceil d\rceil-1)}$ is
$\omega$-regular and represented by Büchi automaton $\mathcal{B}$. For $n<m$,
let the $n$\- and $m$-length prefixes of $w^{\geq}$, denoted $w^{\geq}[0,n-1]$
and $w^{\geq}[0,m-1]$, respectively, be such that they reach the same states
in $\mathcal{B}$. Then there exists an infinite length word $w_{s}$ such that
$\mathit{DS}({w^{\geq}[0,n-1]\cdot
w_{s}},{d})=\mathit{DS}({w^{\geq}[0,m-1]\cdot w_{s}},{d})=\lceil d\rceil-1$.
Now, $\mathit{DS}({w^{\geq}[0,n-1]\cdot
w_{s}},{d})=\mathit{DS}({w^{\geq}[0,n-1]},{d})+\frac{1}{d^{n}}\cdot\mathit{DS}({w_{s}},{d})$
and $\mathit{DS}({w^{\geq}[0,m-1]\cdot
w_{s}},{d})=\mathit{DS}({w^{\geq}[0,m-1]},{d})+\frac{1}{d^{m}}\cdot\mathit{DS}({w_{s}},{d})$.
Eliminating $\mathit{DS}({w_{s}},{d})$ from the equations and simplification,
we get:

$d^{m-1}\cdot(\mathit{DS}({w^{\geq}[0,m-1]},{d})-(\lceil
d\rceil-1))+d^{n-1}\cdot(\mathit{DS}({w^{\geq}[0,n-1]},{d})-(\lceil
d\rceil-1))=0$

The above is a polynomial over $d$ with degree $m-1$ and integer co-
efficients. Specifically, $d=\frac{p}{q}>2$ such that integers $p,q>1$, and
$p$ and $q$ are mutually prime. Since $d=\frac{p}{q}$ is a root of the above
equation, $q$ must divide co-efficient of the highest degree term, in this
case it is $m-1$. The co-efficient of the highest degree term in the
polynomial above is $(w^{\geq}[0]-(\lceil d\rceil-1))$. Recall from
construction of $w^{\geq}$ above, $w^{\geq}[0]=\lceil d\rceil-2$. So the co-
efficient of the highest degree term is $-1$, which is not divisible by
integer $q>1$. Contradiction.

Finally, we use Theorem 10 to prove the discounted-sum comparator is not
$\omega$-regular when the discount-factor $d>1$ is non-integer, rational
number.

######  Theorem 11.

DS-comparator for non-integer, rational discount-factors $d>1$ for all
inequalities and equality are not $\omega$-regular.

######  Proof 4.2.

If the comparator for an aggregate function for any one inequality is not
$\omega$-regular, then the comparator for all inequalities and equality
relation will also not be $\omega$-regular. Therefore, it is sufficient to
prove that the discounted-sum comparator with non-integer, rational value for
relation $\geq$ is not $\omega$-regular.

Let $d>1$ be a non-integer, rational discount-fact. Let $\mathcal{A}$ be the
discounted-sum automaton as described in proof of Lemma 10. Consider its cut-
point language $L^{\geq(\lceil d\rceil-1)}$. From Lemma 10 and [10], we know
that $L^{\geq(\lceil d\rceil-1)}$ is not an $\omega$-regular language.

Suppose there exists an $\omega$-regular DS-comparator
$\mathcal{A}_{d}^{\leq}$ for non-integer rational discount factor $d>1$ for
relation $\geq$. We define the Büchi automaton $\mathcal{P}$ s.t.
$\mathcal{L}(\mathcal{P})=\\{(w,v)|w\in\mathcal{L}(\mathcal{A}),v=\lceil
d\rceil-1\cdot 0^{\omega}\\}$. Note that $\mathit{DS}({\lceil d\rceil-1\cdot
0^{\omega}},{d})=\lceil d\rceil-1$. . Then the cut-point language
$L^{\geq(\lceil d\rceil-1)}$ of deterministic discounted-sum automata
$\mathcal{A}$ can be constructed by taking the intersection of $\mathcal{P}$
with $\mathcal{A}_{d}^{\geq}$. Since all actions are closed under
$\omega$-regular operations, $L^{\geq 1}$ can be represented by a Büchi
automaton. Contradiction to Theorem 10.

######  Theorem 12.

Let $d>1$ be a non-integer, rational discount-factor. The discounted-sum
aggregate function with discount-factor $d$ is not $\omega$-regular.

######  Proof 4.3.

Immediate from Lemma 10 and Theorem 3.

Since the DS-comparator for all non-integer, rational discount-factor $d>1$ is
not $\omega$-regular, the $\omega$-regular-based algorithm for quantitative
inclusion described in Algorithm 1 does not apply to DS-inclusion. In fact,
the decidability of DS-inclusion with non-integer, rational discount-factors
is still open.

###  4.2. Integer discount-factor

In this section, we provide an explicit construction of an $\omega$-regular
comparator for discounted-sum with integer discount-factors. We use this
construction to prove that discounted-sum aggregate function with integer
discount-factor is $\omega$-regular. Finally, we use the $\omega$-regular DS-
comparator in Algorithm 1 to establish $\mathsf{PSPACE}$-completeness of DS-
inclusion with integer discount-factors.

#### Discounted-sum comparator

Let integer $\mu>0$ be the upper-bound on sequences. The core intuition is
that bounded sequences can be converted to their value in base $d$ via a
finite-state transducer. Lexicographic comparison of the converted sequences
renders the desired DS-comparator. Conversion of sequences to base $d$
requires a certain amount of look-ahead by the transducer. Here we describe a
method that directly incorporates the look-ahead with lexicographic comparison
to obtain the DS-comparator for integer discount-factor $d>1$. Here we
construct the discounted-sum comparator for relation $<$.

We explain the construction in detail now. For weight sequence $A$ and integer
discount-factor $d>1$, $\mathit{DS}({A},{d})$ can be interpreted as a value in
base $d$ i.e.
$\mathit{DS}({A},{d})=A[0]+\frac{A[1]}{d}+\frac{A[2]}{d^{2}}+\dots=(A[0].A[1]A[2]\dots)_{d}$
[13]. Unlike comparison of numbers in base $d$, the lexicographically larger
sequence may not be larger in value since (i) The elements of weight sequences
may be larger in value than base $d$, and (ii) Every value has multiple
infinite-sequence representations.

To overcome these challenges, we resort to arithmetic techniques in base $d$.
Note that $\mathit{DS}({B},{d})>\mathit{DS}({A},{d})$ iff there exists a
sequence $C$ such that
$\mathit{DS}({B},{d})=\mathit{DS}({A},{d})+\mathit{DS}({C},{d})$, and
$\mathit{DS}({C},{d})>0$. Therefore, to compare the discounted-sum of $A$ and
$B$, we obtain a sequence $C$. Arithmetic in base $d$ also results in sequence
$X$ of carry elements. Then:

######  Lemma 13.

Let $A,B,C,X$ be weight sequences, $d>1$ be a positive integer such that
following equations holds true:

  1. (1)

When $i=0$, $A[0]+C[0]+X[0]=B[0]$

  2. (2)

When $i\geq 1$, $A[i]+C[i]+X[i]=B[i]+d\cdot X[i-1]$

Then $\mathit{DS}({B},{d})=\mathit{DS}({A},{d})+\mathit{DS}({C},{d})$.

######  Proof 4.4.

$\mathit{DS}({A},{d})+\mathit{DS}({C},{d})=\Sigma_{i=0}^{\infty}A[i]\frac{1}{d^{i}}+\Sigma_{i=0}^{\infty}C[i]\frac{1}{d^{i}}=\Sigma_{i=0}^{\infty}(A[i]+C[i])\frac{1}{d^{i}}=(B[0]-X[0])+\Sigma_{i=1}^{\infty}(B[i]+d\cdot
X[i-1]-X[i])\frac{1}{d^{i}}=(B[0]-X[0])+\Sigma_{i=1}^{\infty}(B[i]+d\cdot
X[i-1]-X[i])\frac{1}{d^{i}}=\Sigma_{i=0}^{\infty}B[i]\cdot\frac{1}{d^{i}}-\Sigma_{i=0}^{\infty}X[i]+\Sigma_{i=0}^{\infty}X[i]=\Sigma_{i=0}^{\infty}B[i]\cdot\frac{1}{d^{i}}=\mathit{DS}({B},{d})$

Hence to determine $\mathit{DS}({B},{d})-\mathit{DS}({A},{d})$, systematically
guess sequences $C$ and $X$ using the equations, element-by-element beginning
with the 0-th index and moving rightwards. There are two crucial observations
here: (i) Computation of $i$-th element of $C$ and $X$ only depends on $i$-th
and $(i-1)$-th elements of $A$ and $B$. Therefore guessing $C[i]$ and $X[i]$
requires finite memory only. (ii) Intuitively, $C$ refers to a representation
of value $\mathit{DS}({B},{d})-\mathit{DS}({A},{d})$ in base $d$ and $X$ is
the carry-sequence. If we can prove that $X$ and $C$ are also bounded-
sequences and can be constructed from a finite-set of integers, we would be
able to further proceed to construct a Büchi automaton for the desired
comparator.

We proceed by providing an inductive construction of sequences $C$ and $X$
that satisfy properties in Lemma 13 (Lemma 14), and show that these sequences
are bounded when $A$ and $B$ are bounded. In particular, when $A$ and $B$ are
bounded integer-sequences, then sequences $C$ and $X$ constructed here are
also bounded-integer sequences. Therefore, they are be constructed from a
finite-set of integers. Proofs for sequence $C$ are in Lemma 15-Lemma 17, and
proof for sequence $X$ is in Lemma 18.

We begin with introducing some notation. Let
$\mathit{DS}^{-}(B,A,d,i)=\Sigma^{i}_{j=0}(B[j]-A[j])\cdot\frac{1}{d^{j}}$ for
all index $i\geq 0$. Also, let
$\mathit{DS}^{-}(B,A,d,\cdot)=\Sigma^{\infty}_{j=0}(B[j]-A[j])\cdot\frac{1}{d^{j}}=\mathit{DS}({B},{d})-\mathit{DS}({A},{d})$.
Define $\mathit{maxC}=\mu\cdot\frac{d}{d-1}$. We define the residual function
$\mathit{Res}:\mathbb{N}\cup\\{0\\}\mapsto\mathbb{R}$ as follows:

$\mathit{Res}(i)=\begin{cases}\mathit{DS}^{-}(B,A,d,\cdot)-\lfloor\mathit{DS}^{-}(B,A,d,\cdot)\rfloor&\text{if
}i=0\\\ \mathit{Res}(i-1)-\lfloor\mathit{Res}(i-1)\cdot
d^{i}\rfloor\cdot\frac{1}{d^{i}}&\text{otherwise}\end{cases}$

Then we define $C[i]$ as follows:

$C[i]=\begin{cases}\lfloor\mathit{DS}^{-}(B,A,d,\cdot)\rfloor&\text{if }i=0\\\
\lfloor\mathit{Res}(i-1)\cdot d^{i}\rfloor&\text{otherwise}\end{cases}$

Intuitively, $C[i]$ is computed by _stripping off_ the value of the $i$-th
digit in a representation of $\mathit{DS}^{-}(B,A,d,\cdot)$ in base $d$.
$C[i]$ denotes the numerical value of the $i$-th position of the difference
between $B$ and $A$. The residual function denotes the numerical value of the
difference remaining after assigning the value of $C[i]$ until that $i$.

We define function
$\mathit{CSum}(i):\mathbb{N}\cup\\{0\\}\rightarrow\mathbb{Z}$ s.t.
$\mathit{CSum}(i)=\Sigma_{j=0}^{i}C[j]\cdot\frac{1}{d^{j}}$. Then, we define
$X[i]$ as follows:

$X[i]=(\mathit{DS}^{-}(B,A,d,i)-\mathit{CSum}(i))\cdot d^{i}$

Therefore, we have defined sequences $C$ and $X$ as above. We now prove the
desired properties one-by-one.

First, we establish sequences $C$, $X$ as defined here satisfy Equations 1-2
from Lemma 13. Therefore, ensuring that $C$ is indeed the difference between
sequences $B$ and $A$, and $X$ is their carry-sequence.

######  Lemma 14.

Let $A$ and $B$ be bounded integer sequences and $C$ and $X$ be defined as
above. Then,

  1. (1)

$B[0]=A[0]+C[0]+X[0]$

  2. (2)

For $i\geq 1$, $B[i]+d\cdot X[i-1]=A[i]+C[i]+X[i]$

######  Proof 4.5.

We prove this by induction on $i$ using definition of function $X$.

When $i=0$, then $X[0]=\mathit{DS}^{-}(B,A,d,0)-\mathit{CSum}(0)\implies
X[0]=B[0]-A[0]-C[0]\implies B[0]=A[0]+C[0]+X[0]$.

When $i=1$, then $X[1]=(\mathit{DS}^{-}(B,A,d,1)-\mathit{CSum}(1))\cdot
d=(B[0]+B[1]\cdot\frac{1}{d})-(A[0]+A[1]\cdot\frac{1}{d})-(C[0]+C[1]\cdot\frac{1}{d}))\cdot
d\implies X[1]=B[0]\cdot d+B[1]-(A[0]\cdot d+A[1])-(C[0]\cdot d+C[1])$. From
the above we obtain $X[1]=d\cdot X[0]+B[1]-A[1]-C[1]\implies B[1]+d\cdot
X[0]=A[1]+C[1]+X[1]$.

Suppose the invariant holds true for all $i\leq n$, we show that it is true
for $n+1$. $X[n+1]=(\mathit{DS}^{-}(B,A,d,n+1)-\mathit{CSum}(n+1))\cdot
d^{n+1}\implies X[n+1]=(\mathit{DS}^{-}(B,A,d,n)-\mathit{CSum}(n))\cdot
d^{n+1}+(B[n+1]-A[n+1]-C[n+1])\implies X[n+1]=X[n]\cdot
d+B[n+1]-A[n+1]-C[n+1]\implies B[n+1]+X[n]\cdot d=A[n+1]+C[n+1]+X[n+1]$.

Next, we establish the sequence $C$ is a bounded integer-sequences, therefore
it can be represented by a finite-set of integers. First of all, by definition
of $C[i]$ it is clear that $C[i]$ is an integer for all $i\geq 0$. We are left
with proving boundedness of $C$. Lemma 15-Lemma 17 establish boundedness of
$C[i]$.

######  Lemma 15.

For all $i\geq 0$,
$\mathit{Res}(i)=\mathit{DS}^{-}(B,A,d,\cdot)-\mathit{CSum}(i)$.

######  Proof 4.6.

Proof by simple induction on the definitions of functions $\mathit{Res}$ and
$C$.

  1. (1)

When $i=0$,
$\mathit{Res}(0)=\mathit{DS}^{-}(B,A,d,\cdot)-\lfloor\mathit{DS}^{-}(B,A,d,\cdot)\rfloor$.
By definition of $C[0]$,
$\mathit{Res}(0)=\mathit{DS}^{-}(B,A,d,\cdot)-C[0]\iff\mathit{Res}(0)=\mathit{DS}^{-}(B,A,d,\cdot)-\mathit{CSum}(0)$.

  2. (2)

Suppose the induction hypothesis is true for all $i<n$. We prove it is true
when $i=n$. When $i=n$,
$\mathit{Res}(n)=\mathit{Res}(n-1)-\lfloor\mathit{Res}(n-1)\cdot
d^{n}\rfloor\cdot\frac{1}{d^{n}}$. By definition of $C[n]$ and I.H, we get
$\mathit{Res}(n)=(\mathit{DS}^{-}(B,A,d,\cdot)-\mathit{CSum}(n-1))-C[n]\cdot\frac{1}{d^{n}}$.
Therefore $\mathit{Res}(n)=\mathit{DS}^{-}(B,A,d,\cdot)-\mathit{CSum}(n)$.

######  Lemma 16.

When $\mathit{DS}^{-}(B,A,d,\cdot)\geq 0$, for all $i\geq 0$,
$0\leq\mathit{Res}(i)<\frac{1}{d^{i}}$.

######  Proof 4.7.

Since, $\mathit{DS}^{-}(B,A,d,\cdot)\geq 0$,
$\mathit{Res}(0)=\mathit{DS}^{-}(B,A,d,\cdot)-\lfloor\mathit{DS}^{-}(B,A,d,\cdot)\rfloor\geq
0$ and
$\mathit{Res}(0)=\mathit{DS}^{-}(B,A,d,\cdot)-\lfloor\mathit{DS}^{-}(B,A,d,\cdot)\rfloor<1$
. Specifically, $0\leq\mathit{Res}(0)<1$.

Suppose for all $i\leq k$, $0\leq\mathit{Res}(i)<\frac{1}{d^{i}}$. We show
this is true even for $k+1$.

Since $\mathit{Res}(k)\geq 0$, $\mathit{Res}(k)\cdot d^{k+1}\geq 0$. Let
$\mathit{Res}(k)\cdot d^{k+1}=x+f$, for integral $x\geq 0$, and fractional
$0\leq f<1$. Then, from definition of $\mathit{Res}$, we get
$\mathit{Res}(k+1)=\frac{x+f}{d^{k+1}}-\frac{x}{d^{k+1}}\implies\mathit{Res}(k+1)<\frac{1}{d^{k+1}}$.

Also, $\mathit{Res}(k+1)\geq 0$ since $a-\lfloor a\rfloor\geq 0$ for all
positive values of $a$ (Lemma 15).

######  Lemma 17.

Let $\mathit{maxC}=\mu\cdot\frac{d}{d-1}$. When
$\mathit{DS}^{-}(B,A,d,\cdot)\geq 0$, for $i=0$, $0\leq
C(0)\leq\mathit{maxC}$, and for $i\geq 1$, $0\leq C(i)<d$.

######  Proof 4.8.

Since both $A$ and $B$ are non-negative bounded weight sequences, maximum
value of $\mathit{DS}^{-}(B,A,d,\cdot)$ is when $B=\\{\mu\\}_{i}$ and
$A=\\{0\\}_{i}$. In this case $\mathit{DS}^{-}(B,A,d,\cdot)=\mathit{maxC}$.
Therefore, $0\leq C[0]\leq\mathit{maxC}$.

From Lemma 16, we know that for all $i$,
$0\leq\mathit{Res}(i)<\frac{1}{d^{i}}$. Alternately, when $i\geq 1$,
$0\leq\mathit{Res}(i-1)<\frac{1}{d^{i-1}}\implies 0\leq\mathit{Res}(i-1)\cdot
d^{i}<\frac{1}{d^{i-1}}\cdot d^{i}\implies 0\leq\mathit{Res}(i-1)\cdot
d^{i}<d\implies 0\leq\lfloor\mathit{Res}(i-1)\cdot d^{i}\rfloor<d\implies
0\leq C[i]<d$.

Therefore, we have established that sequence $C$ is non-negative integer-
valued and is bounded by $\mathit{maxC}=\mu\cdot\frac{d}{d-1}$.

Finally, we prove that sequence $X$ is also a bounded-integer sequence,
thereby proving that it is bounded, and can be represented with a finite-set
of integers. Note that for all $i\geq 0$, by expanding out the definition of
$X[i]$ we get that $X[i]$ is an integer for all $i\geq 0$. We are left with
proving boundedness of $X$:

######  Lemma 18.

Let $\mathit{maxX}=1+\frac{\mu}{d-1}$. When $\mathit{DS}^{-}(B,A,d,\cdot)\geq
0$, then for all $i\geq 0$, $|X(i)|\leq\mathit{maxX}$.

######  Proof 4.9.

From definition of $X$, we know that
$X(i)=(\mathit{DS}^{-}(B,A,d,i)-\mathit{CSum}(i))\cdot d^{i}\implies
X(i)\cdot\frac{1}{d^{i}}=\mathit{DS}^{-}(B,A,d,i)-\mathit{CSum}(i)$. From
Lemma 15 we get
$X(i)\cdot\frac{1}{d^{i}}=\mathit{DS}^{-}(B,A,d,i)-(\mathit{DS}^{-}(B,A,d,\cdot)-\mathit{Res}(i))\implies
X(i)\cdot\frac{1}{d^{i}}=\mathit{Res}(i)-(\mathit{DS}^{-}(B,A,d,\cdot)-\mathit{DS}^{-}(B,A,d,i))\implies
X(i)\cdot\frac{1}{d^{i}}=\mathit{Res}(i)-(\Sigma_{j=i+1}^{\infty}(B[j]-A[j])\cdot\frac{1}{d^{j}})\implies|X(i)\cdot\frac{1}{d^{i}}|\leq|\mathit{Res}(i)|+|(\Sigma_{j=i+1}^{\infty}(B[j]-A[j])\cdot\frac{1}{d^{j}})|\implies|X(i)\cdot\frac{1}{d^{i}}|\leq|\mathit{Res}(i)|+\frac{1}{d^{i+1}}\cdot|(\Sigma_{j=0}^{\infty}(B[j+i+1]-A[j+i+1])\cdot\frac{1}{d^{j}})|\implies|X(i)\cdot\frac{1}{d^{i}}|\leq|\mathit{Res}(i)|+\frac{1}{d^{i+1}}\cdot|\mathit{maxC}|$.
From Lemma 16, this implies
$|X(i)\cdot\frac{1}{d^{i}}|\leq\frac{1}{d^{i}}+\frac{1}{d^{i+1}}\cdot|\mathit{maxC}|\implies|X(i)|\leq
1+\frac{1}{d}\cdot|\mathit{maxC}|\implies|X(i)|\leq
1+\frac{\mu}{d-1}\implies|X(i)|\leq\mathit{maxX}$

We summarize our results from 14-Lemma 18 as follows:

######  Corollary 19.

Let $d>1$ be an integer discount-factor. Let $A$ and $B$ be non-negative
integer sequences bounded by $\mu$, and
$\mathit{DS}({A},{d})<\mathit{DS}({B},{d})$. Then there exists bounded
integer-valued sequences $X$ and $C$ that satisfy the conditions in Lemma 13.
Furthermore, $C$ and $X$ are bounded as follows:

  1. (1)

$0\leq C[0]\leq\mu\cdot\frac{d}{d-1}$ and for all $i\geq 1$, $0\leq C[i]<d$,

  2. (2)

For all $i\geq 0$, $0\leq|X[i]|\leq 1+\frac{\mu}{d-1}$

Intuitively, we construct a Büchi automaton $\mathcal{A}_{d}^{<}$ with states
of the form $(x,c)$ where $x$ and $c$ range over all possible values of $X$
and $C$, respectively, and a special initial state $s$. Transitions over
alphabet $(a,b)$ replicate the equations in Lemma 13. i.e. transitions from
the start state $(s,(a,b),(x,c))$ satisfy $a+c+x=b$ to replicate Equation 1
(Lemma 13) at the 0-th index, and all other transitions
$((x_{1},c_{1}),(a,b),(x_{2},c_{2}))$ satisfy $a+c_{2}+x_{2}=b+d\cdot x_{1}$
to replicate Equation 2 (Lemma 13) at indexes $i>0$. Full construction is as
follows:

#### Construction

Let $\mu_{C}=\mu\cdot\frac{d}{d-1}$ and $\mu_{X}=1+\frac{\mu}{d-1}$.
$\mathcal{A}_{d}^{<}=(\mathit{S},\Sigma,\delta_{d},{\mathit{Init}},\mathcal{F})$

  * •

$\mathit{S}=\\{s\\}\cup\mathcal{F}\cup S_{\bot}$ where
$\mathcal{F}=\\{(x,c)||x|\leq\mu_{X},0\leq c\leq\mu_{C}\\}$, and
$S_{\bot}=\\{(x,\bot)||x|\leq\mu_{X}\\}$ where $\bot$ is a special character,
and $c\in\mathbb{N}$, $x\in\mathbb{Z}$.

  * •

State $s$ is the initial state, and $\mathcal{F}$ are accepting states

  * •

$\Sigma=\\{(a,b):0\leq a,b\leq\mu\\}$ where $a$ and $b$ are integers.

  * •

$\delta_{d}\subseteq\mathit{S}\times\Sigma\times\mathit{S}$ is defined as
follows:

    1. (1)

Transitions from start state $s$:

      1. i

$(s,(a,b),(x,c))$ for all $(x,c)\in\mathcal{F}$ s.t. $a+x+c=b$ and $c\neq 0$

      2. ii

$(s,(a,b),(x,\bot))$ for all $(x,\bot)\in S_{\bot}$ s.t. $a+x=b$

    2. (2)

Transitions within $S_{\bot}$: $((x,\bot),(a,b),(x^{\prime},\bot))$ for all
$(x,\bot)$, $(x^{\prime},\bot)\in S_{\bot}$, if $a+x^{\prime}=b+d\cdot x$

    3. (3)

Transitions within $\mathcal{F}$: $((x,c),(a,b),(x^{\prime},c^{\prime}))$ for
all $(x,c)$, $(x^{\prime},c^{\prime})\in\mathcal{F}$ where $c^{\prime}<d$, if
$a+x^{\prime}+c^{\prime}=b+d\cdot x$

    4. (4)

Transition between $S_{\bot}$ and $\mathcal{F}$:
$((x,\bot),(a,b),(x^{\prime},c^{\prime}))$ for all $(x,\bot)\in S_{\bot}$,
$(x^{\prime},c^{\prime})\in\mathcal{F}$ where $0<c^{\prime}<d$, if
$a+x^{\prime}+c^{\prime}=b+d\cdot x$

######  Theorem 20.

Let $d>1$ be an integer discount-factor, and $\mu>1$ be an integer upper-
bound. Büchi automaton $\mathcal{A}_{d}^{<}$ accepts pair of bounded sequences
$(A,B)$ iff $\mathit{DS}({A},{d})\leq\mathit{DS}({B},{d})$. The Büchi
automaton has $\mathcal{O}(\frac{\mu^{2}}{d})$-many states.

######  Proof 4.10.

Corollary 19 proves that if $\mathit{DS}({A},{d})<\mathit{DS}({B},{d})$ then
sequence $X$ and $C$ satisfying the integer sequence criteria and bounded-
criteria will exist. Let these sequences be $X=X[0]X[1]\dots$ and
$C=[0]C[1]\dots$. Since $\mathit{DS}({C},{d})>0$, there exists an index $i\geq
0$ where $C[i]>0$. Let the first position where $C[i]>0$ be index $j$. By
construction of $\mathcal{A}_{d}^{<}$, the state sequence given by
$s,(X[0],\bot)\dots,(X[j-1],\bot),(X[j],C[j]),(X[j+1],C[j+1])\dots$, where for
all $i\geq j$, $C[i]\neq\bot$, forms a run of word $(A,B)$ in the Büchi
automaton. Furthermore, this run is accepting since state $(x,c)$ where
$c\neq\bot$ are accepting states. Therefore, ($A,B)$ is an accepting word in
$\mathcal{A}_{d}^{<}$.

To prove the other direction, suppose the pair of sequence $(A,B)$ has an
accepting run with state sequence $s$,
$(x_{0},\bot),\dots(x_{j-1},\bot),(x_{j},c_{j}),(x_{j+1},c_{j+1})\dots$, where
for all $i\geq j$, $c_{j}\neq\bot$. Construct sequence X and C as follows: For
all $i\geq 0$, $X[i]=x_{i}$. For all $i<j$, $C[i]=0$ and for all $i\geq j$
$C[i]=c_{i}$. Then the transitions of $\mathcal{A}_{d}^{<}$ guarantees
equations Equation 1\- 2 from Lemma 13 to hold for sequences $A$,$B$ and
$C$,$X$. Therefore, it must be the case that
$\mathit{DS}({B},{d})=\mathit{DS}({A},{d})+\mathit{DS}({C},{d})$. Furthermore,
since the first transition to accepting states $(x,c)$ where $c\neq\bot$ is
possible only if $c>0$, $\mathit{DS}({C},{d})>0$. Therefore,
$\mathit{DS}({A},{d})<\mathit{DS}({B},{d})$. Therefore, $\mathcal{A}_{d}^{<}$
accepts $(A,B)$ if $\mathit{DS}({A},{d})<\mathit{DS}({B},{d})$.

######  Corollary 21.

DS-comparator for integer discount-factors $d>1$ for all inequalities and
equality are $\omega$-regular.

######  Proof 4.11.

Immediate from Theorem 20, and closure properties of Büchi automaton.

Constructions of DS-comparator with integer discount-factor $d>1$ for non-
strict inequality $\leq$ and equality $=$ follow similarly and also have
$\mathcal{O}(\frac{\mu^{2}}{d})$-many states.

#### Discounted-sum aggregate function

We use the $\omega$-regular comparator for DS-aggregate function for integer
discount-factor to prove that discounted-sum with integer discount-factors is
an $\omega$-regular aggregate function.

######  Theorem 22.

Let $d>1$ be an integer discount-factor. The discounted-sum aggregate function
with discount-factor $d$ is $\omega$-regular under base $d$.

######  Proof 4.12.

We define the discounted-sum aggregate function automaton (DS-function
automaton, in short): For integer $\mu>0$, let $\Sigma=\\{0,1,\dots\mu\\}$ be
the input alphabet of DS-function, and $d>1$ be its integer base. Büchi
automaton $\mathcal{A}^{\mu}_{d}$ over alphabet
$\Sigma\times\mathsf{AlphaRep}(d)$ is a DS-function automaton of type
$\Sigma^{\omega}\rightarrow\mathbb{R}$ if for all $A\in\Sigma^{\omega}$,
$(A,\mathsf{rep}(\mathit{DS}({A},{d})),d)\in\mathcal{A}^{\mu}_{d}$. Here we
prove that such a $\mathcal{A}_{d}^{\mu}$ exists.

Let $\mu>0$ be the integer upper-bound. Let $\mathcal{A}^{=}_{d}$ be the DS-
comparator for integer discount-factor $d>1$ for relation $=$. Intersect
$\mathcal{A}^{=}_{d}$ with the Büchi automata consisting of all infinite words
from alphabet $\\{0,1\dots\mu\\}\times\\{0,\dots,d-1\\}$. The resulting
automaton $\mathcal{B}$ accepts $(A,B)$ for $A\in\\{0,\dots,\mu\\}^{\omega}$
and $B\in\\{0,\dots,d-1\\}^{\omega}$ iff
$\mathit{DS}({A},{d})=\mathit{DS}({B},{d})$.

Since all elements of $B$ are bounded by $d-1$, $\mathit{DS}({B},{d})$ can be
represented as an $\omega$-word as follows: Let $B=B[0],B[1]\dots$, then its
$\omega$-word representation in base $d$ is given by
$+\cdot(\mathsf{Int}(\mathit{DS}({B},{d}),d),\mathsf{Frac}(\mathit{DS}({B},{d}),d))$
where $\mathsf{Int}(\mathit{DS}({B},{d}),d)=B[0]\cdot 0^{\omega}$ and
$\mathsf{Frac}(\mathit{DS}({B},{d}),d)=B[1],B[2]\dots$. This transformation of
integer sequence $B$ into its $\omega$-regular word form in base $d$ can be
achieved with a simple transducer $\mathcal{T}$.

Therefore, application of transducer $\mathcal{T}$ to Büchi automaton
$\mathcal{B}$ will result in a Büchi automaton over the alphabet
$\Sigma\times\mathsf{AlphaRep}(d)$ such that for all $A\in\Sigma^{\omega}$ the
automaton accepts $(A,\mathsf{rep}(\mathit{DS}({A},{d}),d))$. This is exactly
the DS-function automaton over input alphabet $\Sigma$ and integer base $d>1$.
Therefore, the discounted-sum aggregate function with integer discount-factors
in $\omega$-regular.

Recall, this proof works only for the discounted-sum aggregate function with
integer discount-factor. In general, there is no known procedure to derive a
function automaton from an $\omega$-regular comparator (Conjecture 4).

#### DS-inclusion

For discounted-sum with integer discount-factor it is in EXPTIME [7, 11] which
does not match with its existing PSPACE lower bound. In this section, we use
the $\omega$-regular DS-comparator for integer to close the gap, and establish
PSPACE-completeness of DS-inclusion.

######  Corollary 23.

Let integer $\mu>1$ be the maximum weight on transitions in DS-automata $P$
and $Q$, and $d>1$ be an integer discount-factor. Let $\mu$ and $d$ be
represented in unary form. Then DS-inclusion, DS-strict-inclusion, and DS-
equivalence between are $\mathsf{PSPACE}$-complete.

######  Proof 4.13.

Since size of DS-comparator is polynomial w.r.t. to upper bound $\mu$, when
represented in unary, (Theorem 20), DS-inclusion is $\mathsf{PSPACE}$ in size
of input weighted $\omega$-automata and $\mu$ (Theorem 7).

Not only does this result improve upon the previously known upper bound of
$\mathsf{EXPTIME}$ but it also closes the gap between upper and lower bounds
for DS-inclusion. The earlier known EXPTIME upper bound in complexity is based
on an exponential determinization construction (subset construction) combined
with arithmetical reasoning [7, 11]. We observe that the determinization
construction can be performed on-the-fly in $\mathsf{PSPACE}$. To perform,
however, the arithmetical reasoning on-the-fly in PSPACE would require
essentially using the same bit-level ($(x,c)$-state) techniques that we have
used to construct DS-comparator.

##  5\. Limit-average comparator

The limit-average of an infinite sequence $M$ is the point of convergence of
the average of prefixes of $M$. Let $\mathsf{Sum}(M[0,n-1])$ denote the sum of
the $n$-length prefix of sequence $M$. The limit-average infimum, denoted by
$\mathsf{LimInfAvg}(M)$, is defined as $\text{lim
inf}_{n\rightarrow\infty}\frac{1}{n}\cdot\mathsf{Sum}(M[0,n-1])$. Similarly,
the limit-average supremum, denoted by $\mathsf{LimSupAvg}(M)$, is defined as
$\text{lim sup}_{n\rightarrow\infty}\frac{1}{n}\cdot\mathsf{Sum}(M[0,n-1])$.
The limit-average of sequence $M$, denoted by $\mathsf{LimAvg}(M)$, is defined
only if the limit-average infimum and limit-average supremum coincide, and
then $\mathsf{LimAvg}(M)=\mathsf{LimInfAvg}(M)$ ($=\mathsf{LimSupAvg}(M)$).
Note that while limit-average infimum and supremum exist for all bounded
sequences, the limit-average may not. To work around this limitataion of
limit-average, most applications simply use limit-average infimum or limit-
average supremum of sequences [8, 11, 12, 22]. However, the usage of limit-
average infimum or limit-average supremum in liu of limit-average for purpose
of comparison can be misleading. For example, consider sequence $A$ s.t.
$\mathsf{LimSupAvg}(A)=2$ and $\mathsf{LimInfAvg}(A)=0$, and sequence $B$ s.t.
$\mathsf{LimAvg}(B)=1$. Clearly, limit-average of $A$ does not exist. So while
it is true that$\mathsf{LimInfAvg}(A)<\mathsf{LimInfAvg}(B)$, indicating that
at infinitely many indices the average of prefixes of $A$ is lower, this
renders an incomplete picture since at infinitley many indices, the average of
prefixes of $B$ is greater as $\mathsf{LimSupAvg}(A)=2$.

Such inaccuracies in limit-average comparison may occur when the limit-average
of at least one sequence does not exist. However, it is not easy to
distinguish sequences for which limit-average exists from those for which it
doesn’t.

We define prefix-average comparison as a relaxation of limit-average
comparison. Prefix-average comparison coincides with limit-average comparison
when limit-average exists for both sequences. Otherwise, it determines whether
eventually the average of prefixes of one sequence are greater than those of
the other. This comparison does not require the limit-average to exist to
return intuitive results. Further, we show that the prefix-average comparator
is $\omega$-context-free.

###  5.1. Limit-average language and comparison

Let $\Sigma=\\{0,1,\dots,\mu\\}$ be a finite alphabet with $\mu>0$. The limit-
average language $\mathcal{L}_{LA}$ contains the sequence (word)
$A\in\Sigma^{\omega}$ iff its limit-average exists. Suppose $\mathcal{L}_{LA}$
were $\omega$-regular, then $\mathcal{L}_{LA}=\bigcup_{i=0}^{n}U_{i}\cdot
V_{i}^{\omega}$, where $U_{i},V_{i}\subseteq\Sigma^{*}$ are regular languages
over finite words. The limit-average of sequences is determined by its
behavior in the limit, so limit-average of sequences in $V_{i}^{\omega}$
exists. Additionally, the average of all (finite) words in $V_{i}$ must be the
same. If this were not the case, then two words in $V_{i}$ with unequal
averages $l_{1}$ and $l_{2}$, can generate a word $w\in V_{i}^{\omega}$ s.t
the average of its prefixes oscillates between $l_{1}$ and $l_{2}$. This
cannot occur, since limit-average of $w$ exists. Let the average of sequences
in $V_{i}$ be $a_{i}$, then limit-average of sequences in $V_{i}^{\omega}$ and
$U_{i}\cdot V_{i}^{\omega}$ is also $a_{i}$. This is contradictory since there
are sequences with limit-average different from the $a_{i}$ (see appendix).
Similarly, since every $\omega$-CFL is represented by
$\bigcup_{i=1}^{n}U_{i}\cdot V_{i}^{\omega}$ for CFLs $U_{i},V_{i}$ over
finite words [14], a similar argument proves that $\mathcal{L}_{LA}$ is not
$\omega$-context-free.

######  Theorem 24.

$\mathcal{L}_{LA}$ is neither an $\omega$-regular nor an $\omega$-context-free
language.

######  Proof 5.1.

We first prove that $\mathcal{L}_{LA}$ is not $\omega$-regular.

Let us assume that the language $\mathcal{L}_{LA}$ is $\omega$-regular. Then
there exists a finite number $n$ s.t.
$\mathcal{L}_{LA}=\bigcup_{i=0}^{n}U_{i}\cdot V_{i}^{\omega}$, where $U_{i}$
and $V_{i}\in\Sigma^{*}$ are regular languages over finite words.

For all $i\in\\{0,1,\dots n\\}$, the limit-average of any word in $U_{i}\cdot
V_{i}^{\omega}$ is given by the suffix of the word in $V_{i}^{\omega}$. Since
$U_{i}\cdot V_{i}^{\omega}\subseteq\mathcal{L}_{LA}$, limit-average exists for
all words in $U_{i}\cdot V_{i}^{\omega}$. Therefore, limit-average of all
words in $V_{i}^{\omega}$ must exist. From Lemma 32, we conclude that the
average of all word in $V_{i}$ must be the same. Furthermore, from Lemma 33,
we know that the limit-average of all words in $V_{i}^{\omega}$ must be the
same, say $\mathsf{LimAvg}(w)=a_{i}$ for all $w\in V_{i}^{\omega}$.

Then the limit-average of all words in $\mathcal{L}_{LA}$ is one of
$a_{0},a_{1}\dots a_{n}$. Let $a=\frac{p}{q}$ s.t $p<q$, snd $a\neq a_{i}$ for
$i\in\\{0,1,\dots,\mu\\}$. Consider the word $w=(1^{p}0^{q-p})^{\omega}$. It
is easy to see the $\mathsf{LimAvg}(w)=a$. However, this word is not present
in $\mathcal{L}_{LA}$ since the limit-average of all words in
$\mathcal{L}_{LA}$ is equal to $a_{0}$ or $a_{1}$ …or $a_{n}$.

Therefore, our assumption that $\mathcal{L}_{LA}$ is an $\omega$-regular
language has been contradicted.

Next we prove that $\mathcal{L}_{LA}$ is not an $\omega$-CFL.

Every $\omega$-context-free language can be written in the form of
$\bigcup_{i=0}^{n}U_{i}\cdot V_{i}^{\omega}$ where $U_{i}$ and $V_{i}$ are
context-free languages over finite words. The rest of this proof is similar to
the proof for non-$\omega$-regularity of $\mathcal{L}_{LA}$.

In the next section, we will define prefix-average comparison as a relaxation
of limit-average comparison. To show how prefix-average comparison relates to
limit-average comparison, we will require the following two lemmas:
Quantifiers $\exists^{\infty}i$ and $\exists^{f}i$ denote the existence of
infinitely many and only finitely many indices $i$, respectively.

######  Lemma 25.

Let $A$ and $B$ be sequences s.t. their limit average exists. If
$\exists^{\infty}i,\mathsf{Sum}(A[0,i-1])\geq\mathsf{Sum}(B[0,i-1])$ then
$\mathsf{LimAvg}(A)\geq\mathsf{LimAvg}(B)$.

######  Proof 5.2.

Let the limit average of sequence $A$, $B$ be $a$, $b$ respectively. Since the
limit average of $A$ and $B$ exists, for every $\epsilon>0$, there exists
$N_{\epsilon}$ s.t. for all $n>N_{\epsilon}$ ,
$|\mathsf{Avg}(A[0,n-1])-a|<\epsilon$ and
$|\mathsf{Avg}(B[0,n-1])-b|<\epsilon$.

Let $a-b=k>0$.

Take $\epsilon=\frac{k}{4}$. Then for all $n>N_{\frac{k}{4}}$, since
$|\mathsf{Avg}(A[0,n-1])-a|<\epsilon$, $|\mathsf{Avg}(B[0,n-1])-b|<\epsilon$
and that $a-b=k>0$,
$\mathsf{Avg}(A[0,n-1])-\mathsf{Avg}(B[0,n-1])>\frac{k}{2}\implies\frac{\mathsf{Sum}(A[0,n-1])}{n}-\frac{\mathsf{Sum}(B[0,n-1])}{n}>\frac{k}{2}\implies\mathsf{Sum}(A[0,n-1])-\mathsf{Sum}(B[0,n-1])>0$.

Specifically,
$\exists^{\infty}i,\mathsf{Sum}(A[0,i-1])>\mathsf{Sum}(B[0,i-1])$.
Furthermore, since there is no index greater than $N_{\frac{k}{4}}$ where
$\mathsf{Sum}(A[0,n-1])\leq\mathsf{Sum}(B[0,n-1])$,
$\exists^{f}i,\mathsf{Sum}(B[0,i-1])\geq\mathsf{Sum}(A[0,i-1])$.

######  Lemma 26.

Let $A$, $B$ be sequences s.t their limit-average exists. If
$\mathsf{LimAvg}(A)>\mathsf{LimAvg}(B)$ then
$\exists^{f}i,\mathsf{Sum}(B[0,i-1])\geq\mathsf{Sum}(A[0,i-1])$ and
$\exists^{\infty}i,\mathsf{Sum}(A[0,i-1])>\mathsf{Sum}(B[0,i-1])$.

######  Proof 5.3.

Let the limit-average of sequence $A$, $B$ be $L_{a}$, $L_{b}$ respectively.
Since, the limit average of both $A$ and $B$ exists, for every $\epsilon>0$,
there exists $N_{\epsilon}$ s.t. for all $n>N_{\epsilon}$ ,
$|\mathsf{Avg}(A[1,n])-L_{a}|<\epsilon$ and
$|\mathsf{Avg}(B[1,n])-L_{b}|<\epsilon$.

Suppose it were possible that $\mathsf{LimAvg}(A)<\mathsf{LimAvg}(B)$. Suppose
$L_{b}-L_{a}=k>0$. Let $\epsilon=\frac{k}{4}$. By arguing as in Lemma 25, it
must be the case that for all $n>N_{\frac{k}{4}}$,
${\mathsf{Sum}(B[1,n])}-{\mathsf{Sum}(A[1,n])}>0$. But this is not possible,
since we are given that
$\exists^{\infty}i,\mathsf{Sum}(A[0,i-1])>\mathsf{Sum}(B[0,i-1])$ (or
$\exists^{\infty}i,\mathsf{Sum}(A[0,i-1]\geq\mathsf{Sum}(B[0,i-1]))$). Hence
$\mathsf{LimAvg}(A)\geq\mathsf{LimAvg}(B)$.

###  5.2. Prefix-average comparison and comparator

The previous section relates limit-average comparison with the sums of equal
length prefixes of the sequences (Lemma 25-26). The comparison criteria is
based on the number of times sum of prefix of one sequence is greater than the
other, which does not rely on the existence of limit-average. Unfortunately,
this criteria cannot be used for limit-average comparison since it is
incomplete (Lemma 26). Specifically, for sequences $A$ and $B$ with equal
limit-average it is possible that
$\exists^{\infty}i,\mathsf{Sum}(A[0,n-1])>\mathsf{Sum}(B[0,n-1])$ and
$\exists^{\infty}i,\mathsf{Sum}(B[0,n-1])>\mathsf{Sum}(A[0,n-1])$. Instead, we
use this criteria to define prefix-average comparison. In this section, we
define prefix-average comparison and explain how it relaxes limit-average
comparison. Lastly, we construct the prefix-average comparator, and prove that
it is not $\omega$-regular but is $\omega$-context-free.

[Prefix-average comparison for relation $\geq$] Let $A$ and $B$ be number
sequences. We say $\mathsf{PrefixAvg}(A)\geq\mathsf{PrefixAvg}(B)$ if
$\exists^{f}i,\mathsf{Sum}(B[0,i-1])\geq\mathsf{Sum}(A[0,i-1])$ and
$\exists^{\infty}i,\mathsf{Sum}(A[0,i-1])>\mathsf{Sum}(B[0,i-1])$. Note that,
by definition prefix average comparison is defined on inequality relation
$\geq$ or $\leq$, and not for the other inequality or equality relations.
Intuitively, prefix-average comparison states that
$\mathsf{PrefixAvg}(A)\geq\mathsf{PrefixAvg}(B)$ if eventually the sum of
prefixes of $A$ are always greater than those of $B$. We use $\geq$ since the
average of prefixes may be equal when the difference between the sum is small.
It coincides with limit-average comparison when the limit-average exists for
both sequences. Definition5.2 and Lemma 25-26 relate limit-average comparison
and prefix-average comparison:

######  Corollary 27.

When limit-average of $A$ and $B$ exists, then

  * •

$\mathsf{PrefixAvg}(A)\geq\mathsf{PrefixAvg}(B)\implies\mathsf{LimAvg}(A)\geq\mathsf{LimAvg}(B)$.

  * •

$\mathsf{LimAvg}(A)>\mathsf{LimAvg}(B)\implies\mathsf{PrefixAvg}(A)\geq\mathsf{PrefixAvg}(B)$.

######  Proof 5.4.

The first item falls directly from definitions.

For the second, let $\mathsf{LimInfAvg}(A)$ and $\mathsf{LimSupAvg}(B)$ be $a$
and $b$ respectively. For all $\epsilon>0$ there exists an $N_{\epsilon}$ s.t
for all $n>N_{\epsilon}$, $\frac{\mathsf{Sum}(A[1,n])}{n}>a-\epsilon$, and
$\frac{\mathsf{Sum}(B[1,n])}{n}<b+\epsilon$. Let $a-b=k>0$. Take
$\epsilon=\frac{k}{4}$. Replicate the argument from Lemma 25 to show that
there can exist only finitely many indexes $i$ where
${\mathsf{Sum}(B[0,i-1])}\geq{\mathsf{Sum}(A[0,i-1])}$. Similarly, show there
exists infinitely many prefixes where
$\mathsf{Sum}(A[0,i-1])>\mathsf{Sum}(B[0,i-1])$

Therefore, limit-average comparison and prefix-average comparison return the
same result on sequences for which limit-average exists. In addition, prefix-
average returns intuitive results when even when limit-average may not exist.
For example, suppose limit-average of $A$ and $B$ do not exist, but
$\mathsf{LimInfAvg}(A)>\mathsf{LimSupAvg}(B)$, then
$\mathsf{PrefixAvg}(A)\geq\mathsf{PrefixAvg}(B)$. Therefore, prefix-average
comparison relaxes limit-average comparison.

The rest of this section describes prefix-average comparator for relation
$\geq$, denoted by $\mathcal{A}_{\mathsf{PA}}^{\geq}$, an automaton that
accepts the pair $(A,B)$ of sequences iff
$\mathsf{PrefixAvg}(A)\geq\mathsf{PrefixAvg}(B)$.

######  Lemma 28.

(Pumping Lemma for $\omega$-regular language [2]) Let $L$ be an
$\omega$-regular language. There exists $p\in\mathbb{N}$ such that, for each
$w=u_{1}w_{1}u_{2}w_{2}\dots\in L$ such that $|w_{i}|\geq p$ for all $i$,
there are sequences of finite words $(x_{i})_{i\in\mathbb{N}}$,
$(y_{i})_{i\in\mathbb{N}}$, $(z_{i})_{i\in\mathbb{N}}$ s.t., for all $i$,
$w_{i}=x_{i}y_{i}z_{i}$, $|x_{i}y_{i}|\leq p$ and $|y_{i}|>0$ and for every
sequence of pumping factors $(j_{i})_{i\in\mathbb{N}}\in\mathbb{N}$, the
pumped word $u_{1}x_{1}y_{1}^{j_{1}}z_{1}u_{2}x_{2}y_{2}^{j_{2}}z_{2}\dots\in
L$.

######  Theorem 29.

The prefix-average comparator for $\geq$ is not $\omega$-regular.

######  Proof 5.5 (Proof Sketch).

We use Lemma 28 to prove that $\mathcal{A}_{\mathsf{PA}}^{\geq}$ is not
$\omega$-regular. Suppose $\mathcal{A}_{\mathsf{PA}}^{\geq}$ were
$\omega$-regular. For $p>0\in\mathbb{N}$, let
$w=(A,B)=((0,1)^{p}(1,0)^{2p})^{\omega}$. The segment $(0,1)^{*}$ can be
pumped s.t the resulting word is no longer in
$\mathcal{A}_{\mathsf{PA}}^{\geq}$.

Concretely, $A=(0^{p}1^{2p})^{\omega}$, $B=(1^{p}0^{2p})^{\omega}$,
$\mathsf{LimAvg}(A)=\frac{2}{3}$, $\mathsf{LimAvg}(B)=\frac{1}{3}$. So,
$w=(A,B)\in\mathcal{A}_{\mathsf{PA}}^{\geq}$. Select as factor $w_{i}$ (from
Lemma 28) the sequence $(0,1)^{p}$. Pump each $y_{i}$ enough times so that the
resulting word is
$\hat{w}=(\hat{A},\hat{B})=((0,1)^{m_{i}}(1,0)^{2p})^{\omega}$ where
$m_{i}>4p$. It is easy to show that
$\hat{w}=(\hat{A},\hat{B})\notin\mathcal{A}_{\mathsf{PA}}^{\geq}$.

We discuss key ideas and sketch the construction of the prefix average
comparator. The term prefix-sum difference at $i$ indicates
$\mathsf{Sum}(A[0,i-1])-\mathsf{Sum}(B[0,i-1])$, i.e. the difference between
sum of $i$-length prefix of $A$ and $B$.

#### Key ideas

For sequences $A$ and $B$ to satisfy
$\mathsf{PrefixAvg}(A)\geq\mathsf{PrefixAvg}(B)$,
$\exists^{f}i,\mathsf{Sum}(B[0,i-1])\geq\mathsf{Sum}(A[0,i-1])$ and
$\exists^{\infty}i,\mathsf{Sum}(A[0,i-1])>\mathsf{Sum}(B[0,i-1])$. This occurs
iff there exists an index $N$ s.t. for all indices $i>N$,
$\mathsf{Sum}(A[0,i-1])-\mathsf{Sum}(B[0,i-1])>0$. While reading a word, the
prefix-sum difference is maintained by states and the stack of $\omega$-PDA:
states maintain whether it is negative or positive, while number of tokens in
the stack equals its absolute value. The automaton non-deterministically
guesses the aforementioned index $N$, beyond which the automaton ensure that
prefix-sum difference remains positive.

#### Construction sketch

The push-down comparator $\mathcal{A}_{\mathsf{PA}}^{\geq}$ consists of three
states: (i) State $s_{P}$ and (ii) State $s_{N}$ that indicate that the
prefix-sum difference is greater than zero and or not respectively, (iii)
accepting state $s_{F}$. An execution of $(A,B)$ begins in state $s_{N}$ with
an empty stack. On reading letter $(a,b)$, the stack pops or pushes $|(a-b)|$
tokens from the stack depending on the current state of the execution. From
state $s_{P}$, the stack pushes tokens if $(a-b)>0,$ and pops otherwise. The
opposite occurs in state $s_{N}$. State transition between $s_{N}$ and $s_{P}$
occurs only if the stack action is to pop but the stack consists of $k<|a-b|$
tokens. In this case, stack is emptied, state transition is performed and
$|a-b|-k$ tokens are pushed into the stack. For an execution of $(A,B)$ to be
an accepting run, the automaton non-deterministically transitions into state
$s_{F}$. State $s_{F}$ acts similar to state $s_{P}$ except that execution is
terminated if there aren’t enough tokens to pop out of the stack.
$\mathcal{A}_{\mathsf{PA}}^{\geq}$ accepts by accepting state.

To see why the construction is correct, it is sufficient to prove that at each
index $i$, the number of tokens in the stack is equal to
$|\mathsf{Sum}(A[0,i-1])-\mathsf{Sum}(B[0,i-1])|$. Furthermore, in state
$s_{N}$, $\mathsf{Sum}(A[0,i-1])-\mathsf{Sum}(B[0,i-1])\leq 0$, and in state
$s_{P}$ and $s_{F}$, $\mathsf{Sum}(A[0,i-1])-\mathsf{Sum}(B[0,i-1])>0$. Next,
the index at which the automaton transitions to the accepting state $s_{F}$
coincides with index $N$. The execution is accepted if it has an infinite
execution in state $s_{F}$, which allows transitions only if
$\mathsf{Sum}(A[0,i-1])-\mathsf{Sum}(B[0,i-1])>0$.

#### Construction

We provide a sketch of the construction of the Büchi push-down autoamaton
$\mathcal{A}_{\mathsf{PA}}^{\geq}$, and then prove that it corresponds to the
prefix average comparator.

Let $\mu$ be the bound on sequences. Then $\Sigma=\\{0,1,\dots,n\\}$ is the
alphabet of sequences. Let
$\mathcal{A}_{\mathsf{PA}}^{\geq}=(\mathit{S},\Sigma\times\Sigma,\Gamma,\delta,s_{0},Z_{0})$
where:

  * •

$\mathit{S}=\\{s_{N},s_{P},s_{F}\\}$ is the set of states of the automaton.

  * •

$\Sigma\times\Sigma$ is the alphabet of the language.

  * •

$\Gamma=\\{Z_{0},\alpha\\}$ is the push down alphabet.

  * •

$s_{0}=s_{N}$ is the start state of the push down automata.

  * •

$Z_{0}$ is the start symbol of the stack.

  * •

$s_{F}$ is the accepting state of the automaton. Automaton
$\mathcal{A}_{\mathsf{PA}}^{\geq}$ accepts words by final state.

  * •

Here we give a sketch of the behavior of the transition function $\delta$.

    * –

When $\mathcal{A}_{\mathsf{PA}}^{\geq}$ is in configuration $(s_{P},\tau)$ for
$\tau\in\Gamma$, push $a$ number of $\alpha$-s into the stack.

Next, pop $b$ number of $\alpha$-s. If after popping $k$ $\alpha$-s where
$k<b$, the PDA’s configuration becomes $(s_{P},Z_{0})$, then first move to
state $(s_{N},Z_{0})$ and then resume with pushing $b-k$ $\alpha$-s into the
stack.

    * –

When $\mathcal{A}_{\mathsf{PA}}^{\geq}$ is in configuration $(s_{N},\tau)$ for
$\tau\in\Gamma$, push $b$ number of $\alpha$-s into the stack

Next, pop $a$ number of $\alpha$-s. If after popping $k$ $\alpha$-s where
$k<a$, the PDA’s configuration becomes $(s_{N},Z_{0})$, then first move to
state $(s_{P},Z_{0})$ and then resume with pushing $a-k$ $\alpha$-s into the
stack.

    * –

When $\mathcal{A}_{\mathsf{PA}}^{\geq}$ is in configuration $(s_{P},\tau)$ for
$\tau\neq Z_{0}$, first move to configuration $(s_{F},\tau)$ and then push $a$
number of $\alpha$-s and pop $b$ number of $\alpha$-s. Note that there are no
provisions for popping $\alpha$ if the stack hits $Z_{0}$ along this
transition.

    * –

When $\mathcal{A}_{\mathsf{PA}}^{\geq}$ is in configuration $(s_{F},\tau)$ for
$\tau\neq Z_{0}$, push $a$ $\alpha$-s then pop $b$ $\alpha$-s.

Note that there are no provisions for popping $\alpha$ if the stack hits
$Z_{0}$ along this transition.

######  Lemma 30.

Push down automaton $\mathcal{A}_{\mathsf{PA}}^{\geq}$ accepts a pair of
sequences $(A,B)$ iff $\mathsf{PrefixAvg}(A)\geq\mathsf{PrefixAvg}(B)$.

######  Proof 5.6 (Proof sketch).

To prove this statement, it is sufficient to demonstrate that
$\mathcal{A}_{\mathsf{PA}}^{\geq}$ accepts a pair of sequences $(A,B)$ iff
there are only finitely many indexes where
$\mathsf{Sum}(B[1,i])>\mathsf{Sum}(A[1,i])$. On
$\mathcal{A}_{\mathsf{PA}}^{\geq}$ this corresponds to the condition that
there being only finitely many times when the PDA is in state $N$ during the
run of $(A,B)$. This is ensured by the push down automaton since the word can
be accepted only in state $F$ and there is no outgoing edge from $F$.
Therefore, every word that is accepted by $\mathcal{A}_{\mathsf{PA}}^{\geq}$
satisfies the condition
$\exists^{f}i,\mathsf{Sum}(B[0,i-1])\geq\mathsf{Sum}(A[0,i-1])$.

Conversely, for every word $(A,B)$ that satisfies
$\exists^{f}i,\mathsf{Sum}(B[0,i-1])\geq\mathsf{Sum}(A[0,i-1])$ there is a
point, call it index $k$, such that for all indexes $m>k$,
$\mathsf{Sum}(B[1,m])\ngeq\mathsf{Sum}(A[1,m])$. If a run of $(A,B)$ switches
to $F$ at this $m$, then it will be accepted by the push down automaton. Since
$\mathcal{A}_{\mathsf{PA}}^{\geq}$ allows for non-deterministic move to
$(F,\tau)$ from $(P,\tau)$, the run of $(A,B)$ will always be able to move to
$F$ after index $m$. Hence, every $(A,B)$ satisfying
$\exists^{f}i,\mathsf{Sum}(B[0,i-1])\geq\mathsf{Sum}(A[0,i-1])$ will be
accepted by $\mathcal{A}_{\mathsf{PA}}^{\geq}$.

######  Theorem 31.

The prefix-average comparator for relation $\geq$ is an $\omega$-CFL.

While $\omega$-CFL can be easily expressed, they do not possess closure
properties, and problems on $\omega$-CFL are easily undecidable. Hence, the
application of $\omega$-context-free comparator will require further
investigation.

##  6\. Concluding remarks

In this paper, we identified a novel mode for comparison in quantitative
systems: the online comparison of aggregate values of sequences of
quantitative weights. This notion is embodied by comparators automata that
read two infinite sequences of weights synchronously and relate their
aggregate values. We showed that all $\omega$-regular aggregate functions have
$\omega$-regular comparators. However, the converse direction is still open:
Are functions with $\omega$-regular comparators also $\omega$-regular? We
showed that $\omega$-regular comparators not only yield generic algorithms for
problems including quantitative inclusion and winning strategies in
incomplete-information quantitative games, they also result in algorithmic
advances. We establish that the discounted-sum inclusion problem is
$\mathsf{PSAPCE}$-complete for integer discount-factor, hence closing a
complexity gap. We showed that discounted-sum aggregate function and their
comparators are $\omega$-regular iff the discount-factor $d>1$ is an integer.
We showed that prefix-average comparator are $\omega$-context-free.

We believe comparators, especially $\omega$-regular comparators, can be of
significant utility in verification and synthesis of quantitative systems, as
demonstrated by the existence of finite-representation of counterexamples of
the quantitative inclusion problem. Another potential application is computing
equilibria in quantitative games. Applications of the prefix-average
comparator, in general $\omega$-context-free comparators, is open to further
investigation. Another direction to pursue is to study aggregate functions in
more detail, and attempt to solve the conjecture relating $\omega$-regular
aggregate functions and $\omega$-regular comparators.

## Acknowledgment

We thank the anonymous reviewers for their comments. We thank K. Chatterjee,
L. Doyen, T. Henzinger, G. A. Perez and J. F. Raskin for corrections to
earlier drafts, and their contributions to this paper. We thank P. Ganty and
R. Majumdar for preliminary discussions on the limit-average comparator. This
work was partially supported by NSF Grant No. 1704883, “Formal Analysis and
Synthesis of Multiagent Systems with Incentives”.

## References

  * [1] S. Almagor, U. Boker, and O. Kupferman.  Whatś decidable about weighted automata?  In Proc. of ATVA, pages 482–491. Springer, 2011.
  * [2] R. Alur, A. Degorre, O. Maler, and G. Weiss.  On omega-languages defined by mean-payoff conditions.  In Proc. of FOSSACS, pages 333–347. Springer, 2009.
  * [3] G. Andersen and V. Conitzer.  Fast equilibrium computation for infinitely repeated games.  In Proc. of AAAI, pages 53–59, 2013.
  * [4] D. Andersson.  An improved algorithm for discounted payoff games.  In ESSLLI Student Session, pages 91–98, 2006.
  * [5] C. Baier, J.-P. Katoen, et al.  Principles of model checking.  MIT press Cambridge, 2008.
  * [6] S. Bansal, S. Chaudhuri, and M. Y. Vardi.  Comparator automata in quantitative verification.  In Proc. of FoSSaCS, 2018.
  * [7] U. Boker and T. A. Henzinger.  Exact and approximate determinization of discounted-sum automata.  LMCS, 10(1), 2014.
  * [8] L. Brim, J. Chaloupka, L. Doyen, R. Gentilini, and J.-F. Raskin.  Faster algorithms for mean-payoff games.  Formal methods in system design, 38(2):97–118, 2011.
  * [9] K. Chatterjee and L. Doyen.  Energy parity games.  In In Proc. of ICALP, pages 599–610. Springer, 2010.
  * [10] K. Chatterjee, L. Doyen, and T. A. Henzinger.  Expressiveness and closure properties for quantitative languages.  In Proc. of LICS, pages 199–208. IEEE, 2009.
  * [11] K. Chatterjee, L. Doyen, and T. A. Henzinger.  Quantitative languages.  Transactions on Computational Logic, 11(4):23, 2010.
  * [12] K. Chatterjee, T. A. Henzinger, and M. Jurdzinski.  Mean-payoff parity games.  In Proc. of LICS, pages 178–187. IEEE, 2005.
  * [13] S. Chaudhuri, S. Sankaranarayanan, and M. Y. Vardi.  Regular real analysis.  In Proc. of LICS, pages 509–518, 2013.
  * [14] R. S. Cohen and A. Y. Gold.  Theory of $\omega$-languages: Characterizations of $\omega$-context-free languages.  Journal of Computer and System Sciences, 15(2):169–184, 1977.
  * [15] L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga.  Model checking discounted temporal properties.  In Proc. of TACAS, pages 77–92. Springer, 2004.
  * [16] L. De Alfaro, M. Faella, and M. Stoelinga.  Linear and branching metrics for quantitative transition systems.  In In Proc. of ICALP, pages 97–109. Springer, 2004.
  * [17] A. Degorre, L. Doyen, R. Gentilini, J.-F. Raskin, and S. Toruńczyk.  Energy and mean-payoff games with imperfect information.  In International Workshop on Computer Science Logic, pages 260–274. Springer, 2010.
  * [18] M. Droste, W. Kuich, and H. Vogler.  Handbook of weighted automata.  Springer, 2009.
  * [19] R. M. Karp.  A characterization of the minimum cycle mean in a digraph.  Discrete mathematics, 23(3):309–311, 1978.
  * [20] M. Mohri.  Weighted automata algorithms.  In Handbook of weighted automata, pages 213–254. Springer, 2009\.
  * [21] W. Thomas, T. Wilke, et al.  Automata, logics, and infinite games: A guide to current research, volume 2500.  Springer Science & Business Media, 2002.
  * [22] U. Zwick and M. Paterson.  The complexity of mean payoff games on graphs.  Theoretical Computer Science, 158(1):343–359, 1996.

##  Appendix A Limsup comparator construction

Formal construction of the limsup comparator is given here. Suppose all
sequences are natural number sequences, bounded by $\mu$. The limsup
comparator is the Büchi automaton
$\mathcal{A}_{\succ\mathit{LS}}=(\mathit{S},\Sigma,\delta,{\mathit{Init}},\mathcal{F})$
where

  * •

$\mathit{S}=\\{s\\}\cup\\{s_{0},s_{1}\dots,s_{\mu}\\}\cup\\{f_{0},f_{1}\dots,f_{\mu}\\}$

  * •

$\Sigma=\\{(a,b):0\leq a,b\leq\mu\\}$ where $a$ and $b$ are integers.

  * •

$\delta\subseteq\mathit{S}\times\Sigma\times\mathit{S}$ is defined as follows:

    1. (1)

Transitions from start state $s$: $(s,(a,b),p)$ for all $(a,b)\in\Sigma$, and
for all $p\in\\{s\\}\cup\\{f_{0},f_{1},\dots,f_{\mu}\\}$.

    2. (2)

Transitions between $f_{k}$ and $s_{k}$ for each $k$:

      1. i

$(f_{k},\alpha,f_{k})$ for $\alpha\in\\{k\\}\times\\{0,1,\dots k\\}$.

      2. ii

$(f_{k},\alpha,s_{k})$ for $\alpha\in\\{0,1,\dots k-1\\}\times\\{0,1,\dots
k\\}$.

      3. iii

$(s_{k},\alpha,s_{k})$ for $\alpha\in\\{0,1,\dots k-1\\}\times\\{0,1,\dots
k\\}$.

      4. iv

$(s_{k},\alpha,f_{k})$ for $\alpha\in\\{k\\}\times\\{0,1,\dots k\\}$.

  * •

${\mathit{Init}}=\\{s\\}$

  * •

$\mathcal{F}=\\{f_{0},f_{1}\dots,f_{\mu}\\}$

##  Appendix B Limit Average Comparator

######  Lemma 32.

Let $\Sigma=\\{0,1\dots\mu\\}$. Let $L\in\Sigma^{*}$ s.t. the limit-average of
all words in the language $L^{\omega}$ exists. Then average of all words in
$L$ is the same.

######  Proof B.1.

Suppose it is possible that two finite words $v_{1}$, $v_{2}\in L$ have
different average. Let their length be $l_{1}$ and $l_{2}$ respectively with
the average $a_{1}$ and $a_{2}$ respectively where $a_{1}\neq a_{2}$. We will
show the presence of a word $w\in L^{\omega}$ s.t. the limit-average of $w$
does not exist.

Let $w_{1}=v_{1}$. Then $\mathsf{Avg}(w_{1})=a_{1}$. Next, let $j_{2}$ be
large enough to construct $w_{2}=w_{i}v_{2}^{j_{2}}$ such that
$\mathsf{Avg}(w_{2})\approx a_{2}$. Next, let $j_{3}$ be large enough to
construct $w_{3}=w_{2}v_{1}^{j_{3}}$ such that $\mathsf{Avg}(w_{3})\approx
a_{1}$. Continue constructing $w_{4},w_{5}\dots$ in a similar fashoin s.t.
their average change between $a_{2},a_{1}\dots$ respectively.

Let these $w=w_{n}$ as $n\rightarrow\infty$. Then $w\in L^{\omega}$, and since
the average of its finite-length prefixes keeps changing between $a_{1}$ and
$a_{2}$, limit-average of $w$ does not exist.

This contradicts the premise that the limit-average of all words in
$L^{\omega}$ exists. Therefore, our assumption that words $v_{1}$ and $v_{2}$
can have different average has been contradicted.

######  Lemma 33.

Let $\Sigma=\\{0,1,\dots\mu\\}$. Let $L\subseteq\Sigma^{*}$ s.t. the average
of all words in $\Sigma$ is the same, say $a$. Let $w\in L^{\omega}$ s.t.
limit-average of $w$ exists. Then $\mathsf{LimAvg}(w)=a$

######  Proof B.2.

Let $w=w_{1}w_{2}w_{3}\dots$. There exists infinitely many prefixes of $w$,
prefix $w[i]=w_{1}w_{2}\dots w_{i}$ s.t. $\mathsf{Avg}(w[i])=a$. Since we are
given that the limit-average of $w$ exists, it must be equal to $a$.