On the Comparison of Discounted-Sum Automata with Multiple Discount Factors

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)\le {\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) \ge {\mathcal {D}}(w)$, or ${\mathcal {N}}(w) > {\mathcal {D}}(w)$ for all words w.

U. Boker—Research supported by the Israel Science Foundation grant 2410/22.

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, [17, 26, 28, 33,34,35]). 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)\le {\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, [3, 5, 11, 14, 15, 21, 22, 27]).

Discounted summation is a common valuation function in quantitative automata theory (e.g, [12, 14, 15, 19]), as well as in various other computational models, such as games (e.g., [1, 4, 37]), Markov decision processes (e.g, [16, 23, 29]), and reinforcement learning (e.g, [32, 36]), 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 ith 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 [15], they are not closed under basic algebraic operations [8], and their comparison is not known to be decidable, relating to various longstanding open problems [9]. 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 [8].

Various variants of NDAs are studied in the literature, among which are functional, k-valued, probabilistic, and more [13, 20, 21]. 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 [4, 23]. 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}}\le {\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 [2, 18], 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 Lemma 1 and Fig. 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}}\ge {\mathcal {D}}$, or ${\mathcal {N}}> {\mathcal {D}}$ (Theorem 4). 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 [8], 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 [6, 8], 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 [9, 24, 25, 30]. 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 $\varSigma$ is an arbitrary finite set, and a word over $\varSigma$ is a finite or infinite sequence of letters in $\varSigma$, 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 $\varSigma ^+$ to be the set of all finite words except the empty word, i.e., $\varSigma ^+=\varSigma ^*\setminus \{\varepsilon \}$. For a word $w=\sigma _0 \sigma _1 \sigma _2 \cdots$ and indexes $i\le 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 \varSigma$, we denote the number of occurrences of $\sigma$ in w by $\#(\sigma ,w)$, and for a set $S\subseteq \varSigma$, we denote $\sum _{\sigma \in S}\#(\sigma ,w)$ by $\#(S,w)$.

For a finite or infinite word w and a letter $\sigma \in \varSigma$, we define the prefix of w up to $\sigma$, $\textsc {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, $\textsc {pref} _\sigma (w) ={\left\{ \begin{array}{ll} w\big [0..\min \{i ~|~w[i] = \sigma \}\big ] &{} \exists i ~|~w[i]=\sigma \\ w &{} \text {otherwise} \end{array}\right. }$

Automata. A nondeterministic discounted-sum automaton (NDA) [15] 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 \varSigma , Q, \iota , \delta , \gamma , \rho \rangle$ over an alphabet $\varSigma$, with a finite set of states Q, an initial set of states $\iota \subseteq Q$, a transition function $\delta \subseteq Q \times \varSigma \times Q$, a weight function $\gamma : \delta \rightarrow \mathbb {Q}$, and a discount-factor function $\rho : \delta \rightarrow \mathbb {Q} \cap (1,\infty )$, assigning to each transition its discount factor, which is a rational greater than one.¹

• 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, \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 \varSigma$, we have $|\{ q' ~{\big |}\,(q,\sigma ,q')\in \delta \}| \le 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) [15] 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 \varSigma , Q, \{q\}, \delta , \gamma , \rho \rangle$.

