TOWER ACKERMANN EXPTIME 2-EXPTIME University of Warwick, Coventry,
<EMAIL_ADDRESS>Research Support Scheme from the
Department of Computer Science at the University of Warwick. University of
Warwick, Coventry, UK and
https://www.dcs.warwick.ac.uk/~mju/marcin.jurdzinski@warwick.ac.ukhttps://orcid.org/0000-0003-3640-8481
University of Warwick, Coventry, UK and
https://apitya.github.io/aditya.prakash@warwick.ac.ukhttps://orcid.org/0000-0002-2404-0707Chancellors’
International Scholarship from the University of Warwick. R. Acharya, M.
Jurdziński and A. Prakash [500]Theory of computation Automata over infinite
objects We acknowledge the Centre for Discrete Mathematics and Its
Applications (DIMAP) at the University of Warwick for partial support.

###### Acknowledgements.

We thank Denis Kuperberg for several insightful exchanges. We are grateful to
the reviewers for their feedback and suggestions on how to improve the paper.2
2 Conference of Very Important Things CVIT 2020 CVIT 2016 December 24–27, 2016
Little Whinging, United Kingdom 42 23

# Lookahead Games and Efficient Determinisation
of History-Deterministic Büchi Automata

Rohan Acharya  Marcin Jurdziński  Aditya Prakash

###### Abstract

Our main technical contribution is a polynomial-time determinisation procedure
for history-deterministic Büchi automata, which settles an open question of
Kuperberg and Skrzypczak, 2015. A key conceptual contribution is the lookahead
game, which is a variant of Bagnol and Kuperberg’s token game, in which Adam
is given a fixed lookahead. We prove that the lookahead game is equivalent to
the $1$-token game. This allows us to show that the $1$-token game
characterises history-determinism for semantically-deterministic Büchi
automata, which paves the way to our polynomial-time determinisation
procedure.

###### keywords:

History determinism, Good-for-games, Automata over infinite words, Games

###### category:

Track B: Automata, Logic, Semantics, and Theory of Programming

##  1 Introduction

History-deterministic (HD) automata are non-deterministic automata in which
the non-determinism can be resolved “on the fly”, based only on the prefix of
the word read so far [6, 15]. This concept can be formalised using the
history-determinism game (HD game), in which two players Adam and Eve make
alternating moves choosing letters and transitions, thus constructing a word
and a run of the automaton on it, respectively. Eve wins if the run is
accepting or if the word is not in the language, and hence Eve’s winning
strategy will successfully resolve non-determinism by constructing an
accepting run on the fly, for all words in the language. An automaton is then
defined to be history-deterministic if Eve has a winning strategy in the game.

Henzinger and Piterman [11] introduced HD automata because of their potential
to speed up key algorithmic tasks in verification and synthesis, such as
language containment and strategy synthesis. In language containment, we ask
whether all executions of an implementation $\mathcal{A}$ satisfy a
specification $\mathcal{H}$. If $\mathcal{H}$ is non-deterministic then the
problem is $\PSPACE$-hard, but if $\mathcal{H}$ is HD then it is more
tractable, because it amounts to checking that $\mathcal{H}$ simulates
$\mathcal{A}$, which can be done in polynomial time if the parity index of
$\mathcal{H}$ is fixed [8, Theorem 3] and in quasi-polynomial time otherwise
[18, Theorem 20]. Henzinger and Piterman introduced HD automata as good-for-
games automata because games whose winning conditions are represented by an HD
automaton can be solved efficiently without automaton determinisation [11,
Theorem 3.1], a well-known compuational bottleneck in synthesis.

###  1.1 Related work

Key questions studied for HD parity automata include recognising them, their
succinctness relative to deterministic automata, minimisation, and
determinisation.

##### Recognising History-Deterministic Automata via Games.

Kuperberg and Skrzypczak [14] gave a polynomial time algorithm to recognise HD
co-Büchi automata, and Bagnol and Kuperberg [2] gave a polynomial time
algorithm to recognise HD Büchi automata. These algorithms have been
conceptually unified by Boker, Kuperberg, Lehtinen, and Skrzypczak [4] to be
based on the $2$-token game introduced by Bagnol and Kuperberg [2], leading to
the $2$-token conjecture.

######  Conjecture 1.1 (The $2$-token conjecture [2, 4]).

A parity automaton is HD if and only if Eve wins the 2-token game on it.

Proving the $2$-token conjecture would imply that recognising HD parity
automata of fixed parity index can be done in polynomial time. In contrast,
the best upper bound currently known for the problem is $\EXPTIME$, dating
back to Henzinger and Piterman [11]. In the general case, when the parity
index is not fixed, a lower bound of $\NP$-hardness has been achieved only
very recently [18].

Bagnol and Kuperberg [2] introduced the $k$-token game as a tool to
characterise the conceptually more complex HD game. Like in the HD game, in
the $k$-token game for $k\geq 1$, two players Adam and Even make alternating
moves choosing letters and transitions, but in addition, in every round, after
Eve chooses a transition, Adam also chooses $k$ transitions. As a result, Adam
constructs a word and $k$ runs, Eve constructs a run, and Eve wins if her run
is accepting or all of Adam’s $k$ runs are rejecting. A key insight in Bagnol
and Kuperberg’s work [2] is that the $2$-token game is equivalent to the
$k$-token game for all $k\geq 2$.

######  Theorem 1.2 ([2]).

Eve wins the $2$-token game on a parity automaton if and only if for all
$k\geq 2$, Eve wins the $k$-token game on it.

Bagnol and Kuperberg’s proof that the $2$-token game characterises history-
determinism for Büchi automata exploits this insight, by showing that if Adam
wins the HD game on a Büchi automaton then he can win the $k$-token game for
some $k$ that is doubly-exponential in the size of the automaton, and hence
also the $2$-token game.

Boker et al. [4] have used an analogous, but more involved, argument to show
that the $2$-token game also characterises history-determinism for co-Büchi
automata, combining Theorem 1.2 with the algorithm of Kuperberg and Skrzypczak
[14] to recognise HD co-Büchi automata efficiently, which was based on the so-
called Joker game. The Joker game is similar to the $1$-token game but,
additionally, Adam has the power to (finitely many times) “play Joker” by
choosing a transition from Eve’s token instead of a transition from his token,
and Eve wins if her run is accepting, or Adam’s run is rejecting, or Adam has
played Joker infinitely many times.

Kuperberg and Skrzypczak’s algorithm uses Joker games in their polynomial time
algorithm to recognise HD co-Büchi automata, but to date, it was not known if
Joker games characterise history-determinism on co-Büchi or Büchi automata, or
on parity automata in general.

##### Succinctness and minimisation of HD automata.

Kuperberg and Skrzypczak [14] proved that HD co-Büchi automata are
exponentially more succinct than deterministic co-Büchi automata [14], which
is known to be tight [15, Theorem 4.1]. Abu Radi and Kupferman [1] showed that
transition-based HD co-Büchi automata can be minimised in polynomial time and
that they have canonicity. In contrast, minimisation of state-based HD Büchi
or HD co-Büchi automata is known to be $\NP$-complete [22, Theorem 1].
Minimisation of transition-based Büchi automata is easily seen to be in $\NP$,
but the exact complexity is open.

##### Determinisation of HD Büchi automata.

Kuperberg and Skrzypczak [14] also proved that every HD Büchi automaton with
$n$ states has an equivalent deterministic Büchi automaton with at most
$n^{2}$ states. However, it is not known if HD Büchi automata are strictly
more succinct than deterministic Büchi automata.

The determinisation procedure of Kuperberg and Skrzypczak for an HD Büchi
automaton $\mathcal{H}$ involves carefully analysing the simulation game
between $\mathcal{H}$ and an equivalent deterministic Büchi automaton of
exponential size. At a high level, the procedure iteratively modifies the
simulation game and the automaton $\mathcal{H}$, eventually yielding an
equivalent game of quadratic size, from which a deterministic Büchi automaton
of quadratic size can be extracted, but the procedure itself runs in
exponential time.

Kuperberg and Skrzypczak also gave a non-deterministic polynomial-time
procedure for determinisation of HD Büchi automata, which guesses a
deterministic Büchi automaton of quadratic size and then checks for language
equivalence [14, Theorem 10]. They left the exact complexity of
determinisation for HD Büchi automata open, in particular, the question of
whether HD Büchi automata can be determinised in polynomial time.

###  1.2 Our Contributions

  * •

We introduce the $k$-lookahead game, a variant of the $1$-token game, in which
Adam’s transition on his token is delayed by $k$ steps, thus giving him a
lookahead of $k$. We prove that the $1$-token game is equivalent to the
$k$-lookahead game.

######  Theorem A.

For every parity automaton $\mathcal{A}$, Eve wins the $1$-lookahead game on
$\mathcal{A}$ if and only if she wins the $k$-lookahead game on $\mathcal{A}$.

The $1$-token game is syntactically equivalent to the $1$-lookahead game. A
thus demonstrates that the $1$-token game is already quite powerful, and it is
analogous to Theorem 1.2 of Bagnol and Kuperberg.

  * •

With A as a key tool, we show that the $1$-token game characterises history-
determinism on semantically-deterministic Büchi automata. These are automata
in which, for every state, all transitions labelled by the same letter lead to
language-equivalent states [20].

######  Theorem B.

A semantically-deterministic Büchi automaton is history-determinsitic if and
only if Eve wins the $1$-token game on it.

A consequence of B is that Joker games characterise history-determinism on
Büchi automata (Theorem 4.9). Since Joker games have smaller arenas than
2-token games, this leads to a more efficient algorithm for recognising HD
Büchi automata (Lemma 4.10).

  * •

We give a parity automaton with priorities $1$, $2$, and $3$ on which Eve wins
the Joker game but that is not HD (Theorem 4.13). This implies that the Joker
game does not characterise history-determinism for parity automata and that B
does not extend to parity automata.

  * •

We give a polynomial time determinisation procedure for HD Büchi automata,
thus resolving an open question of Kuperberg and Skrzypczak [14].

######  Theorem C.

There is a polynomial-time procedure that converts every HD Büchi automaton
with $n$ states into an equivalent deterministic Büchi automaton with $n^{2}$
states.

Our determinisation procedure is inspired by that of Kuperberg and Skrzypczak
[14], but rather than working with the simulation game between the automaton
and a deterministic automaton of exponential size, thanks to B, we can work
with the $1$-token game instead. This results in an algorithm that is
conceptually simpler and that runs in polynomial time.

  * •

We also give a technique to reduce game-based characterisations of history-
determinism to universal automata (automata that accept all words). Hence to
prove the 1-token game characterisation of history-determinism for
semantically-deterministic (SD) Büchi automata, it suffices to prove it for
universal SD Büchi automata (Theorem 3.1). Likewise, to prove the $2$-token
conjecture for parity automata, it suffices to prove it for universal parity
automata (Theorem 3.4).

##  2 Preliminaries

We let $\mathbb{N}=\\{0,1,2,\cdots\\}$ to be the set of natural numbers. For
two natural numbers $i,j$ such that $i<j$, we write $[i,j]$ to denote the set
of integers $\\{i,i+1,\dots,j\\}$, and $[j]$ to denote $[0,j]$. An alphabet
$\Sigma$ is a finite set of letters. We use $\Sigma^{*}$ and $\Sigma^{\omega}$
to denote the set of words of finite and countably infinite length over
$\Sigma$, respectively. We also let $\varepsilon$ be the unique word of length
$0$. A language $\mathcal{L}\in\Sigma^{\omega}$ is a set of words. For a
finite word $u\in\Sigma^{*}$ and a language $\mathcal{L}$, we define
$u^{-1}\mathcal{L}$ to be $\\{w\mid uw\in\mathcal{L}\\}$.

###  2.1 Games

##### Game arenas.

An _arena_ is a directed graph $G=(V,E)$ with vertices partitioned into
$V_{\boldsymbol{\forall}}$ and $V_{\boldsymbol{\exists}}$ between two players
Adam and Eve, respectively. Additionally, a vertex $v_{0}\in
V_{\boldsymbol{\forall}}$ is designated as the initial vertex. We say that
vertices in $V_{\boldsymbol{\exists}}$ are owned by Eve and those in
$V_{\boldsymbol{\forall}}$ are owned by Adam.

A _play_ on this arena is an infinite path starting at $v_{0}$ and it is
formed as follows. A play starts with a token at $v_{0}$ and it proceeds for
infinitely many rounds. At each round, the player who owns the vertex on which
the token is currently placed chooses an outgoing edge, and the token is moved
along this edge to the next vertex for another round of play. This creates an
infinite path in the arena, which we call a play of $G$.

A _game_ $\mathcal{G}$ consists of an arena $G=(V,E)$ and a winning condition
given by a language $L\subseteq E^{\omega}$. We say that Eve _wins a play_
$\rho$ in $G$ if $\rho\in L$, and Adam wins otherwise. A _strategy_ for Eve in
such a game $\mathcal{G}$ is a function from the set of plays that end at an
Eve’s vertex to an outgoing edge from that vertex. Eve’s strategy is said to
be winning if any play produced while she plays according to this strategy is
winning for her. We say that Eve _wins the game_ if she has a winning
strategy. Winning strategies are defined for Adam analogously, and we say that
Adam wins the game if he has a winning strategy. In this paper we deal with
$\omega$-regular games, which are known to be determined [17, 10], i.e., each
game has a winner. Two games are _equivalent_ if they have the same winner.

##### Parity games.

An $[i,j]$-_parity game_ $\mathcal{G}$ is played over a finite game arena
$G=(V,E)$, with the edges of $G$ labelled by a priority function
$\chi:E\xrightarrow{}[i,j]$ for some $i,j\in\mathbb{N}$ with $i<j$, and $i=0$
or $i=1$. A play $\rho$ in the arena of $\mathcal{G}$ is winning for Eve if
and only if the highest edge priority that occurs infinitely often is even. It
is well known that parity games can be solved in polynomial time when the
interval $[i,j]$ is fixed, and in quasi-polynomial time otherwise [7, 13, 16].

###  2.2 Automata

##### Parity automata.

