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

HAL
open science

# Token Games and History-Deterministic Quantitative Automata

Udi Boker, Karoliina Lehtinen

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

## To cite this version:

Udi Boker, Karoliina Lehtinen. Token Games and History-Deterministic Quantitative Automata. FoSSaCS, 2022, Munich, Germany. pp.120-139, 10.1007/978-3-030-99253-8_7. hal-03857930

HAL Id: hal-03857930

https://hal.science/hal-03857930

Submitted on 17 Nov 2022

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.
# Token Games and History-Deterministic Quantitative Automata

Udi Boker¹ and Karoliina Lehtinen²

¹ Reichman University, Herzliya, Israel

² CNRS, Marseille-Aix Université, Université de Toulon, 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 might involve an exponential procedure, or even be undecidable, for example for 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 $\omega$-regular automata. We extend token games to the quantitative setting and analyze their potential to help deciding HDness for 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) automata on infinite words, and that 2-token games characterise HDness of LimInf and LimSup automata. Using these characterisations, we provide solutions to the HDness problem of Inf and Sup automata on finite words in PTIME, for DSum automata on finite and infinite words in NP∩CO-NP, for LimSup automata in quasip polynomial time, and for LimInf automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.

**Keywords:** Automata, History-determinism, Token games, Synthesis

## 1 Introduction

