First note that the transition relation is deterministic and complete.
Therefore, every word has a unique run in $\mathsf{bad}(\mu,d,\leq)$. Let
$\mathsf{last}$ be the last state in the run of finite, bounded weight-
sequence $W$ in the DFA. We use induction on the length of $W$ to prove the
following:

  * •

$\mathsf{last}\in\\{\lfloor-\mathsf{T}\rfloor+1,\dots,\lfloor\mathsf{T}\rfloor\\}$
iff $\mathsf{gap}(W,d)=\mathsf{last}$

  * •

$\mathsf{last}=\mathsf{bad}$ iff $\mathsf{gap}(W,d)>\lfloor\mathsf{T}\rfloor$

  * •

$\mathsf{last}=\mathsf{veryGood}$ iff
$\mathsf{gap}(W,d)\leq\lfloor-\mathsf{T}\rfloor$

Let $W=\varepsilon$ be a word of length 0. By definition of recoverable gap,
$\mathsf{gap}(w,d)=0$. Also, its run in the DFA $\mathsf{bad}(\mu,d,\leq)$ is
the single-state sequence 0, where 0 is the initial state of the
DFA.Therefore, the hypothesis is true for the base case.

Let the hypothesis be true for all words of length $n$. We prove that the
hypothesis can be extended to words of length $n+1$.

Let $W=V\cdot a$ be a word of length $n+1$, where $V$ is a word of length $n$
and $\mathsf{last}_{V}$ be its last state . By induction hypothesis,

  * •

$\mathsf{last}_{V}\in\\{\lfloor-\mathsf{T}\rfloor+1,\dots,\lfloor\mathsf{T}\rfloor\\}$
iff $\mathsf{gap}(V,d)=\mathsf{last}_{V}$

  * •

$\mathsf{last}_{V}=\mathsf{bad}$ iff
$\mathsf{gap}(V,d)>\lfloor\mathsf{T}\rfloor$

  * •

$\mathsf{last}_{V}=\mathsf{veryGood}$ iff
$\mathsf{gap}(V,d)\leq\lfloor-\mathsf{T}\rfloor$

Since, the DFA is deterministic, the last state of $W$ is
$\mathsf{last}=\delta(\mathsf{last}_{V},a)$.

If $\mathsf{gap}(W,d)>\lfloor\mathsf{T}\rfloor$, we show that
$\mathsf{last}=\mathsf{bad}$.

  1. 1.

If $\mathsf{last}_{V}=\mathsf{bad}$, then by construction $\mathsf{bad}$ is a
sink state, in which case $\mathsf{last}=\mathsf{bad}$.

  2. 2.

If
$\mathsf{last}_{V}=s\in\\{\lfloor-\mathsf{T}\rfloor+1,\dots,\lfloor\mathsf{T}\rfloor\\}$.
By I.H, we know that $s=\mathsf{gap}(V,d)$, therefore by definition of
recoverable gap, $\mathsf{gap}(W,d)=d\cdot s+a>\lfloor\mathsf{T}\rfloor$.
Therefore, by the transition function rules, $\mathsf{last}=\mathsf{bad}$.

  3. 3.

If $\mathsf{last}_{V}=\mathsf{veryGood}$. Since $\mathsf{veryGood}$ is a sink
state, none of its transitions will go to state $\mathsf{bad}$.

Conversely, let $\mathsf{last}=\mathsf{bad}$. We show that
$\mathsf{gap}(W,d)>\lfloor\mathsf{T}\rfloor$.

  1. 1.

If $\mathsf{last}_{V}=\mathsf{bad}$ , then by I.H.
$\mathsf{gap}(V,d)>\lfloor\mathsf{T}\rfloor$. Since the discount-factor is an
integer, $V$ is a bad prefix (Corollary 6.3). Since extensions of bad-prefixes
are also bad-prefixes, we get that W is also a bad-prefix. By the same
corollary, we get $\mathsf{gap}(W,d)>\lfloor\mathsf{T}\rfloor$.

  2. 2.

If
$\mathsf{last}_{V}=s\in\\{\lfloor-\mathsf{T}\rfloor+1,\dots,\lfloor\mathsf{T}\rfloor\\}$.
A transition from s goes to $\mathsf{bad}$ only if $d\cdot
s+a>\lfloor\mathsf{T}\rfloor$. By I.H $s=\mathsf{gap}(V,d)$, therefore $d\cdot
s+a=\mathsf{gap}(W,d)>\lfloor\mathsf{T}\rfloor$.

  3. 3.

If $\mathsf{last}_{v}=\mathsf{veryGood}$. Not relevant since there are no
transition from $\mathsf{veryGood}$ to $\mathsf{bad}$.

The proof for $\mathsf{last}=\mathsf{veryGood}$ iff
$\mathsf{gap}(W,d)\leq\lfloor-\mathsf{T}\rfloor$ is similar. It uses the fact
that extensions of a very good prefix are also very good prefixes.

The final case is when
$\mathsf{last}\in\\{\lfloor-\mathsf{T}\rfloor+1,\dots,\lfloor\mathsf{T}\rfloor\\}$.
This is the simplest case since it simply follows the transition relation and
inductive definition of recoverable gap.

Sink $\mathsf{bad}$ is the only accepting state, a words visits $\mathsf{bad}$
iff its recoverable gap is strictly above $\lfloor\mathsf{T}\rfloor$, the DFA
accepts the language of bad-prefixes. ∎

Finally, the DS comparators are constructed as follows:

###### Theorem 6.5

Let $\mu$ be the upper bound, and $d>1$ be the integer discount-factor. DS
comparator for all inequalities and equality are either deterministic safety
or deterministic co-safety automata with $\mathcal{O}(\mu)$ states.

###### Proof 44

This proof should also be treated as an exercise that illustrates that DFA
$\mathsf{bad}(\mu,d,\leq)$ is the basis of all our constructions. In fact, the
analysis of bad-prefixes and very-good prefixes for the one case of the $\leq$
relation is sufficient.

For $>$: Syntactically, DFA $\mathsf{bad}(\mu,d,\leq)$ is also a deterministic
co-safety automaton. We claim that this deterministic co-safety automaton
accepts the DS comparison language for the relation $>$. This is true due to
the complementation duality of the definitions of safety and co-safety
languages. A sequence $A$ is in a co-safety language $L$ iff it has a finite
length prefix $B$ that is a bad prefix for the complement safety language
$\overline{L}$. The missing link here is that DS comparison languages for $>$
and DS comparison language for $\leq$ are complements of each other.

For $\leq$: Flipping accepting and non-accepting states of the deterministic
co-safety comparator for $>$ will do the trick to generate the deterministic
safety comparator for $\leq$ with the same number of states. Another way to
think of the construction of the coveted safety comparator is from DFA
$\mathsf{bad}(\mu,d,\leq)$ itself. First of all, observe that syntactically
the complement of DFA $\mathsf{bad}(\mu,d,\leq)$, denoted by
$\overline{\mathsf{bad}(\mu,d,\leq)}$ is also a deterministic safety automata
with a single non-accepting sink state. Second of all, semantically DFA
$\overline{\mathsf{bad}(\mu,d,\leq)}$ accepts all finite sequences that are
not bad-prefixes of the DS comparison language with relation $\leq$. Hence,
DFA $\overline{\mathsf{bad}(\mu,d,\leq)}$ is also the deterministic safety
automata for DS comparison language for relation $\leq$.

For $<$ and $\geq$: The co-safety and safety automata for $<$ and $\geq$ is
obtained by negating the alphabet on all transitions of the DS comparator
automata for $>$ and $\leq$, respectively. Alternately, once may construct
these comparators from first principles by reasoning over DFA
$\mathsf{bad}(\mu,d,\leq)$, as done in the previous two cases.

For $=$ and $\neq$: The default for construction of DS comparators $=$ is to
take the intersection of those for $\leq$ and $\geq$. However, that would
result in a safety comparator with $\mathcal{O}(\mu^{2})$. Similarly, default
for $\neq$ would also have $\mathcal{O}(\mu)$ states. Instead, we construct
the safety and co-safety comparator for $=$ and $\neq$ in $\mathcal{O}(\mu)$
states as well.

Observe that the bad-prefixes of the DS comparison language for $=$ with
either be bad-prefixes of the same for $\leq$ or the bad-prefixes of $\geq$.
Recall, that a bounded, finite-length weight sequence $W$ is a bad-prefix of
$\leq$ iff $\mathsf{gap}(W,d)>{\mathsf{T}}$ (Lemma 6.4). Analogously, one can
prove that $W$ is a bad-prefix of $\geq$ iff $\mathsf{gap}(W,d)<-\mathsf{T}$.
Therefore, if an infinite sequence $A$ has a finite prefix $B$ such that
either $\mathsf{gap}(B,d)>\mathsf{T}$ or $\mathsf{gap}(B,d)<-\mathsf{T}$, then
the $\neq(\mathit{DS}({A},{d})=0)\equiv\mathit{DS}({A},{d})\neq 0$, i.e., is
$A$ is present in the DS comparison language for $\neq$. Therefore, in DFA
$\mathsf{bad}(\mu,d,\leq)$, if both $\mathsf{bad}$ and $\mathsf{veryGood}$ are
accepting, the resulting deterministic Büchi automaton accepts the DS
comparison language for $\neq$. Now, this can be converted into a
deterministic co-safety automaton, by fusing both the accepting states into
one.

Finally, the safety automata for DS comparison language with $=$ simply flips
the accepting and non-accepting states of the co-safety automata for $\neq$. ∎

As a matter of fact, the most compact non-deterministic DS comparator
constructions with parameters $\mu$, $d$ and $R$ also contain
$\mathcal{O}(\mu)$ states [24]. In fact, we can go a step further and prove
that the deterministic Büchi automaton constructed in Thereom 6.5 are the
minimal forms, i.e., none of the languages represented by these deterministic
automata can be represented by other deterministic automata with fewer number
of states. It is worth noting that not all (non-deterministic) Büchi automata
have minimal forms. However, deterministic Büchi automata are known to have
minimal forms [54, 70].

###### Theorem 6.6

The deterministic Büchi automata constructed in Theorem 6.5 for each DS
comparator are their respective minimal deterministic Büchi automata.

###### Proof 45

Each of the DS comparator constructed in Theorem 6.5 is either a deterministic
safety or co-safety automata. Therefore, if these DBAs were not in minimal
form, then the underlying deterministic DFA corresponding to the appropriate
language of bad-prefixes or their complement would not be in minimal form
either.

For instance, if the DBA for DS comparator for $\leq$ or $>$ were not minimal,
then the DFA $\mathsf{bad}(\mu,d,\leq)$ would not be a minimal DFA either. We
claim that DFA $\mathsf{bad}(\mu,d,\leq)$ is a minimal DFA, and hence it must
be the case that the safety/co-safety automata for DS comparison language for
$\leq$ or $>$ are minimal DBA as well.

In order to prove that DFA $\mathsf{bad}(\mu,d,\leq)$ is minimal, we prove
that no two states are equivalent as per Myhill-Nerode equivalence relation
[74], and proving minimal form [59]. As per this relation, two states $s$ and
$t$ are said to be equivalent, denoted $s\sim t$, if (a). Either both $s$ and
$t$ are accepting states, or both are non-accepting states, and (b). For all
alphabet $a\in\Sigma$, if $s\xrightarrow{a}s^{\prime}$ and
$t\xrightarrow{a}t^{\prime}$ are transitions in the DFA, then $s^{\prime}\sim
t^{\prime}$ must hold. The core idea behind proving that no two states of
$\mathsf{bad}(\mu,d,\leq)$ are equivalent is to realize that the states of
$\mathsf{bad}(\mu,d,\leq)$ represent values of the gap value, and transitions
are governed by arithmetic on them. So, one can easily find an alphabet
$a\in\Sigma$ such that outgoing transitions do not go to equivalent states.

The formal proof can be completed by induction on the minimum distance of
states from the single accepting sink state. The inductive hypothesis is that
no two states that are at a minimum distance of $k\geq 0$ from the accepting
sink state are equivalent. In the base case, k = 0. There is only one such
state - the accepting sink state itself- therefore the I.H. holds vacuously.
For larger values of $k$, the intuition described above will demonstrate the
veracity of the I.H.

Similar arguments will prove that that the DBAs for all other relations are
also minimal. ∎

Hence, in this section, not only did we construct safety/co-safety forms for
DS comparators, our constructions are also the minimal deterministic
representations. These are the most efficient deterministic constructions
possible for DS comparators.

#####  6.4.3 QuIPFly: DS inclusion with integer discount factor

Finally, we solve DS inclusion with integer discount factors with using the
safety and co-safety comparators presented in the previous Section 6.4.2. Here
we will apply the generic algorithm for quantitative inclusion with regular
safety/co-safety comparators (Section 6.3.2) to the case of discounted-sum
with integer discount factors. As seen before in Theorem 6.2, the expectation
is that the resulting algorithm for DS inclusion with integer discount factor
will have an improved complexity. Lastly, we make use of the subset
construction based methods in order to present an improved on-the-fly
algorithm for DS inclusion, called QuIPFly.

The following statement instantiates Theorem 6.2 for discounted-sum
aggregation. Note that the difference in the formal statement is that here we
are able to completely characterize the type of the Büchi automaton as well:

###### Theorem 6.7

Let $P$ and $Q$ be weighted-automata, and $C$ be a regular safety/co-safety
comparator for an inequality with integer discount factor $d>1$.

  * •

Strict DS-inclusion $P\subset Q$ is reduced to emptiness checking of a safety
automaton of size $|P||C||Q|\cdot 2^{\mathcal{O}(|Q|\cdot|C|)}$.

  * •

Non-strict DS-inclusion $P\subseteq Q$ is reduced to emptiness checking of a
weak-Büchi automaton [64] of size $|P||C||Q|\cdot
2^{\mathcal{O}(|Q|\cdot|C|)}$.

###### Proof 46

Unlike Theorem 6.2, the Büchi automaton for emptiness checking has a specific
form: safety or weak-Büchi [64]. We can characterize these forms since we know
that the DS comparator for strict inequality and equality are co-safety and
safety automata respectively (Corollary 6.2).

Recall, that the Büchi automata that is being checked for emptiness is the
counterexample automaton. In essence, the counterexample automaton is formed
by an intersection of the maximal automaton with an appropriate comparator
(Lemma 6.3). Furthermore, we know that when the comparator for non-strict
inequality is safety, as for discounted sum, the maximal automaton will be a
safety automata (Lemma 6.1).

Consequently, in case of strict DS inclusion, the counterexample automata is
constructed by the intersection of a safety maximal automaton with the regular
safety DS-comparator for non-strict inequality. Due to closure of safety
automata under intersection, the resulting counterexample automata will be a
safety automata.

In case of non-strict DS-inclusion, the counterexample automata is constructed
by the intersection of the safety maximal automaton with the regular co-safety
DS-comparator for strict inequality. As a consequence of Theorem 6.1, the
counterexample automaton is weak-Büchi.

Lastly, the size of the resulting safety/weak Büchi automaton is given by the
product of the minimal automata (Corollary 6.1) and the comparator. Recall,
that the size of all comparators for discounted sum are identical (Theorem 6.5
and Theorem 6.6). Hence, all are given a size of $|C|$. ∎

Therefore, the final word is:

######  Corollary 6.4 ([DS-inclusion with safety/co-safety comparator)

Let $P$, $Q$ be weighted-automata, and $C$ be a regular (co)-safety DS-
comparator with integer discount-factor $d>1$.The complexity of DS-inclusion
is $|P||C||Q|\cdot 2^{\mathcal{O}(|Q|\cdot|C|)}$.

Clearly, this is an improvement over the worst-case complexity of QuIP.

######  QuIPFly: An on-the-fly implementation

The algorithm for DS inclusion with integer discount factor $d>1$ proposed in
Theorem 6.7 checks for emptiness of the counterexample automata. A naive
algorithm will construct the counterexample automata fully, and then check if
they are empty by ensuring the absence of an accepting lasso.

In QuIPFly, we implement a more efficient algorithm. In our implementation, we
make use of the fact that counterexample automata is a safety/weak Büchi that
is constructed from the intersection of a safety maximal automata and an
appropriate determinisitc safety/co-safety DS comparator. Recall that maximal
automata can be constructed in an on-the-fly fashion since it involves subset
construction like techniques. Since, the comparators are also deterministic,
they can also be designed in an on-the-fly manner.

In all, this facilitates an on-the-fly procedure for DS inclusion, since
successor states of state in the counterexample automata can be determined
directly from input weighted automata and the comparator automata. The
algorithm terminates as soon as an accepting lasso is detected. When an
accepting lasso is absent, the algorithm traverses all states and edges of the
counterexample automata. Note that for both strict and non-strict DS
inclusion, not every lasso in the counterexample automata is an accepting
lasso. Only those lassos are accepting for which the loop lies entirely inside
one accepting partition of the counterexample automata (recall that states of
weak Büchi automata are partitioned, and safety automata are also weak Büchi
automata). Tracking whether the loop is in an accepting partition by simply
looking at the states in the counterexample automata.

Note that the on-the-fly mechanism does not alter the worst-case performance
of DS inclusion, but it contribute to making the algorithm (a) more efficient
as it can terminate as soon as an accepting lasso is found, and (b) less
memory exhaustive, since it usually doesn’t require to store the entire
counterexample automata in memory at any given time.

####  6.5 Empirical evaluation

The goal of the empirical analysis is to examine performance of DS-inclusion
with integer discount-factor with safety/co-safety comparators against
existing tools to investigate the practical merit of our algorithm. Our
optimized on-the-fly algorithm for safety/co-safety comparator-based approach
for DS inclusion with integer discount factors is implemented in our prototype
called QuIPFly. QuIPFly is written in Python 2.7.12. QuIPFly employs basic
implementation-level optimizations to avoid excessive re-computation.

We compare against (a) Regular-comparator based tool QuIP, and (b) DS-
determinization and linear-programming tool DetLP. Recall from Chapter 5, QuIP
is written in C++, and invokes state-of-the-art Büchi language inclusion-
solver RABIT [5]. We enable the -fast flag in RABIT, and tune its Java-threads
with Xss, Xms, Xmx set to 1GB, 1GB and 8GB, respectively. DetLP is also
written in C++, and uses linear programming solver GLPSOL provided by GLPK
(GNU Linear Prog. Kit) [2]. We compare these tools along two axes: runtime and
number of benchmarks solved.

Figures are best viewed online and in color.

Figure 6.1: Runtime comparion of QuIP andQuIPFly. $s_{P}=s_{Q}$ on $x$-axis,
$wt=4$, $\delta=3$, $d=3$, $P\subset Q$