An $[i,j]$-_non-deterministic parity automaton_
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta)$ consists of a finite directed graph with
edges labelled by letters in $\Sigma$ and _priorities_ in $[i,j]$ for some
$i,j\in\mathbb{N}$ with $i<j$. These edges are called _transitions_ , which
are elements of the set $\Delta\subseteq Q\times\Sigma\times[i,j]\times Q$,
and the vertices of this graph are called _states_ , which are elements of the
set $Q$. Each automaton has a designated _initial state_ $q_{0}\in Q$. For
states $p,q\in Q$ and a letter $a\in\Sigma$, we use $p\xrightarrow{a:c}q$ to
denote a transition from $p$ to $q$ on the letter $a$ that has the priority
$c$.

A _run_ on an infinite word $w$ in $\Sigma^{\omega}$ is an infinite path in
the automaton, starting at the initial state and following transitions that
correspond to the letters of $w$ in sequence. We write that such a run is
_accepting_ if it _satisfies the parity condition_ , i.e., the highest
priority occurring infinitely often amongst the transitions of the run is
even, and a word $w$ in $\Sigma^{\omega}$ is accepting if the automaton has an
accepting run on $w$. The _language_ of an automaton $\mathcal{A}$, denoted by
$\mathcal{L}(\mathcal{A})$, is the set of words that it accepts. We write that
the automaton $\mathcal{A}$ _recognises_ a language $\mathcal{L}$ if
$\mathcal{L}(\mathcal{A})=\mathcal{L}$. A language
$\mathcal{L}\subseteq\Sigma^{\omega}$ is _$\omega$ -regular_ if it is
recognised by some parity automaton. A parity automaton $\mathcal{A}$ is said
to be _deterministic_ if for any given state in $\mathcal{A}$ and any given
letter in $\Sigma$, there is at most one outgoing transition from that state
on that letter.

We write that $[i,j]$, with $i=0$ or $1$, is the parity index of
$\mathcal{A}$. A _Büchi_ (resp. co-Büchi) automaton is a $[1,2]$ (resp.
$[0,1]$) parity automaton. A _safety automaton_ is one where all transitions
have priority $0$.

We write $(\mathcal{A},q)$ to denote the automaton $\mathcal{A}$ with $q$ as
it’s initial state, and $\mathcal{L}(\mathcal{A},q)$ to denote the language it
recognises. Two states $p$ and $q$ in $\mathcal{A}$ are _equivalent_ if
$\mathcal{L}(\mathcal{A},p)=\mathcal{L}(\mathcal{A},q)$.

##### History-determinism.

The (HD game) is a two player turn-based game between Adam and Eve, who take
alternating turns to select a letter and a transition in the automaton (on
that letter), respectively. After the game ends, the sequence of Adam’s
choices of letters is an infinite word, and the sequence of Eve’s choices of
transitions is a run on that word. Eve wins the game if her run is accepting
or Adam’s word is rejecting, and we say that an automaton is HD if Eve has a
winning strategy in the history-determinism game.

######  Definition 2.1 (History-determinism game).

Given a parity automaton $\mathcal{A}=(Q,\Sigma,q_{0},\Delta)$, the _history-
determinism game_ of $\mathcal{A}$ is defined between the players Adam and Eve
as follows, with positions in $Q$. The game starts at $q_{0}$ and proceeds for
infinitely many rounds. For each $i\in\mathbb{N}$, round $i$ starts at a
position $q_{i}\in Q$, and proceeds as follows:

  1. 1.

Adam selects a letter $a_{i}\in\Sigma$;

  2. 2.

Eve selects a transition $q_{i}\xrightarrow{a_{i}:c_{i}}q_{i+1}\in\Delta$.

The new position is $q_{i+1}$ from where round $(i+1)$ is played. Thus, the
play of a history-determinism game can be seen as Adam constructing a word
letter-by-letter, and Eve constructing a run transition-by-transition on the
same word. Eve wins such a play if the following holds: if Adam’s word is in
$\mathcal{L}(\mathcal{A})$, then Eve’s run is accepting.

If Eve wins the history-determinism game on $\mathcal{A}$, then we say that
$\mathcal{A}$ is _history-deterministic_.

##### Semantic-determinism.

Let $\mathcal{A}$ be a parity automaton. A transition $\delta$ from $p$ to $q$
on a letter $a$ in $\mathcal{A}$ is called _language-preserving_ if
$\mathcal{L}(\mathcal{A},q)=a^{-1}\mathcal{L}(\mathcal{A},p)$. We say that a
parity automaton is _semantically-deterministic_ , SD for short, if all
transitions in it are language-preserving. The following lemma can be shown by
a simple inductive argument on the length of words.

######  Lemma 2.2.

If a parity automaton is SD then all states in the automaton that can be
reached from a fixed state $q$ upon reading a finite word $u$ accept the
language $u^{-1}\mathcal{L}(\mathcal{A},q)$.

SD automata were introduced by Kuperberg and Skrzypczak as residual automata
[14]. We follow Abu Radi, Kupferman, and Leshkowitz [21] by calling them SD
automata instead.

###  2.3 Games on Automata

Simulation and simulation-like games (such as token games [2]) are fundamental
amongst the techniques we use in this paper. We define these games below.

##### Simulation and stepahead simulation.

######  Definition 2.3 (Simulation game).

Given two parity automata $\mathcal{A}=(P,\Sigma,p_{0},\Delta_{A})$ and
$\mathcal{B}=(Q,\Sigma,q_{0},\Delta_{B})$, the _simulation game_ between
$\mathcal{B}$ and $\mathcal{A}$ is a two player game played between Eve and
Adam as follows, with positions in $P\times Q$. The game starts at
$(p_{0},q_{0})$, and proceeds for infinitely many rounds. For each $i\geq 0$,
round $i$ starts at position $(p_{i},q_{i})$ and proceeds as follows:

  1. 1.

Adam selects a letter $a_{i}\in\Sigma$;

  2. 2.

Adam selects a transition $p_{i}\xrightarrow{a_{i}:c^{\prime}}p_{i+1}$ in
$\mathcal{A}$;

  3. 3.

Eve selects a transition $q_{i}\xrightarrow{a_{i}:c}q_{i+1}$ in $\mathcal{B}$.

At the end of a play of the simulation game, the letters selected by Adam in
sequence form a word, while the sequence of his selected transitions and the
sequence of Eve’s selected transitions form runs on that word in $\mathcal{A}$
and $\mathcal{B}$, respectively. We say Eve wins the game if her run in
$\mathcal{B}$ is accepting or Adam’s run in $\mathcal{A}$ is rejecting. If Eve
has a strategy to win the simulation game, then we say that $\mathcal{B}$
_simulates_ $\mathcal{A}$.

The _stepahead simulation_ game between $\mathcal{B}$ and $\mathcal{A}$ is
defined similarly to the simulation game, except the orders of move in each
round are changed as follows: Adam selects a letter first, then Eve selects a
transition on $\mathcal{B}$, and then Adam selects a transition on
$\mathcal{A}$. The winning condition is identical, which is that Eve’s run on
$\mathcal{B}$ is accepting if Adam’s run on $\mathcal{A}$ is accepting. If Eve
wins the stepahead simulation game between $\mathcal{B}$ and $\mathcal{A}$,
then we say that $\mathcal{B}$ _step-ahead simulates_ $\mathcal{A}$.

##### Token games.

$k$-token games are similar to stepahead simulation games, but are played on a
single automaton, and Adam constructs $k$ runs instead of one. The winning
objective of Eve requires her to construct an accepting run if one of $k$
Adam’s runs is accepting.

######  Definition 2.4 ($k$-token game).

The _$k$ -token game_ on a non-deterministic parity automaton
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta)$ is defined between the players Adam and
Eve as follows, with positions in $Q\times Q^{k}$. The game starts at
$(q_{0},(q_{0})^{k})$ and proceeds in $\omega$ many rounds. For each
$i\in\mathbb{N}$, the round $i$ starts at a position
$(q_{i},(p^{1}_{i},p^{2}_{i},\cdots,p^{k}_{i}))\in Q\times Q^{k}$, and
proceeds as follows.

  1. 1.

Adam selects a letter $a_{i}\in\Sigma$.

  2. 2.

Eve selects a transition $q_{i}\xrightarrow{a_{i}:c}q_{i+1}\in\Delta$.

  3. 3.

Adam selects $k$ transitions
$p^{1}_{i}\xrightarrow{a_{i}:c^{\prime}_{1}}p^{1}_{i+1},p^{2}_{i}\xrightarrow{a_{i}:c^{\prime}_{2}}p^{2}_{i+1},\cdots
p^{k}_{i}\xrightarrow{a_{i}:c^{\prime}_{k}}p^{k}_{i+1}\in\Delta$.

The new position is $(q_{i+1},(p^{1}_{i+1},p^{2}_{i+1},\cdots,p^{k}_{i+1}))$,
from where round $(i+1)$ begins.

Thus, in a play of the $k$-token game on $\mathcal{A}$, Eve constructs a run
and Adam $k$ runs, all on the same word. Eve wins such a play if the following
holds: if one of Adam’s $k$ runs is accepting, then Eve’s run is accepting.

Observe that the stepahead-simulation game between $\mathcal{A}$ and itself is
equivalent to the $1$-token game on $\mathcal{A}$.

##### Joker games.

_Joker games_ are defined similar to $1$-token games, but additionally in each
round, Adam can choose to play _Joker_ and choose a transition from Eve’s
position instead of a transition from his position. The winning condition for
Eve is the following: If Adam’s sequence of transitions satisfies the parity
conditions and Adam has played finitely many Jokers, then Eve’s run is
accepting as well.

######  Definition 2.5 (Joker games).

The _Joker game_ on a non-deterministic parity automaton
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta)$ is defined between the players Adam and
Eve as follows, with positions in $Q\times Qk$. The game starts at
$(q_{0},q_{0})$ and proceeds in $\omega$ many rounds. For each
$i\in\mathbb{N}$, the round $i$ starts at a position $(q_{i},p_{i})\in Q\times
Q$, and proceeds as follows.

  1. 1.

Adam selects a letter $a_{i}\in\Sigma$.

  2. 2.

Eve selects a transition $q_{i}\xrightarrow{a_{i}:c_{i}}q_{i+1}\in\Delta$

  3. 3.

Adam either selects a transitions
$p_{i}\xrightarrow{a_{i}:c^{\prime}_{i}}p_{i+1}$, or plays Joker and selects a
transition $q_{i}\xrightarrow{a_{i}:c_{i}}p^{\prime}_{i+1}$.

The new position is $(q_{i+1},p_{i+1})$, from where round $(i+1)$ begins.

Eve wins such a play if the following holds: if Adam plays finitely many
Jokers and his sequence of transitions satisfies the parity condition, then
Eve’s run is accepting.

The following observations are easy to see.

######  Lemma 2.6.

If $\mathcal{A}$ is an HD parity automaton, and if $\mathcal{B}$ is a parity
automaton such that
$\mathcal{L}(\mathcal{B})\subseteq\mathcal{L}(\mathcal{A})$, then we have:

  1. 1.

Eve wins the Joker game on $\mathcal{A}$ and the $k$-token game on
$\mathcal{A}$, for all $k\geq 1$;

  2. 2.

$\mathcal{A}$ simulates and step-ahead simulates $\mathcal{B}$.

######  Proof 2.7.

Fix a winning strategy $\sigma$ for Eve in the HD game of $\mathcal{A}$.
Consider the strategy for Eve in the above games, in which she follows
$\sigma$ based on the letters Adam chooses, ignoring the rest of his moves.
Then Eve constructs an accepting run whenever the word constructed by Adam is
accepting. In particular, if Adam constructs an accepting run in the $k$-token
game or the (stepahead) simulation game, then his word must be in
$\mathcal{L}(\mathcal{A})$, implying Eve’s run is accepting as well.

Similarly, in a play of the Joker game, suppose Adam plays finitely many
Jokers and his sequence of transitions satisfies the parity condition. Let $i$
be the last round where Adam played a Joker. Then there is an accepting run on
Adam’s word, which can be obtained by concatenating Eve’s run until round
$(i-1)$ with Adam’s run from round $i$. This implies that Adam’s word is in
$\mathcal{L}(\mathcal{A})$, once again implying that Eve’s run is accepting.

###  2.4 History-Deterministic Automata and Simulation

Let $\mathcal{L}$ be an $\omega$-regular language, and let
$\mathcal{F}_{\mathcal{L}}$ be the set of automata which recognise languages
that are subsets of $\mathcal{L}$, i.e.
$\mathcal{F}_{\mathcal{L}}=\\{\mathcal{A}\mid\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}\\}$.
Consider the relation $\preceq$ on $\mathcal{F}_{\mathcal{L}}$ defined as
$\mathcal{A}\preceq\mathcal{B}$ if $\mathcal{B}$ simulates $\mathcal{A}$.
Then, $\preceq$ is a _preorder_ :

  1. 1.

$\preceq$ is _transitive_ , i.e., $\mathcal{A}\preceq\mathcal{B}$ and
$\mathcal{B}\preceq\mathcal{C}$ implies $\mathcal{A}\preceq\mathcal{C}$,

  2. 2.

$\preceq$ is _reflexive_ , i.e., $\mathcal{A}\preceq\mathcal{A}$.

We call $\preceq$ the _simulation preorder_. Lemma 2.6 implies that any HD
automaton $\mathcal{H}$ which recognises $\mathcal{L}$ is a _greatest_ element
in $\mathcal{F}_{\mathcal{L}}$ with respect to the simulation preorder, i.e.,
$\mathcal{A}\preceq\mathcal{H}$ for all $\mathcal{A}$ with
$\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}(\mathcal{H})$. We show that the
converse also holds.

######  Lemma 2.8.

Let $\mathcal{L}$ be an $\omega$-regular language, and let
$\mathcal{F}_{\mathcal{L}}=\\{\mathcal{A}\mid\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}\\}$.
Then, an automaton $\mathcal{H}$ in $\mathcal{F}_{\mathcal{L}}$ is greatest
w.r.t. the simulation preorder if and only if $\mathcal{H}$ recognises
$\mathcal{L}$ and is history-deterministic.

######  Proof 2.9.

