On Delay and Regret Determinization of Max-Plus Automata

TL;DR

This paper investigates the decidability of determinizing weighted automata over a specific semiring by introducing k-delay and r-regret constraints, establishing complexity results and equivalences with the general problem.

Contribution

It introduces k-delay and r-regret determinization notions for weighted automata and proves their equivalence to general determinization, along with complexity classifications.

Findings

Decidability of determinization is linked to k-delay determinization.

k-delay and r-regret problems are EXPtime-complete.

Determining r-regret determinizability is in EXPtime.

Abstract

Decidability of the determinization problem for weighted automata over the semiring $(\mathbb{Z} \cup {-\infty}, \max, +)$, WA for short, is a long-standing open question. We propose two ways of approaching it by constraining the search space of deterministic WA: k-delay and r-regret. A WA N is k-delay determinizable if there exists a deterministic automaton D that defines the same function as N and for all words {\alpha} in the language of N, the accepting run of D on {\alpha} is always at most k-away from a maximal accepting run of N on {\alpha}. That is, along all prefixes of the same length, the absolute difference between the running sums of weights of the two runs is at most k. A WA N is r-regret determinizable if for all words {\alpha} in its language, its non-determinism can be resolved on the fly to construct a run of N such that the absolute difference between its value and the value assigned to {\alpha} by N is at most r. We show that a WA is determinizable if and only if it is k-delay determinizable for some k. Hence deciding the existence of some k is as difficult as the general determinization problem. When k and r are given as input, the k-delay and r-regret determinization problems are shown to be EXPtime-complete. We also show that determining whether a WA is r-regret determinizable for some r is in EXPtime.

Equations

$$\left|w(q_0{a}_0\dots a_{\ell -1}{q}_{\ell })-w^{\prime }(q_0^{\prime }{a}_0\dots a_{\ell -1}{q}_{\ell }^{\prime })\right|>\chi$$

$$\left|{\sum }_{\ell =0}^j{w}^{\prime }((q_{\ell },i_{\ell }),a_{\ell },(q_{\ell +1},i_{\ell +1}))-{\sum }_{\ell =0}^{j}w(q_{\ell },a_{\ell },q_{\ell +1})\right|$$

$$=$$

$${\sum }_{l=0}^j\left(w(q_l,a_l,q_{l+1})-w^{\prime \prime }(p_l,a_l,p_{l+1})\right)\in \{-k,\dots ,k\}.$$

$$w^{\prime }((q_j,i_j),a_j,(q_{j+1},i_{j+1}))$$

$$=$$

$$\begin{array}[]{lll}&&|(4k+1)w(q_{i-1}a_{i-1}q_{i})-w^{\prime}(q_{i-1}^{\prime}a_{i-1}q_{i}^{\prime})|\\ &=&|(4k+1)w(q_{0}\dots q_{i})-(4k+1)w(q_{0}\dots q_{i-1})-w^{\prime}(q_{0}^{\prime}\dots q_{i}^{\prime})+w^{\prime}(q_{0}^{\prime}\dots q_{i-1}^{\prime})|\\ &\leq&|(4k+1)w(q_{0}\dots q_{i})-w^{\prime}(q_{0}^{\prime}\dots q_{i}^{\prime})|+|w^{\prime}(q_{0}^{\prime}\dots q_{i-1}^{\prime})-(4k+1)w(q_{0}\dots q_{i-1})|\leq 2k,\end{array}$$

