11institutetext: Reichman University, Herzliya, Israel
11email<EMAIL_ADDRESS>11email<EMAIL_ADDRESS>
# On the Comparison of Discounted-Sum Automata with Multiple Discount Factors
††thanks: This is the full version of a chapter with the same title that
appears in the FoSSaCS 2023 conference proceedings.

Udi Boker Research supported by the Israel Science Foundation grant 2410/22.
0000-0003-4322-8892 Guy Hefetz  0000-0002-4451-6581

###### Abstract

We look into the problems of comparing nondeterministic discounted-sum
automata on finite and infinite words. That is, the problems of checking for
automata ${\mathcal{A}}$ and ${\mathcal{B}}$ whether or not it holds that for
all words $w$,
${\mathcal{A}}(w)={\mathcal{B}}(w),{\mathcal{A}}(w)\leq{\mathcal{B}}(w)$, or
${\mathcal{A}}(w)<{\mathcal{B}}(w)$.

These problems are known to be decidable when both automata have the same
single integral discount factor, while decidability is open in all other
settings: when the single discount factor is a non-integral rational; when
each automaton can have multiple discount factors; and even when each has a
single integral discount factor, but the two are different.

We show that it is undecidable to compare discounted-sum automata with
multiple discount factors, even if all are integrals, while it is decidable to
compare them if each has a single, possibly different, integral discount
factor. To this end, we also provide algorithms to check for given
nondeterministic automaton ${\mathcal{N}}$ and deterministic automaton
${\mathcal{D}}$, each with a single, possibly different, rational discount
factor, whether or not ${\mathcal{N}}(w)={\mathcal{D}}(w)$,
${\mathcal{N}}(w)\geq{\mathcal{D}}(w)$, or ${\mathcal{N}}(w)>{\mathcal{D}}(w)$
for all words $w$.

###### Keywords:

Discounted-sum Automata Comparison Containmet.

##  1 Introduction

Equivalence and containment checks of Boolean automata, namely the checks of
whether $L({\mathcal{A}})=L({\mathcal{B}})$, $L({\mathcal{A}})\subseteq
L({\mathcal{B}})$, or $L({\mathcal{A}})\subset L({\mathcal{B}})$, where
$L({\mathcal{A}})$ and $L({\mathcal{B}})$ are the languages that
${\mathcal{A}}$ and ${\mathcal{B}}$ recognize, are central in the usage of
automata theory in diverse areas, and in particular in formal verification
(e.g, [33, 25, 16, 32, 34, 27]). Likewise, comparison of quantitative
automata, which extends the equivalence and containment checks by asking
whether ${\mathcal{A}}(w)={\mathcal{B}}(w)$, whether
${\mathcal{A}}(w)\leq{\mathcal{B}}(w)$, or whether
${\mathcal{A}}(w)<{\mathcal{B}}(w)$ for all words $w$, are essential for
harnessing quantitative-automata theory to the service of diverse fields and
in particular to the service of quantitative formal verification (e.g, [14,
13, 20, 10, 26, 3, 5, 21]).

Discounted summation is a common valuation function in quantitative automata
theory (e.g, [18, 11, 13, 14]), as well as in various other computational
models, such as games (e.g., [36, 4, 1]), Markov decision processes (e.g, [22,
28, 15]), and reinforcement learning (e.g, [31, 35]), as it formalizes the
concept that an immediate reward is better than a potential one in the far
future, as well as that a potential problem (such as a bug in a reactive
system) in the far future is less troubling than a current one.

A nondeterministic discounted-sum automaton (NDA) has rational weights on the
transitions, and a fixed rational discount factor $\lambda>1$. The value of a
(finite or infinite) run is the discounted summation of the weights on the
transitions, such that the weight in the $i$th transition of the run is
divided by $\lambda^{i}$. The value of a (finite or infinite) word is the
infimum value of the automaton runs on it. An NDA thus realizes a function
from words to real numbers.

NDAs cannot always be determinized [14], they are not closed under basic
algebraic operations [7], and their comparison is not known to be decidable,
relating to various longstanding open problems [8]. However, restricting NDAs
to have an integral discount factor $\lambda\in\mathbb{N}\setminus\\{0,1\\}$
provides a robust class of automata that is closed under determinization and
under algebraic operations, and for which comparison is decidable [7].

Various variants of NDAs are studied in the literature, among which are
_functional_ , _k-valued_ , _probabilistic_ , and more [20, 19, 12]. Yet,
until recently, all of these models were restricted to have a single discount
factor. This is a significant restriction of the general discounted-summation
paradigm, in which multiple discount factors are considered. For example,
Markov decision processes and discounted-sum games allow multiple discount
factors within the same entity [22, 4]. In [6], NDAs were extended to NMDAs,
allowing for multiple discount factors, where each transition can have a
different one. Special attention was given to integral NMDAs, namely to those
with only integral discount factors, analyzing whether they preserve the good
properties of integral NDAs. It was shown that they are generally not closed
under determinization and under algebraic operations, while a restricted class
of them, named tidy-NMDAs, in which the choice of discount factors depends on
the prefix of the word read so far, does preserve the good properties of
integral NDAs.

While comparison of tidy-NMDAs with the same choice function is decidable in
PSPACE [6], it was left open whether comparison of general integral NMDAs
${\mathcal{A}}$ and ${\mathcal{B}}$ is decidable. It is even open whether
comparison of two integral NDAs with different (single) discount factors is
decidable.

We show that it is undecidable to resolve for given NMDA ${\mathcal{N}}$ and
deterministic NMDA (DMDA) ${\mathcal{D}}$, even if both have only integral
discount factors, on both finite and infinite words, whether
${\mathcal{N}}\equiv{\mathcal{D}}$ and whether
${\mathcal{N}}\leq{\mathcal{D}}$, and on finite words also whether
${\mathcal{N}}<{\mathcal{D}}$. We prove the undecidability result by reduction
from the halting problem of two-counter machines. The general scheme follows
similar reductions, such as in [17, 2], yet the crux is in simulating a
counter by integral NMDAs. Upfront, discounted summation is not suitable for
simulating counters, since a current increment has, in the discounted setting,
a much higher influence than of a far-away decrement. However, we show that
multiple discount factors allow in a sense to eliminate the influence of time,
having automata in which no matter where a letter appears in the word, it will
have the same influence on the automaton value. (See Lemmas 1 and 3). Another
main part of the proof is in showing how to nondeterministically adjust the
automaton weights and discount factors in order to “detect” whether a counter
is at a current value $0$. (See Figs. 5, 6, 8 and 9.)

On the positive side, we provide algorithms to decide for given NDA
${\mathcal{N}}$ and deterministic NDA (DDA) ${\mathcal{D}}$, with arbitrary,
possibly different, rational discount factors, whether
${\mathcal{N}}\equiv{\mathcal{D}}$, ${\mathcal{N}}\geq{\mathcal{D}}$, or
${\mathcal{N}}>{\mathcal{D}}$ (Theorem 4.1). Our algorithms work on both
finite and infinite words, and run in PSPACE when the automata weights are
represented in binary and their discount factors in unary. Since integral NDAs
can always be determinized [7], our method also provides an algorithm to
compare two integral NDAs, though not necessarily in PSPACE, since
determinization might exponentially increase the number of states. (Even
though determinization of NDAs is in PSPACE [7, 6], the exponential number of
states might require an exponential space in our algorithms of comparing NDAs
with different discount factors.)

The challenge with comparing automata with different discount factors comes
from the combination of their different accumulations, which tends to be
intractable, resulting in the undecidability of comparing integral NMDAs, and
in the open problems of comparing rational NDAs and of analyzing the
representation of numbers in a non-integral basis [29, 23, 24, 8]. Yet, the
main observation underlying our algorithm is that when each automaton has a
single discount factor, we may unfold the combination of their computation
trees only up to some level $k$, after which we can analyze their continuation
separately, first handling the automaton with the lower (slower decreasing)
discount factor and then the other one. The idea is that after level $k$,
since the accumulated discounting of the second automaton is already much more
significant, even a single non-optimal transition of the first automaton
cannot be compensated by a continuation that is better with respect to the
second automaton. We thus compute the optimal suffix words and runs of the
first automaton from level $k$, on top which we compute the optimal runs of
the second automaton.

##  2 Preliminaries

##### Words.

An _alphabet_ $\Sigma$ is an arbitrary finite set, and a _word_ over $\Sigma$
is a finite or infinite sequence of letters in $\Sigma$, with $\varepsilon$
for the empty word. We denote the concatenation of a finite word $u$ and a
finite or infinite word $w$ by $u\cdot w$, or simply by $uw$. We define
$\Sigma^{+}$ to be the set of all finite words except the empty word, i.e.,
$\Sigma^{+}=\Sigma^{*}\setminus\\{\varepsilon\\}$. For a word
$w=\sigma_{0}\sigma_{1}\sigma_{2}\cdots$ and indexes $i\leq j$, we denote the
_letter at index $i$_ as $w[i]=\sigma_{i}$, and the _sub-word from $i$ to $j$_
as $w[i..j]=\sigma_{i}\sigma_{i+1}\cdots\sigma_{j}$.

For a finite word $w$ and letter $\sigma\in\Sigma$, we denote the number of
occurrences of $\sigma$ in $w$ by $\\#(\sigma,w)$, and for a set
$S\subseteq\Sigma$, we denote $\sum_{\sigma\in S}\\#(\sigma,w)$ by $\\#(S,w)$.

For a finite or infinite word $w$ and a letter $\sigma\in\Sigma$, we define
the _prefix of $w$ up to $\sigma$_, $\mbox{\sc pref}_{\sigma}(w)$, as the
minimal prefix of $w$ that contains a $\sigma$ letter if there is a $\sigma$
letter in $w$ or $w$ itself if it does not contain any $\sigma$ letters.
Formally, $\mbox{\sc
pref}_{\sigma}(w)=\begin{cases}w\big{[}0..\min\\{i~{}|~{}w[i]=\sigma\\}\big{]}&\exists
i~{}|~{}w[i]=\sigma\\\ w&\text{otherwise}\end{cases}$

##### Automata.

A nondeterministic discounted-sum automaton (NDA) [14] is an automaton with
rational weights on the transitions, and a fixed rational discount factor
$\lambda>1$. A nondeterministic discounted-sum automaton with multiple
discount factors (NMDA) [6] is similar to an NDA, but with possibly a
different discount factor on each of its transitions. They are formally
defined as follows:

######  Definition 1 ([6])

A nondeterministic discounted-sum automaton with multiple discount factors
(NMDA), on finite or infinite words, is a tuple
${\mathcal{A}}=\langle\Sigma,Q,\iota,\delta,\gamma,\rho\rangle$ over an
alphabet $\Sigma$, with a finite set of states $Q$, an initial set of states
$\iota\subseteq Q$, a transition function $\delta\subseteq Q\times\Sigma\times
Q$, a weight function $\gamma:\delta\to\mathbb{Q}$, and a discount-factor
function $\rho:\delta\to\mathbb{Q}\cap(1,\infty)$, assigning to each
transition its discount factor, which is a rational greater than one.
111Discount factors are sometimes defined as numbers between $0$ and $1$,
under which setting weights are multiplied by these factors rather than
divided by them.

  * •

A _run_ of ${\mathcal{A}}$ is a sequence of states and alphabet letters,
$p_{0},\sigma_{0},p_{1},\sigma_{1},p_{2},\cdots$, such that $p_{0}\in\iota$ is
an initial state, and for every $i$, $(p_{i},\sigma_{i},p_{i+1})\in\delta$.

  * •

The _length_ of a run $r$, denoted by $|r|$, is $n$ for a finite run
$r=p_{0},\sigma_{0},p_{1},\allowbreak\cdots,\sigma_{n-1},p_{n}$, and $\infty$
for an infinite run.

  * •

For an index $i<|r|$, we define the $i$-th transition of $r$ as
$r[i]=(p_{i},\sigma_{i},p_{i+1})$, and the prefix run with $i$ transitions as
$r[0..i]=p_{0},\sigma_{0},p_{1},\cdots,\sigma_{i},p_{i+1}$.

  * •

The _value_ of a finite/infinite run $r$ is
${\mathcal{A}}(r)=\sum_{i=0}^{|r|-1}{\bigg{(}\gamma\big{(}r[i])\big{)}\cdot\prod_{j=0}^{i-1}\frac{1}{\rho\big{(}r[j]\big{)}}\bigg{)}}$.
For example, the value of the run $r_{1}=q_{0},a,q_{0},a,q_{1},b,q_{2}$ of
${\mathcal{A}}$ from Fig. 1 is
${\mathcal{A}}(r_{1})=1+\frac{1}{2}\cdot\frac{1}{3}+2\cdot\frac{1}{2\cdot
3}=\frac{3}{2}$.

  * •

The _value_ of ${\mathcal{A}}$ on a finite or infinite word $w$ is
${\mathcal{A}}(w)=\inf\\{{\mathcal{A}}(r)~{}|~{}r\text{ is a run of
}{\mathcal{A}}\text{ on }w\\}$.

  * •

For every finite run $r=p_{0},\sigma_{0},p_{1},\cdots,\sigma_{n-1},p_{n}$, we
define the _target state_ as $\delta(r)=p_{n}$ and the _accumulated discount
factor_ as $\rho(r)=\prod_{i=0}^{n-1}{\rho\big{(}r[i])\big{)}}$.

  * •

When all discount factors are integers, we say that ${\mathcal{A}}$ is an
_integral_ NMDA.

  * •

In the case where $|\iota|=1$ and for every $q\in Q$ and $\sigma\in\Sigma$, we
have $|\\{q^{\prime}~{}{\big{|}}\>(q,\sigma,q^{\prime})\in\delta\\}|\leq 1$,
we say that ${\mathcal{A}}$ is deterministic, denoted by DMDA, and view
$\delta$ as a function from words to states.

  * •

When the discount factor function $\rho$ is constant,
$\rho\equiv\lambda\in\mathbb{Q}\cap(1,\infty)$, we say that ${\mathcal{A}}$ is
a _nondeterministic discounted-sum automaton_(NDA) [14] with discount factor
$\lambda$ (a $\lambda$-NDA). If ${\mathcal{A}}$ is deterministic, it is a
$\lambda$-DDA.

  * •