We only need to prove the forward implication, since the backward implication
follows from Lemma 2.6. Let $\mathcal{H}$ in $\mathcal{F}_{\mathcal{L}}$ be
such that $\mathcal{A}\preceq\mathcal{H}$ for all $\mathcal{A}$ with
$\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}$. Fix $\mathcal{D}$ to be a
deterministic parity automaton which recognises $\mathcal{L}$ (such a
$\mathcal{D}$ always exists, see [9, Theorem 1.19 and 3.11]). Then, in
particular, $\mathcal{D}\preceq\mathcal{H}$. Observe that this implies
$\mathcal{L}(\mathcal{H})\supseteq\mathcal{L}(\mathcal{D})=\mathcal{L}$, and
since $\mathcal{L}(\mathcal{H})\subseteq\mathcal{L}$, we get that
$\mathcal{L}(\mathcal{H})=\mathcal{L}$.

We proceed to show that Eve wins the HD game on $\mathcal{H}$. Fix $\sigma$ to
be a winning strategy for Eve in the simulation game between $\mathcal{H}$ and
$\mathcal{D}$. We use $\sigma$ to construct a winning strategy in the HD game
on $\mathcal{H}$ as follows. Eve during the letter game on $\mathcal{H}$ keeps
a corresponding play of the simulation game between $\mathcal{H}$ and
$\mathcal{D}$, where Adam is playing the same letters as the HD game and
choosing the unique transitions available to him. Eve then chooses transitions
according to $\sigma$ in the HD game and in the simulation game in her memory.
This way, whenever Adam’s word $w$ in the HD game is in
$\mathcal{L}(\mathcal{H})=\mathcal{L}$, then the unique run in $\mathcal{D}$
on $w$ is accepting, and hence, Eve’s run in the HD game on $\mathcal{H}$ must
be accepting as well.

We make explicit a corollary of the above lemma.

######  Corollary 2.10.

If a nondeterministic parity automaton $\mathcal{A}$ simulates a language-
equivalent history-deterministic automaton $\mathcal{H}$, then $\mathcal{A}$
is history-deterministic.

######  Proof 2.11.

Let $\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{H})=\mathcal{L}$. From
Lemma 2.8, we know that $\mathcal{H}$ is a greatest element in
$\mathcal{F}_{\mathcal{L}}$, and $\mathcal{H}\preceq\mathcal{A}$ implies that
$\mathcal{A}$ is a greatest element in $\mathcal{F}_{\mathcal{L}}$ as well. It
follows from Lemma 2.8 that $\mathcal{A}$ is history-deterministic.

##  3 Sufficient to think about Universal Automata

In the next section, we will show that $1$-token games characterise history-
determinism on semantically-deterministic Büchi automata (B). In order to show
this, we start by reducing this result to the restriction where our automata
are universal (Theorem 3.1), i.e., recognise all words in the language. A very
similar reduction also shows that proving the $2$-token conjecture for
universal parity is sufficient to conclude the $2$-token conjecture for parity
automata (Theorem 4.9).

######  Theorem 3.1.

The following statements are equivalent:

  1. 1.

For any semantically-deterministic Büchi automaton $\mathcal{A}$, Eve wins the
1-token game on $\mathcal{A}$ if and only if $\mathcal{A}$ is history-
deterministic.

  2. 2.

For any semantically-deterministic Büchi automaton $\mathcal{U}$ with
$\mathcal{L}(\mathcal{U})=\Sigma^{\omega}$, Eve wins the 1-token game on
$\mathcal{U}$ if and only if $\mathcal{U}$ is history-deterministic.

We shall use the following fact shown by Boker, Henzinger, Lehtinen, and
Prakash to prove Theorem 3.1 [3].

######  Lemma 3.2 ([3]).

A non-deterministic parity automaton $\mathcal{A}$ is history-deterministic if
and only if it simulates all deterministic safety automata $\mathcal{S}$ with
$\mathcal{L}(\mathcal{S})\subseteq\mathcal{L}(\mathcal{A})$.

For self-containment, we include a proof of Lemma 3.2 in the appendix. We now
prove Theorem 3.1.

######  Proof 3.3 (Proof sketch for Theorem 3.1).

It is clear that 1 implies 2. For the other direction, suppose 2 holds. Let
$\mathcal{A}$ be a semantically-deterministic automaton that is not HD. We
will show that Adam wins the $1$-token game on $\mathcal{A}$.

From Lemma 3.2, we know that there is a deterministic safety automaton
$\mathcal{S}$ such that $\mathcal{A}$ does not simulate $\mathcal{S}$ and
$\mathcal{L}(\mathcal{S})\subseteq\mathcal{L}(\mathcal{A})$. Consider the
product safety automaton $\mathcal{P}$ of $\mathcal{S}$ and $\mathcal{A}$
which recognises the language
$\mathcal{L}(\mathcal{P})=\mathcal{L}(\mathcal{S})$. We then complete
$\mathcal{P}$ by adding an accepting sink state $f$, and transitions to $f$
from all states $q$ on letters $a$ such that $q$ did not have an outgoing
transition on $a$ in $\mathcal{P}$. We call this automaton $\mathcal{U}$. It
is clear that $\mathcal{L}(\mathcal{U},p)=\Sigma^{\omega}$ for all states $p$
in $\mathcal{U}$, and hence $\mathcal{U}$ is SD. We show that Adam wins the HD
game on $\mathcal{U}$, by using his winning strategy in the simulation game
between $\mathcal{A}$ and $\mathcal{S}$ (recall that $\mathcal{P}$ was
constructed by taking product of $\mathcal{S}$ and $\mathcal{A}$). The
hypothesis implies that Adam wins the $1$-token game on $\mathcal{U}$. We then
show that we can adapt a winning strategy for Adam on $1$-token game of
$\mathcal{U}$ to one for the $1$-token game on $\mathcal{A}$, by simply
‘projecting’ his strategy to the $\mathcal{A}$ component: note that since
$\mathcal{S}$ is deterministic, in plays of the $1$-token game on
$\mathcal{U}$, Eve’s and Adam’s states have the same $\mathcal{S}$-component
at the start of each round.

An almost word-by-word identical proof to above also shows that the $2$-token
conjecture can be reduced to the case where the automata are universal.

######  Theorem 3.4.

The following statements are equivalent:

  1. 1.

For any non-deterministic parity automaton $\mathcal{A}$, Eve wins the 2-token
game on $\mathcal{A}$ if and only if $\mathcal{A}$ is history-deterministic.

  2. 2.

For any non-deterministic parity automaton $\mathcal{U}$ with
$\mathcal{L}(\mathcal{U})=\Sigma^{\omega}$, Eve wins the 2-token game on
$\mathcal{U}$ if and only if $\mathcal{U}$ is history-deterministic.

##  4 When 1-Token Game is Enough

In this section, we will show the following result.

See B

Towards this, we first introduce $k$-lookahead games, which are variants of
1-token games where Adam is given a lookahead of $k$.

###  4.1 Lookahead Games

Let us briefly recall how a round of the $1$-token game on a parity automaton
$\mathcal{A}$ works. In each round, Adam selects a letter, then Eve selects a
transition on that letter on her token, and then Adam selects a transition on
that letter on his token. The winning condition for Eve is that at the end of
the play, either Eve’s run is accepting or Adam’s run is rejecting. This is
very close to the simulation game between $\mathcal{A}$ and itself, except
that the order of the moves in which Eve and Adam select transitions has been
reversed. One can, however, see the $1$-token game as a simulation game, where
Adam picks the transition for round $i$ in round ($i+1$). Or equivalently, we
can construct an automaton ${\mathsf{Delay}}(\mathcal{A})$ such that any non-
determinism on $\mathcal{A}$ is ‘delayed’ by one step, and then the $1$-token
game on $\mathcal{A}$ is equivalent to the simulation game between
$\mathcal{A}$ and ${\mathsf{Delay}}(\mathcal{A})$. This insight was used by
Prakash and Thejaswini to give an algorithm for deciding history-determinism
of one-counter nets, by reducing the $1$-token game to a simulation game [19].
Below we give a construction ${\mathsf{Delay}}$ on parity automata that delays
the non-determinism by one-step, inspired by a similar construction for one-
counter nets [19, Lemma 11].

######  Definition 4.1.

For any non-deterministic parity automaton
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta)$, the automaton
${\mathsf{Delay}}(\mathcal{A})$ is constructed so that it runs ‘one letter
behind’ $\mathcal{A}$, by storing a letter in its state space. More formally,
${\mathsf{Delay}}(\mathcal{A})=(Q^{\prime},\Sigma,s,\Delta^{\prime})$, where
$Q^{\prime}=Q\times\Sigma\cup\\{s\\}$, and $s$ is the initial state. The set
of transitions $\Delta^{\prime}$ is the union of the following sets of
transitions.

  1. 1.

$\\{(s\xrightarrow{a:0}(q_{0},a))\mid a\in\Sigma\\}$.

  2. 2.

$\\{((p,a)\xrightarrow{a^{\prime}:c}(q,a^{\prime}))\mid\
(p\xrightarrow{a:c}q)\in\Delta\\}$.

Observe that ${\mathsf{Delay}}(\mathcal{A})$ accepts the same language as
$\mathcal{A}$. The following lemma is easy to prove, since the expanded game
arenas of the $1$-token game on $\mathcal{A}$, and the simulation game between
$\mathcal{A}$ and ${\mathsf{Delay}}(\mathcal{A})$ are equivalent, with
identical winning conditions.

######  Lemma 4.2.

For every non-deterministic parity automaton $\mathcal{A}$, Eve wins the
$1$-token game on $\mathcal{A}$ if and only if $\mathcal{A}$ simulates
${\mathsf{Delay}}(\mathcal{A})$.

Furthermore, we can also show that Eve wins the $1$-token game on
${\mathsf{Delay}}(\mathcal{A})$ if Eve wins the $1$-token game on
$\mathcal{A}$, by simply ‘delaying’ her winning strategy in the $1$-token game
on $\mathcal{A}$.

######  Lemma 4.3.

If Eve wins the $1$-token game on an automaton $\mathcal{A}$, then Eve wins
the $1$-token game on ${\mathsf{Delay}}(\mathcal{A})$.

An iterative application of Lemmas 4.2 and 4.3 gives us the following
corollary.

######  Corollary 4.4.

If Eve wins the $1$-token game on a parity automaton $\mathcal{A}$, then
$\mathcal{A}$ simulates ${\mathsf{Delay}}^{k}(\mathcal{A})$ for all
$k\in\mathbb{N}$.

######  Proof 4.5.

Note that simulation relation is transitive, i.e., if $\mathcal{A}_{0}$
simulates $\mathcal{A}_{1}$ and $\mathcal{A}_{1}$ simulates $\mathcal{A}_{2}$,
then $\mathcal{A}_{0}$ simulates $\mathcal{A}_{2}$. Suppose Eve wins the
$1$-token game on $\mathcal{A}$. From Lemma 4.3, induction gives us that Eve
wins the 1-token game on ${\mathsf{Delay}}^{k}(\mathcal{A})$ for all
$k\in\mathbb{N}$. From Lemma 4.2, we see that
${\mathsf{Delay}}^{k}(\mathcal{A})$ simulates
${\mathsf{Delay}}^{k+1}(\mathcal{A})$ for all $k\in\mathbb{N}$. Combining this
with transitivity of simulation, we get that $\mathcal{A}$ simulates
${\mathsf{Delay}}^{k}(\mathcal{A})$ for all $k\in\mathbb{N}$.

Call the simulation game between $\mathcal{A}$ and
${\mathsf{Delay}}^{k}(\mathcal{A})$ as the _$k$ -lookahead game_ on
$\mathcal{A}$. Note that the $1$-token game of $\mathcal{A}$ is then
equivalent to the $1$-lookahead game of $\mathcal{A}$. Corollary 4.4 can thus
be restated as the following theorem.

See A

###  4.2 Games to Characterise History-Determinism

We now proceed to show B. From Theorem 3.1, we know that it suffices to only
consider SD Büchi automata that are universal. The following lemma shows that
every universal SD Büchi automaton is history-deterministic with sufficient
lookahead.

######  Lemma 4.6.

Let $\mathcal{U}$ be a semantically-deterministic Büchi automata such that
$\mathcal{L}(\mathcal{U})=\Sigma^{\omega}$. Then, there is a $K$ such that
${\mathsf{Delay}}^{K}(\mathcal{U})$ is history-deterministic.

######  Proof 4.7 (Proof sketch).

We let $K=2^{n}$, where $n$ is the number of states of $\mathcal{A}$. The
crucial observation is that since $\mathcal{L}(\mathcal{U},q)=\Sigma^{\omega}$
for any state $q$ in $\mathcal{U}$, any finite word $u$ that has length at
least $2^{n}$ must have a run from $q$ that passes through an accepting
transition. Eve thus wins the history-determinism game on $\mathcal{U}$ by
exploiting the lookahead in ${\mathsf{Delay}}^{K}(\mathcal{A})$ to take at
least one accepting transition every $K$ steps. The run of Eve’s token then
has infinitely many accepting transitions and hence is accepting, as desired.

We can now prove B.

######  Proof 4.8 (Proof of B).

The forward implication is clear by Lemma 2.6. For the backward direction,
suppose that Eve wins the 1-token game on $\mathcal{A}$. Due to Theorem 3.1,
we may assume that $\mathcal{A}$ is universal. Then, from Lemma 4.6, we know
that there is a $K$ such that ${\mathsf{Delay}}^{K}(\mathcal{A})$ is history-
deterministic. If Eve wins the 1-token game on $\mathcal{A}$, then from Lemma
4.2, we know that $\mathcal{A}$ simulates ${\mathsf{Delay}}^{K}(\mathcal{A})$.
But since ${\mathsf{Delay}}^{K}(\mathcal{A})$ is language equivalent to
$\mathcal{A}$, we get from Corollary 2.10 that $\mathcal{A}$ is HD as well.

Having shown that the $1$-token game on a semantically-deterministic Büchi
automaton $\mathcal{A}$ is equivalent to the HD game on $\mathcal{A}$, we are
able to show that Joker games characterise history-determinism on Büchi
automata. We also get an alternate proof of Bagnol and Kuperberg’s result of
$2$-token games characterising history-determinism of Büchi automata as a
corollary.

######  Theorem 4.9.

For every Büchi automaton $\mathcal{A}$, the following statements are
equivalent.

  1. 1.

$\mathcal{A}$ is history-deterministic.

  2. 2.

Eve wins the Joker game on $\mathcal{A}$.

  3. 3.

Eve wins the $2$-token game on $\mathcal{A}$.