$$\mathsf{dom}(\mathcal{U})=\{a_0{a}_1\dots a_n\mid a_0\#a_1\#\dots \#a_n\#\in {\mathcal{L}}_{\mathcal{D}}\}.$$

$$m_q=max\{w+\mu \mid (p,w)\in g,w(p,a,q)=\mu \}.$$

$$w(p_0{a}_0{p}_1\dots a_{i-1}{p}_i)\ge w({\varrho }_q)-B.$$

$$\begin{array}[]{lll}w(\varrho^{\prime}aq)&=&w(\varrho^{\prime})+w(p,a,q)\\ &=&w_{n-1}+g_{n-1}(p)+w(p,a,q)\\ &=&w_{n}-w^{\prime}(g_{n-1},a,g_{n})+{}\\ &&g_{n-1}(p)+w(p,a,q)\\ &=&w_{n}+g_{n}(q).\end{array}$$

$$w_{n-1}+g_{n-1}(p_{n-1})\ge w({\varrho }^{\prime }).$$

$$w^{\prime }(g_{n}a{g}_{n+1})+g_n(p_n)\ge w(p_{n-1}a{p}_n)+g_{n-1}(p_{n-1}).$$

$$\begin{array}[]{lll}w_{n}+g_{n}(p_{n})&=&w_{n-1}+w^{\prime}(g_{n}ag_{n+1})+g_{n}(p_{n})\\ &\geq&w_{n-1}+g_{n-1}(p_{n-1})+w(q_{n-1}ap_{n})\\ &\geq&w(\varrho^{\prime})+w(q_{n-1}ap_{n})\\ &=&w(\varrho).\end{array}$$

$$\mathsf{Val}(\sigma (\alpha ))=\mathsf{Val}({\varrho }^{\prime })=\mathsf{Val}(\varrho )=[[\mathcal{D}]](\alpha )=[[\mathcal{N}]](\alpha ).$$

$$(p_0,q_0)(p_0,q_0,q_1,a_0)\dots (p_{n-1},q_{n-1},q_n,a_{n-1})$$

$$\phi =(p_0,t_0)(p_0,t_0,a_0)(p_0,t_0,p_1,a_0)(p_1,t_1)\dots (p_n,t_n)$$

$${\phi }^{\prime }=(p_1,t_1)(p_1,t_1,a_1)(p_1,t_1,p_2,a_1)(p_2,t_2)\dots (p_n,t_n)$$

$$c_1\le c_0+w(p_0,a,p_1)-w(t_0,a,t_1).$$

$$\begin{array}[]{lll}\mathsf{EL}_{c_{0}}(\varphi)&=&\mathsf{EL}_{0}(\varphi)+c_{0}\\ &=&\mathsf{EL}_{0}(\varphi^{\prime})+c_{0}+w(p_{0},a,p_{1})-w(t_{0},a,t_{1})\\ &\geq&c_{0}-c_{1}+w(p_{0},a,p_{1})-w(t_{0},a,t_{1})\\ &\geq&0,\end{array}$$

$$(p_0,q_0)(p_0,q_0,q_1,a_0)\dots (p_{n-1},q_{n-1},q_n,a_{n-1})$$

Full text

We show that a WA is determinizable if and only if it is $k$-delay determinizable for some $k$. Hence deciding the existence of some $k$ is as difficult as the general determinization problem. When $k$ and $r$ are given as input, the $k$-delay and $r$-regret determinization problems are shown to be \EXP-complete. We also show that determining whether a WA is $r$-regret determinizable for some $r$ is in \EXP.

1 Introduction

Weighted automata. Weighted automata generalize finite automata with weights on transitions [DKV09]. They generalize word languages to partial functions from words to values of a semiring. First introduced by Schützenberger and Chomsky in the 60s, they have been studied for long [DKV09], with applications in natural language and image processing for instance. More recently, they have found new applications in computer-aided verification as a measure of system quality through quantitative properties [CDH10], and in system synthesis, as objectives for quantitative games [FGR12]. In this paper, we consider weighted automata $\mathcal{N}$ over the semiring $(\mathbb{Z}\cup\{-\infty\},\max,+)$, and just call them weighted automata (WA). The value of a run is the sum of the weights occurring on its transitions, and the value of a word is the maximal value of all its accepting runs. Absent transitions have a weight of $-\infty$ and runs of value $-\infty$ are considered non-accepting. This defines a partial function denoted $\llbracket\mathcal{N}\rrbracket:\Sigma^{*}\rightarrow\mathbb{Z}$ whose domain is denoted by $\mathcal{L}_{\mathcal{N}}$.

Determinization problem. Most of the good algorithmic properties of finite automata do not transfer to WA. Notably, the (quantitative) language inclusion $\llbracket\mathcal{A}\rrbracket\leq\llbracket\mathcal{B}\rrbracket$ is undecidable for WA [Kro92] (see also [DGM16] and [ABK11] for different proofs based on reductions from the halting problem for two-counter machines). This has triggered research on sub-classes or other formalisms for which this problem becomes decidable [FGR14, CE*+*10]. This includes the class of deterministic WA (DWA, also known as sequential WA in the literature), which are the WA whose underlying (unweighted) automaton is deterministic. Another scenario where it is desirable to have a DWA is the quantitative synthesis problem, undecidable even for unambiguous WA, yet decidable for DWA [FGR12]. However, and in contrast with finite unweighted automata, WA are not determinizable in general. For instance, the function which outputs the maximal value between the number of $a$’s and the number of $b$’s in a word $\alpha\in\{a,b\}^{*}$ is not realizable with a DWA. This motivates the determinization problem: given a WA $\mathcal{N}$, is it determinizable? I.e. is there a DWA defining the same (partial) function as $\mathcal{N}$?

The determinization problem for computational models is fundamental in theoretical computer science. For WA in particular, it is sometimes more natural (and at least exponentially more succinct) to specify a (non-deterministic) WA, even if some equivalent DWA exists. If the function is specified in a weighted logic equivalent to WA, such as weighted MSO [DG07], the logic-to-automata transformation may construct a non-deterministic, but determinizable, WA. However, despite many research efforts, the largest class for which this problem is known to be decidable is the class of polynomially ambiguous WA [KL09], and the decidability status for the full class of WA is a long-standing open problem. Other contributions and approaches to the determinization problem include the identification of sufficient conditions for determinizability [Moh97], approximate determinizability (for unambiguous WA) where the DWA is required to produce values at most $t$ times the value of the WA, for a given factor $t$ [AKL13], and (incomplete) approximation algorithms when the weights are non-negative [CD16].

Bounded-delay & regret determinizers. In this paper, we adopt another approach that consists in constraining the class of DWA that can be used for determinization. More precisely, we define a class of DWA $\mathfrak{C}$ as a function from WA to sets of DWA, and say that a DWA $\mathcal{D}$ is a $\mathfrak{C}$-determinizer of a WA $\mathcal{N}$ if

$(i)$ $\mathcal{D}\in\mathfrak{C}(\mathcal{N})$and

$(ii)$ $\llbracket\mathcal{N}\rrbracket=\llbracket\mathcal{D}\rrbracket$.

Then, $\mathcal{N}$ is said to be $\mathfrak{C}$-deteminizable if it admits a ${\mathfrak{C}}$-determinizer. If ${\bf DWA}$ denotes the function mapping any WA to the whole set of DWA, then obviously the ${\bf DWA}$-determinization problem is the general (open) determinization problem. In this paper, we consider two restrictions.

First, given a bound $k\in\mathbb{N}$, we look for the class of $k$-delay DWA ${\bf Del}_{k}$, which maintain a strong relation with the sequence of values along some accepting run of the non-deterministic automaton. More precisely, a DWA $\mathcal{D}$ belongs to ${\bf Del}_{k}(\mathcal{N})$ if for all words $\alpha\in\mathcal{L}_{\mathcal{D}}$, there is an accepting run $\varrho$ of $\mathcal{N}$ with maximal value such that the running sum of the prefixes of $\varrho$ and the running sum of the prefixes of the unique run $\varrho_{\mathcal{D}}$ of $\mathcal{D}$ on $\alpha$ are constantly close in the following sense: for all lengths $\ell$, the absolute value of the difference of the value of the prefix of $\varrho$ of length $\ell$ and the value of the prefix of $\varrho_{\mathcal{D}}$ of length $\ell$ is at most $k$. Then the ${\bf Del}_{k}$-determinization problem amounts to deciding whether there exists ${\mathcal{D}}\in{\bf Del}_{k}$ such that $\llbracket\mathcal{N}\rrbracket=\llbracket\mathcal{D}\rrbracket$. And if $k$ is left unspecified, it amounts to decide whether there exists ${\mathcal{D}}\in\bigcup_{k\in{\mathbb{N}}}{\bf Del}_{k}(\mathcal{N})$ such that $\llbracket\mathcal{N}\rrbracket=\llbracket\mathcal{D}\rrbracket$. We note ${\bf Del}$ the function mapping any WA $\mathcal{N}$ to $\bigcup_{k}{\bf Del}_{k}(\mathcal{N})$. We will show that the ${\bf Del}_{k}$-determinization problem is complete for \EXP, and the ${\bf Del}$-determinization problem is equivalent to the general (unconstrained) determinization problem.

The notion of delay has been central in many works on automata with outputs. For instance, it has been a key notion in transducer theory (automata with word outputs) for the determinization and the functionality problems [BCPS03], and the decomposition of finite-valued transducers [SdS08]. The notion of delay has been also used in the theory of WA, for instance to give sufficient conditions for determinizability [Moh97] or for the decomposition of finite-valued group automata [FGR14].

Example 1**.**

Let $A=\{a,b\}$ and $k\in\mathbb{N}$. The left automaton of Fig. 1 maps any word in $AaA^{*}$ to [math], and any word in $AbA^{*}$ to $1$. It is ${\bf Del}_{k}$-determinizable by the right automaton of Fig. 1. After one step, the delay of the DWA is $k$ with both transitions of the left WA. After two or more steps, the delay is always [math]. It is not ${\bf Del}_{j}$-determinizable for any $j<k$. (A second example of a bounded-delay determinizable automaton is shown in Fig. 2.)

Second, we consider the class $\mathbf{Hom}$ of so-called homomorphic DWA. Intuitively, any DWA $\mathcal{D}\in\mathbf{Hom}(\mathcal{N})$ maintains a close relation with the structure of $\mathcal{N}$: the existence of an homomorphism from $\mathcal{D}$ to $\mathcal{N}$. An alternative definition is that of a [math]-regret game [HPR16] played on $\mathcal{N}$: Adam chooses input symbols one by one (forming a word $\alpha\in\mathcal{L}_{\mathcal{N}}$), while Eve reacts by choosing transitions of $\mathcal{N}$, thus constructing a run $\varrho$ of ${\mathcal{N}}$ on the fly (i.e. without knowing the full word $\alpha$ in advance). Eve wins the game if $\varrho$ is accepting and its value is equal to $\llbracket\mathcal{N}\rrbracket(\alpha)$, i.e. $\varrho$ is a maximal accepting run on $\alpha$. Then, any (finite memory) winning strategy for Eve can be seen as a $\mathbf{Hom}$-determinizer of $\mathcal{N}$ and conversely. This generalizes the notion of good-for-games automata, which do not need to be determinized prior to being used as observers in a game, from the Boolean setting [HP06] to the quantitative one. In some sense, $\mathbf{Hom}$-determinizable WA are “good for quantitative games”: when used as an observer in a quantitative game, Eve’s strategy can be applied on the fly instead of determinizing the WA and constructing the synchronized product of the resulting DWA with the game arena. This notion has been first introduced in [AKL10] with motivations coming from the analysis of online algorithms. In [AKL10], it was shown that the $\mathbf{Hom}$-determinization problem is in ¶.

Example 2**.**

The following WA maps both $ab$ and $aa$ to [math]. It is not $\mathbf{Hom}$-determinizable because Eve has to choose whether to go left or right on reading $a$. If she goes right, then Adam wins by choosing letter $b$. If she goes left, Adam wins by picking $a$ again. However, it is almost $\mathbf{Hom}$-determinizable by the DWA obtained by removing the right part, in the sense that the function realized by this DWA is $1$-close from the original one. This motivates approximate determinization.

Approximate determinization. Approximate determinization of a WA $\mathcal{N}$ relaxes the determinization problem to determinizers which do not define exactly the same function as $\mathcal{N}$ but approximate it. Precisely, for a class $\mathfrak{C}$ of DWA, $\mathcal{D}$ a DWA and $r\in\mathbb{N}$, we say that $\mathcal{D}$ is an $(r,\mathfrak{C})$-determinizer of $\mathcal{N}$ if

$(i)$ $\mathcal{D}\in\mathfrak{C}(\mathcal{N})$,

$(ii)$ $\mathcal{L}_{\mathcal{D}}=\mathcal{L}_{\mathcal{N}}$and

$(iii)$ for all words $\alpha\in\mathcal{L}_{\mathcal{N}}$, $|\llbracket\mathcal{N}\rrbracket(\alpha)-\llbracket\mathcal{D}\rrbracket(\alpha)|\leq r$.

Then, $\mathcal{N}$ is $(r,\mathfrak{C})$-determinizable if it admits some $(r,\mathfrak{C})$-determinizer, and it is approximately $\mathfrak{C}$-determinizable if it is $(r,\mathfrak{C})$-determinizable for some $r$.

As Example 2 shows, there are WA that are approximately $\mathbf{Hom}$-determinizable but not $\mathbf{Hom}$-determinizable, making this notion appealing for the class of homomorphic determinizers. However, there are classes $\mathfrak{C}$ for which a WA is approximately $\mathfrak{C}$-determinizable if and only if it is $\mathfrak{C}$-determinizable, making approximate determinization much less interesting for such classes. This is the case for classes $\mathfrak{C}$ which are complete for determinization (Theorem 1), in the sense that any determinizable WA is also $\mathfrak{C}$-determinizable. Obviously, the class $\mathbf{DWA}$ is complete for determinization, but we show it is also the case for the class of bounded-delay determinizers $\mathbf{Del}$ (Theorem 2). Therefore, we study approximate determinization for the class of homomorphic determinizers only. We call such determinizers $r$-regret determinizers, building on the regret game analogy given above. Indeed, a WA $\mathcal{N}$ is $(r,\mathbf{Hom})$-determinizable if and only if Eve wins the regret game previously defined, with the following modified winning condition: the run that she constructs on the fly must be such that $|\llbracket\mathcal{N}\rrbracket(\alpha)-\llbracket\mathcal{D}\rrbracket(\alpha)|\leq r$, for all words $\alpha\in\mathcal{L}_{\mathcal{N}}$ that Adam can play. We say that a WA $\mathcal{N}$ is approximately $\mathbf{Hom}$-determinizable if there exists a $r\in\mathbb{N}$ such that $\mathcal{N}$ is $(r,\mathbf{Hom})$-determinizable.

Contributions. We show that the ${\bf Del}_{k}$-determinization problem problem is \EXP-complete, even when $k$ is fixed (Theorems 3 and 4). We also show that the class $\mathbf{Del}$ is complete for determinization, i.e. any determinizable WA $\mathcal{N}$ is $k$-delay determinizable for some $k$ (Theorem 2). This shows that solving the $\mathbf{Del}$-determinization problem would solve the (open) general determinization problem. This also gives a new (complete) semi-algorithm for determinization, which consists in testing for the existence of $k$-delay determinizers for increasing values $k$. We exhibit a family of bounded-delay determinizable WA, for delays which depend exponentially on the WA. Despite our efforts, exponential delays are the highest lower bound we have found. Interestingly, finding higher lower bounds would lead to a better understanding of the determinization problem, and proving that one of these lower bound is also an upper bound would immediately give decidability. To decide ${\bf Del}_{k}$-determinization, we provide a reduction to $\mathbf{Hom}$-determinization (i.e. [math]-regret determinization), which is known to be decidable in polynomial time [AKL10].

We show that the approximate $\mathbf{Hom}$-determinization problem is decidable in exponential time (Theorem 7), a problem which was left open in [AKL10]. This result is based on a non-trivial extension to the quantitative setting of a game tool proposed by Kuperberg and Skrzypczak in [KS15] for Boolean automata. In particular, our quantitative extension is based on energy games [BFL*+*08] while parity games are sufficient for the Boolean case. If $r$ is given (in binary) the $(r,\mathbf{Hom})$-determinization problem is shown to be \EXP-complete (Theorems 5 and 8). The hardness holds even if $r$ is given in unary. In the course of establishing our results, we also show that every WA $A$ that is approximately $\mathbf{Hom}$-determinizable is also exactly determinizable but there may not be a homomorphism from a deterministic version of the automaton to the original one (Lemma 22 and Theorem 6). Hence, the decision procedure for approximate $\mathbf{Hom}$-determinizability can also be used as an algorithmically verifiable sufficient condition for determinizability.

Other related works. In transducer theory, a notion close to the notion of $k$-delay determinizer has been introduced in [FJLW16], that of $k$-delay uniformizers of a transducer. A uniformizer of a transducer $T$ is an (input)-deterministic transducer such that the word-to-word function it defines (seen as a binary relation) is included in the relation defined by $T$, and any of its accepting runs should be $k$-delay close from some accepting run of $T$. While the notion of $k$-delay uniformizer in transducer theory is close to the notion of $k$-delay determinizer for WA, the presence of a max operation in WA makes the $k$-delay determinization problem conceptually harder.

2 Preliminaries

We denote by $\mathbb{Z}$ the set of all integers; by $\mathbb{N}$, the set of all non-negative integers, i.e. the natural numbers—including [math]; by $\mathbb{S}_{\lhd x}$, the subset $\{s\in\mathbb{S}\>\mid\>s\lhd x\}$ of any given set $\mathbb{S}$. Finally, by $\varepsilon$ we denote the empty word over any alphabet.

Automata. A (non-deterministic weighted finite) automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$ consists of a finite set $Q$ of states, a set $I\subseteq Q$ of initial states, a finite alphabet $A$ of symbols, a transition relation $\Delta\subseteq Q\times A\times Q$, a weight function $w:\Delta\rightarrow\mathbb{Z}$, and a set $F\subseteq Q$ of final states. By $w_{\max}$ we denote the maximal absolute value of a transition weight, i.e. $w_{\max}:=\max_{\delta\in\Delta}|w(\delta)|$. We say $\mathcal{N}$ is pair-deterministic if $|I|=1$ and for all $(q,a)\in Q\times A$ we have that $(q,a,q_{1}),(q,a,q_{2})\in\Delta$ implies $q_{1}=q_{2}$ or $w(q,a,q_{1})\neq w(q,a,q_{2})$; deterministic, if $|I|=1$ and for all $(q,a)\in Q\times A$ we have that $(q,a,q_{1}),(q,a,q_{2})\in\Delta$ implies $q_{1}=q_{2}$.

A run of $\mathcal{N}$ on a word $a_{0}\dots a_{n-1}\in A^{*}$ is a sequence $\varrho=q_{0}a_{0}q_{1}\dots q_{n-1}a_{n-1}q_{n}\in(Q\cdot A)^{*}Q$ such that $(q_{i},a_{i},q_{i+1})\in\Delta$ for all $0\leq i<n$. We say $\varrho$ is initial if $q_{0}\in I$; final, if $q_{n}\in F$; accepting, if it is both initial and final. The automaton $\mathcal{N}$ is said to be trim if for all states $q\in Q$, there is a run from a state $q_{I}\in I$ to $q$ and there is a run from $q$ to some $q_{F}\in F$. The value of $\varrho$, denoted by $w(\varrho)$, corresponds to the sum of the weights of its transitions: $w(\varrho):=\sum_{i=0}^{n-1}w(q_{i},a_{i},q_{i+1}).$

The automaton $\mathcal{N}$ has the (unweighted) language $\mathcal{L}_{\mathcal{N}}=\{\alpha\in A^{*}\>\mid\>$ there is an accepting run of $\mathcal{N}\text{ on }\alpha\}$ and defines a function $\llbracket\mathcal{N}\rrbracket:\mathcal{L}_{\mathcal{N}}\to\mathbb{Z}$ as follows $\alpha\mapsto\max\{w(\varrho)\>\mid\>\varrho$ is an accepting run of $\mathcal{N}$ on $\alpha\}$. A run $\varrho$ of $\mathcal{N}$ on $\alpha$ is said to be maximal if $w(\varrho)=\llbracket\mathcal{N}\rrbracket(\alpha)$.

Determinization with delay. Given $k\in\mathbb{N}$ and two automata $\mathcal{N}=(Q,I,A,\Delta,w,F)$ and $\mathcal{N}^{\prime}=(Q^{\prime},I^{\prime},A,\Delta^{\prime},w^{\prime},F^{\prime})$, we say that $\mathcal{N}$ is $k$-delay-included (or $k$-included, for short) in $\mathcal{N}^{\prime}$, denoted by $\mathcal{N}\subseteq_{k}\mathcal{N}^{\prime}$, if for every accepting run $\varrho=q_{0}a_{0}\dots a_{n-1}q_{n}$ of $\mathcal{N}$, there exists an accepting run $\varrho^{\prime}=q_{0}^{\prime}a_{0}\dots a_{n-1}q_{n}^{\prime}$ of $\mathcal{N}^{\prime}$ such that $w^{\prime}(\varrho^{\prime})=w(\varrho)$, and for every $1\leq i\leq n$, $|w^{\prime}(q_{0}^{\prime}\dots q_{i}^{\prime})-w(q_{0}\dots q_{i})|\leq k$. For an automaton $\mathcal{N}$, we denote by $\mathbf{Del}_{k}(\mathcal{N})$ the set $\{\mathcal{D}\in\mathbf{DWA}\>\mid\>\mathcal{D}\subseteq_{k}\mathcal{N}\}$.

An automaton $\mathcal{N}$ is said to be $k$-delay determinizable if there exists an automaton $\mathcal{D}\in\mathbf{Del}_{k}(\mathcal{N})$ such that $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$. Such an automaton is called a $k$-delay determinizer of $\mathcal{N}$.

Determinization with regret. Given two automata $\mathcal{N}=(Q,I,A,\Delta,w,F)$ and $\mathcal{N}^{\prime}=(Q^{\prime},I^{\prime},A,\Delta^{\prime},w^{\prime},F^{\prime})$, a mapping $\mu:Q\to Q^{\prime}$ from states in $\mathcal{N}$ to states in $\mathcal{N}^{\prime}$ is a homomorphism from $\mathcal{N}$ to $\mathcal{N}^{\prime}$ if $\mu(I)\subseteq I^{\prime}$, $\mu(F)\subseteq F^{\prime}$, $\{\left(\mu(p),a,\mu(q)\right)\>\mid\>(p,a,q)\in\Delta\}\subseteq\Delta^{\prime}$, and $w^{\prime}(\mu(p),a,\mu(q))=w(p,a,q)$. For an automaton $\mathcal{N}$, we denote by $\mathbf{Hom}(\mathcal{N})$ the set of deterministic automata $\mathcal{D}$ for which there is a homomorphism from $\mathcal{D}$ to $\mathcal{N}$. The following lemma follows directly from the preceding definitions.

Lemma 1**.**

For all automata $\mathcal{N}$, for all $\mathcal{D}\in\mathbf{Hom}(\mathcal{N})$, we have that $\mathcal{L}_{\mathcal{D}}\subseteq\mathcal{L}_{\mathcal{N}}$ and $\llbracket\mathcal{D}\rrbracket(\alpha)\leq\llbracket\mathcal{N}\rrbracket(\alpha)$ for all $\alpha\in\mathcal{L}_{\mathcal{N}}$.

Given $r\in\mathbb{N}$ and an automaton $\mathcal{N}$, we say $\mathcal{N}$ is $r$-regret determinizable if there is a deterministic automaton $\mathcal{D}$ such that:

$(i)$ $\mathcal{D}\in\mathbf{Hom}(\mathcal{N})$,

$(ii)$ $\mathcal{L}_{\mathcal{N}}=\mathcal{L}_{\mathcal{D}}$, and

$(iii)$ $\sup_{\alpha\in\mathcal{L}_{\mathcal{N}}}\left|\llbracket\mathcal{N}\rrbracket(\alpha)-\llbracket\mathcal{D}\rrbracket(\alpha)\right|\leq r$.

The automaton $\mathcal{D}$ is said to be an $r$-regret determinizer of $\mathcal{N}$. Note that (i) implies we can remove the absolute value in (iii) because of Lemma 1.

Regret games. Given $r\in\mathbb{N}$ and an automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$, an $r$-regret game is a two-player turn-based game played on $\mathcal{N}$ by Eve and Adam. To begin, Eve chooses an initial state. Then, the game proceeds in rounds as follows. From the current state $q$, Adam chooses a symbol $a\in A$ and Eve chooses a new state $q^{\prime}$ (not necessarily a valid $a$-successor of $q$). After a word $\alpha\in\mathcal{L}_{\mathcal{N}}$ has been played by Adam, he may decide to stop the game. At this point Eve loses if the current state is not final or if she has not constructed a valid run of $\mathcal{N}$ on $\alpha$. Furthermore, she must pay a (regret) value equal to $\llbracket\mathcal{N}\rrbracket(\alpha)$ minus the value of the run she has constructed.

Formally, a strategy for Adam is a finite word $\alpha\in A^{*}$ from runs to symbols and a strategy for Eve is a function $\sigma:(Q\cdot A)^{*}\to Q$ from state-symbol sequences to states. Given a word (strategy) $\alpha=a_{0}\dots a_{n-1}$, we write $\sigma(\alpha)$ to denote the sequence $q_{0}a_{0}\dots a_{n-1}q_{n}$ such that $\sigma(\varepsilon)=q_{0}$ and $\sigma(q_{0}a_{0}\dots q_{i}a_{i})=q_{i+1}$ for all $0\leq i<n$. The regret of $\sigma$ is defined as follows: $\mathbf{reg}^{\sigma}(\mathcal{N}):=\sup_{\alpha\in\mathcal{L}_{\mathcal{N}}}\llbracket\mathcal{N}\rrbracket(\alpha)-\mathsf{Val}(\sigma(\alpha))$ where, for all sequences $\varrho\in(Q\cdot A)^{*}Q$, the function $\mathsf{Val}(\varrho)$ is such that $\varrho\mapsto w(\varrho)$ if $\varrho$ is an accepting run of $\mathcal{N}$ and $\varrho\mapsto-\infty$ otherwise. We say Eve wins the $r$-regret game played on $\mathcal{N}$ if she has a strategy such that $\mathbf{reg}^{\sigma}(\mathcal{N})\leq r$. Such a strategy is said to be winning for her in the regret game.

Games & determinization. A finite-memory strategy $\sigma$ for Eve in a regret game played on an automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$ is a strategy that can be encoded as a deterministic Mealy machine $\mathcal{M}=(S,s_{I},A,\lambda_{u},\lambda_{o})$ where $S$ is a finite set of (memory) states, $s_{I}$ is the initial state, $\lambda_{u}:S\times A\to S$ is the update function and $\lambda_{o}:S\times(A\cup\{\varepsilon\})\to Q$ is the output function. The machine encodes $\sigma$ in the following sense: $\sigma(\varepsilon)=\lambda_{o}(s_{I},\varepsilon)$ and $\sigma(q_{0}a_{0}\dots q_{n}a_{n})=\lambda_{o}(s_{n},a_{n})$ where $s_{0}=s_{I}$ and $s_{i+1}=\lambda_{u}(s_{i},a_{i})$ for all $0\leq i<n$. We then say that $\mathcal{M}$ realizes the strategy $\sigma$ and that $\sigma$ has memory $|S|$. In particular, strategies which have memory $1$ are said to be positional (or memoryless).

A finite-memory strategy $\sigma$ for Eve in a regret game played on $\mathcal{N}$ defines the deterministic automaton $\mathcal{N}_{\sigma}$ obtained by taking the synchronized product of $\mathcal{N}$ and the finite Mealy machine $(S,s_{I},A,\lambda_{u},\lambda_{o})$ realizing $\sigma$. Formally $\mathcal{N}_{\sigma}$ is the automaton $(Q\times S,(\lambda_{o}(s_{I},\varepsilon),s_{I}),A,\Delta^{\prime},w^{\prime},F\times S)$ where: $\Delta^{\prime}$ is the set of all triples $\left((q,s),a,(q^{\prime},s^{\prime})\right)$ such that $(q,s)\in Q\times S,a\in A$, $s^{\prime}=\lambda_{u}(s,a)$, and $q^{\prime}=\lambda_{o}(s,a)$; and $w^{\prime}$ is such that $\left((q,s),a,(q^{\prime},s^{\prime})\right)\mapsto w(q,a,q^{\prime})$.

We remark that, for all $r\in\mathbb{N}$, for all finite-memory strategies $\sigma$ for Eve such that $\mathbf{reg}^{\sigma}(\mathcal{N})\leq r$, we have that $\mathcal{N}_{\sigma}$ is an $r$-regret determinizer of $\mathcal{N}$. Indeed, the desired homomorphism from $\mathcal{N}_{\sigma}$ to $\mathcal{N}$ is the projection on the first dimension of $Q\times S$, i.e. $(q,s)\mapsto q$. Furthermore, from any $r$-regret determinizer $\mathcal{D}$ of $\mathcal{N}$, it is straightforward to define a finite-memory strategy for Eve that is winning for her in the $r$-regret game.

Lemma 2**.**

For all $r\in\mathbb{N}$, an automaton $\mathcal{N}$ is $r$-regret determinizable if and only if there exists a finite-memory strategy $\sigma$ for Eve such that $\mathbf{reg}^{\sigma}(\mathcal{N})\leq r$.

In [AKL10] it was shown that if there exists a [math]-regret strategy for Eve in a regret game, then a [math]-regret memoryless strategy for her exists as well. Furthermore, deciding if the latter holds is in ¶. Hence, by Lemma 2 we obtain the following.

Proposition 3** (From [AKL10]).**

Determining if a given automaton is [math]-regret determinizable is decidable in polynomial time.

A sufficient condition for determinizability. Given $B\in\mathbb{N}$, we say an automaton $\mathcal{N}$ is $B$-bounded if it is trim and for every maximal accepting run $\varrho_{p}=p_{0}a_{0}p_{1}\dots a_{n-1}p_{n}$ of $\mathcal{N}$, for every $0\leq i\leq n$, and for every initial run $\varrho_{q}=q_{0}a_{0}q_{1}\dots a_{i-1}q_{i}$, we have $w(\varrho_{q})-w(p_{0}a_{0}p_{1}\dots a_{i-1}p_{i})\leq B$.

We now prove that, given a $B$-bounded automaton, we are able to build an equivalent deterministic automaton.

Proposition 4**.**

Let $B\in\mathbb{N}$ and let $\mathcal{N}=(Q,I,A,\Delta,w,F)$ be an automaton. If $\mathcal{N}$ is $B$-bounded, then there exists a deterministic automaton $\mathcal{D}$ such that $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$, and whose size and maximal weight are polynomial w.r.t. $w_{\max}$ and $B$, and exponential w.r.t. $|Q|$.

Sketch.

The result is proved by exposing the construction of the deterministic automaton $\mathcal{D}$, inspired by the determinization algorithm presented in [Moh97]. On each input word $\alpha\in A^{*}$, $\mathcal{D}$ outputs the value of the maximal initial run $\varrho_{\alpha}$ of $\mathcal{N}$ on $\alpha$ (respectively the maximal accepting run if $\alpha\in\mathcal{L}_{\mathcal{N}}$), and keeps track of all the other initial runs on $\alpha$ by storing in its state the pairs $(q,w_{q})\in Q\times\{-B,\ldots,B\}$ such that the maximal initial run on $\alpha$ that ends in $q$ has weight $w(\varrho_{\alpha})+w_{q}$. If for some state $q$ the delay $w_{q}$ gets lower than $-B$, the $B$-boundedness assumption allows $\mathcal{D}$ to drop the corresponding runs without modifying the function defined: whenever a run has a delay smaller than $-B$ with respect to $\varrho_{\alpha}$, no continuation will ever be maximal. This ensures that our construction always yields a finite automaton, unlike the determinization algorithm, that does not always terminate. ∎

On complete-for-determinization classes. Given $r\in\mathbb{N}$, a class $\mathfrak{C}$ of DWA, and an automaton $\mathcal{N}$, we say $\mathcal{N}$ is $(r,\mathfrak{C})$-determinizable if there exists $\mathcal{D}\in\mathfrak{C}(\mathcal{N})$ such that:

$(i)$ $\mathcal{L}_{\mathcal{N}}=\mathcal{L}_{\mathcal{D}}$, and

$(ii)$ $\sup_{\alpha\in\mathcal{L}_{\mathcal{N}}}\left|\llbracket\mathcal{N}\rrbracket(\alpha)-\llbracket\mathcal{D}\rrbracket(\alpha)\right|\leq r$.

We will now confirm our claim from the introduction: approximate determinization is not interesting for some classes.

Proposition 5**.**

Let $\mathcal{N}=(Q,I,A,\Delta,w,F)$ be a trim automaton such that the range of $\llbracket\mathcal{N}\rrbracket$ is included into $\{-B,\ldots,B\}$, for some $B\in\mathbb{N}$. Then $\mathcal{N}$ is determinizable.

Proof.

Let $\varrho_{p}=p_{0}a_{0}p_{1}\dots a_{n-1}p_{n}$ be a maximal accepting run of $\mathcal{N}$ and let $\varrho_{q}=q_{0}a_{0}q_{1}\dots a_{i-1}q_{i}$ be an initial run of length $i\leq n$. We define $\varrho_{p}^{i}=p_{0}a_{0}p_{1}\dots a_{i-1}p_{i}$ for $i\leq n$.

By assumption, we have $w(\varrho_{p})\geq-B$. By trimness assumption, the state $q_{i}$ can reach a final state and we have $w(\varrho_{q})-|Q|w_{\max}\leq B$ otherwise there would be an accepting run of value greater than $B$. Similarly, since state $p_{i}$ can be reached from an initial state, we have $-|Q|w_{\max}+a\leq B$, with $a=w(p_{i}a_{i}\dots a_{n-1}p_{n})=w(\varrho_{p})-w(\varrho_{p}^{i})$. By combining the three constraints, we obtain: $w(\varrho_{q})-|Q|w_{\max}-|Q|w_{\max}+a-w(\varrho_{p})\leq 3B$ which, once rearranged, yields: $w(\varrho_{q})-w(\varrho_{p}^{i})\leq 3B+2|Q|w_{\max}$. Thus, $\mathcal{N}$ is $(3B+2|Q|w_{\max})$-bounded and determinizable (by Proposition 4). ∎

Recall that a class $\mathfrak{C}$ of DWA is complete for determinization if any determinizable automaton is also $\mathfrak{C}$-determinizable.

Theorem 1**.**

Given a complete-for-determinization class $\mathfrak{C}$ of DWA, an automaton $\mathcal{N}$ is $(r,\mathfrak{C})$-determinizable, for some $r\in\mathbb{N}$, if and only if it is $\mathfrak{C}$-determinizable.

Proof.

If $\mathcal{N}$ is determinizable, then in particular it is $(r,\mathfrak{C})$-determinizable for any $r$. Conversely, let us assume that $\mathcal{D}$ is an $(r,\mathfrak{C})$-determinizer of $\mathcal{N}$, for some $r$.

Then one can construct an automaton $\mathcal{M}$ such that $\llbracket\mathcal{M}\rrbracket=\llbracket\mathcal{N}\rrbracket-\llbracket\mathcal{D}\rrbracket$ by taking the product of $\mathcal{N}$ and $\mathcal{D}$ with transitions weighted by the difference of the weights of $\mathcal{N}$ and $\mathcal{D}$. Since $\mathcal{D}$ is $r$-close to $\mathcal{N}$, the range of $\mathcal{M}$ is included in the set $\{-r,\ldots,r\}$. This means, according to Propositions 5, that $\mathcal{M}$ (once trimmed) is determinizable and that one can construct a deterministic automaton realizing $\llbracket\mathcal{D}\rrbracket+\llbracket\mathcal{M}\rrbracket=\llbracket\mathcal{N}\rrbracket$. Since $\mathfrak{C}$ is complete for determinization, the result follows. ∎

3 Deciding $k$-delay determinizability

In this section we prove that deciding $k$-delay determinizability is \EXP-complete. First, however, we show that $k$-delay determinization is complete for determinization: if a given automaton is determinizable, then there is a $k$ such that it is $k$-delay determinizable as well. Hence, exposing an upper bound for $k$ would lead to an algorithm for the general determinizability problem. We also give a family of automata for which an exponential delay is required.

3.1 Completeness for determinization

Theorem 2**.**

If an automaton $\mathcal{N}$ is determinizable, then there exists $k\in\mathbb{N}$ such that $\mathcal{N}$ is $k$-delay determinizable.

Proof.

We proceed by contradiction. Suppose $\mathcal{N}=(Q,I,A,\Delta,w,F)$ is determinizable. Denote by $\mathcal{D}=(Q^{\prime},\{q_{I}^{\prime}\},A,\Delta^{\prime},w^{\prime},F^{\prime})$ a deterministic automaton such that $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$. Let us assume, towards a contradiction, that for all $k\in\mathbb{N}$ there is no deterministic automaton $\mathcal{E}$ such that $\mathcal{E}\subseteq_{k}\mathcal{N}$ and $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{E}\rrbracket$. In particular, we have that $\mathcal{D}\not\subseteq_{\chi}\mathcal{N}$ for $\chi:=|Q||Q^{\prime}|(w_{\max}+w_{\max}^{\prime})$. This means that there is a word $\alpha=a_{0}\dots a_{n-1}\in\mathcal{L}_{\mathcal{N}}$ such that for a maximal accepting run $\varrho=q_{0}a_{0}\dots a_{n-1}q_{n}$ of $\mathcal{N}$ on $\alpha$ it holds that

[TABLE]

for some $0\leq\ell\leq n$ and $q^{\prime}_{0}a_{0}\dots a_{n-1}q^{\prime}_{n}$ the unique initial run of $\mathcal{D}$ on $\alpha$. We consider the two possibilities.

Suppose that $w(q_{0}a_{0}\dots a_{\ell-1}q_{\ell})-w^{\prime}(q^{\prime}_{0}a_{0}\dots a_{\ell-1}q^{\prime}_{\ell})>\chi$. Then, at least one final state $q_{n}$ is reachable in $\mathcal{N}$ from $q_{\ell}$, and the shortest path to it consists of at most $|Q|$ transitions. Since $\chi\geq|Q|(w_{\max}+w_{\max}^{\prime})$, $\mathcal{D}$ does not realize the same function as $\mathcal{N}$, which contradicts our hypothesis.

Suppose that $w^{\prime}(q^{\prime}_{0}a_{0}\dots a_{\ell-1}q^{\prime}_{\ell})-w(q_{0}a_{0}\dots a_{\ell-1}q_{\ell})>\chi.$ Using the fact that $\chi=|Q||Q^{\prime}|(w_{\max}+w_{\max}^{\prime})$, we expose a loop that can be pumped down to present a word mapped to different values by $\mathcal{D}$ and $\mathcal{N}$. For every $0\leq j\leq|Q||Q^{\prime}|$, let $0\leq i_{j}\leq\ell$ denote the minimal integer satisfying $w^{\prime}(q^{\prime}_{0}a_{0}\dots a_{i_{j}-1}q^{\prime}_{i_{j}})-w(q_{0}a_{0}\dots a_{i_{j}-1}q_{i_{j}})\geq j(w_{\max}+w_{\max}^{\prime})$. Then there exist $0\leq j<k\leq|Q||Q^{\prime}|$ such that $q_{i_{j}}=q_{i_{k}}$, $q^{\prime}_{i_{j}}=q^{\prime}_{i_{k}}$. Moreover, since $w_{\max}$ and $w_{\max}^{\prime}$ correspond to the maximal weights of $\mathcal{N}$ and $\mathcal{D}$ respectively, $i_{j}\neq i_{k}$ holds, and $w(q_{i_{j}}a_{i_{j}}\dots a_{i_{k}-1}q_{i_{k}})>w^{\prime}(q^{\prime}_{i_{j}}a_{i_{j}}\dots a_{i_{k}-1}q^{\prime}_{i_{k}}).$ Since $\mathcal{D}$ is deterministic, it assigns a strictly lower value than $\llbracket\mathcal{N}\rrbracket$ to the word $a_{0}\dots a_{i_{j}-1}a_{i_{k}}\dots a_{n-1}$, which contradicts our assumption that $\mathcal{D}$ realizes the same function as $\mathcal{N}$. ∎

Although we do not have an upper bound on the $k$ needed for a determinizable automaton to be $k$-delay determinizable, we are able to provide an exponentially large lower bound.

Proposition 6**.**

Given an automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$, a delay $k$ as big as $2^{\mathcal{O}(|Q|)}$ might be needed for it to be $k$-delay determinizable.

To prove the above proposition we will make use of the language of words with a $j$-pair [KZ15].

Words with a $j$-pair. Consider the alphabet $A=\{1,\dots,n\}$. Let $\alpha=a_{0}a_{1}\dots\in A^{*}$ and $j\in A$. A $j$-pair is a pair of positions $i_{1}<i_{2}$ such that $a_{i_{1}}=a_{i_{2}}=j$ and $a_{k}\leq j$, for all $i_{1}\leq k\leq i_{2}$.

Lemma 7**.**

*For all $j\in A$:

$(i)$ for all $\alpha\in A^{*}$, if $\alpha$ contains no $j$-pair, then $|\alpha|<2^{n}$;

$(ii)$ for all $j\in A$, there exists $\alpha\in A^{*}$ such that $|\alpha|=2^{n}-1$ and $\alpha$ contains no $j$-pair.

Proof.

A proof of the first claim is given by Klein and Zimmermman in [KZ15] (Theorem $1$).

To show the second claim holds as well, we can inductively construct a word with the desired property. As the base case, consider $\alpha_{1}=1$. Thus, for some $i$, there is $\alpha_{i}$ which contains no $j$-pair, contains no letter bigger than $i$, and is of length $2^{i}-1$. For the inductive step, we let $\alpha_{i}=\alpha_{i-1}i\alpha_{i-1}$. It is easy to verify that the properties hold once more. ∎

We will now focus on the function $f:A^{*}\to\mathbb{Z}$, which maps a word $\alpha$ to [math] if it contains a $j$-pair and to $-|\alpha|$ otherwise. Fig. 4 depicts the automaton $\mathcal{N}$ realizing $f$ with $3n+1$ states. Proposition 6 then follows from the following result.

Lemma 8**.**

Any determinizer of automaton $\mathcal{N}$ (see Fig. 4), which realizes the function $f$, has a delay of at least $2^{n}-1$.

Proof.

Consider a word $\alpha$ of length $2^{n}-1$ containing no $j$-pair—which exists according to Lemma 7. Further consider an arbitrary $k$-determinizer $\mathcal{D}$ for $\mathcal{N}$. We remark that $\llbracket\mathcal{D}\rrbracket(\alpha)=\llbracket\mathcal{N}\rrbracket(\alpha)=1-2^{n}$, since both automata realize $f$ and $\alpha$ does not contain a $j$-pair. It follows from Lemma 7 that $\alpha\cdot a$ contains a $j$-pair (that is, for all $a\in A$). Hence, for all $a\in A$, we have $\llbracket\mathcal{N}\rrbracket(\alpha\cdot a)=0$. Furthermore, by construction of $\mathcal{N}$, for all maximal accepting runs $q_{0}a_{0}\dots a_{|\alpha|+1}q_{|\alpha|+2}$ of $\mathcal{N}$ on $\alpha\cdot a$ we have $w(q_{0}\dots q_{i})=0$ for all $1\leq i\leq|\alpha|+2$. In particular, for $i=|\alpha|+1$, we have $\llbracket\mathcal{D}\rrbracket(\alpha)-w(q_{0}\dots q_{i})=2^{n}-1$ which proves the claim. ∎

3.2 Upper bound

We now argue that [math]-delay determinizability is in \EXP. Then, we show how to reduce (in exponential time) $k$-delay determinizability to [math]-delay determinizability. We claim that the composition of the two algorithms remains singly exponential.

Proposition 9**.**

Deciding the [math]-delay problem for a given automaton is in \EXP.

The result will follow from Propositions 3 and 12. Before we state and prove Proposition 12 we need some intermediate definitions and lemmas. The following properties of $k$-inclusion, which follow directly from the definition, will be useful later.

Lemma 10**.**

For all automata $\mathcal{N}$, $\mathcal{N}^{\prime}$, and $\mathcal{N}^{\prime\prime}$, for all $k,k^{\prime}\in\mathbb{N}$, the following hold:

if $\mathcal{N}\subseteq_{k}\mathcal{N}^{\prime}$ and $k\leq k^{\prime}$, then $\mathcal{N}\subseteq_{k^{\prime}}\mathcal{N}^{\prime}$; 2. 2.

if $\mathcal{N}\subseteq_{k}\mathcal{N}^{\prime}$ and $\mathcal{N}^{\prime}\subseteq_{k^{\prime}}\mathcal{N}^{\prime\prime}$, then $\mathcal{N}\subseteq_{k+k^{\prime}}\mathcal{N}^{\prime\prime}$; 3. 3.

if $\mathcal{N}\subseteq_{k}\mathcal{N}^{\prime}$, then $\mathcal{L}_{\mathcal{N}}\subseteq\mathcal{L}_{\mathcal{N}^{\prime}}$, and for every $\alpha\in\mathcal{L}_{\mathcal{N}}$, $\llbracket\mathcal{N}\rrbracket(\alpha)\leq\llbracket\mathcal{N}^{\prime}\rrbracket(\alpha)$.

We now show how to decide [math]-delay determinizability by reduction to [math]-regret determinizability. Let us first convince the reader that [math]-regret determinizability implies [math]-delay determinizability.

Proposition 11**.**

If an automaton $\mathcal{N}$ is [math]-regret determinizable, then it is [math]-delay determinizable.

Proof.

We have, from Lemma 2, that Eve has a finite-memory winning strategy $\sigma$ in the [math]-regret game played on $\mathcal{N}$. Then, by definition of the regret game, $\mathcal{L}_{\mathcal{N}}=\mathcal{L}_{\mathcal{N}_{\sigma}}$, and for every $\alpha\in\mathcal{L}_{\mathcal{N}}$, $\llbracket\mathcal{N}\rrbracket(\alpha)-\llbracket\mathcal{N}_{\sigma}\rrbracket(\alpha)\leq 0$, hence $\llbracket\mathcal{N}\rrbracket=\llbracket\mathcal{N}_{\sigma}\rrbracket$. Moreover, as Eve chooses a run in $\mathcal{N}$, we have $\mathcal{N}_{\sigma}\subseteq_{0}\mathcal{N}$. Therefore $\mathcal{N}_{\sigma}$ is a [math]-delay determinizer of $\mathcal{N}$. ∎

The converse of the above result does not hold in general (see Fig. 3). Nonetheless, it holds when the automaton is pair-deterministic. We now show that, under this hypothesis, an automaton is [math]-regret determinizable if and only if the automaton is [math]-delay determinizable.

Proposition 12**.**

A pair-deterministic automaton $\mathcal{N}$ is [math]-delay determinizable if and only if it is [math]-regret determinizable.

Sketch.

If $\mathcal{N}$ is [math]-regret determinizable, then $\mathcal{N}$ is [math]-delay determinizable by Proposition 11. Now suppose that $\mathcal{N}$ is [math]-delay determinizable, and let $\mathcal{D}$ be a [math]-delay determinizer of $\mathcal{N}$. For every initial run $\varrho_{\alpha}=p_{0}a_{0}p_{1}\ldots a_{n-1}p_{n}$ of $\mathcal{D}$ on input $\alpha=a_{0}\ldots a_{n-1}$, there exists exactly one initial run $\varrho^{\prime}_{\alpha}=p^{\prime}_{0}a_{0}p^{\prime}_{1}\ldots a_{n-1}p^{\prime}_{n}$ of $\mathcal{N}$ such that for every $1\leq i\leq n$, $w(p_{0}^{\prime}\dots p_{i}^{\prime})=w^{\prime}(p_{0}\dots p_{i})$. The existence of $\varrho^{\prime}_{\alpha}$ is guaranteed by the fact that $\mathcal{D}$ is a [math]-delay determinizer of $\mathcal{N}$, and, since $\mathcal{N}$ is pair-deterministic, such a run is unique. Then the strategy for Eve in the [math]-regret game played on $\mathcal{N}$ obtained by following, given an input word $\alpha$, the run $\varrho^{\prime}_{\alpha}$ of $\mathcal{N}$, is winning. ∎

We observe that any automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$ can be transformed into a pair-deterministic automaton $\mathcal{P}(\mathcal{N})$ with at most an exponential blow-up in the state-space. Intuitively, we merge all the states from the original automaton which can be reached by reading $a\in A$ and taking a transition with weight $x\in\mathbb{Z}$. This is a generalization of the classical subset construction used to determinize unweighted automata. Critically, the construction is such that $\mathcal{P}(\mathcal{N})\subseteq_{0}\mathcal{N}$ and $\mathcal{N}\subseteq_{0}\mathcal{P}(\mathcal{N})$. (For completeness, the construction is given in appendix.) The next result then follows immediately from the latter property and from Lemma 10 item 2.

Proposition 13**.**

An automaton $\mathcal{N}$ is [math]-delay determinizable if and only if $\mathcal{P}(\mathcal{N})$ is [math]-delay determinizable if and only if $\mathcal{P}(\mathcal{N})$ is [math]-regret determinizable.

We now show how to extend the above techniques to the general case of $k$-delay.

Theorem 3**.**

Deciding the $k$-delay problem for a given automaton is in \EXP.

Given an automaton $\mathcal{N}$ and $k\in\mathbb{N}$, we will construct a new automaton $\delta_{k}(\mathcal{N})$ that will encode delays (up to $k$) in its state space. In this new automaton, for every state-delay pair $(p,i)$ and for every transition $(p,a,q)\in\Delta$, we will have an $a$-labelled transition to $(q,j)$ with weight $i+w(p,a,q)-j$ for all $-k\leq j\leq k$. Intuitively, $i$ is the amount of delay the automaton currently has, and to get to a point where the delay becomes $j$ via transition $(p,a,q)$ a weight of $i+w(p,a,q)-j$ must be outputted. We will then show that the resulting automaton is [math]-delay determinizable if and only if the original automaton is $k$-delay determinizable.

$k$-delay construction. Let $\mathcal{N}=(Q,I,A,\Delta,w,F)$ be an automaton. Let $\delta_{k}(\mathcal{N})=(Q^{\prime},I^{\prime},A,\Delta^{\prime},w^{\prime},F^{\prime})$ be the automaton defined as follows.

• •

$Q^{\prime}=Q\times\{-k,\dots,k\}$;

• •

$I^{\prime}=I\times\{0\}$;

• •

$\Delta^{\prime}=\{((p,i),a,(q,j))\>\mid\>(p,a,q)\in\Delta\}$;

• •

$w^{\prime}:\Delta^{\prime}\rightarrow\mathbb{Z}$, $((p,i),a,(q,j))\mapsto i+w(p,a,q)-j$;

• •

$F^{\prime}=F\times\{0\}$.

Lemma 14**.**

The $k$-delay construction satisfies the following properties.

$\delta_{k}(\mathcal{N})\subseteq_{k}\mathcal{N}$; 2. 2.

for every automaton $\mathcal{M}$ such that $\mathcal{M}\subseteq_{k}\mathcal{N}$, we have $\mathcal{M}\subseteq_{0}\delta_{k}(\mathcal{N})$; 3. 3.

$\llbracket\delta_{k}(\mathcal{N})\rrbracket=\llbracket\mathcal{N}\rrbracket$.

Proof.

1) Let $(q_{0},i_{0})a_{0}(q_{1},i_{1})\dots a_{n-1}(q_{n},i_{n})$ be an accepting run of $\delta_{k}(\mathcal{N})$. Then $q_{0}a_{0}q_{1}\dots a_{n-1}q_{n}$ is an accepting run of $\mathcal{N}$, and for every $0\leq j<n$,