For a state $q\in Q$, we write ${\mathcal{A}}^{q}$ for the NMDA
${\mathcal{A}}^{q}=\langle\Sigma,Q,\set{q},\delta,\gamma,\rho\rangle$.

${\mathcal{A}}:$$q_{0}$$q_{1}$$q_{2}$$a,1,3$$a,\frac{1}{2},2$$a,\frac{1}{4},2$$b,\frac{1}{4},2$$a,1,3$$a,\frac{1}{2},2$$b,2,5$$b,\frac{3}{2},4$
Figure 1: An NMDA ${\mathcal{A}}$. The labeling on the transitions indicate
the alphabet letter, the weight of the transition, and its discount factor.

##### Counter machines.

A two-counter machine [30] ${\mathcal{M}}$ is a sequence
$(l_{1},\ldots,l_{n})$ of commands, for some $n\in\mathbb{N}$, involving two
counters $x$ and $y$. We refer to $\set{1,\ldots,n}$ as the locations of the
machine. For every $i\in\set{1,\ldots,n}$ we refer to $l_{i}$ as the command
in location $i$. There are five possible forms of commands:

$\mbox{\sc inc}(c),\ \mbox{\sc dec}(c),\ \mbox{\sc goto }l_{k},\ \mbox{\sc if
$c$=0 goto $l_{k}$ else goto $l_{k^{\prime}}$},\ \mbox{\sc halt},$

where $c\in\set{x,y}$ is a counter and $1\leq k,k^{\prime}\leq n$ are
locations. For not decreasing a zero-valued counter $c\in\set{x,y}$, every
$\mbox{\sc dec}(c)$ command is preceded by the command if $c$=0 goto
<current_line> else goto <next_line>, and there are no other direct goto-
commands to it. The counters are initially set to $0$. An example of a two-
counter machine is given in Fig. 2.

$l_{1}$. $\mbox{\sc inc}(x)$ $l_{2}$. $\mbox{\sc inc}(x)$ $l_{3}$. if $x$=0
goto $l_{3}$ else goto $l_{4}$ $l_{4}$. $\mbox{\sc dec}(x)$ $l_{5}$. if $x$=0
goto $l_{6}$ else goto $l_{3}$ $l_{6}$. halt

Figure 2: An example of a two-counter machine.

Let $L$ be the set of possible commands in ${\mathcal{M}}$, then a run of
${\mathcal{M}}$ is a sequence
$\psi=\psi_{1},\ldots,\psi_{m}\in(L\times\mathbb{N}\times\mathbb{N})^{*}$ such
that the following hold:

  1. 1.

$\psi_{1}=\langle l_{1},0,0\rangle$.

  2. 2.

For all $1<i\leq m$, let $\psi_{i-1}=(l_{j},\alpha_{x},\alpha_{y})$ and
$\psi_{i}=(l^{\prime},\alpha_{x}^{\prime},\alpha_{y}^{\prime})$. Then, the
following hold.

     * •

If $l_{j}$ is an $\mbox{\sc inc}(x)$ command (resp. $\mbox{\sc inc}(y)$), then
$\alpha_{x}^{\prime}=\alpha_{x}+1$, $\alpha_{y}^{\prime}=\alpha_{y}$ (resp.
$\alpha_{y}=\alpha_{y}+1$, $\alpha_{x}^{\prime}=\alpha_{x}$), and
$l^{\prime}=l_{j+1}$.

     * •

If $l_{j}$ is $\mbox{\sc dec}(x)$ (resp. $\mbox{\sc dec}(y)$) then
$\alpha_{x}^{\prime}=\alpha_{x}-1$, $\alpha_{y}^{\prime}=\alpha_{y}$ (resp.
$\alpha_{y}=\alpha_{y}-1$, $\alpha_{x}^{\prime}=\alpha_{x}$), and
$l^{\prime}=l_{j+1}$.

     * •

If $l_{j}$ is $\mbox{\sc goto }l_{k}$ then $\alpha_{x}^{\prime}=\alpha_{x}$,
$\alpha_{y}^{\prime}=\alpha_{y}$, and $l^{\prime}=l_{k}$.

     * •

If $l_{j}$ is if $x$=0 goto $l_{k}$ else goto $l_{k^{\prime}}$ then
$\alpha_{x}^{\prime}=\alpha_{x}$, $\alpha_{y}^{\prime}=\alpha_{y}$, and
$l^{\prime}=l_{k}$ if $\alpha_{x}=0$, and $l^{\prime}=l_{k^{\prime}}$
otherwise.

     * •

If $l_{j}$ is if $y$=0 goto $l_{k}$ else goto $l_{k^{\prime}}$ then
$\alpha_{x}^{\prime}=\alpha_{x}$, $\alpha_{y}^{\prime}=\alpha_{y}$, and
$l^{\prime}=l_{k}$ if $\alpha_{y}=0$, and $l^{\prime}=l_{k^{\prime}}$
otherwise.

     * •

If $l^{\prime}$ is halt then $i=m$, namely a run does not continue after halt.

If, in addition, we have that $\psi_{m}=\langle
l_{j},\alpha_{x},\alpha_{y}\rangle$ such that $l_{j}$ is a halt command, we
say that $\psi$ is a _halting run_. We say that a machine ${\mathcal{M}}$
0-halts if its run is halting and ends in $\langle l,0,0\rangle$. We say that
a sequence of commands $\tau\in L^{*}$ fits a run $\psi$, if $\tau$ is the
projection of $\psi$ on its first component.

The command trace $\pi=\sigma_{1},\ldots,\sigma_{m}$ of a halting run
$\psi=\psi_{1},\ldots,\psi_{m}$ describes the flow of the run, including a
description of whether a counter $c$ was equal to $0$ or larger than $0$ in
each occurrence of an if $c$=0 goto $l_{k}$ else goto $l_{k^{\prime}}$
command. It is formally defined as follows. $\sigma_{m}=\mbox{\sc halt}$ and
for every $1<i\leq m$, we define $\sigma_{i-1}$ according to
$\psi_{i-1}=(l_{j},\alpha_{x},\alpha_{y})$ in the following manner:

  * •

$\sigma_{i-1}=l_{j}$ if $l_{j}$ is not of the form if $c$=0 goto $l_{k}$ else
goto $l_{k^{\prime}}$.

  * •

$\sigma_{i-1}=(\mbox{\sc goto }l_{k},c=0)$ for $c\in\\{x,y\\}$, if
$\alpha_{c}=0$ and the command $l_{j}$ is of the form if $c$=0 goto $l_{k}$
else goto $l_{k^{\prime}}$.

  * •

$\sigma_{i-1}=(\mbox{\sc goto }l_{k^{\prime}},c>0)$ for $c\in\\{x,y\\}$, if
$\alpha_{c}>0$ and the command $l_{j}$ is of the form if $c$=0 goto $l_{k}$
else goto $l_{k^{\prime}}$.

For example, the command trace of the halting run of the machine in Fig. 2 is
$\mbox{\sc inc}(x)$, $\mbox{\sc inc}(x)$, $(\mbox{\sc goto }l_{4},x>0)$,
$\mbox{\sc dec}(x)$, $(\mbox{\sc goto }l_{3},x>0)$, $(\mbox{\sc goto
}l_{4},x>0)$, $\mbox{\sc dec}(x)$, $(\mbox{\sc goto }l_{6},x=0)$, halt.

Deciding whether a given counter machine ${\mathcal{M}}$ halts is known to be
undecidable [30]. Deciding whether ${\mathcal{M}}$ halts with both counters
having value $0$, termed the $0$-halting problem, is also undecidable. Indeed,
the halting problem can be reduced to the latter by adding some commands that
clear the counters, before every halt command.

##  3 Comparison of NMDAs

We show that comparison of (integral) NMDAs is undecidable by reduction from
the halting problem of two-counter machines. Notice that our NMDAs only use
integral discount factors, while they do have non-integral weights. Yet,
weights can be easily changed to integers as well, by multiplying them all by
a common denominator and making the corresponding adjustments in the
calculations.

We start with a lemma on the accumulated value of certain series of discount
factors and weights. Observe that by the lemma, no matter where the pair of
discount-factor $\lambda\in\mathbb{N}\setminus\\{0,1\\}$ and weight
$w=\frac{\lambda-1}{\lambda}$ appear along the run, they will have the same
effect on the accumulated value. This property will play a key role in
simulating counting by NMDAs.

###### Lemma 1

For every sequence $\lambda_{1},\cdots,\lambda_{m}$ of integers larger than
$1$ and weights $w_{1},\cdots,w_{m}$ such that
$w_{i}=\frac{\lambda_{i}-1}{\lambda_{i}}$, we have
$\sum_{i=1}^{m}{\big{(}w_{i}\cdot\prod_{j=1}^{i-1}\frac{1}{\lambda_{j}}\big{)}}=1-\frac{1}{\prod_{j=1}^{m}\lambda_{j}}$.

###### Proof

We show the claim by induction on $m$.

The base case, i.e. $m=1$, is trivial. For the induction step we have

$\displaystyle\sum_{i=1}^{m+1}{\big{(}w_{i}\cdot\prod_{j=1}^{i-1}\frac{1}{\lambda_{j}}\big{)}}$
$\displaystyle=\sum_{i=1}^{m}{\big{(}w_{i}\cdot\prod_{j=1}^{i-1}\frac{1}{\lambda_{j}}\big{)}}+w_{m+1}\cdot\prod_{j=1}^{m}\frac{1}{\lambda_{j}}$
$\displaystyle=1-\frac{1}{\prod_{j=1}^{m}\lambda_{j}}+\frac{\lambda_{m+1}-1}{\lambda_{m+1}}\cdot\prod_{j=1}^{m}\frac{1}{\lambda_{j}}$
$\displaystyle=1-\frac{\lambda_{m+1}}{\prod_{j=1}^{m+1}\lambda_{j}}+\frac{\lambda_{m+1}-1}{\prod_{j=1}^{m+1}\lambda_{j}}=1-\frac{1}{\prod_{j=1}^{m+1}\lambda_{j}}$

∎

###  3.1 The Reduction

We turn to our reduction from the halting problem of two-counter machines to
the problem of NMDA containment. We provide the construction and the
correctness lemma with respect to automata on finite words, and then show in
Section 3.2 how to use the same construction also for automata on infinite
words.

Given a two-counter machine ${\mathcal{M}}$ with the commands
$(l_{1},\ldots,l_{n})$, we construct an integral DMDA ${\mathcal{A}}$ and an
integral NMDA ${\mathcal{B}}$ on finite words, such that ${\mathcal{M}}$
$0$-halts iff there exists a word $w\in\Sigma^{+}$ such that
${\mathcal{B}}(w)\geq{\mathcal{A}}(w)$ iff there exists a word
$w\in\Sigma^{+}$ such that ${\mathcal{B}}(w)>{\mathcal{A}}(w)$.

The automata ${\mathcal{A}}$ and ${\mathcal{B}}$ operate over the following
alphabet $\Sigma$, which consists of $5n+5$ letters, standing for the possible
elements in a command trace of ${\mathcal{M}}$:

$\displaystyle\Sigma^{\mbox{\sc inc}\mbox{\sc dec}}=\ $
$\displaystyle\set{\mbox{\sc inc}(x),\mbox{\sc dec}(x),\mbox{\sc
inc}(y),\mbox{\sc dec}(y)}$ $\displaystyle\Sigma^{\mbox{\sc goto}}=\ $
$\displaystyle\big{\\{}\mbox{\sc goto }\
l_{k}:k\in\\{1,\ldots,n\\}\big{\\}}\cup$ $\displaystyle\big{\\{}(\mbox{\sc
goto }\ l_{k},c=0):k\in\\{1,\ldots,n\\},c\in\\{x,y\\}\big{\\}}\cup$
$\displaystyle\big{\\{}(\mbox{\sc goto }\
l_{k^{\prime}},c>0):k^{\prime}\in\\{1,\ldots,n\\},c\in\\{x,y\\}\big{\\}}$
$\displaystyle\Sigma^{\mbox{\sc nohalt}}=\ $ $\displaystyle\Sigma^{\mbox{\sc
inc}\mbox{\sc dec}}\cup\Sigma^{\mbox{\sc goto}}$ $\displaystyle\Sigma=\ $
$\displaystyle\Sigma^{\mbox{\sc nohalt}}\cup\big{\\{}\mbox{\sc halt}\big{\\}}$

When ${\mathcal{A}}$ and ${\mathcal{B}}$ read a word $w\in\Sigma^{+}$, they
intuitively simulate a sequence of commands $\tau_{u}$ that induces the
command trace $u=\mbox{\sc pref}_{\mbox{\sc halt}}(w)$. If $\tau_{u}$ fits the
actual run of ${\mathcal{M}}$, and this run 0-halts, then the minimal run of
${\mathcal{B}}$ on $w$ has a value strictly larger than ${\mathcal{A}}(w)$.
If, however, $\tau_{u}$ does not fit the actual run of ${\mathcal{M}}$, or it
does fit the actual run but it does not 0-halt, then the violation is detected
by ${\mathcal{B}}$, which has a run on $w$ with value strictly smaller than
${\mathcal{A}}(w)$.

In the construction, we use the following partial discount-factor functions
$\rho_{p},\rho_{d}:\Sigma^{\mbox{\sc nohalt}}\to\mathbb{N}$ and partial weight
functions $\gamma_{p},\gamma_{d}:\Sigma^{\mbox{\sc nohalt}}\to\mathbb{Q}$.

$\rho_{p}(\sigma)=\begin{cases}5&\sigma=\mbox{\sc inc}(x)\\\
4&\sigma=\mbox{\sc dec}(x)\\\ 7&\sigma=\mbox{\sc inc}(y)\\\ 6&\sigma=\mbox{\sc
dec}(y)\\\
15&\text{otherwise}\end{cases}~{}~{}~{}~{}~{}\rho_{d}(\sigma)=\begin{cases}4&\sigma=\mbox{\sc
inc}(x)\\\ 5&\sigma=\mbox{\sc dec}(x)\\\ 6&\sigma=\mbox{\sc inc}(y)\\\
7&\sigma=\mbox{\sc dec}(y)\\\ 15&\text{otherwise}\end{cases}$