We prove Theorem 4.9 by reducing it to semantically-deterministic automata,
similar to Lemma 16 of Bagnol and Kuperberg (Section B.2).

Joker games on a Büchi automaton have smaller arenas than $2$-token games. As
a result, we get a more efficient algorithm to recognise HD Büchi automata.

######  Lemma 4.10.

Given a non-deterministic Büchi automaton
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta)$, we can decide whether it is history-
deterministic in time $\mathcal{O}(|\Sigma|^{2}|Q|^{3}|\Delta|)$.

######  Remark 4.11.

While we have proven B by reducing it to universal automata for the sake of
simplicity of arguments, one can also give a more direct proof. Such a direct
proof involves arguing that if an automaton $\mathcal{A}$ is not history-
deterministic, then there is a $K$ exponential in the size of $\mathcal{A}$
such that $\mathcal{A}$ does not simulate ${\mathsf{Delay}}^{K}(\mathcal{A})$.
It then follows from Lemma 4.2 that Eve loses the $1$-token game on
$\mathcal{A}$, as desired.

To argue that $\mathcal{A}$ does not simulate
${\mathsf{Delay}}^{K}(\mathcal{A})$, we reason based on the size of Adam’s
strategy in the history-determinism game on $\mathcal{A}$. Adam, in the
simulation game between $\mathcal{A}$ and ${\mathsf{Delay}}^{K}(\mathcal{A})$,
can pick letters according to his strategy in the history-determinism game on
$\mathcal{A}$, thus ensuring Eve produces a rejecting run on her token. At the
same time, Adam can exploit the lookahead in
${\mathsf{Delay}}^{K}(\mathcal{A})$ to construct an accepting run on his
token, thus winning the simulation game between $\mathcal{A}$ and
${\mathsf{Delay}}^{K}(\mathcal{A})$.

$p$$q$a,b:3b:2a:1a,b:3a:2b:1 Figure 1: An [1,2,3]-automaton $\mathcal{A}$ that
is not HD but on which Eve wins the Joker game.

We end this section by showing that unlike Büchi automata, Joker games do not
characterise history-determinism on parity automata.

######  Example 4.12.

Consider the $[1,3]$-automaton $\mathcal{A}$ shown in Figure 1. Note that
$\mathcal{A}$ accepts all words in $\\{a,b\\}^{\omega}$, and is SD. It is easy
to see that the automaton $\mathcal{A}$ is not history-deterministic, since
Adam can win the history-determinism game on $\mathcal{A}$ by choosing the
letter $a$ when Eve’s token is at $p$, and $b$ when her token is at $q$. This
forces Eve to never see an even transition, causing her run to be rejecting.

Eve wins the Joker game on $\mathcal{A}$, however. Consider the strategy of
Eve where she switches states if her and Adam’s tokens are at different
states, and otherwise stays at the same state. For Adam to win, Adam must play
only finitely many Jokers, and construct an accepting run, which requires him
to eventually stay in the same state. But then, Eve’s strategy will ensure
that Eve’s and Adam’s run are eventually identical, thus ensuring Adam cannot
win the Joker game of $\mathcal{A}$.

######  Theorem 4.13.

Joker games do not characterise history-determinism on (semantically-
deterministic) parity automata.

##  5 Determinising HD Büchi Automata in Polynomial Time

In this section, we present a polynomial time determinisation procedure for HD
Büchi automata with only a quadratic state-space blowup. Our procedure
combines ideas from the exponential-time procedure given by Kuperberg and
Skrzypczak [14] with our 1-token game characterisation of history-determinism
on SD Büchi automata.

See C

Let $\mathcal{H}$ be an HD Büchi automaton. Kuperberg and Skrzypczak’s
procedure relies on carefully analysing the simulation game between
$\mathcal{H}$ and an equivalent deterministic Büchi automaton $\mathcal{D}$
whose states are the subsets of $\mathcal{H}$. Their procedure iteratively
makes modifications to $\mathcal{H}$ and $\mathcal{D}$ based on the structure
of Eve’s winning strategies in this game or, more precisely, the progress
measures [12] or the signatures [23] of the vertices in this game, which they
call ranks. The end result of their procedure is a relation between states of
$\mathcal{H}$ and states of $\mathcal{D}$ that correspond to sets containing a
singleton in $\mathcal{H}$. A product construction based on this relation
allows them to construct an equivalent determinsitic Büchi automaton whose
number of states is quadratic in the number of states of $\mathcal{A}$.

The reason Kuperberg and Skrzypczak work with the simulation game between
$\mathcal{H}$ and $\mathcal{D}$ is that it characterises the history-
determinism of $\mathcal{H}$. A non-deterministic automaton is HD if and only
if it simulates an equivalent deterministic one, as shown by Hezinger and
Piterman [11]. Our result on 1-token games characterising history-determinism
(B) allows us to instead work with the $1$-token game on $\mathcal{H}$. This
results in a conceptually simpler procedure that works in polynomial time.

We present our algorithm in two steps. First, we introduce HD Büchi automata
that have a sprint self-simulation, and we give a polynomial time
determinisation procedure for them. The procedure involves a quadratic state-
space blowup. Then, we give a polynomial time iterative procedure to transform
$\mathcal{H}$ into an equivalent HD Büchi automaton of the same size that has
a sprint self-simulation. Overall, this gives us a polynomial time procedure
to determinise HD Büchi automata with a quadratic state-space blowup.

###  5.1 Determinising Automata with Sprint Self-Simulation

In this subsection, we describe what automata with sprint self-simulation are
and give a polynomial time determinisation procedure for such HD Büchi
automata. The key concept here is the _sprint simulation_ relation between two
Büchi automata, characterised by the _sprint step-ahead simulation game_. This
game is similar to the step-ahead simulation game, but the winning condition
for Eve is that she must see an accepting transition before Adam does, i.e.,
she is in a sprint with Adam to see an accepting transition in the step-ahead
simulation game first. Sprint step-ahead simulation (game) would be a more
accurate phrase, but for brevity, we shorten it to just sprint simulation
(game).

######  Definition 5.1.

For two non-deterministic Büchi automata
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta_{A})$ and $\mathcal{B}$ $=$
$(P,\Sigma,p_{0},\Delta_{B})$, the _sprint simulation game_ between
$\mathcal{A}$ and $\mathcal{B}$ is played on the set of positions $Q\times P$
and it proceeds in rounds. In each round $i=0,1,2,\dots$, from position
$(q_{i},p_{i})$, the two players Adam and Eve make the following choices:

  1. 1.

Adam chooses a letter $a_{i}\in\Sigma$;

  2. 2.

Eve chooses a transition
$\delta_{i}=(q_{i}\xrightarrow{a_{i}:c_{i}}q_{i+1})\in\Delta_{A}$;

  3. 3.

Adam chooses a transition
$\delta^{\prime}_{i}=(p_{i}\xrightarrow{a_{i}:c^{\prime}_{i}}p_{i+1})\in\Delta_{B}$.

The new position is $(q_{i+1},p_{i+1})$. At every round $i$, if transition
$\delta_{i}$ is accepting then Eve wins the game, and otherwise, if the
transition $\delta^{\prime}_{i}$ is accepting then Adam wins the game. If
neither $\delta_{i}$ nor $\delta^{\prime}_{i}$ are accepting transitions, then
the game continues for another round. Eve wins every infinite play.

Observe that if Eve wins the sprint simulation game then she can do so by a
positional strategy, because the objective for Eve is a disjunction of a
safety and a reachability objective, which can be seen as a $[0,1]$-parity
game. If Eve has a winning strategy in the above game, we say that
$\mathcal{A}$ sprint simulates $\mathcal{B}$. The sprint simulation relation
is transitive, i.e., if $\mathcal{A}$ sprint simulates $\mathcal{B}$ and
$\mathcal{B}$ sprint simulates $\mathcal{C}$, then $\mathcal{A}$ sprint
simulates $\mathcal{C}$ (Lemma C.1 in appendix).

######  Remark 5.2.

The sprint simulation relation is similar to the ‘dependency’ relation
introduced by Kuperberg and Skrzypczak [14, Definition 30]. While the sprint
simulation relation is between two Büchi automata, dependency relation is
derived from the sprint simulation game between a Büchi automaton and an
equivalent exponential-sized deterministic Büchi automaton.

We say that an HD Büchi automaton $\mathcal{H}$ has a _sprint self-simulation_
if it is semantically-deterministic and for every state $p$ in $\mathcal{H}$,
there is a language-equivalent state $q$, such that $(\mathcal{H},p)$ sprint
simulates $(\mathcal{H},q)$. When $\mathcal{H}$ is clear from the context, we
will just say that $p$ sprint simulates $q$. For the rest of this subsection,
fix $\mathcal{H}=(Q,\Sigma,q_{0},\Delta)$ to be an HD Büchi automaton that has
a sprint self-simulation. The following lemma follows from transitivity of
sprint simulation.

######  Lemma 5.3.

For every state $p$ in $\mathcal{H}$, there is a language-equivalent state $q$
such that $p$ sprint simulates $q$ and $q$ sprint simulates itself.

######  Proof 5.4.

Fix a state $p$ in $\mathcal{H}$. Then, there is a language-equivalent state
$q_{0}$ in $\mathcal{H}$ such that $p$ sprint simulates $q_{0}$. If $q_{0}$
does not sprint simulates itself, there is another language-equivalent $q_{1}$
such that $q_{0}$ sprint simulates $q_{1}$. Repeating this argument, we get a
sequence of states $q_{0},q_{1},q_{2},\dots$, such that $q_{i}$ sprint
simulates $q_{i+1}$. Since, there are finitely many states in $\mathcal{H}$,
we know there are two natural numbers $i<j$ such that $q_{i}=q_{j}$. But then,
by transitivity of sprint simulation (Lemma C.1), we get that $p$ sprint
simulates $q_{i}$ and $q_{i}$ sprint simulates itself, as desired.

Let us call a state $q$ sprint deterministic if the automaton $\mathcal{H}$
can be determinised by deleting transitions to get a deterministic
subautomaton $\mathcal{F}_{q}$ so that the following holds: for all finite
words $w$ that have a run in $\mathcal{H}$ starting at $q$ going through an
accepting transition, the unique run on $w$ in $\mathcal{F}_{q}$ from $q$ also
sees an accepting transition. Thus, for states $q$ that are sprint
deterministic, there is a uniform strategy that achieves the objective of
seeing an accepting transition as soon as possible on all words. We say that
the automaton $\mathcal{F}_{q}$ as above is a witness for sprint determinism
of $q$.

######  Lemma 5.5.

A state $q$ in $\mathcal{H}$ is sprint deterministic if and only if $q$ sprint
simulates itself. Moreover, there is a deterministic subautomaton
$\mathcal{F}$ that can be computed in polynomial time and is a witness for all
sprint deterministic states.

Lemmas 5.3 and 5.5 above tell us that every state in $\mathcal{H}$ is either
sprint deterministic, or it sprint simulates a state that is sprint
deterministic. Fix a subautomaton $\mathcal{F}$ from Lemma 5.5, and a
positional Eve strategy $\tau$ in the step-ahead simulation game from $(p,q)$
for all pairs of states $(p,q)$ such that $p$ sprint simulates $q$.

The deterministic automaton $\mathcal{D}$ is then constructed to consist of
pairs of states $(p,q)$ such that $p$ and $q$ are language equivalent, $p$
sprint simulates $q$, and $q$ is sprint deterministic. Note that the pair of
such states can be found in polynomial time, since checking for language
containment on HD Büchi automata [18, Corollary 17] and deciding the winner of
sprint simulation game can be done in polynomial time. Furthermore, for each
state $p$ in $\mathcal{H}$, we know from Lemmas 5.3 and 5.5 that there is a
state $q$ in $\mathcal{H}$ such that $(p,q)$ is a state in $\mathcal{D}$. We
let the initial state $d_{0}$ be $(q_{0},r_{0})$ for some $r_{0}$ such that
$(q_{0},r_{0})\in\mathcal{D}$.

At a state $(q,p)$, the transitions in $\mathcal{D}$ from the second component
$p$ are chosen according to transitions from $\mathcal{F}$, while transitions
from $q$ are chosen via the positional Eve strategy $\tau$. When an accepting
transition $q\xrightarrow{a:2}q^{\prime}$ is taken on the first component, we
update the second component deterministically to be $p^{\prime}$ such that
$(q^{\prime},p^{\prime})$ is a state in $\mathcal{D}$. Or, equivalently,
$q^{\prime}$ and $p^{\prime}$ are language equivalent, $q^{\prime}$ sprint
simulates $p^{\prime}$, and $p^{\prime}$ is sprint deterministic. The
priorities of transitions in $\mathcal{D}$ are the priorities of transitions
of the first component. A more formal construction of $\mathcal{D}$ can be
found in the appendix.

We show the correctness of our construction using the definition of sprint
simulation game and the fact that $\mathcal{H}$ is semantically-deterministic.

######  Lemma 5.6.

The automaton $\mathcal{D}$ accepts the same language as $\mathcal{H}$.

######  Proof 5.7.

$\mathcal{L}(\mathcal{D})\subseteq\mathcal{L}(\mathcal{H})$: If $\rho$ is an
accepting run of a word $w$ in $\mathcal{D}$, then the projection of $\rho$ on
the first component is an accepting run in $\mathcal{H}$ as well.

$\mathcal{L}(\mathcal{H})\subseteq\mathcal{L}(\mathcal{D})$: We show that for
each state $(p,q)$ in $\mathcal{D}$, if $w\in\mathcal{L}(\mathcal{H},p)$ then
the run from $(p,q)$ on $w$ in $\mathcal{D}$ sees an accepting transition
eventually. We can then conclude by induction and the semantic determinism of
$\mathcal{H}$ that a run on $\mathcal{D}$ on any word in
$\mathcal{L}(\mathcal{H})$ contains infinitely many accepting transitions, and
hence it is accepting. To see this, let $w\in\mathcal{L}(\mathcal{H},p)$ and
let $\rho_{D}$ be the run of $\mathcal{D}$ on $w$ from $(p,q)$. By
construction of $\mathcal{D}$, we know that $q$ is language-equivalent to $p$.
Since $q$ is sprint deterministic, the second component of $\rho_{D}$ in
$\mathcal{D}$ must contain an accepting transition on $w$ eventually. But
since $p$ sprint simulates $q$, the run on the first component of $\rho_{D}$
contains an accepting transition as well, as desired.