*History-determinism.* A nondeterministic [quantitative] automaton is history-deterministic (HD) [11,8] if its nondeterministic choices can be resolved by only considering the word read so far, uniformly across possible suffixes (see Fig. 2 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 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 [16,11,17,18,12,15,8], 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
[19], and HD pushdown automata are both more expressive and at least exponen-
tially more succinct than deterministic ones [20,15]. In the (ω-)regular setting,
history-determinism coincides with good-for-gameness [7], while in the quantita-
tive setting it is stronger [8]. The problem of deciding whether a nondeterministic
automaton is HD is interreducible with deciding the best-value synthesis problem
of a deterministic automaton [14,8]. 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 simple winning condition and
whose arena is the product of $\mathcal{A}$ and $\mathcal{D}$ [16]. 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 [7,8], is also difficult, as it
requires reasoning about composition with all possible games.

*Token games – a possible aid.* In [3], Bagnol and Kuperberg introduced token
games on $\omega$-regular automata, which are closely related to the letter game, but
easier to decide. 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 is that either all runs built by Adam
are rejecting, or Eve's run is accepting. Such games, as they compare concrete
runs, are easier to solve than the letter game.

Then, to decide HDness for 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 [3] that on Büchi automata, the letter game and the 2-token game always have the same winner, and in [6], 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 [3, 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 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 history-determinism for all quantitative (and Boolean) automata on finite words, and for discounted-sum (DSum) automata on infinite words. This results in a PTIME decision procedure for checking HDness of Inf and Sup automata on finite words, and an NP$\cap$CONP procedure for DSum automata on finite and infinite words. Note that the complexity for DSum automata on finite words was already known [14], but on infinite words it was erroneously believed to be NP-hard [17, 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 3), which is in particular the case for all Val automata on finite words [8, Lemma 16], as well as DSum automata on infinite words [8, Lemma 22].

We then show, in Section 5, that the 2-token game, in which Adam builds two runs, characterises history-determinism 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. 1.

We further present, in Section 5.1, algorithms to decide the winner of the two-token games on LimInf and LimSup automata via reductions to solving parity games. The complexity of the procedure for a LimSup automaton $A$ is the same as that of solving a parity game of size polynomial in the size of $A$ with twice as many priorities as there are weights in $A$, which is in quasip polynomial time. For LimInf automata the procedure is in exponential time. In both cases, it is only in polynomial time if the number of weights is logarithmic in the automaton size.

For some variants of the synthesis problem, the complexity of the witness of history-determinism is also of particular interest (while for other variants it is not), as it corresponds to the complexity of the implementation of the solution system [8, Section 5]. We give an exponential upper bound to the complexity of the witness for LimSup and LimInf automata, which, for LimInf, is tight. As a
corollary, we obtain that HD LimSup automata are 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), [16, 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 [3]. The coBüchi case is also resolved in PTIME, originally via an indirect usage of “joker games” [19], and later by using 2-token games [6].

In the quantitative setting, deciding HDness coincides with best-value partial domain synthesis [14], 0-regret synthesis [18] and, for some value functions, 0-regret determinisation [13,8]. 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 [1, Theorem 4.1], which provides a PTIME algorithm for checking whether such an automaton is “determinisable by pruning”, and [8, Theorem 21], which shows that such an automaton is HD if and only if it is determinisable by pruning.

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

For DSum automata on finite words, [14, Theorem 23] provides an NP$\cap$CO-NP solution, using a game that is quite similar to the one-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) 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.

*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 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. A game is determined if for every position, one of the players has a winning strategy.

**Quantitative Automata.** A nondeterministic quantitative<sup>3</sup> 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 nonempty set of states; $\iota \in Q$ is an initial state; and $\delta: Q \times \Sigma \to 2(\mathcal{Q} \times \mathcal{Q})$ is a transition function over weight-state pairs.

A transition is a tuple $(q, \sigma, x, q') \in Q \times \Sigma \times \mathcal{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. The size of an automaton consists of the maximum among the size of its alphabet, state-space, and transition-space.

*Value functions.*

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

$$ - \text{Sum}(v) = \sum_{i=0}^{n-1} v_i \qquad - \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:

$$ - \text{Inf}(v) = \inf\{v_n \mid n \ge 0\} \qquad - \text{Sup}(v) = \sup\{v_n \mid n \ge 0\} $$

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

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

$$ - \text{LimInf}(v) = \lim_{n \to \infty} \inf\{v_i \mid i \ge n\} \qquad - \text{LimSup}(v) = \lim_{n \to \infty} \sup\{v_i \mid i \ge n\} $$

*ω-regular automata* (with acceptance on transitions) can be viewed as special cases of quantitative automata. In particular, a Büchi (resp. coBüchi) automaton can be seen as a quantitative one, in which a rejecting transition has weight 0, an

<footnote n="3">³ We speak of “quantitative” rather than “weighted” automata, following the distinction made in [5] between the two.</footnote>
accepting transition has weight 1, and whose value function is 1 if the sequence of weighs has infinitely many 1's and 0 otherwise (resp. 1 if the sequence of weights has finitely many 0). See more on $\omega$-regular automata, e.g., in [4].

**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 1 (History-determinism [11,8]).** 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 as follows:

- Adam picks a letter $\sigma_i$ from $\Sigma$ and

- 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}$ over infinite words, Eve wins a play in the letter-game if $\text{Val}(\pi) \ge \mathcal{A}(w)$. For $\mathcal{A}$ over finite words, Eve wins if for all $i \in \mathbb{N}$, $\text{Val}(\pi[0..i]) \ge \mathcal{A}(w[0..i])$.

Consider for example the $\text{LimSup}$ automaton $\mathcal{A}$ in Fig. 2. 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 (Cautious strategies [8]).** 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 $\text{Val}(\rho\pi')$ is strictly greater than the value of $\text{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. 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 3 (Present-focused value functions [8]).** 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 [8, Remark 17], for example LimInf and LimSup.

**Proposition 2 ([8, Lemma 16]).** Every value function Val on finite sequences of rational values is present focused.

**Proposition 3 ([8, 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

Token games were introduced by Bagnol and Kuperberg [3] 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 [3, Corollary 21] and coBüchi [6, 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 4 (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. A play consists of an infinite sequence of configurations $(\iota, \iota, \dots, \iota) = (q_0, p_{1,0}, \dots, p_{k,0}), (q_1, p_{1,1}, \dots, p_{k,1}), \dots$. In a configuration $(q_i, p_{1,i}, \dots, p_{k,i})$, the game proceeds to the next configuration 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 con-
catenation of $\sigma_0, \sigma_1, \dots$, as well as $k+1$ infinite sequences $\pi$ (picked by Eve)
and $\pi_1 \dots \pi_k$ (picked by Adam) of transitions over $w$. 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) immediately extend to Eve's strategies in $G_k(\mathcal{A})$. Note that unlike in the letter game, a winning strategy in $G_k(\mathcal{A})$ must not necessarily be cautious, since Adam's run prefixes might not allow him to build an optimal run over the word witnessing that Eve's move was non-cautious.

## 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 [3, 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, Inf and Sup automata
on finite words and DSum automata on finite and infinite words.

**Theorem 1.** Given a nondeterministic automaton $\mathcal{A}$ with a present-focused value function $\text{Val}$ over 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 a 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 $\text{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$

**Corollary 1.** Given a nondeterministic automaton $\mathcal{A}$ over 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 complexity.
*Proof.* A direct consequence of Proposition 2 and Theorem 1. □

*Solving token games.* For resolving the HDness problem of Val automata where Val is present-focused, it then remains to study for which of them the corresponding $G_1$ game is simple to decide.

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

*Proof.* Given a Sup automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$ with weights $W$, $G_1(\mathcal{A})$ reduces to solving a safety game, whose positions $(\sigma, q, q', x_E, t) \in \Sigma \cup \{\varepsilon\} \times Q^2 \times W \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, a weight $x_E$ from $W$, which keeps track of the maximal weight seen on Eve's run so far, 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, m, L)$ where $m$ is the minimal weight of $\mathcal{A}$. The moves and position ownership encode the permitted moves in $G_1(\mathcal{A})$ and update $x_E$ to reflect the maximal value of Eve's run. 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$.

The case of Inf automata is similar, except that instead of keeping Eve's maximal value along her run, we need to keep the minimal value along Adam's run in some variable $x_A$, and the safety condition for Eve is that her current value must always be at least as big as $x_A$ and Adam's next move. Since Adam plays after Eve in each round of the game, we also need to keep Eve's last value, thus having $3|\Sigma|n^2k^2$ positions. □

Next, we show that solving $G_1$ is in NP$\cap$CO-NP for DSum automata.

**Theorem 3.** *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$CO-NP$^4$.*

*Proof.* Consider a $\lambda$-DSum automaton $\mathcal{A} = (\Sigma, Q, \iota, \delta)$, where the weight of a transition $t$ is denoted by $\gamma(t)$. From Propositions 2 and 3 and Theorem 1, Eve wins $G_1(\mathcal{A})$ if and only if $\mathcal{A}$ is HD. It therefore suffices to show that solving $G_1(\mathcal{A})$ is NP$\cap$CO-NP. We achieve this by reducing solving $G_1(\mathcal{A})$ to solving a

<footnote n="4">⁴ It was already known for finite words [14]. It is perhaps surprising for infinite words, given the NP-hardness result in [17, Theorem 6]. In consultation with the authors, we have confirmed that there is an error in the hardness proof.</footnote>
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 2: 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...$ and $x'_0x'_1...$ 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)$, ..., 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})$. The arena has positions in $(\sigma, q, q', t, m) \in \Sigma \cup \{\varepsilon\} \times Q^2 \times \delta \cup \{\varepsilon\} \times \{L, E, A\}$ where $\sigma$ is the potentially empty last played letter, starting with $\varepsilon$, the states $q, q'$ represent the positions of Eve and Adam's tokens, $t$ is the transition just played by Eve if $m = A$ and $\varepsilon$ otherwise, and $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.

A move of Adam that chooses a transition $t' = q' \xrightarrow{\sigma:x} q''$, namely a move $(\sigma, q, q', t, A) \to (\sigma, q, q'', \varepsilon, L)$, 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 [2] 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}$.

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} \left(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\right) = \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$CONP [2], solving $G_1(\mathcal{A})$, and therefore deciding whether $\mathcal{A}$ is HD, is also in NP$\cap$CONP. $\square$

DSum games are positionally determined [22,23,2] 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 [17, Section 5].

# 5 Deciding History-Determinism via Two Token Games

In this section we solve the HDness problem of LimSup and LimInf automata via two-token games. As is the case with Büchi and coBüchi automata, one-token games do not characterise HDness of LimSup and LimInf automata. For LimInf, a possible alternative approach is to try to solve the letter game directly: we can use an equivalent deterministic LimInf automaton to 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 LimInf automata is exponential in the number of its states [10, Theorem 13], so the new game is large, and, in addition, its winning condition, which compares the LimInf value of two runs, is non-standard and needs additional work to be encoded into a parity game. For LimSup automata the situation is even worse, as they are not necessarily equivalent to deterministic LimSup automata, so it is not obvious whether the winner of the letter game is decidable at all.

Here we show that the 2-token-game approach, used to resolve HDness of Büchi and coBüchi automata, can be generalised to LimSup and LimInf automata. While the proof that $G_2$ has the same winner as the letter game is quite different for the Büchi and coBüchi cases, our proofs for the LimSup and LimInf cases follow the same structure, while relying on the Büchi and coBüchi results respectively. However, the argument that $G_2(\mathcal{A})$ is solvable differs according to whether $\mathcal{A}$ is a LimSup or LimInf automaton. In particular, perhaps surprisingly (since the naive approach to solving the letter game seems harder for LimSup), we show that $G_2$ is solvable in quasip polynomial time for LimSup while for LimInf our algorithm is exponential in the number of weights (but not in the number of states).

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

We start, in Section 5.1, with analysing the 2-token game on LimSup and LimInf automata, and show, in Section 5.2, that it characterises their HDness.

## 5.1 $G_2$ on LimSup and LimInf Automata

We first observe that $G_2(\mathcal{A})$, for both a LimSup and a LimInf automaton $\mathcal{A}$, 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.
**Lemma 1.** Given a nondeterministic LimSup automaton $\mathcal{A}$ of size $n$ with $k$ weights, the game $G_2(\mathcal{A})$ can be solved in time quasip polynomial in $n$, and if $k$ is in $O(\log n)$, in time polynomial in $n$.

*Proof.* 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).

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 of weights. It can be solved in quasip polynomial time, or in polynomial time if the number of weights is in $O(\log n)$, using the reader's favourite state-of-the-art parity game algorithm, for instance [9].

□

**Lemma 2.** Given a nondeterministic LimInf automaton $\mathcal{A}$ of size $n$ with $k$ weights, the game $G_2(\mathcal{A})$ can be solved in time exponential in $n$, and if $k$ is in $O(\log n)$, in time polynomial in $n$.

*Proof.* As in the proof of Lemma 1, 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.

Intuitively, the weights on Eve's run will be encoded by *odd* priorities, with smaller weights corresponding to higher priorities, as in 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. This is the role of the memory structure, which encodes which of Adam's runs has seen which weight recently.

More precisely, let $k$ be the number of weights in $\mathcal{A}$. Moves corresponding to Eve choosing a transition of 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, 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 takes a transition with a weight $w \le i$ on one of Adam's
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 Adam's second (resp. first) run takes a transition with weight $w \le i$, then $x_i$ is reset to 0. Transitions 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 transitions have priority 1. Other moves do not affect $x_i$, and have priority 1.

We now argue that the highest priority seen infinitely often along a play is even if and only if the 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 exponential in $k$ 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 [9]. If the number of weights is in $O(\log n)$, then the algorithm is polynomial in the size $n$ of $\mathcal{A}$. $\square$

## 5.2 $G_2$ Characterises HDness for LimSup and LimInf Automata

The rest of the section is dedicated to proving that a LimSup or LimInf automaton is HD if and only if Eve wins the 2-token game on it. In both 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, also known as the width of an automaton [21], 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). 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 [3,6]. The main novelty in the argument is the decomposition of the LimSup (LimInf) automaton $\mathcal{A}$ with $k$ weights into $k-1$ Büchi (coBüchi) automata $A_2, \dots, A_k$ 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. 2.) The HD strategies for $A_2, \dots, A_k$ can then be combined to prove the $k$-HDness of $\mathcal{A}$.

Fig. 1 illustrates the flow of our arguments.

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$ [3, Thm 14].

**Theorem 4.** 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_3.png" /><figcaption>Fig. 1. 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_4.png" /><figcaption>Fig. 2. A LimSup automaton $\mathcal{A}$ and corresponding Büchi automata $A_2$ and $A_3$, as per Lemma 3. (Accepting transitions in $A_2$ and $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 $A_2$ and $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 $A_2$ Eve goes from $s_0$ to $s_1$ and in $A_3$ from $s_0$ to $s_2$.)</figcaption></figure>

*Proof.* This is the generalisation of [3, 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 Adma'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, also known as width [21], 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 (k-HD and k-runs letter game).** A configuration of the game on a LimSup (LimInf) 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 to the next configuration $(q_{i+1,1}, \dots, q_{i+1,k})$ as follows.

- 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 1) is a 1-run letter game and standard HD (Definition 1) is 1-HD.

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

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

*Proof.* The argument is identical to the one used in [3], 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 $\text{Val}(w)$; then her strategy $s_k$ guarantees that her run also achieves $\text{Val}(w)$. $\square$

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

Given a $\text{LimSup}$ automaton $\mathcal{A}$, with weights $\{1, \dots, k\}$, we define $k-1$ auxiliary Büchi automata $\mathcal{A}_2, \dots, \mathcal{A}_k$ with acceptance on transitions, such that each $\mathcal{A}_x$ is a copy of $\mathcal{A}$, where a transition is accepting if its weight $i$ in $\mathcal{A}$ is at least $x$. Each $\mathcal{A}_x$ recognises the set of words $w$ such that $\mathcal{A}(w) \ge x$. (See Fig. 2.)

Given a $\text{LimInf}$ automaton $\mathcal{A}$, we similarly define auxiliary coBüchi automata: $\mathcal{A}_x$ is a copy of $\mathcal{A}$ where transitions with weights smaller than $x$ are rejecting, while those with weights $x$ or larger are accepting. Again, $\mathcal{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 $\text{HD}_{k-1}(\mathcal{A})$.

**Lemma 3.** Given a $\text{LimSup}$ or $\text{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(\mathcal{A}_x)$.

*Proof.* Since $\mathcal{A}_x$ is identical to $\mathcal{A}$ except for the acceptance condition or value function, Eve can use in $G_2(\mathcal{A}_x)$ her winning strategy in $G_2(\mathcal{A})$. For the $\text{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(\mathcal{A}_x)$.

Similarly, for the $\text{LimInf}$ case, if one of Adam's runs avoids seeing a rejecting transition infinitely often in $\mathcal{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 $\mathcal{A}_x$ infinitely often, and accepts. $\square$

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

*Proof.* From Lemma 3, if Eve wins $G_2(\mathcal{A})$, then for all $x \in \{2, \dots, k\}$, Eve also wins $G_2(\mathcal{A}_x)$. Since each $\mathcal{A}_x$ is a Büchi or coBüchi automaton, this implies that for all $x \in \{2, \dots, k\}$, the automaton $\mathcal{A}_x$ is HD [3,6], that is, there is a winning strategy $s_x$ for Eve in the letter game on each $\mathcal{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 $\text{Val}(w) = i$, this word is accepted by $\mathcal{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 $\mathcal{A}_i$ infinitely often for the $\text{LimSup}$ case, or eventually avoiding rejecting transitions in the $\text{LimInf}$ case. $\square$

Finally, we combine the $G_2$ and $\text{HD}_{k-1}$ strategies in $\mathcal{A}$ to show that $\mathcal{A}$ is HD.
**Theorem 5.** 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 3 and Lemma 4 she wins $\text{HD}_{k-1}(\mathcal{A})$, where $k$ is the number of weights in $\mathcal{A}$. By Theorem 4 she also wins $G_{k-1}(\mathcal{A})$ and, finally, by Proposition 4 we get that $\mathcal{A}$ is HD. $\square$

**Theorem 6.** Given a nondeterministic LimSup (resp. LimInf) automaton $\mathcal{A}$ of size $n$ with $k$ weights, the HDness problem of $\mathcal{A}$ can be solved in time quasipoly-nomial (resp. exponential) in $n$. In both cases, if $k$ is in $O(\log n)$, it can be solved in time polynomial in $n$.

*Proof.* It directly follows from Theorem 5 and Lemmas 1 and 2; the former reducing the HDness problem to solving $G_2(\mathcal{A})$, and the latter two showing that $G_2(\mathcal{A})$ can be solved in the stated complexity. $\square$

In contrast to the cases considered in the Section 4, where strategies in $G_1$ immediately induce HD strategies of the same complexity, for Büchi and coBüchi automata, a winning $G_2$ strategy does not necessarily induce an HD strategy (even though 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 LimSup automata.

**Corollary 2.** Given an HD LimSup or LimInf automaton $\mathcal{A}$ of size $n$, there is an HD strategy for $\mathcal{A}$ with memory exponential in $n$. If $\mathcal{A}$ is a LimSup automaton with $O(\log n)$ weights then the memory is only polynomial in $n$.

*Proof.* Let $n$ be the size of $\mathcal{A}$ and $k+1$ the number of weights. We construct an HD strategy for $\mathcal{A}$, by combining an $\text{HD}_k$ strategy and a $G_k$ strategy for it.

The $\text{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 3. For HD Büchi automata, which are equivalent to deterministic automata of quadratic size [19], there always exists a polynomial resolver: 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}$ [19].

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 Lemma 1; 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 Lemma 2 and Theorem 4, the $G_k$ strategy can do with memory of size $n^{k-1} \cdot 3^{k^2}$. The overall HD strategy therefore has memory exponential in the size of $\mathcal{A}$. $\square$

We leave open whether this 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 is exponential. Hence, at least for the LimInf case, we cannot expect to do much better. However, for the LimSup case, it might be that polynomial, or even positional HD strategies could suffice. However, positionality is already open for the Büchi case.

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 3.** 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 ($\omega$-regular) to the quantitative setting. Already 1-token games turn out to be useful for characterising history-determinism for some quantitative automata. For LimSup and LimInf automata, 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.

# Acknowledgments

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

# References

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

2. Daniel Andersson. An improved algorithm for discounted payoff games. In *Proc. of ESSLLI Student Session*, pages 91–98, 2006.
3. Marc Bagnol and Denis Kuperberg. Büchi good-for-games automata are efficiently recognizable. In *38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)*, page 16, 2018.

4. Udi Boker. Why these automata types? In *Proceedings of LPAR*, pages 143–163, 2018.

5. Udi Boker. Quantitative vs. weighted automata. In *Proc. of Reachbility Problems*, pages 1–16, 2021.

6. Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On succinctness and recognisability of alternating good-for-games automata. *arXiv preprint arXiv:2002.07278*, 2020.

7. Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. In *Proceedings of CONCUR*, volume 140 of *LIPIcs*, pages 19:1–19:16, 2019.

8. Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata. In *Proc. of FSTTCS*, pages 35:1–35:20, 2021.

9. Cristian S Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasip polynomial time. In *Proceedings of STOC*, pages 252–263, 2017.

10. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. *ACM Trans. Comput. Log.*, 11(4):23:1–23:38, 2010.

11. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In *Proceedings of ICALP*, pages 139–150, 2009.

12. Thomas Colcombet and Nathanaël Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In *Proc. of FOSSACS*, volume 11425 of *Lecture Notes in Computer Science*, pages 1–26. Springer, 2019.

13. 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.

14. Emmanuel Filiot, Christof Löding, and Sarah Winter. Synthesis from weighted specifications with partial domains over finite words. In Nitin Saxena and Sunil Simon, editors, *FSTTCS*, volume 182 of *LIPIcs*, pages 46:1–46:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.

15. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A bit of nondeterminism makes pushdown automata expressive and succinct. In *Proc. of MFCS*, pages 53:1–53:20, 2021.

16. Thomas Henzinger and Nir Piterman. Solving games without determinization. In *Proceedings of CSL*, pages 395–410, 2006.

17. 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.

18. Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive synthesis without regret. *Acta Informatica*, 54(1):3–39, 2017.

19. Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In *Proceedings of ICALP*, pages 299–310, 2015.

20. Karoliina Lehtinen and Martin Zimmermann. Good-for-games ρ-pushdown automata. In *LICS20*, pages 689–702, 2020.

21. Anirban Majumdar and Denis Kuperberg. Computing the width of non-deterministic automata. *Logical Methods in Computer Science*, 15, 2019.

22. L. S. Shapley. Stochastic games. In *Proc. of Nat. Acad. Sci.*, volume 39, pages 1095–1100, 1953.
23. Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. *Electron. Colloquium Comput. Complex.*, 2(40), 1995.

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

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