# Token Games and History-Deterministic Quantitative-Automata

Udi Boker, Karoliina Lehtinen

► To cite this version:

Udi Boker, Karoliina Lehtinen. Token Games and History-Deterministic Quantitative-Automata. Logical Methods in Computer Science, 2023, Logical Methods in Computer Science, Volume19,Issue4, 10.46298/lmcs-19(4:8)2023 . hal-04271341

HAL Id: hal-04271341

https://hal.science/hal-04271341v1

Submitted on 6 Nov 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# TOKEN GAMES AND HISTORY-DETERMINISTIC QUANTITATIVE AUTOMATA

UDI BOKER ◦ª AND KAROLIINA LEHTINEN ◦ᵇ

ª Reichman University, Herzliya, Israel

ᵇ CNRS, Marseille-Aix Université, LIS, Marseille, France

**ABSTRACT.** A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the HDness problem) is generally a difficult task, which can involve an exponential procedure, or even be undecidable, as is the case for example with pushdown automata. Token games provide a PTIME solution to the HDness problem of Büchi and coBüchi automata, and it is conjectured that 2-token games characterise HDness for all ω-regular automata.

We extend token games to the quantitative setting and analyse their potential to help deciding HDness of quantitative automata. In particular, we show that 1-token games characterise HDness for all quantitative (and Boolean) automata on finite words, as well as discounted-sum (DSum), Inf and Reachability automata on infinite words, and that 2-token games characterise HDness of LimInf and LimSup automata, as well as Sup automata on infinite words. Using these characterisations, we provide solutions to the HDness problem of Safety, Reachability, Inf and Sup automata on finite and infinite words in NΠCO-NP, of LimSup automata in quasip polynomial time, and of LimInf automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.

## 1. INTRODUCTION

**History-determinism.** A nondeterministic (quantitative) automaton is called history-deterministic (HD) [Col09, BL21] if its nondeterministic choices can be resolved by only considering the word read so far, uniformly across possible suffixes (see Fig. 5 for examples of HD and non-HD automata). More precisely, there should be a function (strategy), sometimes called a resolver, that maps the finite prefixes of a word to the transition to be taken at the last letter. The run built in this way must, in the Boolean setting, be accepting whenever

*Key words and phrases:* Quantitative Automata, History-determinism, Token games.

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

<figure><img src="image_2.png" /></figure>