[TABLE]

Therefore $\delta_{k}(\mathcal{N})\subseteq_{k}\mathcal{N}$.

2) Let $\mathcal{M}=(Q^{\prime\prime},I^{\prime\prime},A,\Delta^{\prime\prime},w^{\prime\prime},F^{\prime\prime})$ be an automaton such that $\mathcal{M}\subseteq_{k}\mathcal{N}$. For every accepting run $p_{0}a_{0}\dots a_{n-1}p_{n}$ of $\mathcal{M}$, there exists an accepting run $q_{0}a_{0}\dots a_{n-1}q_{n}$ of $\mathcal{N}$ such that for every $0\leq j<n$

[TABLE]

Let $i_{j}$ denote the above value. Then $(q_{0},i_{0})a_{0}\dots a_{n-1}(q_{n},i_{n})$ is an accepting run of $\delta_{k}(\mathcal{N})$, and for every $0\leq j<n$,

[TABLE]

Therefore $\mathcal{M}\subseteq_{0}\delta_{k}(\mathcal{N})$.

3) This property follows immediately from the first property, the second property in the particular case $\mathcal{M}=\mathcal{N}$, and Lemma 10 item 3. ∎

The next result follows immediately from the preceding Lemma and Lemma 10 item 2.

Proposition 15**.**

An automaton $\mathcal{N}$ is $k$-delay determinizable if and only if $\delta_{k}(\mathcal{N})$ is [math]-delay determinizable.

The above result raises the question of whether, for all $k$, [math]-delay determinization can be reduced to $k$-delay determinization. We give a positive answer to this question in the form of Lemma 16 in Section 3.3.

We now proceed with the proof of Theorem 3.

Proof of Theorem 3.

It should be clear that \TWOEXP membership follows from Proposition 15 and Proposition 9. We now observe that the subset construction used to decide [math]-delay determinizability need only be applied on the first component of the state space resulting from the use of the delay construction. In other words, once both constructions are applied, a state will correspond to a function $f:Q\to\{-k,\dots,k\}\cup\{\bot\}$, where $q\mapsto\bot$ signifies that $q$ is not in the subset. The size of the resulting state space is then $2^{\mathcal{O}(|Q|\log_{2}k)}$. Thus, the composition of this two constructions yields only a single exponential. ∎

3.3 Lower bound

We reduce the [math]-delay uniformization problem for synchronous transducers to that of deciding whether a given automaton is $k$-delay determinizable (for any fixed $k\in\mathbb{N}$). As the former problem is known to be \EXP-complete (see [FJLW16]), this implies the latter is \EXP-hard.

Theorem 4**.**

Deciding the $k$-delay problem for a given automaton is \EXP-hard, even for fixed $k\in\mathbb{N}$.

For convenience, we will first prove that the [math]-delay problem reduces to the $k$-delay problem for any fixed $k$. We then show the former is \EXP-hard.

Lemma 16**.**

The [math]-delay problem reduces in logarithmic space to the $k$-delay problem, for any fixed $k\in\mathbb{N}$.

Let us fix some $k\in\mathbb{N}$. Given the automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$ we denote by $x\cdot\mathcal{N}$ the automaton $(Q,I,A,\Delta,x\cdot w,F)$, where $x\cdot w$ is such that $d\mapsto x\cdot w(d)$ for all $d\in\Delta$. Lemma 16 is a direct consequence of the following.

Lemma 17**.**

For every automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$, the following statements are equivalent.

$\mathcal{N}$* is [math]-delay determinizable;* 2. 2.

$(4k+1)\cdot\mathcal{N}$* is [math]-delay determinizable;* 3. 3.

$(4k+1)\cdot\mathcal{N}$* is $k$-delay determinizable.*

Proof.

Given a [math]-delay determinizer $\mathcal{D}$ of $\mathcal{N}$, the automaton $(4k+1)\cdot\mathcal{D}$ is easily seen to be a [math]-delay determinizer of $(4k+1)\cdot\mathcal{N}$. This proves that the first statement implies the second one. Moreover, as a direct consequence of Lemma 10 item 1, the second statement implies the third one. To complete the proof, we argue that if $(4k+1)\cdot\mathcal{N}$ is $k$-delay determinizable, then $\mathcal{N}$ is [math]-delay determinizable. Let $\mathcal{D}^{\prime}=(Q^{\prime},I^{\prime},A,\Delta^{\prime},w^{\prime},F^{\prime})$ be a $k$-delay determinizer of $(4k+1)\cdot\mathcal{N}$. Let $\gamma$ be the function mapping every integer $x$ to the unique integer $\gamma(x)$ satisfying $|(4k+1)\gamma(x)-x|\leq 2k$, and let $\gamma(\mathcal{D}^{\prime})$ denote the deterministic automaton $(Q^{\prime},I^{\prime},A,\Delta^{\prime},\gamma\circ w^{\prime},F^{\prime})$. We now argue that $\gamma(\mathcal{D}^{\prime})$ is a [math]-delay determinizer of $\mathcal{N}$. For every sequence $\varrho^{\prime}=q^{\prime}_{0}a_{0}\dots a_{n-1}q^{\prime}_{n}\in(Q^{\prime}\cdot A)^{*}Q^{\prime}$, since the states and transitions of $\mathcal{D}^{\prime}$ and $\gamma(\mathcal{D}^{\prime})$ are identical, $\varrho^{\prime}$ is an accepting run of $\mathcal{D}^{\prime}$ if and only if it is an accepting run of $\gamma(\mathcal{D}^{\prime})$. Therefore, since $\mathcal{D}^{\prime}$ is a $k$-delay determinizer of $(4k+1)\cdot\mathcal{N}$, if $\varrho^{\prime}$ is an accepting run of $\gamma(\mathcal{D}^{\prime})$, there exists an accepting run $\varrho=q_{0}a_{0}\dots a_{n-1}q_{n}$ of $\mathcal{N}$ such that $(4k+1)w(\varrho)=w^{\prime}(\varrho^{\prime})$, and for every $0\leq i\leq n$, $|(4k+1)w(q_{0}\dots q_{i})-w^{\prime}(q_{0}^{\prime}\dots q_{i}^{\prime})|\leq k$. As a consequence, for every $1\leq i\leq n$ we have