$\gamma_{p}(\sigma)=\frac{\rho_{p}(\sigma)-1}{\rho_{p}(\sigma)}$, and
$\gamma_{d}(\sigma)=\frac{\rho_{d}(\sigma)-1}{\rho_{d}(\sigma)}$. We say that
$\rho_{p}$ and $\gamma_{p}$ are the _primal_ discount-factor and weight
functions, while $\rho_{d}$ and $\gamma_{d}$ are the _dual_ functions. Observe
that for every $c\in\\{x,y\\}$ we have that

$\displaystyle\rho_{p}(\mbox{\sc inc}(c))=\rho_{d}(\mbox{\sc
dec}(c))>\rho_{p}(\mbox{\sc dec}(c))=\rho_{d}(\mbox{\sc inc}(c))$ (1)

Intuitively, we will use the primal functions for ${\mathcal{A}}$’s discount
factors and weights, and the dual functions for identifying violations. Notice
that if changing the primal functions to the dual ones in more occurrences of
$\mbox{\sc inc}(c)$ letters than of $\mbox{\sc dec}(c)$ letters along some
run, then by Lemma 1 the run will get a value lower than the original one.

We continue with their formal definitions.
${\mathcal{A}}=\langle\Sigma,\\{q_{\mathcal{A}},q_{\mathcal{A}}^{h}\\},\\{q_{\mathcal{A}}\\},\delta_{\mathcal{A}},\gamma_{\mathcal{A}},\rho_{\mathcal{A}}\rangle$
is an integral DMDA consisting of two states, as depicted in Fig. 3. Observe
that the initial state $q_{\mathcal{A}}$ has self loops for every alphabet
letter in $\Sigma^{\mbox{\sc nohalt}}$ with weights and discount factors
according to the primal functions, and a transition
$(q_{\mathcal{A}},\mbox{\sc halt},q_{\mathcal{A}}^{h})$ with weight of
$\frac{14}{15}$ and a discount factor of $15$.

$q_{\mathcal{A}}$$q_{{\mathcal{A}}}^{h}$$\mbox{\sc
inc}(x),\frac{4}{5},5$$\mbox{\sc dec}(x),\frac{3}{4},4$$\mbox{\sc
inc}(y),\frac{6}{7},7$$\Sigma^{\mbox{\sc goto}},\frac{14}{15},15$$\mbox{\sc
dec}(y),\frac{5}{6},6$$\mbox{\sc halt},\frac{14}{15},15$$\Sigma,0,2$ Figure 3:
The DMDA ${\mathcal{A}}$ constructed for the proof of Lemma 2.

The integral NMDA
${\mathcal{B}}=\langle\Sigma,Q_{\mathcal{B}},\iota_{\mathcal{B}},\delta_{\mathcal{B}},\gamma_{\mathcal{B}},\rho_{\mathcal{B}}\rangle$
is the union of the following eight gadgets (checkers), each responsible for
checking a certain type of violation in the description of a 0-halting run of
${\mathcal{M}}$. It also has the states
$q_{\mathsf{freeze}},q_{\mathsf{halt}}\in Q_{\mathcal{B}}$ such that for all
$\sigma\in\Sigma$, there are 0-weighted transitions
$(q_{\mathsf{freeze}},\sigma,q_{\mathsf{freeze}})\in\delta_{\mathcal{B}}$ and
$(q_{\mathsf{halt}},\sigma,q_{\mathsf{halt}})\in\delta_{\mathcal{B}}$ with an
arbitrary discount factor. Observer that in all of ${\mathcal{B}}$’s gadgets,
the transition over the letter halt to $q_{\mathsf{halt}}$ has a weight higher
than the weight of the corresponding transition in ${\mathcal{A}}$, so that
when no violation is detected, the value of ${\mathcal{B}}$ on a word is
higher than the value of ${\mathcal{A}}$ on it.

1\. Halt Checker. This gadget, depicted in Fig. 4, checks for violations of
non-halting runs. Observe that its initial state $q_{\mathsf{HC}}$ has self
loops identical to those of ${\mathcal{A}}$’s initial state, a transition to
$q_{\mathsf{halt}}$ over halt with a weight higher than the corresponding
weight in ${\mathcal{A}}$, and a transition to the state $q_{\mathsf{last}}$
over every letter that is not halt, “guessing” that the run ends without a
halt command.

$q_{\mathsf{HC}}$$q_{\mathsf{halt}}$$q_{\mathsf{last}}$$q_{\mathsf{freeze}}$$\mbox{\sc
inc}(x),\frac{4}{5},5$$\mbox{\sc dec}(x),\frac{3}{4},4$$\mbox{\sc
inc}(y),\frac{6}{7},7$$\Sigma^{\mbox{\sc goto}}$,$\frac{14}{15},15$$\mbox{\sc
dec}(y),\frac{5}{6},6$halt,$\frac{15}{16},16$$\Sigma,0,2$$\Sigma^{\mbox{\sc
nohalt}},0,2$$\Sigma,2,2$$\Sigma,0,2$ Figure 4: The Halt Checker in the NMDA
${\mathcal{B}}$.

2\. Negative-Counters Checker. The second gadget, depicted in Fig. 5, checks
that the input prefix $u$ has no more $\mbox{\sc dec}(c)$ than $\mbox{\sc
inc}(c)$ commands for each counter $c\in\\{x,y\\}$. It is similar to
${\mathcal{A}}$, however having self loops in its initial states that favor
$\mbox{\sc dec}(c)$ commands when compared to ${\mathcal{A}}$.

$q_{\mathsf{Nx}}$$q_{\mathsf{halt}}$$\mbox{\sc
inc}(x),\frac{9}{10},10$$\mbox{\sc dec}(x),\frac{1}{2},2$$\mbox{\sc
inc}(y),\frac{6}{7},7$$\Sigma^{\mbox{\sc goto}}$,$\frac{14}{15},15$$\mbox{\sc
dec}(y),\frac{5}{6},6$$\mbox{\sc
halt},\frac{15}{16},16$$q_{\mathsf{Ny}}$$\mbox{\sc
inc}(x),\frac{4}{5},5$$\mbox{\sc dec}(x),\frac{3}{4},4$$\mbox{\sc
inc}(y),\frac{13}{14},14$$\Sigma^{\mbox{\sc
goto}}$,$\frac{14}{15},15$$\mbox{\sc dec}(y),\frac{2}{3},3$$\mbox{\sc
halt},\frac{15}{16},16$ Figure 5: The negative-counters checker, on the left
for $x$ and on the right for $y$, in the NMDA ${\mathcal{B}}$.

3\. Positive-Counters Checker. The third gadget, depicted in Fig. 6, checks
that for every $c\in\\{x,y\\}$, the input prefix $u$ has no more $\mbox{\sc
inc}(c)$ than $\mbox{\sc dec}(c)$ commands. It is similar to ${\mathcal{A}}$,
while having self loops in its initial state according to the dual functions
rather than the primal ones.

$q_{\mathsf{BC}}$$q_{\mathsf{halt}}$$\mbox{\sc
inc}(x),\frac{3}{4},4$$\mbox{\sc dec}(x),\frac{4}{5},5$$\mbox{\sc
inc}(y),\frac{5}{6},6$$\Sigma^{\mbox{\sc goto}}$,$\frac{14}{15},15$$\mbox{\sc
dec}(y),\frac{6}{7},7$$\mbox{\sc halt},\frac{15}{16},16$ Figure 6: The
Positive-Counters Checker in the NMDA ${\mathcal{B}}$.

4\. Command Checker. The next gadget checks for local violations of successive
commands. That is, it makes sure that the letter $w_{i}$ represents a command
that can follow the command represented by $w_{i-1}$ in ${\mathcal{M}}$,
ignoring the counter values. For example, if the command in location $l_{2}$
is $\mbox{\sc inc}(x)$, then from state $q_{2}$, which is associated with
$l_{2}$, we move with the letter $\mbox{\sc inc}(x)$ to $q_{3}$, which is
associated with $l_{3}$. The test is local, as this gadget does not check for
violations involving illegal jumps due to the values of the counters. An
example of the command checker for the counter machine in Fig. 2 is given in
Fig. 7.

$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{5}$$q_{6}$$q_{\mathsf{halt}}$$q_{\mathsf{freeze}}$$\mbox{\sc
inc}(x),\frac{4}{5},5$$\mbox{\sc inc}(x),\frac{4}{5},5$$(\mbox{\sc goto
}l_{3},x=0),\frac{14}{15},15$$\mbox{\sc goto
}l_{4}$$x>0,\frac{14}{15},15$$\mbox{\sc dec}(x),\frac{3}{4},4$$(\mbox{\sc goto
}l_{6},x=0),$$\frac{14}{15},15$$(\mbox{\sc goto
}l_{3},x>0),\frac{14}{15},15$$\mbox{\sc
halt},$$\frac{15}{16},16$$\Sigma\setminus\\{\mbox{\sc
inc}(x)\\},$$0,2$$\Sigma\setminus\\{\mbox{\sc halt}\\},$$0,2$ Figure 7: The
command checker that corresponds to the counter machine in Fig. 2.

The command checker, which is a DMDA, consists of states $q_{1},\ldots,q_{n}$
that correspond to the commands $l_{1},\ldots,l_{n}$, and the states
$q_{\mathsf{halt}}$ and $q_{\mathsf{freeze}}$. For two locations $j$ and $k$,
there is a transition from $q_{j}$ to $q_{k}$ on the letter $\sigma$ iff
$l_{k}$ can locally follow $l_{j}$ in a run of ${\mathcal{M}}$ that has
$\sigma$ in the corresponding location of the command trace. That is, either
$l_{j}$ is a $\mbox{\sc goto }l_{k}$ command (meaning $l_{j}=\sigma=\mbox{\sc
goto }l_{k}$), $k$ is the next location after $j$ and $l_{j}$ is an inc or a
dec command (meaning $k=j+1$ and $l_{j}=\sigma\in\Sigma^{\mbox{\sc
inc}\mbox{\sc dec}}$), $l_{j}$ is an if $c$=0 goto $l_{k}$ else goto
$l_{k^{\prime}}$ command with $\sigma=(\mbox{\sc goto }l_{k},c=0)$, or $l_{j}$
is an if $c$=0 goto $l_{s}$ else goto $l_{k}$ command with $\sigma=(\mbox{\sc
goto }l_{k},c>0)$. The weights and discount factors of the $\Sigma^{\mbox{\sc
nohalt}}$ transitions mentioned above are according to the primal functions
$\gamma_{p}$ and $\rho_{p}$ respectively. For every location $j$ such that
$l_{j}=\mbox{\sc halt}$, there is a transition from $q_{j}$ to
$q_{\mathsf{halt}}$ labeled by the letter halt with a weight of
$\frac{15}{16}$ and a discount factor of $16$. Every other transition that was
not specified above leads to $q_{\mathsf{freeze}}$ with weight $0$ and some
discount factor.

5,6. Zero-Jump Checkers. The next gadgets, depicted in Fig. 8, check for
violations in conditional jumps. In this case, we use a different checker
instance for each counter $c\in\\{x,y\\}$, ensuring that for every if $c$=0
goto $l_{k}$ else goto $l_{k^{\prime}}$ command, if the jump $\mbox{\sc goto
}l_{k}$ is taken, then the value of $c$ is indeed $0$.

$q_{\mathsf{ZC}}^{c}$$q_{c}$$q_{\mathsf{halt}}$$\Sigma^{\mbox{\sc
goto}}$,$\frac{14}{15},15$$\Sigma^{\mbox{\sc inc}\mbox{\sc
dec}}\setminus\set{\mbox{\sc inc}(c),\mbox{\sc
dec}(c)},\gamma_{p}(\sigma),\rho_{p}(\sigma)$$\set{\mbox{\sc inc}(c),\mbox{\sc
dec}(c)},\gamma_{d}(\sigma),\rho_{d}(\sigma)$$(\mbox{\sc goto
}l_{k},c=0),$$\frac{14}{15},15$$\Sigma^{\mbox{\sc inc}\mbox{\sc
dec}},\gamma_{p}(\sigma),\rho_{p}(\sigma)$$\Sigma^{\mbox{\sc
goto}}$,$\frac{14}{15},15$$\mbox{\sc halt},\frac{15}{16},16$$\mbox{\sc
halt},\frac{15}{16},16$ Figure 8: The Zero-Jump Checker (for a counter
$c\in\set{x,y}$) in the NMDA ${\mathcal{B}}$.

Intuitively, $q_{\mathsf{ZC}}^{c}$ profits from words that have more
$\mbox{\sc inc}(c)$ than $\mbox{\sc dec}(c)$ letters, while $q_{c}$ continues
like ${\mathcal{A}}$. If the move to $q_{c}$ occurred after a balanced number
of $\mbox{\sc inc}(c)$ and $\mbox{\sc dec}(c)$, as it should be in a real
command trace, neither the prefix word before the move to $q_{c}$, nor the
suffix word after it result in a profit. Otherwise, provided that the counter
is $0$ at the end of the run (as guaranteed by the negative- and positive-
counters checkers), both prefix and suffix words get profits, resulting in a
smaller value for the run.

7,8. Positive-Jump Checkers. These gadgets, depicted in Fig. 9, are dual to
the zero-jump checkers, checking for the dual violations in conditional jumps.
Similarly to the zero-jump checkers, we have a different instance for each
counter $c\in\\{x,y\\}$, ensuring that for every if $c$=0 goto $l_{k}$ else
goto $l_{k^{\prime}}$ command, if the jump $\mbox{\sc goto }l_{k^{\prime}}$ is
taken, then the value of $c$ is indeed greater than $0$.