Fig. 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 [31] ${\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 $\{1,\ldots ,n\}$ as the locations of the machine. For every $i\in \{1,\ldots ,n\}$ we refer to $l_i$ as the command in location i. There are five possible forms of commands:

$$\textsc {inc} (c),\ \textsc {dec} (c),\ \textsc {goto }l_k,\ \textsc {if}\ c=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'},\ \textsc {halt},$$

where $c\in \{x,y\}$ is a counter and $1\le k,k'\le n$ are locations. For not decreasing a zero-valued counter $c\in \{x,y\}$, every $\textsc {dec} (c)$ command is preceded by the command , 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.

Fig. 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. $\psi _1=\langle l_1,0,0 \rangle$.

• 2. For all $1< i\le m$, let $\psi _{i-1}=(l_j,\alpha _x,\alpha _y)$ and $\psi _{i}=(l',\alpha _x',\alpha _y')$. Then, the following hold.

  • If $l_j$ is an $\textsc {inc} (x)$ command (resp. $\textsc {inc} (y)$), then $\alpha _x'=\alpha _x+1$, $\alpha _y'=\alpha _y$ (resp. $\alpha _y=\alpha _y+1$, $\alpha _x'=\alpha _x$), and $l'=l_{j+1}$.

  • If $l_j$ is $\textsc {dec} (x)$ (resp. $\textsc {dec} (y)$) then $\alpha _x'=\alpha _x-1$, $\alpha _y'=\alpha _y$ (resp. $\alpha _y=\alpha _y-1$, $\alpha _x'=\alpha _x$), and $l'=l_{j+1}$.

  • If $l_j$ is $\textsc {goto }l_k$ then $\alpha _x'=\alpha _x$, $\alpha _y'=\alpha _y$, and $l'=l_k$.

  • If $l_j$ is $\textsc {if}\ x=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$ then $\alpha _x'=\alpha _x$, $\alpha _y'=\alpha _y$, and $l'=l_k$ if $\alpha _x=0$, and $l'=l_{k'}$ otherwise.

  • If $l_j$ is $\textsc {if}\ y=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$ then $\alpha _x'=\alpha _x$, $\alpha _y'=\alpha _y$, and $l'=l_k$ if $\alpha _y=0$, and $l'=l_{k'}$ otherwise.

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

If, in addition, we have that $\psi _m=\langle l_j,\alpha _x,\alpha _y \rangle$ such that $l_j$ is a $\textsc {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 $\textsc {if}\ c=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$ command. It is formally defined as follows. $\sigma _{m}=\textsc {halt}$ and for every $1< i\le 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 $\textsc {if}\ c=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$.

• $\sigma _{i-1}=(\textsc {goto }l_k,c=0)$ for $c\in \{x,y\}$, if $\alpha _c=0$ and the command $l_j$ is of the form $\textsc {if}\ c=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$.

• $\sigma _{i-1}=(\textsc {goto }l_{k'},c>0)$ for $c\in \{x,y\}$, if $\alpha _c>0$ and the command $l_j$ is of the form $\textsc {if}\ c=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$.

For example, the command trace of the halting run of the machine in Fig. 2 is $\textsc {inc} (x)$, $\textsc {inc} (x)$, $(\textsc {goto }l_4, x>0)$, $\textsc {dec} (x)$, $(\textsc {goto }l_3, x>0)$, $(\textsc {goto }l_4, x>0)$, $\textsc {dec} (x)$, $(\textsc {goto }l_6, x=0)$, $\textsc {halt}$.

Deciding whether a given counter machine ${\mathcal {M}}$ halts is known to be undecidable [31]. 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}$.

The proof is by induction on m and appears in [7].

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 \varSigma ^+$ such that ${\mathcal {B}}(w)\ge {\mathcal {A}}(w)$ iff there exists a word $w\in \varSigma ^+$ such that ${\mathcal {B}}(w) > {\mathcal {A}}(w)$.

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

$$\begin{aligned} \varSigma ^{\textsc {inc} \textsc {dec}}= \ {}&\{\textsc {inc} (x),\textsc {dec} (x),\textsc {inc} (y),\textsc {dec} (y)\} \\ \varSigma ^{\textsc {goto}}=\ {}&\big \{\textsc {goto }\ l_k: k\in \{1,\ldots ,n\}\big \}\cup \\&\big \{(\textsc {goto }\ l_k,c=0): k\in \{1,\ldots ,n\},c\in \{x,y\}\big \}\cup \\&\big \{(\textsc {goto }\ l_{k'},c>0): k'\in \{1,\ldots ,n\},c\in \{x,y\}\big \} \\ \varSigma ^{\textsc {nohalt}}=\ {}&\varSigma ^{\textsc {inc} \textsc {dec}}\cup \varSigma ^{\textsc {goto}}\\ \varSigma =\ {}&\varSigma ^{\textsc {nohalt}}\cup \big \{\textsc {halt} \big \} \end{aligned}$$

When ${\mathcal {A}}$ and ${\mathcal {B}}$ read a word $w\in \varSigma ^+$, they intuitively simulate a sequence of commands $\tau _u$ that induces the command trace $u=\textsc {pref} _{\textsc {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:\varSigma ^{\textsc {nohalt}}\rightarrow \mathbb {N}$ and partial weight functions $\gamma _p,\gamma _d:\varSigma ^{\textsc {nohalt}}\rightarrow \mathbb {Q}$.

$$ \rho _p(\sigma )={\left\{ \begin{array}{ll} 5 &{} \sigma =\textsc {inc} (x)\\ 4 &{} \sigma =\textsc {dec} (x)\\ 7 &{} \sigma =\textsc {inc} (y)\\ 6 &{} \sigma =\textsc {dec} (y)\\ 15 &{} \text {otherwise} \end{array}\right. } ~~~~~ \rho _d(\sigma )={\left\{ \begin{array}{ll} 4 &{} \sigma =\textsc {inc} (x)\\ 5 &{} \sigma =\textsc {dec} (x)\\ 6 &{} \sigma =\textsc {inc} (y)\\ 7 &{} \sigma =\textsc {dec} (y)\\ 15 &{} \text {otherwise} \end{array}\right. } $$

$\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

$$\begin{aligned} \rho _p(\textsc {inc} (c))=\rho _d(\textsc {dec} (c))>\rho _p(\textsc {dec} (c))=\rho _d(\textsc {inc} (c)) \end{aligned}$$

(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 $\textsc {inc} (c)$ letters than of $\textsc {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 \varSigma ,\{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 $\varSigma ^{\textsc {nohalt}}$ with weights and discount factors according to the primal functions, and a transition $(q_{\mathcal {A}},\textsc {halt}, q_{\mathcal {A}}^h)$ with weight of $\frac{14}{15}$ and a discount factor of 15.

Fig. 3.

The DMDA ${\mathcal {A}}$ constructed for the proof of Lemma 2.

The integral NMDA ${\mathcal {B}}=\langle \varSigma ,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_{\textsf{freeze}},q_{\textsf{halt}}\in Q_{\mathcal {B}}$ such that for all $\sigma \in \varSigma$, there are 0-weighted transitions $(q_{\textsf{freeze}},\sigma ,q_{\textsf{freeze}})\in \delta _{\mathcal {B}}$ and $(q_{\textsf{halt}},\sigma ,q_{\textsf{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_{\textsf{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_{\textsf{HC}}$ has self loops identical to those of ${\mathcal {A}}$’s initial state, a transition to $q_{\textsf{halt}}$ over halt with a weight higher than the corresponding weight in ${\mathcal {A}}$, and a transition to the state $q_{\textsf{last}}$ over every letter that is not halt, “guessing” that the run ends without a halt command.

Fig. 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 $\textsc {dec} (c)$ than $\textsc {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 $\textsc {dec} (c)$ commands when compared to ${\mathcal {A}}$.

Fig. 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 $\textsc {inc} (c)$ than $\textsc {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.

Fig. 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 $\textsc {inc} (x)$, then from state $q_2$, which is associated with $l_2$, we move with the letter $\textsc {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.

Fig. 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_{\textsf{halt}}$ and $q_{\textsf{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 $\textsc {goto }l_k$ command (meaning $l_j=\sigma =\textsc {goto }l_k$), k is the next location after j and $l_j$ is an $\textsc {inc}$ or a $\textsc {dec}$ command (meaning $k=j+1$ and $l_j=\sigma \in \varSigma ^{\textsc {inc} \textsc {dec}}$), $l_j$ is an $\textsc {if}\ c=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$ command with $\sigma =(\textsc {goto }l_k,c=0)$, or $l_j$ is an $\textsc {if}\ c=0\ \textsc {goto}\ l_s\ \textsc {else}\ \textsc {goto}\ l_k$ command with $\sigma =(\textsc {goto }l_k,c>0)$. The weights and discount factors of the $\varSigma ^{\textsc {nohalt}}$ transitions mentioned above are according to the primal functions $\gamma _p$ and $\rho _p$ respectively. For every location j such that $l_j=\textsc {halt}$, there is a transition from $q_j$ to $q_{\textsf{halt}}$ labeled by the letter $\textsc {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_{\textsf{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 $\textsc {if}\ c=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$ command, if the jump $\textsc {goto }l_k$ is taken, then the value of c is indeed 0.

Fig. 8.

The Zero-Jump Checker (for a counter $c\in \{x,y\}$) in the NMDA ${\mathcal {B}}$.

Intuitively, $q_{\textsf{ZC}}^c$ profits from words that have more $\textsc {inc} (c)$ than $\textsc {dec} (c)$ letters, while $q_c$ continues like ${\mathcal {A}}$. If the move to $q_c$ occurred after a balanced number of $\textsc {inc} (c)$ and $\textsc {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 $\textsc {if}\ c=0\ \textsc {goto}\ l_k\ \textsc {else}\ \textsc {goto}\ l_{k'}$ command, if the jump $\textsc {goto }l_{k'}$ is taken, then the value of c is indeed greater than 0.

Fig. 9.

The Positive-Jump Checker (for a counter c) in the NMDA ${\mathcal {B}}$.

Intuitively, if the counter is 0 on a $(\textsc {goto }l_{k'},c>0)$ command when there was no $\textsc {inc} (c)$ command yet, the gadget benefits by moving from $q_\textsf{PC0}^c$ to $q_{\textsf{freeze}}$. If there was an $\textsc {inc} (c)$ command, it benefits by having the dual functions on the move from $q_\textsf{PC0}^c$ to $q_\textsf{PC1}^c$ over $\textsc {inc} (c)$ and the primal functions on one additional self loop of $q_\textsf{PC1}^c$ over $\textsc {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 \varSigma ^+$ such that ${\mathcal {B}}(w)\ge {\mathcal {A}}(w)$ iff there exists a word $w\in \varSigma ^+$ such that ${\mathcal {B}}(w) > {\mathcal {A}}(w)$.

The proof uses the construction presented above, and can be found in [7].

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 [31].

Theorem 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) \le {\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)\le {\mathcal {A}}(w)$ for all words w, but not to whether ${\mathcal {B}}(w) <{\mathcal {A}}(w)$ for all words w.

Theorem 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) \le {\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=\textsc {pref} _{\textsc {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)\le {\mathcal {A}}(w)$.    $\square$

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

Theorem 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)\le 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) \le {\mathcal {B}}(w)$ for all words w. Indeed, if ${\mathcal {A}}(w) \le {\mathcal {B}}(w)$ then ${\mathcal {A}}(w) \le \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 1 and 2.    $\square$

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 $\textsc {lowrun}({\mathcal {A}})$ (resp. $\textsc {highrun}({\mathcal {A}})$) = $\min$ (resp. $\max$) $\{{\mathcal {A}}(r) ~{\big |}\,r$ is an infinite run of ${\mathcal {A}}~(\text {on some word }w \in \varSigma ^\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. [10, Proof of Theorem 9]). Notice that $\textsc {lowrun}({\mathcal {A}})$ and $\textsc {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 $\textsc {lowword}({\mathcal {A}})$ (resp. $\textsc {highword}({\mathcal {A}})$)= $\min$ (resp. $\max$) $\{{\mathcal {A}}(w) ~{\big |}\,w \in \varSigma ^\omega \}$. Observe that $\textsc {lowword}({\mathcal {A}})=\textsc {lowrun}({\mathcal {A}})$, $\textsc {highword}({\mathcal {A}})\le \textsc {highrun}({\mathcal {A}})$, and for deterministic automaton, $\textsc {highword}({\mathcal {A}})=\textsc {highrun}({\mathcal {A}})$.

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

$$\begin{aligned} \textsc {lowrun}({\mathcal {A}}^q) \le {\mathcal {A}}^q(w) \le \textsc {lowrun}({\mathcal {A}}^q) + \textsc {maxdiff}(\mathsf {{\mathcal {A}}}) \end{aligned}$$

(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 \varSigma ^\omega \}$.

Proof

Consider an alphabet $\varSigma$, discount factors $\lambda _A,\lambda _D\in \mathbb {Q} \cap (1,\infty )$, a $\lambda _A$-NDA ${\mathcal {A}}=\langle \varSigma , Q_{\mathcal {A}}, \iota _{\mathcal {A}}, \delta _{\mathcal {A}}, \gamma _{\mathcal {A}} \rangle$ and a $\lambda _D$-DDA ${\mathcal {D}}=\langle \varSigma , 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 $\textsc {lowword}({\mathcal {C}})$.

When $\lambda _A\ne \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 $\textsc {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')\in \delta _{\mathcal {A}}$, let $\textsc {minval}(q,\sigma ,q')=\gamma _{\mathcal {A}}(q,\sigma ,q') + \frac{1}{\lambda _A}\cdot \textsc {lowword}({\mathcal {A}}^{q'})$ 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}= \{t=(q,\sigma ,q')\in \delta _{\mathcal {A}}~{\big |}\,\textsc {minval}(t)=\textsc {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 $\textsc {lowrun}({\mathcal {A}}^q)$ (cf. [10, 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 \varSigma ^\omega \}=\textsc {lowrun}({\mathcal {A}})-\textsc {highword}({\mathcal {D}})$. (Recall that since ${\mathcal {D}}$ is deterministic, we can easily compute $\textsc {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 \{ \textsc {minval}(t')- \textsc {minval}(t'') \ \Big |\ \begin{matrix} t'=(q,\sigma ',q')\in \delta _{\mathcal {A}}\setminus \delta _{pr},\\ t''=(q,\sigma '',q'')\in \delta _{pr}\end{matrix} \Big \}$. Observe that $m_{\mathcal {A}}> 0$.

Considering the connection between $m_{\mathcal {A}}$ and $\textsc {maxdiff}(\mathsf {{\mathcal {D}}})$, notice first that if $\textsc {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 \varSigma ^\omega \}=\textsc {lowrun}({\mathcal {A}})-\textsc {lowrun}({\mathcal {D}})$. Otherwise, meaning $\textsc {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

$$\begin{aligned} \frac{\textsc {maxdiff}(\mathsf {{\mathcal {D}}})}{{\lambda _D}^k} < \frac{m_{\mathcal {A}}}{{\lambda _A}^k} \end{aligned}$$

(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

$$\begin{aligned} {\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) \end{aligned}$$

(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 (full proof in [7]). 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 \varSigma , Q_{\mathcal {A}}\times Q_{\mathcal {D}}, \{(\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',p'))=\gamma _{\mathcal {D}}(p,\sigma ,p')$.

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)=\textsc {highrun}({\mathcal {C}}^{(\delta _{\mathcal {A}}(\psi ),\delta _{\mathcal {D}}(u))})$. This leads to

$$\begin{aligned}&\min \{{\mathcal {A}}(v)-{\mathcal {D}}(v)~{\big |}\,v\in \varSigma ^\omega \} =\\&\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 \varSigma ^k, w\in \varSigma ^\omega , \\ \psi \text { is a run of } {\mathcal {A}}\text { on } u \end{matrix} \Big \} =\\&\min _{\psi }\Bigg \{ {\mathcal {A}}(\psi ) + \frac{\textsc {lowrun}({\mathcal {A}}^{\delta _{\mathcal {A}}(\psi )})}{{\lambda _A}^k} - {\mathcal {D}}(u) - \frac{\textsc {highrun}({\mathcal {C}}^{(\delta _{\mathcal {A}}(\psi ),\delta _{\mathcal {D}}(u))})}{{\lambda _D}^k}\Big | \begin{matrix} u\in \varSigma ^k, \\ \psi \text { is a run}\\ \text {of } {\mathcal {A}}\text { on } u \end{matrix} \Bigg \} \end{aligned}$$

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 $\textsc {maxval}(p,\sigma ,p')=\gamma _{\mathcal {D}}(p,\sigma ,p') + \frac{1}{\lambda _D}\cdot \textsc {highword}({\mathcal {D}}^{p'})$, instead of $\textsc {minval}(q,\sigma ,q')$.

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

• k should be the minimal integer such that $\frac{\textsc {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 then calculate $\textsc {lowrun}({\mathcal {C}}^{(\delta _{\mathcal {A}}(\psi ),\delta _{\mathcal {D}}(u))})$ for every k-sized run of ${\mathcal {A}}$, $\psi$, and conclude that $\min \{{\mathcal {A}}-{\mathcal {D}}\}$ is equal to $\min _{\psi }\{ {\mathcal {A}}(\psi ) + \frac{\textsc {lowrun}({\mathcal {C}}^{(\delta _{\mathcal {A}}(\psi ),\delta _{\mathcal {D}}(u))})}{{\lambda _A}^k} - {\mathcal {D}}(u) - \frac{\textsc {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).

   $\square$

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 $\textsc {highword}({\mathcal {D}}^{p})$ in the case that $\lambda _A>\lambda _D$.

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

Lemma 4

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 \{{\mathcal {A}}(u)-{\mathcal {D}}(u) ~{\big |}\,u \in \varSigma ^+\}$, 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 $\varSigma$, a discount factor $\lambda \in \mathbb {Q} \cap (1,\infty )$, and a $\lambda$-NDA (DDA) ${\mathcal {N}}=\langle \varSigma , 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{\varSigma }, Q_{\mathcal {N}}\cup \{q_\tau \}, \iota _{\mathcal {N}}, \delta _{\hat{{\mathcal {N}}}}, \gamma _{\hat{{\mathcal {N}}}} \rangle$ on infinite words. The new alphabet $\hat{\varSigma }=\varSigma \cup \{\tau \}$ contains a new letter $\tau \notin \varSigma$ 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 \{(q_\tau ,\sigma , q_\tau ~{\big |}\,\sigma \in \hat{\varSigma })\} \cup \{(q,\tau , q_\tau ~{\big |}\,q\in Q_{\mathcal {N}}\setminus \iota _{\mathcal {N}})\}$, and

$\gamma _{\hat{{\mathcal {N}}}}(t) = {\left\{ \begin{array}{ll} \gamma _{\mathcal {N}}(t) &{} t \in \delta _{\mathcal {N}}\\ 0 &{} \text {otherwise} \end{array}\right. }$

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

• 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. 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. 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 \{{\mathcal {N}}^q(r)~{\big |}\,r \text { is a run of }{\mathcal {N}}^q\} =\textsc {lowrun}({\hat{{\mathcal {N}}}}^q)$ and $\sup \{{\mathcal {N}}^q(r)~{\big |}\,r \text { is a run of }{\mathcal {N}}^q\} =\textsc {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 $\textsc {lowrun}({\hat{{\mathcal {N}}}}^q)$ is attained by an infinite run taking a $\tau$ transition. We calculate $\textsc {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 $\textsc {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')\in \delta _{pr}$ to some marked state $q'$. The process terminates when an iteration has no new states to mark. Analogously, we can determine whether $\textsc {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 \{{\mathcal {A}}(u)-{\mathcal {D}}(u)~{\big |}\,u\in \varSigma ^+\} = \min \{\hat{{\mathcal {A}}}(w)-\hat{{\mathcal {D}}}(w) ~{\big |}\,w \in \varSigma ^\omega \}$, and that $\inf \{{\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 $\textsc {lowrun}$ or $\textsc {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 \{{\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 $\textsc {lowrun}$ and $\textsc {highrun}$ are attainable.    $\square$

Complexity analysis We show below that the algorithm of Lemmas 3 and 4 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 (proof appears in [7]).

Lemma 5

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)}$.

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\le S, p\le S, M\le 2\cdot 2^S$, $\frac{\lambda _{\mathcal {D}}}{\lambda _D - 1} \le \frac{{p_{\mathcal {D}}}}{{p_{\mathcal {D}}}-{q_{\mathcal {D}}}} \le {p_{\mathcal {D}}} \le 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}}} \ge 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 5, 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

$$\begin{aligned} m_{\mathcal {A}}&= \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}} \\ {}&\ge \frac{1}{{p}^{3n}} \ge \frac{1}{{S}^{3S}} {\mathop {>}\limits ^{\text {for } S \ge 1}} \frac{1}{({2^S})^{3S}} = \frac{1}{2^{3S^2}} \end{aligned}$$

for some $x_1, x_2, y_1, y_2\le 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 $\textsc {maxdiff}(\mathsf {{\mathcal {D}}})\le M\cdot \frac{\lambda _{{\mathcal {D}}}}{\lambda _{{\mathcal {D}}}-1}$, hence

$$\begin{aligned} \frac{\textsc {maxdiff}(\mathsf {{\mathcal {D}}})}{m_{\mathcal {A}}} \le \frac{M\cdot \frac{\lambda _{{\mathcal {D}}}}{\lambda _{{\mathcal {D}}}-1}}{m_{\mathcal {A}}} \le \frac{2^{1+S}\cdot S}{m_{\mathcal {A}}} {\mathop {<}\limits ^{(\text {for } S \ge 1)}} \frac{2^{3S}}{m_{\mathcal {A}}} < 2^{3S+3S^2} \end{aligned}$$

Recall that we unfold the computation tree until level k, which is the minimal integer such that $(\frac{\lambda _D}{\lambda _A})^k > \frac{\textsc {maxdiff}(\mathsf {{\mathcal {D}}})}{m_{\mathcal {A}}}$. Observe that for $S\ge 1$ we have $\big (\frac{\lambda _{{\mathcal {D}}}}{\lambda _{{\mathcal {A}}}}\big )^{S^2} \ge \big (1 + \frac{1}{S^2}\big )^{S^2}\ge 2$, hence for $k'=S^2\cdot (3S+3S^2)$, we have

$$\big (\frac{\lambda _D}{\lambda _A}\big )^{k'} = \big ((\frac{\lambda _D}{\lambda _A})^{S^2}\big )^{3S+3S^2} \ge 2^ {3S+3S^2} > \frac{\textsc {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{\textsc {lowrun}({\mathcal {A}}^{\delta _{\mathcal {A}}(\psi )})}{{\lambda _A}^k} - {\mathcal {D}}(u) - \frac{\textsc {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)\le k \log _2(S)$, requiring polynomial space.

We thus get the following complexity result.

Theorem 4

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) \ge {\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 4 in the case of finite words, checking whether $\min \{{\mathcal {A}}(w)-{\mathcal {D}}(w)\} < 0$ and whether $\min \{{\mathcal {A}}(w)-{\mathcal {D}}(w)\} \le 0$. In the case of finite words, we also use the information of whether there is an actual word that gets the desired value.    $\square$

Since integral NDAs can always be determinized [8], 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) \ge {\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.