[TABLE]

hence $w(q_{i-1}a_{i-1}q_{i})=\gamma(w(q_{i-1}^{\prime}a_{i-1}q_{i}^{\prime}))$. As a consequence, $\gamma(\mathcal{D}^{\prime})$ is a [math]-delay determinizer of $\mathcal{N}$. ∎

We can now show that the $k$-delay problem is \EXP-hard by arguing that the [math]-delay problem is \EXP-hard. Let us introduce some notation regarding transducers.

Transducers. A (synchronous) transducer $\mathcal{T}$ from an input alphabet $A_{I}$ to an output alphabet $A_{O}$ is an unweighted automaton $(Q,I,A_{I}\times A_{O},\Delta,F)$. We denote the domain of $\mathcal{T}$ by $\mathsf{dom}(\mathcal{T}):=\{a_{0}\dots a_{n-1}\in A_{I}^{*}\>\mid\>(a_{0},b_{0})\dots(a_{n-1},b_{n-1})\in(A_{I}\times A_{O})^{*}\}$. The transducer $\mathcal{T}$ is said to be input-deterministic if for all $p\in Q$, for all $a\in A_{I}$, there exist at most one state-output pair $(q,b)\in Q\times A_{O}$ such that $(p,(a,b),q)\in\Delta$. A transducer $\mathcal{U}$ from $A_{I}$ to $A_{O}$ is a [math]-delay uniformizer of $\mathcal{T}$ if

$(i)$ $\mathcal{U}$is input-deterministic,

$(ii)$ $\mathcal{L}_{\mathcal{U}}\subseteq\mathcal{L}_{\mathcal{T}}$, and

$(iii)$ $\mathsf{dom}(\mathcal{U})=\mathsf{dom}(\mathcal{T})$.

If such a transducer exists, we say $\mathcal{T}$ is [math]-delay uniformizable. Given a transducer, to determine whether it is [math]-delay uniformizable is an \EXP-hard problem [FJLW16].

Intuitively, a transducer induces a relation from input words to output words. We construct an automaton that replaces the output alphabet by unique positive integer identifiers. For convenience, we also make sure the constructed automaton defines a function which maps every word in its language to [math].