$q_{\mathsf{PC0}}^{c}$$q_{\mathsf{PC1}}^{c}$$q_{\mathsf{PC2}}^{c}$$q_{\mathsf{freeze}}$$q_{\mathsf{halt}}$$\Sigma^{\mbox{\sc
goto}},\frac{14}{15},15$$\Sigma^{\mbox{\sc inc}\mbox{\sc
dec}}\setminus\set{\mbox{\sc
inc}(c)},\gamma_{p}(\sigma),\rho_{p}(\sigma)$$\mbox{\sc
inc}(c),$$\gamma_{d}(\mbox{\sc inc}(c)),$$\rho_{d}(\mbox{\sc
inc}(c))$$\mbox{\sc halt},\frac{15}{16},16$$(\mbox{\sc goto
}l_{k^{\prime}},c>0),0,2$$\Sigma^{\mbox{\sc inc}\mbox{\sc
dec}},$$\gamma_{p}(\sigma),\rho_{p}(\sigma)$$\Sigma^{\mbox{\sc
goto}},\frac{14}{15},15$$(\mbox{\sc goto
}l_{k^{\prime}},c>0),\frac{14}{15},15$$\Sigma^{\mbox{\sc inc}\mbox{\sc
dec}}\setminus\set{\mbox{\sc inc}(c),\mbox{\sc
dec}(c)},\gamma_{p}(\sigma),\rho_{p}(\sigma)$$\Sigma^{\mbox{\sc
goto}},\frac{14}{15},15$$\set{\mbox{\sc inc}(c),\mbox{\sc
dec}(c)},\gamma_{d}(\sigma),\rho_{d}(\sigma)$$\mbox{\sc
halt},\frac{15}{16},16$$\mbox{\sc halt},1,2$ Figure 9: The Positive-Jump
Checker (for a counter $c$) in the NMDA ${\mathcal{B}}$.

Intuitively, if the counter is $0$ on a $(\mbox{\sc goto }l_{k^{\prime}},c>0)$
command when there was no $\mbox{\sc inc}(c)$ command yet, the gadget benefits
by moving from $q_{\mathsf{PC0}}^{c}$ to $q_{\mathsf{freeze}}$. If there was
an $\mbox{\sc inc}(c)$ command, it benefits by having the dual functions on
the move from $q_{\mathsf{PC0}}^{c}$ to $q_{\mathsf{PC1}}^{c}$ over $\mbox{\sc
inc}(c)$ and the primal functions on one additional self loop of
$q_{\mathsf{PC1}}^{c}$ over $\mbox{\sc dec}(c)$.

###### Lemma 2

Given a two-counter machine ${\mathcal{M}}$, we can compute an integral DMDA
${\mathcal{A}}$ and an integral NMDA ${\mathcal{B}}$ on finite words, such
that ${\mathcal{M}}$ $0$-halts iff there exists a word $w\in\Sigma^{+}$ such
that ${\mathcal{B}}(w)\geq{\mathcal{A}}(w)$ iff there exists a word
$w\in\Sigma^{+}$ such that ${\mathcal{B}}(w)>{\mathcal{A}}(w)$.

###### Proof

Given a two-counter machine ${\mathcal{M}}$, consider the DMDA ${\mathcal{A}}$
and the NMDA ${\mathcal{B}}$ constructed in Section 3.1, and an input word
$w$. Let $u=\mbox{\sc pref}_{\mbox{\sc halt}}(w)$.

We prove the claim by showing that I) if $u$ correctly describes a 0-halting
run of ${\mathcal{M}}$ then ${\mathcal{B}}(w)>{\mathcal{A}}(w)$, and II) if
$u$ does not fit the actual run of ${\mathcal{M}}$, or if it does fit it, but
the run does not 0-halt, then the violation is detected by ${\mathcal{B}}$, in
the sense that ${\mathcal{B}}(w)<{\mathcal{A}}(w)$.

I. We start with the case that $u$ correctly describes a 0-halting run of
${\mathcal{M}}$, and show that ${\mathcal{B}}(w)>{\mathcal{A}}(w)$.

Observe that in all of ${\mathcal{B}}$’s checkers, the transition over the
halt command to the $q_{\mathsf{halt}}$ state has a weight higher than the
weight of the corresponding transition in ${\mathcal{A}}$. Thus, if a checker
behaves like ${\mathcal{A}}$ over $u$, namely uses the primal functions, it
generates a value higher than that of ${\mathcal{A}}$.

We show below that each of the checkers generates a value higher than the
value of ${\mathcal{A}}$ on $u$ (which is also the value of ${\mathcal{A}}$ on
$w$), also if it nondeterministically “guesses a violation”, behaving
differently than ${\mathcal{A}}$.

1\. Halt Checker. Since $u$ does have the halt command, the run of the halt
checker on $u$, if guessing a violation, will end in the pair of transitions
from $q_{\mathsf{HC}}$ to $q_{\mathsf{last}}$ to $q_{\mathsf{freeze}}$ with
discount factor $2$ and weights $0$ and $2$, respectively.

Let $D$ be the accumulated discount factor in the gadget up to these pair of
transitions. According to Lemma 1, the accumulated weight at this point is
$1-\frac{1}{D}$, hence the value of the run will be
$1-\frac{1}{D}+\frac{1}{D}\cdot 0+\frac{1}{2D}\cdot 2=1$, which is, according
to Lemma 1, larger than the value of ${\mathcal{A}}$ on any word.

2,3. Negative- and Positive-Counters Checkers. Since $u$ has the same number
of $\mbox{\sc inc}(c)$ and $\mbox{\sc dec}(c)$ letters, by Eq. 1 and Lemma 1,
these gadgets and ${\mathcal{A}}$ will have the same value on the prefix of
$u$ until the last transition, on which the gadgets will have a higher weight.

4\. Command Checker. As this gadget is deterministic, it cannot “guess a
violation”, and its value on $u$ is larger than ${\mathcal{A}}(u)$ due to the
weight on the halt command.

5,6. Zero-Jump Checkers. Consider a counter $c\in\set{x,y}$ and a run $r$ of
the gadget on $u$. If $r$ did not move to $q_{c}$, we have
${\mathcal{B}}(r)>{\mathcal{A}}(w)$, similarly to the analysis in the
negative- and positive-counters checkers. Otherwise, denote the transition
that $r$ used to move to $q_{c}$ as $t$. Observe that since $u$ correlates to
the actual run of ${\mathcal{M}}$, we have that $t$ was indeed taken when
$c=0$. In this case the value of the run will not be affected, since before
$t$ we have the same number of $\mbox{\sc inc}(c)$ and $\mbox{\sc dec}(c)$
letters, and after $t$ we also have the same number of $\mbox{\sc inc}(c)$ and
$\mbox{\sc dec}(c)$ letters. Hence, due to the last transition over the halt
command, we have ${\mathcal{B}}(r)>{\mathcal{A}}(u)$.

7,8. Positive-Jump Checkers. Consider a counter $c\in\set{x,y}$ and a run $r$
of the gadget on $u$. If $r$ never reaches $q_{\mathsf{PC1}}^{c}$, it has the
same sequence of weights and discount factors as ${\mathcal{A}}$, except for
the higher-valued halt transition. If $r$ reaches $q_{\mathsf{PC1}}^{c}$ but
never reaches $q_{\mathsf{PC2}}^{c}$, since $u$ ends with a halt letter, we
have that $r$ ends with a transition to $q_{\mathsf{freeze}}$ that has a
weight of $1$, hence ${\mathcal{B}}(r)=1>{\mathcal{A}}(w)$.

If $r$ reaches $q_{\mathsf{PC2}}^{c}$, let $u=y\cdot\mbox{\sc inc}(c)\cdot
z\cdot v$ where $y$ has no $\mbox{\sc inc}(c)$ letters, $t=r[|y|+1+|z|]$ is
the first transition in $r$ targeted at $q_{\mathsf{PC2}}^{c}$, and
$\alpha_{c}\geq 1$ is the value of the counter $c$ when $t$ is taken. We have
that $1+\\#(\mbox{\sc inc}(c),z)=\\#(\mbox{\sc dec}(c),z)+\alpha_{c}$. Since
$u$ is balanced, we also have that $\\#(\mbox{\sc dec}(c),v)=\\#(\mbox{\sc
inc}(c),v)+\alpha_{c}$. For the first $\mbox{\sc inc}(c)$ letter, $r$ gets a
discount factor of $\rho_{d}(\mbox{\sc inc}(c))=\rho_{p}(\mbox{\sc dec}(c))$.
All the following $\mbox{\sc inc}(c)$ and $\mbox{\sc dec}(c)$ letters
contribute discount factors according to $\rho_{p}$ in $z$ and according to
$\rho_{d}$ in $v$. Hence, $r$ gets the discount factor $\rho_{p}(\mbox{\sc
dec}(c))$ a total of

$\displaystyle 1+\\#(\mbox{\sc dec}(c),z)+\\#(\mbox{\sc inc}(c),v)$
$\displaystyle=1+1+\\#(\mbox{\sc inc}(c),z)-\alpha_{c}+\\#(\mbox{\sc
inc}(c),v)$ $\displaystyle=\\#(\mbox{\sc inc}(c),u)+1-\alpha_{c}$
$\displaystyle\leq\\#(\mbox{\sc inc}(c),u)=\\#(\mbox{\sc dec}(c),u)$

times, and the discount factor $\rho_{p}(\mbox{\sc inc}(c))$ a total of

$\displaystyle\\#(\mbox{\sc inc}(c),z)+\\#(\mbox{\sc dec}(c),v)$
$\displaystyle=\\#(\mbox{\sc inc}(c),z)+\\#(\mbox{\sc inc}(c),v)+\alpha_{c}$
$\displaystyle=\\#(\mbox{\sc inc}(c),u)-1+\alpha_{c}\geq\\#(\mbox{\sc
inc}(c),u)$

times.

Therefore, the value of $r$ is at least as big as the value of ${\mathcal{A}}$
on the prefix of $u$ until the halt transition, and due to the higher weight
of $r$ on the latter, we have ${\mathcal{B}}(r)>{\mathcal{A}}(u)$.

II. We continue with the case that $u$ does not correctly describe a 0-halting
run of ${\mathcal{M}}$, and show that ${\mathcal{B}}(w)<{\mathcal{A}}(w)$.
Observe that the incorrectness must fall into one of the following cases, each
of which results in a lower value of one of ${\mathcal{B}}$’s gadgets on $u$,
compared to the value of ${\mathcal{A}}$ on $u$:

  * •

The word $u$ has no halt command. In this case the minimal-valued run of the
halt checker on $u$ will be the same as of ${\mathcal{A}}$ until the last
transition, on which the halt checker will have a $0$ weight, compared to a
strictly positive weight in ${\mathcal{A}}$.

  * •

The word $u$ does not describe a run that ends up with value $0$ in both
counters. Then there are the following sub-cases:

    * –

The word $u$ has more $\mbox{\sc dec}(c)$ than $\mbox{\sc inc}(c)$ letters for
some counter $c\in\\{x,y\\}$. For $c=x$, in the negative-counters checker,
more discount factors were changed from $4$ to $2$ than those changed from $5$
to $10$, compared to their values in ${\mathcal{A}}$, implying that the total
value of the gadget until the last letter will be lower than of
${\mathcal{A}}$ on it. For $c=y$, we have a similar analysis with respect to
the discount factors $6;3$, and $7;14$.

    * –

The word $u$ has more $\mbox{\sc inc}(c)$ than $\mbox{\sc dec}(c)$ letters for
some counter $c\in\\{x,y\\}$. By Eq. 1 and Lemma 1, the value of the positive-
counters checker until the last transition will be lower than of
${\mathcal{A}}$ until the last transition.

Observe, though, that the weight of the gadgets on the halt transition ($16$)
is still higher than that of ${\mathcal{A}}$ on it ($15$). Nevertheless, since
a “violation detection” results in replacing at least one discount factor from
$4$ to $2$, from $6$ to $3$, from $5$ to $4$, or from $7$ to $6$ (and
replacing the corresponding weights, for preserving the $\frac{\rho-1}{\rho}$
ratio), and the ratio difference between $16$ and $15$ is less significant
than between the other pairs of weights, we have that the gadget’s value and
therefore ${\mathcal{B}}$’s value on $u$ is smaller than ${\mathcal{A}}(u)$.
Indeed, by Lemma 1 ${\mathcal{A}}(u)=1-\frac{1}{D_{\mathcal{A}}}$, where
$D_{\mathcal{A}}$ is the multiplication of the discount factors along
${\mathcal{A}}$’s run, and ${\mathcal{B}}(u)\leq
1-(\frac{1}{D_{\mathcal{A}}}\cdot\frac{7}{6}\cdot\frac{15}{16})<1-\frac{1}{D_{\mathcal{A}}}={\mathcal{A}}(u)$.

  * •

The word $u$ does not correctly describe the run of ${\mathcal{M}}$. Then
there are the following sub-cases:

    * –

The incorrect description does not relate to conditional jumps. Then the
command-checker has the same weights and discount factors as ${\mathcal{A}}$
on the prefix of $u$ until the incorrect description, after which it has $0$
weights, compared to strictly positive weights in ${\mathcal{A}}$.

    * –

The incorrect description relates to conditional jumps. Then there are the
following sub-sub-cases:

      * *

A counter $c>0$ at a position $i$ of ${\mathcal{M}}$’s run, while
$u[i]=\mbox{\sc goto }l_{k},c=0$. Let $v=u[0..i{-}1]$ and $u=v\cdot
v^{\prime}$, and consider the run $r$ of the zero-jump checker on $u$ that
moves to $q_{c}$ after $v$. Then $\\#(\mbox{\sc inc}(c),v)>\\#(\mbox{\sc
dec}(c),v)$ and $\\#(\mbox{\sc inc}(c),v^{\prime})<\\#(\mbox{\sc
dec}(c),v^{\prime})$. (We may assume that the total number of $\mbox{\sc
inc}(c)$ and $\mbox{\sc dec}(c)$ letters is the same, as otherwise one of the
previous checkers detects it.)

All the $\mbox{\sc inc}(c)$ and $\mbox{\sc dec}(c)$ transitions in
$r[0..i{-}1]$ have weights and discount factors according to the dual
functions, and those transitions in $r[i..|w|{-}1]$ have weights and discount
factors according to the primal functions. Therefore, compared to
${\mathcal{A}}$, more weights changed from $\gamma_{p}(\mbox{\sc inc}(c))$ to
$\gamma_{d}(\mbox{\sc inc}(c))=\gamma_{p}(\mbox{\sc dec}(c))$ than weights
changed from $\gamma_{p}(\mbox{\sc dec}(c))$ to $\gamma_{d}(\mbox{\sc
dec}(c))=\gamma_{p}(\mbox{\sc inc}(c))$, resulting in a lower total value of
$r$ than of ${\mathcal{A}}$ on $u$. (As shown for the negative- and positive-
counters checkers, the higher weight of the halt transition is less
significant than the lower values above.)

      * *