<footnote>* The present article extends [BL22] with additional results on Inf, Sup and Reachability automata on infinite words as well as some additional discussion throughout.</footnote>
the word is in the language of the automaton and, in the more general quantitative setting, attain the value of the automaton on the word (i.e., the supremum of all its runs' values).

History-determinism lies in between determinism and nondeterminism, enjoying in some aspects the best of both worlds: HD automata are, like deterministic ones, useful for solving games and reactive synthesis [HP06, Col09, HPR16, HPR17, CF19, GJLZ21, BL21], yet can sometimes be more expressive and/or succinct. For example, HD coBüchi and LimInf automata can be exponentially more succinct than deterministic ones [KS15], and HD pushdown automata are both more expressive and at least exponentially more succinct than deterministic ones [LZ22, GJLZ21]. In the (ω-)regular setting, history-determinism coincides with good-for-gameness [BL19], a notion characterised by the compositional properties of the automaton [HP06], while in the quantitative setting it is stronger [BL21]. The problem of deciding whether a nondeterministic automaton is HD is interreducible with deciding the best-value synthesis problem of a deterministic automaton of the same type [FLW20, BL21]. In this quantitative version of the reactive synthesis problem, the system must guarantee a behaviour that matches the value of any global behaviour compatible with the environment's actions. The witness of HDness corresponds exactly to the solution system of this synthesis problem, providing another motivation for this line of research.

**Deciding history-determinism – a difficult task.** History-determinism is formally defined by a letter game played on the automaton $\mathcal{A}$ between Adam and Eve, where Adam produces an input word $w$, letter by letter, and Eve tries to resolve the nondeterminism in $\mathcal{A}$ so that the resulting run attains $\mathcal{A}$'s value on $w$. Then $\mathcal{A}$ is HD if Eve has a winning strategy in the letter game on it. The difficulty of deciding who wins the letter game stems from its complicated winning condition – Eve wins if her run has the value of the supremum over all runs of $\mathcal{A}$ on $w$.

The naive solution is to determinise $\mathcal{A}$ into an automaton $\mathcal{D}$, and consider a game equivalent to the letter game that has a simpler winning condition and whose arena is the product of $\mathcal{A}$ and $\mathcal{D}$ [HP06]. The downside with this approach, however, is that it requires the determinisation of $\mathcal{A}$, which often involves a procedure exponential in the size of $\mathcal{A}$ and sometimes is even impossible due to an expressiveness gap. Note that deciding whether an automaton is good-for-games, which is closely related to whether it is HD [BL19, BL21], is also difficult, as it requires reasoning about composition with all possible games.

**Token games – a possible aid.** The one-token-game, which is closely related to the letter game but easier to solve, was introduced by Löding in an algorithm for deciding determinisability-by-pruning of a regular automaton, and was formally defined in [LR13, Definition 5]. It was later generalised by Bagnol and Kuperberg [BK18] to a k-token-game on $\omega$-regular automata, for a given $k \in \mathbb{N}$, in the course of seeking an easier to decide characterisation of history-determinism.

In a k-token game on an automaton $\mathcal{A}$, denoted by $G_k(\mathcal{A})$, like in the letter game, Adam generates a word $w$ letter by letter, and Eve builds a run on $w$ by resolving the nondeterminism. In addition, Adam also has to resolve the nondeterminism of $\mathcal{A}$ to build $k$ runs letter-by-letter over $w$. The winning condition for Eve in these games on Boolean automata is that either all runs built by Adam are rejecting, or Eve's run is accepting. Such games, as they compare a finite number of pairs of runs, are easier to solve than the letter game.
Then, to decide HDness of a class of automata, one can attempt to show that the letter game always has the same winner as a *k*-token game, for some *k*, and solve the *k*-token game. (If Eve wins the letter game then she wins the *k*-token game, for every *k*, by using the same strategy, ignoring Adam's runs. However, it might be that she wins a *k*-token game, taking advantage of her knowledge of how Adam resolves the nondeterminism, but loses the letter game.)

Bagnol and Kuperberg showed in [BK18] that on Büchi automata, the letter game and the 2-token game always have the same winner, and in [BKLS20], Boker, Kuperberg, Lehtinen and Skrzypczak extended this result to coBüchi automata. In both cases, this allows for a PTIME procedure for deciding HDness. Furthermore, Bagnol and Kuperberg suggested in [BK18, Conclusion] that 2-token games might characterise HDness also for parity automata (and therefore for all $\omega$-regular automata); a conjecture (termed later the G2 conjecture) that is still open.

**Our contribution.** We extend token games to the quantitative setting, and use them to decide the HDness of some quantitative automata. We define a *k*-token game on a quantitative automaton exactly as on a Boolean one, except that Eve wins if her run has a value at least as high as all of Adam's runs.

We show first, in Section 4, that the 1-token game, in which Adam just has one run to build, characterises HDness for all quantitative (and Boolean) automata on finite words, and for Safety, Reachability, Inf and discounted-sum (DSum) automata on infinite words. This results in a PTIME decision procedure for checking HDness of Safety, Reachability, and Inf automata, and an NP$\cap$CONP procedure for DSum automata, both on finite and infinite words. Note that the complexity for DSum automata on finite words was already known [FLW20], but on infinite words it was erroneously believed to be NP-hard [HPR16, Theorem 6].

Towards getting the above results, we analyse key properties of value functions of quantitative automata, and show that the 1-token game characterises HDness for every Val automaton, such that Val is present-focused (Definition 2.3), which is in particular the case for all Val automata on finite words [BL21, Lemma 16], as well as DSum [BL21, Lemma 22] and Inf automata on infinite words.

We then show, in Section 5, that the 2-token game, in which Adam builds two runs, characterises HDness for both LimSup and LimInf automata. The approach here is more involved: it decomposes the quantitative automaton into a collection of Büchi or coBüchi automata such that if Eve wins the 2-token game on the original automaton, she also wins in the component automata. Since the 2-token game characterises HD for Büchi and coBüchi automata, the component automata are then HD and the witness strategies can be combined with the 2-token strategy of the original automaton to build a letter-game strategy for Eve.

The general flow of our approach is illustrated in Fig. 4. As a corollary, we obtain that $G_2$ also characterises HDness for Sup automata on infinite words.

We further present, in Section 5.2, algorithms to decide the winner of the 2-token games on LimInf and LimSup automata via reductions to solving parity games, and on Sup automata on infinite words via reduction to coBüchi games. The complexity of the procedure for a LimSup automaton $\mathcal{A}$ is the same as that of solving a parity game of size polynomial in the size of $\mathcal{A}$ with twice as many priorities as there are weights in $\mathcal{A}$, which is in quasip polynomial time. For LimInf automata the procedure is in exponential time. In both cases, it is in
polynomial time if the number of weights is logarithmic in the automaton size. For Sup automata, the procedure is always polynomial. These results are summarised in Table 1.

For some variants of the synthesis problem, the complexity of the witness of history-determinism is also of interest (for other variants it is not), as it corresponds to the complexity of the implementation of the solution system [BL21, Section 5]. We give an exponential upper bound to the complexity of the witness for LimSup, LimInf and Sup automata, which, for LimInf, is tight. As a corollary, we obtain that HD LimSup automata are exactly as expressive as deterministic LimSup automata and at most exponentially more succinct.

**Related work.** In the $\omega$-regular setting (where HDness coincides with good-for-gameness), [HP06, Section 4] provides an exponential scheme for checking HDness of all $\omega$-regular automata, based on determinisation and checking fair simulation. HDness of Büchi automata is resolved, as mentioned above, in PTIME, using 2-token games [BK18]. The coBüchi case is also resolved in PTIME, originally via an indirect usage of “joker games” [KS15], and later by using 2-token games [BKLS20].

In the quantitative setting, deciding HDness coincides with best-value partial domain synthesis [FLW20], 0-regret synthesis [HPR17] and, for some value functions, 0-regret determinisation [FJL$^+$17, BL21]. There are procedures to decide HDness (which is sometimes called good-for-gameness due to erroneously assuming them equivalent) of Sum, Avg, and DSum automata on finite words, as follows. For Sum and Avg automata on finite words, a PTIME solution combines [AKL10, Theorem 4.1], which provides a PTIME algorithm for checking whether such an automaton is “determinisable by pruning”, and [BL21, Theorem 21], which shows that such an automaton is HD if and only if it is determinisable by pruning.

**Proposition 1.1.** Deciding whether a Sum or Avg automaton on finite words is history-deterministic is in PTIME.

For DSum automata on finite words, [FLW20, Theorem 23] provides an NP$\cap$CO-NP solution, using a game that is quite similar to the 1-token game, differing from it in a few aspects – for example, Adam is asked to either copy Eve with his token or move into a second phase where he plays transitions first – and uses a characterisation of HD strategies resembling our notion of cautious strategies (Definition 2.2) specialised to DSum automata.

## 2. PRELIMINARIES

**Words.** An alphabet $\Sigma$ is a finite nonempty set of letters. A finite (resp. infinite) word $u = \sigma_0 \dots \sigma_k \in \Sigma^*$ (resp. $w = \sigma_0 \sigma_1 \dots \in \Sigma^\omega$) is a finite (resp. infinite) sequence of letters from $\Sigma$; $\varepsilon$ is the empty word. We write $\Sigma^\infty$ for $\Sigma^* \cup \Sigma^\omega$. We use $[i..j]$ to denote a set $\{i, \dots, j\}$ of integers, $[i]$ for $[i..i]$, $[..j]$ for $[0..j]$, and $[i..]$ for integers equal to or larger than $i$. We write $w[i..j]$, $w[..j]$, and $w[i..]$ for the infix $\sigma_i \dots \sigma_j$, prefix $\sigma_0 \dots \sigma_j$, and suffix $\sigma_i \dots$ of $w$. A language is a set of words.
<table><caption>Table 1: Characterisation of history-determinism by 1- and 2-token games (the characterisation of the specific automata types refers to automata on infinite words), and the complexity of checking whether an automaton is history-deterministic.</caption><thead><tr><th rowspan="2">Automata Type</th><th colspan="2">HD is characterised by</th><th colspan="2">HDness Complexity</th></tr><tr><th>G<sub>1</sub></th><th>G<sub>2</sub></th><th>Finite words</th><th>Infinite words</th></tr></thead><tbody><tr><td>All automata on<br>finite words</td><td colspan="2">✓<br>Corrolary 4.2</td><td colspan="2">Varies</td></tr><tr><td>All automata on<br>infinite words</td><td><b>Not all</b><br>[BK18, Lemma 8]</td><td><b>Open</b><br>[BK18]</td><td colspan="2">Varies</td></tr><tr><td>Safety</td><td>✓<br>Theorem 4.5</td><td></td><td colspan="2">PTIME<br>Theorem 4.10 &nbsp; Theorem 4.11</td></tr><tr><td>Reachability</td><td>✓<br>Theorem 4.8</td><td></td><td colspan="2">PTIME<br>Theorem 4.10 &nbsp; Theorem 4.11</td></tr><tr><td>Inf</td><td>✓<br>Theorem 4.5</td><td></td><td colspan="2">PTIME<br>Theorem 4.13</td></tr><tr><td>Sup</td><td><b>X</b><br>Proposition 4.9</td><td>✓<br>Corrolary 5.7</td><td colspan="2">PTIME<br>Theorem 4.12 &nbsp; Theorem 5.9</td></tr><tr><td>DSum</td><td colspan="2">✓<br>Corrolary 4.3</td><td colspan="2">NP∩CO-NP<br>Theorem 4.14</td></tr><tr><td>LimInf</td><td><b>X</b><br>[BK18, Lemma 8]</td><td>✓<br>Theorem 5.6</td><td>-</td><td>Quasipoly.<br>Theorem 5.11</td></tr><tr><td>LimSup</td><td><b>X</b><br>[BK18, Lemma 8]</td><td>✓<br>Theorem 5.6</td><td>-</td><td>Quasipoly.<br>Theorem 5.10</td></tr></tbody></table>

**Games.** We consider a variety of turn-based zero-sum games between Adam (A) and Eve (E). Formally, a game is played on an arena of which the positions are partitioned between the two players. A play is a maximal (finite or infinite) path. The winning condition partitions plays into those that are winning for each player. In some of the technical developments we use *parity games*, in which moves are coloured with integer priorities and a play is winning for Eve if the maximal priority that occurs infinitely often along the play is even. A coBüchi game is the special case of a parity game with priorities 1 and 0. A weak game is the special case of a coBüchi game in which priorities 0 and 1 do not both occur within a single cycle.

A strategy for a player $P \in \{A, E\}$ maps partial plays ending in a position belonging to $P$ to a successor position. A (partial) play $\pi$ agrees with a strategy $s_P$ of $P$, written $\pi \in s_P$, if whenever its prefix $p$ ends in a position of $P$, the next move is $s_P(p)$. A strategy of $P$ is winning from a position $v$ if all plays starting at $v$ that agree with it are winning for $P$. A strategy is positional if it maps all plays that end in the same position to the same successor.

**Quantitative Automata.** A *nondeterministic quantitative*<fnref n="1" /> *automaton* (or just automaton from here on) on words is a tuple $\mathcal{A} = (\Sigma, Q, \iota, \delta)$, where $\Sigma$ is an alphabet; $Q$ is a finite

<footnote n="1">¹We speak of “quantitative” rather than “weighted” automata, following the distinction made in [Bok21] between the two.</footnote>
nonempty set of states; $\iota \in Q$ is an initial state; and $\delta: Q \times \Sigma \to 2(Q \times Q)$ is a transition function over weight-state pairs.

A transition is a tuple $(q, \sigma, x, q') \in Q \times \Sigma \times Q \times Q$, also written $q \xrightarrow{\sigma:x} q'$. (There might be several transitions with different weights over the same letter between the same states.) We write $\gamma(t) = x$ for the weight of a transition $t = (q, \sigma, x, q')$. $\mathcal{A}$ is deterministic if for all $q \in Q$ and $a \in \Sigma$, $\delta(q, a)$ is a singleton. We require that the automaton $\mathcal{A}$ is total, namely that for every state $q \in Q$ and letter $\sigma \in \Sigma$, there is at least one state $q'$ and a transition $q \xrightarrow{\sigma:x} q'$.

A run of $\mathcal{A}$ on a word $w$ is a sequence $\rho = q_0 \xrightarrow{w[0]:x_0} q_1 \xrightarrow{w[1]:x_1} q_2 \dots$ of transitions where $q_0 = \iota$ and $(x_i, q_{i+1}) \in \delta(q_i, w[i])$. As each transition $t_i$ carries a weight $\gamma(t_i) \in \mathbb{Q}$, the sequence $\rho$ provides a weight sequence $\gamma(\rho) = \gamma(t_0)\gamma(t_1)\dots$ A Val (e.g., Sum) automaton is one equipped with a *value function* Val: $\mathbb{Q}^* \to \mathbb{R}$ or Val: $\mathbb{Q}^\omega \to \mathbb{R}$, which assigns real values to runs of $\mathcal{A}$. The value of a run $\rho$ is Val($\gamma(\rho)$). The value of $\mathcal{A}$ on a word $w$ is the supremum of Val($\rho$) over all runs $\rho$ of $\mathcal{A}$ on $w$. Two automata $\mathcal{A}$ and $\mathcal{A}'$ are *equivalent*, if they realise the same function from words to reals. The size of an automaton consists of the maximum among the size of its alphabet, state-space, and transition-space.

**Value functions.** We list below the value functions that we will consider in the sequel.

For finite sequences $v_0v_1\dots v_{n-1}$ of rational weights:

$$ \bullet \text{ Sum}(v) = \sum_{i=0}^{n-1} v_i $$

$$ \bullet \text{ Avg}(v) = \frac{1}{n} \sum_{i=0}^{n-1} v_i $$

For finite and infinite sequences $v_0v_1\dots$ of rational weights:

$$ \bullet \text{ Inf}(v) = \inf\{v_n \mid n \ge 0\} $$

$$ \bullet \text{ Sup}(v) = \sup\{v_n \mid n \ge 0\} $$

$$ \bullet \text{ For a discount factor } \lambda \in \mathbb{Q} \cap (0, 1), \text{ } \lambda\text{-DSum}(v) = \sum_{i \ge 0} \lambda^i v_i $$

For infinite sequences $v_0v_1\dots$ of rational weights:

$$ \bullet \text{ LimInf}(v) = \lim_{n \to \infty} \inf\{v_i \mid i \ge n\} $$

$$ \bullet \text{ LimSup}(v) = \lim_{n \to \infty} \sup\{v_i \mid i \ge n\} $$

*Regular and $\omega$-regular automata* (with acceptance on transitions) can be viewed as special cases of quantitative automata with weights in $\{0,1\}$, where the language of the automaton consists of words with value 1. In particular, considering only weights in $\{0,1\}$, Büchi coincides with **LimSup**, coBüchi with **LimInf**, Reachability with **Sup** and **Safety** with **Inf**. With this in mind, **Reachability** and **Safety** automata on finite and infinite words, are defined as $\mathcal{A} = (\Sigma, Q, \iota, \delta)$ as above, with weights 0 and 1 on transitions, and we assume that for **Reachability** automata every accepting transition, that is a transition with weight 1, leads to a sink with self-loops of weight 1, called the target (we use this assumption in Section 4.1), and for **Safety** automata, every rejecting transition, that is a transition with weight 0, leads to a sink with self-loops of weight 0. We call the rest of the automaton its safe region. We say that the automaton accepts a word if its value is 1: A **Reachability** automaton accepts words with runs that reach the target, while a **Safety** automaton accepts words with runs that remain in the safe region. See more on $\omega$-regular automata, e.g., in [Bok18].
**History-determinism.** Intuitively, an automaton is history-deterministic if there is a strategy to resolve its nondeterminism according to the word read so far such that for every word, the value of the resulting run is the value of the word.

**Definition 2.1** (History-determinism [Col09, BL21]). A Val automaton $\mathcal{A}$ is history-deterministic (HD) if Eve wins the following win-lose letter game, in which Adam chooses the next letter and Eve resolves the nondeterminism, aiming to construct a run whose value is equivalent to the generated word's value.

**Letter game:** A play begins in $q_0 = \iota$ (the initial state of $\mathcal{A}$) and at the $i^{th}$ turn, from state $q_i$, it progresses to a next state $q_{i+1}$ as follows:

* Adam picks a letter $\sigma_i$ from $\Sigma$ and then

* Eve chooses a transition $t_i = q_i \xrightarrow{\sigma_i:x_i} q_{i+1}$.

In the limit, a play consists of an infinite word $w$ that is derived from the concatenation of $\sigma_0, \sigma_1, \dots$, as well as an infinite sequence $\pi = t_0, t_1, \dots$ of transitions. For $\mathcal{A}$ on infinite words, Eve wins a play in the letter-game if $Val(\pi) \ge \mathcal{A}(w)$. For $\mathcal{A}$ on finite words, Eve wins if for all $i \in \mathbb{N}$, $Val(\pi[0..i]) \ge \mathcal{A}(w[0..i])$.

Consider for example the LimSup automaton $\mathcal{A}$ in Fig. 5. Eve loses the letter game on $\mathcal{A}$: Adam can start with the letter $a$; then if Eve goes from $s_0$ to $s_1$, Adam continues to choose $a$ forever, generating the word $a^\omega$, where $\mathcal{A}(a^\omega) = 3$, while Eve's run has the value 2. If, on the other hand, Eve chooses on her first move to go from $s_0$ to $s_2$, Adam continues with choosing $b$ forever, generating the word $ab^\omega$, where $\mathcal{A}(ab^\omega) = 2$, while Eve's run has the value 1.

**Families of value functions.** We will provide some of our results with respect to a family of Val automata based on properties of the value function Val.

We first define *cautious strategies* for Eve in both the letter game and token games (Section 3), which we use to define *present-focused* value functions. Intuitively, a strategy is cautious if it avoids mistakes: it only builds run prefixes that can achieve the maximal value of any continuation of the current word prefix.

**Definition 2.2** (Cautious strategies [BL21]). Consider the letter game on a Val automaton $\mathcal{A}$, in which Eve builds a run of $\mathcal{A}$ transition by transition. A move (transition) $t = q \xrightarrow{\sigma:x} q'$ of Eve, played after some run $\rho$ ending in a state $q$, is *non-cautious* if for some word $w$, there is a run $\pi'$ from $q$ over $\sigma w$ such that $Val(\rho\pi')$ is strictly greater than the value of $Val(\rho\pi)$ for any $\pi$ starting with $t$. A strategy is *cautious* if it makes no non-cautious moves.

A winning strategy for Eve in the letter game must of course be cautious; Whether all cautious strategies are winning depends on the value function. For example, a cautious strategy in a Safety automaton is obviously winning, as it inevitably remains in the safe region while Adam plays prefixes of words in the language, while a cautious strategy in a Reachability automaton might not be winning as cautiousness does not require Eve to ever reach the target with her run. We call a value function present-focused if, morally, it depends on the prefixes of the value sequence, formalised by winning the letter game via cautious strategies.

**Definition 2.3** (Present-focused value functions [BL21]). A value function Val, on finite or infinite sequences, is present-focused if for all automata $\mathcal{A}$ with value function Val, every cautious strategy for Eve in the letter game on $\mathcal{A}$ is also a winning strategy in that game.
Value functions on finite sequences are present-focused, as they can only depend on prefixes, while value functions on infinite sequences are not necessarily present-focused [BL21, Remark 17], for example LimInf and LimSup.

**Proposition 2.4** [BL21, Lemma 16]. Every value function Val on finite sequences of rational values is present focused.

**Proposition 2.5** [BL21, Lemma 22]. For every $\lambda \in \mathbb{Q} \cap (0, 1)$, $\lambda$-DSum on infinite sequences of rational values is a present-focused value function.

### 3. TOKEN GAMES

The one-token-game was introduced by Löding and was then formally defined in [LR13, Definition 5]. It was later generalised by Bagnol and Kuperberg [BK18] to a k-token-game, for a given $k \in \mathbb{N}$, in the scope of resolving the HDness problem of Büchi automata.

In the *k*-token game, known as $G_k$, the players proceed as in the letter game, except that now Adam has *k* tokens that he must move after Eve has made her move, thus building *k* runs. For Adam to win, at least one of these must be better than Eve's run. In the Boolean setting, this run must be accepting, thus witnessing that the word is in the language of the automaton. Intuitively, the more tokens Adam has, the less information he is giving Eve about the future of the word he is building.

We generalise token games to the quantitative setting, defining that the maximal value produced by Adam's runs witnesses a lower bound on the value of the word, and Eve's task is to match or surpass this value on her run.

In the Boolean setting, $G_2$ has the same winner as the letter game for Büchi [BK18, Corollary 21] and coBüchi [BKLS20, Theorem 28] automata (the case of parity and more powerful automata is open). Since $G_2$ is solvable in polynomial time for Büchi and coBüchi acceptance conditions, this gives a PTIME algorithm for deciding HDness, which avoids the determinisation used to solve the letter game directly. In the following sections we study how different token games can be used to decide HDness for different quantitative automata.

**Definition 3.1** (*k*-token games). Consider a Val automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$. A configuration of the game $G_k(\mathcal{A})$ for $k \ge 1$ is a tuple $(q, p_1, \dots, p_k) \in Q^{k+1}$ of states, and the initial configuration is $\iota^{k+1}$. In a configuration $(q_i, p_{1,i}, \dots, p_{k,i})$, the game proceeds to the next configuration $(q_{i+1}, p_{1,i+1}, \dots, p_{k,i+1})$ as follows.

* Adam picks a letter $\sigma_i$ from $\Sigma$,

* Eve picks a transition $q_i \xrightarrow{\sigma_i:x_{0,i}} q_{i+1}$, and

* Adam picks transitions, $p_{1,i} \xrightarrow{\sigma_i:x_{1,i}} p_{1,i+1}, \dots, p_{k,i} \xrightarrow{\sigma_i:x_{k,i}} p_{k,i+1}$.

In the limit, a play consists of an infinite word $w$ that is derived from the concatenation of $\sigma_0, \sigma_1, \dots$, as well as $k+1$ infinite sequences $\pi, \pi_1, \pi_2, \dots, \pi_k$ of transitions over $w$, where $\pi$ is picked by Eve and $\pi_1, \dots, \pi_k$ by Adam. Eve wins the play if $\text{Val}(\pi) \ge \max(\text{Val}(\pi_1), \dots, \text{Val}(\pi_k))$.

On finite words, $G_k$ is defined as above, except that the winning condition is a safety condition for Eve: for all finite prefixes of a play, it must be the case that the value of Eve's run is at least the value of each of Adam's runs.

Cautious strategies (Definition 2.2) immediately extend to Eve's strategies in $G_k(\mathcal{A})$. Unlike in the letter game, a winning strategy in $G_k(\mathcal{A})$ must not necessarily be cautious: a
non-cautious move does not necessarily allow Adam to win, since Adam might not have a token available to build an optimal run on the word witnessing Eve's lack of caution.

## 4. DECIDING HISTORY-DETERMINISM VIA ONE-TOKEN GAMES

Bagnol and Kuperberg showed that the one-token game $G_1$ does not suffice to characterise HDness for Büchi automata [BK18, Lemma 8]. However, it turns out that $G_1$ does characterise HDness for all quantitative (and Boolean) automata on finite words and some quantitative automata on infinite words.

We can then use $G_1$ to decide history-determinism of some of these automata, over which the $G_1$ game is simple to decide. In particular, this is the case for Sup automata on finite words and Reachability, Safety, Inf and DSum automata on finite and infinite words.

### 4.1. $G_1$ Characterises HDness for some automata.

**Theorem 4.1.** Given a nondeterministic automaton $\mathcal{A}$ with a present-focused value function Val on finite or infinite words, Eve wins $G_1(\mathcal{A})$ if and only if $\mathcal{A}$ is HD. Furthermore, a winning strategy for Eve in $G_1(\mathcal{A})$ induces an HD strategy with the same memory.

*Proof.* One direction is easy: if $\mathcal{A}$ is HD, Eve can use her HD strategy to win $G_1$ by ignoring Adam's token. For the other direction, assume that Eve wins $G_1$.

We consider the following family of copycat strategies for Adam in $G_1$: a copycat strategy is one where Adam moves his token in the same way as Eve until she makes a non-cautious move $t = q \xrightarrow{\sigma:x} q'$ after building a run $\rho$; that is, there is some word $w$ and run $\pi'$ from $q$ on $\sigma w$, such that for every run $\pi$ on $\sigma w$ starting with $t$, we have $\text{Val}(\rho\pi') > \text{Val}(\rho\pi)$. Then the copycat strategy stops copying and directs Adam's token along the run $\pi'$ and plays the word $w$. If Eve plays a non-cautious move in $G_1$ against a copycat strategy, she loses. Then, if Eve wins $G_1$ with a strategy $s$, she wins in particular against all copycat strategies and therefore $s$ never makes a non-cautious move against such a strategy.

Eve can then play in the letter game over $\mathcal{A}$ with a strategy $s'$ that moves her token as $s$ would in $G_1(\mathcal{A})$ assuming Adam uses a copycat strategy. Then, $s'$ never makes a non-cautious move and is therefore a cautious strategy. Since Val is present-focused, any cautious strategy, and in particular $s'$, is winning in the letter game, so $\mathcal{A}$ is HD. Note that $s'$ requires no more memory than $s$. $\square$

Notice that the converse of the above does not hold, namely there are value functions Val that are not present-focused, while $G_1$ still characterises HD for all Val-automata, as will be shown for Reachability automata.

An immediate corollary of Theorem 4.1 is that $G_1$ characterises history-determinism for all automata on finite words, as all value functions on finite words are present focused.

**Corollary 4.2.** Given a nondeterministic automaton $\mathcal{A}$ on finite words, Eve wins $G_1(\mathcal{A})$ if and only if $\mathcal{A}$ is HD, and winning strategies in $G_1(\mathcal{A})$ induce HD strategies for $\mathcal{A}$ of the same memory size.

*Proof.* A direct consequence of Proposition 2.4 and Theorem 4.1. $\square$

**Corollary 4.3.** Given a nondeterministic DSum automaton $\mathcal{A}$ on finite or infinite words, Eve wins $G_1(\mathcal{A})$ if and only if $\mathcal{A}$ is HD, and winning strategies in $G_1(\mathcal{A})$ induce HD strategies for $\mathcal{A}$ of the same memory size.
*Proof.* A direct consequence of Propositions 2.4 and 2.5 and Theorem 4.1. □

Considering the memory size of the HD strategy, notice that for DSum automata on finite and infinite words, positional strategies suffice; that is these automata are HD if and only if they are determinisable by pruning [BL21, Theorem 23] and [HPR16, Section 5].

**Lemma 4.4.** *The value function Inf on infinite sequences of rational values is present-focused.*

*Proof.* Consider a cautious strategy *s* of Eve in the letter game on an Inf automaton *A*, and assume toward contradiction that there exists a play in which Adam wins playing against *s*.

Let *w* be the word generated along this play. Then, the run of *A* on *w* that Eve generated along the play has some value *x* < *A*(*w*). Let *u* be the shortest prefix of *w*, after which Eve chose a transition *t* = *q* $\xrightarrow{\sigma:x}$ *q'* with value *x*, and let *ρ* be the corresponding prefix of the run generated by Eve. Clearly, every continuation of *ρ* on the suffix of *w* from *u* will generate a run whose value is at most *x*, thus strictly smaller than *A*(*w*).

Let $\rho'$ be the longest prefix of $\rho$, for which there is a continuation on the corresponding suffix $v$ of $w$, generating a run with value $\mathcal{A}(w)$. Notice that such a run prefix $\rho'$ exists, since it is bounded by above by $\rho$ and below by the empty run, whose continuation on the suffix $v$ of $w$ is an arbitrary run on $w$.

Then, the move $t_0 = q_0 \xrightarrow{\sigma_0:x_0} q'_0$ of Eve, played after $\rho'$ is a non-cautious transition: for the suffix $v$ of $w$, there is a run $\pi'$ from $q$ over $\sigma v$ such that $\text{Inf}(\rho'\pi')$ is strictly greater than the value of $\text{Inf}(\rho'\pi)$ for any $\pi$ starting with $t_0$. Thus, we reached a contradiction to the cautiousness of $s$. □

**Theorem 4.5.** *Given a nondeterministic Inf (or Safety) automaton *A* on infinite words, Eve wins *G*₁(*A*) if and only if *A* is HD, and winning strategies in *G*₁(*A*) induce HD strategies for *A* of the same memory size.*

*Proof.* A direct consequence of Theorem 4.1 and Lemma 4.4. □

We move to **Reachability** automata on infinite words.

Observe that the **Reachability** value function with respect to infinite words is not present-
focused (see the automaton $\mathcal{A}$ in Fig. 1), causing also a difference between history-determinism
of a **Reachability** automaton when considered with respect to finite and infinite words (see
the automaton $\mathcal{B}$ in Fig. 1).

Nevertheless, there is a close connection between reachability with respect to finite and
infinite words, as shown below, allowing us to show that 1-token games do characterise
history-determinism also for **Reachability** automata on infinite words.

Recall that we assume that all accepting transitions in a **Reachability** lead to a sink state
that has an accepting self loop on all the alphabet letters – once an accepting transition
has been reached, nothing else matters. Hence, **Reachability** automata with acceptance
on transitions and on states are very similar; the only difference is whether this “heaven”
state is marked accepting or the transition leading to it is. For simplicity, we will consider
automata with acceptance on states in the proof that $G_1$ characterises history-determinism
in **Reachability** automata.

Define a state *q* of a **Reachability** automaton *A* "almost accepting" if there exists a
strategy *s* in the letter game on *A*<sup>*q*</sup> on infinite words, such that for every infinite word *w*,
the run that *s* entails on *w* is accepting. (Notice that every accepting state is also almost
<figure><img src="image_3.png" /><figcaption>Figure 1: An automaton $\mathcal{A}$, demonstrating that the Reachability value function on infinite words is not present-focused: the strategy of Eve that remains forever in $s_0$ is cautious, but does not win the letter game on $\mathcal{A}$. The Reachability automaton $\mathcal{B}$ demonstrates another difference between reachability on finite and infinite words: It is HD on infinite words, but not HD on finite words.</figcaption></figure>

accepting.) Given a Reachability automaton $\mathcal{A}$, we define Polish($\mathcal{A}$) to be the Reachability automaton that is derived from $\mathcal{A}$, by making every almost accepting state of $\mathcal{A}$ accepting.

**Proposition 4.6.** Given a Reachability automaton $\mathcal{A}$ over an alphabet $\Sigma$ with states $Q$ and transitions $\delta$, computing Polish($\mathcal{A}$) is in $O(|\delta| \cdot |\Sigma|)$, and the corresponding strategies that witness almost-acceptance are positional with respect to the product of $Q$ and $\Sigma$.

*Proof.* The “almost acceptance game”, used to find the almost accepting states, is an adaptation of the letter game: Eve wins a play if her run on the word generated by Adam reaches an accepting state. Thus, it is a reachability game over an arena that is the product of the alphabet $\Sigma$ (for Adam’s moves that choose the next letter) and $\mathcal{A}$ (for Eve’s moves that choose her next transition). As computing the winning region of reachability games is linear in the number of the arena’s transitions, and winning strategies in these games are positional, the claim directly follows. $\square$

**Lemma 4.7.** Consider a Reachability automaton $\mathcal{A}$. Then: i) If Eve wins $G_1(\mathcal{A})$ on infinite words then Eve wins $G_1(\text{Polish}(\mathcal{A}))$ on finite words; and ii) If Polish($\mathcal{A}$) on finite words is HD then $\mathcal{A}$ on infinite words is HD.

*Proof.* Let $\mathcal{A}$ be the automaton on infinite words and $\mathcal{A}'$ stand for Polish($\mathcal{A}$) on finite words.

i) Let $s$ be a winning strategy for Eve in $G_1(\mathcal{A})$. We define a strategy $s'$ for Eve in $G_1(\mathcal{A}')$ and show that it is winning: The strategy $s'$ follows $s$ until it reaches an almost accepting state.

If $s'$ eventually reaches an almost accepting state then Eve obviously wins, reaching an accepting state of $\mathcal{A}'$ with her strategy witnessing almost acceptance.

Otherwise, we are guaranteed that Adam’s run also never reaches an accepting state of $\mathcal{A}'$ (which is an almost accepting state of $\mathcal{A}$): Assume toward contradiction that Adam does reach such an almost accepting state $q_A$ when Eve is at a state $q_E$ that is not almost accepting. Then, we claim that Adam can win $G_1(\mathcal{A})$, by generating some infinite suffix $w$, over which he can reach an accepting state of $\mathcal{A}$, using the strategy $s_A$ that witnesses the almost acceptance of $q_A$, while Eve’s strategy $s$ cannot.

Indeed, assume toward contradiction that for every word $w$, the strategy $s$ can reach an accepting state, using the knowledge that Adam starts in $q_A$ and follows $s_A$. Then, we can define a strategy $s_E$ for Eve in the letter game on $\mathcal{A}^{q_E}$ that also reaches an accepting
state on every word $w$: It follows $s$, providing it in every step with the required knowledge about $s_A$, which is possible, since $s_A$ is fixed for the state $q_A$. This however implies that $q_E$ is almost accepting, leading to a contradiction.

ii) Let $s'$ be Eve's winning strategy in the letter game on $\mathcal{A}'$. We define a strategy $s$ for Eve in the letter game on $\mathcal{A}$ and show that it is winning: In every play, the strategy $s$ starts just like $s'$, and continues according to the following two disjoint cases:

- If Adam generates a prefix $u$, such that $u \in L(\mathcal{A}')$ then, since $s'$ is winning in the letter game on $\mathcal{A}'$, Eve, following $s'$, is guaranteed to reach a state $q$ that is almost accepting in $\mathcal{A}$. Then, after the prefix $u$, the strategy $s$ continues like the strategy that witnesses the almost acceptance of $q$, which guarantees to reach an accepting state in $\mathcal{A}$ for whatever infinite suffix that Adam generates, making Eve win.

- Otherwise, $s$ continues forever like $s'$: the word that Adam generates is rejecting and Eve wins. $\square$

**Theorem 4.8.** Given a nondeterministic Reachability automaton $\mathcal{A}$ on infinite words, Eve wins $G_1(\mathcal{A})$ if and only if $\mathcal{A}$ is HD, and winning strategies in $G_1(\mathcal{A})$ induce HD strategies for $\mathcal{A}$ of the same memory size.

*Proof.* If $\mathcal{A}$ is HD then Eve obviously wins $G_1(\mathcal{A})$, by using the same strategy as in the letter game, ignoring Adam's token.

If Eve wins $G_1(\mathcal{A})$ then by Lemma 4.7.i she also wins $G_1(\text{Polish}(\mathcal{A}))$ on finite words, thus by Corrolary 4.2 *Polish*(A) on finite words is HD, implying by Lemma 4.7.ii that A is HD.

Regarding the memory of the HD strategy, observe that Eve's strategy $s$ in $G_1(\text{Polish}(\mathcal{A}))$ is the same as her strategy in $G_1(\mathcal{A})$ (see the proof of Lemma 4.7); her strategy $s'$ in the letter game on *Polish*(A) needs memory of the same size as $s$ (Corrolary 4.2), and her strategy in the letter game on $\mathcal{A}$ either follows $s'$ or diverts to a strategy that witnesses almost-acceptance, which is positional in the arena of the letter game (Proposition 4.6). $\square$

Considering the memory size of the HD strategy, notice that for reachability (and safety) automata, positional strategies suffice; that is these automata are HD if and only if they are determinisable by pruning [BKS17, Theorem 17].

So far, we have shown that the 1-token game characterises history-determinism for various quantitative automata, and in particular for Reachability and Inf on infinite words. The Sup value function can be seen both as a generalisation of Reachability to more than two weights, and as a dual of Inf. However, it turns out that Sup automata behave rather differently, as demonstrated in Fig. 2.

**Proposition 4.9.** $G_1$ does not characterise history-determinism for Sup automata on infinite words.

*Proof.* The automaton $\mathcal{A}$ depicted in Fig. 2 is not HD, while Eve wins $G_1$ on it. $\square$

## 4.2. Solving $G_1$ and Deciding HDness.

We continue with solving the HDness problem of some of the automata types discussed in Section 4.1, for which it is easy to solve the $G_1$ game.

We start with Reachability and Safety automata on finite words, for which solving $G_1$ reduces to solving a safety game.
<figure><img src="image_4.png" /><figcaption>Figure 2: A Sup automaton $\mathcal{A}$, demonstrating that $G_1$ does not characterise history-determinism for Sup automata on infinite words: $\mathcal{A}$ is not HD as Adam can play $a$ when Eve's run is in $s_0$ and $b$ when Eve's run is in $s_1$. If Eve stays in $s_0$, then the word has value 1 and Eve's run has value 0; if Eve goes to $s_1$, then the word has value 3 but Eve's run has value 2. Eve wins $G_1$ by moving to $s_1$ once Adam's token is in $s_1$. If Adam stays in $s_0$, they have the same run; if Adam moves and plays $b$ before Eve moves, she gets value 3 and wins; if he doesn't, then Eve gets the same value as Adam.</figcaption></figure>

**Theorem 4.10.** Deciding whether a Reachability or Safety automaton on finite words is HD can be done in time cubic in the size of $\mathcal{A}$.

*Proof.* By Corrolary 4.2, it is enough to solve $G_1(\mathcal{A})$.

Given a Safety or Reachability automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$ on finite words, $G_1(\mathcal{A})$ reduces to a safety game, whose positions $(\sigma, q, q', t) \in \Sigma \cup \{\varepsilon\} \times Q^2 \times \{L, E, A\}$ consist of a possibly empty letter $\sigma$ representing the last letter played, a pair of states $(q, q')$, one for Eve and one for Adam, which keep track of the end of the current run built by each player, and a turn variable $t \in \{L, E, A\}$ indicating whether it is Adam's turn to give a letter (L), Eve's turn to choose a transition (E), or Adam's turn to choose a transition (A). The initial position is $(\varepsilon, \iota, \iota, L)$. The moves and position ownership encode the permitted moves in $G_1(\mathcal{A})$.

In both cases $G_1(\mathcal{A})$ is a safety game: in the Reachability case, Eve wins if the play remains in positions where either neither player's token has reached the target, or she has reached the target; in the Safety cases, Eve wins if the play remains in positions where either her token is in the safe region, or Adam's token has left the safe region. In both cases, the game can be represented by a cubic-sized arena, which can then be solved in linear time by computing Adam's attractor to the non-safe region. $\square$

While $G_1(\mathcal{A})$ is a safety game if $\mathcal{A}$ operates on finite words, this is no longer the case for $\mathcal{A}$ on infinite words, as, for example in the Reachability case, Eve could reach the target any time after Adam, turning a potentially losing play prefix into a winning one. Nevertheless, solving $G_1$ is still simple, reducing it to solving weak games.

**Theorem 4.11.** Deciding whether a Reachability or Safety automaton $\mathcal{A}$ on infinite words is HD can be done in time cubic in the size of $\mathcal{A}$.

*Proof.* By Theorems 4.5 and 4.8, it is enough to solve $G_1(\mathcal{A})$.

We can encode $G_1(\mathcal{A})$ as a weak game on an arena that consists, as in the proof of Theorem 4.10, of the product of two copies of $\mathcal{A}$ to keep track of each player's token, the alphabet to indicate Adam's last choice of letter, and a variable to indicate whose turn it is to play. For the Safety case, a move is good for Eve, encoded with priority 0, if after the move either Adam's token is out of the safe region, or her token is within the safe region. Other moves are bad for Eve, encoded with priority 1. Eve wins plays that eventually remain within the good region. Similarly, in the Reachability case, a move is good for Eve, encoded with priority 0 if either her token has reached the target or Adam's token has not reached
the target. In both cases, the winning condition is a weak condition since there are no plays alternating good and bad moves infinitely often. In both cases, the resulting game can then be solved in linear time [HMS].

Note that alternatively, for a Safety automaton $\mathcal{A}$, one can encode $G_1(\mathcal{A})$ as a safety game. Indeed, positions in which Eve's token has left the safe region while Adam's token is in a state with a non-empty language are winning for Adam, and can be marked unsafe for Eve, while positions in which Adam's token is in a state with empty language are winning for Eve, and can be marked safe for Eve. Then Eve wins if and only if the play remains in safe positions, that is, either her token is in the safe region of $\mathcal{A}$ or Adam's token is in a state with empty language.

Analogously, there is an alternative solution also for a Reachability automaton $\mathcal{A}$, whereby $G_1(\mathcal{A})$ is encoded as a reachability game, in which the target positions are the almost accepting ones (which, by Proposition 4.6, can be computed in time cubic in the size of $\mathcal{A}$): Positions in which Eve's token is in an almost accepting state are the ones she needs to reach. $\square$

Solving $G_1$ for Sup automata reduces, as in some of the previous cases, to solving safety games.

**Theorem 4.12.** Deciding whether a Sup automaton on finite words is HD is in PTIME, namely in $O(|\Sigma|n^2k)$, where $\Sigma$ is the automaton's alphabet, $k$ the number of weights and $n$ the number of states.

*Proof.* By Corrolary 4.2, it is enough to solve $G_1$.

Given a Sup automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$ with weights $W$, $G_1(\mathcal{A})$ reduces to a safety game, by taking, as in the previous proofs, the product of two copies of $\mathcal{A}$, $\Sigma$, and a variable to keep track of whose turn it is to play. In addition, we use an additional variable $x_E$ to keep track of the maximal weight on Eve's run so far.

The winning condition for Eve is a safety condition: Adam wins if he picks a move with a weight higher than $x_E$, the maximal weight on Eve's run. Then plays in this game are in bijection with plays of $G_1(\mathcal{A})$, and Eve wins if and only if she can avoid Adam choosing a transition with a larger weight than $x_E$, that is, if she can win $G_1(\mathcal{A})$.

Then, solving $G_1(\mathcal{A})$ reduces to solving this safety game, which can be done in time linear in the number of positions of the arena, which is $3|\Sigma|n^2k$. $\square$

Solving $G_1$ for Inf automata reduces to solving safety games, when the automata operate on finite words, and to solving weak games, when the automata operate on infinite words.

**Theorem 4.13.** Deciding whether an Inf automaton on finite or infinite words is HD is in PTIME, namely in $O(|\Sigma|n^2k^2)$, where $\Sigma$ is the automaton's alphabet, $k$ the number of weights and $n$ the number of states.

*Proof.* By Theorem 4.5 and Corrolary 4.2, it is enough to solve $G_1$ on the Inf automaton $\mathcal{A}$.

Analogously to the previous proofs, we can encode $G_1(\mathcal{A})$ as a product of two copies of $\mathcal{A}$ to keep track of each player's token, the alphabet to keep track of the last letter chosen by Adam, a variable to keep track of whose turn it is to play, and a pair of variables to remember the least value read so far by each player's token. (Notice that as opposed to the Sup case, proved in Theorem 4.12, the encoding in this case needs to keep the least value read so far by both players, and cannot do with only one of them.)
In the case of finite words, the winning condition for Eve is a safety condition: the least value seen so far by Eve's token must always be at least as high as the one seen by Adam's token.

In the case of infinite words, the winning condition for Eve is that eventually the value seen by Adam's token must remain at least as high as the one seen by Eve's token. Since there are only finitely many possible values and the least value for each token can only decrease along the run, this is a weak condition.

In both cases the resulting game, of size $O(|\Sigma|n^2k^2)$, can be solved in linear time [HMS].

<figure><img src="image_5.png" /></figure>

Next, we show that solving $G_1$ is in $NP \cap \text{co-NP}$ for DSum automata.

**Theorem 4.14.** For every $\lambda \in \mathbb{Q} \cap (0, 1)$, deciding whether a $\lambda$-DSum automaton $\mathcal{A}$, on finite or infinite words, is HD is in $NP \cap \text{co-NP}^2$.

*Proof.* Consider a $\lambda$-DSum automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$, where the weight of a transition $t$ is denoted by $\gamma(t)$. By Corrolary 4.3, it suffices to show that solving $G_1(\mathcal{A})$ is $NP \cap \text{co-NP}$. We achieve this by reducing solving $G_1(\mathcal{A})$ to solving a discounted-sum threshold game, which Eve wins if the DSum of a play is non-negative. It is enough to consider infinite games, as they also encode finite games, by allowing Adam to move to a forever-zero-position in each of his turns.

The reduction follows the same pattern as that in the proof of Theorem 4.12: we represent the arena of the game $G_1(\mathcal{A})$ as a finite arena, and encode its winning condition, which requires the difference between the DSum of two runs to be non-negative, as a threshold DSum winning condition. Note first that the difference between the $\lambda$-DSum of the two sequences $x_0x_1\dots$ and $x'_0x'_1\dots$ of weights is equal to the $\lambda$-DSum of the sequence of differences $d_0 = (x_0 - x'_0), d_1 = (x_1 - x'_1), \dots$, as follows: $(\sum_{i=0}^{\infty} \lambda^i x_i) - (\sum_{i=0}^{\infty} \lambda^i x'_i) = (\sum_{i=0}^{\infty} \lambda^i (x_i - x'_i))$.