###  5.2 Towards Automata with Sprint Self-Simulation

We now present a polynomial time algorithm to convert an HD Büchi automaton
into an equivalent HD Büchi automaton that has a sprint self-simulation.
Throughout this subsection, let $\mathcal{H}=(Q,\Sigma,q_{0},\Delta)$ be an HD
Büchi automaton.

We say that $\mathcal{H}$ is _good_ if $\mathcal{H}$ is semantically-
deterministic and Eve wins the Joker game from all states in $\mathcal{H}$.
Every HD Büchi automaton $\mathcal{H}$ can be converted to an equivalent good
HD Büchi automaton in polynomial time: we fix a winning strategy $\tau$ for
Eve on the Joker game on $\mathcal{H}$, and consider the subautomaton
$\mathcal{H}_{N}$ consisting of transitions that Eve takes according to $\tau$
(Lemma C.6). We thus assume without loss of generality that $\mathcal{H}$ is
good.

To get an HD Büchi automaton equivalent to $\mathcal{H}$ and that has a sprint
self-simulation, we iteratively make modifications to $\mathcal{H}$ based on
the ranks of the $1$-token game on $\mathcal{H}$. We first give a description
of the $1$-token game on a Büchi automaton as a $[0,2]$-parity game, and
briefly recall the properties of ranks that we need on such games.

######  Definition 5.8.

For a semantically-deterministic Büchi automaton
$\mathcal{B}=(Q,\Sigma,q_{0},\Delta)$, define the $[0,2]$-parity game
$G_{1}(\mathcal{B})=(V,E)$ as follows:

  * •

The set of vertices $V$ consists of the set $V=V_{1}\cup V_{2}\cup V_{3}$,
where:

    1. 1.

$V_{1}=\\{(p,q)\mid\text{ $p,q$ are states reachable from $q_{0}$ upon reading
the same word $w$}\\}$

    2. 2.

$V_{2}=\\{(p,a,q)\mid(p,q)\in V_{1}\\}$

    3. 3.

$V_{3}=\\{(p^{\prime},q,a)\mid(p,a,q)\in V_{2}\text{ and
}p\xrightarrow{a}p^{\prime}\in\Delta\\}$

Eve’s vertices are $V_{\boldsymbol{\exists}}=V_{2}$, while Adam’s vertices are
$V_{\boldsymbol{\forall}}=V_{1}\cup V_{3}$

  * •

The set of edges $E$ is the union of following sets:

    1. 1.

$E_{1}=\\{(p,q)\xrightarrow{}(p,a,q)\mid a\in\Sigma\\}$ (Adam chooses a
letter)

    2. 2.

$E_{2}=\\{(p,a,q)\xrightarrow{}(p^{\prime},q,a)\mid
p\xrightarrow{a:c}p^{\prime}\in\Delta\\}$ (Eve chooses a transition on her
token)

    3. 3.

$E_{3}=\\{(p^{\prime},q,a)\xrightarrow{}(p^{\prime},q^{\prime})\mid
q\xrightarrow{a:c}q^{\prime}\in\Delta\\}$ (Adam chooses a transition on his
token)

  * •

The priority function $\Omega$ is defined as follows. All elements in $E_{1}$
are assigned priority 0, while edges $(p,a,q)\xrightarrow{}(p^{\prime},q,a)$
in $E_{2}$ are assigned priority 2 if the transition
$\delta=p\xrightarrow{a:c}p^{\prime}$ in $\mathcal{B}$ is accepting (or
equivalently, $c=2$), and 0 otherwise. The edge
$(p^{\prime},q,a)\xrightarrow{}(p^{\prime},q^{\prime})$ in $E_{3}$ is assigned
priority 1 if the transition $q\xrightarrow{a:c}q^{\prime}$ is accepting, and
0 otherwise.

Observe that since $\mathcal{H}$ is SD, we have
$\mathcal{L}(\mathcal{H},p)=\mathcal{L}(\mathcal{H},q)$ if $(p,q)$ is a vertex
in $G_{1}(\mathcal{H})$.

##### Ranks.

We now define the ranks of a $[0,2]$-parity game $\mathcal{G}$. For each
vertex $v$ in $\mathcal{G}$, $\text{rank}(v)$ is the largest number of 1’s
that Adam can guarantee Eve will see before seeing a 2 in the play (or only
0’s) starting from $v$.

Observe that Eve wins such a parity game from every position if and only if
the ranks of all the vertices are bounded. If this is the case, then there is
a positional winning strategy $\tau$, using which Eve can guarantee that she
sees at most $\text{rank}(v)$ many 1’s before seeing a 2 (or seeing 0’s
forever) [23, Lemma 8] in every play. We will call such a strategy _optimal_.
For $[0,2]$-parity games with $n$ vertices and $m$ edges, an optimal strategy
can be computed in time $\mathcal{O}(mn)$ [12, Theorem 11].

The following property of ranks follows from their definition.

######  Lemma 5.9.

Let $\mathcal{G}$ be a $[0,2]$-parity game, and let $v\xrightarrow{e}u$ be an
edge in $\mathcal{G}$, such that either $v$ belongs to Adam, or the edge $e$
is prescribed by Eve’s optimal strategy $\tau$. Then the edge $e$ has priority
2 or $\text{rank}(v)\geq\text{rank}(u)$. Furthermore, this inequality is
strict if $e$ has priority 1.

Consider the $1$-token game $G_{1}(\mathcal{H})$, and the ranks of its
vertices. Note that for a vertex $(q,p)$ in $G_{1}(\mathcal{H})$, we have
$\text{rank}(q,p)=0$ if and only if $q$ sprint simulates $p$. Define, for each
state $q\in\mathcal{H}$, its optimal rank $\text{opt}(q)$ to be the minimum
rank of a vertex of the form $(q,p)$ in $G_{1}(\mathcal{H})$. Note that if
$\text{opt}(q)=0$ for all states $q\in\mathcal{H}$, then $\mathcal{H}$ has a
sprint self-simulation. Thus, our iterative procedure focuses on reducing the
optimal ranks for all states until they are all $0$. We describe this
procedure below.

##### Iterating towards a sprint self-simulation.

Set $\mathcal{H}_{0}=\mathcal{H}$. For each $i\geq 0$, perform the following
three steps on $\mathcal{H}_{i}$ until $\mathcal{H}_{i+1}=\mathcal{H}_{i}$.

  1. 1.

For all vertices $(p,q)\in G_{1}(\mathcal{H}_{i})$, compute the optimal ranks
$\text{opt}_{i}(p)$ in $G_{1}(\mathcal{H}_{i})$.

  2. 2.

Obtain $\mathcal{H}^{\prime}_{i}$ from $\mathcal{H}_{i}$ by removing all
transitions $q\xrightarrow{a:1}q^{\prime}$ with
$\text{opt}_{i}(q)<\text{opt}_{i}(q^{\prime})$.

  3. 3.

Obtain $\mathcal{H}_{i+1}$ from $\mathcal{H}^{\prime}_{i}$, by making all
transitions $q\xrightarrow{a:1}q^{\prime}$ with
$\text{opt}_{i}(q)>\text{opt}_{i}(q^{\prime})$ accepting.

In the Appendix, we show that for each $i$, both $\mathcal{H}^{\prime}_{i}$
and $\mathcal{H}_{i+1}$ are good HD Büchi automata that are equivalent to
$\mathcal{H}_{i}$ (Lemmas C.8 and C.10). By a simple induction, we get that
each $\mathcal{H}_{i}$ for $i\geq 0$ is a good HD Büchi automaton equivalent
to $\mathcal{H}$.

Note that in steps 2 and 3, we are either removing rejecting transitions or
making rejecting transitions accepting, and hence this procedure terminates
after at most $|\Delta|$ iterations. Let $\mathcal{H}^{*}$ be the automaton
obtained after the procedure terminates. Since $\mathcal{H}^{*}$ is good, we
know that it is SD. The next lemma thus shows that $\mathcal{H}^{*}$ has a
sprint self-simulation.

######  Lemma 5.10.

For all states $p$ in $\mathcal{H}^{*}$, there is a language-equivalent state
$q$ in $\mathcal{H}^{*}$ such that $p$ sprint simulates $q$.

######  Proof 5.11.

Assume, to the contrary, that there exists a state $p$ such that
$\text{opt}^{*}(p)=\text{rank}^{*}(p,q)>0$. Fix an optimal winning strategy
$\tau$ for Eve in $G_{1}(\mathcal{H}^{*})$. Consider a finite play $\rho$ of
$G_{1}(\mathcal{H}^{*})$ from $(p,q)$ where Eve is playing according to
$\tau$, Adam chooses an accepting transition in his token at some point, while
Eve is never able to. Then by monotonicity of ranks (Lemma 5.9), we know that
$\text{rank}^{*}$ strictly decreases across $\rho$ at some point. Then, there
must be a rejecting transition across which the quantity $\text{opt}^{*}$
decreases as well. But since such transitions would have been made accepting
in step 3 of the iteration, we get a contradiction.

From the polynomial time determinisation construction for HD Büchi automata
that have a sprint self-simulation presented in Section 5.1, we get a
polynomial time determinisation procedure for HD Büchi automata. This
concludes the proof of C.

##  6 Discussion

Our paper has shown two key results on HD Büchi automata: a $1$-token game
based characterisation of history-determinism for semantically-deterministic
Büchi automata, and a polynomial time determinisation procedure. In the
process of obtaining these results, we developed several novel techniques that
we believe to be equally exciting and insightful. We finish by remarking some
implications of our results and techniques, and natural future directions that
our work points to.

Our first technique, presented in Section 3, reduces game based
characterisations of history-determinism on parity automata to parity
universal automata. But the history-determinism game on such an automaton is
just a parity game, since Adam’s word is always accepting. The $2$-token
conjecture thus reduces, by Theorem 3.4, to showing that this parity game is
equivalent to the $2$-token game. This seems easy enough to show at first
glance, but it proves to be (unsurprisingly) difficult. This result also shows
that the difficulty in proving or disproving the $2$-token conjecture arises
not from the language an automaton recognises, but rather from the structure
of the automaton.

We also introduced lookahead games, and showed that $k$-lookahead games are
equivalent to $1$-token games for all $k\geq 1$ (A). This shows that the
$1$-token games are quite powerful, in the same sense that $2$-token games are
powerful due to them being equivalent to $k$-token games for all $k\geq 2$.
While our $1$-token game characterisation of history-determinism on SD Büchi
automata does not extend to parity automata (Theorem 4.13), one can combine
the two different approaches to give the $2$-token game more power, both in
the form of lookahead and more tokens. It would be interesting to consider
such games to try extending the $2$-token conjecture beyond Büchi and co-Büchi
automata.

Our algorithm to determinise HD Büchi automata involves a quadratic blowup.
However, we do not know whether this is tight. In fact, it is still open if HD
Büchi automata are strictly more succinct than determinstic Büchi automata.
Nevertheless, we are hopeful that our algorithm can offer some insights on how
to make progress on this problem.

Let us end with a problem highlighted by Boker and Lehtinen in their recent
survey [6, Section 6.3.2]. In all the existing game-based characterisations
which are used to recognise HD automata efficiently, including ours (B), it is
not clear how we can naturally convert a winning strategy for Eve from the
$2$-token game or the Joker game to a winning strategy in the HD game. Our
algorithm to determinise HD Büchi automata, however, can be seen as one:
starting with a winning strategy for Eve in the Joker game, we construct a
strategy in the HD game that requires linear memory, thus obtaining a
deterministic automaton of quadratic size. But the proof of correctness of our
algorithm relies on B. Towards a more pure strategy-transfer argument, where
ideally an algorithm for strategy transfer also proves a game-based
characterisation of history-determinism, our algorithm comes tantalisingly
close. Indeed, proving that the automaton constructed in Step 2 preserves the
relevant invariants (Lemma C.8) is the only place where we use the fact that
we started with an HD automaton. We believe that trying to get rid of this
assumption, in order to give an alternative strategy-transfer proof for the
$1$-token game characterisation of history-determinism on SD Büchi automata,
could lead to crucial insights towards better understanding HD (Büchi)
automata and token games.