A counter $c=0$ at a position $i$ of ${\mathcal{M}}$’s run, while
$u[i]=\mbox{\sc goto }l_{k},c>0$. Let $r$ be a minimal-valued run of the
positive-jump checker on $u$.

If there are no $\mbox{\sc inc}(c)$ letters in $u$ before position $i$, $r$
will have the same weights and discount factors as ${\mathcal{A}}$ until the
$i$’s letter, on which it will move from $q_{\mathsf{PC1}}^{c}$ to
$q_{\mathsf{freeze}}$, continuing with $0$-weight transitions, compared to
strictly positive ones in ${\mathcal{A}}$.

Otherwise, we have that the first $\mbox{\sc inc}(c)$ letter of $u$ takes $r$
from $q_{\mathsf{PC0}}^{c}$ to $q_{\mathsf{PC1}}^{c}$ with a discount factor
of $\rho_{d}(\mbox{\sc inc}(c))$. Then in $q_{\mathsf{PC1}}^{c}$ we have more
$\mbox{\sc dec}(c)$ transitions than $\mbox{\sc inc}(c)$ transitions, and in
$q_{\mathsf{PC2}}^{c}$ we have the same number of $\mbox{\sc dec}(c)$ and
$\mbox{\sc inc}(c)$ transitions. (We may assume that $u$ passed the previous
checkers, and thus has the same total number of $\mbox{\sc inc}(c)$ and
$\mbox{\sc dec}(c)$ letters.) Hence, we get two more discount factors of
$\rho_{d}(\mbox{\sc inc}(c))$ than $\rho_{p}(\mbox{\sc inc}(c))$, resulting in
a value smaller than ${\mathcal{A}}(u)$. (As in the previous cases, the higher
value of the halt transition is less significant.)

∎

###  3.2 Undecidability of Comparison

For finite words, the undecidability result directly follows from Lemma 2 and
the undecidability of the 0-halting problem of counter machines [30].

###### Theorem 3.1

Strict and non-strict containment of (integral) NMDAs on finite words are
undecidable. More precisely, the problems of deciding for given integral NMDA
${\mathcal{N}}$ and integral DMDA ${\mathcal{D}}$ whether
${\mathcal{N}}(w)\leq{\mathcal{D}}(w)$ for all finite words $w$ and whether
${\mathcal{N}}(w)<{\mathcal{D}}(w)$ for all finite words $w$.

For infinite words, undecidability of non-strict containment also follows from
the reduction given in Section 3.1, as the reduction considers prefixes of the
word until the first halt command. We leave open the question of whether
strict containment is also undecidable for infinite words. The problem with
the latter is that a halt command might never appear in an infinite word $w$
that incorrectly describes a halting run of the two-counter machine, in which
case both automata ${\mathcal{A}}$ and ${\mathcal{B}}$ of the reduction will
have the same value on $w$. On words $w$ that have a halt command but do not
correctly describe a halting run of the two-counter machine we have
${\mathcal{B}}(w)<{\mathcal{A}}(w)$, and on a word $w$ that does correctly
describe a halting run we have ${\mathcal{B}}(w)>{\mathcal{A}}(w)$. Hence, the
reduction only relates to whether ${\mathcal{B}}(w)\leq{\mathcal{A}}(w)$ for
all words $w$, but not to whether ${\mathcal{B}}(w)<{\mathcal{A}}(w)$ for all
words $w$.

###### Theorem 3.2

Non-strict containment of (integral) NMDAs on infinite words is undecidable.
More precisely, the problem of deciding for given integral NMDA
${\mathcal{N}}$ and integral DMDA ${\mathcal{D}}$ whether
${\mathcal{N}}(w)\leq{\mathcal{D}}(w)$ for all infinite words $w$.

###### Proof

The automata ${\mathcal{A}}$ and ${\mathcal{B}}$ in the reduction given in
Section 3.1 can operate as is on infinite words, ignoring the Halt-Checker
gadget of ${\mathcal{B}}$ which is only relevant to finite words.

Since the values of both ${\mathcal{A}}$ and ${\mathcal{B}}$ on an input word
$w$ only relate to the prefix $u=\mbox{\sc pref}_{\mbox{\sc halt}(w)}$ of $w$
until the first halt command, we still have that
${\mathcal{B}}(w)>{\mathcal{A}}(w)$ if $u$ correctly describes a halting run
of the two-counter machine ${\mathcal{M}}$ and that
${\mathcal{B}}(w)<{\mathcal{A}}(w)$ if $u$ is finite and does not correctly
describe a halting run of ${\mathcal{M}}$.

Yet, for infinite words there is also the possibility that the word $w$ does
not contain the halt command. In this case, the value of both ${\mathcal{A}}$
and the command checker of ${\mathcal{B}}$ will converge to $1$, getting
${\mathcal{A}}(w)={\mathcal{B}}(w)$.

Hence, if ${\mathcal{M}}$ 0-halts, there is a word $w$, such that
${\mathcal{B}}(w)>{\mathcal{A}}(w)$ and otherwise, for all words $w$, we have
${\mathcal{B}}(w)\leq{\mathcal{A}}(w)$. ∎

Observe that for NMDAs, equivalence and non-strict containment are
interreducible.

###### Theorem 3.3

Equivalence of (integral) NMDAs on finite as well as infinite words is
undecidable. That is, the problem of deciding for given integral NMDAs
${\mathcal{A}}$ and ${\mathcal{B}}$ on finite or infinite words whether
${\mathcal{A}}(w)={\mathcal{B}}(w)$ for all words $w$.

###### Proof

Assume toward contradiction the existence of a procedure for equivalence check
of ${\mathcal{A}}$ and ${\mathcal{B}}$. We can use the nondeterminism to
obtain an automaton ${\mathcal{C}}={\mathcal{A}}\cup{\mathcal{B}}$, having
$C(w)\leq A(w)$ for all words $w$. We can then check whether ${\mathcal{C}}$
is equivalent to ${\mathcal{A}}$, which holds if and only if
${\mathcal{A}}(w)\leq{\mathcal{B}}(w)$ for all words $w$. Indeed, if
${\mathcal{A}}(w)\leq{\mathcal{B}}(w)$ then
${\mathcal{A}}(w)\leq\min({\mathcal{A}}(w),{\mathcal{B}}(w))={\mathcal{C}}(w)$,
while if there exists a word $w$, such that
${\mathcal{B}}(w)<{\mathcal{A}}(w)$, we have
${\mathcal{C}}(w)=\min({\mathcal{A}}(w),{\mathcal{B}}(w))<{\mathcal{A}}(w)$,
implying that ${\mathcal{C}}$ and ${\mathcal{A}}$ are not equivalent. Thus,
such a procedure contradicts the undecidability of non-strict containment,
shown in Theorems 3.1 and 3.2. ∎

##  4 Comparison of NDAs with Different Discount Factors

We present below our algorithm for the comparison of NDAs with different
discount factors. We start with automata on infinite words, and then show how
to solve the case of finite words by reduction to the case of infinite words.

The algorithm is based on our main observation that, due to the difference
between the discount factors, we only need to consider the combination of the
automata computation trees up to some level $k$, after which we can consider
first the best/worst continuation of the automaton with the smaller discount
factor, and on top of it the worst/best continuation of the second automaton.

For an NDA ${\mathcal{A}}$, we define its _lowest_ (resp.  _highest_)
_infinite run value_ by $\mbox{\sc lowrun}({\mathcal{A}})$ (resp. $\mbox{\sc
highrun}({\mathcal{A}})$) = $\min$ (resp. $\max$)
$\\{{\mathcal{A}}(r)~{}{\big{|}}\>r$ is an infinite run of
${\mathcal{A}}~{}(\text{on some word }w\in\Sigma^{\omega})\\}$.

Observe that we can use $\min$ and $\max$ (rather than $\inf$ and $\sup$)
since the infimum and supremum values are indeed attainable by specific
infinite runs of the NDA (cf. [9, Proof of Theorem 9]). Notice that $\mbox{\sc
lowrun}({\mathcal{A}})$ and $\mbox{\sc highrun}({\mathcal{A}})$ can be
calculated in PTIME by a simple reduction to one-player discounted-payoff
games [4].

Considering word values, we also refer to the _lowest_ (resp.  _highest_)
_word value_ of ${\mathcal{A}}$, defined by $\mbox{\sc
lowword}({\mathcal{A}})$ (resp. $\mbox{\sc highword}({\mathcal{A}})$)= $\min$
(resp. $\max$) $\set{{\mathcal{A}}(w)~{}{\big{|}}\>w\in\Sigma^{\omega}}$.
Observe that $\mbox{\sc lowword}({\mathcal{A}})=\mbox{\sc
lowrun}({\mathcal{A}})$, $\mbox{\sc highword}({\mathcal{A}})\leq\mbox{\sc
highrun}({\mathcal{A}})$, and for deterministic automaton, $\mbox{\sc
highword}({\mathcal{A}})=\mbox{\sc highrun}({\mathcal{A}})$.

For an NMDA ${\mathcal{A}}$ with states $Q$, we define the _maximal difference
between suffix runs_ of ${\mathcal{A}}$ as $\mbox{\sc
maxdiff}(\mathsf{{\mathcal{A}}})=\max\set{\mbox{\sc
highrun}({\mathcal{A}}^{q})-\mbox{\sc
lowrun}({\mathcal{A}}^{q})~{}{\big{|}}\>{q\in Q}}$. Notice that $\mbox{\sc
maxdiff}(\mathsf{{\mathcal{A}}})\geq 0$ and that ${\mathcal{A}}^{q}(w)$ is
bounded as follows.

$\mbox{\sc lowrun}({\mathcal{A}}^{q})\leq{\mathcal{A}}^{q}(w)\leq\mbox{\sc
lowrun}({\mathcal{A}}^{q})+\mbox{\sc maxdiff}(\mathsf{{\mathcal{A}}})$ (2)

###### Lemma 3

There is an algorithm that computes for every input discount factors
$\lambda_{A},\lambda_{D}\in\mathbb{Q}\cap(1,\infty)$, $\lambda_{A}$-NDA
${\mathcal{A}}$ and $\lambda_{D}$-DDA ${\mathcal{D}}$ on infinite words the
value of
$\min\\{{\mathcal{A}}(w)-{\mathcal{D}}(w)~{}{\big{|}}\>w\in\Sigma^{\omega}\\}$.

###### Proof

Consider an alphabet $\Sigma$, discount factors
$\lambda_{A},\lambda_{D}\in\mathbb{Q}\cap(1,\infty)$, a $\lambda_{A}$-NDA
${\mathcal{A}}=\langle\Sigma,Q_{\mathcal{A}},\iota_{\mathcal{A}},\delta_{\mathcal{A}},\gamma_{\mathcal{A}}\rangle$
and a $\lambda_{D}$-DDA
${\mathcal{D}}=\langle\Sigma,Q_{\mathcal{D}},\iota_{\mathcal{D}},\delta_{\mathcal{D}},\gamma_{\mathcal{D}}\rangle$.
When $\lambda_{A}=\lambda_{D}$, we can generate a $\lambda_{A}$-NDA
${\mathcal{C}}\equiv{\mathcal{A}}-{\mathcal{D}}$ over the product of
${\mathcal{A}}$ and ${\mathcal{D}}$ and compute $\mbox{\sc
lowword}({\mathcal{C}})$.

When $\lambda_{A}\neq\lambda_{D}$, we consider first the case that
$\lambda_{A}<\lambda_{D}$.

Our algorithm unfolds the computation trees of ${\mathcal{A}}$ and
${\mathcal{D}}$, up to a level in which only the minimal-valued suffix words
of ${\mathcal{A}}$ remain relevant – Due to the massive difference between the
accumulated discount factor in ${\mathcal{A}}$ compared to the one in
${\mathcal{D}}$, any “penalty” of not continuing with a minimal-valued suffix
word in ${\mathcal{A}}$, defined below as $m_{\mathcal{A}}$, cannot be
compensated even by the maximal-valued word of ${\mathcal{D}}$, which “profit”
is at most as high as $\mbox{\sc maxdiff}(\mathsf{{\mathcal{D}}})$. Hence, at
that level, it is enough to look among the minimal-valued suffixes of
${\mathcal{A}}$ for the one that implies the highest value in ${\mathcal{D}}$.

For every transition $t=(q,\sigma,q^{\prime})\in\delta_{\mathcal{A}}$, let
$\mbox{\sc
minval}(q,\sigma,q^{\prime})=\gamma_{\mathcal{A}}(q,\sigma,q^{\prime})+\frac{1}{\lambda_{A}}\cdot\mbox{\sc
lowword}({\mathcal{A}}^{q^{\prime}})$ be the best (minimal) value that
${\mathcal{A}}^{q}$ can get by taking $t$ as the first transition. We say that
$t$ is _preferred_ if it starts a minimal-valued infinite run of
${\mathcal{A}}^{q}$, namely
$\delta_{pr}=\set{t=(q,\sigma,q^{\prime})\in\delta_{\mathcal{A}}~{}{\big{|}}\>\mbox{\sc
minval}(t)=\mbox{\sc lowword}({\mathcal{A}}^{q})}$ is the set of preferred
transitions of ${\mathcal{A}}$. Observe that an infinite run of
${\mathcal{A}}^{q}$ that takes only transitions from $\delta_{pr}$, has a
value equal to $\mbox{\sc lowrun}({\mathcal{A}}^{q})$ (cf. [9, Proof of
Theorem 9]).

If all the transitions of ${\mathcal{A}}$ are preferred, ${\mathcal{A}}$ has
the same value on all words, and then
$\min\\{{\mathcal{A}}(w)-{\mathcal{D}}(w)~{}{\big{|}}\>w\in\Sigma^{\omega}\\}=\mbox{\sc
lowrun}({\mathcal{A}})-\mbox{\sc highword}({\mathcal{D}})$. (Recall that since
${\mathcal{D}}$ is deterministic, we can easily compute $\mbox{\sc
highword}({\mathcal{D}})$.) Otherwise, let $m_{\mathcal{A}}$ be the minimal
penalty for not taking a preferred transition in ${\mathcal{A}}$, meaning
$m_{\mathcal{A}}=\min\Big{\\{}\mbox{\sc minval}(t^{\prime})-\mbox{\sc
minval}(t^{\prime\prime})\ \Big{|}\
\begin{matrix}t^{\prime}=(q,\sigma^{\prime},q^{\prime})\in\delta_{\mathcal{A}}\setminus\delta_{pr},\\\
t^{\prime\prime}=(q,\sigma^{\prime\prime},q^{\prime\prime})\in\delta_{pr}\end{matrix}\Big{\\}}$.
Observe that $m_{\mathcal{A}}>0$.