We now describe the DSum arena $G$ in which Eve wins with a non-strict 0-threshold objective if and only if she wins $G_1(\mathcal{A})$. (See an example in Fig. 3.) The arena has positions in $(m, \sigma, t, q, q') \in \{L, E, A\} \times \Sigma \cup \{\varepsilon\} \times \delta \cup \{\varepsilon\} \times Q^2$ where $m$ denotes the move type, having $L$ for Adam choosing a letter, $E$ for Eve choosing a transition and $A$ for Adam choosing a transition; $\sigma$ is the last played letter if $m = E$ or $m = A$ and $\varepsilon$ otherwise; $t$ is the transition just played by Eve if $m = A$ and $\varepsilon$ otherwise; and the states $q, q'$ represent the positions of Eve and Adam's tokens.

A move of Adam that chooses a transition $t' = q' \xrightarrow{\sigma:x} q''$, namely a move $(A, \sigma, t, q, q') \rightarrow (L, \varepsilon, \varepsilon, q, q'')$, is given weight $\gamma(t) - \gamma(t')$, that is, the difference between the weights of the transitions chosen by both players. Other transitions are given weight 0. Observe that we need to compensate for the fact that only one edge in three is weighted. One option to do it is to take a discount factor $\lambda' = \lambda^{\frac{1}{3}}$ for the DSum game $G$. Yet, $\lambda'$ can then be irrational, which somewhat complicates things. Another option is to consider discounted-sum games with multiple discount factors [And06] and choose three rational discount factors $\lambda', \lambda'', \lambda''' \in \mathbb{Q} \cap (0, 1)$, such that $\lambda' \cdot \lambda'' \cdot \lambda''' = \lambda$. Since the first two weights in every triple are 0, only the multiplication of the three discount factors toward the third weight is what matters. For $\lambda = \frac{p}{q}$, where $p < q$ are positive integers, one can choose $\lambda' = \frac{4p}{4p+1}$, $\lambda'' = \frac{4p+1}{4p+2}$, and $\lambda''' = \frac{2p+1}{2q}$.

<footnote n="2">²It was already known for finite words [FLW20]. It is perhaps surprising for infinite words, given the NP-hardness result in [HPR16, Theorem 6]. In consultation with the authors, we have confirmed that there is an error in the hardness proof.</footnote>
Plays in $G_1(\mathcal{A})$ and in $G$ are in bijection. It now suffices to argue that the winning condition of $G$, namely that the $(\lambda', \lambda'', \lambda''')$-DSum of the play is non-negative, correctly encodes the winning condition of $G_1(\mathcal{A})$, meaning that the difference between the $\lambda$-DSum of Eve's run and of Adam's run is non-negative.

Let $d_0d_1...$ be the sequence of weight differences between the transitions played by both players in $G_1(\mathcal{A})$, and let $\lambda_0, \lambda_1, ...$ and $w_0, w_1, ...$ be the corresponding sequences of discount factors and weights in the $(\lambda', \lambda'', \lambda''')$-DSum game, respectively, where for every $i = (0 \mod 3)$, we have $w_i = 0$ and $\lambda_i = \lambda'$, for every $i = (1 \mod 3)$, we have $w_i = 0$ and $\lambda_i = \lambda''$, and for every $i = (2 \mod 3)$, we have $w_i = d_i$ and $\lambda_i = \lambda'''$. Then the value of the $(\lambda', \lambda'', \lambda''')$-DSum sequence is equal to the required DSum sequence multiplied by $\lambda' \cdot \lambda''$:

$$ (\lambda', \lambda'', \lambda''')\text{-DSum} = \sum_{i=0}^{\infty} (0 \cdot \prod_{j=0}^{3i-1} \lambda_j + 0 \cdot \prod_{j=0}^{3i} \lambda_j + w_{3i+2} \cdot \prod_{j=0}^{3i+1} \lambda_j) = \lambda' \cdot \lambda'' \cdot \sum_{i=0}^{\infty} \lambda^i d_i $$

Hence Eve wins the game $G_1(\mathcal{A})$ if and only if she wins the 0-threshold $(\lambda', \lambda'', \lambda''')$-DSum game over $G$. As $G$ has a state-space polynomial in the state-space of $\mathcal{A}$ and solving DSum-games is in NP$\cap$NP [And06], solving $G_1(\mathcal{A})$, and therefore deciding whether $\mathcal{A}$ is HD, is also in NP$\cap$NP. $\square$

DSum games are positionally determined [Sha53, ZP95, And06] so this algorithm also computes a finite-memory witness of HDness for $\mathcal{A}$ that is of polynomial size in the state-space of $\mathcal{A}$. However, a positional witness also exists [HPR16, Section 5].

One might be tempted to think that the proof of Theorem 4.14 generalises to discounted-sum automata with multiple discount factors [BH21]. Yet, this is not the case: While the value function of discounted-summation with multiple discount factors is indeed present-focused, using an argument analogous to the one in [BL21, Lemma 22], and the proof of Theorem 4.14 indeed uses discounted-sum games with multiple discount factors, the issue is that the value difference between the discounted-summation of two weight sequences is much more involved with multiple discount factors than with a single one. Hence, the representation that we use in the proof of Theorem 4.14 to capture this value difference no longer holds in the case of multiple discount factors. We leave open the question of the complexity (and decidability) of HDness of discounted-sum automata with multiple discount factors.

## 5. DECIDING HISTORY-DETERMINISM VIA TWO TOKEN GAMES

In this section we solve the HDness problem of Sup, LimSup and LimInf automata on infinite words via two-token games. As is the case with Büchi and coBüchi automata [BK18, Lemma 8]$^3$, one-token games do not characterise HDness of LimSup and LimInf automata. We showed in Section 4 that this is also the case for Sup automata on infinite words (unlike on finite words where one token does suffice).

For Sup and LimInf, a possible approach is to solve the letter game directly: an equivalent deterministic automaton can track the value of a word, and the winning condition of the letter game corresponds to comparing Eve's run to the one of the deterministic automaton. Unfortunately, determinising both Sup and LimInf automata is exponential in the number of

<footnote>$^3$The Büchi automaton presented in [BK18, Lemma 8] is a weak one, so it can also be viewed as a coBüchi one.</footnote>
states [CDH10, Theorem 13], so the new game is large. In addition, for LimInf automata, its winning condition, which compares the LimInf value of two runs, is non-standard and

A DSum automaton $\mathcal{A}$ with a discount factor $\lambda = \frac{5}{7}$

<figure><img src="image_6.png" /></figure>

A DSum game $G$ with discount factors $\lambda' = \frac{20}{21}$, $\lambda'' = \frac{21}{22}$, and $\lambda''' = \frac{11}{14}$

<figure><img src="image_7.png" /><figcaption>Figure 3: An example of a DSum automaton $\mathcal{A}$ and the corresponding DSum game $G$ with multiple discount factors, as per the proof of Theorem 4.14, such that Eve wins $G1(\mathcal{A})$ if and only if she wins $G$ with respect to the non-strict 0-threshold. Rectangular positions in $G$ are of Adam and ellipses of Eve.</figcaption></figure>
needs additional work to be encoded into a parity game. For $\mathbf{LimSup}$ automata the situation is even worse, as they are not necessarily equivalent to deterministic $\mathbf{LimSup}$ automata, so it is not obvious whether the winner of the letter game is decidable at all.

Here we first show, in Section 5.1, that the 2-token-game approach, used to resolve HDness of Büchi and coBüchi automata, can be generalised to $\mathbf{Sup}$, $\mathbf{LimSup}$ and $\mathbf{LimInf}$ automata. Our proofs for the $\mathbf{LimSup}$ and $\mathbf{LimInf}$ cases follow the same structure, while relying on the $G_2$ characterisation of HDness for Büchi and coBüchi automata respectively. We then show that $G_2$ also characterises the HDness of $\mathbf{Sup}$ automata on infinite words, via reduction to the $\mathbf{LimSup}$ case.

We then analyse the complexity of solving $G_2$ for these three automata classes, in Section 5.2. Perhaps surprisingly (since the naive approach to solving the letter game seems harder for $\mathbf{LimSup}$), we show that $G_2$ is solvable in quasip polynomial time for $\mathbf{LimSup}$ while for $\mathbf{LimInf}$ our algorithm is exponential in the number of weights (but not in the number of states). For $\mathbf{Sup}$ automata on infinite words, solving $G_2$ can be done in polynomial time, as it reduces to solving a coBüchi game of cubic size.

Without loss of generality, we assume the weights to be $\{1, 2, \dots\}$.

### 5.1. $G_2$ Characterises HDness for some automata.

This section is dedicated to proving that a $\mathbf{LimSup}$, $\mathbf{LimInf}$ or $\mathbf{Sup}$ automaton on infinite words is HD if and only if Eve wins the 2-token game on it. In both the $\mathbf{LimSup}$ and the $\mathbf{LimInf}$ cases, the structure of the argument is similar. One direction is immediate: if an automaton $\mathcal{A}$ is HD, then Eve can use the letter-game strategy to win in $G_2(\mathcal{A})$, ignoring Adam's tokens. The other direction requires more work. We use an additional notion, that of $k$-HDness, which generalises HDness, in the sense that Eve maintains $k$ runs, rather than only one, and needs at least one of them to be optimal. We will then show that if Eve wins $G_2(\mathcal{A})$, then $\mathcal{A}$ is $k$-HD for a finite $k$ (namely, the number of weights in $\mathcal{A}$ minus one); this is where the argument differs slightly according to the value function. Finally, we will show that for automata that are $k$-HD, for any finite $k$, a strategy for Eve in $G_2(\mathcal{A})$ can be combined with the $k$-HD strategy to obtain a strategy for her in the letter game.

Many of the tools used in this proof are familiar from the $\omega$-regular setting [BK18, BKLS20]. The main novelty in the argument is the decomposition of the $\mathbf{LimSup}$ ($\mathbf{LimInf}$) automaton $\mathcal{A}$ with $k$ weights into $k-1$ Büchi (coBüchi) automata $A_2, \dots, A_k$, each $A_i$ of which recognises the language of words of value at least $i$, that are HD whenever Eve wins $G_2(\mathcal{A})$. (The converse does not hold, namely $A_2, \dots, A_k$ can be HD even if Eve loses $G_2(\mathcal{A})$ – see Fig. 5.) In both cases, the HD strategies for $A_2, \dots, A_k$ can then be combined to prove the $k$-HDness of $\mathcal{A}$.

Fig. 4 illustrates the flow of our arguments.

Finally, we show that $G_2$ also characterises the HDness of $\mathbf{Sup}$ automata on infinite words using the characterisation for $\mathbf{LimSup}$.

We first generalise to quantitative automata Bagnol and Kuperberg's key insight that if Eve wins $G_2$, then she also wins $G_k$ for all $k$ [BK18, Thm 14].

**Theorem 5.1.** Given a quantitative automaton $\mathcal{A}$, if Eve wins $G_2(\mathcal{A})$ then she also wins $G_k(\mathcal{A})$ for any $k \in \mathbb{N} \setminus \{0\}$. Furthermore, if her winning strategy in $G_2(\mathcal{A})$ has memory of size $m$ and $\mathcal{A}$ has $n$ states, then she has a winning strategy in $G_k(\mathcal{A})$ with memory of size $n^{k-1} \cdot m^k$.
<figure><img src="image_8.png" /><figcaption>Figure 4: The flow of arguments for showing that $G_2(\mathcal{A}) \implies \mathrm{HD}(\mathcal{A})$ for a LimInf or LimSup automaton $\mathcal{A}$.</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Figure 5: A LimSup automaton $\mathcal{A}$ and corresponding Büchi automata $\mathcal{A}_2$ and $\mathcal{A}_3$, as per Lemma 5.4. (Accepting transitions in $\mathcal{A}_2$ and $\mathcal{A}_3$ are marked with double lines.) Observe that $\mathcal{A}$ is not HD and Eve loses the two-token game on $\mathcal{A}$, while both $\mathcal{A}_2$ and $\mathcal{A}_3$ are HD. (In $\mathcal{A}$, if Eve goes from $s_0$ to $s_1$, Adam goes from $s_0$ to $s_2$ and continues with an $a$, and if she goes from $s_0$ to $s_2$, Adam goes from $s_0$ to $s_1$ and continues with a $b$. In $\mathcal{A}_2$ Eve goes from $s_0$ to $s_1$ and in $\mathcal{A}_3$ from $s_0$ to $s_2$.)</figcaption></figure>

*Proof.* This is the generalisation of [BK18, Thm 14]. The proof is similar to Bagnol and Kuperberg's original proof, but without assuming positional strategies for Eve in $G_k(\mathcal{A})$. If Eve wins $G_2(\mathcal{A})$ then she obviously wins $G_1(\mathcal{A})$, using her $G_2$ strategy with respect to two copies of Adam's single token in $G_1$. We thus consider below $G_k(\mathcal{A})$ for every $k \in \mathbb{N} \setminus \{0, 1, 2\}$.

Let $s_2$ be a winning strategy for Eve in $G_2(\mathcal{A})$. We inductively show that Eve has a winning strategy $s_i$ in $G_i(\mathcal{A})$ for each finite $i$. To do so, we assume a winning strategy $s_{i-1}$ in $G_{i-1}(\mathcal{A})$. The strategy $s_i$ maintains some additional (not necessarily finite) memory that maintains the position of one virtual token in $\mathcal{A}$, a position in the (not necessarily finite) memory structure of $s_{i-1}$, and a position in the (not necessarily finite) memory structure of $s_2$. The virtual token is initially at the initial state of $\mathcal{A}$. The strategy $s_i$ then plays as follows: at each turn, after Adam has moved his $i$ tokens and played a letter (or, at the first turn, just played a letter), it first updates the $s_{i-1}$ memory structure, by ignoring the last of Adam's tokens, and, treating the position of the virtual token as Eve's token in $G_{i-1}(\mathcal{A})$, it updates the position of the virtual token according to the strategy $s_{i-1}$; it then updates
the $s_2$ memory structure by treating Adam's last token and the virtual token as Adam's 2 tokens in $G_2(\mathcal{A})$, and finally outputs the transition to be played according to $s_2$.

We now argue that this strategy is indeed winning in $G_i(\mathcal{A})$. Since $s_{i-1}$ is a winning strategy in $G_{i-1}(\mathcal{A})$, the virtual token traces a run of which the value is at least as large as the value of any of the runs built by the first $i-1$ tokens of Adam. Since $s_2$ is also winning, the value of the run built by Eve's token is at least as large as the values of the runs built by the virtual token and by Adam's last token. Hence, Eve is guaranteed to achieve at least the supremum value of Adam's $i$ runs, making this a winning strategy in $G_i(\mathcal{A})$.

As for the memory size of a winning strategy for Eve in $G_k(\mathcal{A})$, let $m$ be the memory size of her winning strategy in $G_2(\mathcal{A})$ and $n$ the number of states in $\mathcal{A}$. Then, by the above construction of her strategy in $G_k(\mathcal{A})$, the memory of her strategy in $G_3(\mathcal{A})$ is $n$ for the virtual token times $m$ for the copy of her memory in $G_2(\mathcal{A})$ times $m$ for the copy of her memory in $G_{i-1}(\mathcal{A}) = G_2(\mathcal{A})$, namely $n \cdot m \cdot m = n \cdot m^2$. Then for $G_4(\mathcal{A})$ it is $n \cdot m \cdot (n \cdot m^2) = n^2 \cdot m^3$; for $G_5(\mathcal{A})$ it is $n \cdot m \cdot (n^2 \cdot m^3) = n^3 \cdot m^4$, and for $G_k(\mathcal{A})$ it is $n^{k-1} \cdot m^k$. $\square$

We proceed with the definition of $k$-HDness (a related, but different notion is the “width” of an automaton [MK19]), based on the $k$-runs letter game (not to be confused with $G_k$, the $k$-token game), which generalises the letter game.

**Definition 5.2** (*k*-HD and *k*-runs letter game). A configuration of the game on a quantitative automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$ is a tuple $q^k \in Q^k$ of states of $\mathcal{A}$, initialised to $\iota^k$.

In a configuration $(q_{i,1}, \dots, q_{i,k})$, the game proceeds as follows to the next configuration $(q_{i+1,1}, \dots, q_{i+1,k})$.

* Adam picks a letter $\sigma_i \in \Sigma$, then

* Eve chooses for each $q_{i,j}$, a transition $q_{i,j} \xrightarrow{\sigma_i:x_{i,j}} q_{i+1,j}$

In the limit, a play consists of an infinite word $w$ that is derived from the concatenation of $\sigma_0, \sigma_1, \dots$, as well as of $k$ infinite sequences $\rho_0, \rho_1, \dots$ of transitions. Eve wins the play if $\max_{j \in \{1 \dots k\}} \mathrm{Val}(\rho_j) = \mathcal{A}(w)$.

If Eve has a winning strategy, we say that $\mathcal{A}$ is $k$-HD, or that $\mathrm{HD}_k(\mathcal{A})$ holds.

Notice that the standard letter game (Definition 2.1) is a 1-run letter game and standard HD (Definition 2.1) is 1-HD.

Next, we use $\mathrm{HD}_k(\mathcal{A})$ to show that $G_2$ characterises HDness.

**Proposition 5.3** [BK18]. Given a quantitative automaton $\mathcal{A}$, if $\mathrm{HD}_k(\mathcal{A})$ for some $k \in \mathbb{N}$, and Eve wins $G_k(\mathcal{A})$, then $\mathcal{A}$ is HD.

*Proof.* The argument is identical to the one used in [BK18], which we summarise here. The strategy $\tau$ for Eve in $\mathrm{HD}_k(\mathcal{A})$ provides a way of playing $k$ tokens that guarantees that one of the $k$ runs formed achieves the automaton's value on the word $w$ played by Adam. If Eve moreover wins $G_k(\mathcal{A})$ with some strategy $s_k$, she can, in order to win in the letter game, play $s_k$ against Adam's letters and $k$ virtual tokens that she moves according to $\tau$. The winning strategy $\tau$ guarantees that one of the $k$ runs built by the $k$ virtual tokens achieves $\mathrm{Val}(w)$; then her strategy $s_k$ guarantees that her run also achieves $\mathrm{Val}(w). $\square

It remains to prove that if Eve wins $G_2(\mathcal{A})$, then $\mathrm{HD}_k(\mathcal{A})$ for some $k$.

Given a $\mathrm{LimSup}$ automaton $\mathcal{A}$, with weights $\{1, \dots, k\}$, we define $k-1$ auxiliary Büchi automata $A_2, \dots, A_k$ with acceptance on transitions: each $A_x$ is a copy of $\mathcal{A}$, where a transition is accepting if its weight $i$ in $\mathcal{A}$ is at least $x$. (See Fig. 5.) Dually, given a $\mathrm{LimInf}$
automaton $\mathcal{A}$, each $A_x$ is a coBüchi automaton, and consists of a copy of $\mathcal{A}$ where transitions with weights smaller than $x$ are rejecting, while those with weights $x$ or larger are accepting. Again, in both cases $A_x$ recognises the set of words $w$ such that $\mathcal{A}(w) \ge x$.

We now use these auxiliary automata to argue that if $G_2(\mathcal{A})$ then $\mathrm{HD}_{k-1}(\mathcal{A})$.

**Lemma 5.4.** *Given a LimSup or LimInf automaton $\mathcal{A}$ with weights $\{1, \dots, k\}$, if Eve wins $G_2(\mathcal{A})$, then for all $x \in \{2, \dots, k\}$, Eve also wins $G_2(A_x)$.*

*Proof.* Since $A_x$ is identical to $\mathcal{A}$ except for the acceptance condition or value function, Eve can use in $G_2(A_x)$ her winning strategy in $G_2(\mathcal{A})$.

For the LimSup case, if one of Adam's runs sees an accepting transition infinitely often, the underlying transition of $\mathcal{A}$ visited infinitely often has weight at least $x$. Then, Eve's strategy guarantees that her run also sees infinitely often a value at least as large as $x$, corresponding to an accepting transition in $G_2(A_x)$.

Similarly, for the LimInf case, if one of Adam's runs avoids seeing a rejecting transition infinitely often in $A_x$, then this run's value in $\mathcal{A}$ is at least $x$, and Eve's strategy guarantees that her run's value in $\mathcal{A}$ is at least $x$, meaning that it avoids seeing a rejecting transition in $A_x$ infinitely often, and accepts. $\square$

**Lemma 5.5.** *Given a LimSup or LimInf automaton $\mathcal{A}$ with weights $[1..k]$, if Eve wins $G_2(A_x)$ for all $x \in [2..k]$ then $\mathrm{HD}_{k-1}(\mathcal{A})$ holds.*

*Proof.* From Lemma 5.4, if Eve wins $G_2(\mathcal{A})$, then for all $x \in [2..k]$, Eve also wins $G_2(A_x)$. We first argue that each $A_x$ is HD.

Since each $A_x$ is a Büchi or coBüchi automaton, this implies that for all $x \in [2..k]$, the automaton $A_x$ is HD [BK18, BKLS20], witnessed by a winning strategy $s_x$ for Eve in the letter game on each $A_x$.

Now, in the $(k-1)$-run letter game on $\mathcal{A}$, Eve can use each $s_x$ to move one token. Then, if Adam plays a word $w$ with some value $\mathrm{Val}(w) = i$, this word is accepted by $A_i$, and therefore the strategy $s_i$ guarantees that the run of the $i^{th}$ token achieves at least the value $i$, corresponding to seeing accepting transitions of $A_i$ infinitely often for the LimSup case, or eventually avoiding rejecting transitions in the LimInf case. $\square$

Finally, we combine the $G_2$ and $\mathrm{HD}_{k-1}$ strategies in $\mathcal{A}$ to show that $\mathcal{A}$ is HD.

**Theorem 5.6.** *A nondeterministic LimSup or LimInf automaton $\mathcal{A}$ is HD if and only if Eve wins $G_2(\mathcal{A})$.*

*Proof.* If $\mathcal{A}$ is HD then Eve can use the letter-game strategy to win in $G_2(\mathcal{A})$, ignoring Adam's moves. If Eve wins $G_2(\mathcal{A})$ then by Lemma 5.4 and Lemma 5.5 she wins $\mathrm{HD}_{k-1}(\mathcal{A})$, where $k$ is the number of weights in $\mathcal{A}$. By Theorem 5.1 she also wins $G_{k-1}(\mathcal{A})$ and, finally, by Proposition 5.3 we get that $\mathcal{A}$ is HD. $\square$

We show next that $G_2$ characterises HDness also for Sup automata, by reducing the problem to the case of LimSup automata.

**Corollary 5.7.** *A nondeterministic Sup automaton $\mathcal{A}$ on infinite words is HD if and only if Eve wins $G_2(\mathcal{A})$.*

*Proof.* One direction is direct: if $\mathcal{A}$ is HD, then Eve wins $G_2(\mathcal{A})$ by using her HD strategy and ignoring Adam's tokens.

For the other direction, given a Sup automaton $\mathcal{A}$ with initial state $i$ and $k$ weights, we construct a LimSup automaton $\mathcal{A}'$, such that i) if $\mathcal{A}'$ is HD then $\mathcal{A}$ is HD, and ii) if Eve wins
$G_2(\mathcal{A})$, then she also wins $G_2(\mathcal{A}')$. As by Theorem 5.6 Eve wins $G_2(\mathcal{A}')$ if and only if $\mathcal{A}'$ is HD, we conclude that if Eve wins $G_2(\mathcal{A})$, then $\mathcal{A}$ is HD.