## References

  * [1] Bader Abu Radi and Orna Kupferman.  Minimization and Canonization of GFG Transition-Based Automata.  Logical Methods in Computer Science, 18(3), 2022.  doi:10.46298/lmcs-18(3:16)2022.
  * [2] Marc Bagnol and Denis Kuperberg.  Büchi Good-for-Games Automata Are Efficiently Recognizable.  In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, volume 122 of LIPIcs, pages 16:1–16:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.  doi:10.4230/LIPIcs.FSTTCS.2018.16.
  * [3] Udi Boker, Thomas Henzinger, Karoliina Lehtinen, and Aditya Prakash.  History-Determinism vs. Fair Simulation.  To appear.
  * [4] Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michal Skrzypczak.  On the Succinctness of Alternating Parity Good-for-Games Automata.  CoRR, abs/2009.14437, 2020.  arXiv:2009.14437.
  * [5] Udi Boker and Karoliina Lehtinen.  Token Games and History-Deterministic Quantitative-Automata.  Logical Methods in Computer Science, 19(4), 2023.  doi:10.46298/LMCS-19(4:8)2023.
  * [6] Udi Boker and Karoliina Lehtinen.  When a Little Nondeterminism Goes a Long Way: An Introduction to History-Determinism.  ACM SIGLOG News, 10(1):24–51, 2023.  doi:10.1145/3584676.3584682.
  * [7] Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan.  Deciding Parity Games in Quasi-polynomial Time.  SIAM J. Comput., 51(2):17–152, 2022.  doi:10.1137/17m1145288.
  * [8] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman.  Generalized Parity Games.  In Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, volume 4423 of Lecture Notes in Computer Science, pages 153–167. Springer, 2007.  doi:10.1007/978-3-540-71389-0_12.
  * [9] Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors.  Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002\.  doi:10.1007/3-540-36387-4.
  * [10] Yuri Gurevich and Leo Harrington.  Trees, Automata, and Games.  In Symposium on Theory of Computing, STOC 1982, pages 60–65. ACM, 1982.  doi:10.1145/800070.802177.
  * [11] Thomas A. Henzinger and Nir Piterman.  Solving Games Without Determinization.  In Computer Science Logic, CSL 2006, volume 4207 of Lecture Notes in Computer Science, pages 395–410. Springer, 2006.  doi:10.1007/11874683_26.
  * [12] Marcin Jurdzinski.  Small Progress Measures for Solving Parity Games.  In STACS 2000, volume 1770 of Lecture Notes in Computer Science, pages 290–301. Springer, 2000.  URL: https://doi.org/10.1007/3-540-46541-3_24.
  * [13] Marcin Jurdzinski and Ranko Lazic.  Succinct Progress Measures for Solving Parity Games.  In Symposium on Logic in Computer Science, LICS 2017, pages 1–9. IEEE Computer Society, 2017.  doi:10.1109/LICS.2017.8005092.
  * [14] Denis Kuperberg and Michal Skrzypczak.  On Determinisation of Good-for-Games Automata.  In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 299–310. Springer, 2015.  doi:10.1007/978-3-662-47666-6_24.
  * [15] Orna Kupferman.  Using the Past for Resolving the Future.  Frontiers Comput. Sci., 4, 2022.  doi:10.3389/fcomp.2022.1114625.
  * [16] Karoliina Lehtinen, Pawel Parys, Sven Schewe, and Dominik Wojtczak.  A Recursive Approach to Solving Parity Games in Quasipolynomial Time.  Log. Methods Comput. Sci., 18(1), 2022.  doi:10.46298/lmcs-18(1:8)2022.
  * [17] Donald A. Martin.  Borel Determinacy.  Annals of Mathematics, 102(2):363–371, 1975.  URL: http://www.jstor.org/stable/1971035.
  * [18] Aditya Prakash.  Checking History-Determinism is NP-hard for Parity Automata.  In Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14574 of Lecture Notes in Computer Science, pages 212–233. Springer, 2024\.  doi:10.1007/978-3-031-57228-9_11.
  * [19] Aditya Prakash and K. S. Thejaswini.  On History-Deterministic One-Counter Nets.  In Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, volume 13992 of Lecture Notes in Computer Science, pages 218–239. Springer, 2023.  doi:10.1007/978-3-031-30829-1_11.
  * [20] Bader Abu Radi and Orna Kupferman.  On Semantically-Deterministic Automata.  In International Colloquium on Automata, Languages, and Programming, ICALP 2023, volume 261 of LIPIcs, pages 109:1–109:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.  URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.109.
  * [21] Bader Abu Radi, Orna Kupferman, and Ofer Leshkowitz.  A Hierarchy of Nondeterminism.  In Mathematical Foundations of Computer Science, MFCS 2021, volume 202 of LIPIcs, pages 85:1–85:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.  URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.85.
  * [22] Sven Schewe.  Minimising Good-For-Games Automata Is NP-Complete.  In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, volume 182 of LIPIcs, pages 56:1–56:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.  doi:10.4230/LIPICS.FSTTCS.2020.56.
  * [23] Igor Walukiewicz.  Monadic Second-Order Logic on Tree-like Structures.  Theor. Comput. Sci., 275(1-2):311–346, 2002.  doi:10.1016/S0304-3975(01)00185-2.

##  Appendix A Appendix for Section 3

See 3.2

######  Proof A.1.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta)$. If $\mathcal{A}$ is HD, then by
Lemma 2.6, it simulates all such $\mathcal{S}$ with
$\mathcal{L}(\mathcal{S})\subseteq\mathcal{L}(\mathcal{A})$. For the other
direction, assume that $\mathcal{A}$ is not history-deterministic. Then, Adam
has a finite memory winning strategy in the history-determinism game on
$\mathcal{A}$ which can be represented by a _deterministic transducer_
$\mathcal{M}=(M,\Delta,m_{0},\Delta_{M},f:M\xrightarrow{}\Sigma)$ that outputs
letters in $\Sigma$ based on transitions that Eve picks in the history-
determinism game. More formally, the transducer $\mathcal{M}$ corresponds to a
finite memory Adam winning strategy as follows. In round $i$ of the HD game on
$\mathcal{A}$ for each $i\geq 0$, where the Eve’s state is at $q_{i}$ and
Adam’s memory is at $m_{i}$, Adam starts by picking the letter
$a_{i}=f(m_{i})$. Eve then picks a transition $\delta_{i}$ in
$\mathcal{A}_{i}$ on the letter $a_{i}$. Adam then updates his memory by the
unique transition $m_{i}\xrightarrow{\delta_{i}}m_{i+1}$ in $\mathcal{M}$.

Note that $\mathcal{M}$ recognises the set of winning plays of Adam, i.e., any
word $w_{\Delta}\in\Delta^{\omega}$ that has a run in $\mathcal{M}$ represents
a rejecting run in $\mathcal{A}$ over an accepting word in $\mathcal{A}$.

Consider the safety automaton
$\mathcal{M}_{\Sigma}=(M,\Sigma,m_{0},\Delta^{\prime}_{M})$, obtained by
‘projecting’ $\mathcal{M}$ onto $\Sigma$, i.e., $m\xrightarrow{a:0}m^{\prime}$
is a transition in $\mathcal{M}_{\Sigma}$ iff there is a transition
$m\xrightarrow{\delta}m^{\prime}$ such that $f(m)=a$ and $\delta\in\Delta$ is
a transition on the letter $a$. Note that
$\mathcal{L}(\mathcal{M}_{\Sigma})\subseteq\mathcal{L}(\mathcal{A})$, since
Adam only constructs accepting words in the HD game on $\mathcal{A}$ when
playing according to $\mathcal{M}$.

Now, let $\mathcal{S}$ be the safety automaton obtained by determinising
$\mathcal{M}_{\Sigma}$ via the subset construction. Since
$\mathcal{L}(\mathcal{S})=\mathcal{L}(\mathcal{M}_{\Sigma})$, we get that
$\mathcal{L}(\mathcal{S})\subseteq\mathcal{L}(\mathcal{A})$. We claim that
$\mathcal{A}$ does not simulate $\mathcal{S}$. Indeed, consider the following
winning strategy of Adam in the simulation game between $\mathcal{A}$ and
$\mathcal{S}$, where Adam uses $\mathcal{M}$ as a memory to choose letters.

At the start of round 0, Adam’s token is at the state $\\{m_{0}\\}$, his
memory is $m_{0}$, while Eve’s token is at $q_{0}$. At round $i$ for each
$i\geq 0$, suppose that Adam’s token in at $S_{i}$, his memory is $m_{i}$ such
that $m_{i}\in S_{i}$, and Eve’s token is at $q_{i}$. Then, Adam chooses the
letter $a_{i}=f(m_{i})$, Eve picks the transition $\delta_{i}$ on $a_{i}$, and
Adam’s token takes the deterministic transition on $a_{i}$ to
$S_{i+1}\subseteq M$ in $\mathcal{S}$. Let $m_{i+1}$ be such that
$m_{i}\xrightarrow{\delta_{i}}m_{i+1}$ is the the unique transition on
$\delta_{i}$ at $m_{i}$ in $\mathcal{M}$. We update Adam’s memory to be
$m_{i+1}$, which is an element of $S_{i+1}$.

Note that any Eve’s run on her token in the above play would be rejecting,
since such plays correspond to a word in $\mathcal{M}$. But Adam’s run on his
token in the safety automaton $\mathcal{S}$ is accepting, as desired.

See 3.1

######  Proof A.2.

It is clear that 1 implies 2. For the other direction, suppose that for all SD
Büchi automata $\mathcal{U}$ with $\mathcal{L}(\mathcal{U})=\Sigma^{\omega}$,
$\mathcal{U}$ is HD if and only if Eve wins the 1-token game on $\mathcal{U}$.

Let $\mathcal{A}=(Q,\Sigma,\Delta,q_{0})$ be a SD Büchi automaton. The
backward implication is clear, that is, if $\mathcal{A}$ is HD, then Eve wins
the 1-token game on $\mathcal{A}$ (Lemma 2.6). For the forward implication,
suppose $\mathcal{A}$ is not HD. Then, by Lemma 3.2, we know there is a
deterministic safety automaton $\mathcal{S}=(S,\Sigma,s_{0},\Delta_{S})$ such
that $\mathcal{L}(\mathcal{S})\subseteq\mathcal{L}(\mathcal{A})$, and
$\mathcal{A}$ does not simulate $\mathcal{S}$. For convenience, we will assume
that $\mathcal{S}$ does not have any states that are not safe, and instead
might be incomplete, i.e., there can be states from which there is no
$a$-transition from some $a\in\Sigma$. Consider the product automaton of
$\mathcal{A}$ and $\mathcal{S}$ given by
$\mathcal{P}=(P,\Sigma,p_{0},\Delta_{P})$, where

  * •

The set of states $P=Q\times S$, the initial state $p_{0}=(q_{0},s_{0})$

  * •

$(q,s)\xrightarrow{a:c}(q^{\prime},s^{\prime})$ is a transition in
$\Delta_{P}$ if and only if $q\xrightarrow{a:c}q^{\prime}$ is a transition in
$\mathcal{A}$, and $s\xrightarrow{a:0}s^{\prime}$ is a transition in
$\mathcal{S}$.

We note that
$\mathcal{L}(\mathcal{P})=\mathcal{L}(\mathcal{S})\cap\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{S})$.
Consider the automaton $\mathcal{U}$ obtained by completing $\mathcal{P}$ with
an accepting sink state $f$. That is, for all states $p$ in $\mathcal{P}$,
$a\in\Sigma$ such that there is no outgoing transition from $p$ on $a$, we add
the transition $p\xrightarrow{a:k}f$, and the self-loops $f\xrightarrow{a:k}f$
for some even number $k$. In the case of Büchi automata, $k=2$.

  1. 1.

$\mathcal{L}(\mathcal{U})=\Sigma^{\omega}$. For any word
$w\in\mathcal{L}(\mathcal{S})$, it is accepted by $\mathcal{P}$ and hence by
$\mathcal{U}$. If $w\notin\mathcal{L}(\mathcal{S})$, then any run of
$\mathcal{U}$ on $w$ ends up at $f$, and hence $w\in\mathcal{L}(\mathcal{U})$.

  2. 2.

$\mathcal{U}$ is SD. Indeed, for each state $q$, we can argue similarly that
$\mathcal{L}(\mathcal{U},q)=\Sigma^{\omega}$.

  3. 3.

$\mathcal{U}$ is not HD. The player Adam can use a winning strategy for the
simulation game between $\mathcal{A}$ and $\mathcal{S}$, in the HD game on
$\mathcal{U}$. Since Adam will construct a word in $\mathcal{S}$ using this
strategy, Eve can never reach $f$, neither can her run in the history-
determinism game on $\mathcal{U}$ be accepting.

  4. 4.

If Adam wins the 1-token game on $\mathcal{U}$, then Adam wins the 1-token
game on $\mathcal{A}$. Let $\sigma$ be a winning strategy for Adam in the
1-token game on $\mathcal{U}$. Note that at any point in the 1-token game on
$\mathcal{U}$, if Eve’s token is at a state $(q,s)$, then Adam’s token must
also be at a state of the form $(q^{\prime},s)$ since $\mathcal{S}$ is
deterministic, for some state $q^{\prime}$ in $\mathcal{A}$. Thus, $\sigma$
will never choose a letter $a$ in the $1$-token game on $\mathcal{U}$ whenever
Eve’s token is at a state $(q,s)$ where there is no $a$-transition on $s$ in
$\mathcal{S}$, since then Eve can move her token to $f$ and win. Similarly,
Adam will never be able to move his token to $f$ if he plays according to
$\sigma$ as well. With this, we see that any play of the $1$-token game in
$\mathcal{U}$ where Adam plays according to his $\sigma$ strategy corresponds
to a play of $1$-token game on $\mathcal{A}$. It follows that Adam wins the
$1$-token game on $\mathcal{A}$ by playing according to the strategy $\sigma$
and keeping in his memory states of $\mathcal{S}$.

Since Adam wins the 1-token game on $\mathcal{U}$ if $\mathcal{U}$ is not
history-deterministic by the hypothesis, 4 gives us that Adam wins the
$1$-token game on $\mathcal{A}$, as desired.

##  Appendix B Appendix for Section 4

###  B.1 Lookahead Games

See 4.6

######  Proof B.1.

We let $K=2^{n}$, where $n$ is the number of states in $\mathcal{U}$. We start
by proving the following claim.

######  Claim 1.

For any state $q$ in $\mathcal{U}$ that is reachable from the initial state,
and any finite word $u$ of length at least $K$, there is a run from $q$ on $u$
in $\mathcal{U}$ that visits an accepting transition.

Note that since $\mathcal{U}$ is semantically-deterministic, we have that
$\mathcal{L}(\mathcal{U},q)=\Sigma^{\omega}$. Consider the sequence of sets of
states that can be visited on reading the prefixes of $u$:

$\\{q\\}\xrightarrow{a_{1}}S_{1}\xrightarrow{a_{2}}S_{1}\cdots\xrightarrow{a_{K}}S_{K},$

where $u=a_{1}a_{2}\cdots a_{K}$ and $S_{i+1}$ is the set of all states that
have a transition from $S_{i}$ on the letter $a_{i}$. Then, observe that two
subsets $S_{i}$ and $S_{j}$ for $i<j$ must be the same.