Considering the connection between $m_{\mathcal{A}}$ and $\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})$, notice first that if $\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})=0$, ${\mathcal{D}}$ has the same value on all
words, and then we have
$\min\\{{\mathcal{A}}(w)-{\mathcal{D}}(w)~{}{\big{|}}\>w\in\Sigma^{\omega}\\}=\mbox{\sc
lowrun}({\mathcal{A}})-\mbox{\sc lowrun}({\mathcal{D}})$. Otherwise, meaning
$\mbox{\sc maxdiff}(\mathsf{{\mathcal{D}}})>0$, we unfold the computation
trees of ${\mathcal{A}}$ and ${\mathcal{D}}$ for the first $k$ levels, until
the maximal difference between suffix runs in ${\mathcal{D}}$, divided by the
accumulated discount factor of ${\mathcal{D}}$, is smaller than the minimal
penalty for not taking a preferred transition in ${\mathcal{A}}$, divided by
the accumulated discount factor of ${\mathcal{A}}$. Meaning, $k$ is the
minimal integer such that

$\frac{\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})}{{\lambda_{D}}^{k}}<\frac{m_{\mathcal{A}}}{{\lambda_{A}}^{k}}$
(3)

Starting at level $k$, the penalty gained by taking a non-preferred transition
of ${\mathcal{A}}$ cannot be compensated by a higher-valued word of
${\mathcal{D}}$.

At level $k$, we consider separately every run $\psi$ of ${\mathcal{A}}$ on
some prefix word $u$. We should look for a suffix word $w$, that minimizes

${\mathcal{A}}(uw)-{\mathcal{D}}(uw)={\mathcal{A}}(\psi)+\frac{1}{{\lambda_{A}}^{k}}\cdot{\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}(w)-{\mathcal{D}}(u)-\frac{1}{{\lambda_{D}}^{k}}\cdot{\mathcal{D}}^{\delta_{\mathcal{D}}(u)}(w)$
(4)

A central point of the algorithm is that every word that minimizes
${\mathcal{A}}-{\mathcal{D}}$ must take only preferred transitions of
${\mathcal{A}}$ starting at level $k$ (see Lemma 4). As all possible remaining
continuations after level $k$ yield the same value in ${\mathcal{A}}$, we can
choose among them the continuation that yields the highest value in
${\mathcal{D}}$.

Let ${\mathcal{B}}$ be the partial automaton with the states of
${\mathcal{A}}$, but only its preferred transitions $\delta_{pr}$. (We ignore
words on which ${\mathcal{B}}$ has no runs.) We shall use the automata product
${\mathcal{B}}^{\delta_{\mathcal{A}}(\psi)}\times{\mathcal{D}}^{\delta_{\mathcal{D}}(u)}$
to force suffix words that only take preferred transitions of ${\mathcal{A}}$,
while calculating among them the highest value in ${\mathcal{D}}$.

Let
${\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))}=\langle\Sigma,Q_{\mathcal{A}}\times
Q_{\mathcal{D}},\set{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))},\delta_{pr}\times\delta_{\mathcal{D}},\gamma_{\mathcal{C}}\rangle$
be the partial $\lambda_{D}$-NDA that is generated by the product of
${\mathcal{B}}^{\delta_{\mathcal{A}}(\psi)}$ and
${\mathcal{D}}^{\delta_{\mathcal{D}}(u)}$, while only considering the weights
(and discount factor) of ${\mathcal{D}}$, meaning
$\gamma_{\mathcal{C}}((q,p),\sigma,(q^{\prime},p^{\prime}))=\gamma_{\mathcal{D}}(p,\sigma,p^{\prime})$.

A word $w$ has a run in ${\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}$ that uses
only preferred transitions iff $w$ has a run in
${\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))}$. Also,
observe that the nondeterminism in ${\mathcal{C}}$ is only related to the
nondeterminism in ${\mathcal{A}}$, and the weight function of ${\mathcal{C}}$
only depends on the weights of ${\mathcal{D}}$, hence all the runs of
${\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))}$ on the
same word result in the same value, which is the value of that word in
${\mathcal{D}}$. Combining both observations, we get that a word $w$ has a run
in ${\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}$ that uses only preferred
transitions iff $w$ has a run $r$ in
${\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))}$ such
that
${\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))}(r)={\mathcal{D}}^{\delta_{\mathcal{D}}(u)}(w)$.
Hence, after taking the $k$-sized run $\psi$ of ${\mathcal{A}}$, and under the
notations defined in Eq. 4, a suffix word $w$ that can take only preferred
transitions of ${\mathcal{A}}$, and maximizes
${\mathcal{D}}^{\delta_{\mathcal{D}}(u)}(w)$, has a value of
${\mathcal{D}}^{\delta_{\mathcal{D}}(u)}(w)=\mbox{\sc
highrun}({\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))})$.
This leads to

$\displaystyle\min\set{{\mathcal{A}}(v)-{\mathcal{D}}(v)~{}{\big{|}}\>v\in\Sigma^{\omega}}=$
$\displaystyle\min\Big{\\{}{\mathcal{A}}(\psi)+\frac{{\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}(w)}{{\lambda_{A}}^{k}}-{\mathcal{D}}(u)-\frac{{\mathcal{D}}^{\delta_{\mathcal{D}}(u)}(w)}{{\lambda_{D}}^{k}}\Big{|}\begin{matrix}u\in\Sigma^{k},w\in\Sigma^{\omega},\\\
\psi\text{ is a run of }{\mathcal{A}}\text{ on }u\end{matrix}\Big{\\}}=$
$\displaystyle\min_{\psi}\Bigg{\\{}{\mathcal{A}}(\psi)+\frac{\mbox{\sc
lowrun}({\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)})}{{\lambda_{A}}^{k}}-{\mathcal{D}}(u)-\frac{\mbox{\sc
highrun}({\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))})}{{\lambda_{D}}^{k}}\Big{|}\begin{matrix}u\in\Sigma^{k},\\\
\psi\text{ is a run}\\\ \text{of }{\mathcal{A}}\text{ on
}u\end{matrix}\Bigg{\\}}$

and it is only left to calculate this value for every $k$-sized run of
${\mathcal{A}}$, meaning for every leaf in the computation tree of
${\mathcal{A}}$.

The case of $\lambda_{A}>\lambda_{D}$ is analogous, with the following
changes:

  * •

For every transition of ${\mathcal{D}}$, we compute $\mbox{\sc
maxval}(p,\sigma,p^{\prime})=\gamma_{\mathcal{D}}(p,\sigma,p^{\prime})+\frac{1}{\lambda_{D}}\cdot\mbox{\sc
highword}({\mathcal{D}}^{p^{\prime}})$, instead of $\mbox{\sc
minval}(q,\sigma,q^{\prime})$.

  * •

The preferred transitions of ${\mathcal{D}}$ are the ones that start a
maximal-valued infinite run, that is
$\delta_{pr}=\set{t=(p,\sigma^{\prime},p^{\prime})\in\delta_{\mathcal{D}}~{}{\big{|}}\>\mbox{\sc
maxval}(t)=\mbox{\sc highrun}({\mathcal{D}}^{p})}$, and the minimal penalty
$m_{\mathcal{D}}$ is
$m_{\mathcal{D}}=\min\Big{\\{}\mbox{\sc maxval}(t^{\prime\prime})-\mbox{\sc
maxval}(t^{\prime})\ \Big{|}\
\begin{matrix}t^{\prime\prime}=(p,\sigma^{\prime\prime},p^{\prime\prime})\in\delta_{pr},\\\
t^{\prime}=(p,\sigma^{\prime},p^{\prime})\in\delta_{\mathcal{D}}\setminus\delta_{pr}\end{matrix}\Big{\\}}$

  * •

$k$ should be the minimal integer such that $\frac{\mbox{\sc
maxdiff}(\mathsf{{\mathcal{A}}})}{{\lambda_{A}}^{k}}<\frac{m_{\mathcal{D}}}{{\lambda_{D}}^{k}}$.

  * •

We define ${\mathcal{B}}$ to be the restriction of ${\mathcal{D}}$ to its
preferred transitions, and
${\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))}$ as a
partial $\lambda_{A}$-NDA on the product of
${\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}$ and
${\mathcal{B}}^{\delta_{\mathcal{D}}(u)}$ while considering the weights of
${\mathcal{A}}$.

  * •

We calculate $\mbox{\sc
lowrun}({\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))})$
for every $k$-sized run of ${\mathcal{A}}$, $\psi$, and conclude that
$\min\set{{\mathcal{A}}-{\mathcal{D}}}$ is equal to

$\displaystyle\min_{\psi}\set{{\mathcal{A}}(\psi)+\frac{\mbox{\sc
lowrun}({\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))})}{{\lambda_{A}}^{k}}-{\mathcal{D}}(u)-\frac{\mbox{\sc
highrun}({\mathcal{D}}_{\delta_{\mathcal{D}}(u)})}{{\lambda_{D}}^{k}}}$

Observe that in this case, it might not hold that all runs of
${\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))}$ on the
same word have the same value, but such property is not required, since we
look for the minimal run value (which is the minimal word value).

∎

Notice that the algorithm of Lemma 3 does not work if switching the direction
of containment, namely if considering a deterministic ${\mathcal{A}}$ and a
nondeterministic ${\mathcal{D}}$. The determinism of ${\mathcal{D}}$ is
required for finding the maximal value of a valid word in
${\mathcal{B}}^{\delta_{\mathcal{A}}(\psi)}\times{\mathcal{D}}^{\delta_{\mathcal{D}}(u)}$.
If ${\mathcal{D}}$ is not deterministic, the maximal-valued run of
${\mathcal{B}}^{\delta_{\mathcal{A}}(\psi)}\times{\mathcal{D}}^{\delta_{\mathcal{D}}(u)}$
on some word $w$ equals the value of some run of ${\mathcal{D}}$ on $w$, but
not necessarily the value of ${\mathcal{D}}$ on $w$. We also need
${\mathcal{D}}$ to be deterministic for computing $\mbox{\sc
highword}({\mathcal{D}}^{p})$ in the case that $\lambda_{A}>\lambda_{D}$.

To show the correctness of Lemma 3, we present the following claim.

###### Lemma 4

For every input discount factors
$\lambda_{A},\lambda_{D}\in\mathbb{Q}\cap(1,\infty)$ such that
$\lambda_{A}<\lambda_{D}$, $\lambda_{A}$-NDA ${\mathcal{A}}$ and
$\lambda_{D}$-DDA ${\mathcal{D}}$, every infinite word $w$ that minimizes
${\mathcal{A}}(w)-{\mathcal{D}}(w)$ must take a preferred transition of
${\mathcal{A}}$ at every level $k$ for which $\frac{\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})}{{\lambda_{D}}^{k}}<\frac{m_{\mathcal{A}}}{{\lambda_{A}}^{k}}$.

###### Proof

Consider discount factors $\lambda_{A},\lambda_{D}\in\mathbb{Q}\cap(1,\infty)$
such that $\lambda_{A}<\lambda_{D}$, $\lambda_{A}$-NDA ${\mathcal{A}}$,
$\lambda_{D}$-DDA ${\mathcal{D}}$, and $k$ the minimal integer such that

$\frac{\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})}{{\lambda_{D}}^{k}}<\frac{m_{\mathcal{A}}}{{\lambda_{A}}^{k}}$

Assume toward contradiction the existence of a word $v$ that minimizes
${\mathcal{A}}-{\mathcal{D}}$, while a minimal-valued run $\psi_{\mathcal{A}}$
of ${\mathcal{A}}$ on $v$ does not take a preferred transition at some level
$n\geq k$. Let $u$ be the $n$-sized prefix of $v$, $w$ the corresponding
suffix (meaning $v=u\cdot w$), $\psi$ the prefix run of $\psi_{\mathcal{A}}$
on $u$, and $w^{\prime}$ some minimal-valued word of
${\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}$. The first transition taken by
$\psi_{\mathcal{A}}$ when continuing with $w$ is not preferred, meaning

${\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}(w)\geq\mbox{\sc
lowword}({\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)})+m_{\mathcal{A}}={\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}(w^{\prime})+m_{\mathcal{A}}$
(5)

Hence,

$\displaystyle{\mathcal{A}}(v)-{\mathcal{D}}(v)$
$\displaystyle\overset{\mathrm{{}^{\eqref{eq:Suffix}}}}{=}{\mathcal{A}}(\psi)+\frac{{\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}(w)}{{\lambda_{A}}^{n}}-{\mathcal{D}}(u)-\frac{{\mathcal{D}}^{\delta_{\mathcal{D}}(u)}(w)}{{\lambda_{D}}^{n}}$
$\displaystyle\overset{\mathrm{{}^{\eqref{eq:NotPreferredSuffix},\eqref{eq:ValuesRange}}}}{\geq}{\mathcal{A}}(\psi)+\frac{{\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}(w^{\prime})+m_{\mathcal{A}}}{{\lambda_{A}}^{n}}-{\mathcal{D}}(u)-\frac{\mbox{\sc
lowrun}({\mathcal{D}}^{\delta_{\mathcal{D}}(u)})+\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})}{{\lambda_{D}}^{n}}$
$\displaystyle\overset{\mathrm{{}^{\eqref{eq:UnfoldingLevel}}}}{>}{\mathcal{A}}(\psi)+\frac{{\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}(w^{\prime})}{{\lambda_{A}}^{n}}-{\mathcal{D}}(u)-\frac{\mbox{\sc
lowrun}({\mathcal{D}}^{\delta_{\mathcal{D}}(u)})}{{\lambda_{D}}^{n}}$
$\displaystyle\overset{\mathrm{{}^{\eqref{eq:ValuesRange}}}}{\geq}{\mathcal{A}}(\psi)+\frac{{\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)}(w^{\prime})}{{\lambda_{A}}^{n}}-{\mathcal{D}}(u)-\frac{{\mathcal{D}}^{\delta_{\mathcal{D}}(u)}(w^{\prime})}{{\lambda_{D}}^{n}}$
$\displaystyle\overset{\mathrm{{}^{\eqref{eq:Suffix}}}}{=}{\mathcal{A}}(u\cdot
w^{\prime})-{\mathcal{D}}(u\cdot w^{\prime})$