From transducers to weighted automata. Given a transducer $\mathcal{T}=(Q,I,A_{I}\times A_{O},\Delta,F)$ with $A_{0}=\{1,\dots M\}$, we construct a weighted automaton $\mathcal{N}_{\mathcal{T}}=(Q^{\prime},I,A_{I}\cup\{\#\},\Delta^{\prime},w,F)$ as follows:

• •

$Q^{\prime}=Q\cup Q\times A_{O}$,

• •

$\Delta^{\prime}=\{\left(p,a,(q,m)\right),\left((q,m),\#,q\right)\>\mid\>(p,(a,m),q)\in\Delta\}$,

• •

$w:\Delta^{\prime}\to\mathbb{Z}$, $\left(p,a,(q,m)\right)\mapsto m$ and $\left((q,m),\#,q\right)\mapsto-m$.

Lemma 18**.**

The translation from transducers to weighted automata satisfies the following properties.

$q_{0}(a_{0},m_{0})\dots(a_{n-1},m_{n-1})q_{n}$* is a run of $\mathcal{T}$ if and only if $q_{0}a_{0}(q_{0},m_{0})\#\dots(q_{n-1},m_{n-1})\#q_{n}$ is a run of $\mathcal{N}_{\mathcal{T}}$. Moreover, for all $0\leq i\leq n$*

• •

$w(q_{0}\dots q_{i})=0$, and

• •

$w(q_{0}\dots(q_{i},m_{i}))=m_{i}$; 2. 2.

$\mathcal{L}_{\mathcal{N}_{\mathcal{T}}}=\{a_{0}\#\dots\#a_{n}\#\>\mid\>a_{0}\dots a_{n}\in\mathsf{dom}(\mathcal{T})\}$; 3. 3.

$\llbracket\mathcal{N}_{\mathcal{T}}\rrbracket(\alpha)=0$* for all $\alpha\in\mathcal{L}_{\mathcal{N}_{\mathcal{T}}}$.*

Proof.

The first item follows by construction of the automaton $\mathcal{N}_{\mathcal{T}}$. Items $2$ and $3$ are direct consequences of item $1$. ∎

We are now ready to show the [math]-delay uniformization problem reduces in polynomial time to the [math]-delay determinization problem. To do so, we show that any [math]-delay uniformizer of a transducer $\mathcal{T}$ can be transformed into a [math]-delay determinizer of $\mathcal{N}_{\mathcal{T}}$, and vice versa.

Lemma 19**.**

Deciding the [math]-delay problem for a given automaton is \EXP-hard.

Proof.

Given a transducer $\mathcal{T}=(Q,I,A_{I}\times A_{O},\Delta,F)$ with $A_{0}=\{1,\dots,M\}$, we construct $\mathcal{N}_{\mathcal{T}}=(Q^{\prime},I,A_{I}\cup\{\#\},\Delta^{\prime},w,F)$. Suppose $\mathcal{U}=(S,\{s_{0}\},A_{I}\times A_{O},R,G)$ is a [math]-delay uniformizer of $\mathcal{T}$. In what follows we argue that $\mathcal{N}_{\mathcal{U}}$ is a [math]-delay determinizer of $\mathcal{N}_{\mathcal{T}}$. Since $\mathcal{U}$ is input-deterministic, the automaton $\mathcal{N}_{\mathcal{U}}$ is deterministic. Also, since $\mathcal{U}$ is a [math]-delay uniformizer of $\mathcal{T}$, then we have that $\mathsf{dom}(\mathcal{U})=\mathsf{dom}(\mathcal{T})$. Hence, from Lemma 18 item $2$ it follows that $\mathcal{L}_{\mathcal{N}_{\mathcal{T}}}=\mathcal{L}_{\mathcal{N}_{\mathcal{U}}}$. Since both automata map their languages to the value [math] (see Lemma 18 item $3$), we have that $\llbracket\mathcal{N}_{\mathcal{U}}\rrbracket=\llbracket\mathcal{N}_{\mathcal{T}}\rrbracket$. Finally, by using Lemma 18 item $1$, we get that $\mathcal{N}_{\mathcal{U}}\subseteq_{0}\mathcal{N}_{\mathcal{T}}$ from the fact that $\mathcal{L}_{\mathcal{U}}\subseteq\mathcal{L}_{\mathcal{T}}$.

Assume $\mathcal{D}=(S,\{s_{0}\},A_{I}\cup\{\#\},R,\mu,G)$ is a [math]-delay determinizer of $\mathcal{N}_{\mathcal{T}}$. Let $\mathcal{U}$ be the transducer $(S,\{s_{0}\},A_{I}\times A_{O},R^{\prime},G)$ where $R^{\prime}=\{\left(p,(a,m),s)\right)\>\mid\>(p,a,q),(q,\#,s)\in R\land\mu(p,a,q)=-\mu(q,\#,s)=m\}$. Since $\mathcal{D}$ is deterministic, we have that $\mathcal{U}$ is input-deterministic. By construction, we have that

[TABLE]

Therefore, since $\mathcal{L}_{\mathcal{N}_{\mathcal{T}}}=\mathcal{L}_{\mathcal{D}}$, from Lemma 18 item $2$ we get that $\mathsf{dom}(\mathcal{U})=\mathsf{dom}(\mathcal{T})$. Also, by construction, we have that $s_{0}(a_{0},m_{0})\dots(a_{n-1},m_{n-1})s_{n}$ is a run of $\mathcal{U}$ if and only if $s_{0}a_{0}q_{0}\#s_{1}a_{1}q_{1}\#\dots q_{n-1}\#s_{n}$ is a run of $\mathcal{D}$ such that $\mu(s_{0}\dots q_{i})=m_{i}$ for all $0\leq i\leq n$. Moreover, since $\mathcal{D}$ is a [math]-delay determinizer of $\mathcal{N}_{\mathcal{T}}$, $\mu(s_{0}\dots s_{i})=0$ for all $0\leq i\leq n$ (see Lemma 18 item $3$). Finally, because $\mathcal{D}\subseteq_{0}\mathcal{N}_{\mathcal{T}}$, we get that $\mathcal{L}_{\mathcal{U}}\subseteq\mathcal{L}_{\mathcal{T}}$ by Lemma 18 item $1$ and the above argument. ∎

4 Deciding $r$-regret determinizability

In this section we argue that the $r$-regret problem is \EXP-complete. It will be convenient to suppose all automata we work with are trim. This is no loss of generality with regard to $r$-regret determinizability, i.e. an automaton $\mathcal{N}$ is $r$-regret determinizable if and only if its trim version, $\mathcal{N}^{\prime}$, is $r$-regret determinizable. Clearly, an $r$-regret determinizer of $\mathcal{N}^{\prime}$ is also an $r$-regret determinizer of $\mathcal{N}$. Also, it is easy to show that the trim version $\mathcal{D}^{\prime}$ of an $r$-regret determinizer $\mathcal{D}$ of $\mathcal{N}$ must also be an $r$-regret determinizer of $\mathcal{N}^{\prime}$. Furthermore, any automaton can be trimmed in polynomial time.

4.1 Upper bound

We will now give an exponential time algorithm to determine whether a given automaton is $r$-regret determinizable, for a given $r$. The algorithm is based on a quantitative version of the Joker game introduced by Kuperberg and Skrzypczak to study the determinization of good-for-games automata [KS15]. More precisely, the Joker game will correspond to generalization of the classical energy games [CdAHS03].

The algorithm is as follows: construct an energy game with resets (which we call the Joker game) based on the given automaton and decide if Eve wins it; if this is not the case, then for all $r\in\mathbb{N}$ the automaton is not $r$-regret determinizable; otherwise, using the winning strategy for Eve in the Joker game, construct a deterministic automaton $\mathcal{D}$ realizing the same function as $\mathcal{N}$ and use it to decide if $\mathcal{N}$ is $r$-regret determinizable. The last step of the algorithm is the simplest. Given a deterministic version of the original automaton, one can use it as a “monitor” and reduce the $r$-regret determinizability problem to deciding the winner in an energy game.

Theorem 5**.**

Deciding the $r$-regret problem for a given automaton is in \EXP.

Energy games with resets. An energy game with resets (EGR for short) is an infinite-duration two-player turn-based game played by Eve and Adam on a directed weighted graph. Formally, an EGR $\mathcal{G}=(V,V_{\exists},E,E_{\varrho},w)$ consists of: a set $V$ of vertices, a set $V_{\exists}\subseteq V$ of vertices of Eve—the set $V_{\forall}:=(V\setminus V_{\exists})$ of vertices thus belongs to Adam, a set $E\subseteq V\times V$ of directed edges, a set $E_{\varrho}\subseteq E$ of reset edges such that $E_{\varrho}\subseteq V_{\forall}\times V$, and a weight function $w:E\to\mathbb{Z}$. (Observe that if $E_{\varrho}=\varnothing$, we obtain the classical energy games without resets [CdAHS03].) Pictorially, we represent Eve vertices by squares and Adam vertices by circles. We denote by $w_{\max}$ the value $\max_{e\in E}|w(e)|$. Intuitively, from the current vertex $u$, the player who owns $u$ (i.e. Eve if $u\in V_{\exists}$, and Adam otherwise) chooses an edge $(u,v)\in E$ and the play moves to $v$. We formalize the notions of strategy and play below.

A strategy for Eve (respectively, Adam) in $\mathcal{G}$ is a mapping $\sigma:V^{*}\cdot V_{\exists}\to V$ (respectively, $\tau:V^{*}\cdot V_{\forall}\to V$) such that $\sigma(v_{0}\dots v_{n})=v_{n+1}$ ($\tau(v_{0}\dots v_{n})=v_{n+1}$) implies $(v_{n},v_{n+1})\in E$. As in regret games, a strategy $\sigma$ for either player is one which can be encoded as a deterministic Mealy machine $(S,s_{I},\lambda_{u},\lambda_{o})$ with update function $\lambda_{u}:S\times V\to S$ and output function $\lambda_{o}:S\times V\to V$. The machine encodes $\sigma$ in the following sense: $\sigma(v_{0}\dots v_{n})=\lambda_{u}(s_{n},v_{n})$ where $s_{0}=s_{I}$ and $s_{i+1}=\lambda_{u}(s_{i},v_{i})$ for all $0\leq i<n$. As usual, the memory of a finite-memory strategy refers to the size of the Mealy machine realizing it.

A play in $\mathcal{G}$ from $v\in V$ corresponds to an infinite path in the underlying directed graph $(V,E)$. That is, a sequence $\pi=v_{0}v_{1}\dots$ such that $(v_{i},v_{i+1})\in E$ for all $i\in\mathbb{N}$. Since an EGR is played for an infinite duration, we will henceforth assume they are played on digraphs with no sinks: i.e. for all $u\in V$, there exists $v\in V$ such that $(u,v)\in E$. We say a play $\pi=v_{0}v_{1}\dots$ is consistent with a strategy $\sigma$ for Eve (respectively, $\tau$ for Adam) if it holds that $v_{i}\in V_{\exists}$ implies $\sigma(v_{0}\dots v_{i})=v_{i+1}$ ($v_{i}\not\in V_{\forall}$ implies $\tau(v_{0}\dots v_{i})=v_{i+1}$). Given a strategy $\sigma$ for Eve and a strategy $\tau$ for Adam, and a vertex $v\in V$ there is a unique play $\pi^{v}_{\sigma\tau}$ compatible with both $\sigma$ and $\tau$ from $v$.

Given a finite path $\varphi$ in $\mathcal{G}$, i.e. a sequence $v_{0}\dots v_{n}$ such that $(v_{i},v_{i+1})\in E$ for all $0\leq i<n$, and an initial credit $c_{0}\in\mathbb{N}$, we define the energy level of $\varphi$ as $\mathsf{EL}_{c_{0}}(\varphi):=c_{0}+\sum^{n-1}_{j=i_{0}}w(v_{j},v_{j+1})$ where $0\leq i_{0}<n$ is the minimal index such that $(v_{\ell},v_{\ell+1})\not\in E_{\varrho}$ for all $i_{0}<\ell<n$.

We say Eve wins the EGR from a vertex $v\in V$ with initial credit $c_{0}$ if she has a strategy $\sigma$ such that, for all strategies $\tau$ for Adam, for all finite prefixes $\varphi$ of $\pi^{v}_{\sigma\tau}$ we have $\mathsf{EL}_{c_{0}}(\varphi)\geq 0$. Adam wins the EGR from $v$ with initial credit $c_{0}$ if and only if Eve does not win it.

Example 3**.**

Consider the EGR shown in Fig. 5. In this game, Eve wins from $v_{0}$ with initial credit $2$. Indeed, whenever Adam plays from $v_{1}$ to $v_{0}$ the energy level drops by $1$ but is then increased by $1$ when the play returns to $v_{1}$; when he plays from $v_{1}$ to $v_{2}$ the energy level is first reset to $2$ and then drops to [math] when the play reaches $v_{0}$. Clearly then, Adam cannot force a negative energy level. However, if $E_{\varrho}$ were empty, then Eve would lose the game regardless of the initial credit.

The following properties of energy games (both, with or without resets), which include positional determinacy, will be useful in the sequel. A game is positionally determined if: for all instances of the game, from all vertices, either Eve has a positional strategy which is winning for her against any strategy for Adam, or Adam has a positional strategy which is winning for him against any strategy for Eve.

Proposition 20**.**

For any energy game (both, with or without resets) $\mathcal{G}=(V,V_{\exists},E,E_{\varrho},w)$ the following hold.

The game is positionally determined if $c_{0}\geq|V|w_{\max}$. 2. 2.

For all $v\in V$, Eve wins from $v\in V$ with initial credit $|V|w_{\max}$ if and only if there exists $c_{0}\in\mathbb{N}$ such that she wins from $v\in V$ with initial credit $c_{0}$. 3. 3.

Determining if there exists $c_{0}\in\mathbb{N}$ such that Eve wins from $v\in V$ with initial credit $c_{0}$ is decidable in time polynomial in $|V|$, $|E|$, and $w_{\max}$.

Sketch.

All three properties are known to hold for energy games without resets (see, e.g. [CdAHS03, BCD*+*11]).

For EGRs the arguments to show these properties hold are almost identical to those used in [BCD*+*11]. We first define a finite version of the game which is stopped after the first cycle is formed and in which the winner is determined based on properties of that cycle. If we let Eve win if and only if the cycle has non-negative sum of weights or it contains a reset, then we can show she wins this First Cycle Game [AR14] if and only if she wins the EGR with initial credit $|V|w_{\max}$. Furthermore, using a result from [AR14] we obtain that positional strategies suffice for both players in both games, i.e. the games are positionally determined.

The second property follows from the relationship between the EGR and the first cycle game we construct. More precisely, we show that winning strategies for both players transfer between the games. In the first cycle game, Adam wins if he can force cycles which have a negative sum of weights. Hence, if Eve does not win the EGR with initial credit $|V|w_{\max}$, then by determinacy, Adam wins the first cycle game, and his strategy—when played on the original EGR—ensures only negatively-weighted cycles are formed, which in turn means that he wins the EGR with any initial credit.

Finally, to obtain an algorithm, we reduce the problem of deciding if Eve wins the EGR from $v\in V$ with a given initial credit $c_{0}$ to her winning a safety game [AG11] played on an unweighted digraph where the states keep track of the energy level (up to a maximum of $|V|w_{\max}$). ∎

Energy games will be our main tool for the rest of this section. They allow us to claim that, given an automaton $\mathcal{N}$ and a deterministic automaton $\mathcal{D}$ which defines the same function, we can decide $r$-regret determinizability.

Proposition 21**.**

Given an automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$ and $\mathcal{D}=(Q^{\prime},\{q^{\prime}_{I}\},A,\Delta^{\prime},w^{\prime},F^{\prime})$ such that $\mathcal{D}$ is deterministic and $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$, the $r$-regret problem for $\mathcal{N}$ is decidable in time polynomial in $|Q|$, $|Q^{\prime}|$, $|A|$, $w_{\max}$, and $w_{\max}^{\prime}$.

Sketch.

We construct an energy game without resets which simulates the regret game played on $\mathcal{N}$ while using $\mathcal{D}$ to compare the weights of transitions chosen by Eve to those of the maximal run of $\mathcal{N}$. Intuitively, Eve chooses an initial state in $\mathcal{N}$, then Adam chooses a symbol, and Eve responds with a transition $t\in\Delta$ in $\mathcal{N}$. Finally, the state of $\mathcal{D}$ is deterministically updated via transition $t^{\prime}$. The weight of the whole round is $w(t)-w^{\prime}(t^{\prime})$. We also make sure Eve loses if in the regret game she reaches a non-final state and the run of $\mathcal{D}$ is at a final state; or if she reaches a final state with too low an energy level (implying a large regret). Formally, the energy game without resets is $\mathcal{G}=(V,V_{\exists},E,\varnothing,\mu)$ where:

• •

$V=Q^{2}\cup Q^{3}\times A\cup\{\top,\bot,\bot^{r}_{1},\bot^{r}_{2}\}$;

• •

$V_{\exists}=Q^{3}\times A$;

• •

$E$ contains edges to simulate transitions of $\mathcal{N}$ and $\mathcal{D}$, i.e. $\{\left((p,q),(p,q,q^{\prime},a)\right)\>\mid\>(q,a,q^{\prime})\in\Delta^{\prime}\}\cup\{\left((p,q,q^{\prime},a),(p^{\prime},q^{\prime})\right)\>\mid\>(p,a,p^{\prime})\in\Delta\}$, edges required to verify Eve does not reach a non-final state when $\mathcal{D}$ accepts, i.e. $\{\left((p,q),\bot\right)\>\mid\>p\not\in F\land q\in F^{\prime}\}\cup\{(\bot,\bot)\}$, edges used to make sure the regret is at most $r$ when on final states, i.e. $\{\left((p,q),\bot^{r}_{1}\right)\>\mid\>p\in F\land q\in F^{\prime}\}\cup\{(\bot^{r}_{1},\bot^{r}_{2}),(\bot^{r}_{2},\bot^{r}_{1})\}$, and edges to punish one of the players if an automaton blocks, i.e. $\{\left((p,q),\top\right)\>\mid\>\lnot\exists(q,a,q^{\prime})\in\Delta^{\prime}\}\cup\{\left((p,q,q^{\prime},a),\bot\right)\>\mid\>\lnot\exists(p,a,p^{\prime})\in\Delta\}\cup\{(\top,\top)\}$;

• •

$\mu:E\to\mathbb{Z}$ is such that

• –

$\left((p,q,q^{\prime},a),(p^{\prime},q^{\prime})\right)\mapsto w(p,a,p^{\prime})-w^{\prime}(q,a,q^{\prime})$,

• –

$(\bot,\bot)\mapsto-1$,

• –

$\left((p,q),\bot^{r}_{1}\right)\mapsto 1-|Q^{\prime}|(w_{\max}+w_{\max}^{\prime})$,

• –

$(\bot^{r}_{1},\bot^{r}_{2})\mapsto-1$, $(\bot^{r}_{2},\bot^{r}_{1})\mapsto 1$,

• –

$(\top,\top)\mapsto 1$, and

• –

$e\mapsto 0$ for all other $e\in E$.

We then claim that for some $p_{I}\in I$, Eve wins the energy game without resets $\mathcal{G}$ from $(p_{I},q^{\prime}_{I})$ with initial credit $r+|Q^{\prime}|(w_{\max}+w_{\max}^{\prime})$ if and only if $\mathcal{N}$ is $r$-regret determinizable. The result then follows from the fact $\mathcal{G}$ is of size polynomial w.r.t. $\mathcal{D}$ and $\mathcal{N}$, and the application of the algorithm (see Proposition 20) to determine the winner of $\mathcal{G}$. ∎

The Joker game. The Joker game (JG) is a game played by Eve and Adam on an automaton $(Q,I,A,\Delta,w,F)$. It is played as follows: Eve chooses as initial state $p\in I$ and Adam an initial state $q\in I$ and the initial configuration becomes $(p,q)\in I^{2}$. From the current configuration $(p,q)\in Q^{2}$

(Step i): Adam chooses a symbol $a\in A$,

(Step ii): then Eve chooses a transition $(p,a,p^{\prime})\in\Delta$, and

(Step iii): Adam can

(Step iii.a): choose a transition $(q,a,q^{\prime})\in\Delta$ or

(Step iii.b): play $\mathsf{joker}$ and choose a transition $(p,a,q^{\prime})\in\Delta$.

The new configuration is then $(p^{\prime},q^{\prime})$. The weight assigned to each round corresponds to the weight of the transition chosen by Eve minus the weight of that chosen by Adam. If Adam played $\mathsf{joker}$, then the sum of weights is reset before adding the weight of the configuration change. Additionally, if Eve moves to a non-final state and Adam moves to a final state, or if Eve can no longer extend the run she is constructing, then (Step $\star$): we ensure Eve loses the game.

We formalize the JG played on $\mathcal{N}=(Q,I,A,\Delta,w,F)$ as an EGR $(V,V_{\exists},E,E_{\varrho},\mu)$ with $V=V_{\exists}\cup V_{\forall}$, $E=\bigcup_{1\leq i\leq 3}E_{\forall_{i}}\cup E_{\exists}\cup E_{\varrho}\cup\{(\bot,\bot)\}$ where:

• •

$V_{\exists}=Q^{2}\times A\cup\{\bot\}$;

• •

$V_{\forall}=Q^{2}\cup Q^{3}\times A$;

• •

(Step i): $E_{\forall_{1}}=\{\left((p,q),(p,q,a)\right)\>\mid\>(p,q)\in Q^{2},(q,a,q^{\prime})\in\Delta\}$;

• •

(Step ii): $E_{\exists}=\{\left((p,q,a),(p,q,p^{\prime},a)\right)\>\mid\>(p,q,a)\in V_{\exists},(p,a,p^{\prime})\in\Delta\}$;

• •

(Step iii.a): $E_{\forall_{2}}=\{\left((p,q,p^{\prime},a),(p^{\prime},q^{\prime})\right)\>\mid\>(p,q,p^{\prime},a)\in Q^{3}\times A,(q,a,q^{\prime})\in\Delta\}$;

• •

(Step iii.b): $E_{\varrho}=\{\left((p,q,p^{\prime},a),(p^{\prime},p^{\prime\prime})\right)\>\mid\>(p,q,p^{\prime},a)\in Q^{3}\times A,(p,a,p^{\prime\prime})\in\Delta\}$;

• •

(Step $\star$): $E_{\forall_{3}}=\{\left((p,q),\bot\right)\>\mid\>p\not\in F\land q\in F\text{ or }\exists a\in A,\forall p^{\prime}\in Q:(p,a,p^{\prime})\not\in\Delta\}\cup\{(\bot,\bot)\}$; and

• •

$\mu$ is such that

• –

$(\bot,\bot)\mapsto-1$,

• –

$e\mapsto w(p,a,p^{\prime})-w(q,a,q^{\prime})$ for all $e=\left((p,q,p^{\prime},a),(p^{\prime},q^{\prime})\right)\in E_{\forall_{2}}$,

• –

$e\mapsto w(p,a,p^{\prime})-w(p,a,p^{\prime\prime})$ for all $e=\left((p,q,p^{\prime},a),(p,p^{\prime\prime})\right)\in E_{\varrho}$,

• –

and $e\mapsto 0$ for all other $e\in E$.

It is easy to verify that there are no sinks in the EGR.

Winning the Joker game. We say Eve wins the JG played on $(Q,I,A,\Delta,w,F)$ if there is $p\in I$ such that, for all $q\in I$, she wins from $(p,q)$ with initial credit $|V|\mu_{\max}$ (where $\mu_{\max}:=\max_{e\in E}|\mu(e)|$). Proposition 20 tells us that, if Eve wins with some initial credit, then she also wins with initial credit $|V|\mu_{\max}$.

We now establish a relationship between $r$-regret determinization and the JG.

Lemma 22**.**

If an automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$ is $r$-regret determinizable, for some $r\in\mathbb{N}$, then Eve wins the JG played on $\mathcal{N}$.

Proof.

We will actually prove the contrapositive holds. Suppose Eve does not win the JG. By determinacy of EGRs (Proposition 20 item 1) we know that Adam, for all $p_{0}\in I$, has a strategy $\tau$ to force from some $(p_{0},q_{0})\in I^{2}$ a play which eventually witnesses a negative energy level. Furthermore, he can do so for any initial credit (Proposition 20 item 2). Let us now assume, towards a contradiction, that Eve wins the $r$-regret game with a strategy $\sigma$ such that $\sigma(\varepsilon)=p_{0}$. Since $\sigma$ is winning for her in the regret game, then for all $\alpha\in A^{*}$, $\sigma(\alpha)$ is an initial run of $\mathcal{N}$. Hence $\sigma$ can be converted into a strategy for Eve in the JG by ignoring the transitions chosen by Adam and following $\sigma$ when Adam chooses a symbol $a\in A$. If Eve follows $\sigma$ to play in the JG against $\tau$, then there exists $q_{0}\in I$ such that $\pi^{(p_{0},q_{0})}_{\sigma\tau}$ eventually witnesses a negative energy level even if the initial credit is $r+2|Q|w_{\max}$ (because $\tau$ is winning for Adam in the JG with any initial credit). Moreover, $\pi^{(p_{0},q_{0})}_{\sigma\tau}$ never reaches the vertex $\bot$, since $\sigma(\alpha)$ is an initial run of $\mathcal{N}$ for all $\alpha\in A^{*}$. If we let $\varphi=(p_{0},q_{0})(p_{0},q_{0},a_{0})(p_{0},q_{0},p_{1},a_{0})\dots(p_{n},q_{n})$ be the first prefix that witnesses a negative energy level with initial credit $r+2|Q|w_{\max}$, and $0\leq i_{0}<n$ be the minimal index such that no reset occurs for all $i_{0}<\ell<n$, then $\varrho=p_{0}a_{0}p_{1}a_{1}\dots p_{n}$ and $\varrho^{\prime}=p_{0}a_{0}\dots p_{i_{0}}a_{i_{0}}q_{i_{0}+1}\dots q_{n}$ are two runs in $\mathcal{N}$ such that $w(\varrho^{\prime})>w(\varrho)+r+2|Q|w_{\max}$. Since $\mathcal{N}$ is trim, there is a final run $q_{n}a_{n}\dots a_{m-1}q_{m}$ such that $m-n\leq|Q|$. Hence, we have that $\llbracket\mathcal{N}\rrbracket(a_{0}\dots a_{m-1})-\mathsf{Val}(\sigma(a_{0}\dots a_{m-1}))>r$, which contradicts the fact that $\sigma$ is winning for Eve in the regret game. It follows that there cannot be a winning strategy for Eve in the $r$-regret game. ∎

From the above results we have that if we construct the JG for the given automaton and Eve does not win the JG, then the automaton cannot be $r$-regret determinizable (no matter the value of $r$). We now study the case when Eve does win.

Using the JG to determinize an automaton. Let $\mathcal{N}=(Q,I,A,\Delta,w,F)$ be an automaton. We will assume that Eve wins the JG played on $\mathcal{N}$. Denote by $W^{\mathrm{JG}}\subseteq Q^{2}$ the winning region of Eve. That is, $W^{\mathrm{JG}}$ is the set of all $(p,q)\in Q^{2}$ such that Eve wins the EGR from $(p,q)$ with initial credit $|V|\mu_{\max}$. Also, let us write $Q^{\mathrm{JG}}$ for the projection of $W^{\mathrm{JG}}$ on its first component. Moreover, for every $(p,q)\in W^{\mathrm{JG}}$, let $\mathsf{Cr}(p,q)$ denote the minimal integer $c\in\mathbb{N}$ such that Eve wins the JG from $(p,q)$ with initial credit $c$.

We will now prove some properties of the sets $W^{\mathrm{JG}}$ and $Q^{\mathrm{JG}}$. First, the relation $W^{\mathrm{JG}}$ is transitive.

Lemma 23**.**

For all $p,q,t\in Q$, if $(p,q),(q,t)\in W^{\mathrm{JG}}$ then $(p,t)\in W^{\mathrm{JG}}$.

Sketch.

For every $(p,q)\in W^{\mathrm{JG}}$, let $\sigma_{(p,q)}$ denote a winning strategy for Eve in the JG played from $(p,q)$ with initial credit $\mathsf{Cr}(p,q)$. We define a strategy $\sigma$ for Eve in the JG as follows. For $(p,q),(q,t)\in W^{\mathrm{JG}}$, let $q_{p,t}\in Q$ denote the state such that $\mathsf{Cr}(p,q_{p,t})+\mathsf{Cr}(q_{p,t},t)$ is minimal. For every $(p,t,a)\in Q^{2}\times A$, if $(p,q),(p,t)\in W^{\mathrm{JG}}$, we then set $\sigma\left((p,t,a)\right)=\sigma_{(p,q_{p,t})}((p,q_{p,t})(p,q_{p,t},a))$. We then claim that for every $(p,q)(q,t)\in W^{\mathrm{JG}}$, the strategy $\sigma$ is winning for Eve in the EGR starting from $(p,t)$ with initial credit $\mathsf{Cr}(p,q_{p,t})+\mathsf{Cr}(q_{p,t},t)$. ∎

Another property which will be useful in the sequel is that, all the $a$-successors of a state $p\in Q^{\mathrm{JG}}$ are related (by $W^{\mathrm{JG}}$) to the $a$-successor chosen by a winning strategy for Eve.

Lemma 24**.**

For all $(p,q)\in W^{\mathrm{JG}}$ and $a\in A$, let $\sigma^{\mathrm{JG}}$ be a winning strategy for Eve in the JG from $(p,q)$ with initial credit $c\in\mathbb{N}$, and let $(p,q,p^{\prime},a)=\sigma^{\mathrm{JG}}\left((p,q)(p,q,a)\right)$. Then, for all $(t,a,p^{\prime\prime})\in\Delta$ such that $t\in\{p,q\}$, it holds that $(p^{\prime},p^{\prime\prime})\in W^{\mathrm{JG}}$, and $\mathsf{Cr}(p^{\prime},p^{\prime\prime})\leq c+w(p,a,p^{\prime})-w(t,a,p^{\prime\prime})$.

Proof.

Observe that from any $(p,q)\in W^{\mathrm{JG}}$ in the JG, after Adam has chosen a letter $a\in A$ and Eve a transition $(p,a,p^{\prime})\in\Delta$, Adam could play $\mathsf{joker}$ and choose any transition $(p,a,p^{\prime\prime})\in\Delta$ or (without playing $\mathsf{joker}$) choose any transition $(q,a,p^{\prime\prime})$. Hence, for any winning strategy $\sigma^{\mathrm{JG}}$ for Eve in the JG played from $(p,q)$ with initial credit $c$ such that $\sigma^{\mathrm{JG}}\left((p,q)(p,q,a)\right)=(p,q,p^{\prime},a)$, for any $(t,a,p^{\prime\prime})\in\Delta$ such that $t\in\{p,q\}$, reaching $(p^{\prime},p^{\prime\prime})$ is consistent with $\sigma^{\mathrm{JG}}$. It follows that $\sigma^{\mathrm{JG}}$ must be winning for Eve from $(p^{\prime},p^{\prime\prime})$ with initial credit $c_{1}=c+w(p,a,p^{\prime})-w(t,a,p^{\prime\prime})$. If $c_{1}\leq|V|\mu_{\max}$, we are done. Otherwise, by Proposition 20, there is a strategy $\sigma^{\prime}$ winning for Eve from $(p^{\prime},p^{\prime\prime})$ with initial credit $|V|\mu_{\max}$. From the definition of $W^{\mathrm{JG}}$ we get that $(p^{\prime},p^{\prime\prime})\in W^{\mathrm{JG}}$ as required, and the result follows. ∎

Corollary 25**.**

If there are winning strategies $\sigma^{\mathrm{JG}}_{1},\sigma^{\mathrm{JG}}_{2}$ for Eve in the JG with initial credit $|V|\mu_{\max}$ from $(p,q_{1}),(p,q_{2})$, respectively, such that $\sigma^{\mathrm{JG}}_{1}\left((p,q_{1})(p,q_{1},a)\right)=(p,q_{1},p_{1},a)$ and $\sigma^{\mathrm{JG}}_{2}\left((p,q_{2})(p,q_{2},a)\right)=(p,q_{2},p_{2},a)$ for some $a\in A$, then $(p_{1},p_{2}),(p_{2},p_{1})\in W^{\mathrm{JG}}$.

Finally, we note that by following a winning strategy for Eve in the JG, we are sure all alternative runs of an automaton are related (by $W^{\mathrm{JG}}$) to the run built by Eve.

Lemma 26**.**

For all play prefixes $(p_{0},q_{0})(p_{0},q_{0},a_{0})\dots$ $(p_{n-1},q_{n-1},p_{n},a_{n-1})(p_{n},q_{n})$ consistent with a winning strategy for Eve in the JG from $(p_{0},q_{0})$ with initial credit $|V|\mu_{\max}$, for all runs $p_{0}a_{0}p^{\prime}_{1}a_{1}\dots a_{n-1}p^{\prime}_{n}$ of $\mathcal{N}$ on $a_{0}\dots a_{n-1}$ we have that $(p_{n},p^{\prime}_{n})\in W^{\mathrm{JG}}$.

Proof.

Let $\sigma^{\mathrm{JG}}_{1}$ denote the winning strategy referred to in the claim.

First, it is easy to show by induction that $(p_{i},q_{i})\in W^{\mathrm{JG}}$ for all $0\leq i\leq n$. Intuitively, using the fact that $\sigma^{\mathrm{JG}}_{1}$ is winning for Eve with initial credit $|V|\mu_{\max}$ from $(p_{0},q_{0})$ we get that for any $(p_{i},q_{i})$ the strategy $\sigma^{\mathrm{JG}}_{1}$ is winning for her with some initial credit. Then, by Proposition 20, there is another strategy $\sigma^{\prime}$ that is winning from $(p_{i},q_{i})$ with initial credit $|V|\mu_{\max}$.

We will now argue, by induction, that $(p_{i},p^{\prime}_{i})\in W^{\mathrm{JG}}$ for all $0<i\leq n$. For the base case, it should be clear that $(p_{1},p^{\prime}_{1})\in W^{\mathrm{JG}}$. This follows from Lemma 24. Hence, we can assume the claim holds for some $0<i<n$. By definition of $W^{\mathrm{JG}}$ we have that Eve has a winning strategy $\sigma^{\mathrm{JG}}_{2}$ in the JG from $(p_{i},p^{\prime}_{i})$ with initial credit $|V|\mu_{\max}$. It follows from Corollary 25 that $(p_{i+1},t)\in W^{\mathrm{JG}}$ where $(p_{i},q_{i},p_{i+1},a_{i})=\sigma^{\mathrm{JG}}_{1}\left((p_{0},q_{0})\dots(p_{i},q_{i},a_{i})\right)$ and $(p_{i},q_{i},t,a_{i})=\sigma^{\mathrm{JG}}_{2}\left((p_{0},p_{0})\dots(p_{i},p^{\prime}_{i},a_{i})\right).$ Using Lemma 24 we get that $(t,p^{\prime}_{i+1})\in W^{\mathrm{JG}}$. Now, by transitivity of $W^{\mathrm{JG}}$ (see Lemma 23) we conclude that $(p_{i+1},p^{\prime}_{i+1})\in W^{\mathrm{JG}}$. The claim then follows by induction. ∎

We now prove that if Eve wins the JG played on $\mathcal{N}$, then the automaton $\mathcal{N}$ is determinizable. In order to do so, we first prove that $\mathcal{N}$ is $2|V|\mu_{\max}$-bounded.

Proposition 27**.**

Let $\mathcal{N}=(Q,I,A,\Delta,w,F)$ be such that Eve wins the JG played on $\mathcal{N}$. Then $\mathcal{N}$ is $2|V|\mu_{\max}$-bounded.

Proof.

Let $\varrho_{p}=p_{0}a_{0}p_{1}\dots a_{n-1}p_{n}$ be a maximal accepting run of $\mathcal{N}$, let $i\in\{0,\ldots,n\}$, and let $\varrho_{q}=q_{0}a_{0}q_{1}\dots a_{i-1}q_{i}$ be an initial run. Let us prove that $w(\varrho_{q})-w(p_{0}a_{0}p_{1}\dots a_{i-1}p_{i})\leq 2|V|\mu_{\max}.$ Let $\varrho_{p,1}$ denote the run $p_{0}a_{0}p_{1}\dots a_{i-1}p_{i}$, let $\varrho_{p,2}$ denote the run $p_{i}a_{i}p_{i+1}\dots a_{n-1}p_{n}$. First, let $\sigma^{\mathrm{JG}}_{1}$ be a winning strategy for Eve in the JG from $(p^{\prime}_{0},q_{0})$ (for some $p^{\prime}_{0}\in I$) with initial credit $|V|\mu_{\max}$. Let $\varphi_{q}=(p^{\prime}_{0},q_{0})(p^{\prime}_{0},q_{0},a_{0})(p^{\prime}_{0},q_{0},p^{\prime}_{1},a_{0})(p^{\prime}_{1},q_{1})\dots(p^{\prime}_{i},q_{i})$ be the play prefix consistent with $\sigma^{\mathrm{JG}}_{1}$ that corresponds to Adam playing the word $a_{0}\ldots a_{i-1}$ and choosing the states from the run $\varrho_{q}$. Since $\sigma^{\mathrm{JG}}_{1}$ is winning, Adam cannot enforce a negative energy level, in other words $\mathsf{EL}_{|V|\mu_{\max}}(\varphi_{q})\geq 0$, hence: $w(\varrho_{q})-w(p^{\prime}_{0}a_{0}p^{\prime}_{1}\dots a_{i-1}p^{\prime}_{i})\leq|V|\mu_{\max}.$ Second, by Lemma 26, $(p_{i}^{\prime},p_{i})\in W^{\mathrm{JG}}$, hence Eve has a winning strategy $\sigma^{\mathrm{JG}}_{2}$ in the JG starting from $(p_{i}^{\prime},p_{i})$ with initial credit $|V|\mu_{\max}$. Let $\varphi_{p,2}=(p^{\prime}_{i},p_{i})(p^{\prime}_{i},p_{i},a_{i})(p^{\prime}_{i},p_{i},p^{\prime}_{i+1},a_{i})(p^{\prime}_{i+1},p_{i+1})\dots(p^{\prime}_{n},p_{n})$ be the play prefix consistent with $\sigma^{\mathrm{JG}}_{2}$ that corresponds to Adam playing the word $a_{i}\ldots a_{n}$ and choosing the states from the run $\varrho_{p,2}$. Since $\sigma^{\mathrm{JG}}_{2}$ is winning, $p_{n}^{\prime}$ is a final state and (for the same reason as above) we have $w(\varrho_{p,2})-w(p^{\prime}_{i}a_{i}p^{\prime}_{i+1}\dots a_{n-1}p^{\prime}_{n})\leq|V|\mu_{\max}=|V|\mu_{\max}.$ Finally, since $\varrho_{p}$ is maximal by hypothesis, $w(p^{\prime}_{0}a_{0}p^{\prime}_{1}\dots a_{n-1}p^{\prime}_{n})\leq w(\varrho_{p})$. Since $w(\varrho_{p})=w(\varrho_{p,1})+w(\varrho_{p,2})$, the desired result follows. ∎

Since, by definition of the JG, both $|V|$ and $\mu_{\max}$ are polynomial w.r.t. $|Q|$ and $w_{\max}$, using Proposition 4 gives us the following.

Theorem 6**.**

Given an automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$, if Eve wins the JG played on $\mathcal{N}$, then there exists a deterministic automaton $\mathcal{D}$ such that $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$, and whose size and maximal weight are polynomial w.r.t. $w_{\max}$, and exponential w.r.t. $|Q|$.

With the results above, we are now in position to prove an \EXP upper bound for the $r$-regret problem.

Proof of Theorem 5.

Given an automaton $\mathcal{N}$ and $r\in\mathbb{N}$, we first determine whether Eve wins the JG played on $\mathcal{N}=(Q,I,A,\Delta,w,F)$. To do so, we determine the winner of the corresponding EGR from all $(p,q)\in I^{2}$ with initial credit $|V|\mu_{\max}$. We can then, in polynomial time, decide if there exists $p\in I$ such that, for all $q\in I$, Eve can win the EGR from $(p,q)$. If the latter does not hold, then by contrapositive of Lemma 22, $\mathcal{N}$ is not $r$-regret determinizable. Otherwise, we construct $\mathcal{D}$ such that $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$ and $\mathcal{D}$ is deterministic using Theorem 6. Finally, we use $\mathcal{D}$ to decide if Eve wins the $r$-regret game using Proposition 21. Since $\mathcal{D}$ is of size exponential w.r.t. to $\mathcal{N}$ but its maximal weight is polynomial w.r.t. $w_{\max}$, the resulting energy game without resets can be solved in exponential time by Proposition 20. ∎

As a corollary, we obtain that the existential version of the $r$-regret problem is also decidable. More precisely, using the techniques we have just presented, we are able to decide the question: does there exist $r\in\mathbb{N}$ such that a given automaton $\mathcal{N}$ is $r$-regret determinizable? The algorithm to decide the latter question is almost identical to the one we give for the $r$-regret problem. The only difference lies in the last step, that is, the energy game without resets constructed from the deterministic version of the automaton that one can obtain from the JG. Instead of using a function of $r$ as initial credit, we ask if Eve wins the energy game with initial credit $|V|\mu_{\max}$—we also remove the gadget using vertices $\bot^{r}_{1},\bot^{r}_{2}$ which ensure a regret of at most $r$.

Theorem 7**.**

Given an automaton, deciding whether there exists $r\in\mathbb{N}$ such that it is $r$-regret determinizable is in \EXP.

4.2 Lower bound

In this section we argue that the complexity of the algorithm we described in the previous section is optimal. More precisely, the $r$-regret problem is \EXP-hard even if the regret threshold $r$ is fixed.

Theorem 8**.**

Deciding the $r$-regret problem for a given automaton is \EXP-hard, even for fixed $r\in\mathbb{N}_{>0}$.

Observe that, in regret games, Eve may need to keep track of all runs of the given automaton on the word $\alpha$ which is being “spelled” by Adam. Indeed, if she has so far constructed the run $\varrho$ and Adam chooses symbol $a$ next, then her choice of transition to extend $\varrho$ may depend on the set of states at which alternative runs of the automaton on $\alpha$ end. The set of all such configurations is exponential.

Our proof of the $r$-regret problem being \EXP-hard makes sure that Eve has to keep track of a set of states as mentioned above. Then, we encode configurations of a binary counter into the sets of states so that the set of states at which Eve believes alternative runs could be at, represent a valuation of the binary counter. Finally, we give gadgets which simulate addition of constants to the current valuation of the counter. These ingredients allow us to simulate Countdown games [JSL08] using regret games. As the former kind of games are \EXP-hard, the result follows. The same reduction has been used to show that regret minimization against eloquent adversaries in several quantitative synthesis games is \EXP-hard [HPR16].

5 Further research directions

When the regret $r$ is given, the $r$-regret determinization problem is \EXP-complete. When $r$ is not given, the problem is in \EXP but we did not found any lower bound other than ¶-hardness. Characterizing the precise complexity of this problem is open.

The latter is related to the following question. From our decision procedure for solving the existential regret problem, it appears that if a WA is $r$-regret determinizable for some $r$, it is also $r^{\prime}$-regret determinizable for some $r^{\prime}$ that depends exponentially on the WA. So far, we have not found any family of WA that exhibit exponential regret behaviour, and the best lower bound we have is quadratic in the size of the WA (see Appendix E).

Finally, we would like to investigate the notions of delay- and regret-determinization for other measures, such as discounted sum [CDH10] or ratio [FGR12]. These notions also make sense for other problems, such as comparison and equality of weighted automata (which are undecidable for max-plus automata), and disambiguation (deciding whether a given WA is equivalent to some unambiguous one) [KL09].

Appendix A On Proposition 3

Ratio vs. difference. We remark that the results from [AKL10] are on minimizing regret with respect to the ratio measure and not the difference. However, ratio $1$ coincides with difference [math].

Determinization by pruning & (N,min,+) vs. (Z,max,+). In [AKL10] the authors actually consider automata over the tropical semiring. That is, their automata can only have non-negative integers and they use $\min$ instead of $\max$ to aggregate multiple runs of the automaton over the same word. However, it is easy to see that Eve wins an $r$-regret game played on an automaton $\mathcal{N}$ with integer weights if and only if she wins an $r$-regret game on the same automaton with weights “shifted” so they all become negative (recall we use $\max$ and not $\min$). More precisely we subtract $w_{\max}$ from the weights of all transitions, then multiply them all by $-1$, and denote the resulting automaton by $\mathcal{M}$. Clearly, the $(\mathbb{N}\cup\{+\infty\},\min,+)$-automaton $\mathcal{M}$ is $r$-regret determinizable if and only if the $(\mathbb{Z}\cup\{-\infty\},\max,+)$-automaton $\mathcal{N}$ is $r$-regret determinizable.

Appendix B Proof of Proposition 4

We present here in details the sketched construction. Let us define $\mathcal{D}=(Q^{\prime},\{q_{I}^{\prime}\},A,\Delta^{\prime},F^{\prime},w^{\prime})$ as follows.

• •

$Q^{\prime}$ is the set of functions from $Q$ to the set $\{-B,\ldots,B\}\cup\{-\infty\}$. The idea is that, on input $u$, $\mathcal{D}$ deterministically chooses a run $\varrho$ of $\mathcal{N}$ on $u$, outputs the corresponding weight, and uses its state to keep in memory, for each state $q\in Q$, the delay between $\varrho$ and the maximal run of $\mathcal{N}$ on $u$ ending in $q$;

• •

$q_{I}^{\prime}$ is the function mapping each initial state of $\mathcal{N}$ to [math], and all the other states to $-\infty$;

• •

We now define $\Delta^{\prime}$ and $w^{\prime}$. For every pair $(g,a)\in Q^{\prime}\times A$, we have $(g,a,\delta_{g,a})\in\Delta^{\prime}$ and $w^{\prime}(g,a,g^{\prime})=w_{g,a}$, where $\delta_{g,a}$ and $w_{g,a}$ are constructed as follows. First, we update the information concerning the runs of $\mathcal{N}$ contained in $g$. For every $q\in Q$, let

[TABLE]

The runs whose weight is too low are dropped. Let $Q_{B}\subseteq Q$ be the set of states $q$ such that $m_{p}-m_{q}\leq B$ for every $p\in Q$. In particular, if $m_{q}=-\infty$, $q\notin Q_{B}$. For every $q\in Q\setminus Q_{B}$, we set $\delta_{g,a}(q)=-\infty$. Then, $w_{g,a}$ is defined as the weight corresponding to the maximal accepting run, if any is left, and to the value of the maximal (non accepting) run otherwise. Formally, if $Q_{B}\cap F=\varnothing$, then $w_{g,a}=max\{m_{q}\>\mid\>q\in Q\}$, otherwise $w_{g,a}=max\{m_{q}\>\mid\>q\in F\}$. Finally, the state is updated accordingly. For every $q\in Q_{B}$, we set $\delta_{g,a}(q)=m_{q}-w_{g,a}$.

• •

$F^{\prime}$ is the set of functions $g\in Q^{\prime}$ such that $g(q_{f})\neq-\infty$ for some final state $q_{f}\in F$.

By definition, $\mathcal{D}$ is complete and deterministic, $|Q^{\prime}|=(2B+2)^{|Q|}$ and its maximal weight is $B+w_{\max}$. In order to complete the proof of Theorem 6, we need to prove that $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$. To do so, we expose three properties satisfied by $\mathcal{D}$.

Given a run $\varrho=p_{0}a_{0}p_{1}\ldots a_{n-1}p_{n}$ of $\mathcal{N}$, let us call $\varrho$ good if for every $0\leq i\leq n$, and for every run $\varrho_{q}=q_{0}a_{0}q_{1}\dots a_{i-1}q_{i}$,

[TABLE]

Proposition 27 ensures us that every maximal accepting run of $\mathcal{N}$ is good. Let $u\in A^{*}$, let $g_{0}a_{0}g_{1}\ldots a_{n-1}g_{n}$ be the run of $\mathcal{D}$ on $u$, and for every $0\leq i\leq n$ let $w_{i}$ denote the weight $w^{\prime}(g_{0}a_{0}g_{1}\ldots a_{i-1}g_{i})$.

P1:

For every $q\in F$, $g_{n}(q)\leq 0$, and if $g_{n}(p)\neq-\infty$ for at least one state $p\in F$, then there exists $q\in F$ such that $g_{n}(q)=0$.

P2:

Let $q\in Q$. If $g_{n}(q)\neq-\infty$, then there exists an initial run $\varrho=q_{0}a_{0}q_{1}\ldots a_{n-1}q_{n}$ of $\mathcal{N}$ on $u$ such that $q_{n}=q$ and $w(\varrho)=w_{n}+g_{n}(q)$.

P3:

Let $\varrho=p_{0}a_{0}p_{1}\ldots a_{n-1}p_{n}$ be an initial run of $\mathcal{N}$ on $u$. If $\varrho$ is good, then $w_{n}+g_{n}(q_{n})\geq w(\varrho)$.

Proof.

P1 follows immediately from the definition of $\Delta^{\prime}$. P2 and P3 are proved by induction on the size of $u$. If $u=\varepsilon$, then the state $g_{n}$ reached by $\mathcal{D}$ on input $u$ is the initial state $q_{I}^{\prime}$ of $\mathcal{D}$, and the weight $w_{n}$ corresponding to this run is [math]. Then, by definition of $I^{\prime}$, for every $q\in Q$ either $q$ is initial and $q_{I}^{\prime}(q)=0$, which is the value of the initial run $\varrho^{\prime}=q$ of $\mathcal{N}$ on $\varepsilon$, or $q$ is not initial and $q_{I}^{\prime}(q)=-\infty$. This proves P2. Conversely, every initial run $\varrho$ of $\mathcal{N}$ on $u$ is of the form $q_{I}$ for some $q_{I}\in I$, and $q_{I}^{\prime}(q_{I})=0$, which proves P3. Now suppose that $u=va$ for some $v\in A^{*}$ and $a\in A$, and that P2 and P3 hold for $v$.

Let us first prove that P2 holds for $u$. Suppose that $g_{n}(q)\neq-\infty$. By definition of $\Delta^{\prime}$, there exists $p\in Q$ and $(p,a,q)\in\Delta$ such that $g_{n}(q)=g_{n-1}(p)+w(p,a,q)-w^{\prime}(g_{n-1},a,g_{n})$. Then $g_{n-1}(p)\neq-\infty$, hence, by the induction hypothesis, there exists an initial run $\varrho^{\prime}=q_{0}a_{0}q_{1}\ldots a_{n-2}q_{n-1}$ of $\mathcal{N}$ on $v$ such that $q_{n-1}=p$ and $w(\varrho^{\prime})=w_{n-1}+g_{n-1}(p)$. Then the run $\varrho^{\prime}aq$ of $\mathcal{N}$ on $u$ satisfies the statement of P2, since

[TABLE]

Finally, we prove P3. Suppose that $\varrho$ is good. First, note that the run $p_{0}a_{0}p_{1}\ldots a_{n-2}p_{n-1}$ on $v$, which is obtained by removing the last transition of $\varrho$, is also good. Hence, by the induction hypothesis,

[TABLE]

Second, if we suppose that $g_{n}(p_{n})=-\infty$, we obtain a contradiction with the fact that $\varrho$ is good, since, using P2 and the definition of $\Delta^{\prime}$, we are able to build a run $\psi$ on $u$ such that $w(\varrho)<B-w(\psi)$. Hence $g_{n}(p_{n})\neq-\infty$, and, by definition of $\Delta^{\prime}$,

[TABLE]

These inequalities imply the correctness of P3, since

[TABLE]

∎

Corollary 28**.**

The function defined by $\mathcal{D}$ is equal to $\llbracket\mathcal{N}\rrbracket$.

Proof.

Let us begin by proving that for every input word $u$, $\llbracket\mathcal{N}\rrbracket(u)\geq\llbracket\mathcal{D}\rrbracket(u)$. Let $u\in\mathcal{L}_{\mathcal{D}}$, and let $g$ be the state reached by $\mathcal{D}$ on input $u$. Then $g$ is final, hence, by definition of $F^{\prime}$, there exists a state $q_{f}\in F$ such that $g(q_{f})\neq-\infty$. Moreover, by P1, there exists a final state $p_{f}\in F$ such that $g_{n}(p_{f})=0$. This implies, by P2, the existence of an initial run $\varrho=p_{0}a_{0}p_{1}\ldots a_{n-1}p_{n}$ of $\mathcal{N}$ on $u$ such that $p_{n}=p_{f}\in F$ and $w(\varrho)=\llbracket\mathcal{D}\rrbracket(u)$. Since $q_{n}$ is a final state, $\varrho$ is accepting, hence $\llbracket\mathcal{N}\rrbracket(u)\geq w(\varrho)=\llbracket\mathcal{D}\rrbracket(u)$.

Finally, we prove that, conversely, for every input word $v$, $\llbracket\mathcal{D}\rrbracket(u)\geq\llbracket\mathcal{N}\rrbracket(u)$. Let $v\in\mathcal{L}_{\mathcal{N}}$, let $\psi$ be a maximal accepting run of $\mathcal{N}$ on $v$, and let $q\in F$ be the corresponding final state. Let $g_{v}$ be the state of $\mathcal{D}$ reached on input $v$, and let $w_{v}$ be the associated output. By Proposition 27, $\psi$ is good, hence by P3, $w_{v}+g_{v}(q)\geq w(\psi)=\llbracket\mathcal{N}\rrbracket(v)$. Therefore $g_{v}(q)\neq-\infty$, and, since $q$ is a final state of $\mathcal{N}$, $g_{v}$ is a final state of $\mathcal{D}$. Moreover, by P1, $g_{v}(q)\leq 0$, hence $\llbracket\mathcal{D}\rrbracket(u)=w_{v}\geq\llbracket\mathcal{N}\rrbracket(u)$. ∎

Appendix C Proof of Lemma 12

Proof.

If $\mathcal{N}$ is [math]-regret determinizable, then $\mathcal{N}$ is [math]-delay determinizable by Proposition 11. Now suppose that $\mathcal{N}$ is [math]-delay determinizable, and let $\mathcal{D}$ be a [math]-delay determinizer of $\mathcal{N}$. Using $\mathcal{D}$, we define a winning strategy $\sigma_{\mathcal{D}}$ for Eve in the [math]-regret game played on $\mathcal{N}$. Given a sequence $q_{0}a_{0}\ldots q_{n-1}a_{n-1}$ in $(Q\cdot A)^{*}$, the state $\sigma_{\mathcal{D}}(q_{0}a_{0}\ldots q_{n-1}a_{n-1})$ is defined as follows. Let $\alpha$ denote the input word $a_{0}\ldots a_{n-1}$. If $\mathcal{D}$ has no initial run on $\alpha$, this word is not a prefix of any word of $\mathcal{L}_{\mathcal{N}}$, hence whatever Eve does, Adam will not be able to win. We set $\sigma_{\mathcal{D}}(q_{0}a_{0}\ldots q_{n-1}a_{n-1})=q_{n-1}$. Otherwise, let $\varrho_{\alpha}=p_{0}a_{0}\ldots p_{n-1}a_{n-1}p_{n}$ be the initial run of $\mathcal{D}$ on $\alpha$. Since $\mathcal{D}$ is a [math]-delay determinizer of $\mathcal{N}$, there exists an initial run $\varrho^{\prime}_{\alpha}=p^{\prime}_{0}a_{0}\ldots p^{\prime}_{n-1}a_{n-1}p^{\prime}_{n}$ of $\mathcal{N}$ such that for every $1\leq i\leq n$, $w(p_{0}^{\prime}\dots p_{i}^{\prime})=w^{\prime}(p_{0}\dots p_{i})$. Moreover, since $\mathcal{N}$ is pair-deterministic, such a run is unique. We set $\sigma_{\mathcal{D}}(q_{0}a_{0}\ldots q_{n-1}a_{n-1})=p^{\prime}_{n}$. Note that, for every $1\leq i\leq n-1$, the run $\varrho_{a_{0}\ldots a_{i}}$ is equal to the prefix $p_{0}a_{0}\ldots p_{i}a_{i}p_{i+1}$ of $\varrho_{\alpha}$, since $\mathcal{D}$ is deterministic. Therefore, the run $\varrho^{\prime}_{a_{0}\ldots a_{i}}$ is equal to the prefix $p^{\prime}_{0}a_{0}\ldots p^{\prime}_{i}a_{i}p^{\prime}_{i+1}$ of $\varrho^{\prime}_{\alpha}$, since $\mathcal{N}$ is pair-deterministic. Then $\sigma(p^{\prime}_{0}a_{0}\ldots p^{\prime}_{i}a_{i})=p^{\prime}_{i+1}$ for every $1\leq i\leq n-1$, hence $\sigma(a_{0}\ldots a_{n-1})=\varrho^{\prime}$ and

[TABLE]

This proves that $\sigma_{\mathcal{D}}$ is a winning strategy for the [math]-regret game played on $\mathcal{N}$. ∎

Appendix D Making an automaton pair-deterministic

Subset construction. Let $\mathcal{N}=(Q,I,A,\Delta,w,F)$ be an automaton. Let $\mathcal{P}(\mathcal{N})=(Q^{\prime},I^{\prime},A,\Delta^{\prime},w^{\prime},F^{\prime})$ be the automaton defined as follows.

• •

$Q^{\prime}=\mathcal{P}(Q)$;

• •

$I^{\prime}=\{I\}$;

• •

$\Delta^{\prime}=\{(U,a,\Delta_{a}^{x}(U))\>\mid\>a\in A,x\in\textsf{Im}(w)\}$, where $\Delta_{a}^{x}(U)=\bigcup_{p\in U}\{q\in Q\>\mid\>(p,a,q)\in\Delta,w(p,a,q)=x\}$;

• •

$w^{\prime}:\Delta^{\prime}\rightarrow\mathbb{Z}$, $(U,a,\Delta_{a}^{x}(U))\mapsto x$;

• •

$F^{\prime}=\{P\subset Q\>\mid\>P\cap F\neq\varnothing\}$.

Lemma 29**.**

The subset construction satisfies the following properties.

$\mathcal{N}\subseteq_{0}\mathcal{P}(\mathcal{N})$; 2. 2.

$\mathcal{P}(\mathcal{N})\subseteq_{0}\mathcal{N}$; 3. 3.

$\llbracket\mathcal{P}(\mathcal{N})\rrbracket=\llbracket\mathcal{N}\rrbracket$.

Proof.

1. Let $\varrho=q_{0}a_{0}\dots a_{n-1}q_{n}$ be an accepting run of $\mathcal{N}$. Let $U_{0}=I$, and for every $1\leq i\leq n$, let $U_{i}=\Delta_{a_{i-1}}^{w(q_{i-1},a_{i-1},q_{i})}(U_{i-1})$. Note that for every $0\leq i\leq n$, $q_{i}\in U_{i}$. Then $\varrho^{\prime}=U_{0}a_{0}\dots a_{n-1}U_{n}$ is an accepting run of $\mathcal{P}(\mathcal{N})$, and for every $0\leq i<n$, $w^{\prime}(U_{i},a_{i},U_{i+1})=w(q_{i},a_{i},q_{i+1})$. Therefore, $\mathcal{N}\subseteq_{0}\mathcal{P}(\mathcal{N})$.

2. Let $\varrho=U_{0}a_{0}\dots a_{n-1}U_{n}$ be an accepting run of $\mathcal{P}(\mathcal{N})$. Let $q_{n}$ be any element of $U_{n}\cap F$. For every $0<i<n$, suppose that $q_{i+1}\in U_{i+1}$ is defined, and let $q_{i}\in U_{i}$ be inductively defined as follows. By definition of $\Delta^{\prime}$, $U_{i+1}=\Delta_{a_{i}}^{w^{\prime}(U_{i},a_{i},U_{i+1})}(U_{i})$, hence, as $q_{i+1}\in U_{i+1}$, there exists $q_{i}\in U_{i}$ such that $(q_{i},a_{i},q_{i+1})\in\Delta$ and $w(q_{i},a_{i},q_{i+1})=w^{\prime}(U_{i},a_{i},U_{i+1})$. Then $\varrho^{\prime}=q_{0}a_{0}\dots a_{n-1}q_{n}$ is an accepting run of $\mathcal{N}$, and $w(q_{i},a_{i},q_{i+1})=w^{\prime}(U_{i},a_{i},U_{i+1})$ for all $0\leq i<n$. Therefore, $\mathcal{P}(\mathcal{N})\subseteq_{0}\mathcal{N}$.

3. This property follows immediately from the two others and Lemma 10 item 3. ∎

Appendix E A lower bound on the required $r$ for $r$-regret determinizability

In this section we give an example of an automaton which requires a quadratic regret threshold $r$ for it to be $r$-regret determinizable.

Proposition 30**.**

Given an automaton $\mathcal{N}$, a regret $r$ as big as $\mathcal{O}(|V|)$ might be needed for it to be $r$-regret determinizable.

Proof.

Let $k\in\mathbb{N}_{>0}$ and consider the corresponding $\mathcal{N}_{k}$ automaton constructed as shown in Fig. 6. Note that $\mathcal{N}_{k}$ consists of two deterministic automata. As the latter are also disjoint, the only decision for Eve to make in this game is to start from $p_{1}$ or from $q_{1}$. Further, notice that if she does start in $p_{1}$, then any word with more than $k$ consecutive $a$’s forces her into the state $\bot$ which is not accepting. An alternative run starting from $q_{1}$ reaches $q_{k}$, which is accepting, when reading the same word. Thus, Eve really has no choice but to start in $q_{1}$ to realize at least the domain of $\mathcal{N}_{k}$.

Observe that any word with more than $k$ consecutive $a$’s is not accepted by the left sub-automaton. Hence, the maximal regret of the strategy for Eve which starts from $q_{1}$ is witnessed by a word of the form $a^{i_{1}}b^{j_{1}}\dots a^{i_{n}}b^{j_{n}}$ where $i_{\ell}\leq k$ for all $1\leq\ell\leq n$. Such a word is assigned a value of $\sum_{\ell=1}^{n}i_{\ell}$ by the left sub-automaton. On the other hand, any word with $k$ or more $b$’s is assigned a value equivalent to the length of the word minus $k$ by the right automaton. It is now easy to see that, if Eve starts in $q_{1}$, she will have a regret value of at least $k^{2}$. This value is realized, for instance, by the word $(a^{k}b)^{k}$. ∎

Appendix F Proof of Proposition 20 (On Energy Games with Resets)

In this section we study the properties of EGRs. Let us start by establishing that they are uniformly positionally determined. (The latter is even stronger than positional determinacy. A game is uniformly positionally determined if, for all instances of the game, it is always the case that both players have a positional strategy which is winning from all vertices from which it is possible for that player to win, i.e. his winning region.) In order to prove this, we will make use of a First Cycle Game [AR14].

To simplify our arguments, in the sequel we will fix an arbitrary unique initial vertex $v_{I}$ from which the game starts.

First cycle energy games. A first cycle energy game (FCEG) is played by Eve and Adam. Formally, an FCEG is—just like an EGR—a tuple $\mathcal{G}=(V,V_{\exists},v_{I},E,E_{\varrho},w)$ where the digraph $(V,E)$ has no sinks. We call $\mathcal{G}$ the arena on which both an EGR or an FCEG could be played. The main difference between the FCEG and the EGR played on $\mathcal{G}$ is that the former is a finite game. More precisely, the FCEG is played up to the point when the first cycle is formed. The winner of the game is then determined by looking at the cycle: if it has a negative sum of weights and it does not contain a reset edge, then Adam wins; else Eve wins. In other words, Adam and Eve choose edges, from $v_{I}$ to form a lasso, i.e. a finite path $\varphi=v_{0}\dots v_{i}\dots v_{n}$ such that $v_{n}=v_{i}$ and $v_{j}\neq v_{k}$ for all $0\leq j<k<n$. We then say that $\varphi$ is winning for Eve if and only if $(v_{j},v_{j+1})\in E_{\varrho}$ for some $i\leq j<n$ or $\sum_{\ell=i}^{n-1}w(v_{\ell},v_{\ell+1})\geq 0$, otherwise $\varphi$ is winning for Adam. (Note that the property of $\varphi$ being winning for Eve is determined solely on the “cycle part” of the lasso. More specifically, the cycle $v_{i}\dots v_{n}$.)

EGRs are greedy. Let $Y$ be a cycle property. We say an infinite-duration game is $Y$-greedy (or just greedy, when $Y$ is clear from the context) if and only if:

• •

all plays $\pi$ such that every cycle in $\pi$ satisfies $Y$ are winning for Eve; and

• •

all plays $\pi$ such that every cycle in $\pi$ does not satisfy $Y$ are winning for Adam.

We will now focus on the cycle property used to determine if Eve wins the FCEG defined above: either the cycle contains a reset edge or the sum of the weights of cycle is non-negative. Let us start with the following observation.

Lemma 31**.**

If a play $\pi$ is such that all of its cycles have negative sum of weights, then for all $c_{0}\in\mathbb{N}$ there is a finite path $\varphi$ which is a prefix of $\pi$ and for which it holds that $\mathsf{EL}_{c_{0}}(\varphi)<0$.

We claim that EGRs are greedy with respect to this property.

Lemma 32**.**

An EGR $\mathcal{G}=(V,V_{\exists},v_{I},E,E_{\varrho},w)$ with initial credit $|V|w_{\max}$ is greedy.

Proof.

For convenience, we will focus on simple cycles.

Let $\pi=v_{0}v_{1}\dots$ be a play of the game such that all cycles from $\pi$ either contain a reset edge or have non-negative sum of weights. We will argue that, for all prefixes $\varphi$ of $\pi$ with length at most $n$ we have that $\mathsf{EL}_{c_{0}}(\varphi)\geq 0$. We proceed by induction on $n$. If $n=0$ then the claim holds trivially. Now, let us consider an arbitrary prefix $\varphi=v_{0}\dots v_{n+1}$. By induction hypothesis, we have that $\mathsf{EL}_{c_{0}}(v_{0}\dots v_{n})\geq 0$. Let $i$ be the index of the latest occurrence of a reset edge in $\varphi$ (with $i=0$ if there is no such edge). If $\mathsf{EL}_{c_{0}}(\varphi)<0$ then clearly $n-i>|V|$ since at least $|V|$ edges are necessary to go from $c_{0}=|V|w_{\max}$ to a negative number in $\mathcal{G}$. Furthermore, it follows that between $i$ and $n$ we have cycle $\chi=v_{i}\dots v_{j}$ which does not contain a reset edge and such that the sum of its transition weights is negative. This contradicts our assumption that all cycles from $\pi$ have a reset edge or non-negative sum of weights. Hence, the claim holds by induction and the play is winning for Eve with initial credit $|V|w_{\max}$.

Let $\pi=v_{0}v_{1}\dots$ be a play of the game such that all cycles from $\pi$ have negative sum of weights. From Lemma 31 we have that for some prefix $\varphi$ of $\pi$ the energy level becomes negative, i.e. $\mathsf{EL}_{c_{0}}(\varphi)<0$. Hence, the play is winning for Adam. ∎

Since EGRs are greedy, it follows from [AR14] that strategies transfer between an EGR and an FCEG played on the same arena. More formally,

Proposition 33**.**

Let $\mathcal{G}=(V,V_{\exists},v_{I},E,E_{\varrho},w)$ be an arena. Every memoryless strategy $s$ for Eve (Adam) in the ERG played on $\mathcal{G}$ with initial credit $|V|w_{\max}$ is winning for her (him) if and only if $s$ is winning for her (him) in the FCEG played on $\mathcal{G}$.

More cycle properties. Let $Y$ be a cycle property. We say $Y$ is closed under cyclic permutations if for any cycle $\chi=v_{0}v_{1}\dots v_{n-1}v_{0}$ such that $\chi\models Y$ we have that $v_{1}v_{2}\dots v_{n-1}v_{0}v_{1}\models Y$. We also say $Y$ is closed under concatenation if for any two cycles $\chi=v_{0}v_{1}\dots v_{n-1}v_{0}$ and $\chi^{\prime}=v_{0}v^{\prime}_{1}\dots v^{\prime}_{m-1}v_{0}$ such that $\chi,\chi^{\prime}\models Y$ we have that $\chi\dot{v}^{\prime}_{1}\dots v^{\prime}_{m-1}v_{0}\models Y$.

Lemma 34**.**

The property of a cycle being winning for Eve (Adam) in an FCEG is closed under cyclic permutations and concatenation.

Proof.

Clearly, a cycle being winning for Adam is closed under both operations. Indeed, by commutativity of addition, if a cycle has negative sum of weights, the order of the weights does not matter. Additionally, the concatenation of two negatively weighted cycles concatenated yields a negatively weighted cycle.

Let us consider now the property of a cycle being winning for Eve. If it contains a reset edge then any cyclic permutation of the cycle will also contain it. If it does not have a reset edge then it must have a non-negative sum of weights. Thus, the result follows by commutativity of addition. Additionally, concatenation preserves containment of a reset edge and, again, two positively weighted cycles can only yield a positively weighted cycle when concatenated. ∎

It then follows immediately from Lemmas 32, 34 and [AR14] that EGRs and FCEGs are uniformly positionally determined.

Proposition 35**.**

Let $\mathcal{G}=(V,V_{\exists},v_{I},E,E_{\varrho},w)$ be an arena. The EGR played on $\mathcal{G}$ with initial credit $|V|w_{\max}$ and the FCEG played on $\mathcal{G}$ are both uniformly positionally determined.

Using Lemma 31 and Proposition 35 we can show that Eve wins an EGR with some initial credit $c_{0}\in\mathbb{N}$ if and only if she wins with initial credit $|V|w_{\max}$.

Proposition 36**.**

Let $\mathcal{G}=(V,V_{\exists},v_{I},E,E_{\varrho},w)$ be an arena Eve wins the EGR played on $\mathcal{G}$ with initial credit $|V|w_{\max}$ if and only if she wins it with some initial credit $c_{0}\in\mathbb{N}$.

Proof.

One direction is obvious: if Eve wins the EGR with initial credit $c_{0}=|V|w_{\max}$ then clearly she wins the EGR with some initial credit. We argue that if there exists some initial credit with which she wins the EGR then $|V|w_{\max}$ suffices. We will, in fact, show that the contrapositive holds. Suppose that Eve does not win the EGR with initial credit $|V|w_{\max}$. Then by determinacy of the EGR with that initial credit (Proposition 35), and using Proposition 33 together with Lemma 31 we have that Adam has a strategy $\tau$ in the EGR which, regardless of the initial credit, ensures a negative energy level is witnessed. Hence, there is no initial credit for which Eve wins. ∎

A pseudo-polynomial algorithm. We will reduce the problem of deciding if Eve wins an EGR with a given initial credit $c_{0}\in\mathbb{N}$ to that of deciding if she wins a safety game [AG11]. Safety games are played by Eve and Adam on an unweighted arena $(V,V_{\exists},v_{I},E,U)$ with a set $U\subseteq V$ of unsafe vertices which determine the goals of the players. Eve wins the safety game if she has a strategy which ensures no the play does not contain vertices from $U$, otherwise Adam wins. Safety games are known to be uniformly positionally determined and solvable in linear time [AG11].

More formally, for a given EGR $(V,V_{\exists},v_{I},E,E_{\varrho},w)$ and initial credit $c_{0}$, we define a safety game played on $(V^{\prime},V^{\prime}_{\exists},v^{\prime}_{I},E^{\prime},U)$ where

• •

$V^{\prime}=V\times\left(\{\bot\}\cup\{0,1,\dots,|V|w_{\max}\}\right)$,

• •

$V^{\prime}_{\exists}=V\times\left(\{\bot\}\cup\{0,1,\dots,|V|w_{\max}\}\right)$,

• •

$v^{\prime}_{I}=(v_{I},c_{0})$,

• •

$E^{\prime}$ includes the edge $((u,c),(q,v))$ if and only if

• –

$(u,v)\in E\setminus E_{\varrho}$, $c\neq\bot$, and $d=\max\{w(u,v)+c,|V|w_{\max}\}$ or

• –

$(u,v)\in E_{\varrho}$, $c\neq\bot$, and $d=\max\{w(u,v)+c_{0},|V|w_{\max}$ or

• –

$c=\bot$, $d=\bot$, and $u=v$.

• •

$U=V\times\{\bot\}$.

Informally, if the energy level goes above $|V|w_{\max}$ then we “bounce” it back to $|V|w_{\max}$.

Proposition 37**.**

Eve wins the EGR $(V,V_{\exists},v_{I},E,E_{\varrho},w)$ with initial credit $c_{0}\in\mathbb{N}$ if and only if she wins the safety game played on $(V^{\prime},V^{\prime}_{\exists},v^{\prime}_{I},E^{\prime},U)$.

Proof.

Clearly, if Eve wins the safety game then she wins the EGR with initial credit $c_{0}$.

Conversely, if she has a strategy $\sigma$ to win the EGR with initial credit $c_{0}$, then, by Proposition 35 she can do so with a uniformly positional strategy. That is, she has a strategy $\sigma^{\prime}$ which ensures that from any vertex from which she can win with some initial credit, she wins with $\sigma^{\prime}$ and initial credit $|V|w_{\max}$. We claim that Eve must also be able to win the safety game. Indeed, at least until the first time the energy level is “bounced” back, by playing according to $\sigma$, the energy level cannot become negative. For any play which does reach a point at which the energy level is “bounced” back, we observe that the reached vertex $u$ (the first component of the safety-game vertex $(u,c)$) is also reachable in the EGR by a play consistent with $\sigma$. Hence, $\sigma$ must be winning for Eve in the EGR played from $u$ with some initial credit. By Proposition 36, $|V|w_{\max}$ should suffice for $\sigma^{\prime}$ to be winning for her in the EGR from $u$. Henceforth, she plays according to $\sigma^{\prime}$ and the energy level cannot become negative by the above argument.

The result then follows by determinacy of safety games. ∎

Appendix G Proof of Proposition 21

Given an automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$ and $\mathcal{D}=(Q^{\prime},\{q^{\prime}_{I}\},A,\Delta^{\prime},w^{\prime},F^{\prime})$ such that $\mathcal{D}$ is deterministic and $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$, we construct the energy game without resets is $\mathcal{G}=(V,V_{\exists},E,\varnothing,\mu)$ as described in the sketch provided in the main body of the paper.

Since $\mathcal{G}$ is of size polynomial w.r.t. $\mathcal{D}$ and $\mathcal{N}$, and we have a pseudo-polynomial algorithm to determine the winner of energy games, it suffices for us to prove the following claim.

Lemma 38**.**

The automaton $\mathcal{N}$ is $r$-regret determinizable if and only if there exists $p_{I}\in I$ such that Eve wins the energy game without resets $\mathcal{G}$ from $(p_{I},q^{\prime}_{I})$ with initial credit $r+|Q^{\prime}|(w_{\max}+w_{\max}^{\prime})$.

Proof.

We will argue that if Eve wins the energy game, then she wins the $r$-regret game and if Adam wins the energy game, then she cannot win the $r$-regret game. The desired result follows from determinacy of energy games (Proposition 20).

Assume Eve wins the game from some $(p_{I},q^{\prime}_{I})$ with strategy $\sigma$. Clearly, any play consistent with $\sigma$ never reaches the vertex $\bot$. The strategy $\sigma$ can be turned into a strategy $\sigma^{\prime}$ for Eve in the regret game as follows: for every symbol given by Adam in the regret game, $\sigma^{\prime}$ selects a transition of $\mathcal{N}$ based on what $\sigma$ does in response to the deterministic transition of $\mathcal{D}$. More formally, for any word $\alpha=a_{0}\dots a_{n-1}\in A^{*}$ which can be extended to a word $\alpha^{\prime}\in\mathcal{L}_{\mathcal{N}}$, we have $\sigma^{\prime}(\varepsilon)=p_{I}$ and $\sigma^{\prime}(\alpha)=\sigma\left((p_{0},q_{0})(p_{0},q_{0},q_{1},a_{0})\dots(p_{n-1},q_{n-1},q_{n},a_{n-1})\right)$ where $p_{0}=p_{I},q_{0}=q^{\prime}_{I}$ and

[TABLE]

is consistent with $\sigma$. The latter is well defined since we have argued that no play consistent with $\sigma$ reaches $\bot$. Additionally, since Adam can choose to avoid $\top^{r}_{1},\top^{r}_{2}$, there are plays consistent with any strategy of Eve which do not reach these vertices. Finally, since we have assumed $\alpha$ can be extended to a word in the language of $\mathcal{N}$, $\top$ cannot be reached. For words which cannot be extended in this way, $\sigma^{\prime}$ behaves arbitrarily. Observe that if $\alpha\in\mathcal{L}_{\mathcal{N}}$, then $\alpha\in\mathcal{L}_{\mathcal{D}}$ and thus $p_{n}\in F$ since otherwise Adam could reach $\bot$ in the energy game when playing against $\sigma$, and this would contradict the fact that $\sigma$ is winning. Furthermore, we have that $\llbracket\mathcal{N}\rrbracket(\alpha)-\mathsf{Val}(\sigma^{\prime}(\alpha))\leq r$ since otherwise Adam could reach $\bot^{r}_{1}$ in the energy game when playing against $\sigma$ and make her lose the game (since $\llbracket\mathcal{N}\rrbracket(\alpha)=\llbracket\mathcal{D}\rrbracket(\alpha)=w(q_{0}\dots q_{n})$), again contradicting the fact that $\sigma$ is winning not be winning.

Assume Adam wins the game $\mathcal{G}$ from every $(p_{I},q^{\prime}_{I})$. Suppose, for a contradiction, that Eve has a strategy $\sigma$ with which she wins the $r$-regret game. Let $\sigma(\varepsilon)=p_{0}$ and $\tau$ be the strategy for Adam in the energy game which is winning for him from $(p_{0},q^{\prime}_{I})$. The strategy $\sigma$ can be turned into a strategy for Eve in the energy game by ignoring the states of $\mathcal{D}$ and choosing transitions of $\mathcal{N}$ when Adam chooses a symbol. Hence, the play $\pi^{(p_{0},q^{\prime}_{0})}_{\sigma\tau}$ in the energy game must be losing for Eve, by choice of $\tau$. If the play is losing because vertex $\bot$ is reached, then either $\sigma$ does not reach a final state of $\mathcal{N}$ after reading a word in $\mathcal{L}_{\mathcal{N}}$ or she got stuck and cannot continue choosing transitions. In both cases, this contradicts the fact that $\sigma$ is winning for her in the regret game. If the play is losing because vertices $\bot^{r}_{1}$ and $\bot^{r}_{2}$ were reached, then $\sigma$ cannot be winning in the regret game because it assigns a weight to a word $\alpha\in\mathcal{L}_{\mathcal{N}}$ that is too low w.r.t. to $\llbracket\mathcal{D}\rrbracket(\alpha)=\llbracket\mathcal{N}\rrbracket(\alpha)$. Finally, if the play is losing because the energy level drops below [math], despite the initial credit of $r+|Q^{\prime}|(w_{\max}+w_{\max}^{\prime})$, after prefix $\varphi=\dots(p_{n},q_{n})$, then since $\mathcal{D}$ is trim, there is a word $\beta=b_{0}\dots b_{m-1}$ such that $m\leq|Q^{\prime}|$ and there is an accepting of $\mathcal{D}$ from $q_{n}$ on $\beta$. Clearly then, the difference between the value of the run constructed by $\sigma$ and the value assigned by $\mathcal{D}$ to the overall word is strictly greater than $r$. Hence, $\sigma$ cannot be winning for Eve in the regret game. ∎

Appendix H Proof of Lemma 23

Proof.

Let $W^{\prime}$ denote the set of pairs $(p,t)\in Q^{2}$ such that $(p,q),(q,t)\in W^{\mathrm{JG}}$ for some $q\in Q$. Given $(p,t)\in W^{\prime}$, let $q_{p,t}\in Q$ denote the state such that $\mathsf{Cr}(p,q_{p,t})+\mathsf{Cr}(q_{p,t},t)$ is minimal. We prove that for every $(p,t)\in W^{\prime}$, $\mathsf{Cr}(p,t)\leq\mathsf{Cr}(p,q_{p,t})+\mathsf{Cr}(q_{p,t},t)$. The lemma then follows, by Proposition 20 and the definition of $W^{\mathrm{JG}}$.

The proof is done by exposing a positional strategy $\sigma$ for Eve in the JG played on $\mathcal{N}=(Q,I,A,\Delta,w,F)$. For every $(p,q)\in W^{\mathrm{JG}}$, let $\sigma_{(p,q)}$ denote a winning strategy for Eve in the JG played from $(p,q)$ with initial credit $\mathsf{Cr}(p,q)$. For every $(p,t,a)\in Q^{2}\times A$, if $(p,t)\in W^{\prime}$, let $\sigma((p,t,a))=\sigma_{(p,q_{p,t})}((p,q_{p,t})(p,q_{p,t},a))$. We now prove that, for every $p,t\in W^{\prime}$, the strategy $\sigma$ is winning for Eve in the JG played on $\mathcal{N}$ starting from $(p,t)$, with initial credit $\mathsf{Cr}(p,q_{p,t})+\mathsf{Cr}(q_{p,t},t)$. Suppose, towards a contradiction, that there exists a play consistent with $\sigma$

[TABLE]

such that $\mathsf{EL}_{c_{0}}(\varphi)<0$, where $c_{0}=\mathsf{Cr}(p_{0},q_{p_{0},t_{0}})+\mathsf{Cr}(q_{p_{0},t_{0}},t_{0})$. Moreover, let us suppose that we have chosen the play $\varphi$ such that there exists no play of shorter length satisfying this property.

First, let us set

[TABLE]

and $c_{1}=\mathsf{Cr}(p_{1},q_{p_{1},t_{1}})+\mathsf{Cr}(q_{p_{1},t_{1}},t_{1})$. By the hypothesis of minimality over the length of $\varphi$, we obtain that $\mathsf{EL}_{c_{1}}(\varphi^{\prime})\geq 0$. Now, let $q_{0}=q_{p_{0},t_{0}}$ and let $q_{1}^{\prime}=\sigma_{(q_{0},t_{0})}((p_{0},t_{0},a))$. Note that, by definition of $\sigma$, $p_{1}=\sigma_{(p_{0},q_{0})}((p_{0},q_{0},a))$. Therefore, by Lemma 24, $\mathsf{Cr}(p_{1},q^{\prime}_{1})\leq\mathsf{Cr}(p_{0},q_{0})+w(p_{0},a,p_{1})-w(q_{0},a,q^{\prime}_{1})$ and $\mathsf{Cr}(q^{\prime}_{1},t_{1})\leq\mathsf{Cr}(q_{0},t_{0})+w(q_{0},a,q^{\prime}_{1})-w(t_{0},a,t_{1})$. Moreover, by definition of $q_{p_{1},t_{1}}$, $c_{1}\leq\mathsf{Cr}(p_{1},q^{\prime}_{1})+\mathsf{Cr}(q^{\prime}_{1},t_{1})$, hence

[TABLE]

Therefore, we obtain

[TABLE]

which is a contradiction. ∎

Appendix I Proof of Theorem 7

We will adapt the proof of Proposition 21 to show that the existential $r$-regret problem can be solved by reduction to an energy game if a deterministic version of the automaton is known. Together with the techniques developed in Section 4.1, this will imply the existential $r$-regret problem is decidable in exponential time.

Proposition 39**.**

Given an automaton $\mathcal{N}=(Q,I,A,\Delta,w,F)$ and $\mathcal{D}=(Q^{\prime},\{q^{\prime}_{I}\},A,\Delta^{\prime},w^{\prime},F^{\prime})$ such that $\mathcal{D}$ is deterministic and $\llbracket\mathcal{D}\rrbracket=\llbracket\mathcal{N}\rrbracket$, the existential $r$-regret problem for $\mathcal{N}$ is decidable in time polynomial in $|Q|$, $|Q^{\prime}|$, $|A|$, $w_{\max}$, and $w_{\max}^{\prime}$.

Proof.

As for the proof of Proposition 21, we construct an energy game without resets which simulates the regret game played on $\mathcal{N}$ while using $\mathcal{D}$ to compare the weights of transitions chosen by Eve to those of the maximal run of $\mathcal{N}$. Crucially, we will not add gadgets to punish Eve if she does not ensure a regret of at most $r$. This is because we do not fix such an $r$ a priori. Formally, the energy game without resets is $\mathcal{G}=(V,V_{\exists},E,\varnothing,\mu)$ where:

• •

$V=Q^{2}\cup Q^{3}\times A\cup\{\top,\bot\}$;

• •

$V_{\exists}=Q^{3}\times A$;

• •

$E$ contains edges to simulate transitions of $\mathcal{N}$ and $\mathcal{D}$, i.e. $\{\left((p,q),(p,q,q^{\prime},a)\right)\>\mid\>(q,a,q^{\prime})\in\Delta^{\prime}\}\cup\{\left((p,q,q^{\prime},a),(p^{\prime},q^{\prime})\right)\>\mid\>(p,a,p^{\prime})\in\Delta\}$, edges required to verify Eve does not reach a non-final state when $\mathcal{D}$ accepts, i.e. $\{\left((p,q),\bot\right)\>\mid\>p\not\in F\land q\in F^{\prime}\}\cup\{(\bot,\bot)\}$, and edges to punish one of the players if an automaton blocks, i.e. $\{\left((p,q),\top\right)\>\mid\>\lnot\exists(q,a,q^{\prime})\in\Delta^{\prime}\}\cup\{\left((p,q,q^{\prime},a),\bot\right)\>\mid\>\lnot\exists(p,a,p^{\prime})\in\Delta\}\cup\{(\top,\top)\}$;

• •

$\mu:E\to\mathbb{Z}$ is such that

• –

$\left((p,q,q^{\prime},a),(p^{\prime},q^{\prime})\right)\mapsto w(p,a,p^{\prime})-w^{\prime}(q,a,q^{\prime})$,

• –

$(\bot,\bot)\mapsto-1$,

• –

$(\top,\top)\mapsto 1$, and

• –

$e\mapsto 0$ for all other $e\in E$.

We then claim that for some $p_{I}\in I$, Eve wins the energy game without resets $\mathcal{G}$ from $(p_{I},q^{\prime}_{I})$ with initial credit $|V|\mu_{\max}$ if and only if $\mathcal{N}$ is $r$-regret determinizable for some $r\in\mathbb{N}$. As before, the result will follow from the fact $\mathcal{G}$ is of size polynomial w.r.t. $\mathcal{D}$ and $\mathcal{N}$, and the application of the pseudo-polynomial algorithm to determine the winner of $\mathcal{G}$.

Assume Eve wins the game from some $(p_{I},q^{\prime}_{I})$ with strategy $\sigma$. Clearly, any play consistent with $\sigma$ never reaches the vertex $\bot$. The strategy $\sigma$ can be turned into a strategy $\sigma^{\prime}$ for Eve in the regret game as follows: for every symbol given by Adam in the regret game, $\sigma^{\prime}$ selects a transition of $\mathcal{N}$ based on what $\sigma$ does in response to the deterministic transition of $\mathcal{D}$. More formally, for any word $\alpha=a_{0}\dots a_{n-1}\in A^{*}$ which can be extended to a word $\alpha^{\prime}\in\mathcal{L}_{\mathcal{N}}$, we have $\sigma^{\prime}(\varepsilon)=p_{I}$ and $\sigma^{\prime}(\alpha)=\sigma\left((p_{0},q_{0})(p_{0},q_{0},q_{1},a_{0})\dots(p_{n-1},q_{n-1},q_{n},a_{n-1})\right)$ where $p_{0}=p_{I},q_{0}=q^{\prime}_{I}$ and

[TABLE]

is consistent with $\sigma$. The latter is well defined since we have argued that no play consistent with $\sigma$ reaches $\bot$. Also, since we have assumed $\alpha$ can be extended to a word in the language of $\mathcal{N}$, $\top$ cannot be reached. For words which cannot be extended in this way, $\sigma^{\prime}$ behaves arbitrarily. Observe that if $\alpha\in\mathcal{L}_{\mathcal{N}}$, then $\alpha\in\mathcal{L}_{\mathcal{D}}$ and thus $p_{n}\in F$ since otherwise Adam could reach $\bot$ in the energy game when playing against $\sigma$, and this would contradict the fact that $\sigma$ is winning. Furthermore, we have that $\llbracket\mathcal{N}\rrbracket(\alpha)-\mathsf{Val}(\sigma^{\prime}(\alpha))\leq|V|\mu_{\max}$, since $\sigma$ is winning for eve in the energy game. Hence, Eve wins the $r$-regret game for $r=|V|\mu_{\max}$.

Suppose Eve does not win the game from some $(p_{I},q^{\prime}_{I})$ with initial credit $|V|\mu_{\max}$, then by Proposition 20, Adam wins the game for every $(p_{I},q^{\prime}_{I})$ regardless of the initial credit $c_{0}$. Suppose, for a contradiction, that Eve has a strategy $\sigma$ with which she wins the $r$-regret game for some $r\in\mathbb{N}$. Because of our reduction from $r$-regret games to EGRs, we obtain from Proposition 20 that $\sigma$ can be assumed to be a finite memory strategy. Let $m_{\sigma}$ be the amount of memory used by the machine realizing $\sigma$, i.e. the size of the machine. Let $\sigma(\varepsilon)=p_{0}$ and $\tau$ be the strategy for Adam in the energy game which is winning for him from $(p_{0},q^{\prime}_{I})$. The strategy $\sigma$ can be turned into a strategy for Eve in the energy game by ignoring the states of $\mathcal{D}$ and choosing transitions of $\mathcal{N}$ when Adam chooses a symbol. Hence, the play $\pi^{(p_{0},q^{\prime}_{0})}_{\sigma\tau}$ in the energy game must be losing for Eve, by choice of $\tau$. If the play is losing because vertex $\bot$ is reached, then either $\sigma$ does not reach a final state of $\mathcal{N}$ after reading a word in $\mathcal{L}_{\mathcal{N}}$ or she got stuck and cannot continue choosing transitions. In both cases, this contradicts the fact that $\sigma$ is winning for her in the regret game. Now, we will focus on the case where the play is losing because the energy level drops below [math]. Recall that this will be the case, regardless of the initial credit, by choice of $\tau$. Thus, let $c_{0}=|V|\mu_{\max}m_{\sigma}$ and let $\varphi=\dots(p_{n},q_{n})$ be the minimal prefix of $\pi^{(p_{0},q^{\prime}_{0})}_{\sigma\tau}$ such that $\mathsf{EL}_{c_{0}}(\varphi)<0$. Clearly $\varphi$ contains a negatively-weighted cycle $\chi$ which, furthermore, is a cycle on the machine realizing $\sigma$. Hence, Adam can “pump” $\chi$. A bit more precisely: after $\varphi$, Adam can repeat $r+|Q^{\prime}|(w_{\max}+w_{\max}^{\prime})$ times the cycle $\chi$ and then spell any word which will make $\mathcal{N}$ accept the word (recall $\mathcal{N}$ is trim, so this is always possible from every state) and make sure the regret of $\sigma$ is greater than $r$. The latter contradicts the fact that $\sigma$ is winning for Eve in the $r$-regret game. The result thus follows. ∎

Appendix J Proof of Theorem 8

Our proof is by reduction from countdown games. A countdown game $\mathcal{C}$ consists of a weighted graph $(S,T)$, where $S$ is the set of states and $T\subseteq S\times\mathbb{N}\setminus\{0\}\times S$ is the transition relation, and a target value $N\in\mathbb{N}$. If $t=(s,d,s^{\prime})\in T$ then we say that the duration of the transition $t$ is $d$. A configuration of a countdown game is a pair $(s,c)$, where $s\in S$ is a state and $c\in\mathbb{N}$. A move of a countdown game from a configuration $(s,c)$ consists in player Counter choosing a duration $d$ such that $(s,d,s^{\prime})\in T$ for some $s^{\prime}\in S$ followed by player Spoiler choosing $s^{\prime}$ such that $(s,d,s^{\prime})\in T$, the new configuration is then $(s^{\prime},c+d)$. Counter wins if the game reaches a configuration of the form $(s,N)$ and Spoiler wins if the game reaches a configuration $(s,c)$ such that $c<N$ and for all $t=(s,d,s^{\prime})\in T$ we have that $c+d>N$.

Deciding the winner in a countdown game $\mathcal{C}$ from a configuration $(s,0)$—where $N$ and all durations in $\mathcal{C}$ are given in binary—is \EXP-complete [JSL08].

Let us fix a countdown game $\mathcal{C}=((S,T),N)$ and let $n=\lfloor\log_{2}N\rfloor+2$.

Simplifying assumptions. Clearly, if Spoiler has a winning strategy and the game continues beyond his winning the game, then eventually a configuration $(s,c)$, such that $c\geq 2^{n}$, is reached. Thus, we can assume w.l.o.g. that plays in $\mathcal{C}$ which visit a configuration $(s,N)$ are winning for Counter and plays which don’t visit a configuration $(s,N)$ but eventually get to a configuration $(s^{\prime},c)$ such that $c\geq 2^{n}$ are winning for Spoiler.

Additionally, we can also assume that $T$ in $\mathcal{C}$ is total. That is to say, for all $s\in S$ there is some duration $d$ such that $(s,d,s^{\prime})\in T$ for some $s^{\prime}\in S$. If this were not the case then for every $s$ with no outgoing transitions we could add a transition $(s,N+1,s_{\bot})$ where $s_{\bot}$ is a newly added state. It is easy to see that either player has a winning strategy in this new game if and only if he has a winning strategy in the original game.

Reduction. We will now construct a sum-automaton $\mathcal{N}$ with $w_{\max}=2$ such that, in a regret game played on $\mathcal{N}$, Eve can ensure regret value strictly less than $2$ if and only if Counter has a winning strategy in $\mathcal{C}$. It will be clear from the proof how to generalize the argument to any (strict or non-strict) regret threshold.

The alphabet of the automaton $\mathcal{N}=(Q,\{q_{I}\},A,\Delta,w,F)$ is $A=\{b_{i}\>\mid\>0\leq i\leq n\}\cup\{c_{i}\>\mid\>0<i\leq n\}\cup\{bail,choose\}\cup S$. We assume all states are final, i.e. $Q=F$. We now describe the structure of $\mathcal{N}$ (i.e. $Q$, $\Delta$ and $w$).

Initial gadget. Fig. 7 depicts the initial state of the automaton. Here, Eve has the choice of playing left or right. If she plays to the left then Adam can play $bail$ and force her to $\bot_{0}$ while the alternative run resulting from her having chosen to go right goes to $\bot_{2}$. Hence, playing left already gives Adam a winning strategy to ensure regret $2$, so she plays to the right. If Adam now plays $bail$ then Eve can go to $\bot_{2}$ and as $W=2$ this implies the regret will be [math]. Therefore, Adam plays [math].

Counter gadget. Fig. 8 shows the left sub-automaton. All states from $\{\overline{x_{i}}\>\mid\>0\leq i\leq n\}$ have incoming transitions from the left part of the initial gadget with symbol $A\setminus\{bail\}$ and weight [math]. Let $y_{0}\dots y_{n}\in\mathbb{B}$ be the (little-endian) binary representation of $N$, then for all $x_{i}$ such that $y_{i}=1$ there is a transition from $x_{i}$ to $\bot_{0}$ with weight [math] and symbol $bail$. Similarly, for all $\overline{x_{i}}$ such that $y_{i}=0$ there is a transition from $\overline{x_{i}}$ to $\bot_{0}$ with weight [math] and symbol $bail$. All the remaining transitions not shown in the figure cycle on the same state, e.g. $x_{i}$ goes to $x_{i}$ with symbol $choose$ and weight [math].

The sub-automaton we have just described corresponds to a counter gadget (little-endian encoding) which keeps track of the sum of the durations “spelled” by Adam. At any point in time, the states of this sub-automaton in which Eve believes alternative runs are now will represent the binary encoding of the current sum of durations. Indeed, the initial gadget makes sure Eve plays into the right sub-automaton and therefore she knows there are alternative runs that could be at any of the $\overline{x_{i}}$ states. This corresponds to the [math] value of the initial configuration.

Adder gadget. Let us now focus on the right sub-automaton in which Eve finds herself at the moment. The right transition with symbol $A\setminus\{bail\}$ from the initial gadget goes to state $s$—the initial state from $\mathcal{C}$. It is easy to see how we can simulate Counter’s choice of duration and Spoiler’s choice of successor. From $s$ there are transitions to every $(s,c)$, such that $(s,c,s^{\prime})\in T$ for some $s^{\prime}\in S$ in $\mathcal{C}$, with symbol $choose$ and weight [math]. Transitions with all other symbols and weight $1$ going to $\bot_{1}$—a trapping state with a [math]-weight cycle with every symbol—from $s$ ensure Adam plays $choose$, else since $w_{\max}=2$ the regret of the game will be at most $1$ and Eve wins.

Fig. 9 shows how Eve forces Adam to “spell” the duration $c$ of a transition of $\mathcal{C}$ from $(s,c)$. For concreteness, assume that Eve has chosen duration $9$. The top source in Fig. 9 is therefore the state $(s,9)$. Again, transitions with all the symbols not depicted go to $\bot_{1}$ with weight $1$. Hence, Adam will play $b_{0}$ and Eve has the choice of going straight down or moving to a state where Adam is forced to play $c_{1}$. Recall from the description of the counter gadget that the belief of Eve encodes the binary representation of the current sum of delays. If she believes a play is in $x_{1}$ (and therefore none in $\overline{x_{1}}$) then after Adam plays $b_{0}$ it is important for her to make him play $c_{1}$ or this alternative run will end up in $\bot_{2}$. It will be clear from the construction that Adam always has a strategy to keep the play in the right sub-automaton without reaching $\bot_{1}$ and therefore if any alternative run from the left sub-automaton is able to reach $\bot_{2}$ then Adam wins (i.e. can ensure regret $2$). Thus, Eve decides to force Adam to play $c_{1}$. As the duration was $9$ this gadget now forces Adam to play $b_{4}$ and again presents the choice of forcing Adam to play $c_{5}$ to Eve. Clearly this can be generalized for any duration. This gadget in fact simulates a cascade configuration of $n$ $1$-bit adders.

Finally, from the bottom trap in the adder gadget, we have transitions with symbols from $S$ with weight [math] to the corresponding states (thus simulating Spoiler’s choice of successor state). Additionally, with any symbol from $S$ and with weight [math] Eve can also choose to go to a state $q_{bail}$ where Adam is forced to play $bail$ and Eve is forced into $\bot_{0}$.

Proof.

Note that if the simulation of the counter has been faithful and the belief of Eve encodes the value $N$ then by playing $bail$, Adam forces all of the alternative runs in the left sub-automaton into the $\bot_{0}$ trap. Hence, if Counter has a winning strategy and Eve faithfully simulates the $\mathcal{C}$ she can force this outcome of all plays going to $\bot_{0}$. Note that from the right sub-automaton we have that $\bot_{2}$ is not reachable and therefore the highest value assigned to any word is $1$. Therefore, her regret is of at most $1$.

Conversely, if both players faithfully simulate $\mathcal{C}$ and the configuration $N$ is never reached, i.e. Spoiler had a winning strategy in $\mathcal{C}$, then eventually some alternative run in the left sub-automaton will reach $x_{n}$ and from there it will go to $\bot_{2}$. Again, the construction makes sure that Adam always has a strategy to keep the play in the right sub-automaton from reaching $\bot_{1}$ and therefore this outcome yields a regret of $2$ for Eve. ∎