###### Design and setup for experiments

Due to lack of standardized benchmarks for weighted automata, we follow a
standard approach to performance evaluation of automata-theoretic tools [6,
71, 86] by experimenting with randomly generated benchmarks, using random
benchmark generation procedure described in [24].

The parameters for each experiment are number of states $s_{P}$ and $s_{Q}$ of
weighted automata, transition density $\delta$, maximum weight $wt$, integer
discount-factor $d$, and
$\mathsf{inc}\in\\{\mathsf{strct},\mathsf{nstrct}\\}$. In each experiment,
weighted automata $P$ and $Q$ are randomly generated, and runtime of
$\mathsf{inc}$-DS-inclusion for all three tools is reported with a timeout of
900$\sec$. We run the experiment for each parameter tuple 50 times. All
experiments are run on a single node of a high-performance cluster consisting
of two quad-core Intel-Xeon processor running at 2.83GHz, with 8GB of memory
per node. We experiment with $s_{P}=s_{Q}$ ranging from 0-1500 in increments
of 25, $\delta\in\\{3,3.5,4\\}$, $d=3$, and
$wt\in\\{d^{1}+1,d^{3}-1,d^{4}-1\\}$.

###### Observations and Inferences

Figure 6.2: Number of benchmarks solved between DetLP and QuIPFly.
$s_{P}=s_{Q}=75$, $wt=4$, $\delta=3$, $d=3$, $P\subset Q$

For clarity of exposition, we present the observations for only one parameter-
tuple. Trends and observations for other parameters were similar.

######  QuIPFly outperforms QuIP

by at least an order of magnitude in runtime. Fig 6.1 plots the median runtime
of all 50 experiments for the given parameter-values for QuIP and QuIPFly.
More importantly, QuIPFly solves all of our benchmarks within a fraction of
the timeout, whereas QuIP struggled to solve at least 50% of the benchmarks
with larger inputs (beyond $s_{P}=s_{Q}=1000$). Primary cause of failure is
memory overflow inside RABIT. We conclude that regular safety/co-safety
comparators outperform their regular counterpart, giving credit to the simpler
subset-constructions vs. Büchi complementation.

######  QuIPFly outperforms DetLP

comprehensively in runtime and in number of benchmarks solved. We were unable
to plot DetLP in Fig 6.1 since it solved fewer than 50% benchmarks even with
small input instances. Fig 6.2 compares the runtime of both tools on the same
set of 50 benchmarks for a representative parameter-tuple on which all 50
benchmarks were solved. The plot shows that QuIPFly beats DetLP by 2-4 orders
of magnitude on all benchmarks.

###### Overall verdict

Overall, QuIPFly outperforms QuIP and DetLP by a significant margin along both
axes, runtime and number of benchmarks solved. This analysis gives unanimous
evidence in favor of our safety/co-safety approach to solving DS-inclusion.

####  6.6 Chapter summary

The goal of this chapter was to improve comparator-based solutions for DS
inclusion. To this end, here we further the understanding of language-
theoretic properties of discounted-sum aggregate function by demonstrating
that DS-comparison languages form safety and co-safety languages. These
properties are utilized to obtain a decision procedure for DS-inclusion that
offers both tighter theoretical complexity, improved scalability, and better
performance than separation-of-techniques. To the best of our knowledge, this
is the first work that applies language-theoretic properties such as
safety/co-safety in the context of quantitative reasoning. In doing so, we
demonstrate that the close integration of structural analysis and numerical
analysis using comparator automata can enhance algorithms in quantitative
reasoning since they can benefit from the abundance of work in qualitative
reasoning.

###  Chapter 7 DS inclusion with non-integer discount factors

The theoretical and practical progress in DS inclusion so far have been made
for the case when the discount factor is an integer. The problem of complexity
of DS inclusion with non-integer discount factors is still very much open - so
much so that even its decidability is a mystery so far. In wake of the unknown
decidability of DS inclusion with non-integer discount factor, this chapter
takes the approach of developing pragmatic solutions to the problem. In this
case, we develop an anytime algorithm [49] for DS inclusion for non-integer
discount factors.

####  7.1 Introduction

In its most generality, the decidability of DS inclusion is still unknown
[39]. The goal of this work is to build a pragmatic solution for DS inclusion
despite its unknown decidability. Prior results have shown that the parameter
that determines the rate at which weights loose their significance, called the
discount factor, primarily governs the hardness of DS inclusion: When the
discount factor is an integer, DS inclusion is PSPACE-complete [25]; On the
contrary, when the discount factor is a non-integer, decidability of DS
inclusion is unknown, and has been an open problem for more than a decade
[39]. This work strives to address DS inclusion for non-integer discount
factors, since most practical applications of DS aggregate function, such as
reinforcement learning [85], planning under uncertainty [78], and game theory
[75], make use of non-integer discount factors. In particular, these
applications require that the discount factor $d>1$ to be very close to 1,
i.e. $1<d<2$. Therefore, this work focuses on DS inclusion when $1<d<2$.

This work addresses DS inclusion for non-integer discount factors. In
particular, we investigate the case when the discount factor $d>1$ is very
close to 1, i.e. $1<d<2$, since that is the value used in practice. Our focus
is not on resolving whether DS inclusion is decidable for $1<d<2$ but to
design pragmatic solutions for DS inclusion despite its decidability being
unknown.

A natural step in this direction is to solve approximations of DS inclusion.
However, we discover that approximations of DS inclusion is at least as hard
as DS inclusion itself (Theorem 7.1), since DS inclusion reduces to its
approximations in polynomial time. Hence, the decidability of approximations
of DS inclusion is also currently unknown. As a result, we are faced with the
challenge to design a solution for DS inclusion with $1<d<2$ without the
ability to develop algorithms for DS inclusion or its approximations.

To address this challenge, we turn to anytime algorithms that have been used
extensively to design pragmatic solution in AI for problems with high
computational complexity or even undecidability [49]. Anytime algorithms are a
class of algorithms that generate approximate answers quickly and proceed to
construct progressively better approximate solutions over time [49]. In the
process, they may either generate an exact solution and terminate, or
continuously generate a better approximation. In the context of designing a
pragmatic solution for DS inclusion with $1<d<2$ , we design an anytime
algorithm for the same. In addition, our anytime algorithm is co-computational
enumerable, i.e., it is guaranteed to terminate on input instances on which DS
inclusion does not hold. The algorithm gives only approximate answers
otherwise.

The formalism is detailed here. Let $P$ and $Q$ be weighted automata, and let
$1<d<2$ be the discount factor. We say $P$ is DS included in  $Q$, denoted by
$P\subseteq Q$, if weight of all executions in $P$ is less than or equal to
that in $Q$. So, our anytime algorithm, called $\mathsf{DSInclusion}$, either
terminates and returns a crisp $\mathsf{True}$ or $\mathsf{False}$ answer to
$P\subseteq Q$, or it continuously generates an approximation that $P$ is
$d\cdot\varepsilon$-close to $Q$, in a precise sense defined below. If an
execution of $\mathsf{DSInclusion}$ is interrupted due to external factors
such as manual interference or resource overflow, then the algorithm will
return the most recently computed $d\cdot\varepsilon$-close approximation.
Additionally, if $P\subseteq Q$ does not hold, then the algorithm is
guaranteed to terminate after a finite amount of time. Note that we do not
prove termination when $P\subseteq Q$ holds. But this is not surprising,
because if we could then we would have proven decidability of DS inclusion for
$1<d<2$.

The core of our algorithm is $\mathsf{anytimeInclusion}$ (Overview: § 7.3,
Description: § 7.6), a tail recursive algorithm that recurses on the
approximation factor $0<\varepsilon<1$ by halving it in each new invocation.
Conceptually, $\mathsf{anytimeInclusion}$ over- and under-approximates DS
inclusion in each new invocation of the algorithm, and continues until either
an exact solution is obtained or the algorithms’ execution is interrupted. Due
to the unknown decidability of both approximations, partial solutions for the
over- and under-approximations are developed. Comparator automata [25] based
techniques for aggregate functions that represent lower- and upper-
approximations of discounted sum are used, respectively for the partial
solutions (§ 7.4 and § 7.5, respectively).

Another advantage of our anytime algorithm is that it can be run upto a
desired precision $0<\varepsilon_{c}<1$. For this the recursive procedure
$\mathsf{DSInclusion}$ will be run till it is invoked with approximation
factor $\varepsilon_{c}$ in the worst case, i.e., in the worst-case
$\mathsf{DSInclusion}$ will be invoked for
$\mathcal{O}(\log\frac{1}{\varepsilon_{c}})$ times, each time with a lower
approximation factor. In this case, the complexity of running
$\mathsf{DSInclusion}$ is linear in $\frac{1}{\varepsilon_{c}}$, exponential
in size of the input DS automata and exponential in $\frac{1}{(d-1)^{2}}$.
This shows that as $d$ and $\varepsilon_{c}$ become smaller solving upto a
desired precision explodes rapidly. These observations are expected, as they
corroborate with the known result on undecidability of sum-inclusion (Loosely
speaking, DS inclusion with $d=1$, and $\varepsilon=0$) [11, 62].

In conclusion, this work does not resolve the decidability debate on DS
inclusion with $1<d<2$. Instead, it designs an anytime algorithm that renders
approximations with theoretical guarantees, and time-bounds when the precision
value is fixed. Thus, our algorithm is suitable for pragmatic purposes.

####  7.2 Preliminaries

This section defines terminology and notation used in the rest of this
chapter. A key difference in this chapter is that we solve DS inclusion over
finite words. A similar proof can be adapted for infinite words.

A finite sequence of weights is said to be bounded by $\mu>0$ if the absolute
value of all weights in the sequence are less than or equal to $\mu$.

A finite-state automaton [87] 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. A finite-state automaton is deterministic if for all states $s$ and
inputs $a$, $|\\{s^{\prime}|(s,a,s^{\prime})\in\delta\\}|\leq 1$ and
$|{\mathit{Init}}|=1$; otherwise, it is nondeterministic. Deterministic and
non-determinsitic finite-state automata are denoted by DFA and NFA,
respectively. An NFA is complete if for all $s\in\mathit{S}$ and $a\in\Sigma$,
there exists a transition $(s,a,t)\in\delta$ for some state $t\in\mathit{S}$.
For a word $w=w_{0}w_{1}\dots w_{m}\in\Sigma^{*}$, a run $\rho$ of $w$ is a
sequence of states $s_{0}s_{1}\dots s_{m+1}$, such that
$s_{0}\in{\mathit{Init}}$, and $\tau_{i}=(s_{i},w_{i},s_{i+1})\in\delta$ for
all $i$. A run $\rho$ is accepting if its last state $s_{m+1}\in\mathcal{F}$.
A word $w$ is _accepted_ by NFA/DFA if it has an accepting run. Regular
languages are languages accepted by DFA/NFA.

A weighted automaton over finite words (weighted automaton, in short), is a
tuple $\mathcal{A}=(\mathcal{M},\gamma,f)$, where
$\mathcal{M}=(\mathit{S},\Sigma,\delta,{\mathit{Init}},\mathit{S})$ is a
complete NFA with all states as accepting,
$\gamma:\delta\rightarrow\mathbb{Z}$ is a weight function, and
$f:\mathbb{Z}^{*}\rightarrow\mathbb{R}$ is an aggregation function. Words and
runs in weighted automata are defined as they are in an NFA. The weight
sequence of a run $\rho=s_{0}s_{1}\dots s_{m+1}$ of word $w=w_{0}w_{1}\dots
w_{m}$ is $wt_{\rho}=n_{0}n_{1}\dots n_{m}$ 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 $f{(wt_{\rho})}$. The weight of word $w\in\Sigma^{*}$
in weighted automata is defined as
$\mathit{wt}(w,\mathcal{A})=max\\{f(\rho)|\rho$ is a run of $w$ in
$\mathcal{A}\\}$. The problem of $f$-inclusion compares the weight of words in
two weighted automata with the same aggregate function. Given weighted
automata $P$ and $Q$ with aggregate function
$f:\mathbb{N}^{*}\rightarrow\mathbb{R}$, $P$ is said to be $f$-included in $Q$
if for all words $w\in\Sigma^{*}$, $\mathit{wt}(w,P)\leq\mathit{wt}(w,Q)$.

This work studies the discounted-sum inclusion problem. The discounted sum
(DS) of a finite sequence $A=a_{0}\dots a_{n}$ for discount factor $d>1$,
denoted $\mathit{DS}({A},{d})=a_{0}+\frac{a_{1}}{d}\dots+\frac{a_{n}}{d^{n}}$.
DS automata with discount factor $d>1$ are weighted automata with discounted
sum aggregation with discount factor $d$. Therefore, given two DS automata $P$
and $Q$ with the same discount factor, $P$ is DS-included in $Q$ if weight of
every word in $P$ is less than or equal to that in $Q$. We reserve the
notation $P\subseteq Q$ to denote $P$ is DS-included in $Q$. While DS
inclusion is PSPACE-complete when the discount factor is an integer, its
decidability is still open for non-integer discount factors [32, 39]. For sake
of clearer exposition, this paper assumes that the weight along transitions in
a DS automata are non-negative integers. There are no technical differences in
extending the result to integer weights.

In a similar vein to recent progess on DS inlcusion for integer discount
factors [24, 28], this work makes use of comparator automata to design the
anytime algorithm. Comparator automata and comparison languages are defined as
follows: For a finite set of integers $\Sigma$, an aggregate function
$f:\mathbb{Z}^{*}\rightarrow\mathbb{R}$, and equality or inequality relation
$\mathsf{R}\in\\{<,>,\leq,\geq,=,\neq\\}$, the comparison language for $f$ and
$\mathsf{R}$ is a language over the alphabet $\Sigma$ that accepts a word
$A\in\Sigma^{*}$ iff $f(A)$ $\mathsf{R}$ $0$ holds. A comparator automaton
(comparator, in short) for $f$ and $\mathsf{R}$ is an automaton that accepts
the comparison language for $f$ and $\mathsf{R}$ [25]. A comparator is regular
if its automaton is an NFA. Prior work has shown that comparator for
discounted sum (DS comparator, in short) is regular for all $\mathsf{R}$ iff
the discount factor is an integer [26]. Regularity of the comparator has been
crucial to the progress in DS inclusion for integer discount factors.
Therefore, another contribution in this work is to define an approximation for
discounted-sum with non-integer discount factor so that its comparator is
regular. We will use these regular comparators to design the anytime
algorithm.

####  7.3 Overview

Before delving into the technical details of the anytime algorithm, we give a
roadmap of the approach. Notions of approximations are central to anytime
algorithms, so we begin with defining approximations to DS inclusion:

######  Definition 7.1 ($d\cdot\varepsilon$-close approximation)

Given DS automata $P$ and $Q$ with discount factor $d>1$, and an approximation
parameter $\varepsilon>0$, $P$ is said to be $d\cdot\varepsilon$-close to $Q$,
denoted by $P\subseteq Q+d\cdot\varepsilon$, if for all words
$w\in\Sigma^{\omega}$,
$\mathit{wt}(w,P)\leq\mathit{wt}(w,Q)+d\cdot\varepsilon$.

######  Definition 7.2 ($d\cdot\varepsilon$-far approximation)

Given DS automata $P$ and $Q$ with discount factor $d>1$, and an approximation
parameter $\varepsilon>0$, $P$ is said to be $d\cdot\varepsilon$-far from $Q$,
denoted by $P\subseteq Q-d\cdot\varepsilon$, if for all words
$w\in\Sigma^{\omega}$,
$\mathit{wt}(w,P)\leq\mathit{wt}(w,Q)-d\cdot\varepsilon$.

Given the open decidability status of DS inclusion, the next alternative is to
develop algorithms for the aforementioned approximations. That is not possible
either, however, for the following reason:

###### Theorem 7.1

[Unknown decidability of approximations]

  1. 1.

There exists a polynomial time reduction from DS inclusion to
$d\cdot\varepsilon$-close approximation for an approximation factor
$\varepsilon>0$.

  2. 2.

There exists a polynomial time reduction from DS inclusion to
$d\cdot\varepsilon$-far approximation for an approximation factor
$\varepsilon>0$.

###### Proof 47

The intuitive argument behind showing that $P\subseteq Q$ reduces to
$P^{\prime}\subseteq Q^{\prime}+d\cdot\varepsilon$ for an $\varepsilon>0$ is
to show that one can transform $Q$ into a weighted automaton $Q^{\prime}$ such
that $Q^{\prime}=Q-d\cdot\varepsilon$. Similarly, to show that $P\subseteq Q$
reduces to $P^{\prime}\subseteq Q^{\prime}-d\cdot\varepsilon$, we show that
one can transform $Q$ into $Q^{\prime}$ such that
$Q^{\prime}=Q+d\cdot\varepsilon$. An direct corollary of Theorem 7.1 is that
the decidability of approximations of DS inclusion is currently unknown as
well.