leading to a contradiction. ∎

Moving to automata on finite words, we reduce the problem to the corresponding
problem with respect to automata on infinite words, by adding to the alphabet
a new letter that represents the end of the word, and making some required
adjustments.

###### Lemma 5

There is an algorithm that computes for every input discount factors
$\lambda_{A},\lambda_{D}\in\mathbb{Q}\cap(1,\infty)$, $\lambda_{A}$-NDA
${\mathcal{A}}$ and $\lambda_{D}$-DDA ${\mathcal{D}}$ on finite words the
value of
$\inf\set{{\mathcal{A}}(u)-{\mathcal{D}}(u)~{}{\big{|}}\>u\in\Sigma^{+}}$, and
determines if there exists a finite word $u$ for which
${\mathcal{A}}(u)-{\mathcal{D}}(u)$ equals that value.

###### Proof

Without loss of generality, we assume that initial states of automata have no
incoming transitions. (Every automaton can be changed in linear time to an
equivalent automaton with this property.)

We convert, as described below, an NDA ${\mathcal{N}}$ on finite words to an
NDA $\hat{{\mathcal{N}}}$ on infinite words, such that $\hat{{\mathcal{N}}}$
intuitively simulates the finite runs of ${\mathcal{N}}$. For an alphabet
$\Sigma$, a discount factor $\lambda\in\mathbb{Q}\cap(1,\infty)$, and a
$\lambda$-NDA (DDA)
${\mathcal{N}}=\langle\Sigma,Q_{\mathcal{N}},\iota_{\mathcal{N}},\delta_{\mathcal{N}},\gamma_{\mathcal{N}}\rangle$
on finite words, we define the $\lambda$-NDA (DDA)
$\hat{{\mathcal{N}}}=\langle\hat{\Sigma},Q_{\mathcal{N}}\cup\set{q_{\tau}},\iota_{\mathcal{N}},\delta_{\hat{{\mathcal{N}}}},\gamma_{\hat{{\mathcal{N}}}}\rangle$
on infinite words. The new alphabet $\hat{\Sigma}=\Sigma\cup\set{\tau}$
contains a new letter $\tau\notin\Sigma$ that indicates the end of a finite
word. The new state $q_{\tau}$ has $0$-valued self loops on every letter in
the alphabet, and there are $0$-valued transitions from every non-initial
state to $q_{\tau}$ on the new letter $\tau$. Formally,
$\delta_{\hat{{\mathcal{N}}}}=\delta_{\mathcal{N}}\cup\set{(q_{\tau},\sigma,q_{\tau}~{}{\big{|}}\>\sigma\in\hat{\Sigma})}\cup\set{(q,\tau,q_{\tau}~{}{\big{|}}\>q\in
Q_{\mathcal{N}}\setminus\iota_{\mathcal{N}})}$, and
$\gamma_{\hat{{\mathcal{N}}}}(t)=\begin{cases}\gamma_{\mathcal{N}}(t)&t\in\delta_{\mathcal{N}}\\\
0&\text{otherwise}\end{cases}$

Observe that for every state $q\in Q_{\mathcal{N}}$, the following hold.

  1. 1.

For every finite run $r_{\mathcal{N}}$ of ${\mathcal{N}}^{q}$, there is an
infinite run $r_{\hat{{\mathcal{N}}}}$ of $\hat{{\mathcal{N}}}^{q}$, such that
${\hat{{\mathcal{N}}}}^{q}(r_{\hat{{\mathcal{N}}}})={{{\mathcal{N}}}}^{q}(r_{{{\mathcal{N}}}})$,
and $r_{\hat{{\mathcal{N}}}}$ takes some $\tau$ transitions.
($r_{\hat{{\mathcal{N}}}}$ can start as $r_{\mathcal{N}}$ and then continue
with only $\tau$ transitions.)

  2. 2.

For every infinite run $r_{\hat{{\mathcal{N}}}}$ of $\hat{{\mathcal{N}}}^{q}$
that has a $\tau$ transition, there is a finite run $r_{\mathcal{N}}$ of
${\mathcal{N}}^{q}$, such that
${\hat{{\mathcal{N}}}}^{q}(r_{\hat{{\mathcal{N}}}})={{{\mathcal{N}}}}^{q}(r_{{{\mathcal{N}}}})$.
($r_{\mathcal{N}}$ can be the longest prefix of $r_{\hat{{\mathcal{N}}}}$ up
to the first $\tau$ transition).

  3. 3.

For every infinite run $r_{\hat{{\mathcal{N}}}}$ of $\hat{{\mathcal{N}}}^{q}$
that has no $\tau$ transition, there is a series of finite runs of
${\mathcal{N}}^{q}$, such that the values of the runs in ${\mathcal{N}}^{q}$
converge to ${\hat{{\mathcal{N}}}}^{q}(r_{\hat{{\mathcal{N}}}})$. (For
example, the series of all prefixes of $r_{\hat{{\mathcal{N}}}}$).

Hence, for every $q\in Q_{\mathcal{N}}$ we have
$\inf\set{{\mathcal{N}}^{q}(r)~{}{\big{|}}\>r\text{ is a run of
}{\mathcal{N}}^{q}}=\mbox{\sc lowrun}({\hat{{\mathcal{N}}}}^{q})$ and
$\sup\set{{\mathcal{N}}^{q}(r)~{}{\big{|}}\>r\text{ is a run of
}{\mathcal{N}}^{q}}=\mbox{\sc highrun}({\hat{{\mathcal{N}}}}^{q})$. (For a
non-initial state $q$, we also consider the “run” of ${\mathcal{N}}^{q}$ on
the empty word, and define its value to be $0$.) Notice that the infimum
(supremum) run value of ${\mathcal{N}}^{q}$ is attained by an actual run of
${\mathcal{N}}^{q}$ iff there is an infinite run of $\hat{{\mathcal{N}}}^{q}$
that gets this value and takes a $\tau$ transition.

For every state $q\in Q_{\hat{{\mathcal{N}}}}$, we can determine, as follows,
whether $\mbox{\sc lowrun}({\hat{{\mathcal{N}}}}^{q})$ is attained by an
infinite run taking a $\tau$ transition. We calculate $\mbox{\sc
lowrun}({\hat{{\mathcal{N}}}}^{q})$ for all states, and then start a process
that iteratively marks the states of $\hat{{\mathcal{N}}}$, such that at the
end, $q\in Q_{\hat{{\mathcal{N}}}}$ is marked iff $\mbox{\sc
lowrun}({\hat{{\mathcal{N}}}}^{q})$ can be achieved by a run with a $\tau$
transition. We start with $q_{\tau}$ as the only marked state. In each
iteration we further mark every state $q$ from which there exists a preferred
transition $t=(q,\sigma,q^{\prime})\in\delta_{pr}$ to some marked state
$q^{\prime}$. The process terminates when an iteration has no new states to
mark. Analogously, we can determine whether $\mbox{\sc
highrun}({\hat{{\mathcal{N}}}}^{q})$ is attained by a run that goes to
$q_{\tau}$.

Consider discount factors
$\lambda_{A},\lambda_{D}\in\mathbb{Q}\cap(1,\infty)$, a $\lambda_{A}$-NDA
${\mathcal{A}}$ and a $\lambda_{D}$-DDA ${\mathcal{D}}$ on finite words. When
$\lambda_{A}=\lambda_{D}$, similarly to Lemma 3, the algorithm finds the
infimum value of ${\mathcal{C}}\equiv{\mathcal{A}}-{\mathcal{D}}$ using
$\hat{{\mathcal{C}}}$, and determines if an actual finite word attains this
value using the process described above.

Otherwise, the algorithm converts ${\mathcal{A}}$ and ${\mathcal{D}}$ to
$\hat{{\mathcal{A}}}$ and $\hat{{\mathcal{D}}}$, and proceeds as in Lemma 3
over $\hat{{\mathcal{A}}}$ and $\hat{{\mathcal{D}}}$. According to the above
observations, we have that
$\inf\set{{\mathcal{A}}(u)-{\mathcal{D}}(u)~{}{\big{|}}\>u\in\Sigma^{+}}=\min\\{\hat{{\mathcal{A}}}(w)-\hat{{\mathcal{D}}}(w)~{}{\big{|}}\>w\in\Sigma^{\omega}\\}$,
and that $\inf\set{{\mathcal{A}}(u)-{\mathcal{D}}(u)}$ is attainable iff
$\min\\{\hat{{\mathcal{A}}}(w)-\hat{{\mathcal{D}}}(w)\\}$ is attainable by
some word that has a $\tau$ transition. Hence, whenever computing lowrun or
highrun, we also perform the process described above, to determine whether
this value is attainable by a run that has a $\tau$ transition. We determine
that $\inf\set{{\mathcal{A}}(u)-{\mathcal{D}}(u)}$ is attainable iff exists a
leaf of the computation tree that leads to it, for which the relevant values
lowrun and highrun are attainable. ∎

####  4.0.1 Complexity analysis

We show below that the algorithm of Lemmas 3 and 5 only needs a polynomial
space, with respect to the size of the input automata, implying a PSPACE
algorithm for the corresponding decision problems. We define the size of an
NDA ${\mathcal{N}}$, denoted by $|{\mathcal{N}}|$, as the maximum between the
number of its transitions, the maximal binary representation of any weight in
it, and the maximal unary representation of the discount factor. (Binary
representation of the discount factors might cause our algorithm to use an
exponential space, in case that the two factors are very close to each other.)
The input NDAs may have rational weights, yet it will be more convenient to
consider equivalent NDAs with integral weights that are obtained by
multiplying all the weights by their common denominator [6]. (Observe that it
causes the values of all words to be multiplied by this same ratio, and it
keeps the same input size, up to a polynomial change.)

Before proceeding to the complexity analysis, we provide an auxiliary lemma.

###### Lemma 6

For every integers $p>q\in\mathbb{N}\setminus\\{0\\}$, a $\frac{p}{q}$-NDA
${\mathcal{A}}$ with integral weights, and a lasso run
$r=t_{0},t_{1},\ldots,t_{x{-}1},(t_{x},t_{x{+}1},\ldots,t_{x+y-1})^{\omega}$
of ${\mathcal{A}}$, there exists an integer $b$, such that
${\mathcal{A}}(r)=\frac{b}{p^{x}(p^{y}-q^{y})}$.

###### Proof

Let $\lambda=\frac{p}{q}$ be ${\mathcal{A}}$’s discount factor, and $\gamma$
its weight function. Consider a lasso run
$r=t_{0},t_{1},\ldots,t_{x{-}1},(t_{x},t_{x{+}1},\ldots,t_{x+y-1})^{\omega}$
of ${\mathcal{A}}$. Let
$v_{f}=\gamma(t_{0})+\frac{1}{\lambda}\gamma(t_{1})+\ldots+\frac{1}{\lambda^{x{-}1}}\gamma(t_{x{-}1})$
be its prefix value, and
$v_{\ell}=\gamma(t_{x})+\frac{1}{\lambda}\gamma(t_{x{+}1})+\ldots+\frac{1}{\lambda^{y{-}1}}\gamma(t_{x+y-1})$
its loop value.

Since all the weights are integers, we have that $v_{f}=\frac{a_{f}}{p^{x}}$
and $v_{\ell}=\frac{a_{\ell}}{p^{y}}$ for some integers $a_{f}$ and
$a_{\ell}$. Recall that for a loop $\ell$ of length $y$ and accumulated value
$v_{\ell}$ in a $\lambda$-NDA, the accumulated value of its infinite
repetition is
$\sum_{i=0}^{\infty}\frac{v_{\ell}}{(\lambda^{y})^{i}}=v_{\ell}\frac{\lambda^{y}}{\lambda^{y}-1}$.
Hence the value of $r$ is

$\displaystyle\gamma(r)$ $\displaystyle=v_{f}+\frac{1}{\lambda^{x}}\cdot
v_{\ell}\frac{\lambda^{y}}{\lambda^{y}-1}=\frac{a_{f}}{p^{x}}+\frac{a_{\ell}}{p^{y}}\cdot\frac{1}{\lambda^{x-y}(\lambda^{y}-1)}=\frac{a_{f}}{p^{x}}+\frac{a_{\ell}\cdot
q^{x-y}}{p^{y+x-y}(\frac{p^{y}-q^{y}}{q^{y}})}$
$\displaystyle=\frac{a_{f}(p^{y}-q^{y})+a_{\ell}\cdot
q^{x}}{p^{x}(p^{y}-q^{y})}$

∎

Proceeding to the complexity analysis, let the input size be
$S=|{\mathcal{A}}|+|{\mathcal{D}}|$, the reduced forms of
$\lambda_{\mathcal{A}}$ and $\lambda_{\mathcal{D}}$ be $\frac{{p}}{{q}}$ and
$\frac{{p_{\mathcal{D}}}}{{q_{\mathcal{D}}}}$ respectively, the number of
states in ${\mathcal{A}}$ be $n$, and the maximal difference between
transition weights in ${\mathcal{D}}$ be $M$. Observe that $n\leq S,p\leq
S,M\leq 2\cdot 2^{S}$,
$\frac{\lambda_{\mathcal{D}}}{\lambda_{D}-1}\leq\frac{{p_{\mathcal{D}}}}{{p_{\mathcal{D}}}-{q_{\mathcal{D}}}}\leq{p_{\mathcal{D}}}\leq
S$, and for $\lambda_{{\mathcal{D}}}>\lambda_{{\mathcal{A}}}>1$, we also have
$\frac{\lambda_{\mathcal{D}}}{\lambda_{\mathcal{A}}}=\frac{p\cdot
q_{\mathcal{D}}}{q\cdot p_{\mathcal{D}}}\geq 1+\frac{1}{S^{2}}$.