$\mathcal{A}'$ has the same alphabet as $\mathcal{A}$. The state-space of $\mathcal{A}'$ consists of $k$ copies of $\mathcal{A}$, one for each weight: for each state $q$ of $\mathcal{A}$, we have states $q_i$ of $\mathcal{A}'$, for $i \in [1..k]$. In the $i^{th}$ copy of $\mathcal{A}$, we only keep transitions of weight up to $i$ in $\mathcal{A}$, and all of them have weight $i$ in $\mathcal{A}'$. Transitions of higher weight $x$ move from the $i^{th}$ copy to the $x^{th}$ copy. More precisely, for each pair of weights $i$ and $x$:

* $(q_i, \sigma, i, q'_i)$ is a transition in $\mathcal{A}'$ if $(q, \sigma, x, q')$ is a transition in $\mathcal{A}$ and $x \le i$.

* $(q_i, \sigma, x, q'_x)$ is a transition in $\mathcal{A}'$ if $(q, \sigma, x, q')$ is a transition in $\mathcal{A}$ and $x > i$.

The initial state of $\mathcal{A}'$ is $\iota_1$.

First note that this LimSup-automaton computes the same function as $\mathcal{A}$: runs of $\mathcal{A}$ and $\mathcal{A}'$ are in value-preserving bijection since in $\mathcal{A}'$ the weight that occurs on each transition is the largest weight seen so far in the corresponding run of $\mathcal{A}$.

Then, observe that if $\mathcal{A}'$ is HD then $\mathcal{A}$ is HD. Indeed, Eve's winning strategy $s'$ in the letter game on $\mathcal{A}'$ can be used in the letter game on $\mathcal{A}$ by choosing the transition $(q, \sigma, x, q')$ instead of $(q_i, \sigma, x, q'_x)$ and the available transition $(q, \sigma, x, q')$ maximising $x$ instead of $(q_i, \sigma, i, q'_i)$. Again, this strategy achieves a run of the same value as $s'$ on every word since whenever $s'$ moves to the next copy of $\mathcal{A}$, it sees a transition of the corresponding weight, guaranteeing at least this value. Eve therefore also wins in the letter game on $\mathcal{A}$.

Similarly, we claim that if Eve wins $G_2(\mathcal{A})$, she also wins $G_2(\mathcal{A}')$. Indeed, given a winning strategy $s$ in $G_2(\mathcal{A})$, she can play according to the strategy $s'$ that chooses the available $(q_i, \sigma, i, q'_x)$ or $(q_i, \sigma, x, q'_x)$ transition whenever $s$ chooses $(q, \sigma, x, q')$, and interprets Adam's moves $(q_i, \sigma, x, q'_x)$ in $G_2(\mathcal{A}')$ as $(q, \sigma, x, q')$ in $G_2(\mathcal{A})$ and Adam's moves $(q_i, \sigma, i, q'_i)$ in $G_2(\mathcal{A}')$ as the available transition $(q, \sigma, x, q')$ maximising $x$ in $G_2(\mathcal{A})$. Then, whatever values Adam's tokens achieve in $G_2(\mathcal{A}')$, $s$ guarantees that Eve's token in $G_2(\mathcal{A})$ does better, and $s'$ guarantees this same value for Eve's token in $G_2(\mathcal{A}'))$. $\square$

**Remark 5.8.** An alternative proof for the above corollary can be obtained by following the same proof schema as for Theorem 5.6, but decomposing the **Sup** automaton into **Reachability** automata instead of Büchi or coBüchi automata.

## 5.2. Solving $G_2$ and Deciding HDness.

Now that we have established that $G_2$ characterises history-determinism for Sup, LimSup, and LimInf automata, we study the complexity of solving $G_2$ in each case. We start with the case of Sup automata on infinite words, which is the simplest, via reduction to polynomially sized coBüchi game.

**Theorem 5.9.** Deciding whether a Sup automaton $\mathcal{A}$ on infinite words is HD can be done in time polynomial in the size of $\mathcal{A}$.

*Proof.* By Corrolary 5.7, it is enough to solve $G_2(\mathcal{A})$.

We encode $G_2(\mathcal{A})$ for a Sup automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$ as a coBüchi game as follows. The arena is that of $G_2(\mathcal{A})$, represented as the product of the alphabet and three copies of $\mathcal{A}$, to reflect the current letter and the current position of each of the three runs, and a variable indicating whose turn it is to move. In addition, a variable $x_E$ keeps track of the greatest value seen by Eve's run so far, and $x_A$ keeps track of the greatest value seen by either of Adam's runs so far. The winning condition for Eve is then that eventually $x_E \ge x_A$.
remains true, which is a coBüchi condition. The size of the arena is thus polynomial, and the complexity of solving coBüchi games is quadratic [CH12]. □

We proceed with the LimSup and LimInf cases, for which $G_2$ can be solved via a reduction to a parity game. The $G_2$ winning condition for LimSup automata can be encoded by adding carefully chosen priorities to the arena of $G_2(\mathcal{A})$, while for LimInf the encoding requires additional positions.

**Theorem 5.10.** Deciding whether a LimSup automaton $\mathcal{A}$ of size $n$ with $k$ weights is HD is quasip polynomial in $n$, and if $k$ is in $O(\log n)$, in time polynomial in $n$.

*Proof.* By Theorem 5.6, it is enough to solve $G_2(\mathcal{A})$.

We encode the game $G_2(\mathcal{A})$, for a LimSup automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$, into a parity game as follows. The arena is simply the arena of $G_2(\mathcal{A})$, seen as a product of the alphabet and three copies of $\mathcal{A}$, to reflect the current letter and the current position of each of the three runs (one for Eve, two for Adam), and a variable to keep track of which turn it is to play. (Adam's turn to give a letter, Eve's turn to choose a transition, Adam's turn to choose his first transition, or Adam's turn to choose his second transition.)

Adam's letter-picking moves are labelled with priority 0, Eve's choices of transition $q \xrightarrow{\sigma:x} q'$ are labelled with priority $2x$ and Adam's choices of transition $q \xrightarrow{\sigma:x} q'$ are labelled with priority $2x-1$.

We claim that Eve wins this parity game if and only if she wins $G_2(\mathcal{A})$, that is, the priorities correctly encode the winner of $G_2(\mathcal{A})$. Observe that the even priorities seen infinitely often in a play of the parity game are exactly priorities $2x$, where $x$ is a weight seen infinitely often in Eve's run in the corresponding play in $G_2(\mathcal{A})$. The odd priorities seen infinitely often on the other hand are $2x-1$, where $x > 0$ occurs infinitely often on one of Adam's runs in the corresponding play of $G_2(\mathcal{A})$. Hence, Eve can match the maximal value of Adam's runs in $G_2(\mathcal{A})$ if and only if she can win the parity game that encodes $G_2(\mathcal{A})$.

The number of positions in this game is polynomial in the size $n$ of $\mathcal{A}$; the maximal priority is linear in the number $k$ of its weights. It can be solved in quasip polynomial time, or in polynomial time if $k$ is in $O(\log n)$, using the reader's favourite state-of-the-art parity game algorithm, for instance [CJK$^+$17]. □

**Theorem 5.11.** Deciding whether a LimInf automaton $\mathcal{A}$ of size $n$ with $k$ weights is HD can be done in time exponential in $k$, and if $k$ is in $O(\log n)$, in time polynomial in $n$.

*Proof.* By Theorem 5.6, it is enough to solve $G_2(\mathcal{A})$.

As in the proof of Theorem 5.10, we can represent $G_2(\mathcal{A})$ as a game on an arena that is the product of three copies of $\mathcal{A}$, one for Eve and two for Adam. The winning condition for Eve is that the smallest weight seen infinitely often on the run built on her copy of $\mathcal{A}$ should be at least as large as both of the minimal weights seen infinitely often on the runs built on Adam's copies. We will encode this winning condition as a parity condition, but, unlike in the LimSup case, we will need to use an additional memory structure, which we describe now.

The weights on Eve's run will be encoded by *odd* priorities, with smaller weights corresponding to higher priorities, as for LimInf the lowest weight seen infinitely often is the one that matters, while weights on Adam's runs will be encoded by *even* priorities, but only once both of Adam's runs have seen the corresponding weight or a lower one. Keeping track of this last condition requires the following additional memory structure, which encodes which of Adam's runs has seen which weight recently.
<figure><img src="image_10.png" /><figcaption>Figure 6: Memory structure as described in the proof of Theorem 5.11 for keeping track of when both of Adam’s runs in $G_2(\mathcal{A})$ have seen a priority smaller than $i = 5$. The labels $\tau_1$ and $\tau_2$ stand for moves in $G_2(\mathcal{A})$ that correspond to Adam choosing a transition of $\mathcal{A}$ with weight $w \le 5$ in his first and second runs, respectively. A label $\{\dots\}$ stands for all moves in $G_2(\mathcal{A})$ except for those in $\{\dots\}$.</figcaption></figure>

More precisely, let $k$ be the number of weights in $\mathcal{A}$. Moves corresponding to Eve choosing a transition of $\mathcal{A}$ with weight $i$ have priority $2(k-i+1)-1$, that is, an odd priority that is larger the smaller $i$ is. Further, for each weight $i \in [1..k]$, we use a three-valued variable $x_i \in \{0, 1, 2\}$, initiated to 0, which gets updated as follows: if $x_i = 0$ and the game move corresponds to Adam choosing a transition of $\mathcal{A}$ with weight $w \le i$ in one of his runs, $x_i$ is updated to 1 or 2 according to which of Adam’s run saw this weight; if $x_i = 1$ (resp. 2) and the game move corresponds to Adam choosing a transition of $\mathcal{A}$ with weight $w \le i$ in his second (resp. first) run, then $x_i$ is reset to 0. Moves that reset variables to 0 have priority $2(k-i+1)$ for the minimal $i$ such that the transition resets $x_i$ to 0. Other moves have priority 1.

We now argue that the highest priority seen infinitely often along a play is even if and only if the $\text{LimInf}$ value of Eve’s run is at least as high as that of both of Adam’s runs. Indeed, the maximal odd priority seen infinitely often on a play is $2(k-i+1)-1$ such that $i$ is the minimal priority seen on Eve’s run infinitely often, and the maximal even priority seen infinitely often is $2(k-j+1)$ where $j$ is the minimal weight such that both of Adam’s runs see $j$ or a smaller priority infinitely often. In particular, $2(k-i+1)-1 < 2(k-j+1)$ if and only if $i \ge j$, that is, if Eve wins $G_2(\mathcal{A})$.

This parity game is of size polynomial in $n$ and exponential in $k$, where the latter is due to the memory structure $(\{0, 1, 2\}^k)$ and has $2k$ priorities. As the number of priorities is logarithmic in the size of the game, it can be solved in polynomial time [CJK$^{+}$17]. If $k$ is in $O(\log n)$, then the algorithm is polynomial in the size $n$ of $\mathcal{A}$. $\square$

These results can be compared to the problem referred to as zero-regret synthesis against word-strategies in [HPR17]. There, the $\text{LimInf}$ and $\text{Sup}$ cases are solved in exponential time in the size of the automaton via determinisation. In contrast, our procedure is polynomial for $\text{Sup}$, quasip polynomial for $\text{LimSup}$ and exponential in the number of weights for $\text{LimInf}$.

In contrast to the cases considered in Section 4, where strategies in $G_1$ induce HD strategies of the same memory size, a winning $G_2$ strategy does not necessarily induce an HD strategy of the same memory size (even when it implies the existence of such a strategy). We now analyse the size of the HD strategies which our proofs show exist whenever Eve wins $G_2$, and discuss the implications for the determinability of HD $\text{LimSup}$ automata.
**Corollary 5.12.** *Consider an HD Sup, LimSup, or LimInf automaton *A* of size *n* with *k* + 1 weights on infinite words. If *A* is a Sup or LimSup automaton, there is an HD strategy for *A* with memory polynomial in *n* if *k* is in O(log *n*), and of memory exponential in *k* otherwise. If *A* is a LimInf automaton, there is an HD strategy for *A* with memory exponential in *n*.*

*Proof.* We construct an HD strategy for LimSup or LimInf $\mathcal{A}$, by combining an $HD_k$ strategy and a $G_k$ strategy for it.

The $HD_k$ strategy—which, like the HD strategy, is hard to compute directly—combines the HD strategies of the $k$ auxiliary Büchi or coBüchi automata for $\mathcal{A}$, as constructed in Lemma 5.4. For HD Büchi automata, which are equivalent to deterministic automata of quadratic size [KS15], there always exist polynomial resolvers: indeed, the letter game can be represented as a polynomial parity game, in which a positional strategy for Eve corresponds to a resolver. For HD coBüchi automata on the other hand, these auxiliary strategies might have exponential memory in the number of states of $\mathcal{A}$ [KS15].

The $G_k$ strategy on the other hand is positional for LimSup, since it can be encoded as a parity game directly on the $G_k(\mathcal{A})$ arena, similarly to the reduction in Theorem 5.10; the size of the $G_k(\mathcal{A})$ arena is $O(n^{k+1})$. The overall HD strategy for LimSup therefore needs memory exponential in the number of weights.

For LimInf on the other hand, by Theorems 5.1 and 5.11, the $G_k$ strategy can do with memory of size $n^{k-1} \cdot 3^{k^2}$. The overall HD strategy however needs memory exponential in both $n$ and $k$, due to strategies in the component coBüchi automata potentially requiring memory exponential in $n$.

For the Sup case, recall the LimSup automaton $\mathcal{A}'$, which has $k \cdot n$ states and $k$ weights, from the proof of Corollary 5.7, which is HD if and only if $\mathcal{A}$ is HD. From the same proof, an HD strategy in $\mathcal{A}'$ can be interpreted as an HD strategy in $\mathcal{A}$. Since $\mathcal{A}'$ is of polynomial size in $n$ and has as many weights as $\mathcal{A}$, $\mathcal{A}'$ has an HD strategy that has memory exponential in $k$, and therefore so does $\mathcal{A}$. If $k$ is in $O(\log n)$, then the memory is polynomial in $n$. $\square$

We leave open whether the memory bounds of Corollary 5.12 can be improved upon. Already for coBüchi automata, it is known that deciding whether an automaton is HD is polynomial despite there being automata for which the optimal HD strategy needs exponential memory. Hence, at least for the LimInf case, we cannot expect to do much better. However, for the Sup and LimSup cases, it might be that strategies with polynomial memory suffice.

Our proof does however imply that if a LimSup automaton $\mathcal{A}$ is HD, then there is a *finite memory* HD strategy, which implies that $\mathcal{A}$ is determinisable, without increasing the number of weights, by taking a product of $\mathcal{A}$ with the finite HD strategy. (Recall that every LimInf automaton can be determinised, while not every LimSup automaton can.)

**Corollary 5.13.** Every HD LimSup automaton is equivalent to a deterministic one with at most an exponential number of states and the same set of weights.

## 6. CONCLUSIONS

We have extended the token-game approach to characterising history-determinism from the Boolean (ω-regular) to the quantitative setting. Already 1-token games turn out to be useful for characterising history-determinism for some quantitative automata. For LimSup, LimInf and Sup automata on infinite words, one token is not enough, but the 2-token game does the trick. Given the correspondence between deciding history-determinism and the best-value
synthesis problem, our results also directly provide algorithms both to decide whether the synthesis problem is realisable and to compute a solution strategy.

This application further motivates understanding the limits of these techniques. Whether the 2-token game $G_2$ characterises more general Boolean classes of automata beyond Büchi and coBüchi automata is already an open question. Similarly, we leave open whether the $G_2$ game also characterises history-determinism for limit-average automata and other quantitative automata. At the moment we are not aware of examples of automata of any kind (quantitative, pushdown, register, timed, ...) for which Eve could win $G_2$ despite the automaton not being history-deterministic, yet even for parity automata, a proof of characterisation remains elusive.

The case of limit average automata is particularly interesting as it is a well-studied value-function. However, deciding the HDness of these automata presents some additional difficulties: first, the tokens games are less straight-forward to solve, as their winning conditions can no longer be encoded into parity conditions, as is the case for LimSup and LimInf; second, the characterisation of HDness is also likely to be challenging, as the techniques we have used here (present-focused value functions, decomposition into auxiliary automata) don't seem to apply.

## ACKNOWLEDGMENT

We thank Guillermo A. Pérez for discussing history-determinism of discounted-sum and limit-average automata.

## REFERENCES

[AKL10] Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. *ACM Trans. Algorithms*, 6(2):28:1–28:36, 2010. doi:10.1145/1721837.1721844.

[And06] Daniel Andersson. An improved algorithm for discounted payoff games. In *Proc. of ESSLLI Student Session*, pages 91–98, 2006.

[BH21] Udi Boker and Guy Hefetz. Discounted-sum automata with multiple discount factors. In *Proceedings of CSL*, pages 12:1–12:23, 2021. doi:10.4230/LIPIcs.CSL.2021.12.

[BK18] Marc Bagnol and Denis Kuperberg. Büchi good-for-games automata are efficiently recognizable. In *Proceedings of FSTTCS*, 2018. doi:10.4230/LIPIcs.FSTTCS.2018.16.

[BKLS20] Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michal Skrzypczak. On succinctness and recognisability of alternating good-for-games automata. *arXiv preprint arXiv:2002.07278*, 2020.

[BKS17] Udi Boker, Orna Kupferman, and Michal Skrzypczak. How deterministic are good-for-games automata? In *Proceedings of FSTTCS*, pages 18:1–18:14, 2017. doi:10.4230/LIPIcs.FSTTCS.2017.18.

[BL19] Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. volume 140 of *LIPIcs*, pages 19:1–19:16, 2019. doi:10.4230/LIPIcs.CONCUR.2019.19.

[BL21] Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata. In *Proc. of FSTTCS*, pages 35:1–35:20, 2021. doi:10.4230/LIPIcs.FSTTCS.2021.38.

[BL22] Udi Boker and Karoliina Lehtinen. Token games and history-deterministic quantitative automata. In *FOSSACS*, pages 120–139, 2022. doi:10.1007/978-3-030-99253-8\_7.

[Bok18] Udi Boker. Why these automata types? In *Proceedings of LPAR*, pages 143–163, 2018. doi:10.29007/c3bj.

[Bok21] Udi Boker. Quantitative vs. weighted automata. In *Proc. of Reachbility Problems*, pages 1–16, 2021. doi:10.1007/978-3-030-89716-1\_1.

[CDH10] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. *ACM Trans. Comput. Log.*, 11(4):23:1–23:38, 2010. doi:10.1145/1805950.1805953.
[CF19] Thomas Colcombet and Nathanaël Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In Proc. of FOSSACS, 2019. doi:10.1007/978-3-030-17127-8\_1.

[CH12] Krishnendu Chatterjee and Monika Henzinger. An $O(n^2)$ time algorithm for alternating Büchi games. In Proceedings of ACM-SIAM symposium on Discrete Algorithms, pages 1386–1399. SIAM, 2012. doi:10.1137/1.9781611973099.109.

[CJK$^+$17] Cristian S Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasiprogenomial time. In Proceedings of STOC, pages 252–263, 2017. doi: 10.1145/3055399.3055409.

[Col09] Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Proceedings of ICALP, pages 139–150, 2009. doi:10.1007/978-3-642-02930-1\_12.

[FJL$^+$17] Emmanuel Filiot, Ismaël Jecker, Nathan Lhote, Guillermo A. Pérez, and Jean-François Raskin. On delay and regret determinization of max-plus automata. In LICS, pages 1–12, 2017. doi: 10.1109/LICS.2017.8005096.

[FLW20] Emmanuel Filiot, Christof Löding, and Sarah Winter. Synthesis from weighted specifications with partial domains over finite words. In Proceedings of FSTTCS, 2020. doi:10.4230/LIPIcs.FSTTCS.2020.46.

[GJLZ21] Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A bit of non-determinism makes pushdown automata expressive and succinct. pages 53:1–53:20, 2021. doi: 10.4230/LIPIcs.MFCS.2021.53.

[HMS] Malte Helmert, Robert Mattmüller, and Sven Schewe. Selective approaches for solving weak games. In Susanne Graf and Wenhui Zhang, editors, Proceedings of ATVA. doi:10.1007/11901914\_17.

[HP06] Thomas Henzinger and Nir Piterman. Solving games without determinization. In Proceedings of CSL, pages 395–410, 2006. doi:10.1007/11874683\_26.

[HPR16] Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Minimizing regret in discounted-sum games. In Jean-Marc Talbot and Laurent Regnier, editors, CSL, volume 62 of LIPIcs, pages 30:1–30:17, 2016. doi:10.4230/LIPIcs.CSL.2016.30.

[HPR17] Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive synthesis without regret. Acta Informatica, 54(1):3–39, 2017. doi:10.1007/s00236-021-00410-0.

[KS15] Denis Kuperberg and Michal Skrzypczak. On determinisation of good-for-games automata. In Proceedings of ICALP, pages 299–310, 2015.

[LR13] Christof Löding and Stefan Repke. Decidability results on the existence of lookahead delegators for NFA. In Proc. of FSTTCS 2013, pages 327–338, 2013. doi:10.4230/LIPIcs.FSTTCS.2013.327.

[LZ22] Karoliina Lehtinen and Martin Zimmermann. Good-for-games $\omega$-pushdown automata. volume 18, 2022. doi:10.46298/lmcs-18(1:3)2022.

[MK19] Anirban Majumdar and Denis Kuperberg. Computing the width of non-deterministic automata. Logical Methods in Computer Science, 15, 2019. doi:10.23638/LMCS-15(4:10)2019.

[Sha53] L. S. Shapley. Stochastic games. In Proc. of Nat. Acad. Sci., volume 39, pages 1095–1100, 1953.

[ZP95] Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. Electron. Colloquium Comput. Complex., 2(40), 1995. doi:10.1016/0304-3975(95)00188-3.