DS inclusion is decidable iff over approximation of DS is decidable: First we
prove that every instance of DS inclusion can be reduced to an instance of
over approximation of DS inclusion. Let $d>1$ be a discount factor and $P$ and
$Q$ be DS automata. Then we will show that there exists alternate DS automata
$R$ and $S$, and an approximation factor $\varepsilon>0$ such that $P\subseteq
Q\iff R\subseteq S+d\cdot\varepsilon$. Let $\\#$ be an character that is not
present in the alphabet of $P$ and $Q$ First of all, we generate a new DS
automaton $P_{\\#}$ from $P$ such that every word in P is prefixed with the
character $\\#$ and its weight is multiplied by $\frac{1}{d}$. This can be
done by a simple automata-theoretic transformation of $P$: Include all states
and transitions from $P$ in $P_{\\#}$. Retain all accepting states of $P$ in
$P_{\\#}$. Add a new state $s_{\\#}$. Add a transition from $s_{\\#}$ to state
$s_{v_{\mathit{init}}}$ of $P$, and assign it a weight of 0. Make the new
state $s_{\\#}$ the accepting state. This is $P_{\\#}$. Similarly, construct
DS automaton $Q_{\\#}$ from $Q$. It is easy to see that $P\subseteq Q$ iff
$P_{\\#}\subseteq Q_{\\#}$. Finally, construct $Q^{\prime}$ from $Q_{\\#}$ by
assigning the transition from $s_{\\#}$ to $s_{init}$ a weight of $-1$. Then
it is easy to see that $P_{\\#}\subseteq Q_{\\#}$ iff $P_{\\#}\subseteq
Q^{\prime}+1$. Let $\varepsilon=\frac{1}{d}$, then it is easy to see that
$P_{\\#}\subseteq Q_{\\#}$ iff $P_{\\#}\subseteq
Q^{\prime}+d\cdot\varepsilon$. Therefore, $P\subseteq Q$ iff $P_{\\#}\subseteq
Q^{\prime}+d\cdot\varepsilon$.

Next, we prove that every instance of over-approximation of DS inclusion can
be reduced to an instance of DS inclusion. Let $P$ and $Q$ be DS automata with
discount factor $d>1$, and let $\varepsilon>0$ be its approximation factor.
Suppose $P\subseteq Q+d\cdot\varepsilon$ holds. Let
$d\cdot\varepsilon=\frac{r}{s}$. Generate $P_{\\#}$ and $Q_{\\#}$ as earlier.
Since $P\subseteq Q+d\cdot\varepsilon$ holds, we get that $P_{\\#}\subseteq
Q_{\\#}+\varepsilon$ holds. Modify $Q_{\\#}$ to $Q^{\prime}$ so that the
weight of the transition from its inital state is now $\varepsilon$. Suppose
$\varepsilon=\frac{m}{n}$ for natural numbers $m,n>0$. Then, Multiply the
weight of all edges in $P_{\\#}$ and $Q^{\prime}$ with $n$ to obtain new DS
automata $R$ and $S$, respectively. Then, it is easy to see that $P\subseteq
Q+d\cdot\varepsilon$ holds then $R\subseteq S$ holds.

DS inclusion is decidable iff under approximation of DS is decidable: Similar
to the previous proof except that the “+” will be replace by “-”. ∎

Given these challenges, we propose an anytime algorithm for DS inclusion. The
anytime algorithm either terminates after a finite amount of time with a crisp
$\mathsf{True}$ or $\mathsf{False}$ answer to DS inclusion, or it continuously
generates $d\cdot\varepsilon$-close approximations, where the approximation
factor $0<\varepsilon<1$ decreases in time. If an execution of the algorithm
is interrupted at anytime before a natural termination, then it returns the
most recently computed $d\cdot\varepsilon$-close approximation.

Algorithm 4 $\mathsf{anytimeInclusion}(P,Q,d,\varepsilon)$
Inputs: DS automata $P$, $Q$, discount factor $1<d<2$, and approximation
factor $0<\varepsilon<1$

1: if $\mathsf{lowApproxDSInc}(P,Q,d,\varepsilon)$ returns $P\subseteq
Q=\mathsf{False}$ then

2: return $P\subseteq Q=\mathsf{False}$

3: end if

4: if $\mathsf{upperApproxDSInc}(P,Q,d,\varepsilon)$ returns $P\subseteq
Q=\mathsf{True}$ then

5: return $P\subseteq Q=\mathsf{True}$

6: end if

7: if Interrupt then return $P\subseteq Q+d\cdot\varepsilon=\mathsf{True}$

8: $\mathsf{anytimeInclusion}(P,Q,d,\frac{\varepsilon}{2})$

Algorithm 4 outlines our anytime procedure. On receiving DS automata $P$ and
$Q$ with discount factor $1<d<2$, the algorithm invokes
$\mathsf{anytimeInclusion}$ with an initial approximation factor
$0<\varepsilon_{\mathsf{init}}<1$. As is clear from Algorithm 4,
$\mathsf{anytimeInclusion}$ is a tail recursive procedure in which the
approximation factor is halved in each new invocation. In the invocation with
approximation factor $0<\varepsilon<1$, $\mathsf{anytimeInclusion}$ calls two
functions $\mathsf{lowApproxDSInc}$ and $\mathsf{upperApproxDSInc}$. Ideally,
these procedures would over- and under- approximate DS inclusion using
$d\cdot\varepsilon$-close and $d\cdot\varepsilon$-far, respectively.
Unfortunately, that is not possible due to Theorem 7.1. Therefore, a challenge
here is the design of these two subprocedures. At this point it is sufficient
to know that in response to the challenge we design $\mathsf{lowApproxDSInc}$
so that it combines partial solutions of DS inclusion and
$d\cdot\varepsilon$-close approximation. Specifically, given approximation
factor $\varepsilon>0$, its outcomes are either $P\subseteq Q=\mathsf{False}$
or $P\subseteq Q+d\cdot\varepsilon=\mathsf{True}$. Similarly, the algorithm
$\mathsf{upperApproxDSInc}$ is designed to return either $P\subseteq
Q=\mathsf{True}$ or $P\subseteq Q-d\cdot\varepsilon=\mathsf{False}$, hence
combining DS inclusion and $d\cdot\varepsilon$-far approximation. The
algorithm design for $\mathsf{lowApproxDSInc}$ and $\mathsf{upperApproxDSInc}$
use regular comparator automata for aggregate functions that represent the
lower and upper approximations of discounted sum, respectively. These
subprocedures have been presented in detail in § 7.4 and § 7.5, respectively.

Equipped with descriptions of $\mathsf{lowApproxDSInc}$ and
$\mathsf{upperApproxDSInc}$, we can finally describe
$\mathsf{anytimeInclusion}$ (Algorithm 4). Without loss of generality, suppose
that $\mathsf{anytimeInclusion}$ can be interrupted only on completion of
$\mathsf{upperApproxDSInc}$. Consider the invocation with approximation factor
$0<\varepsilon<1$. First, $\mathsf{lowApproxDSInc}$ will be called. If it
returns $P\subseteq Q=\mathsf{False}$, then $\mathsf{anytimeInclusion}$ is
terminated, and it returns the crisp outcome that $P\subseteq
Q=\mathsf{False}$. Otherwise, $\mathsf{lowApproxDSInc}$ must have returned
$P\subseteq Q+d\cdot\varepsilon=\mathsf{True}$, i.e. the
$d\cdot\varepsilon$-close approximation holds. Therefore, if
$\mathsf{anytimeInclusion}$ is interrupted here onward, it can return this
approximate result. But if $\mathsf{anytimeInclusion}$ is not interrupted, it
proceeds to solve $\mathsf{upperApproxDSInc}$. If $\mathsf{upperApproxDSInc}$
returns $P\subseteq Q=\mathsf{True}$, once again $\mathsf{anytimeInclusion}$
is terminated, and the crisp $P\subseteq Q=\mathsf{Ture}$ solution is
returned. If $\mathsf{anytimeInclusion}$ is interrupted at this point, the
algorithm returns the $d\cdot\varepsilon$-close approximation result obtained
from $\mathsf{lowApproxDSInc}$. Finally, if the algorithm has not been
interrupted yet, $\mathsf{anytimeInclusion}$ is invoked with lower
approximation factor $\frac{\varepsilon}{2}$. That completes the description
of our anytime algorithm.

Finally, to see why this algorithm is co-recursively enumerable, observe that
if $P\subseteq Q=\mathsf{False}$, then there must be an approximation factor
$0<\gamma<1$ such that for all $0<\delta<\gamma$, $P\subseteq
Q+d\cdot\delta=\mathsf{False}$. Therefore, as the approximation factor is
halved in each invocation of $\mathsf{anytimeInclusion}$, it will eventually
be smaller than the aforementioned $\gamma$. When this happens, then
subprocedure $\mathsf{lowApproxDSInc}$ will be forced to return $P\subseteq
Q=\mathsf{False}$. Hence, if $P\subseteq Q=\mathsf{False}$, then the anytime
algorithm will necessarily terminate.

####  7.4 Algorithm $\mathsf{lowApproxDSInc}$

This section describes Algorithm $\mathsf{lowApproxDSInc}$. Recall, given
inputs DS automata $P$ and $Q$, discount factor $1<d<2$ and approximation
factor $0<\varepsilon<1$, $\mathsf{lowApproxDSInc}(P,Q,d,\varepsilon)$ either
returns $P\subseteq Q$ does not hold or $P\subseteq Q+d\cdot\varepsilon$
holds. Note that these outcomes are not mutually exclusive, i.e., there exist
input instances for which both of the outcomes may hold. In these cases, the
algorithm may return either of the outcomes; the procedure will still be
sound.

Intuitively, $\mathsf{lowApproxDSInc}$ solves whether $P$ is $f$-included in
$Q$, where $f$ is an aggregate function that approximates the discounted-sum
from below. Let this aggregate function, denoted $\mathsf{DSLow}$, be defined
such that given a weight-sequence $W$, discount factor $1<d<2$ and
approximation factor $0<\varepsilon<1$,
$0\leq\mathit{DS}({W},{d})-\mathsf{DSLow}(W,k,p)<d\cdot\varepsilon$ holds.
Then, we argue that if $P$ is $\mathsf{DSLow}$-included in $Q$, then
$P\subseteq Q+d\cdot\varepsilon$ holds. Otherwise, if $P$ is not
$\mathsf{DSLow}$-included in $Q$, then $P\subseteq Q$ will not hold.
Therefore, $\mathsf{lowApproxDSInc}$ solves $\mathsf{DSLow}$-inclusion. We use
techniques from regular comparators [25] to solve $\mathsf{DSLow}$-inclusion.

Organization and notation. First, the lower approximation of discounted-sum
$\mathsf{DSLow}$ is formally defined in § 7.4.1. Second, a regular comparator
for $\mathsf{DSLow}$ is constructed in § 7.4.2. Finally, we use the regular
comparator to design $\mathsf{lowApproxDSInc}$ § 7.4.3. Let $k,p>0$ be
positive rationals such that the discount factor $1<d<2$ and approximation
factor $0<\varepsilon<1$ are expressed as $d=1+2^{-k}$ and
$\varepsilon=2^{-p}$, respectively.

#####  7.4.1 Lower approximation of discounted-sum

This section defines lower approximation of discounted sum when $1<d<2$. A
consideration while defining the aggregate function is that its comparator
should be regular. Therefore, our definition of lower approximation of
discounted sum is motivated from the notion of recoverable gap [31] which is
known to play an important role in guaranteeing regularity of comparators
[26].

The recoverable gap of a weight sequence $W$ w.r.t discount factor $d>1$ is
$d^{|W|-1}\cdot\mathit{DS}({W},{d})$. In other words, it is the normalized DS
of a weight sequence. Intuitively, the recoverable gap of a weight sequence
gives a measure of how far its discounted-sum is from 0, and hence is a
building block for designing the comparator automata. A property of
recoverable gap that results in the regularity of comparator for DS with
integer discount factor is that the minimum non-zero difference between the
recoverable gap of sequences is fixed. Specifically, this difference is 1 when
the discount factor is an integer. But for non-integer discount factors, this
difference can become arbitrarily small [10]. This explains why DS comparator
are not regular for non-integer discount factors.

To this effect, we begin by defining an approximation of the recoverable gap
such that the aforementioned difference is fixed under the new definition.
This is guaranteed by rounding-off the recoverable gap to a fixed resolution
$r=(d-1)\cdot\varepsilon=2^{-(p+k)}$, where $d=1+2^{-k}$ is the discount
factor and $\varepsilon=2^{-p}$ is the approximation factor. Formally, let
$\mathsf{roundLow}(x,k,p)$ denote the largest integer multiple of the
resolution that is less than or equal to $x$, for $x\in\mathbb{R}$. Then,
$\mathsf{roundLow}(x,k,p)=i\cdot 2^{-(p+k)}$ for an integer $i\in\mathbb{Z}$
such that for all integers $j\in\mathbb{Z}$ for which $j\cdot 2^{-(p+k)}\leq
x$, we get that $j\leq i$. Then,

###### Lemma 7.1

Let $k,p>0$ be rational-valued parameters. Then, for all real values
$x\in\mathbb{R}$, $0\leq x-\mathsf{roundLow}(x,k,p)<2^{-(p+k)}$.

###### Proof 48

There exists a unique integer $i\in\mathbb{Z}$ and $0\leq b<2^{-(p+k)}$ such
that $x=i\cdot 2^{-(p+k)}+b$. Then, $\mathsf{roundLow}(x,k,p)=i\cdot
2^{-(p+k)}$. Therefore, we get that $0\leq
x-\mathsf{roundLow}(x,k,p)<2^{-(p+k)}$. ∎

######  Lemma 7.2 (Monotonicity)

Let $k,p>0$ be rational-valued parameters. Then, if $x\leq y$, then
$\mathsf{roundLow}(x,k,p)\leq\mathsf{roundLow}(y,k,p)$.

###### Proof 49

There exist unique integers $i,j,\in\mathbb{Z}$, and positive values $0\leq
a,b<2^{-(p+k)}$ such that $x=i\cdot 2^{-(p+k)}+a$ and $y=j\cdot 2^{-(p+k)}+b$.
By definition of $\mathsf{roundLow}$, $\mathsf{roundLow}(x,k,p)=i\cdot
2^{-(p+k)}$ and $\mathsf{roundLow}(y,k,p)=j\cdot 2^{-(p+k)}$. Then, if $x\leq
y$ then one of the two must have occurred:

  * •

$i<j$. In this case, $\mathsf{roundLow}(x,k,p)<\mathsf{roundLow}(y,k,p)$.

  * •

$i=j$ and $a\leq b$. In this case,
$\mathsf{roundLow}(x,k,p)=\mathsf{roundLow}(y,k,p)$

Therefore, if $x\leq y$ then
$\mathsf{roundLow}(x,k,p)\leq\mathsf{roundLow}(y,k,p)$. ∎

Then, for all real values $x\in\mathbb{R}$, $0\leq
x-\mathsf{roundLow}(x,k,p)<2^{-(p+k)}$. Then, lower gap is defined as follows:

######  Definition 7.3 (Lower gap)

Let $k,p>0$. Let $W$ be a finite weight sequence. The lower gap of $W$ with
discount factor $d=1+2^{-k}$ and approximation factor $\varepsilon=2^{-p}$,
denoted $\mathsf{gapLower}(W,k,p)$, is

$\mathsf{gapLower}(W,k,p)=\begin{cases}0,\text{ for }|W|=0\\\
\mathsf{roundLow}(\mathsf{gapLower}(U,k,p)+u,k,p)\text{ for }W=U\cdot
u\end{cases}$

Note that the minimum non-zero difference between the lower gap of weight
sequences is the resolution $r=2^{-(p+k)}$. Similar to the relationship
between recoverable gap and DS, lower approximation of DS is defined as
follows:

######  Definition 7.4 (Lower approximation of discounted-sum)

Let $k,p>0$. Let $W$ be a finite weight sequence. The lower approximation of
discounted sum, called lower DS, for weight sequence $W$ with discount factor
$d=1+2^{-k}$ and approximation factor $\varepsilon=2^{-p}$ is denoted by and
defined as

$\mathsf{DSLow}(W,k,p)={\mathsf{gapLower}(W,k,p)}/{d^{|W|-1}}$

To complete the definition, we prove that the value computed by
$\mathsf{DSLow}$ in Definition 7.4 corresponds to a value close to the
discounted-sum. To prove that we first establish the following” Given discount
factor $d=1+2^{-k}$ and approximation factor $\varepsilon=2^{-p}$, a
resolution sequence of length $n>0$, denoted $R_{n}$, is the $n$-length
sequence in which all elements are $r=2^{-(p+k)}$.

###### Lemma 7.3

Let $k,p>0$ be rational-valued parameters. Let $d=1+2^{-k}$ be the non-
integer, rational discount factor and $\varepsilon=2^{-p}$ be the
approximation factor. Let $W$ be a finite non-empty weight sequence. Then
$0\leq\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)<\mathsf{gap}(R_{|W|},d)$.

###### Proof 50

We prove the above by induction on the length sequence $W$.

Base case: When $|W|=1$. Let $W=w_{0}$. In this case,
$\mathsf{gap}(W,d)=w_{0}$ and
$\mathsf{gapLower}(W,k,p)=\mathsf{roundLow}(w_{0},k,p)$. Then, from Lemma 7.1
we get that $0\leq\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)<r$, which in turn
is the same as
$0\leq\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)<\mathsf{gap}(R_{1},d){d}$.

Inductive hypothesis: For all weight-sequences $W$ of length $n\geq 1$, it is
true that
$0\leq\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)<\mathsf{gap}(R_{n},d)$.

Induction step: We extend this result to weight-sequences of length $n+1$. Let
$W$ be an $n+1$-length weight-sequence. Then $W=W[n]\cdot w_{n}$, where $W[n]$
is the $n$-length prefix of $W$ and $w_{n}$ is $n+1$-th element.

We first show that $\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)\geq 0$:

$\displaystyle\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)$ $\displaystyle=$
$\displaystyle
d\cdot\mathsf{gap}(W[n],d)+w_{n}-\mathsf{roundLow}(d\cdot\mathsf{gapLower}(W[n],k,p)+w_{n},k,p)$
$\displaystyle\text{ Using monotonicity of }\mathsf{roundLow}\text{ and the
inductive hypothesis, we get}$ $\displaystyle\geq$ $\displaystyle
d\cdot\mathsf{gap}(W[n],d)+w_{n}-\mathsf{roundLow}(d\cdot\mathsf{gap}(W[n],d)+w_{n},k,p)$
From Lemma 7.1, we get the desired result.

Next, we show that
$\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)<\mathsf{gap}(R_{n+1},d)$.

$\displaystyle\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)$ $\displaystyle=$
$\displaystyle
d\cdot\mathsf{gap}(W[n],d)+w_{n}-\mathsf{roundLow}(d\cdot\mathsf{gapLower}(W[n],k,p)+w_{n},k,p)$
From Lemma 7.1, we get $\displaystyle<$ $\displaystyle
d\cdot\mathsf{gap}(W[n],d)+w_{n}-{(d\cdot\mathsf{gapLower}(W[n],k,p)+w_{n})}+2^{-(p+k)}$
$\displaystyle=$ $\displaystyle
d\cdot\mathsf{gap}(W[n],d)-{d\cdot\mathsf{gapLower}(W[n],k,p)}+2^{-(p+k)}$
From the inductive hypothesis, we get $\displaystyle<$ $\displaystyle
d\cdot\mathsf{gap}(R_{n},d)+2^{-(p+k)}\text{ where }R_{n}\text{ is the
}n\text{-length resolution sequence}$ $\displaystyle=$
$\displaystyle\mathsf{gap}(R_{n+1},d)\text{ where }R\text{ is the
}n+1\text{-length resolution sequence}$

This completes both sides of the proof. ∎

###### Theorem 7.2

Let $d=1+2^{-k}$ be the discount factor and $\varepsilon=2^{-p}$ be the
approximation factor, for rationals $p,k>0$. Then for all weight sequences
$W$, $0\leq\mathit{DS}({W},{d})-\mathsf{DSLow}(W,k,p)<d\cdot\varepsilon$.

###### Proof 51

The statement clearly holds when $|W|=0$ since
$\mathit{DS}({W},{d})=\mathsf{DSLow}(W,k,p)=0$. For $|W|>n$, we have proven
that
$0\leq\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)<\mathsf{gap}(R_{|W|},d)$,
where $R_{|W|}$ is the $|W|$-length sequence in which all elements are equal
to $r=2^{-(p+k)}$ (Lemma 7.3). Finally, division by $d^{|W|-1}$ completes the
proof.

The complete details are as follows: When $|W|=0$,
$\mathit{DS}({W},{d})=\mathsf{DSLow}(W,k,p)=0$, since
$\mathsf{gap}(W,d)=\mathsf{gapLower}(W,k,p)=0$. Therefore,
$0\leq\mathit{DS}({W},{d})-\mathsf{DSLow}(W,k,p)<d\cdot 2^{-p}$ holds when
$|W|=0$.

Otherwise, from Lemma 7.3, we get that
$0\leq\mathsf{gap}(W,d)-\mathsf{gapLower}(W,k,p)<\mathsf{gap}(R_{n},d)$, where
$n=|W|$. On division by $d^{n-1}$, we get that
$0\leq\mathit{DS}({W},{d})-\mathsf{DSLow}(W,k,p)<\mathit{DS}({R},{d})$. Now
$\mathit{DS}({R},{d})\leq\mathit{DS}({R_{\infty}},{d})$, where $R_{\infty}$ is
the $\infty$-length resolution sequence. Now,
$\mathit{DS}({R_{\infty}},{d})=\frac{2^{-(p+k)}\cdot
d}{d-1}=\frac{(d-1)\cdot\varepsilon\cdot d}{d-1}<\varepsilon\cdot d$.
Therefore, we get the desired result that
$0\leq\mathit{DS}({W},{d})-\mathsf{DSLow}(W,k,p)<d\cdot\varepsilon$.

∎

Therefore, the lower approximation of DS is well defined in this section.

#####  7.4.2 Comparator for lower approximation of DS

This section covers the construction of the comparator automaton for the lower
approximation of discounted-sum from Defintion 7.4. We show that the
comparator is regular by explicitly constructing its DFA. The construction
will utilize the fixed non-zero minimum property of the lower gap.

We begin with formal definitions of the comparison language and comparator
automata for lower DS.

######  Definition 7.5 (Comparison language for lower approximation of DS)

Let $\mu>0$ be an integer bound, and $k,p$ be positive integers. The
comparison language for lower approximation of discounted sum with discount
factor $d=1+2^{-k}$, approximation factor $\varepsilon=2^{-p}$, upper bound
$\mu$ and inequality relation $\mathsf{R}\in\\{\leq,\geq\\}$ is a language of
finite weight sequences $W$ over the alphabet $\Sigma=\\{-\mu,\dots,\mu\\}$
that accepts $W$ iff $\mathsf{DSLow}(W,k,p)$ $\mathsf{R}$ $0$ holds.

######  Definition 7.6 (Comparator automata for lower approximation of DS)

Let $\mu>0$ be an integer bound, and $k,p$ be positive integers. The
comparator automata for lower approximation of discounted sum with discount
factor $d=1+2^{-k}$, approximation factor $\varepsilon=2^{-p}$, upper bound
$\mu$ and inequality relation $\mathsf{R}\in\\{\leq,\geq\\}$ is an automaton
that accepts the corresponding comparison language.

Next, we construct a DFA for the comparator for lower DS.

The first observation towards the construction is that $\mathsf{DSLow}(W,k,p)$
$\mathsf{R}$ $0$ iff $\mathsf{gapLower}(W,k,p)$ $\mathsf{R}$ $0$, for all
finite weight sequences $W$. Therefore, it is sufficient to construct a DFA
that accepts weight sequence $W$ iff $\mathsf{gapLower}(W,k,p)$ $\mathsf{R}$
$0$. We achieve this by (a). Creating one state of the DFA for every possible
value of lower gap. (b). Note that the definition of lower gap (Definition
7.3) is inductive on the length of the weight sequence. So, transitions
between states is defined so that they obey the inductive definition. For (a),
note that lower gap are of the form $i\cdot r$ where $i\in\mathbb{Z}$.
Therefore, for all $i\in\mathbb{Z}$, we introduce a state $i$ to represent the
lower gap $i\cdot r$. For (b). we include a transition from state $i$ to state
$j$ on symbol $a\in\Sigma=\\{-\mu,\dots,\mu\\}$ iff $j\cdot
r=\mathsf{gapLower}(i\cdot r+a,k,p)$, thereby following Definition 7.3. Note
that this equation makes the transition relation deterministic as for all
$i\in\mathbb{Z}$ and $a\in\Sigma$ there is a unique $j\in\mathbb{Z}$ that
satisfies it. Since $\mathsf{gapLower}(W,k,p)=0$ when $|W|=0$, state 0 is made
the initial state. Finally, a state $i$ is an accepting state iff $i$
$\mathsf{R}$ $0$ holds.

The automaton created above has infinitely many states as every possible value
of lower gap corresponds to a state. To obtain finitely many states, we show
that it is sufficient to consider finitely many values of the lower gap:

######  Lemma 7.4 (Bounds on lower gap-value)

Let $\mu>0$ be an integer bound. Let $k,p$ be positive integers s.t.
$d=1+2^{-k}$ is the discount factor, and $\varepsilon=2^{-p}$ is the
approximation factor. Let $W$ be a finite and bounded weight sequence.

  1. 1.

If $\mathsf{gapLower}(W,k,p)\leq-\mu\cdot 2^{k}$ then for all
$u\in\\{-\mu,\dots,\mu\\}$, $\mathsf{gapLower}(W\cdot u,k,p)\leq-\mu\cdot
2^{k}$.

  2. 2.

If $\mathsf{gapLower}(W,k,p)\geq\mu\cdot 2^{k}+2^{-p}$ then for all
$u\in\\{-\mu,\dots,\mu\\}$, $\mathsf{gapLower}(W\cdot u,k,p)\geq\mu\cdot
2^{k}+2^{-p}$.

###### Proof 52

Proof for (1.). Recall, $\mathsf{gapLower}(W\cdot
u,k,p)=\mathsf{roundLow}(d\cdot\mathsf{gapLower}(W,k,p)+u,k,p)$. From the
definition of $\mathsf{roundLow}$, we get that $\mathsf{gapLower}(W\cdot
u,k,p)\leq d\cdot\mathsf{gapLower}(W,k,p)+u$. Since
$\mathsf{gapLower}(W,k,p)\leq-\mu\cdot 2^{k}$ holds, we get
$\mathsf{gapLower}(W\cdot u,k,p)\leq d\cdot(-\mu\cdot
2^{k})+u=(1+2^{-k})\cdot(-\mu\cdot 2^{k})+u=-\mu\cdot 2^{k}-\mu+u$. Since $u$
is at most $\mu$, we get that $\mathsf{gapLower}(W\cdot u,k,p)\leq-\mu\cdot
2^{k}$.

Proof of (2.) follows similarly, and hence has been omitted. ∎

The outcome of Lemma 7.4 is that it is sufficient to track the lower gap value
only when it is between $-\mu\cdot 2^{k}$ and $\mu\cdot 2^{k}+2^{-p}$ in the
construction.

###### Construction

Let $\mu>0$, $d=1+2^{-k}$, $\varepsilon=2^{-p}$ be the upper bound, discount
factor and approximation factor, respectively. Let $\mathsf{T}_{l}$ be the
largest integer such that $\mathsf{T}_{l}\cdot 2^{-(p+k)}\leq-\mu\cdot 2^{k}$
(Lemma 7.4\- Part 1). Let $\mathsf{T}_{u}$ be the smallest integer such that
$\mathsf{T}_{u}\cdot 2^{-(p+k)}\geq\mu\cdot 2^{k}+2^{-p}$ (Lemma 7.4 \- Part
2). For relation $\mathsf{R}\in\\{\leq,\geq\\}$, construct DFA
$\mathsf{compLow}(\mu,k,p,\mathsf{R})=(S,s_{I},\Sigma,\delta,\mathcal{F})$ as
follows:

  * •

$S=\\{\mathsf{T}_{l},\mathsf{T}_{l}+1,\dots,\mathsf{T}_{u}\\}$,
$s_{I}=\\{0\\}$ and $\mathcal{F}=\\{i|i\in S\text{ and $i$ $\mathsf{R}$
$0$}\\}$

  * •

Alphabet $\Sigma=\\{-\mu,-\mu+1,\dots,\mu-1,\mu\\}$

  * •

Transition function $\delta\subseteq S\times\Sigma\times S$ where
$(s,a,t)\in\delta$ then:

    1. 1.

If $s=\mathsf{T}_{l}$ or $s=\mathsf{T}_{u}$, then $t=s$ for all $a\in\Sigma$

    2. 2.

Else, let $\mathsf{roundLow}(d\cdot s\cdot 2^{-(p+k)}+a,k,p)=i\cdot
2^{-(p+k)}$ for $i\in\mathbb{Z}$

      1. (a)

If $\mathsf{T}_{l}\leq i\leq\mathsf{T}_{u}$, then $t=i$

      2. (b)

If $i>{\mathsf{T}_{u}}$, then $t=\mathsf{T}_{u}$

      3. (c)

If $i<{\mathsf{T}_{l}}$, then $t=\mathsf{T}_{l}$

###### Theorem 7.3

Let $\mu>0$ be and integer upper bound. Let $k,p>0$ be rational parameters
s.t. $d=1+2^{-k}$ is the discount factor and $\varepsilon=2^{-p}$ is the
approximation parameter. DFA $\mathsf{compLow}(\mu,k,p,\mathsf{R})$ accepts a
finite weight sequence $W\in\Sigma^{*}$ iff $\mathsf{DSLow}(W,k,p)$
$\mathsf{R}$ $0$. DFA $\mathsf{compLow}(\mu,k,p,\mathsf{R})$ has
$\mathcal{O}(\mu\cdot 2^{2k+p})$ states.

###### Proof 53

The proof shows that the final state of a the run of a word represents its
lower gap value. For this we show three things: Let $s_{f}$ be the final state
of the run. (a). if $\mathsf{T}_{l}<s_{f}<\mathsf{T}_{u}$ then its lower gap
value is $s_{f}\cdot r$, (b). if $\mathsf{T}_{l}\geq s_{f}$ then the lower gap
value is less than or equal to $\mathsf{T}_{l}\cdot r$, and (c). if
$\mathsf{T}_{u}\leq s_{f}$ then the lower gap value is greater than or equal
to $\mathsf{T}_{u}\cdot r$.

The proof is very similar to Theorem 6.4, and hence its details have been left
for the reader to fill in. ∎

#####  7.4.3 Algorithm details for $\mathsf{lowApproxDSInc}$

This section describes $\mathsf{lowApproxDSInc}$. Recall, given DS automata
$P$ and $Q$, discount factor $d=1+2^{-k}$ and approximation factor $2^{-p}$,
$\mathsf{lowApproxDSInc}$ returns either $P\subseteq Q=\mathsf{False}$ or
$P\subseteq Q+d\cdot\varepsilon=\mathsf{True}$. In cases where both outcomes
are possible, $\mathsf{lowApproxDSInc}$ may return either of the outcomes. In
our design of $\mathsf{lowApproxDSInc}$, it performs
$\mathsf{DSLow}$-inclusion between the DS automaton, as justified in Lemma
7.5\- 7.6. Subsequently, the algorithm uses the regular comparator for
$\mathsf{DSLow}$ to design its inclusion procedure (Algorithm 5). Lastly, we
illustrate a property of $\mathsf{lowApproxDSInc}$ that is necessary in our
anytime procedure for DS inclusion to become co-recursively enumerable
(Theorem 7.6).

Terminology: A run $\rho_{P}$ of word $w$ in $P$ is said to be dominated by
$Q$ if there exists a run $\rho_{Q}$ in $Q$ on the same word such that
$\mathsf{DSLow}(\rho_{P}-\rho_{Q},k,p)\leq 0$.

###### Lemma 7.5

Given DS automata $P$ and $Q$, discount factor $d=1+2^{-k}$ and approximation
factor $\varepsilon=2^{-p}$ for rational values $k,p>0$.

  1. 1.

If all runs in $P$ are dominated by $Q$, then $P\subseteq Q+d\cdot\varepsilon$
holds.

  2. 2.

If there exists a run in $P$ that is not dominated by $Q$, then $P\subseteq Q$
does not hold.

###### Proof 54

Proof of (1.): Let for all words $w\in\Sigma^{*}$, for all runs of $w$
$\rho_{P}\in P$, there exists a run of $w$ $\rho_{Q}\in Q$ such that
$\mathsf{DSLow}(\rho_{P}-\rho_{Q},k,p)\leq 0$ be true. Then
$\mathsf{DSLow}(\rho_{P}-\rho_{Q},k,p)\leq 0$ implies that
$\mathit{DS}({\rho_{P}-\rho_{Q}},{d})\leq
d\cdot\varepsilon\equiv\mathit{DS}({\rho_{P}},{d})\leq\mathit{DS}({\rho_{Q}},{d})+d\cdot\varepsilon$.
Since weight of a word is given by the maximum weight of its all runs, we get
that for all word $w\in\Sigma^{*}$,
$\mathit{wt}_{P}(w)<\mathit{wt}_{Q}(w)+d\cdot\varepsilon$. Therefore,
$P\subseteq Q+d\cdot\varepsilon$ holds.

Proof of (2.): Let $w\in\Sigma^{*}$ be the word for which there exists a run
of $w$ $\rho_{P}\in P$ such that for all runs of $w\rho_{Q}\in Q$,
$\mathsf{DSLow}(\rho_{P}-\rho_{Q},k,p)>0$ holds.
$\mathsf{DSLow}(\rho_{P}-\rho_{Q},k,p)>0$ implies
$\mathit{DS}({\rho_{P}-\rho_{Q}},{d})>0\equiv\mathit{DS}({\rho_{P}},{d})>\mathit{DS}({\rho_{Q}},{d})$.
Since weight of a word is given by the maximum weight of its all runs, we get
that there exists word $w\in\Sigma^{*}$,
$\mathit{wt}_{P}(w)>\mathit{wt}_{Q}(w)$. So, $P\subseteq Q$ does not hold. ∎

Therefore, $\mathsf{lowApproxDSInc}(P,Q,d,\varepsilon)$ is designed such that
it returns $\mathsf{True}$ iff all runs in $P$ are dominated by $Q$. To attain
this, we construct NFA $\mathsf{dominated}$ in Algorithm 5 so that it contains
all runs in $P$ that are dominated by $Q$. This construction utilizes the
comparator automata for lower DS. Lastly, language inclusion between
$\mathsf{dominated}$ and NFA $\hat{P}_{-wt}$, that consists of all runs of
$P$, determines if all runs of $P$ are dominated or not. Recall, currently we
assume all weights in the DS automata are non-negative integers. As a result,
the upper bound for comparator construction is set to $\mu$, where $\mu>0$ is
the maximum weight along all transitions in both DS automata. In case the
weights along transitions are non-negative, then the comparator will be
constructed with upper bound $2\cdot\mu>0$, where $\mu$ is the maximum of
absolute values of weight along all transitions in both DS automata. The rest
will be identical.

###### Algorithm Details

For DS automaton $P$, procedure $\mathsf{AugmentWtAndLabel}(P)$ generates an
NFA $\hat{P}$ by converting transition $s\xrightarrow{a}t$ with weight $wt$
and unique transitions label $l$ in $P$ to a transition
$s\xrightarrow{a,wt,l}t$ in $\hat{P}$ (Line 1). Procedure
$\mathsf{productDif}(\hat{P},Q)$ generates the product of NDA $\hat{P}$ with
DS automaton $Q$ in an NDA $\hat{P}-Q$ such that it also records the
difference of weight of transitions. Therefore, if
$s\xrightarrow{a,wt_{1},l}t$ and $p\xrightarrow{a}q$ with weight $wt_{2}$ are
transitions in $\hat{P}$ and $Q$, respectively, then
$(s,p)\xrightarrow{a,wt_{1}-wt_{2},l}(t,q)$ is a transition in $\hat{P}-Q$.
All states in NFA $\hat{P}-Q$ are accepting states. From § 7.4.1 we know that
$\mathsf{approxDSComp}$ is the comparator for lower approximation of DS with
upper bound $\mu$, discount factor $d$, approximation factor $\varepsilon$ and
relation $\leq$. NDA $\mathsf{dominatedWitness}$ forms the intersection of
$\hat{P}-Q$ with the comparator by matching the weight-component in
$\hat{P}-Q$ with the weight-alphabet in the comparator. Therefore, if
$s\xrightarrow{a,wt,l}t$ and $p\xrightarrow{wt}q$ are transitions in
$\hat{P}-Q$ and the comparator, respectively, then
$(s,p)\xrightarrow{a,wt,l}(t,q)$ is a transition in the intersection.
Furthermore, a state $(r,s)$ is accepting iff both $r$ and $s$ are accepting
states in their respective NFA. Finally, $\mathsf{dominated}$ and
$\hat{P}_{-wt}$ are obtained by projecting out the weight component from
$\mathsf{dominatedWitness}$ and $\hat{P}$, respectively. Specifically, if
$s\xrightarrow{a,wt,l}t$ is a transition in the original automaton, then
$s\xrightarrow{a,l}t$ is a transition in the final automata. Here,
$\hat{P}_{wt}\subseteq\mathsf{dominated}$ refers to language inclusion between
the two NFAs.

Algorithm 5 $\mathsf{lowApproxDSInc}(P,Q,d,\varepsilon)$
Inputs: DS automata $P$, $Q$, discount factor $1<d<2$, approximation factor
$0<\varepsilon<1$

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

2: $\hat{P}-{Q}\leftarrow\mathsf{productDif}(\hat{P},{Q})$

3:
$\mathsf{dominatedWitness}\leftarrow\textsf{Intersect}(\hat{P}-{Q},\mathsf{compLow}(\mu,\log\frac{1}{d-1},\log\frac{1}{\varepsilon},\leq))$,
where $\mu$ is the maximum of the absolute value of weights in $\hat{P}-{Q}$

4: $\mathsf{dominated}\leftarrow\textsf{Project}(\mathsf{dominatedWitness})$

5:
$\mathsf{aux}\leftarrow\hat{P}_{-wt}\subseteq_{\mathsf{LI}}\mathsf{dominated}$
// $\subseteq_{\mathsf{LI}}$ refers to Language inclusion

6: if $\mathsf{aux}$ then

7: return $P\subseteq Q+d\cdot\varepsilon=\mathsf{True}$

8: else

9: return $P\subseteq Q=\mathsf{False}$

10: end if

###### Lemma 7.6

Given DS automata $P$ and $Q$, discount factor $d=1+2^{-k}$ and approximation
factor $\varepsilon=2^{-p}$ for rational values $k,p>0$,
$\mathsf{lowApproxDSInc}(P,Q,d,\varepsilon)$ returns $\mathsf{True}$ iff all
runs in $P$ are dominated by $Q$.

###### Proof 55

From the algorithm, it is clear that there is a one-one correspondence between
words $(w,L)\in\hat{P}_{-wt}$ and runs $\rho_{P}$ of word $w$ in $P$ for all
words $w\in\Sigma^{*}$.

From the algorithm, it is also clear that $(w,L)\in\mathsf{dominated}$ iff
$w\in\Sigma^{*}$, with a run $\rho_{P}\in P$ which has been labelled by $L$
such that there exists a run $\rho_{Q}\in Q$ of $w$ such that
$\mathsf{DSLow}(\rho_{P}-\rho_{Q},k,p)\leq 0$.

Then $\mathsf{aux}==\mathsf{True}$ iff
$\hat{P}_{-wt}\subseteq\mathsf{dominated}$. By definition of language
inclusion, this holds iff for all $(w,L)\in\hat{P}_{-wt}$ we get that
$(w,L)\in\mathsf{dominated}$. From the one-one correspondence between words in
$\hat{P}_{-wt}$ and runs in $P$, we get that for all $w\in\Sigma^{*}$, for all
runs $\rho_{P}\in P$ of $w$, let $(w,L)$ be its correspondence in
$\hat{P}_{-wt}$ then $(w,L)\in\mathsf{dominated}$. By the condition under
which a word is a member of $\mathsf{dominated}$ we get that $w\in\Sigma^{*}$,
for all runs $\rho_{P}\in P$ of $w$, such that there exists a run $\rho_{Q}\in
Q$ of $w$ such that $\mathsf{DSLow}(\rho_{P}-\rho_{Q},k,p)\leq 0$. ∎

###### Theorem 7.4

[ Soundness] For all inputs DS automata $P$ and $Q$, discount factor
$d=1+2^{-k}$ and approximation factor $\varepsilon=2^{-p}$ for rational values
$k,p>0$, algorithm $\mathsf{lowApproxDSInc}$ is sound.

###### Proof 56

This follows directly from Lemma 7.5 and Lemma 7.6. ∎

###### Theorem 7.5

[Complexity] Given DS automata $P$ and $Q$, discount factor $d=1+2^{-k}$ and
approximation factor $\varepsilon=2^{-p}$ for rational values $k,p>0$. Let
$\mu$ be the absolute value of the largest weight in $P$ and $Q$. Then the
worst case complexity of $\mathsf{lowApproxDSInc}$ is $2^{\mathcal{O}(n)}$
where $n=|P|\cdot|Q|\cdot\frac{\mu}{(d-1)^{2}\cdot\varepsilon}$.

###### Proof 57

The size of $\mathsf{dominated}$ is
$\mathcal{O}(|P|\cdot|Q|\cdot\mathsf{compLow(\mu,\log(\frac{1}{d-1}),\log(\frac{1}{\varepsilon}))})$,
which is equal to
$\mathcal{O}(|P|\cdot|Q|\cdot\frac{\mu}{(d-1)^{2}\cdot\varepsilon})$. Then,
the complexity of $\hat{P}_{-wt}\subseteq\mathsf{dominated}$ is $|P|\cdot
2^{\mathcal{O}(|P|\cdot|Q|\cdot\frac{\mu}{(d-1)^{2}\cdot\varepsilon})}$. This
equates to
$2^{\mathcal{O}(|P|\cdot|Q|\cdot\frac{\mu}{(d-1)^{2}\cdot\varepsilon}+\log(|P|)}$.
Keeping the dominating terms in the exponent, we get the worst-case complexity
to be
$2^{\mathcal{O}(|P|\cdot|Q|\cdot\frac{\mu}{(d-1)^{2}\cdot\varepsilon})}$. ∎

Lastly, we show that if $P\subseteq Q$ does not hold, there exists a
sufficiently small approximation factor $\varepsilon>0$ such that when
$\mathsf{lowApproxDSInc}$ is invoked with $\varepsilon$, it returns that
$P\subseteq Q$ does not hold. This property will be crucial in proving co-
recursive enumerability of our anytime procedure for DS inlcusion.

######  Theorem 7.6 (Bias)

Given DS automata $P$, $Q$, and discount factor $1<d<2$. If $P\subseteq
Q=\mathsf{False}$, there exists an approximation factor $0<\varepsilon<1$ such
that for all $0<\gamma<\varepsilon$, $\mathsf{lowApproxDSInc}(P,Q,d,\gamma)$
returns $P\subseteq Q=\mathsf{False}$.

###### Proof 58

The core idea is that when $P\subseteq Q$ does not hold, then there must exist
a word $w\in\Sigma^{*}$ such that
$\mathit{wt}(w,P)>\mathit{wt}(w,Q)+d\cdot\delta$. Therefore, for a
sufficiently low value of $\varepsilon$, $P\subseteq
Q+d\cdot\varepsilon=\mathsf{False}$. Then, for these values of $\varepsilon$,
$\mathsf{lowApproxDSInc}$ will necessarily return $P\subseteq
Q=\mathsf{False}$.

Since $P\subseteq Q=\mathsf{False}$ there exists a word $w\in\Sigma^{*}$ such
that $\mathit{wt}(w,P)=\mathit{wt}(w,Q)+d\cdot\gamma$ for a rational value
$\gamma>0$. Since weight of words is computed as the maximum of weight of its
runs, there must exist a run $\rho_{P}$ of $w$ in $P$ such that for all runs
$\rho_{Q}$ of $w$ in $Q$, we get that such that
$\mathit{DS}({\rho_{P}},{d})-\mathit{DS}({\rho_{Q}},{d})>d\cdot\gamma=\mathit{DS}({\rho_{P}-\rho_{Q}},{d})>d\cdot\gamma$.
Let $k,p>0$ be rational values such that $d=1+2^{-k}$ and $\gamma=2^{-p}$.
From Theorem 7.2, we get that for all $q\geq p+1$
$\mathsf{DSLow}(\rho_{P}-\rho_{Q},k,q)>d\cdot\frac{\gamma}{2}$. Therefore,
from Lemma 7.5 we get that for all $q\geq p+1$,
$\mathsf{lowApproxDSInc}(P,Q,d,q)=\mathsf{False}$. ∎

####  7.5 Algorithm $\mathsf{upperApproxDSInc}$

This section describes Algorithm $\mathsf{upperApproxDSInc}$ \- the second
sub-procedures in our anytime algorithm for DS inclusion. Given inputs DS
automata $P$ and $Q$, discount factor $1<d<2$ and approximation factor
$0<\varepsilon<1$, $\mathsf{upperApproxDSInc}$ $(P,Q,d,\varepsilon)$ either
returns $P\subseteq Q$ holds or $P\subseteq Q-d\cdot\varepsilon$ does not
hold. As earlier, these outcomes are not mutually exclusive. In these cases,
the algorithm may return either of the outcomes as they are both sound.

The design of $\mathsf{upperApproxDSInc}$ follows that of
$\mathsf{lowApproxDSInc}$ very closely. Intuitively,
$\mathsf{upperApproxDSInc}$ solves whether $P$ is $f$-included in $Q$ where
aggregate function $f$ is the upper approximation of discounted-sum. Notice
how similar this is to the intuition behind $\mathsf{lowApproxDSInc}$. As a
result, $\mathsf{upperApproxDSInc}$ follows the same three stages as earlier:
(a). Define the upper approximation of discounted-sum, (b). Construct its
regular comparator, and (c). Use the regular comparator to design
$\mathsf{upperApproxDSInc}$. Each of these individual steps are very similar
to those in the previous section. As a result, the critical distinctions are
highlighted first, and then the details are given. One may skip the details to
avoid repetition. The details are mentioned here for sake of completeness.

The first distinction is in the definition of the upper approximation of
discounted. It is similar to that of the lower approximation for DS except
that it makes use of an upper gap. In turn, the upper gap of a value is
defined similar to the lower gap except that the upper gap is rounded-off to
the smallest multiple of $2^{-(p+k)}$ that is greater than or equal to the
value, where $p$ and $k$ are defined as earlier. Using a similar vein of
reasoning as in § 7.4.2, the comparator for the upper approximation can also
be constructed. Second, algorithm $\mathsf{upperApproxDSInc}$ is almost
identical to $\mathsf{lowApproxDSInc}$ in Algorithm 5 except that in Line 3
algorithm $\mathsf{upperApproxDSInc}$ constructs the regular comparator for
the upper approximation of discounted sum.

Yet, another important distinction between $\mathsf{lowApproxDSInc}$ and
$\mathsf{upperApproxDSInc}$ is that if $P\subseteq Q=\mathsf{True}$ holds,
then $\mathsf{upperApproxDSInc}$ cannot guarantee that for a small enough
value of the approximation factor $\mathsf{upperApproxDSInc}$ with return
$P\subseteq Q=\mathsf{True}$. The core idea here is that if $P\subseteq
Q=\mathsf{True}$ then the difference between words in $P$ and in $Q$ could be
arbitrarily small. In particular, for every possible value of the
approximation factor, there may be a word for which the difference in its
weight in $P$ and $Q$ is smaller than the approximation factor. As a result,
the option of $P\subseteq Q-d\cdot\varepsilon=\mathsf{False}$ may get
triggered, never returning the outcome that $P\subseteq Q=\mathsf{True}$
holds.

The rest of this section gives all details of $\mathsf{upperApproxDSInc}$.

#####  7.5.1 Upper approximation of discounted-sum

In the first stage we define the upper approximation of discounted-sum so that
its recoverable gap obeys the bounded non-zero minimal difference property.

For a rational number $x\in\mathbb{Q}$, let $\mathsf{roundUpper}(x,k,p)$
denote the smallest integer multiple of resolution that is more than or equal
to $x$. Formally, $\mathsf{roundUpper}(x,k,p)=i\cdot 2^{-(p+k)}$ for an
integer $i\in\mathbb{Z}$ such that for all $j\in\mathbb{Z}$, $j\cdot
2^{-(p+k)}\geq x$ implies $i\leq j$. The upper gap value and upper
approximation of discounted sum are defined as follows:

###### Lemma 7.7

Let $k,p>0$ be rational-valued parameters. Then, for all real values
$x\in\mathbb{R}$, $0\leq\mathsf{roundUpper}(x,k,p)-x<2^{-(p+k)}$.

###### Proof 59

There exists a unique integer $i\in\mathbb{Z}$ and $0\leq b<2^{-(p+k)}$ such
that $x=i\cdot 2^{-(p+k)}-b$. Then, $\mathsf{roundUpper}(x,k,p)=i\cdot
2^{-(p+k)}$. Therefore, we get that
$0\leq\mathsf{roundUpper}(x,k,p)-x<2^{-(p+k)}$. ∎

######  Lemma 7.8 (Monotonicity)

Let $k,p>0$ be rational-valued parameters. Then, if $x\geq y$, then
$\mathsf{roundLow}(x,k,p)\geq\mathsf{roundLow}(y,k,p)$.

###### Proof 60

The proof of this is very similar to that of Lemma 7.2. ∎

######  Definition 7.7 (Upper gap)

Let $W$ be a finite weight sequence. The upper gap of $W$ with discount factor
$d=1+2^{-k}$ and approximation factor $\varepsilon=2^{-p}$, denoted
$\mathsf{gapUpper}(W,k,p)$, is

$\mathsf{gapUpper}(W,k,p)=\begin{cases}0,\text{ for }|W|=0\\\
\mathsf{roundUpper}(\mathsf{gapUpper}(U,k,p)+u,k,p)\text{ for }W=U\cdot
u\end{cases}$

######  Definition 7.8 (Upper approximation of discounted-sum)

Let $W$ be a finite weight sequence. The upper approximation of discounted
sum, called upper DS, for weight sequence $W$ with discount factor
$d=1+2^{-k}$ and approximation factor $\varepsilon=2^{-p}$ is denoted by and
defined as

$\mathsf{DSUpper}(W,k,p)=\mathsf{gapUpper}(W,k,p)/d^{|W|-1}$

Definition 7.8 is completed by showing the it indeed corresponds to an upper
approximation of discounted sum. This requires a basic lemma statement:

###### Lemma 7.9

Let $k,p>0$ be rational-valued parameters. Let $d=1+2^{-k}$ be the non-
integer, rational discount factor and $\varepsilon=2^{-p}$ be the
approximation factor. Let $W$ be a finite non-empty weight sequence. Then
$0\leq\mathsf{gapUpper}(W,k,p)-\mathsf{gap}(W,d)<\mathsf{gap}(R_{|W|},d)$.

###### Proof 61

The proof argument follows by induction on length of weight sequence $W$. It
makes use of Lemma 7.7 and Lemma 7.8, and closely follows the proof presented
in Lemma 7.3. ∎

###### Theorem 7.7

Let $d=1+2^{-k}$ be the discount factor and $\varepsilon=2^{-p}$ be the
approximation factor, for rationals $p,k>0$. Then for all weight sequences
$W$, $0\leq\mathsf{DSUpper}(W,k,p)-\mathit{DS}({W},{d})<d\cdot\varepsilon$.

###### Proof 62

The proof argument makes use of Lemma 7.9 and closely follows that of Theorem
7.2. ∎

#####  7.5.2 Comparator automata for upper approximation of DS

This section constructs a regular comparator for the upper DS defined above.
The construction here differs from that of the comparator for lower DS in only
one aspect - the values of the thresholds within which it is sufficient to
track the value of upper gap in. In this section, we define the comparison
language and its comparator automata, prove the necessary thresholds and give
the complete construction of the comparator.

######  Definition 7.9 (Comparison language for upper approximation of DS)

Let $\mu>0$ be an integer bound, and $k,p$ be positive rationals. The
comparison language for upper approximation of discounted sum with discount
factor $d=1+2^{-k}$, approximation factor $\varepsilon=2^{-p}$, upper bound
$\mu$ and inequality relation $\mathsf{R}\in\\{\leq,\geq\\}$ is a language
that accepts bounded and finite weight sequence $W\in\Sigma^{*}$ iff
$\mathsf{DSUpper}(W,k,p)$ $\mathsf{R}$ $0$ holds.

######  Definition 7.10 (Comparator automata for upper approximation of DS)

Let $\mu>0$ be an integer bound, and $k,p$ be positive rationals. The
comparator automata for upper approximation of discounted sum with discount
factor $d=1+2^{-k}$, approximation factor $\varepsilon=2^{-p}$, upper bound
$\mu$ and inequality relation $\mathsf{R}\in\\{\leq,\geq\\}$ is an automaton
that accepts the corresponding comparison language.

We establish the range of sufficient values for the upper gap. The new bounds
are as follows:

###### Lemma 7.10

Let $\mu>0$ be an integer bound. Let $k,p$ be positive rationals s.t.
$d=1+2^{-k}$ is the discount factor, and $\varepsilon=2^{-p}$ is the
approximation factor. Let $W$ be a finite and bounded weight sequence.

  1. 1.

If $\mathsf{gapUpper}(W,k,p)\leq-\mu\cdot 2^{k}-2^{-p}$ then for all
$u\in\\{-\mu,\dots,\mu\\}$, $\mathsf{gapUpper}(W\cdot u,k,p)\leq-\mu\cdot
2^{k}-2^{-p}$.

  2. 2.

If $\mathsf{gapUpper}(W,k,p)\geq\mu\cdot 2^{k}$, then for all
$u\in\\{-\mu,\dots,\mu\\}$, $\mathsf{gapUpper}(W\cdot u,k,p)\geq\mu\cdot
2^{k}$.

###### Proof 63

Part 1. Let $W$ and $u$ be as defined above. Then $\mathsf{gapUpper}(W\cdot
u,k,p)=\mathsf{roundUpper}(d\cdot\mathsf{gapUpper}(W,k,p)+u,k,p)$. From Lemma
7.7, we get that $\mathsf{gapUpper}(W\cdot u,k,p)\leq
d\cdot\mathsf{gapUpper}(W,k,p)+u+2^{-(p+k)}$. From our assumption, we further
get that $\mathsf{gapUpper}(W\cdot u,k,p)\leq d\cdot-(\mu\cdot
2^{k}+2^{-p})+u=(1+2^{-k})\cdot-(\mu\cdot 2^{k}+2^{-p})+u+2^{-(p+k)}=-\mu\cdot
2^{k}-\mu-2^{-p}-2^{-(p+k)}+u+2^{-(p+k)}\leq-(\mu\cdot 2^{k}+2^{-p})$.

Part 2. Let $W$ and $u$ be as defined above. Then $\mathsf{gapUpper}(W\cdot
u,k,p)=\mathsf{roundUpper}(d\cdot\mathsf{gapUpper}(W,k,p)+u,k,p)$. From Lemma
7.7, we get that $\mathsf{gapUpper}(W\cdot u,k,p)\geq
d\cdot\mathsf{gapUpper}(W,k,p)+u$. Further, from our assumptions we get that
$\mathsf{gapUpper}(W\cdot u,k,p)\geq d\cdot\mu\cdot
2^{k}+u=(1+2^{-k})\cdot\mu\cdot 2^{k}+u=\mu\cdot 2^{k}+\mu+u\geq\mu\cdot
2^{k}$, since $\mu\geq u$. ∎

###### Construction

Let $\mu>0$, $d=1+2^{-k}$, $\varepsilon=2^{-p}$ be the upper bound, discount
factor and approximation factor, respectively. Let $\mathsf{T}_{l}$ be the
largest integer such that $\mathsf{T}_{l}\cdot 2^{-(p+k)}\leq-\mu\cdot 2^{k}$.
Let $\mathsf{T}_{u}$ be the smallest integer such that $\mathsf{T}_{u}\cdot
2^{-(p+k)}\geq\mu\cdot 2^{k}+2^{-p}$. Note, the thresholds are from Lemma
7.10. For relation $\mathsf{R}\in\\{\leq,\geq\\}$, construct DFA
$\mathsf{compUpper}(\mu,k,p,\mathsf{R})=(S,s_{I},\Sigma,\delta,\mathcal{F})$
as follows:

  * •

$S=\\{\mathsf{T}_{l},\mathsf{T}_{l}+1,\dots,\mathsf{T}_{u}\\}$,
$s_{I}=\\{0\\}$ and $\mathcal{F}=\\{i|i\in S\text{ and $i$ $R$ $0$}\\}$

  * •

Alphabet $\Sigma=\\{-\mu,-\mu+1,\dots,\mu-1,\mu\\}$

  * •

Transition function $\delta\subseteq S\times\Sigma\rightarrow S$ where
$(s,a,t)\in\delta$ then:

    1. 1.

If $s=\mathsf{T}_{l}$ or $s=\mathsf{T}_{u}$, then $t=s$ for all $a\in\Sigma$

    2. 2.

Else, let $\mathsf{roundUpper}(d\cdot s\cdot 2^{-(p+k)}+a,k,p)=i\cdot
2^{-(p+k)}$ for an integer $i$

      1. (a)

If $\mathsf{T}_{l}\leq i\leq\mathsf{T}_{u}$, then $t=i$

      2. (b)

If $i>{\mathsf{T}_{h}}$, then $t=\mathsf{T}_{u}$

      3. (c)

If $i<{\mathsf{T}_{l}}$, then $t=\mathsf{T}_{l}$

###### Theorem 7.8

Let $\mu>0$ be and integer upper bound. Let $k,p>0$ be rational parameters
s.t. $d=1+2^{-k}$ is the discount factor and $\varepsilon=2^{-p}$ is the
approximation parameter. DFA $\mathsf{compUpper}(\mu,k,p,\mathsf{R})$ accepts
a finite weight sequence $W\in\Sigma^{*}$ iff $\mathsf{DSUpper}(W,k,p)$
$\mathsf{R}$ $0$. DFA $\mathsf{compUpper}(\mu,k,p,\mathsf{R})$ has
$\mathcal{O}(\mu\cdot 2^{2k+p})$ states.

#####  7.5.3 Algorithm $\mathsf{upperApproxDSInc}$

This section utilizes the comparator for upper approximation of DS to describe
$\mathsf{upperApproxDSInc}$ (Algorithm 6). Recall, given inputs $P$, $Q$,
discount factor $1<d<2$ and approximation factor $0<\varepsilon<1$,
$\mathsf{upperApproxDSInc}(P,Q,d,\varepsilon)$ returns $P\subseteq Q$ holds or
$P\subseteq Q-d\cdot\varepsilon$ does not hold.

Once again, the intuition and algorithm design fo $\mathsf{upperApproxDSInc}$
resembles that of $\mathsf{lowApproxDSInc}$. Intuitively,
$\mathsf{upperApproxDSInc}$ solves whether $P$ is $f$-included in $Q$ where
aggregate function $f$ is the upper approximation of discounted-sum. Lemma
7.11 precisely states the intuition, and the algorithm is given in Algorithm
6.

We begin with formalizing the intuition. We say, a run $\rho_{P}$ of word $w$
in $P$ is dominated by $Q$ if there exists a run $\rho_{Q}$ in $Q$ on the same
word such that $\mathsf{DSUpper}(\rho_{P}-\rho_{Q},k,p)\leq 0$. Then,

###### Lemma 7.11

Given DS automata $P$ and $Q$, discount factor $d=1+2^{-k}$ and approximation
factor $\varepsilon=2^{-p}$ for rational values $k,p>0$.

  1. 1.

If all runs in $P$ are dominated by $Q$, then $P\subseteq Q$ holds.

  2. 2.

If there exists a run in $P$ that is not dominated by $Q$, then $P\subseteq
Q-d\cdot\varepsilon$ does not hold.

###### Proof 64

Proof of (1.) Let for all words $w\in\Sigma^{*}$, for all runs of $w$ in
$\rho_{P}\in P$, there exists a run of word $w$ $\rho_{Q}\in Q$ such that
$\mathsf{DSUpper}(\rho_{P}-\rho_{Q},k,p)\leq 0$ implies that
$\mathit{DS}({\rho_{P}-\rho_{Q}},{d})\leq 0$. By arguing as in Lemma 7.5, we
get that $P\subseteq Q$.

Proof of (2.) Let $w\in\Sigma*$ be a word for which there exists a run of
$w\rho_{P}\in P$ such that for all runs of $w$ $\rho_{Q}\in Q$,
$\mathsf{DSUpper}(\rho_{P}-\rho_{Q},k,p)>0$ implies
$\mathit{DS}({\rho_{P}-\rho_{Q}},{d})>-d\cdot\varepsilon$. Therefore, by
arguing as done in Lemma 7.5, we get that $P\subseteq Q-d\cdot\varepsilon$
does not hold. ∎

Algorithm 6 $\mathsf{upperApproxDSInc}(P,Q,d,\varepsilon)$
Inputs: DS automata $P$, $Q$, discount factor $1<d<2$, approximation factor
$0<\varepsilon<1$

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

2: $\hat{P}-{Q}\leftarrow\mathsf{productDif}(\hat{P},{Q})$

3:
$\mathsf{dominatedWitness}\leftarrow\textsf{Intersect}(\hat{P}-{Q},\mathsf{compUpper}(\mu,\log\frac{1}{(d-1)},\log\frac{1}{\varepsilon},\leq))$
where $\mu$ is the maximum of the absolute value of weights in $\hat{P}-{Q}$

4: $\mathsf{dominated}\leftarrow\textsf{Project}(\mathsf{dominatedWitness})$

5: $\hat{P}_{-wt}\subseteq\mathsf{dominated}$

6: if $\mathsf{aux}$ then

7: return $P\subseteq Q=\mathsf{True}$

8: else

9: return $P\subseteq Q-d\cdot\varepsilon=\mathsf{False}$

10: end if

We design Algorithm 6 so that it resembles Algorithm 5 except that in this
case the comparator refers to that of the upper approximation of discounted-
sum:

###### Lemma 7.12

Given DS automata $P$ and $Q$, discount factor $d=1+2^{-k}$ and approximation
factor $\varepsilon=2^{-p}$ for rational values $k,p>0$,
$\mathsf{upperApproxDSInc}(P,Q,d,\varepsilon)$ returns $\mathsf{True}$ iff all
runs in $P$ are dominated by $Q$.

###### Proof 65

The proof argument is similar to that in Lemma 7.6. ∎

######  Theorem 7.9 (Soundness)

For all inputs DS automata $P$ and $Q$, discount factor $d=1+2^{-k}$ and
approximation factor $\varepsilon=2^{-p}$ for rational values $k,p>0$,
algorithm $\mathsf{upperApproxDSInc}$ is sound.

###### Proof 66

The proof is similar to proof that Theorem 7.4. ∎

######  Theorem 7.10 (Complexity)

Given DS automata $P$ and $Q$, discount factor $d=1+2^{-k}$ and approximation
factor $\varepsilon=2^{-p}$ for rational values $k,p>0$. Let $\mu$ be the
absolute value of the largest weight in $P$ and $Q$. Then the worst case
complexity of $\mathsf{upperApproxDSInc}$ is $2^{\mathcal{O}(n)}$ where
$n=|P|\cdot|Q|\cdot\frac{\mu}{(d-1)^{2}\cdot\varepsilon}$.

###### Proof 67

The proof is similar to that of Theorem 7.5. ∎

####  7.6 Anytime algorithm for DS inclusion

This section describes the core contribution of this work. We design an
anytime algorithm for discounted-sum inclusion. On inputs DS automata $P$ and
$Q$, and discount factor $1<d<2$, our algorithm $\mathsf{DSInclusion}(P,Q,d)$
either terminates and returns a crisp $\mathsf{True}$ or $\mathsf{False}$
answer to $P\subseteq Q$, or it establishes a $d\cdot\varepsilon$-close
approximation, where the approximation factor $\varepsilon>0$ decreases with
time. In addition, algorithm $\mathsf{DSInclusion}$ is co-computational
enumerable i.e. if $P\subseteq Q$ does not hold then
$\mathsf{DSInclusion}(P,Q,d)$ is guaranteed to terminate with that outcome
after a finite amount of time.

This section proves soundness, and co-computational enumerability of
$\mathsf{DSInclusion}$. Finally, we evaluate the complexity of running
$\mathsf{DSInclusion}$ upto a desired approximation (Theorem 7.13). The
analysis reveals that as $\varepsilon$ tends to 0, the worst-case complexity
grows rapidly.

###### Algorithm details

$\mathsf{DSInclusion}$ invokes $\mathsf{anytimeInclusion}$ with an initial
approximation factor $0<\varepsilon_{\textsf{init}}<1$, where
$\mathsf{anytimeInclusion}$ is described in Algorithm 4. Here
$\varepsilon_{\textsf{init}}=\frac{1}{2}$. Formally,
$\mathsf{DSInclusion}(P,Q,d)=\mathsf{anytimeInclusion}(P,Q,d,0.5)$ Recall,
Algorithm 4 is a tail recursive procedure in which subprocedures
$\mathsf{lowApproxDSInc}$ and $\mathsf{upperApproxDSInc}$ are invoked in each
round of the recursion. If the current round of recursion is invoked with
approximation factor $\varepsilon>0$, then $\mathsf{lowApproxDSInc}$ and
$\mathsf{upperApproxDSInc}$ are invoked with $\varepsilon$. In this round, if
$\mathsf{lowApproxDSInc}$ or $\mathsf{upperApproxDSInc}$ returns $P\subseteq
Q$ does not hold or $P\subseteq Q$ holds, respectively,
$\mathsf{anytimeInclusion}$ terminates. Otherwise, it invokes
$\mathsf{anytimeInclusion}$ with approximation factor $\frac{\varepsilon}{2}$.

In order to analyse $\mathsf{DSInclusion}$, we begin with some useful
terminology: $\mathsf{DSInclusion}(P,Q,d)$ is said to be in the
$\varepsilon$-th round when the current invocation of
$\mathsf{anytimeInclusion}$ occurs with approximation factor $\varepsilon$.
$\mathsf{DSInclusion}(P,Q,d)$ is said to terminate in the $\varepsilon$-th
round  if $\mathsf{anytimeInclusion}(P,Q,d,\varepsilon)$ returns a crisp
solution to DS inclusion in the $\varepsilon$-th round. Finally,
$\mathsf{DSInclusion}(P,Q,d)$ is said to terminate if there exists a
$\varepsilon>0$ such that it terminates in the $\varepsilon$-th round.

###### Theorem 7.11

[Soundness] Let $P$, $Q$ be DS automata, and $1<d<2$ be the discount factor.

  1. 1.

If $P$ is not DS-included in $Q$ and $\mathsf{DSInclusion}(P,Q,d)$ terminates,
then $\mathsf{DSInclusion}(P,Q,d)$ returns $P\subseteq Q=\mathsf{False}$

  2. 2.

If $P$ is DS-included in $Q$ holds and $\mathsf{DSInclusion}(P,Q,d)$
terminates, then $\mathsf{DSInclusion}(P,Q,d)$ returns $P\subseteq
Q=\mathsf{True}$

  3. 3.

If $\mathsf{DSInclusion}(P,Q,d)$ does not terminate in the $\varepsilon$-th
round in which the approximation factor is $\varepsilon>0$, then $P\subseteq
Q+d\cdot\varepsilon$ holds.

###### Proof 68

We reason about $\mathsf{anytimeInclusion}$ as that is sufficient.

Proof of (1.) and (2.): $\mathsf{anytimeInclusion}$ terminates only if either
$\mathsf{lowApproxDSInc}$ returns $P\subseteq Q=\mathsf{False}$ or
$\mathsf{upperApproxDSInc}$ returns $P\subseteq Q=\mathsf{True}$. Since each
of these subprocedures is individually sound (Theorem 7.4 and Theorem 7.9,
respectively), statements (1.) and (2.) hold.

Proof of (3.): $\mathsf{anytimeInclusion}$ does not terminate in the
$\varepsilon$-th round only if $\mathsf{lowApproxDSInc}$ and
$\mathsf{upperApproxDSInc}$ return $P\subseteq
Q+d\cdot\varepsilon=\mathsf{True}$ and $P\subseteq
Q-d\cdot\varepsilon=\mathsf{False}$, respectively. Therefore, by soundness of
$\mathsf{lowApproxDSInc}$ (Theorem 7.4), it holds that $P$ is
$d\cdot\varepsilon$-close to $Q$. ∎

Next, we prove that $\mathsf{DSInclusion}$ is co-computational enumerable.

######  Theorem 7.12 (Co-ce)

Let $P$, $Q$ be DS automata, and $1<d<2$ be the discount factor. If
$P\subseteq Q=\mathsf{False}$ then $\mathsf{DSInclusion}(P,Q,d)$ terminates
after a finite number of recursions. Upon termination,
$\mathsf{DSInclusion}(P,Q,d)$ returns $P\subseteq Q=\mathsf{False}$.

###### Proof 69

By soundness of $\mathsf{upperApproxDSInc}$, we know that
$\mathsf{upperApproxDSInc}$ will return $P\subseteq
Q-d\cdot\varepsilon=\mathsf{False}$ in every invocation. Hence,
$\mathsf{DSInclusion}$ cannot terminate due to $\mathsf{upperApproxDSInc}$.
Therefore, if $\mathsf{DSInclusion}$ terminates, it must be because
$\mathsf{lowApproxDSInc}$ returns $P\subseteq Q=\mathsf{False}$ for some
$\varepsilon>0$. It remains to show that such an approximation factor exists.
But that is exactly the result in Theorem 7.6. Therefore, if $P\subseteq
Q=\mathsf{False}$, then $\mathsf{DSInclusion}$ is guaranteed to terminate with
the outcome $P\subseteq Q=\mathsf{False}$. ∎

Note that we cannot determine, apriori, the number of recursive invocations
that will be conducted for a given input instance. If we could, then we could
have proved the decidability of discounted sum inclusion for discount factor
$1<d<2$. As a result, one cannot determine the worst-case complexity of
$\mathsf{DSInclusion}$ in general. However, the worst-case complexity can be
computed upto a certain precision. More precisely, if a user decides that it
will run $\mathsf{DSInclusion}$ until either it terminates with a crisp
solution or $d\cdot\varepsilon_{c}$-close approximation is established, where
approximation factor $\varepsilon_{c}$ is pre-determined. Note that it is not
sufficient to recursively only invoke $\mathsf{lowApproxDSInc}$ till the
approximation factor is $\varepsilon_{c}$ since then we would never be able to
generate the outcome that DS inclusion holds. The worst-case complexity upto
$\varepsilon_{c}$ is computed as follows:

######  Theorem 7.13 (Complexity given precision)

Given DS automata $P$ and $Q$, discount factor $1<d<2$. Let $\mu$ be the
largest weight in $P$ and $Q$. Let $0<\varepsilon_{\mathsf{c}}<1$ be the
desired precision. Then, the worst-case complexity of solving DS inclusion
upto a precision of $\varepsilon_{\mathsf{c}}$ is $2^{\mathcal{O}(n)}$ where
$n=|P|\cdot|Q|\cdot\frac{\mu}{(d-1)^{2}}\cdot\log(\frac{1}{\varepsilon_{c}})$

###### Proof 70

Without loss of generality, let $\varepsilon_{c}=2^{-m}$ for$m\in\mathbb{N}$.
Then in the worst case, $\mathsf{DSInclusion}$ will terminate after invoking
$\mathsf{anytimeInclusion}$ with $\varepsilon_{c}$. The worst case complexity
of $\mathsf{DSInclusion}$ with precision $\varepsilon_{c}$ is calculate by
taking the sum of the complexity of each invocation of
$\mathsf{anytimeInclusion}$ till that point. The calculation evaluates to the
expression in the statement. ∎

So, as $\varepsilon_{\mathsf{c}}$ converges to 0, i.e, DS inclusion is solved
exactly, the worst-case complexity explodes rapidly. This renders a
quantitative measure of the difficulty of solving DS inclusion. Although this
isn’t concrete evidence for undecidability of DS inclusion, it certainly
points in that direction. Finally, if $d=1$, DS inclusion would be the same as
sum. Then the above evaluation corroborates the known undecidability of
quantitative inclusion with sum [11].

####  7.7 Chapter summary

This chapter investigates DS inclusion when the discount factor $1<d<2$ is not
an integer. The decidability of this problem has been open for more that a
decade now. So, this chapter focuses on designing solutions for DS inclusion
that could be used in practice despite its decidability being unknown. To this
effect, we design an anytime algorithm for DS inclusion. The algorithm may not
always solve the problem exactly. In these cases, it will generate an
approximate result, which is a meaningful outcome in practice. To the best of
our knowledge, this is the first attempt to solve DS inclusion with non-
integer discount factors for practical purposes. While this chapter looks into
DS inclusion over finite words, we believe the same ideas can be extended to
DS inclusion over infinite words. Our algorithm design is motivated by
designing regular comparator automata for approximations of DS with non-
integer discount factors. Thus, not only are comparators able to design
scalable solutions when the discount factor is an integer, as shown in Chapter
6, they also makes algorithmic advances for non-integer discount factors.

##  Part III Quantitative games with discounted-sum

###  Chapter 8 On the analysis of quantitative games

This part continues the investigation of automata-based quantitative reasoning
by studying their impact on quantitative games. We show that even here,
comparator automata delivers the benefits of scalability, efficiency, and
broader applicability.

####  8.1 Introduction

Quantitative properties of systems are increasingly being explored in
automated reasoning across diverse application areas, including software
verification [19, 66, 68], security [43, 56], computer-aided education [53],
and even verification of deep neural networks [22, 82]. In decision making
domains such as planning and reactive synthesis, quantitative properties have
been deployed to obtain high-quality solutions [29], describe hard and soft
constraints [69], constraints on cost and resource [58], and the like. In most
cases, planning and synthesis with quantitative properties is formulated into
an analysis problem over a two player, finite-state game arena with a cost
model that encodes the quantitative property [37].

Optimization over such games is a popular choice of analysis in literature.
Typically, optimization over these games has polynomial time algorithms.
However, the degree of polynomial may be too high to scale in practice;
resulting in limited applicability of the synthesis task at hand [30].
Furthermore, often times these synthesis tasks are accompanied with temporal
goals. Under this extension, the games are required to generate an optimal
solution while also satisfying the temporal objective. However, prior works
have proven that optimal strategies may not exist under extension with
temporal goals, rendering analysis by optimization incompatible with temporal
goals [41].

To this end, we propose an alternate form of analysis in which the objective
is to search for a solution that adheres to a given threshold constraint as
opposed to generating an optimal solution. We call this analysis the
satisficing problem, a well-established notion that we borrow from economics
[1]. Our argument is that in several cases optimal solutions may be replaced
with satisficing ones. For instance, a solution with minimal battery
consumption can be substituted by one that operates within the battery life.
This work contrasts between the optimization problem and the satisficng
problem w.r.t. theoretical complexity, empirical performance, and temporal
extensibility.

More specifically, this work studies the aforementioned contrast on two
player, finite-state games with the discounted-sum aggregate function as the
cost model, which is a staple cost-model in decision making domains [75, 78,
85]. In these games, players take turns to pass a token along the transition
relation between the states. As the token is pushed around, the play
accumulates weights along the transitions using the discounted-sum cost model.
The players are assumed to have opposing objectives: one player maximizes the
cost while the other minimizes it. The optimization problem is to find the
optimal cost of all possible plays in the game [83]. We define the satisficing
problem as follows: Given a threshold value $v\in\mathbb{Q}$, does there exist
a strategy for the minimizing player such that the cost of all resulting plays
is less than (or $\leq$) to the threshold $v$?

From prior work, one can infer that the optimization problem is pseudo-
polynomial [57, 93]. Zwick and Patterson have shown that a value-iteration
(VI) algorithm converges to the optimal cost at infinitum [93]. Interestingly,
even though the VI algorithm finds extensive usage [29, 30], a thorough worst-
case analysis of VI has hitherto been absent. This work, first of all, amends
the oversight. In § 8.2, we present the analysis for VI for all discount
factors $d>1$. Towards this, we observe that VI performs many arithmetic
operations. Therefore, it is crucial to account for the cost of arithmetic
operations as well. Its significance is emphasised as we show that there are
orders of magnitude of difference between the complexity of VI under unit-cost
and bit-cost models of arithmetic. For instance, when the discount factor is
an integer, we show that VI is $\mathcal{O}(|V|^{2})\cdot|E|)$ and
$\mathcal{O}(|V|^{4}\cdot|E|)$ under unit- and bit-cost model, respectively,
where $V$ and $E$ are the set of states and transitions. In addition, we
observe that VI can take as many as $\Theta(|V|^{2})$ iterations to compute
the optimal value. Note that this bound is tight, indicating that the
scalability of VI will be limited only to games with a small number of states
and transitions. We confirm this though an empirical analysis. We show that
despite heuristics, VI-based algorithms cannot escape their worst-case
behavior, adversely impacting its empirical performance (§ 8.4). Finally, it
is known that these games may not have optimal solutions when extended with
temporal goals [41].

In contrast, our examination of the satisficing problem illustrates its
advantages over optimization. We solve satisficing via an automata-based
approach as opposed to an arithmetic approach (§ 8.3). Our approach is
motivated by recent advances in automata-based reasoning of quantitative
properties using comparator automata [25, 28]. We show that when the discount
factor is an integer, satisficing problem can be solved in
$\mathcal{O}(|V|+|E|)$ via an efficient reduction to safety/reachability games
[87]. Observe that there is a fundamental separation between the complexity of
satisficing and the number of iterations required in VI, indicating a
computational gain of our comparator-based solution for satisficing. As
before, an empirical evaluation confirms this as well. Last but not the least,
we show that unlike optimization, satisficing naturally integrates with
temporal goals. The reason is that since both, saisficing and temporal goals,
adopt automata-based solutions, the two can be seamlessly combined with one
another (§ 8.6). Currently, our method works for integer discount factors
only. We believe, these results can be extended to the non-integer case with
some approximation guarantee.

####  8.2 Optimization problem

The optimization problem can be solved by a VI algorithm (§ 8.2.1 [93]). While
a reduction from mean-payoff games proves that the VI algorithm is pseudo-
polynomial, a thorough worst-case analysis of VI has been missing. This
section undertakes a thorough investigation of its worst-case complexity.

Our analysis also exposes the dependence of VI on the discount factor $d>1$
and the cost-model for arithmetic operations i.e. unit-cost or bit-cost model.
We observe that these parameters bring about drastic changes to the
algorithm’s theoretical evaluation. Our analysis works for all discount
factors $d>1$.

We begin by describing the VI algorithm in § 8.2.1. First, we prove that it is
sufficient for VI to perform a finite-number of iterations to compute the
optimal value in § 8.2.2. Finally, this result is used to compute the worst-
case complexity of VI under the unit- and bit-cost models of arithmetic in §
8.2.3.

#####  8.2.1 Value-iteration algorithm

The VI algorithm plays a min-max game between the two players [93]. Let
$\mathit{wt}_{k}(v)$ denote the optimal cost of a $k$-length game that begins
in state $v\in V$. Then $\mathit{wt}_{k}(v)$ can be computed using the
following equations: The optimal cost of a 1-length game beginning in state
$v\in V$ is as follows:

$\displaystyle\mathit{wt}_{1}(v)=\begin{cases}\textit{max}\\{\gamma(v,w)|(v,w)\in
E\\}&\text{ if }v\in V_{0}\\\ \textit{min}\\{\gamma(v,w)|(v,w)\in E\\}&\text{
if }v\in V_{1}\end{cases}$

Given the optimal-cost of a $k$-length game, the optimal cost of a
$(k+1)$-length game is computed as follows:

$\displaystyle\mathit{wt}_{k+1}(v)=\begin{cases}\textit{max}\\{\gamma(v,w)+\frac{1}{d}\cdot\mathit{wt}_{k}(w)|(v,w)\in
E\\}\text{ if }v\in V_{0}\\\
\textit{min}\\{\gamma(v,w)+\frac{1}{d}\cdot\mathit{wt}_{k}(w)|(v,w)\in
E\\}\text{ if }v\in V_{1}\end{cases}$

Then, it has been shown that the optimal cost of a $k$-length game beginning
at state $v\in V$ converges to the optimal cost of an infinite-length game
beginning in state $v\in V$ [83, 93] as $k\rightarrow\infty$. In particular,
let $W$ be the optimal value (beginning in state $v_{\mathit{init}}$), then
$W=\text{lim}_{{}_{\rightarrow}k\rightarrow\infty}\mathit{wt}_{k}(v_{\mathit{init}})$.

#####  8.2.2 Number of iterations

The VI algorithm, as defined above, waits for convergence to terminate.
Clearly, that is not sufficient for a worst-case analysis. To this end, in
this section we establish a crisp bound on the number of iterations required
to compute the optimal value. Furthermore, we show that the bound we calculate
is tight.

###### Upper bound on number of iterations.

We prove the upper bound in several steps, as described below:

  1. Step 1

We show that the optimal value $W$ must fall between an interval such that as
the number of iterations $k$ of the VI algorithm increases, the interval
length converges to 0.

  2. Step 2

We show that the optimal value $W$ is a rational number with denominator at
most $\mathsf{bound_{W}}$, where $\mathsf{bound_{W}}$ is parameterized by
numerator and denominator of the discount factor and the number of states in
the graph game.

  3. Step 3

Next, we show that the denominator of the minimum non-zero difference between
possible values of the optimal cost is at most $\mathsf{bound_{diff}}$, where
$\mathsf{bound_{diff}}$ is also parameterized by numerator and denominator of
the discount factor and the number of states in the graph game.

  4. Step 4

Finally, we use the previous three Steps to prove the pseudo-polynomial bound.
Since the interval in Step 1 converges to 0, we can choose a $k$ such that the
interval is less than than $1/\mathsf{bound_{diff}}$. In our computations
below, we will see that
$\frac{1}{\mathsf{bound_{diff}}}<\frac{1}{\mathsf{bound_{v}}}$. Therefore,
there can be only one rational number with denominator $\mathsf{bound_{W}}$ or
less in the interval identified by the chosen $k$. Since this interval must
also contain the optimal value $W$, the unique rational number with
denominator less than or equal to $\mathsf{bound_{W}}$ must be the optimal
value $W$.

Our task is to compute the value of $k$.

We prove all of these steps one-by-one. We begin with proof of Step 1. We show
that there is a finite-horizon approximation of the optimal value, i.e., for
all $k\in\mathbb{N}$ the optimal value can be bounded using
$\mathit{wt}_{k}(v_{\mathit{init}})$ as follows:

###### Lemma 8.1

Let $W$ be the optimal value of a graph game $G$. Let $\mu>0$ be the maximum
of absolute value of cost on all transitions in $G$. Then, for all
$k\in\mathbb{N}$,

$\mathit{wt}_{k}(v_{\mathsf{init}})-\frac{1}{d^{k-1}}\cdot\frac{\mu}{d-1}\leq
W\leq\mathit{wt}_{k}(v_{\mathsf{init}})+\frac{1}{d^{k-1}}\cdot\frac{\mu}{d-1}$

###### Proof 71

This holds because since $W$ is the limit of
$\mathit{wt}_{k}(v_{\mathsf{init}})$ as $k\rightarrow\infty$, its value must
lie in between the minimum and maximum cost possible if the $k$-length game is
extended to an infinite-length game. The minimum possible extension would be
when the $k$-length game is extended by iterations in which the cost incurred
in each round is $-\mu$. Therefore, the resulting lowest value is
$\mathit{wt}_{k}(v_{\mathsf{init}})-\frac{1}{d^{k-1}}\cdot\frac{\mu}{d-1}$.
Similarly, the maximum value is
$\mathit{wt}_{k}(v_{\mathsf{init}})+\frac{1}{d^{k-1}}\cdot\frac{\mu}{d-1}$. ∎

Clearly, as $k\rightarrow\infty$, the interval around the optimal value $W$
converges to 0. This way we can find an arbitrarily small interval around the
optimal value $W$.

To prove Step 2, we know that there exist memoryless optimal strategies for
both players [83]. Therefore, there must exists an optimal play that is in the
form of a simple lasso. A lasso is a play represented as $v_{0}v_{1}\dots
v_{n}(s_{0}s_{2}\dots s_{m})^{\omega}$. The initial segment $v_{0}v_{1}\dots
v_{n}$ is called the head of the lasso, and the cycle segment $s_{0}s_{1}\dots
s_{m}$ the loop of the lasso. A lasso is simple if each state in
$\\{v_{0}\dots v_{n},s_{0},\dots s_{m}\\}$ is distinct. Hence, in order to
compute the optimal value, it is sufficient to examine simple lassos in the
game only. Therefore, we evaluate the DS of cost sequences derived from simple
lassos only. Let $l=a_{0}\dots a_{n}(b_{0}\dots b_{m})^{\omega}$ be the cost
sequence of a lasso. Let $l_{1}=a_{0}\dots a_{n}$ and $l_{2}=b_{0}\dots b_{m}$
correspond to the cost sequences of the head and loop of lasso, respectively.
Then,

###### Lemma 8.2

Let $l=l_{1}\cdot(l_{2})^{\omega}$ represent an integer cost sequence of a
lasso, where $l_{1}$ and $l_{2}$ are the cost sequences of the head and loop
of the lasso. Let $d=\frac{p}{q}$ be the discount factor. Then,
$\mathit{DS}({l},{d})$ is a rational number with denominator at most
($p^{|l_{2}|}-q^{|l_{2}|})\cdot(p^{|l_{1}|})$.

###### Proof 72

The result can proven by unrolling the expression of DS of a cost-sequence on
a lasso path. The discounted sum of $l$ is given as follows:

$\displaystyle\mathit{DS}({l},{d})=$
$\displaystyle\mathit{DS}({l_{1}},{d})+\frac{1}{d^{|l_{1}|}}\cdot(\mathit{DS}({(l_{2})^{\omega}},{d}))$
$\displaystyle=$
$\displaystyle\mathit{DS}({l_{1}},{d})+\frac{1}{d^{|l_{1}|}}\cdot\Big{(}\mathit{DS}({l_{2}},{d})+\frac{1}{d^{|l_{2}|}}\cdot\mathit{DS}({l_{2}},{d})+\frac{1}{d^{2\cdot|l_{2}|}}\cdot\mathit{DS}({l_{2}},{d})+\dots\Big{)}$
Taking closed form expression of the term in the parenthesis, we get
$\displaystyle=$
$\displaystyle\mathit{DS}({l_{1}},{d})+\frac{1}{d^{|l_{1}|}}\cdot\Big{(}\frac{d^{|l_{2}|}}{d^{|l_{2}|}-1}\Big{)}\cdot\mathit{DS}({l_{2}},{d})$
$\displaystyle\text{Let }l_{2}=b_{0}b_{1}\dots b_{|l_{2}|-1}\text{ where
}b_{i}\in\mathbb{Z}$ $\displaystyle=$
$\displaystyle\mathit{DS}({l_{1}},{d})+\frac{1}{d^{|l_{1}|}}\cdot\Big{(}\frac{d^{|l_{2}|}}{d^{|l_{2}|}-1}\Big{)}\cdot\Big{(}b_{0}+\frac{b_{1}}{d}+\dots+\frac{b_{|l_{2}|-1}}{d^{|l_{2}|-1}}\Big{)}$
$\displaystyle=$
$\displaystyle\mathit{DS}({l_{1}},{d})+\frac{1}{d^{|l_{1}|}}\cdot\Big{(}\frac{1}{d^{|l_{2}|}-1}\Big{)}\cdot\Big{(}b_{0}\cdot
d^{|l_{2}|}+{b_{1}}\cdot d^{|l_{2}|-1}+\dots+{b_{|l_{2}|-1}}{d}\Big{)}$
$\displaystyle\text{Expressing }d=\frac{p}{q}\text{, we get}$ $\displaystyle=$
$\displaystyle\mathit{DS}({l_{1}},{d})+\frac{1}{d^{|l_{1}|}}\cdot\frac{q^{|l_{2}|}}{p^{|l_{2}|}-q^{|l_{2}|}}\cdot\Big{(}b_{0}(\frac{p}{q})^{|l_{2}|}+\dots
b_{|l_{2}|-1}\cdot\frac{p}{q}\Big{)}$
$\displaystyle\mathit{DS}({l_{1}},{d})+\frac{1}{d^{|l_{1}|}}\cdot\frac{1}{p^{|l_{2}|}-q^{|l_{2}|}}\cdot
M,\text{ where }M\in\mathbb{Z}$ $\displaystyle\text{Expressing
}d=\frac{p}{q}\text{ again, we get}$ $\displaystyle=$
$\displaystyle\frac{1}{p^{|l_{1}|}}\cdot\frac{1}{p^{|l_{2}|}-q^{|l_{2}|}}\cdot
N,\text{ where }N\in\mathbb{Z}$

∎

The essence of Lemma 8.2 is that the DS of the cost-sequence of a lasso,
simple or non-simple, is a rational number. From here, we can immediately
derive Step 2:

###### Corollary 8.1

Let $G=(V,v_{\mathit{init}},E,\gamma)$ be a graph game. Let $d=\frac{p}{q}$ be
the discount factor. Then the optimal value of the game is a rational number
with denominator at most $(p^{|V|}-q^{|V|})\cdot(p^{|V|})$

###### Proof 73

The optimal value is obtained on a simple lasso as both players have
memoryless strategies that result in the optimal value. The length of the
simple lasso is at most $|V|$. Therefore, the length of the head and loop are
at most $|V|$ each. Hence, the expression from Lemma 8.2 simplifies to
$(p^{|V|}-q^{|V|})\cdot(p^{|V|})$. ∎

Similarly, Step 3 is resolved as follows:

###### Corollary 8.2

Let $G=(V,v_{\mathit{init}},E,\gamma)$ be a graph game. Let $d=\frac{p}{q}$ be
the discount factor. Then the minimal non-zero difference between the cost on
simple lassos is a rational number with denominator at most
$(p^{(|V|^{2})}-q^{(|V|^{2})})\cdot(p^{(|V|^{2})})$.

###### Proof 74

The difference of two lassos $l_{1}$ and $l_{2}$ can be represented by another
lasso $l=l_{1}\times l_{2}$ constructed from taking their product, and
assigning the difference of their costs on each transition. If the maximum
length of the lassos is $|V|$, then the maximum length of the difference lasso
will be $|V|^{2}$. Then, from Lemma 8.2 we immediately obtain that the upper
bound of the denominator of the minimum non-zero difference of optimal plays
is $(p^{(|V|^{2})}-q^{(|V|^{2})})\cdot(p^{(|V|^{2})})$. ∎

Therefore, $\mathsf{bound}_{{W}}=(p^{|V|}-q^{|V|})\cdot(p^{|V|})$ and
$\mathsf{bound}_{\mathsf{diff}}=(p^{(|V|^{2})}-q^{(|V|^{2})})\cdot(p^{(|V|^{2})})$.
Recall, in [93] Zwick-Paterson informally claim that a pseudo-polynomial
algorithm can be devised to compute the optimal value of the game. We
formalize their statement in the final step as follows:

###### Theorem 8.1

Let $G=(V,v_{\mathit{init}},E,\gamma)$ be a graph game. The number of
iterations required by the value-iteration algorithm or the length of the
finite-length game to compute the optimal value $W$ is

  1. 1.

$\mathcal{O}(|V|^{2})$ when discount factor $d\geq 2$,

  2. 2.

$\mathcal{O}\Big{(}\frac{\log(\mu)}{d-1}+|V|^{2}\Big{)}$ when discount factor
$1<d<2$.

###### Proof 75

Recall, the task is to find a $k$ such that the interval identified by Step 1
is less than $\frac{1}{\mathsf{bound}_{\mathsf{diff}}}$. Note that
$\mathsf{bound}_{{W}}<\mathsf{bound}_{\mathsf{diff}}$. Therefore,
$\frac{1}{\mathsf{bound_{diff}}}<\frac{1}{\mathsf{bound_{v}}}$. Hence, there
can be only one rational value with denominator $\mathsf{bound}_{\mathsf{W}}$
or less in the small interval identified by the chosen $k$. Since the optimal
value must also lie in this interval, the unique rational number with
denominator $\mathsf{bound}_{\mathsf{W}}$ or less must be the optimal value.
Let $k$ be such that the interval from Step 1 is less than
$\frac{1}{\mathsf{bound}_{\mathsf{diff}}}$. Then,

$\displaystyle 2\cdot\frac{\mu}{d-1\cdot d^{k-1}}\leq$ $\displaystyle
c\cdot\frac{1}{(p^{(|V|^{2})}-q^{(|V|^{2})})\cdot(p^{(|V|^{2})})}\text{ for
some }c>0$ $\displaystyle 2\cdot\frac{\mu}{d-1\cdot d^{k-1}}\leq$
$\displaystyle
c\cdot\frac{q^{2\cdot|V|^{2}}}{(p^{(|V|^{2})}-q^{(|V|^{2})})\cdot(p^{(|V|^{2})})}\text{
for some }c>0$ $\displaystyle 2\cdot\frac{\mu}{d-1\cdot d^{k-1}}\leq$
$\displaystyle c\cdot\frac{1}{(d^{(|V|^{2})}-1)\cdot(d^{(|V|^{2})})}\text{ for
}c>0$ $\displaystyle d-1\cdot d^{k-1}\geq$ $\displaystyle
c^{\prime}\cdot\mu\cdot(d^{(|V|^{2})}-1)\cdot(d^{(|V|^{2})})\text{ for
}c^{\prime}>0$ $\displaystyle 2\cdot\log(d-1)+k\cdot\log(d)\geq$
$\displaystyle
c^{\prime\prime}+\log(\mu)+\log(d^{(|V|^{2})}-1)+{|V|^{2}}\cdot\log(d)\text{
for }c^{\prime\prime}>0$

The following cases occur depending how large or small the values are:

  1. Case 1.

When $d\geq 2$: In this case, both $d$ and $d^{|V|^{2}}$ are large. Then,

$\displaystyle 2\cdot\log(d-1)+k\cdot\log(d)$ $\displaystyle\geq
c^{\prime\prime}+\log(\mu)+\log(d^{(|V|^{2})}-1)+{|V|^{2}}\cdot\log(d)\text{
for }c^{\prime\prime}>0$ $\displaystyle 2\cdot\log(d)+k\cdot\log(d)$
$\displaystyle\geq
c^{\prime\prime}+\log(\mu)+{(|V|^{2})}\log(d)+{|V|^{2}}\cdot\log(d)\text{ for
}c^{\prime\prime}>0$ $\displaystyle k$ $\displaystyle=\mathcal{O}(|V|^{2})$

  2. Case 2.

When $d$ is small but $d^{|V|^{2}}$ is not: In this case,
$\log(d)\approx(d-1)$, and $\log(d-1)\approx 2-d$. Then,

$\displaystyle 2\cdot\log(d-1)+k\cdot\log(d)$ $\displaystyle\geq
c^{\prime\prime}+\log(\mu)+\log(d^{(|V|^{2})}-1)+{|V|^{2}}\cdot\log(d)\text{
for }c^{\prime\prime}>0$ $\displaystyle 2\cdot\log(d-1)+k\cdot\log(d)$
$\displaystyle\geq
c^{\prime\prime}+\log(\mu)+{(|V|^{2})}\log(d)+{|V|^{2}}\cdot\log(d)\text{ for
}c^{\prime\prime}>0$ $\displaystyle 2\cdot(2-d)+k\cdot(d-1)$
$\displaystyle\geq
c^{\prime\prime}+\log(\mu)+{(|V|^{2})}(d-1)+{|V|^{2}}\cdot(d-1)\text{ for
}c^{\prime\prime}>0$ $\displaystyle
k=\mathcal{O}\Big{(}\frac{\log(\mu)}{d-1}+|V|^{2}\Big{)}$

  3. Case 3.

When both $d$ and $d^{|V|^{2}}$ are small. Then, in addition to the
approximations from the earlier case, $\log(d^{|V|}-1)\approx(2-d^{|V|})$. So,

$\displaystyle 2\cdot\log(d-1)+k\cdot\log(d)$ $\displaystyle\geq
c^{\prime\prime}+\log(\mu)+\log(d^{(|V|^{2})}-1)+{|V|^{2}}\cdot\log(d)\text{
for }c^{\prime\prime}>0$ $\displaystyle 2\cdot\log(d-1)+k\cdot\log(d)$
$\displaystyle\geq
c^{\prime\prime}+\log(\mu)+2-d^{(|V|^{2})}+{|V|^{2}}\cdot\log(d)\text{ for
}c^{\prime\prime}>0$ $\displaystyle 2\cdot(2-d)+k\cdot(d-1)$
$\displaystyle\geq
c^{\prime\prime}+\log(\mu)+2-d^{(|V|^{2})}+{|V|^{2}}\cdot(d-1)\text{ for
}c^{\prime\prime}>0$ $\displaystyle
k=\mathcal{O}\Big{(}\frac{\log(\mu)}{d-1}+|V|^{2}\Big{)}$

∎

###### Lower bound on number of iterations

Start……$w>0$$0$101000 Figure 8.1: Sketch of game graph which requires
$\Omega(|V|^{2})$ iterations

This bound is tight. We show this by constructing a quantitative graph game
for which it is necessary that the VI algorithm takes $\Omega(|V|^{2})$
iterations. We give a sketch of this input instance in Fig 8.1. Let all states
in Fig 8.1 belong to the maximizing player. Hence, the optimization problem
reduces to searching for a path with optimal cost. The idea is to show that
the cost of finite-length game with lesser than $\Omega(|V|^{2})$-length will
result in an incorrect optimal cost. Therefore, Fig 8.1 is designed in a way
so that the path for optimal cost of a $k$-length game is along the right hand
side (RHS) loop when $k$ is small, but along the left hand side (LHS) loop
when $k$ is large. This way, the correct maximal value can be obtained only at
a large value for $k$. Hence the VI algorithm runs for at least $k$
iterations.

Fig 8.1 realizes these objectives by making the loop to the RHS larger than
the one on the LHS, as shown in Fig 8.1, and assigning $w>0$. The intuition is
that when $k$ is small, the optimal path is along the RHS loop since $w>0$.
However, since the RHS is larger, it accumulates cost slower than the LHS
loop. As a result, as $k$ becomes larger, for an appropriate assignment to
$w$, the cost on the LHS will eventually be larger than that on the PHS. By
meticulous reverse engineering of the size of both loops and the value of $w$,
one can guarantee that $k=\Omega(|V|^{2})$.

A concrete instance is as follows: Let the left hand side loop have $4n$
edges, the right hand side of the loop have $2n$ edges, and
$w=\frac{1}{d^{3n}}+\frac{1}{d^{7n}}+\cdots+\frac{1}{d^{m\cdot n-1}}$ such
that $m\cdot n-1=c\cdot n^{2}$ for a positive integer $c>0$. One can show for
a finite games of length $(m\cdot n-1)$ or less, the optimal path arises from
the loop to the right. But for games of length greater than $(m\cdot n-1)$,
the optimal path will be to due to the left hand side loop.

#####  8.2.3 Worst-case complexity analysis

Finally, we present the complete worst-case complexity analysis. Since, VI
algorithm is dominated by arithmetic operations, we take into account their
cost as well. We work with the unit-cost and bit-cost models of arithmetic. We
observe that this choice has a drastic impact to the worst-case complexities.

###### Unit-cost model

Under the unit-cost model of arithmetic, all arithmetic operations are assumed
to take constant time.

###### Theorem 8.2

Let $G=(V,v_{\mathit{init}},E,\gamma)$ be a quantitative graph game. The
worst-case complexity of computing the optimal value under unit-cost model for
arithmetic operations is

  1. 1.

$\mathcal{O}(|V|^{2}\cdot|E|)$ when discount factor $d\geq 2$,

  2. 2.

$\mathcal{O}\Big{(}\frac{\log(\mu)\cdot|E|}{d-1}+|V|^{2}\cdot|E|\Big{)}$ when
discount factor $1<d<2$.

###### Proof 76

The cost of updating the cost of all vertices from iteration $j$ to $j+1$ is
linear in $|E|$ since every transition is traversed exactly once. Therefore,
the worst-case complexity of computing the optimal values of a $k$-length game
is $\mathcal{O}(k\cdot|E|)$. In particular, the worst-case complexity of
computing the optimal value is $\mathcal{O}(|V|^{2}\cdot|E|)$ or
$\mathcal{O}\Big{(}\frac{\log(\mu)\cdot|E|}{d-1}+|V|^{2}\cdot|E|\Big{)}$
depending on whether the discount factor $d\geq 2$ or $1<d<2$, respectively
(Theorem 8.1). ∎

###### Bit-cost model

Under the bit-cost model, the cost of arithmetic operations depends on the
size of the numerical values. Iintegers are represented in their bit-wise
representation. Rational numbers $\frac{r}{s}$ are represented as a tuple of
the bit-wise representation of integers $r$ and $s$. For two integers of
length $n$ and $m$, the cost of their addition and multiplication is $O(m+n)$
and $O(m\cdot n)$, respectively.

To compute the cost of arithmetic in each iteration of the value-iteration
algorithm, we define the cost of a transition $(v,w)\in E$ in the $k$-th
iteration as

$\displaystyle\mathsf{cost}_{1}(v,w)=\gamma(v,w)\text{ and
}\mathsf{cost}_{k}(v,w)=\gamma(v,w)+\frac{1}{d}\cdot\mathit{wt}_{k-1}(v)\text{
for }k>1$

Then, clearly, $\mathit{wt}_{k}(v)=\mu\\{\mathsf{cost}_{k}(v,w)|w\in vE\\}$ if
$v\in V_{0}$ and $\mathit{wt}_{k}(v)=\min\\{\mathsf{cost}_{k}(v,w)|w\in vE\\}$
if $v\in V_{1}$. Since, we compute the cost of every transition in each
iteration, it is crucial to analyze the size and cost of computing
$\mathsf{cost}$.

###### Lemma 8.3

Let $G$ be a quantiative graph game. Let $\mu>0$ be the maximum of absolute
value of all costs along transitions. Let $d=\frac{p}{q}$ be the discount
factor. Then for all $(v,w)\in E$, for all $k>0$

$\mathsf{cost}_{k}(v,w)=\frac{q^{k-1}\cdot n_{1}+q^{k-2}p\cdot
n_{2}+\cdots+p^{k-1}n_{k}}{p^{k-1}}$

where $n_{i}\in\mathbb{Z}$ such that $|n_{i}|\leq\mu$ for all
$i\in\\{1,\dots,k\\}$.

###### Proof 77

Lemma 8.3 can be proven by induction on $k$. ∎

###### Lemma 8.4

Let $G$ be a quantiative graph game. Let $\mu>0$ be the maximum of absolute
value of all costs along transitions. Let $d=\frac{p}{q}$ be the discount
factor. For all $(v,w)\in E$, for all $k>0$ the cost of computing
$\mathsf{cost}_{k}(v,w)$ in the $k$-th iteration is $\mathcal{O}(k\cdot\log
p\cdot\mu\\{\log\mu,\log p\\})$.

###### Proof 78

We compute the cost of computing $\mathsf{cost}_{k}(v,w)$ given that optimal
costs have been computed for the $(k-1)$-th iteration. Recall,

$\displaystyle\mathsf{cost}_{k}(v,w)$
$\displaystyle=\gamma(v,w)+\frac{1}{d}\cdot\mathit{wt}_{k-1}(v)\text{ }=\text{
}\gamma(v,w)+\frac{q}{p}\cdot\mathit{wt}_{k-1}(v)$
$\displaystyle=\gamma(v,w)+\frac{q}{p}\cdot\frac{q^{k-2}\cdot
n_{1}+q^{k-3}p\cdot n_{2}+\cdots+p^{k-2}n_{k-1}}{p^{k-2}}$

for some $n_{i}\in\mathbb{Z}$ such that $|n_{i}|\leq\mu$. Therefore,
computation of $\mathsf{cost}_{k}(v,w)$ involves four operations:

  1. 1.

Multiplication of $q$ with $(q^{k-2}\cdot n_{1}+q^{k-3}p\cdot
n_{2}+\cdots+p^{k-2}n_{k-1})$. The later is bounded by $(k-1)\cdot\mu\cdot
p^{k-1}$ since $|n_{i}|\leq\mu$ and $p>q$. The cost of this operation is
$\mathcal{O}(\log((k-1)\cdot\mu\cdot
p^{k-1})\cdot\log(p))=\mathcal{O}(((k-1)\cdot\log
p+\log\mu+\log(k-1))\cdot(\log p))$.

  2. 2.

Multiplication of $p$ with $p^{k-2}$. Its cost is $\mathcal{O}((k-2)\cdot(\log
p)^{2})$.

  3. 3.

Multiplication of $p^{k-1}$ with $\gamma(v,w)$. Its cost is
$\mathcal{O}((k-1)\cdot\log p\cdot\log\mu)$.

  4. 4.

Addition of $\gamma(v,w)\cdot p^{k-1}$ with $q\cdot(q^{k-2}\cdot
n_{1}+q^{k-3}p\cdot n_{2}+\cdots+p^{k-2}n_{k-1})$. The cost is linear in their
representations.

Therefore, the cost of computing $\mathsf{cost}_{k}(v,w)$ is
$\mathcal{O}(k\cdot\log p\cdot\mu\\{\log\mu,\log p\\})$. ∎

Now, we can compute the cost of computing optimal costs in the $k$-th
iteration from the $k-1$-th iteration.

###### Lemma 8.5

Let $G$ be a quantiative graph game. Let $\mu>0$ be the maximum of absolute
value of all costs along transitions. Let $d=\frac{p}{q}$ be the discount
factor. The worst-case complexity of computing optimal costs in the $k$-th
iteration from the $(k-1)$-th iteration is $\mathcal{O}(|E|\cdot
k\cdot\log\mu\cdot\log p)$.

###### Proof 79

The update requires us to first compute the transition cost in the $k$-th
iteration for every transition in the game. Lemma 8.4 gives the cost of
computing the transition cost of one transition. Therefore, the worst-case
complexity of computing transition cost for all transitions is
$\mathcal{O}(|E|\cdot k\cdot\log p\cdot\mu\\{\log\mu,\log p\\})$.

To compute the optimal cost for each state, we are required to compute the
maximum transition cost of all outgoing transitions from the state. Since the
denominator is same, the maximum value can be computed via lexicographic
comparison of the numerators on all transitions. Therefore, the cost of
computing maximum for all states is $\mathcal{O}(|E|\cdot
k\cdot\log\mu\cdot\log p)$.

Therefore, total cost of computing optimal costs in the $k$-th iteration from
the $(k-1)$-th iteration is $\mathcal{O}(|E|\cdot k\cdot\log
p\cdot\mu\\{\log\mu,\log p\\})$. ∎

Finally, the worst-case complexity of computing the optimal value of the
quantitative game under bit-cost model for arithmetic operations is as
follows:

###### Theorem 8.3

Let $G=(V,v_{\mathit{init}},E,\gamma)$ be a quantitative graph game. Let
$\mu>0$ be the maximum of absolute value of all costs along transitions. Let
$d=\frac{p}{q}>1$ be the discount factor. The worst-case complexity of
computing the optimal value under bit-cost model for arithmetic operations is

  1. 1.

$\mathcal{O}(|V|^{4}\cdot|E|\cdot\log p\cdot\mu\\{\log\mu,\log p\\})$ when
$d\geq 2$,

  2. 2.

$\mathcal{O}(\Big{(}\frac{\log(\mu)}{d-1}+|V|^{2}\Big{)}^{2}\cdot|E|\cdot\log
p\cdot\mu\\{\log\mu,\log p\\})$ when $1<d<2$.

###### Proof 80

This is the sum of computing the optimal costs for all iterations.

When $d\geq 2$, it is sufficient to perform value iteration for $O(|V|^{2})$
times (Theorem 8.1). So, the cost is
$\mathcal{O}((1+2+3\cdot+|V|^{2})\cdot|E|\cdot\log p\cdot\mu\\{\log\mu,\log
p\\})$. This expression simplifies to $\mathcal{O}(|V|^{4}\cdot|E|\cdot\log
p\cdot\mu\\{\log\mu,\log p\\})$.

A similar computation solves the case for $1<d<2$. ∎

###### Final remarks (Integer discount factor)

Our analysis from Theorem 8.1 till Theorem 8.3 show that VI will not scale
well despite being polynomial in size of the graph game. Even when the
discount factor $d>1$ is an integer ($d\geq 2$), the algorithm requires
$\Theta(|V|^{2})$ iterations as Theorem 8.1 is tight. In this case, VI will be
$\mathcal{O}(|V|^{2}\cdot|E|)$ and $\mathcal{O}(|V|^{4}\cdot|E|)$ under the
unit-cost and bit-cost models for arithmetic operation, respectively (Theorem
8.2 and Theorem 8.3, respectively).

From a practical point of view, implementations of VI will use the bit-cost
model as they may rely on multi-precision libraries in order to to avoid
floating-point errors. Therefore, VI for optimization will be expensive in
practice. One may argue that the upper bounds from Theorem 8.3 may be
tightened. But it must be noted that since VI requires $\Omega(|V|^{2})$
iterations, even a tighter analysis will not significantly improve its
performance in practice.

####  8.3 Satisficing problem

This section formally defines and investigates the satisficing problem. The
intuition captured by satisficing is to determine whether a player can
guarantee that the cost of all plays will never exceeds a given threshold
value. Hence, satisficing can be perceived as a decision variant of
optimization. In this section, we prove that when the discount factor is an
integer, the satisficing problem can be solved in linear time in size of the
game graph. Therefore, showing that satisficing is more scalable and efficient
than optimization. A key feature of our solution for satisficing is that our
solution relies on purely automata-based methods and avoids numerical
computations.

We begin by formally defining the satisficing problem as follows:

######  Definition 8.1 (Satisficing problem)

Given a quantitative graph game $G$ and a threshold value $v\in\mathbb{Q}$,
the satisficing problem is to determine whether player $P_{1}$ has a strategy
such that for all possible resulting plays of the game, the cost of all plays
is less than (or $\leq$) to the threshold $v$, assuming that the objectives of
$P_{0}$ and $P_{1}$ are to maximize and minimize the cost of plays,
respectively.

This section is divided into two parts. § 8.3.1 describes the core technique
that our solution builds on. At the heart of our solution lie DS comparator
automata. Prior work on DS comparator automata have been limited to
representing languages that accept a bounded weight sequence $A$ iff
$\mathit{DS}({A},{d})$ $\mathsf{inc}$ $0$. This section generalizes the
definition to accept weight sequence $A$ iff $\mathit{DS}({A},{d})$
$\mathsf{inc}$ $v$, for an arbitrary but fixed threshold $v\in\mathbb{Q}$. §
8.3.2 presents our complete solution. Here we use the DS comparators to reduce
the satisficing problem to solving a safety or reachability game, when the
discount factor is an integer. In this way, we solve satisficing with
automata-based methods only.

#####  8.3.1 Foundations of DS comparator automata with threshold
$v\in\mathbb{Q}$

This section generalizes DS comparison languages and DS comparator automata to
arbitrary rational threshold values $v\in\mathbb{Q}$. It formally defines the
notions, and studies their safety or co-safety, and $\omega$-regular
properties.

We begin with formal definitions:

######  Definition 8.2 (DS comparison language with threshold
$v\in\mathbb{Q}$)

For an integer upper bound $\mu>0$, discount factor $d>1$, equality or