Let $u^{\prime}$ and $v$ be the finite words $u^{\prime}=a_{1}a_{2}\cdots
a_{i}$ and $v=a_{i+1}a_{i+2}\cdots a_{j}$. Thus, the sequence of sets of
states visited on prefixes of $w$ cycles from $S_{i}$ upon reading a $v$ to
$S_{i}$. Since $w$ is in $\mathcal{L}(\mathcal{A},q)$, there must be an
accepting transition seen from a state in $S_{i}$ on a run on the finite word
$v$, as desired. We proceed to show that ${\mathsf{Delay}}^{K}(\mathcal{A})$
is history-deterministic, by describing a winning strategy for Eve in the
history-determinism game on ${\mathsf{Delay}}^{K}(\mathcal{A})$. Starting from
the initial state in ${\mathsf{Delay}}^{K}(\mathcal{A})$, the transitions on
the first $K$ letters of any word is deterministic, after which Eve’s state in
${\mathsf{Delay}}^{K}(\mathcal{A})$ is of the form $(q_{0},u_{0})$, where
$u_{0}$ is a word of length $K$. By 1, we know that there is a finite run
$\rho_{0}$ from $q_{0}$ on $u_{0}$ that contains at least one accepting
transition. Hence, Eve chooses the transitions in
${\mathsf{Delay}}^{K}(\mathcal{A})$ for the next $K$ rounds in the history-
determinism game according to $\rho_{0}$. After these $K$ rounds, Eve’s token
in the history-determinism game is at a state $(q_{1},u_{1})$, where again
$u_{1}$ is a finite word of length $K$. But now Eve can repeat this strategy
in the next $K$ rounds, following a run $\rho_{1}$ from $q_{1}$ on $u_{1}$ in
$\mathcal{A}$ that contains an accepting transition. Thus, Eve repeating this
strategy after every $K$ rounds causes Eve to construct an accepting run in
the history-determinism game on ${\mathsf{Delay}}^{K}(\mathcal{A})$. It
follows that ${\mathsf{Delay}}^{K}(\mathcal{A})$ is history-deterministic.

###  B.2 Joker Games characterises History-Determinism on Büchi Automata

See 4.9

In order to show Theorem 4.9, we start by showing the following lemma, which
allows us to reduce it to the case when $\mathcal{A}$ is semantically-
deterministic. This is an adaptation of Lemma 16 in the work of Bagnol and
Kuperberg [2], for showing that Eve winning 2-token games on Büchi automata
characterises history-determinism.

######  Lemma B.2.

Suppose Eve wins the Joker game on a non-deterministic parity automaton
$\mathcal{A}$, and let $\mathcal{B}$ be the sub-automaton obtained by removing
any transitions that are not language-preserving. Then we have:

  1. 1.

$\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{B})$

  2. 2.

Eve wins the Joker game on $\mathcal{B}$

  3. 3.

If $\mathcal{B}$ is history-deterministic, then so is $\mathcal{A}$

######  Proof B.3.

If Eve wins the Joker game on $\mathcal{A}$, then note that her winning
strategy can only take language-preserving transitions: if she picks a
transition $p\xrightarrow{a}q$ in the history-determinism game on
$\mathcal{A}$ such that $\mathcal{L}(\mathcal{A},q)\subsetneq
a^{-1}\mathcal{L}(\mathcal{A},p)$, then Adam can play Joker and construct a
run on the word $aw$ where $w\in
a^{-1}(\mathcal{L}(\mathcal{A},p)\setminus\mathcal{L}(\mathcal{A},q))$, and
win the Joker game. This implies that Eve has to take transitions only in
$\mathcal{B}$ to win the Joker game, which shows 2. The proof of 1 follows as
well, since for any word $w\in\mathcal{L}(\mathcal{A})$ that Adam plays, Adam
can construct an accepting run in his token, forcing Eve to construct an
accepting run on $w$ while taking only language-preserving transitions.

Finally for 3, if $\mathcal{B}$ is history-deterministic, Eve can use her
strategy in the history-determinism game on $\mathcal{B}$ to win the history-
determinism game on $\mathcal{A}$, since $\mathcal{B}$ is a subautomaton of
$\mathcal{A}$ with $\mathcal{L}(\mathcal{B})=\mathcal{L}(\mathcal{A})$.

######  Corollary B.4.

Given a Büchi automaton $\mathcal{A}$, Eve wins the Joker game on
$\mathcal{A}$ if and only if $\mathcal{A}$ is history-deterministic.

######  Proof B.5.

$\Rightarrow:$ If Eve wins the Joker game on $\mathcal{A}$, then she wins the
Joker game on $\mathcal{B}$, where $\mathcal{B}$ is the subautomaton obtained
by removing transitions in $\mathcal{A}$ that are not language-preserving.
Note that from B, a semantically-deterministic Büchi automaton $\mathcal{B}$
is history-deterministic if and only if Eve wins the 1-token game on
$\mathcal{B}$, which is true since Eve wins the Joker game on $\mathcal{B}$.
It follows from Lemma B.2 that $\mathcal{A}$ is history-deterministic as well.

$\Leftarrow:$ This is clear from Lemma 2.6.

Replacing Joker game with 2-token game in Lemmas B.2 and B.4 yields the result
of Bagnol and Kuperberg that 2-token game also characterises history-
determinism on Büchi automata [2] as a corollary. This conclude the proof of
Theorem 4.9.

###  B.3 Solving Joker Games

Joker games can be represented as a $[0,2]$-parity game, as we show below.

######  Definition B.6 (Joker game on a Büchi automaton).

For a non-deterministic Büchi automaton $\mathcal{A}=(Q,\Sigma,q_{0},\Delta)$,
define the game $G_{J}(\mathcal{A})=(V,E)$ with the parity condition $\Omega$
as follows.

  * •

The set of vertices $V$ consists of the set $V=V_{1}\cup V_{2}\cup V_{3}$,
where:

    1. 1.

$V_{1}=Q\times Q$

    2. 2.

$V_{2}=Q\times\Sigma\times Q$

    3. 3.

$V_{3}=Q\times Q\times\Sigma$

Eve’s vertices are $V_{\boldsymbol{\exists}}=V_{2}$, while Adam’s vertices are
$V_{\boldsymbol{\forall}}=V_{1}\cup V_{3}$. The initial vertex is
$(q_{0},q_{0})$.

  * •

The set of edges $E$ is the union of following sets:

    1. 1.

$E_{1}=\\{(p,q)\xrightarrow{}(p,a,q)\mid a\in\Sigma\\}$. These edges
correspond to Adam choosing a letter at the beginning of each round.

    2. 2.

$E_{2}=\\{(p,a,q)\xrightarrow{}(p^{\prime},q,a)\mid
p\xrightarrow{a:c}p^{\prime}\in\Delta\\}$. These edges correspond to Eve
choosing a transition on her token

    3. 3.

$E_{3}=\\{(p^{\prime},q,a)\xrightarrow{}(p^{\prime},q^{\prime})\mid
q\xrightarrow{a:c}q^{\prime}\in\Delta\\}$. These edges correspond to Adam
choosing a transition on his token, without playing a Joker

    4. 4.

$E_{J}=\\{(p^{\prime},q,a)\xrightarrow{}(p^{\prime},q^{\prime})\mid
p\xrightarrow{a:c}q^{\prime}\in\Delta\\}$. These edges correspond to Adam
playing a Joker and choosing a transition from the state of Eve’s token.

  * •

The priority function $\Omega$ is defined as follows: All elements in $E_{1}$
are assigned priority 0, while edges $(p,a,q)\xrightarrow{}(p^{\prime},q,a)$
in $E_{2}$ are assigned priority 2 if the transition
$\delta=p\xrightarrow{a:c}p^{\prime}$ in $\mathcal{B}$ is accepting (or
equivalently, $c=2$), and 0 otherwise. The edge
$(p^{\prime},q,a)\xrightarrow{}(p^{\prime},q^{\prime})$ in $E_{3}$ is assigned
priority 1 if the transition $q\xrightarrow{a:c}q^{\prime}$ is accepting, and
0 otherwise. The edges in $E_{J}$ are assigned priority 2.

Note that the above game has $\mathcal{O}(|\Sigma||Q|^{2})$ many vertices and
$\mathcal{O}(|\Sigma||Q||\Delta|)$ many edges with priorities in
$\\{0,1,2\\}$. Since such parity games with $n$ vertices and $m$ edges can be
solved in time $\mathcal{O}(mn)$ time [12, Theorem 11], we get that history-
determinism of a Büchi automaton can be decided in time
$\mathcal{O}(|\Sigma|^{2}|Q|^{3}|E|)$, an improvement from the
$\mathcal{O}(|\Sigma|^{2}|Q|^{4}|E|^{2})$ time of Bagnol and Kuperberg [2,
Theorem 12].

See 4.10

##  Appendix C Appendix for Section 5

###  C.1 Step-ahead Simulation

We start by showing that the relations of step-ahead simulation and sprint
simulation is transitive. The transitivity of step-ahead simulation is easier
to prove, as shown by the following lemma.

######  Lemma C.1.

Let $\mathcal{A}$, $\mathcal{B}$ and $\mathcal{C}$ be non-deterministic parity
automata such that $\mathcal{A}$ step-ahead simulates $\mathcal{B}$ and
$\mathcal{B}$ step-ahead simulates $\mathcal{C}$. Then $\mathcal{A}$ step-
ahead simulates $\mathcal{C}$.

######  Proof C.2.

Similar to Lemma 4.2, we can argue that the game arenas of the expanded game
arenas of step-ahead simulation game between $\mathcal{A}$ and $\mathcal{B}$,
and of simulation game between $\mathcal{A}$ and
${\mathsf{Delay}}(\mathcal{B})$ are equivalent. Thus, $\mathcal{A}$ simulates
${\mathsf{Delay}}(\mathcal{B})$ and $\mathcal{B}$ simulates
${\mathsf{Delay}}(\mathcal{C})$. Moreover, it is clear that
${\mathsf{Delay}}(\mathcal{B})$ simulates $\mathcal{B}$: in the simulation
game between ${\mathsf{Delay}}(\mathcal{B})$ and $\mathcal{B}$, Eve in
${\mathsf{Delay}}(\mathcal{B})$ in $(i+1)^{th}$ round can simply ‘copy’ Adam’s
transition on $\mathcal{B}$ in the $i^{th}$ round for each $i\geq 0$. All in
all, we have that $\mathcal{A}$ simulates ${\mathsf{Delay}}(\mathcal{B})$,
${\mathsf{Delay}}(\mathcal{B})$ simulates $\mathcal{B}$, and $\mathcal{B}$
simulates ${\mathsf{Delay}}(\mathcal{C})$. By transitivity of simulation, we
get that $\mathcal{A}$ simulates ${\mathsf{Delay}}(\mathcal{C})$, or
equivalently, $\mathcal{A}$ step-ahead simulates $\mathcal{C}$.

Let us recall the definition of sprint simulation for Büchi automata. See 5.1

We shall reduce sprint simulation between two Büchi automata to step-ahead
simulation between two _reachability automata_. These are restricted Büchi
automata where all the accepting transitions occur as self-loops on an
accepting sink state, and this sink state has accepting self-loops on all
letters in its alphabet.