Observe that ${\mathcal{A}}$ has a best infinite run (and ${\mathcal{D}}$ has
a worst infinite run), in a lasso form as in Lemma 6, with $x,y\in[1..n]$.
Indeed, following preferred transitions, a run must complete a lasso, and then
may forever repeat its choices of preferred transitions. Hence,
$m_{\mathcal{A}}$, being the difference between two lasso runs, is in the form
of

$\displaystyle m_{\mathcal{A}}$
$\displaystyle=\frac{b_{1}}{{p}^{x_{1}}({p}^{y_{1}}-{q}^{y_{1}})}-\frac{b_{2}}{{p}^{x_{2}}({p}^{y_{2}}-{q}^{y_{2}})}=\frac{b_{3}}{{p}^{n}({p}^{y_{1}}-{q}^{y_{1}})({p}^{y_{2}}-{q}^{y_{2}})}>\frac{b_{3}}{{p}^{n}{p}^{y_{1}}{p}^{y_{2}}}$
$\displaystyle\geq\frac{1}{{p}^{3n}}\geq\frac{1}{{S}^{3S}}\stackrel{{\scriptstyle\text{for
}S\geq 1}}{{>}}\frac{1}{({2^{S}})^{3S}}=\frac{1}{2^{3S^{2}}}$

for some $x_{1},x_{2},y_{1},y_{2}\leq n$ and some integers
$b_{1},b_{2},b_{3}$. (Similarly, we can show that
$m_{\mathcal{D}}>\frac{1}{2^{3S^{2}}}$.) We have $\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})\leq
M\cdot\frac{\lambda_{{\mathcal{D}}}}{\lambda_{{\mathcal{D}}}-1}$, hence

$\frac{\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})}{m_{\mathcal{A}}}\leq\frac{M\cdot\frac{\lambda_{{\mathcal{D}}}}{\lambda_{{\mathcal{D}}}-1}}{m_{\mathcal{A}}}\leq\frac{2^{1+S}\cdot
S}{m_{\mathcal{A}}}\stackrel{{\scriptstyle(\text{for }S\geq
1)}}{{<}}\frac{2^{3S}}{m_{\mathcal{A}}}<2^{3S+3S^{2}}$

Recall that we unfold the computation tree until level $k$, which is the
minimal integer such that
$(\frac{\lambda_{D}}{\lambda_{A}})^{k}>\frac{\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})}{m_{\mathcal{A}}}$. Observe that for $S\geq
1$ we have
$\big{(}\frac{\lambda_{{\mathcal{D}}}}{\lambda_{{\mathcal{A}}}}\big{)}^{S^{2}}\geq\big{(}1+\frac{1}{S^{2}}\big{)}^{S^{2}}\geq
2$, hence for $k^{\prime}=S^{2}\cdot(3S+3S^{2})$, we have

$\big{(}\frac{\lambda_{D}}{\lambda_{A}}\big{)}^{k^{\prime}}=\big{(}(\frac{\lambda_{D}}{\lambda_{A}})^{S^{2}}\big{)}^{3S+3S^{2}}\geq
2^{3S+3S^{2}}>\frac{\mbox{\sc
maxdiff}(\mathsf{{\mathcal{D}}})}{m_{\mathcal{A}}}$

meaning that $k$ is polynomial in $S$. Similar analysis shows that $k$ is
polynomial in $S$ also for $\lambda_{{\mathcal{D}}}<\lambda_{{\mathcal{A}}}$.

Considering decision problems that use our algorithm, due to the equivalence
of NPSPACE and PSPACE, the algorithm can nondeterministically guess an optimal
prefix word $u$ of size $k$, letter by letter, as well as a run $\psi$ of
${\mathcal{A}}$ on $u$, transition by transition, and then compute the value
of ${\mathcal{A}}(\psi)+\frac{\mbox{\sc
lowrun}({\mathcal{A}}^{\delta_{\mathcal{A}}(\psi)})}{{\lambda_{A}}^{k}}-{\mathcal{D}}(u)-\frac{\mbox{\sc
highrun}({\mathcal{C}}^{(\delta_{\mathcal{A}}(\psi),\delta_{\mathcal{D}}(u))})}{{\lambda_{D}}^{k}}$.

Observe that along the run of the algorithm, we need to save the following
information, which can be done in polynomial space:

  * •

The automaton ${\mathcal{C}}\equiv{\mathcal{B}}\times{\mathcal{D}}$ (or
${\mathcal{A}}\times{\mathcal{B}}$), which requires polynomial space.

  * •

${\lambda_{\mathcal{A}}}^{k}$ (for ${\mathcal{A}}(\psi)$) and
${\lambda_{\mathcal{D}}}^{k}$ (for ${\mathcal{D}}(u)$). Since we save them in
binary representation, we have $\log_{2}(\lambda^{k})\leq k\log_{2}(S)$,
requiring polynomial space.

We thus get the following complexity result.

###### Theorem 4.1

For input discount factors
$\lambda_{A},\lambda_{D}\in\mathbb{Q}\cap(1,\infty)$, $\lambda_{A}$-NDA
${\mathcal{A}}$ and $\lambda_{D}$-DDA ${\mathcal{D}}$ on finite or infinite
words, it is decidable in PSPACE whether
${\mathcal{A}}(w)\geq{\mathcal{D}}(w)$ and whether
${\mathcal{A}}(w)>{\mathcal{D}}(w)$ for all words $w$.

###### Proof

We use Lemma 3 in the case of infinite words and Lemma 5 in the case of finite
words, checking whether $\min\set{{\mathcal{A}}(w)-{\mathcal{D}}(w)}<0$ and
whether $\min\set{{\mathcal{A}}(w)-{\mathcal{D}}(w)}\leq 0$. In the case of
finite words, we also use the information of whether there is an actual word
that gets the desired value. ∎

Since integral NDAs can always be determinized [7], we get as a corollary that
there is an algorithm to decide equivalence and strict and non-strict
containment of integral NDAs with different (or the same) discount factors.
Note, however, that it might not be in PSPACE, since determinization
exponentially increases the number of states, resulting in $k$ that is
exponential in $S$, and storing in binary representation values in the order
of $\lambda^{k}$ might require exponential space.

###### Corollary 1

There are algorithms to decide for input integral discount factors
$\lambda_{A},\lambda_{B}\in\mathbb{N}$, $\lambda_{A}$-NDA ${\mathcal{A}}$ and
$\lambda_{B}$-NDA ${\mathcal{B}}$ on finite or infinite words whether or not
${\mathcal{A}}(w)>{\mathcal{B}}(w)$, ${\mathcal{A}}(w)\geq{\mathcal{B}}(w)$,
or ${\mathcal{A}}(w)={\mathcal{B}}(w)$ for all words $w$.

##  5 Conclusions

The new decidability result, providing an algorithm for comparing discounted-
sum automata with different integral discount factors, may allow to extend the
usage of discounted-sum automata in formal verification, while the
undecidability result strengthen the justification of restricting discounted-
sum automata with multiple integral discount factors to tidy NMDAs. The new
algorithm also extends the possible, more limited, usage of discounted-sum
automata with rational discount factors, while further research should be put
into this direction.

## References

  * [1] de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: proceedings of ICALP. vol. 2719, pp. 1022–1037 (2003). https://doi.org/10.1007/3-540-45061-0_79
  * [2] Almagor, S., Boker, U., Kupferman, O.: What’s decidable about weighted automata? Information and Computatio 282 (2022). https://doi.org/10.1016/j.ic.2020.104651
  * [3] Almagor, S., Kupferman, O., Ringert, J.O., Velner, Y.: Quantitative assume guarantee synthesis. In: proceedings of CAV. pp. 353–374. Springer (2017). https://doi.org/10.1007/978-3-319-63390-9_19
  * [4] Andersson, D.: An improved algorithm for discounted payoff games. In: proceedings of ESSLLI Student Session. pp. 91–98 (2006)
  * [5] Bansal, S., Chaudhuri, S., Vardi, M.Y.: Comparator automata in quantitative verification. In: proceedings of FoSSaCS. LNCS, vol. 10803, pp. 420–437 (2018). https://doi.org/10.1007/978-3-319-89366-2_23
  * [6] Boker, U., Hefetz, G.: Discounted-sum automata with multiple discount factors. In: proceedings of CSL. LIPIcs, vol. 183, pp. 12:1–12:23. Schloss Dagstuhl \- Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.CSL.2021.12
  * [7] Boker, U., Henzinger, T.A.: Exact and approximate determinization of discounted-sum automata. Log. Methods Comput. Sci. 10(1) (2014). https://doi.org/10.2168/LMCS-10(1:10)2014
  * [8] Boker, U., Henzinger, T.A., Otop, J.: The target discounted-sum problem. In: proceedings of LICS. pp. 750–761 (2015). https://doi.org/10.1109/LICS.2015.74
  * [9] Boker, U., Lehtinen, K.: History determinism vs. good for gameness in quantitative automata. In: proceedings of FSTTCS. pp. 38:1–38:20 (2021). https://doi.org/10.4230/LIPIcs.FSTTCS.2021.38
  * [10] Brenguier, R., Clemente, L., Hunter, P., Pérez, G.A., Randour, M., Raskin, J.F., Sankur, O., Sassolas, M.: Non-zero sum games for reactive synthesis. In: Language and Automata Theory and Applications. pp. 3–23. Springer (2016)
  * [11] Chatterjee, K., Doyen, L., Henzinger, T.A.: Alternating weighted automata. In: proceedings of FCT. LNCS, vol. 5699, pp. 3–13 (2009). https://doi.org/10.1007/978-3-642-03409-1_2
  * [12] Chatterjee, K., Doyen, L., Henzinger, T.A.: Probabilistic weighted automata. In: proceedings of CONCUR. LNCS, vol. 5710, pp. 244–258 (2009). https://doi.org/10.1007/978-3-642-04081-8_17
  * [13] Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and closure properties for quantitative languages. Log. Methods Comput. Sci. 6(3) (2010), http://arxiv.org/abs/1007.4018
  * [14] Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4), 23:1–23:38 (2010). https://doi.org/10.1145/1805950.1805953
  * [15] Chatterjee, K., Forejt, V., Wojtczak, D.: Multi-objective discounted reward verification in graphs and MDPs. In: proceedings of LPAR. LNCS, vol. 8312, pp. 228–242 (2013). https://doi.org/10.1007/978-3-642-45221-5_17
  * [16] Clarke, E.M., Draghicescu, I.A., Kurshan, R.P.: A unified approach for showing language containment and equivalence between various types of $\omega$-automata. Information Processing Letters 46, 301–308 (1993)
  * [17] Degorre, A., Doyen, L., Gentilini, R., Raskin, J., Toruńczyk, S.: Energy and mean-payoff games with imperfect information. In: proceedings of CSL. LNCS, vol. 6247, pp. 260–274 (2010). https://doi.org/10.1007/978-3-642-15205-4_22
  * [18] Droste, M., Kuske, D.: Skew and infinitary formal power series. Theor. Comput. Sci. 366(3), 199–227 (2006). https://doi.org/10.1016/j.tcs.2006.08.024
  * [19] Filiot, E., Gentilini, R., Raskin, J.: Finite-valued weighted automata. In: proceedings of FSTTCS. LIPIcs, vol. 29, pp. 133–145 (2014). https://doi.org/10.4230/LIPIcs.FSTTCS.2014.133
  * [20] Filiot, E., Gentilini, R., Raskin, J.: Quantitative languages defined by functional automata. Log. Methods Comput. Sci. 11(3) (2015). https://doi.org/10.2168/LMCS-11(3:14)2015
  * [21] Filiot, E., Löding, C., Winter, S.: Synthesis from weighted specifications with partial domains over finite words. In: proceedings of FSTTCS. pp. 46:1–46:16 (2020). https://doi.org/10.4230/LIPIcs.FSTTCS.2020.46
  * [22] Gimbert, H., Zielonka, W.: Limits of multi-discounted markov decision processes. In: proceedings of LICS. pp. 89–98 (2007). https://doi.org/10.1109/LICS.2007.28
  * [23] Glendinning, P., Sidorov, N.: Unique representations of real numbers in non-integer bases. Mathematical Research Letters 8(4), 535–543 (2001)
  * [24] Hare, K.: Beta-expansions of pisot and salem numbers. In: Waterloo Workshop in Computer Algebra (2006)
  * [25] Hojati, R., Touati, H., Kurshan, R., Brayton, R.: Efficient $\omega$-regular language containment. In: proceedings of CAV. LNCS, vol. 663. springer (1992)
  * [26] Hunter, P., Pérez, G.A., Raskin, J.: Reactive synthesis without regret. Acta Informatica 54(1), 3–39 (2017). https://doi.org/10.1007/s00236-016-0268-z
  * [27] Kupferman, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM 47(2), 312–360 (2000)
  * [28] Madani, O., Thorup, M., Zwick, U.: Discounted deterministic markov decision processes and discounted all-pairs shortest paths. ACM Trans. Algorithms 6(2), 33:1–33:25 (2010). https://doi.org/10.1145/1721837.1721849
  * [29] Mahler, K.: An unsolved problem on the powers of $\frac{3}{2}$. The journal of the Australian mathematical society 8(2), 313–321 (1968)
  * [30] Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Series in Automatic Computation, Prentice-Hall (1967)
  * [31] Sutton, R.S., G.Barto, A.: Introduction to Reinforcement Learning. MIT Press (1998), http://dl.acm.org/doi/book/10.5555/551283
  * [32] Tasiran, S., Hojati, R., Brayton, R.: Language containment using non-deterministic omega-automata. In: proceedings of CHARME. LNCS, vol. 987, pp. 261–277. springer (1995)
  * [33] Vardi, M.Y.: Verification of concurrent programs: The automata-theoretic framework. In: proceedings of LICS. pp. 167–176 (1987)
  * [34] Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency: Structure versus Automata. LNCS, vol. 1043, pp. 238–266 (1996)
  * [35] Wang, Y., Ye, Q., Liu, T.: Beyond exponentially discounted sum: Automatic learning of return function. CoRR (2019), http://arxiv.org/abs/1905.11591
  * [36] Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158, 343–359 (1996). https://doi.org/10.1016/0304-3975(95)00188-3