For each non-deterministic Büchi automaton
$\mathcal{A}=(Q,\Sigma,q_{0},\Delta_{A})$, we construct the reachability
automaton $\mathcal{A}_{\\#}=(Q_{\\#},\Sigma_{\\#},q_{0},\Delta_{\\#})$ as
follows. The automaton $\mathcal{A}_{\\#}$ is over the alphabet
$\Sigma_{\\#}=\Sigma\cup\\{\\#\\}$ for some $\\#\notin\Sigma$. The set
$Q_{\\#}$ consists of the states $Q$ and two additional sink states $f$ and
$r$. The transitions $\Delta_{\\#}$ consists of all rejecting transitions in
$\Delta$, and the following additional transitions.

  1. 1.

Transitions $p\xrightarrow{a:1}f$ for all accepting transition
$p\xrightarrow{a:2}q$ in $\mathcal{A}$.

  2. 2.

Transitions $p\xrightarrow{\\#:1}r$ for each state $p$ in $Q$.

  3. 3.

Transitions $f\xrightarrow{a:2}f$ and $r\xrightarrow{a:1}r$ for each
$a\in\Sigma$.

The following lemma relates sprint simulation between two Büchi automata
$\mathcal{A}$ and $\mathcal{B}$ to step-ahead simulation between
$\mathcal{A}_{\\#}$ and $\mathcal{B}_{\\#}$.

######  Lemma C.3.

Given two Büchi automata $\mathcal{A}$ and $\mathcal{B}$, $\mathcal{A}$ sprint
simulates $\mathcal{B}$ if and only if $\mathcal{A}_{\\#}$ step-ahead
simulates $\mathcal{B}_{\\#}$.

######  Proof C.4.

$\Rightarrow.$ Observe that Eve taking an accepting transition on her token in
no later round than Adam in the sprint simulation game between $\mathcal{A}$
and $\mathcal{B}$ corresponds to Eve’s token reaching the state $f$ in no
later round than Adam’s in the step-ahead simulation game between
$\mathcal{A}_{\\#}$ and $\mathcal{B}_{\\#}$.

$\Leftarrow.$ Suppose Adam has a strategy to ensure that his token can take an
accepting transition on his token before Eve in the sprint simulation game
between $\mathcal{A}$ and $\mathcal{B}$. Then, Adam, by playing according to
the same strategy in the step-ahead simulation game between
$\mathcal{A}_{\\#}$ and $\mathcal{B}_{\\#}$, can ensure his token reaches $f$
before Eve’s token does. From here, he can select $\\#$ as letters for all the
future rounds, causing Eve’s run on her token to be rejecting while his run on
his token is accepting.

We utilise the above construction to prove Lemma 5.5 as well. See 5.5

######  Proof C.5.

It is clear that if $q$ is sprint deterministic, then $q$ sprint simulates
itself. Thus, let $q$ be a state such that $(\mathcal{H},q)$ step-ahead
simulates $(\mathcal{H},q)$. From Lemma C.3, this is equivalent to
$(\mathcal{H}_{\\#},q)$ step-ahead simulating itself, which in turn is
equivalent to the Eve winning the 1-token game on $(\mathcal{H}_{\\#},q)$.
Boker and Lehtinen have shown that $1$-token games characterises history-
determinism on reachability automata and HD reachability automata have
positional strategies in the history-determinism game which can be found in
polynomial time via $1$-token games [5, Theorems 4.8 and 4.10].

Fix an uniform positional strategy in the HD game from all states $q$ such
that $(\mathcal{H}_{\\#},q)$ is HD, and let $\mathcal{F}_{\\#}$ be the
deterministic subautomaton consisting of the transitions in this strategy. Let
$\mathcal{F}^{\prime}$ be the largest common subautomaton of $\mathcal{H}$ and
$\mathcal{F}_{\\#}$. Observe that for each state $q\in Q$ and letter
$a\in\Sigma$ such that there is a transition $q\xrightarrow{a:2}f$ in
$\mathcal{H}_{\\#}$, there is a transition $q\xrightarrow{a:2}p$ in
$\mathcal{H}$ by construction. Adding one such transition in
$\mathcal{F}^{\prime}$ for each such state and letter pair, we get a
deterministic subautomaton $\mathcal{F}$ of $\mathcal{H}$ that is a sprint
determinism witness for all states $q$ that sprint simulates itself, as
desired.

#### Formal description of $\mathcal{D}$

Let $\mathcal{H}$ be a history-deterministic automaton such that it is
semantically-deterministic, and for every state $p$ in $\mathcal{H}$, there is
a language equivalent state $q$ such that $p$ sprint simulates $q$. Fix the
subautomaton $\mathcal{F}$ from Lemma 5.5, and a positional Eve strategy
$\tau:Q\times\Sigma\times Q\xrightarrow{}\Delta$ for all pairs of states
$(p,q)$ such that $p$ sprint simulates $q$. Then, the deterministic automaton
$\mathcal{D}$ is constructed as follows.

  * •

The states of $\mathcal{D}$ consists of states $(p,q)$ that are pairs of
language-euivalent states in $\mathcal{H}$ such that $p$ sprint simulates $q$
and $q$ is sprint deterministic. We let the initial state $d_{0}$ to be
$(q_{0},p_{0})$ such that $p_{0}$ is sprint deterministic and $q_{0}$ sprint
simulates $r$.

  * •

Fix an ordering on the states of $\mathcal{H}$. $\mathcal{D}$ has the
following transition on reading the letter $a$ from a state $(q,p)$.

    * –

The transition $\delta(q,p)\xrightarrow{a:2}(q^{\prime},p^{\prime})$, if there
is an accepting transition $q\xrightarrow{a:2}q^{\prime}$ in $\mathcal{A}$,
where $p^{\prime}$ is the least state in the ordering such that $p^{\prime}$
is equivalent to $q^{\prime}$, $q^{\prime}$ sprint simulates $p^{\prime}$ and
$p^{\prime}$ is sprint deterministic.

    * –

Otherwise, the transition $(q,p)\xrightarrow{a:1}(q^{\prime},p^{\prime})$,
where $\tau(q,a,p)=(q\xrightarrow{a:1}q^{\prime})$ is the transition
prescribed by Eve’s sprint simulation strategy $\tau$, and
$p\xrightarrow{a:1}p^{\prime}$ is the unique transition from $p$ on $a$ in
$\mathcal{F}$.

###  C.2 Towards Automata with Stepahead Simulation

Recall that we call a history-deterministic Büchi automaton $\mathcal{H}$ good
if $\mathcal{H}$ is semantically-deterministic and Eve wins the Joker game
from all states in $\mathcal{H}$. We show that every history-deterministic
Büchi automaton can be converted to an equivalent good HD Büchi automaton in
polynomial time.

######  Lemma C.6.

Every history-deterministic Büchi automaton $\mathcal{H}$ has an equivalent
good history-deterministic Büchi automaton $\mathcal{H}_{N}$ as a subautomaton
which can be computed in polynomial time.

######  Proof C.7.

Fix a positional winning strategy $\tau$ for Eve on the Joker game of
$\mathcal{H}$. Consider the automaton $\mathcal{H}_{N}$ only consisting of
transitions that can be taken via Eve’s token in any play of the Joker game
where Eve is playing according to $\tau$. We shall show that $\mathcal{H}_{N}$
is good.

Since $\mathcal{H}_{N}$ consists of transitions that are used by a winning
strategy in the Joker game of $\mathcal{H}$ for Eve, it follows that Eve wins
the Joker game on $\mathcal{H}_{N}$. Furthermore, we claim that Eve wins the
Joker game from all states in $\mathcal{H}_{N}$. Suppose to the contrary that
there is a state $q$ in $\mathcal{H}_{N}$ such that Eve loses the Joker game
on $(\mathcal{H}_{N},q)$. Then, consider the play of the Joker game where Eve
is playing according to $\tau$ and Eve’s token reaches the state $q$, Adam
then plays Joker in the next round and plays to win the Joker game. Then, Adam
wins the Joker game, which is a contradiction since $\tau$ is a winning
strategy. We argue that the automaton $\mathcal{H}_{N}$ only consists of
language-preserving transitions similarly.

The automaton $\mathcal{H}_{N}$ is also equivalent to $\mathcal{H}$. Indeed,
for any word $w$ accepted in $\mathcal{H}$ with an accepting run $\rho$,
consider the play of the Joker game where Eve plays according to $\tau$ while
Adam moves his token according to $\rho$. Then, since $\tau$ is a winning
strategy, Eve’s run in her token is accepting. As the run of her token is
entirely contained in $\mathcal{H}_{N}$, we get that
$w\in\mathcal{L}(\mathcal{H}_{N})$.

Since a winning strategy for Eve in the Joker game on $\mathcal{H}$ can be
found in polynomial time, such an $\mathcal{H}_{N}$ can be constructed from
$\mathcal{H}$ in polynomial time.

Let us fix a good history-deterministic Büchi automaton $\mathcal{H}$. We
recall the iterative procedure presented in Section 5.2. We start by setting
$\mathcal{H}_{0}=\mathcal{H}$, and then do the following three steps on
$\mathcal{H}_{i}$ for each $i$ till we get
$\mathcal{H}_{i+1}=\mathcal{H}_{i}$.

  1. 1.

For vertices $(p,q)\in G_{1}(\mathcal{H}_{i})$, compute $\text{opt}_{i}(p)$ to
be the optimal-ranks of states in $G_{1}(\mathcal{H}_{i})$.

  2. 2.

Remove each transition $q\xrightarrow{a:1}q^{\prime}$ with
$\text{opt}_{i}(q)<\text{opt}_{i}(q^{\prime})$ in $\mathcal{H}_{i}$ to obtain
$\mathcal{H}^{\prime}_{i}$.

  3. 3.

Make each transition $q\xrightarrow{a:1}q^{\prime}$ with
$\text{opt}_{i}(q)>\text{opt}_{i}(q^{\prime})$ in $\mathcal{H}^{\prime}_{i}$
accepting, to obtain $\mathcal{H}_{i+1}$.

We will show that steps 2 and 3 preserves the invariants that
$\mathcal{H}^{\prime}_{i}$ and $\mathcal{H}_{i+1}$ are good and language-
equivalent to $\mathcal{H}_{i}$.

######  Lemma C.8.

$\mathcal{H}^{\prime}_{i}$ is good and
$\mathcal{L}(\mathcal{H}^{\prime}_{i},q)=\mathcal{L}(\mathcal{H}_{i},q)$ for
each state $q$ in $\mathcal{H}_{i}$.

######  Proof C.9.

Fix $\tau_{i}$ to be a rank-optimal Eve strategy in $G_{1}(\mathcal{H}_{i})$.
Let $q$ be a state in $\mathcal{H}_{i}$. We will first show that Eve wins the
step-ahead simulation game between $(\mathcal{H}^{\prime}_{i},q)$ and
$(\mathcal{H}_{i},q)$, by giving a winning strategy $\sigma$ for Eve. The
strategy $\sigma$ will require Eve to store in her memory a state $m$ in
$\mathcal{H}_{i}$, which we initialise to be $m=q$.

Throughout the play we will preserve the following two invariants.

  1. I1

The state of Eve’s token, Adam’s token, and Eve’s memory are all equivalent in
$\mathcal{H}_{i}$.

  2. I2

If Eve’s token and Eve’s memory are at the states $p_{j}$ and $m_{j}$
respectively, then $(p_{j},m_{j})$ is a vertex in $G_{1}(\mathcal{H}_{i})$,
i.e., $p_{j}$ and $m_{j}$ can be reached from the initial state $q_{0}$ upon
reading the same word.

Let us also fix a strategy $\pi$ for Eve in the step-ahead simulation game
between $(\mathcal{H}^{\prime}_{i},m)$ and $(\mathcal{H}^{\prime}_{i},q)$,
which we know exists since $m$ and $q$ are language-equivalent, and
$(\mathcal{H}^{\prime}_{i},m)$ is HD since Eve wins the Joker game on
$(\mathcal{H}^{\prime}_{i},m)$ (Theorem 4.9).

Eve then plays according to $\sigma$ as follows. At a position $(p_{j},q_{j})$
where Eve’s memory state is $m_{j}$, suppose Adam chooses the letter
$a_{j}\in\Sigma$. Let
$\delta_{j}=p_{j}\xrightarrow{a_{j}:c_{j}}p^{\prime}_{j}$ be the transition
prescribed by the rank-optimal strategy $\tau_{i}$. We will distinguish
between the following two cases.

  1. 1.

If $\delta_{j}$ is a transition in $\mathcal{H}^{\prime}_{i}$. Then Eve picks
the transition $p_{j}\xrightarrow{a_{j}:c_{j}}p^{\prime}_{j}$ in her token.
Eve updates her memory $m_{j+1}$ according to the transition prescribed by
$\pi$ in the step-ahead simulation game between
$(\mathcal{H}^{\prime}_{i},m_{j})$ and $(\mathcal{H}^{\prime}_{i},q_{j})$.

  2. 2.

If $\delta_{j}$ is not a transition in $\mathcal{H}^{\prime}_{i}$, i.e., it
has been removed from $\mathcal{H}_{i}$ to obtain $\mathcal{H}^{\prime}_{i}$.
Then, let $m^{\prime}$ be the state so that
$\text{opt}_{i}(p_{j})=\text{rank}_{i}(p_{j},m^{\prime})$. We then let Eve
pick the transition on $a_{j}$ prescribed by $\tau_{i}$ in the step-ahead
simulation game between $(\mathcal{H}_{i},p_{j})$ and
$(\mathcal{H}_{i},m^{\prime})$. As for the memory, we fix another step-ahead
simulation strategy $\pi^{\prime}$ between $(\mathcal{H}_{i},m^{\prime})$ and
$(\mathcal{H}_{i},q_{j})$. Eve will then update her memory according to
transition prescribed by $\pi^{\prime}$ on the letter $a_{j}$.

This concludes the description of the strategy $\sigma$ for Eve. To see that
this is a winning strategy, note that whenever Eve’s token takes a rejecting
transition in a play from the step-ahead simulation game between
$(\mathcal{H}^{\prime}_{i},p_{j})$ and $(\mathcal{H}_{i},q_{j})$, the quantity
$\text{rank}_{i}(p_{j},m_{j})$ is non-increasing, and strictly decreases if
Eve makes a move of the second kind.

If Adam constructs an accepting run on his token, then either Eve makes a move
of the second kind eventually, or the memory token takes an accepting
transition (since $\pi$ is a winning strategy). Both of these scenarios cause
the quantity $\text{rank}_{i}(p_{j},m_{j})$ to strictly decrease. Since
$\text{rank}(p_{j}.m_{j})$ is finite and cannot go below 0, Eve’s token will
take an accepting transition on her token in $\mathcal{H}^{\prime}_{i}$
eventually if Adam constructs an accepting run on his token. But then, we can
repeat this argument and use induction to show that Eve’s token will take an
accepting transition infinitely many times. Thus, Eve wins the step-ahead
simulation game between $(\mathcal{H}^{\prime}_{i},q)$ and
$(\mathcal{H}_{i},q)$.

Hence,
$\mathcal{L}(\mathcal{H}^{\prime}_{i},q)\supseteq\mathcal{L}(\mathcal{H}_{i},q)$,
and since $\mathcal{H}^{\prime}_{i}$ is obtained from $\mathcal{H}_{i}$ by
deleting transitions,
$\mathcal{L}(\mathcal{H}^{\prime}_{i},q)=\mathcal{L}(\mathcal{H}_{i},q)$. This
implies that $\mathcal{H}^{\prime}_{i}$ is also SD, since $\mathcal{H}_{i}$ is
SD. Furthermore, since $(\mathcal{H}^{\prime}_{i},q)$ step-ahead simulates
$(\mathcal{H}_{i},q)$, $(\mathcal{H}^{\prime}_{i},q)$ also step-ahead
simulates itself (recall that $\mathcal{H}^{\prime}_{i}$ is a subautotmaton of
$\mathcal{H}_{i}$), implying Eve wins the Joker game from every state in
$\mathcal{H}^{\prime}_{i}$. It follows that $\mathcal{H}^{\prime}_{i}$ is a
good history-deterministic Büchi automaton.

Note that the second step in the procedure ensures that the quantity
$\text{opt}_{i}$ is non-increasing across rejecting transitions. This can be
used to prove easily that $\mathcal{H}_{i+1}$ is good and language-equivalent
to $\mathcal{H}^{\prime}_{i}$.

######  Lemma C.10.

$\mathcal{H}_{i+1}$ is good and
$\mathcal{L}(\mathcal{H}_{i+1},q)=\mathcal{L}(\mathcal{H}^{\prime}_{i},q)$ for
each state $q$ in $\mathcal{H}^{\prime}_{i}$.

######  Proof C.11.

It suffices to show that a run is accepting in $\mathcal{H}_{i+1}$ if and only
if the same run is accepting in $\mathcal{H}^{\prime}_{i}$, since then one can
easily construct a winning strategy for Eve in the Joker game on
$\mathcal{H}_{i+1}$ from her winning strategy in the Joker game on
$\mathcal{H}^{\prime}_{i}$.

One direction is clear: if a run in $\mathcal{H}^{\prime}_{i}$ is accepting,
then the same run must be accepting in $\mathcal{H}_{i+1}$, since we only make
certain rejecting transitions accepting.

For the other direction, suppose that $\rho$ is an accepting run in
$\mathcal{H}_{i+1}$, and consider the same run $\rho$ in
$\mathcal{H}^{\prime}_{i}$. Note that the $\text{opt}_{i}$ values are non-
increasing across rejecting transitions, and for every transition
$\delta=q\xrightarrow{a:c}q^{\prime}$ such that $\delta$ is an accepting
transition in $\mathcal{H}_{i+1}$, the $\text{opt}_{i}$ value strictly
decreases. Thus, if $\rho$ has infinitely many accepting transitions in
$\mathcal{H}_{i+1}$, then $\rho$ must also have infinitely many accepting
transitions in $\mathcal{H}^{\prime}_{i}$ since $\text{opt}_{i}$ is bounded by
the size of the arena $G_{1}(\mathcal{H}^{\prime}_{i})$.

From Lemmas C.8 and C.10, we conclude that our iterative procedure maintains
the history-determinism, language and the property of the automaton being good
through its steps.