Reichman University, Herzliya, Israel and
<EMAIL_ADDRESS>Science Foundation grant 2410/22 Institute of Science and Technology Austria
(ISTA), Klosterneuburg, Austria and
<EMAIL_ADDRESS>CNRS, LIS, Aix-
Marseille Univ. and https://lehtinenkaroliina.wordpress.com/lehtinen@lis-
lab.fr0000-0003-1171-8790ANR QUASY 23-CE48-0008-01 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 and Centre for
Discrete Mathematics and Its Applications (DIMAP) U. Boker, T. A. Henzinger,
K. Lehtinen, and A. Prakash [500]Theory of computation Automata over infinite
objects 2 2 Conference of Very Important Things CVIT 2016 CVIT 2016 December
24–27, 2016 Little Whinging, United Kingdom 42 23

# History-Determinism vs Fair Simulation

Udi Boker  Thomas A. Henzinger  Karoliina Lehtinen  Aditya Prakash

###### Abstract

An automaton ${\mathcal{A}}$ is history-deterministic if its nondeterminism
can be resolved on the fly, only using the prefix of the word read so far.
This mild form of nondeterminism has attracted particular attention for its
applications in synthesis problems. An automaton ${\mathcal{A}}$ is guidable
with respect to a class $C$ of automata if it can fairly simulate every
automaton ${\mathcal{B}}$ in $C$, whose language is contained in that of
${\mathcal{A}}$. In other words, guidable automata are those for which
inclusion and simulation coincide, making them particularly interesting for
model-checking.

We study the connection between these two notions, and specifically the
question of when they coincide. For classes of automata on which they do,
deciding guidability, an otherwise challenging decision problem, reduces to
deciding history-determinism, a problem that is starting to be well-understood
for many classes.

We provide a selection of sufficient criteria for a class $C$ of automata to
guarantee the coincidence of the notions, and use them to show that the
notions coincide for the most common automata classes, among which are
$\omega$-regular automata and many infinite-state automata with safety and
reachability acceptance conditions, including vector addition systems with
states, one-counter nets, pushdown-, Parikh-, and timed-automata.

We also demonstrate that history-determinism and guidability do not always
coincide, for example, for the classes of timed automata with a fixed number
of clocks.

###### keywords:

History-Determinism

###### category:

##  1 Introduction

Language inclusion between automata is a key problem in verification: given an
automaton representing a program and another representing a specification,
language inclusion of the former in the latter captures precisely whether all
executions of the program satisfy the specification. Unfortunately, in the
presence of nondeterminism, inclusion is algorithmically hard. For instance,
for regular automata it is PSpace-hard on both finite and infinite words.

Fair simulation is a more syntactic approximation of inclusion, defined by the
simulation game [13]. In this game, one player, in the role of the spoiler,
builds, transition by transition, a run in one of the automata, say
${\mathcal{A}}$, while the other, in the role of the duplicator, chooses at
each turn a matching transition in the other automaton, say ${\mathcal{B}}$.
The second player’s task is to build a run that is accepting if the first
player’s run is accepting. If the duplicator has a winning strategy, then
${\mathcal{B}}$ is said to simulate ${\mathcal{A}}$, which, in particular,
implies that ${\mathcal{A}}$’s language is included in ${\mathcal{B}}$’s
language. Simulation, due to its local and syntactic nature, is generally
easier to check than inclusion: for instance it is in PTime for
nondeterministic Büchi automata. As a result, automata for which language
inclusion and simulation coincide are particularly well-suited for model-
checking. We call such automata guidable, after a similar notion used
previously as an alternative to determinism for tree automata [9]. Despite
their clear usefulness for model checking, guidable automata have so far been
mostly used as a tool, but not studied much in their own right, with the
notable exception of [19].

Guidability is not easy to decide: it is contingent on an automaton simulating
a potentially infinite number of language-included automata. We would like to
have, whenever possible, a characterisation that is more amenable to
algorithmic detection.

Deterministic automata are of course always guidable, and so are history-
deterministic automata. These are mildly nondeterministic automata, in which
nondeterministic choices are permitted, but can only depend on the word read
so far, rather than the future of the word. These automata have received a
fair bit of attention recently due, in particular, to their applications in
synthesis problems [6]. In general, they offer an interesting compromise
between the power of nondeterministic automata and the better algorithmic
properties of deterministic ones. In particular, they can simulate all
equivalent, or language-contained, automata as they only need the history to
resolve nondeterministic choice in the best possible way—in other words, they
are guidable. In fact, at first it might appear that history-determinism and
guidability should coincide; indeed, this is the case if we consider
guidability with respect to all labelled transition systems [14, Theorem 4].
However, there are also classes of automata for which this is not the case.

Guidability and history-determinism coinciding on a class $C$ of automata is
equivalent to the description “for every automaton ${\mathcal{A}}\in C$ that
is not history-deterministic, there is some ${\mathcal{A}}^{\prime}\in C$ that
is language-included in ${\mathcal{A}}$ but that ${\mathcal{A}}$ does not
simulate” (D). Then it is easy enough to hand-pick automata to build classes
where guidability and history-determinism do not coincide (for example, a
class of inclusion-incomparable automata that are not all history-
deterministic). However, as we will see, there are also more natural classes
of automata, such as timed automata with a bounded number of clocks, for which
guidability and history-determinism differ.

The characterisation (D) is too abstract to be much use for analysing the
usual automata classes we are interested in. We therefore prove that several
more concrete criteria (Theorem 1.1) imply that guidability and history-
determinism coincide, and use each of these in a comprehensive analysis of
standard automata classes. Roughly, each of the criteria describes some
sufficient closure properties which guarantee the existence of
${\mathcal{A}}^{\prime}$ from description (D). If some automaton can simulate
another automaton that is sufficiently difficult to simulate (for example a
deterministic one, since they simulate all equivalent automaton), then it must
be history-deterministic; as a result, a class of automata having sufficient
closure properties (such as closure under determinisation), implies that
guidability and history-determinism coincide. The challenge is to identify,
for a variety of different classes of automata $C$, an automaton that is
sufficiently difficult to simulate, while remaining in $C$.

In order to discuss our sufficient criteria in more detail, we need to start
with a couple of key notions, the first of which is the 1-token game and the
second is the 1-token ghost.

History-determinism of an automaton is tricky and expensive to decide directly
[12]; As an alternative, Bagnoal and Kuperberg used $k$-token games as
potential characterisations for history-determinism [2]. Roughly, they
resemble a (fair) simulation-like game, played on a single automaton, where
one player, Eve (in the role of Duplicator), must build transition-by-
transition a run on a word dictated letter-by-letter by Adam, who, after each
of Eve’s choices, also builds $k$ runs transition-by-transition. Eve then wins
if her run is accepting whenever Adam’s run is accepting. Bagnol and Kuperberg
showed that for Büchi automata, the $2$-token game indeed characterises
history-determinism, which means that deciding history-determinism for Büchi
automata is in PTime [2]. Since then, the $1$\- or $2$-token games have been
shown to characterise history-determinism for various automata classes,
including coBüchi [4], ${\mathsf{DSum}}$, ${\mathsf{LimInf}}$, and
${\mathsf{LimSup}}$ automata [5]. These games contrast with the letter game, a
game which always characterises history-determinism, but which is often
challenging to solve directly [12].

In this work, we make heavy use of token-games, this time to understand the
connection between history-determinism and guidability. In particular, we
extend token games to be played over two automata (Definition 3.2), separating
between Eve’s and Adam’s automata, and define, given an automaton
${\mathcal{A}}$, that an automaton ${\mathcal{A}}^{\prime}$ is a $1$-token
ghost of ${\mathcal{A}}$ if ${\mathcal{A}}^{\prime}$ is language-equivalent to
${\mathcal{A}}$ and Eve wins the $1$-token game between
${\mathcal{A}}^{\prime}$ and ${\mathcal{A}}$. For some classes of automata
such a ghost is easy to construct, while for other classes it might not exist
due to lacking closure properties.

With these notions, we can now state our criteria.

######  Theorem 1.1.

The notions of history-determinism and guidability coincide for a class $C$ of
labelled transitions systems (LTSs) if at least one of the following holds:

  1. 1.

_Determinisation._ $C$ is closed under history-determinism, i.e., for each
nondeterministic LTS in $C$, there is a language-equivalent history-
deterministic (or deterministic) LTS in $C$ as well. (Lemma 4.1)

  2. 2.

_$1$ -token ghost._ $1$-token games characterise history-determinism in $C$,
and $C$ is closed under $1$-token ghost. (Lemma 4.6)

  3. 3.

_Strategy ghost._ For every ${\mathcal{A}}\in C$ that is not history-
deterministic, there is a deterministic LTS ${\mathcal{B}}$ over the alphabet
of transitions of ${\mathcal{A}}$, such that ${\mathcal{B}}$ recognises the
plays of a winning strategy of Adam in the letter game on ${\mathcal{A}}$, and
${\mathcal{B}}$, projected onto the alphabet of ${\mathcal{A}}$, has a
$1$-token ghost in $C$. (Lemma 4.8)

We prove the criteria of Theorem 1.1 in Section 4, and use them in Section 5
to show that the notions of history-determinism and guidability coincide for
numerous classes of automata, listed in Section 1. We also provide counter-
examples of classes for which history-determinism and guidability do not
coincide, as listed in Section 1, and elaborated on in Section 6. We restrict
our analysis to automata over infinite words, which are better behaved in this
context, and discuss how to adapt our techniques for finite words in Section
7.

Automata Class |  HD = Guidability by
---|---
$\omega$-regular |  _Determinisation_
Fixed-index parity (e.g., Büchi), Weak |  _Strategy ghost_ Corollary 5.1
Linear |  _Strategy ghost_ Theorem 5.13. (Not ghost-closed Theorem 5.11)
Safety & Reachability |
pushdown automata, VASS, timed, one-counter automata, one-counter net, Parikh |  _$1$ -token ghost_
Theorems 5.9 and 5.6 |
VPA with any $\omega$-regular acceptance condition |  _Strategy ghost_ Theorem 5.7
Classes for which $\mathrm{HD}$ $\neq$ guidability:
\- Büchi automata with a bounded number of states. Theorem 6.1
\- Timed automata with a bounded number of clocks. Theorem 6.2
Notable classes for which we leave the question $\mathrm{HD}$ $=$ ?
guidability open:
\- PDA/OCA/OCN/Timed automata with general $\omega$-regular acceptance

Table 1: History-determinism vs guidability

A practical corollary of our result is that guidability is decidable, with the
complexity of deciding history-determinism, for $\omega$-regular automata
(ExpTime for parity automata, PTime for Büchi and coBüchi), safety and
reachability timed automata (ExpTime) and visibly pushdown automata (ExpTime).
For details on the complexity of these procedures, we refer the reader to a
recent survey [6].

##  2 Preliminaries

We use $\mathbb{N}$ and $\mathbb{N}^{+}$ to denote the set of non-negative and
positive integers respectively. We use $[i..j]$ to denote the set
$\\{i,\ldots,j\\}$ of integers, and $[i]$ for the set $[1..i]$. An alphabet
$\Sigma$ is a non-empty set of letters. A finite or infinite word is a finite
or infinite sequence of letters from $\Sigma$ respectively. We let
$\varepsilon$ be the empty word, and $\Sigma_{\varepsilon}$ the set
$\Sigma\cup\\{\varepsilon\\}$. The set of all finite (resp. infinite) words is
denoted by $\Sigma^{*}$ (resp. $\Sigma^{\omega}$). A _language_ is a set of
words.

###  2.1 Labelled transition systems

A _labelled transition system_ (LTS)
${\mathcal{A}}=(\Sigma,Q,\iota,\Delta,\alpha)$ consists of a potentially
infinite alphabet $\Sigma$, a potentially infinite state-space $Q$, an initial
state $\iota\in Q$, a labelled transition relation $\Delta\subseteq
Q\times\Sigma_{\varepsilon}\times Q$, and a set of accepting runs $\alpha$,
where a run $\rho$ is a (finite or infinite) sequence of transitions starting
in $\iota$ and following $\Delta$. We may write
$q\xrightarrow[]{\sigma}q^{\prime}$ instead of
$(q,\sigma,q^{\prime})\in\Delta$ for $\sigma\in\Sigma_{\varepsilon}$. Given a
finite run
$\rho=q_{0}\xrightarrow{\sigma_{1}}q_{1}\xrightarrow{\sigma_{2}}\cdots\xrightarrow{\sigma_{k}}q_{k}$
on the word
$v=\sigma_{0}\cdot\sigma_{1}\cdot\sigma_{2}\cdots\sigma_{k}\in\Sigma_{\varepsilon}^{k+1}$,
we write $q_{0}\xRightarrow{v,\rho}q_{k}$ to denote that $\rho$ is a
transition sequence on the word $v$ that starts at $q_{0}$ and ends at
$q_{k}$. An LTS is _deterministic_ if for every state $q$ and letter
$\sigma\in\Sigma$, there is at most one transition
$q\xrightarrow{\sigma}q^{\prime}$ from $q$ on the $\sigma$, and there are no
transitions on $\varepsilon$.

A word $w\in\Sigma^{\omega}$ is accepted by an LTS ${\mathcal{A}}$ if there is
an accepting run of ${\mathcal{A}}$ on $w$. The language $L({\mathcal{A}})$ of
${\mathcal{A}}$ is the set of words that it accepts. An LTS ${\mathcal{A}}$ is
contained in an LTS ${\mathcal{B}}$, denoted by
${\mathcal{A}}\leq{\mathcal{B}}$, if $L({\mathcal{A}})\subseteq
L({\mathcal{B}})$, while ${\mathcal{A}}$ and ${\mathcal{B}}$ are equivalent,
denoted by ${\mathcal{A}}\equiv{\mathcal{B}}$ if
$L({\mathcal{A}})=L({\mathcal{B}})$.

A _transducer_ is like an LTS without acceptance condition and
$\varepsilon$-transitions but with an output labelling: it is given by a tuple
$(\Sigma_{I},\Sigma_{O},Q,\iota,\Delta,\gamma)$, where $\Sigma_{I}$ and
$\Sigma_{O}$ are the input and output alphabets, respectively,
$\Delta\subseteq Q\times\Sigma_{I}\times Q$ is the transition relation, and
$\gamma:\Delta\to\Sigma_{O}$ is the output function. A _strategy_ in general
is a deterministic transducer. It is finite memory if the transducer has a
finite state space.

###  2.2 Automata

We briefly recall the automata types considered here, which we assume to
operate on infinite words unless stated otherwise, and leave the formal
definitions to the appendix.

LTSs are represented concisely by various automata. An automaton
${\mathcal{A}}$ induces an LTS ${\mathcal{B}}$, whose states are the
configurations of ${\mathcal{A}}$, and whose runs are the same as
${\mathcal{A}}$’s runs. If ${\mathcal{A}}$’s states and configurations are the
same, as is the case with $\omega$-regular automata which we define below,
then ${\mathcal{B}}$ is identical to ${\mathcal{A}}$, but with the acceptance
condition given by a set of runs (as opposed to an $\omega$-regular
conditions). If the configurations of ${\mathcal{A}}$ contain additional data,
as is the case for example with pushdown automata, then ${\mathcal{B}}$ and
${\mathcal{A}}$ have different states. Notice that ${\mathcal{A}}$ is
deterministic iff ${\mathcal{B}}$ is. The acceptance condition of
${\mathcal{A}}$ induces the acceptance condition on ${\mathcal{B}}$.

In a parity condition, $\alpha$ assigns priorities in $\mathbb{N}$ to either
states or transitions, and a run is accepting if the highest priority that
occurs infinitely often along it is even. An $[i,j]$-parity automaton, for
$i<j$ two natural numbers is a parity automaton whose priorities are in
$[i,j]$. A parity automaton is said to be a _weak automaton_ if there is no
cycle in the automaton containing both an even and odd priority. In a
reachability condition, some states are labelled final; a run accepts if it
reaches a final state. In a safety automaton, some states are labelled safe; a
run accepts if it remains within the safe region.

In a nondeterministic $\omega$-regular automaton
$(\Sigma,Q,\iota,\delta,\alpha)$, $\Sigma$ and $Q$ are finite, and the
acceptance condition $\alpha$ is based on the set of states (or transitions)
visited infinitely often along a run. A timed automaton (TWA)
$(\Sigma,Q,\iota,C,\delta,\alpha)$ has a set of clocks $C$ and its transitions
are guarded by inequalities between the clock values and can reset clocks. It
reads timed words, which consist of letters of a finite alphabet $\Sigma$
paired with delays from $\mathbb{R}$. A timed automaton recognises a timed
language, for example “at some point an event occurs twice exactly one time-
unit apart.”

We also handle pushdown automata, one-counter automata, vector addition
systems with states, one-counter nets and Parikh automata with reachability
and safety acceptance. We define these classes of infinite state systems
uniformly in Section 5.2 as classes of finite state automata with transitions
that modify an infinite content space. A visibly pushdown automaton (VPA) is a
pushdown automaton without $\varepsilon$-transitions, in which the input
alphabet is partitioned into $\textsf{pop},\textsf{push}$ and noop letters
that induce only transitions that $\textsf{pop},\textsf{push}$ and have no
effect on the stack respectively.

##  3 History-determinism, simulation and related games

Different simulation-like games that capture either a relationship between
automata or properties of a single automaton are at the heart of our technical
developments. In this section we go over the various games—both known and
newly defined—that will be played throughout this article, and which allow us
to connect guidability and history-determinism. These games are all based on
Adam (the spoiler) building a word letter by letter, and potentially a run in
an automaton over that word, while his opponent Eve (the duplicator) tries to
build a single accepting run transition by transition. The differences between
these games are based on whether they are played on one or two automata,
whether Adam picks transitions, and if so, whether he does it before Eve. The
winning condition is similar in all cases: Eve’s run must be accepting
whenever Adam’s run is accepting, or if Adam does not have a run, then
whenever the word built by Adam’s moves is in the language of a specified
automaton. This results in three styles of games: (i) simulation games, played
on two automata, in which Adam plays before Eve, and each builds a run in
their respective automaton; (ii) token-games, which can be played on one or
two automata, in which Adam first declares the letter, and then Eve plays her
transition before Adam plays his; and (iii) the letter game, played on a
single automaton, in which Adam only chooses letters and does not build a run
at all.

Fair simulation between two LTSs (or automata) is captured by the simulation
game defined below:

######  Definition 3.1 (Simulation game).

Consider LTSs ${\mathcal{A}}=(\Sigma,Q_{A},\iota_{A},\Delta_{A},\alpha_{A})$
and ${\mathcal{B}}=(\Sigma,Q,\iota_{B},\Delta_{B},\alpha_{B})$. The simulation
game $Sim({\mathcal{B}},{\mathcal{A}})$ between ${\mathcal{B}}$ and
${\mathcal{A}}$ is a two player-game played between Adam and Eve with
positions in $Q_{A}\times Q_{B}$ which starts at the position
$(p_{0},q_{0})=(\iota_{A},\iota_{B})$. At round $i$ of the play, for $i\geq
0$, when the position is $(p_{i},q_{i})$:

  * •

Adam picks $\sigma_{i}\in\Sigma$ and a transition (or transition sequence, in
the presence of $\varepsilon$-transitions)
$p_{i}\xRightarrow{\sigma_{i},\rho_{i}}p_{i+1}$ in ${\mathcal{A}}$;

  * •

Eve picks a transition (or transition sequence, in the presence of
$\varepsilon$-transitions)
$q_{i}\xRightarrow{\sigma_{i},\rho^{\prime}_{i}}q_{i+1}$ in ${\mathcal{B}}$;
they proceed from $(p_{i+1},q_{i+1})$.

An infinite play produces a run $\rho_{A}$ in ${\mathcal{A}}$ consisting of
transitions chosen by Adam and a run $\rho_{E}$ in ${\mathcal{B}}$ of
transitions chosen by Eve, both on $\sigma_{0}\sigma_{1}\sigma_{2}\cdots$. We
say that Eve wins the play if $\rho_{E}$ is accepting or $\rho_{A}$ is
rejecting.

If Eve has a winning strategy in this game, we say that ${\mathcal{B}}$
simulates ${\mathcal{A}}$, denoted by $Sim({\mathcal{B}},{\mathcal{A}})$. It
is easy to observe that if ${\mathcal{B}}$ simulates ${\mathcal{A}}$, then
$L({\mathcal{A}})\subseteq L({\mathcal{B}})$. An LTS ${\mathcal{A}}$ is
_guidable_ with respect to a class $C$ of LTSs if ${\mathcal{A}}$ simulates
every LTS ${\mathcal{A}}^{\prime}$ in $C$ that satisfies
$L({\mathcal{A}}^{\prime})\subseteq L({\mathcal{A}})$.

The following _letter game_ based definition of history-determinism, was
introduced by Henzinger and Piterman [12], and coincides with Colcombet’s
notion of translation strategies [8].

Given an LTS ${\mathcal{A}}$, the letter game on ${\mathcal{A}}$, denoted by
$\mathrm{HD}({\mathcal{A}})$ is similar to the simulation game except that
instead of playing transitions in an automaton, Adam just chooses letters and
builds a word $w$, letter by letter, which should be in the language of
${\mathcal{A}}$, while Eve tries to build a run of ${\mathcal{A}}$ over $w$.
More precisely, the letter game starts with Eve’s token at the initial state
$\iota$, and proceeds in rounds. At round $i$, where Eve’s token is at
$q_{i}$:

  * •

Adam chooses a letter $\sigma_{i}$ in the alphabet $\Sigma$ of
${\mathcal{A}}$;

  * •

Eve chooses a transition $q_{i}\xrightarrow[]{\sigma_{i}}q_{i+1}$ (or a
transition sequence $q_{i}\xRightarrow{\sigma_{i},\rho_{i}}q_{i+1}$ in the
presence of $\varepsilon$-transitions) of ${\mathcal{A}}$ over $\sigma_{i}$;
Eve’s token moves to $q_{i+1}$.

In the limit, a play consists of the word $w=\sigma_{0}\sigma_{1}\cdots$ and
the run $\rho=\rho_{0}\cdot\rho_{1}\cdot\rho_{2}\cdots$. Eve wins the play if
$w\notin L({\mathcal{A}})$ or $\rho$ is accepting. We say that ${\mathcal{A}}$
is history-deterministic ($\mathrm{HD}$) if Eve has a winning strategy in the
letter game over ${\mathcal{A}}$.

Token games are known to characterise history-determinism on various classes
of automata [2, 5, 6]. We generalise token games to be played on two LTSs
below, which makes them more akin to a variation of simulation. This will help
us relate simulation and history-determinism in Section 4. We only use the
$1$-token version here.

######  Definition 3.2 ($1$-token games over two LTSs (or automata)).

Consider LTSs ${\mathcal{A}}^{\prime}$ and ${\mathcal{A}}$ with initial states
$p_{0}$ and $q_{0}$ respectively. In the $1$-token game on
${\mathcal{A}}^{\prime}$ and ${\mathcal{A}}$ denoted by
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$, Eve has a token with which she
constructs a run in ${\mathcal{A}}^{\prime}$, and Adam has a token with which
he constructs a run in ${\mathcal{A}}$. The game proceeds in rounds, and at
round $i$ of the play with token positions $(p_{i},q_{i})$, for each $i\geq
0$:

  * •

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

  * •

Eve chooses a transition (or a transition sequence, in the presence of
$\varepsilon$-transitions)
$p_{i}\xRightarrow{\sigma_{i},\rho^{\prime}_{i}}p_{i+1}$ in
${\mathcal{A}}^{\prime}$;

  * •

Adam chooses a transition (or transition sequence, in the presence of
$\varepsilon$-transitions) $q_{i}\xRightarrow{\sigma_{i},\rho_{i}}q_{i+1}$;
the game proceeds from $(p_{i+1},q_{i+1})$.

An infinite play produces a word $w=\sigma_{0}\dots$, a sequence of
transitions $\rho_{E}$ of ${\mathcal{A}}^{\prime}$ chosen by Eve, and a
sequence of transitions $\rho_{A}$ in ${\mathcal{A}}$ chosen by Adam. Eve wins
if $\rho_{E}$ is accepting or if $\rho_{A}$ is rejecting.

A strategy for Eve here is a function
$\mathsf{s}:(\Delta^{+})^{*}\times\Sigma\to(\Delta^{\prime})^{*}$, where
$\Sigma$ is the alphabet of ${\mathcal{A}}$ and ${\mathcal{A}}^{\prime}$, and
$\Delta$ and $\Delta^{\prime}$ are the sets of transitions of ${\mathcal{A}}$
and ${\mathcal{A}}^{\prime}$, respectively. When clear from context,
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$ also denotes the claim that Eve
has a winning strategy in the game
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$. As an automaton and its induced
LTS have the same runs, $G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$ holds
for automata ${\mathcal{A}}$ and ${\mathcal{A}}^{\prime}$ iff it holds for
their induced LTSs. We also write $G_{1}({\mathcal{A}})$ for
$G_{1}({\mathcal{A}},{\mathcal{A}})$.

Note that the $1$-token game and the simulation game differ in one key aspect:
in the simulation game, Adam plays first, and Eve can use the information of
the transition to inform her choice, while in the $1$-token game, Eve must
choose her transition based only on the letter chosen by Adam, who plays his
transition after Eve.

##  4 Criteria for when History-Determinism = Guidability

We now provide criteria which guarantee that history-determinism and
guidability coincide for a class of LTSs. In Section 5, we use these to show
the coincidence of the two notions for many standard automata classes.

###  4.1 Closure under (history-)determinism

A first observation is that if every LTS ${\mathcal{A}}$ can be determinised
within the class $C$, or even if there exists an equivalent $\mathrm{HD}$ LTS
${\mathcal{A}}^{\prime}$ within $C$ then ${\mathcal{A}}$ is $\mathrm{HD}$ if
and only if it is guidable.

######  Lemma 4.1.

History-determinism and guidability coincide for any class $C$ of LTSs in
which the languages expressed by history-deterministic (or deterministic) LTSs
are the same as languages expressed by nondeterministic LTSs.

The proof is simple: one direction is trivial ($\mathrm{HD}$ always implies
guidability) and conversely, if an automaton ${\mathcal{A}}$ is not
$\mathrm{HD}$, then it cannot simulate any equivalent $\mathrm{HD}$ automaton,
implying that ${\mathcal{A}}$ is not guidable.

Various examples of such classes are provided in Section 5.1, as summarised in
Section 1. In particular, the general class of all labelled-transition systems
[14], safety/reachability visibly pushdown automata [1], as well as finite-
state automata on finite words (NFAs), and co-Büchi, Parity, Rabin, Streett,
and Muller automata on infinite words. Yet, this is not the case for Büchi
automata or parity automata with a fixed parity index. History-determinism is
also strictly less expressive than nondeterminism for pushdown automata,
Parikh automata, timed automata and one-counter nets.

###  4.2 Via token games

For classes that are not closed under determinisation, we have to find some
other type of automaton that is difficult to simulate. To do so, we revisit
token games, previously used to help decide history-determinism, to relate
history-determinism and guidability. Recall that we extended the definition of
$1$-token games, so that they are played on two automata, rather than one. In
the next definition, we use this extended notion of $1$-token game to
identify, for each automaton ${\mathcal{A}}$, an automaton
${\mathcal{A}}^{\prime}$ such that Eve wins the the $1$-token game on
${\mathcal{A}}$ if and only if ${\mathcal{A}}$ simulates
${\mathcal{A}}^{\prime}$.

######  Definition 4.2 (1-token ghost).

An LTS (or an automaton) ${\mathcal{A}}^{\prime}$ is a _$1$ -token ghost_ of
an LTS ${\mathcal{A}}$, denoted by
$\textsf{1-TokenGhost}({\mathcal{A}}^{\prime},{\mathcal{A}})$, if
${\mathcal{A}}^{\prime}\equiv{\mathcal{A}}$ and
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$.

To show that the ghost automaton has the property that
$Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$ if and only if Eve wins
$G_{1}({\mathcal{A}},{\mathcal{A}})$, we compose the strategies in
$Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$ and
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$.

######  Lemma 4.3.

Consider LTSs ${\mathcal{A}}$ and ${\mathcal{A}}^{\prime}$, such that
${\mathcal{A}}$ simulates ${\mathcal{A}}^{\prime}$ and
$\textsf{1-TokenGhost}({\mathcal{A}}^{\prime},{\mathcal{A}})$. Then Eve wins
$G_{1}({\mathcal{A}})$.

######  Proof 4.4.

Let $s_{sim}$ be a winning strategy of Eve in the simulation game between
${\mathcal{A}}$ and ${\mathcal{A}}^{\prime}$, and $s^{\prime}$ her winning
strategy in $G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$. Eve then has a
winning strategy $s$ in $G_{1}({\mathcal{A}})$: she plays the strategy
$s_{sim}$ in $Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$ against her imaginary
friend Berta, who plays the strategy $s^{\prime}$ in
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$ against Adam. In more detail: In
each round $i$ of the game $G_{1}({\mathcal{A}})$, Adam chooses a transition
sequence $\rho_{i-1}$ in ${\mathcal{A}}$ on $\sigma_{i-1}$ (except for the
first round) on his token and a letter $\sigma_{i}$, then Berta chooses the
transition sequence
$\rho^{B}_{i}=s^{\prime}\left(\rho_{0}\ldots\rho_{i-1},\sigma_{i}\right)$ over
the letter $\sigma_{i}$ in ${\mathcal{A}}^{\prime}$ on her token in
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$, and then Eve chooses the
transition sequence $\rho_{i}=s_{sim}(\rho^{B}_{0}\ldots\rho^{B}_{i-1})$ in
${\mathcal{A}}$.

The run built by Eve with the strategy $s$ is accepting if the run built by
Berta is, which is in turn accepting if Adam’s run is. Hence, $s$ is a winning
strategy for Eve in $G_{1}({\mathcal{A}})$.

Then, for classes in which token games characterise history-determinism and
which are closed under the ghost relation, guidability and history-determinism
coincide.

######  Definition 4.5.

A class $C$ of LTSs is _closed under $1$-token ghost_ if for every
${\mathcal{A}}\in C$ there exists ${\mathcal{A}}^{\prime}\in C$ such that
$\textsf{1-TokenGhost}({\mathcal{A}}^{\prime},{\mathcal{A}})$.

######  Lemma 4.6.

Given a class $C$ of LTSs closed under $1$-token ghost for which $G_{1}$
characterises history-determinism, history-determinism and guidability
coincide for $C$.

######  Proof 4.7.

Being $\mathrm{HD}$ always implies guidability, so one direction is easy. For
the other direction, if ${\mathcal{A}}$ simulates every LTS
${\mathcal{A}}^{\prime}\in C$, such that
${\mathcal{A}}^{\prime}\leq{\mathcal{A}}$, then in particular it simulates an
LTS ${\mathcal{A}}^{\prime}\in C$, such that
$\textsf{1-TokenGhost}({\mathcal{A}}^{\prime},{\mathcal{A}})$, as $C$ is
closed under the $1$-token ghost. By Lemma 4.3, Eve wins
$G_{1}({\mathcal{A}})$, implying that ${\mathcal{A}}$ is $\mathrm{HD}$, as
$G_{1}$ characterises history-determinism in $C$.

A $1$-token ghost is often easy to build, by delaying nondeterministic choices
by one letter (Definition 5.3), as shown in Section 5.2 for pushdown automata,
one-counter automata, vector addition system with states, one-counter nets and
Parikh automata.

For some automata classes, however, showing closure under $1$-token ghosts is
trickier: for VPA the stack action must occur as the letter is read, and for
timed automata configuration updates are sensitive to the current timestamp.
We handle these complications in Section 5.3. We can also only use Lemma 4.6
with respect to automata classes for which $1$-token games characterise
history-determinism, which is not the case for parity automata or $\omega$-VPA
[2].

###  4.3 Via Adam’s strategy in the letter game

As we will see in detail in Section 5.4, some classes, such as linear
automata, are neither closed under $1$-token ghost nor determinisation, so
there is no hope for the above criteria to apply. Our final criterion is an
alternative which, instead of requiring all automata to admit a $1$-ghost,
builds a difficult-to-simulate automaton from Adam’s winning strategy in the
letter game. The intuition is that Adam’s winning strategy in the letter game
on an automaton ${\mathcal{A}}$ captures behaviour that is difficult for
${\mathcal{A}}$ to simulate, so if we can turn Adam’s strategy into an
automaton (which will be language-contained in ${\mathcal{A}}$ since Adam must
play a word in the language of ${\mathcal{A}}$), then this automaton will not
be simulated by ${\mathcal{A}}$. To build this automaton, we first project an
automaton ${\mathcal{B}}$ recognising Adam’s winning plays from his strategy
onto the alphabet of ${\mathcal{A}}$, to obtain an automaton
${\mathcal{B}}_{\Sigma}$ that recognises the words played by Adam’s strategy.
Then, by taking the $1$-token ghost of ${\mathcal{B}}_{\Sigma}$, we obtain an
automaton ${\mathcal{B}}^{\prime}$ against which the simulation game is
essentially the letter game against Adam’s strategy. If the resulting
automaton is always still in the class $C$, guidability and history-
determinism coincide.

######  Lemma 4.8.

History-determinism and guidability coincide for classes $C$ of LTSs in which,
for each ${\mathcal{A}}\in C$ that is not history-deterministic, there is a
deterministic LTS ${\mathcal{B}}$ over the alphabet of transitions of
${\mathcal{A}}$ that recognises the plays of a winning strategy of Adam in the
letter game on ${\mathcal{A}}$, and ${\mathcal{B}}$, projected onto the
alphabet of ${\mathcal{A}}$, has a $1$-token ghost in $C$.

######  Proof 4.9.

Consider a winning strategy $\tau$ of Adam in the letter game on
${\mathcal{A}}$, and let ${\mathcal{B}}$ be a deterministic LTS that
recognises the plays of $\tau$, seen as runs of ${\mathcal{A}}$. Let
${\mathcal{B}}_{\Sigma}$ be the projection of ${\mathcal{B}}$ onto $\Sigma$:
it is otherwise like ${\mathcal{B}}$, except that its alphabet is $\Sigma$
instead of the transitions $\Delta_{\mathcal{A}}$ of ${\mathcal{A}}$ and as a
result it has additional nondeterminism. Crucially, every transition in
${\mathcal{B}}$ is still a transition in ${\mathcal{B}}_{\Sigma}$. Given a
sequence of transitions $t_{0}t_{1}\dots t_{i}\in\Delta_{\mathcal{A}}^{*}$, we
call $t^{\prime\prime}_{0}t^{\prime\prime}_{1}\dots t^{\prime\prime}_{i}$ its
run in ${\mathcal{B}}$, which is uniquely defined since ${\mathcal{B}}$ is
deterministic. Note that this sequence of transitions is also a run over the
word of $t_{0}t_{1}\dots t_{i}$ in ${\mathcal{B}}_{\Sigma}$. This also extends
to infinite sequences. Since every run accepted by ${\mathcal{B}}$ is a play
winning for Adam in the letter game over ${\mathcal{A}}$, their projection
onto $\Sigma$ must be in $L({\mathcal{A}})$, so
$L({\mathcal{B}}_{\Sigma})\subseteq L({\mathcal{A}})$.

Now, let ${\mathcal{B}}^{\prime}$ be the $1$-token ghost of
${\mathcal{B}}_{\Sigma}$, witnessed by a strategy $\mathsf{s}_{1}$ of Eve in
the game $G_{1}({\mathcal{B}}^{\prime},{\mathcal{B}}_{\Sigma})$. Assume,
towards contradiction, that $Sim({\mathcal{A}},{\mathcal{B}}^{\prime})$ via
some strategy $\mathsf{s}_{sim}$. We construct a strategy $\mathsf{s}$ of Eve
in the letter game on ${\mathcal{A}}$ that is winning against $\tau$, in which
Eve plays $\mathsf{s}_{sim}$ against her imaginary friend Berta in
$Sim({\mathcal{A}},{\mathcal{B}}^{\prime})$, who in turn is playing
$\mathsf{s}_{1}$ against Adam in
$G_{1}({\mathcal{B}}^{\prime},{\mathcal{B}}_{\Sigma})$.

In more detail, Adam begins by playing $\sigma_{0}$ according to $\tau$ in the
letter game on ${\mathcal{A}}$; Berta responds with a transition (or sequence
of transitions in the presence of $\varepsilon$-transitions)
$\rho^{\prime}_{0}=\mathsf{s}_{1}(\sigma_{0})$; and then Eve responds with
$\mathsf{s}(\sigma_{0})=\rho_{0}=\mathsf{s}_{sim}(\rho^{\prime}_{0})$. On the
$i^{th}$ round, when Adam chooses the letter $\sigma_{i}$, after the sequence
$\rho_{0}\dots\rho_{i-1}$ of Eve’s moves in the letter game, and the sequence
$\rho^{\prime\prime}_{0},\dots,\rho^{\prime\prime}_{i-1}$ of transitions in
${\mathcal{B}}_{\Sigma}$, which is the $\Sigma$-projection of the unique run
of ${\mathcal{B}}$ on $\rho_{0}\dots\rho_{i-1}$, viewed as a word over
$\Delta_{A}$, Berta makes the move
$\rho^{\prime}_{i}=\mathsf{s}_{1}(\rho^{\prime\prime}_{0},\dots,\rho^{\prime\prime}_{i-1},\sigma_{i})$
in $G_{1}(B^{\prime},{\mathcal{B}}_{\Sigma})$, and then Eve the move
$\mathsf{s}(\sigma_{0},\rho_{0},\dots,\rho_{i-1},\sigma_{i})=\rho_{i}=\mathsf{s}_{sim}(\rho^{\prime}_{0},\dots,\rho^{\prime}_{i-1})$
in $Sim({\mathcal{A}},{\mathcal{B}}^{\prime})$ and in the letter game.

We argue that $\mathsf{s}$ is winning against $\tau$. Indeed, the run
$\rho^{\prime\prime}_{0}\rho^{\prime\prime}_{1}\dots$ in
${\mathcal{B}}_{\Sigma}$ must be accepting since the sequence of transitions
$\rho_{0}\rho_{1}\dots$ that Eve plays agrees with $\tau$. Then, since Berta
is playing a winning strategy in
$G_{1}({\mathcal{B}}^{\prime},{\mathcal{B}}_{\Sigma})$, the sequence
$\rho^{\prime}_{0}\rho^{\prime}_{1}\dots$ is also an accepting run over the
same word. Since Eve is playing a winning strategy in
$Sim({\mathcal{A}},{\mathcal{B}}^{\prime})$, the sequence
$\rho_{0}\rho_{1}\dots$ is also an accepting run over the same word. This
contradicts $\tau$ being a winning strategy for Adam. We conclude that
${\mathcal{A}}$ does not simulate ${\mathcal{B}}^{\prime}$ and is therefore
not guidable.

Lemma 4.8 can be applied to various automata classes, as summarised in Section
1, including $\omega$-regular automata with an $[i,j]$-parity acceptance
condition (Section 5.1), linear automata (Section 5.4), and visibly pushdown
automata (Section 5.3).

This concludes our criteria. Concerning the necessity of each criterion,
notice that:

  * •

The first criterion (Theorem 1.1.1) is not subsumed by the others, as
demonstrated with the class of all LTSs—it is closed under determinization [7,
Theorem 3.4], but $G_{1}$ does not characterise history-determinism, which is
required for the second criterion, and the letter game need not always be
determined, which is required for the third.

  * •

The second criterion (Theorem 1.1.2) does not imply the first one, as
demonstrated by, for instance, safety pushdown automata [11, Theorem 4.1]. The
implication from the second criterion to third criterion is unclear, however,
and connects to the case of PDA, where the strategies for the players in
letter game are not yet understood [11, Section 6].

  * •

Finally, the third criterion (Theorem 1.1.3) is not subsumed by the other two,
as evident from the case of linear automata (Section 5.4).

##  5 Automata Classes for which History-Determinism = Guidability

###  5.1 Straightforward cases

By Theorem 1.1.1, history-determinism and guidability coincide for all
automata classes closed under determinisation, including: regular automata
(NFAs); VPAs on finite words; $\omega$-regular automata [17]; co-Büchi [18];
and subclasses of $\omega$-regular automata whose deterministic fragment is
$\omega$-regular-complete, such as parity, Rabin, Streett, Muller, and
Emerson-Lei. Some subclasses of $\omega$-regular automata are not closed under
determinisation, e.g., Büchi automata, but as long as they subsume safety
automata, we can build on the fact that Adam’s letter-game strategies are
recognised by deterministic safety automata, and apply Theorem 1.1.3: since
safety automata are determinisable they are closed under $1$-token ghost.

######  Corollary 5.1.

History-determinism and guidability coincide for classes of $\omega$-regular
automata with an $[i,j]$-parity acceptance condition, as well as for the class
of weak automata.

###  5.2 Uniform infinite state systems

In this section, we show that the notions of history-determinism and
guidability coincide on the following classes with safety and reachability
acceptance conditions: pushdown automata, one-counter automata, vector
addition system with states, one-counter nets and Parikh automata. We take a
unified approach by defining all of these classes as cases of “uniform
automata classes”, and showing that the two notions coincide for such classes
(Theorem 5.5).

These uniform automata classes are specified by a content space
${\mathcal{C}}$ (e.g., stack contents) and a set ${\mathcal{K}}$ of partial
functions $f:{\mathcal{C}}\rightharpoonup{\mathcal{C}}$ that contains the
identity function $f_{id}$ that maps each element in ${\mathcal{C}}$ to itself
(e.g., stack updates). The class specified by ${\mathcal{C}}$ and
${\mathcal{K}}$ contains all the automata
${\mathcal{A}}=(\Sigma,Q,\iota,c_{0},\Delta,F_{A},F_{C})$ that have a finite
alphabet $\Sigma$, a finite state space $Q$, and finitely many transitions
$(q,\sigma,f,q^{\prime})\in\Delta$, labelled by a letter
$\sigma\in\Sigma_{\varepsilon}=\Sigma\cup\\{\varepsilon\\}$ and a function
$f\in{\mathcal{K}}$. The automaton ${\mathcal{A}}$ induces an LTS that has
states $(q,c)\in Q\times{\mathcal{C}}$, with transitions
$(q,c)\xrightarrow{\sigma}(q^{\prime},c^{\prime})$, such that
$(q,\sigma,f,q^{\prime})$ is a transition in ${\mathcal{A}}$ and
$f(c)=c^{\prime}$.

The acceptance semantics of an automaton in such a class is specified by a set
of accepting states $F_{A}\subseteq Q$ and a set of accepting contents
$F_{C}\subseteq{\mathcal{C}}$. We will often desire some structure on $F_{C}$,
so we impose the restriction that $F_{C}$ belongs to a set
${\mathcal{S}}\subseteq{\mathcal{P}}(C)$ of subsets of ${\mathcal{C}}$. We
call “$({\mathcal{C}},{\mathcal{K}},{\mathcal{S}})$-automata” the class of all
automata ${\mathcal{A}}=(\Sigma,Q,\iota,c_{0},\Delta,F_{A},F_{C})$ as above
with $F_{C}\in{\mathcal{S}}$. Safety automata require an accepting run to have
all states in $F_{A}$ and all content in $F_{C}$. We distinguish between
synchronous reachability that requires an accepting run to reach an accepting
state and an accepting content at the same time, and asynchronous reachability
that requires an accepting run to just reach an accepting state and an
accepting content, not necessarily at the same time.

######  Definition 5.2.

A class of automata is _uniform_ if it can be specified as
$({\mathcal{C}},{\mathcal{K}},{\mathcal{S}})$-automata with either safety,
synchronous reachability, or asynchronous reachability acceptance semantic.

We show that uniform automata classes are closed under $1$-token ghost by
explicitly constructing for each automaton ${\mathcal{A}}$ in the class a
$1$-token ghost, called ${\mathsf{Delay}}({\mathcal{A}})$, inspired by Prakash
and Thejaswini [20, Lemma 11]. For each run in ${\mathcal{A}}$, we will have a
run in ${\mathsf{Delay}}({\mathcal{A}})$ that lags one transition behind. This
one-step lag is implemented by storing the previous letter in the state space
of ${\mathcal{A}}$, in addition to the state of ${\mathcal{A}}$; transitions
are then taken based on the previous letter, while reading the current letter,
which is now stored.

######  Definition 5.3 (${\mathsf{Delay}}$).

Let ${\mathcal{A}}=(\Sigma,Q,\iota,c_{0},\Delta,F_{Q},F_{C})$ be an automaton
in a uniform class $({\mathcal{C}},{\mathcal{K}},{\mathcal{S}})$. The
automaton
${\mathsf{Delay}}({\mathcal{A}})=(\Sigma,Q^{\prime},\iota^{\prime},c_{0},\Delta^{\prime},F^{\prime}_{Q},F_{C})$
is the ${\mathsf{Delay}}$ of ${\mathcal{A}}$, where

  1. 1.

The set of states $Q^{\prime}$ is $(Q\times\Sigma)\cup\\{\iota^{\prime}\\}$

  2. 2.

The set of transitions $\Delta^{\prime}$ is given by the union of:

     * •

$\\{(\iota^{\prime},\sigma,f_{id},(\iota,\sigma))\mid\sigma\in\Sigma\\}$

     * •

$\\{((q,\sigma),\sigma^{\prime},f,(q^{\prime},\sigma^{\prime}))\mid\sigma,\sigma^{\prime}\in\Sigma,\text{
and }(q,\sigma,f,q^{\prime})\in\Delta\\}$

     * •

$\\{(q,\sigma),\varepsilon,f,(q^{\prime},\sigma)\mid\sigma\in\Sigma,\text{ and
}(q,\varepsilon,f,q^{\prime})\in\Delta\\}$

  3. 3.

The set $F^{\prime}_{Q}$ consists of state of the form $(q,\sigma)$ such that
$q\in F_{Q}$, and $\iota^{\prime}$ if $\iota\in F_{Q}$.

The automaton ${\mathsf{Delay}}({\mathcal{A}})$ has the same acceptance
semantics as ${\mathcal{A}}$ (safety, synchronous reachability or asynchronous
reachability).

######  Lemma 5.4.

Given an automaton ${\mathcal{A}}$ in a uniform automata class $C$, the
automaton ${\mathsf{Delay}}({\mathcal{A}})$ is in $C$ and is a 1-token ghost
of ${\mathcal{A}}$.

We show that $G_{1}$ characterises history-determinism on all uniform automata
classes (Lemma C.2), by reducing to safety and reachability LTSs [7]. With
Lemma 5.4 and Theorem 1.1.2, we get that history-determinism and guidability
coincide on all uniform automata classes.

######  Theorem 5.5.

History-determinism and guidability coincide for uniform automata classes.

It now suffices to represent various automata classes as uniform ones to show
that guidability and history-determinism coincide on them. For pushdown and
one-counter automata, vector addition systems and one-counter nets, as well as
for Parikh automata, the contents are the counter or stack contents, while the
update functions are their increments, decrements, pops and pushes. The update
partial functions also implement which parts of the contents can be used to
enable transitions: for example, for pushdown automata, the partial functions
are either defined for all contents where the stack is empty, or undefined for
all such contents; for Parikh automata, the contents do not influence which
transitions are enabled, so the functions are fully defined. (Formal
definitions are given in Definitions C.4, C.5 and C.6.)

######  Corollary 5.6.

History-determinism and guidability coincide for the classes of pushdown
automata, one-counter automata, vector addition systems with states, one-
counter nets with safety and reachability acceptance conditions, and for
Parikh automata with safety, synchronous reachability and asynchronous
reachability acceptance conditions.

#### Non-uniform classes

The class of visibly pushdown automata is not uniform, as there are additional
constraints on transitions, namely the kind of function that changes content
depends on the letter seen. Timed automata also do not constitute a uniform
class, since the alphabet is infinite as it consists of all timed letters, and
the clock valuations are updated according to both the transition (resets) and
the delay of the input letter. In Section 5.4, we consider linear automata:
these are Büchi automata that have no cycles apart from self-loops. Linear
automata also does not form a uniform class, since they restrict the state-
space. In what follows, we give alternative constructions of $1$-token-ghosts
for these classes. The case of linear automata is trickier, as we show that it
is not closed under $1$-token ghost. We therefore use, in Section 5.4, a more
involved argument that allows us to use Theorem 1.1.3.

###  5.3 Visibly pushdown and timed automata

Visibly pushdown automata over infinite words ($\omega$-VPAs) are neither
(history-) determinisable, nor does $G_{1}$ characterise history-determinism
on them. Nevertheless, we can use Theorem 1.1.3 to show that history-
determinism and guidability coincide for this class.

######  Theorem 5.7.

History-determinism and guidability coincide for the class of visibly pushdown
automata with any $\omega$-regular acceptance condition.

######  Proof 5.8 (Proof sketch).

First we show that the class is closed under $1$-token ghost. Like in the
previous cases, we build an automaton that executes the same transitions, but
one step later. The technical challenge is executing transitions with a delay,
as an $\omega$-VPA must respect the stack discipline of the input alphabet. We
overcome this by maintaining a “semantic stack” that consists of the actual
stack and one additional letter that is embedded in the state space and
stores, when necessary, the letter that should have been in the top of the
stack.

Then, we describe the letter-game for an $\omega$-VPA as a game on a visibly
pushdown arena with a “stair parity” acceptance condition, to show that Adam’s
winning strategies can be implemented by $\omega$-VPA transducers. We then
turn this transducer into a deterministic $\omega$-VPA recognising the plays
that agree with Adam’s strategy, and apply Theorem 1.1.3.

We turn to safety and reachability timed automata, for which we apply Theorem
1.1.2, yet with a specially tailored ${\mathsf{Delay}}$ construction.

######  Theorem 5.9.

For the class of timed automata with safety or reachability acceptance
conditions, the notions of history-determinism and guidability coincide.

######  Proof 5.10 (Proof sketch).

The goal is to simulate such an automaton ${\mathcal{A}}$ with a delay, as in
Definition 5.3. Yet, the difficulty is that delaying a clock-reset by a step
will affect the value of the clock for future comparisons, and there is no
delaying of the passage of time. Hence a naive construction would end up
recognising the timed language of words in which timestamps are shifted by
one. We overcome the difficulty by duplicating in the $1$-token ghost
construction each clock of ${\mathcal{A}}$, using one copy for comparisons in
guards and the other to simulate retroactive resets. In addition, the state-
space stores the effect of the previous delay, by remembering the
corresponding region, that is, how the timestamp compares to existing clocks
and constants. With this construction, and the $G_{1}$-characterisation of
history-determinism for safety and reachability automata, we complete the
proof.

###  5.4 Linear automata

A _linear_ (also called _very weak_) automaton is a Büchi automaton in which
all cycles are self loops. (In linear automata, the acceptance condition does
not really matter, since over an automaton with only self loops, all the
standard $\omega$-regular acceptance conditions coincide.)

First, observe that linear automata are not closed under
(history-)determinisation. (The standard Büchi automaton over the alphabet
$\Sigma=\\{a,b\\}$ recognizing the language of finitely many $a$’s is linear.)
We show that they are also not closed under $1$-token ghost, by proving that
the linear automaton depicted in Figure 1 admits no $1$-token ghost in the
class.

######  Theorem 5.11.

The class of linear automata is not closed under $1$-token ghost.

######  Proof 5.12.

Let ${\mathcal{A}}$ be the linear automaton depicted in Figure 1, and assume
toward contradiction that there is a linear automaton
${\mathcal{A}}^{\prime}$, satisfying
$\textsf{1-TokenGhost}({\mathcal{A}}^{\prime},{\mathcal{A}})$, witnesses by a
winning strategy $\mathsf{s}$ of Eve in
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$.

In a play $\pi_{1}$ of $G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$ in which
Eve plays along $\mathsf{s}$ and Adam plays $(ab)^{*}$ while staying in
$q_{0}$, at some points of time $2k{-}1$ and $2k$, Eve must remain in the same
state $q^{\prime}$ of ${\mathcal{A}}^{\prime}$ after Adam chose the letters
$a$ and $b$, respectively, since ${\mathcal{A}}^{\prime}$ is linear.

In a play $\pi_{2}$ of $G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$ in which
Eve plays along $\mathsf{s}$ and Adam starts with $(ab)^{k{-}1}a$ while
staying in $q_{0}$, Eve reaches, as per the previous claim, the state
$q^{\prime}$ of ${\mathcal{A}}^{\prime}$. Then, if Adam continues with the
word $ca^{\omega}$, while moving from $q_{0}$ to $q_{1}$ (over the previous
$a$) and then to $q_{3}$ (over $c$), Eve has some accepting continuation run
$\rho$ from the state $q^{\prime}$ over the suffix $ca^{\omega}$, since
$\mathsf{s}$ is winning for Eve in
$G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$ and Adam’s run is accepting.

Thus, there is an accepting run of ${\mathcal{A}}^{\prime}$ on the word
$w=(ab)^{k}ca^{\omega}$, following in the first $2k$ steps the run of Eve in
the play $\pi_{1}$, reaching the state $q^{\prime}$, and then in the next
steps following her accepting continuation in $\pi_{2}$. Yet, ${\mathcal{A}}$
does not have an accepting run on $w$, contradicting the equivalence of
${\mathcal{A}}$ and ${\mathcal{A}}^{\prime}$, and thus the assumption that
$\textsf{1-TokenGhost}({\mathcal{A}}^{\prime},{\mathcal{A}})$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$a,b$$a$$b$$c$$d$$a,b$ Figure 1: A linear
automaton which admits no linear automaton that is a $1$-token ghost of it.

Yet, history-determinism and guidability do coincide for the class of linear
automata. The underlying reason is that when a linear automaton
${\mathcal{A}}$ is not history-deterministic, Adam’s winning strategy in the
letter game can be adapted to a linear automaton that does have a $1$-token
ghost within the class of linear automata, thus satisfying Theorem 1.1.3.

######  Theorem 5.13.

History-determinism and guidability coincide for the class of linear automata.

######  Proof 5.14 (Proof sketch).

History-determinism implies guidability with respect to all classes. For the
other direction, consider a linear automaton
${\mathcal{A}}=(\Sigma,Q,\iota,\Delta,\alpha)$ that is not $\mathrm{HD}$, and
let ${\mathcal{M}}=(\Delta,\Sigma,M,m_{0},\Delta_{M}:M\times\Delta\to
M,\gamma:M\to\Sigma)$ be a deterministic finite-state transducer representing
a finite-memory winning strategy $\mathsf{s}_{M}$ of Adam in the letter game.

We then build, by taking a product of ${\mathcal{M}}$ and ${\mathcal{A}}$, a
deterministic safety automaton ${\mathcal{P}}$, that recognises the set of
plays that can occur in the letter game on ${\mathcal{A}}$ if Adam plays
according to $\mathsf{s}_{M}$. From ${\mathcal{P}}$, we take its projection
${\mathcal{N}}$ onto the alphabet $\Sigma$ of ${\mathcal{A}}$. ${\mathcal{N}}$
need not be linear, but we adapt it into a linear ${\mathcal{N}}^{\prime}$
that will still correspond to a winning strategy of Adam in the letter game.
${\mathcal{N}}^{\prime}$ will thus constitute a projection of a deterministic
automaton ${\mathcal{P}}^{\prime}$ onto the alphabet $\Sigma$, where
${\mathcal{P}}^{\prime}$ is over the alphabet of transitions of
${\mathcal{A}}$ and recognises the plays of a winning strategy of Adam in the
letter game. Once achieving that, we can apply the ${\mathsf{Delay}}$
construction on ${\mathcal{N}}^{\prime}$—it will not introduce, in this case,
non-self cycles, since the states of ${\mathcal{N}}^{\prime}$ (as the
projection of the states of ${\mathcal{P}}^{\prime}$), have outgoing
transitions only on a single letter. Hence, we satisfy Theorem 1.1.3, proving
the stated claim.

The transformation of ${\mathcal{N}}$ into ${\mathcal{N}}^{\prime}$ is quite
technical, and is left to Section C.4.

##  6 Automata Classes for which History-Determinism $\neq$ Guidability

In this section we study classes which admit guidable automata that are not
history-deterministic. They offer insight into how, in practice, the criteria
can fail to hold, and witness that even on arguably natural automata classes,
guidability and history determinism do not necessarily coincide. The main
reason for the equivalence between the notions to fail for these classes is a
bound on the allowed resources – the number of states in the first class and
the number of clocks in the second.

Our first example of when history-determinism and guidability differ are Büchi
automata with a bounded number of states, witnessed by the automaton in Figure
2.

######  Theorem 6.1.

For every $n\in\mathbb{N}^{+}$, history-determinism and guidability are
distinct notions for the class of Büchi automata with up to $2n$ states.

$q_{1}$$q_{2}$$q_{3}$$q_{4}$$...$$\\!\\!\\!q_{2n{-}1}\\!\\!\\!$$q_{2n}$$a,b$$a,b$$b$$a,b$$a,b$$a,b$$b$$a,b$$a,b$$b$
Figure 2: A Büchi automaton that accepts words with a finite number of $a$’s.
To simulate any equivalent small enough Büchi automaton ${\mathcal{B}}$, Eve
moves to the next accepting state once the other automaton is in a maximally
strongly connected component with an accepting state. The size constraint on
${\mathcal{B}}$, and the observation that a such a component can not both have
a transition on $a$ and an accepting state guarantees that this strategy wins
in the simulation game. However, ${\mathcal{B}}$ is not history-deterministic.

This counter-example is simple, but quite artificial. We proceed with a class
which is, arguably, more natural: timed automata with a bounded number of
clocks.

######  Theorem 6.2.

History-determinism and guidability are distinct notions for the class
$\mathbb{T}_{k}$ of timed-automata over finite words with at most $k$ clocks,
for each $k\in\mathbb{N}$.

######  Proof 6.3 (Proof sketch).

We consider the language of infinite words in which there are $k$ event pairs
that occur exactly one time-unit apart both before and after the first
occurence of a $\$$ letter. Then, the guidable automaton for this language can
freely reset its clocks until the $\$$-separator, which allows it to ensure it
tracks all delays tracked by a smaller automaton with up to $k$ clocks.
Crucially, any automaton that only accepts words in this language must keep
track of $k$ clock values when the separator occurs, as otherwise, it will
also accept some word in which the second of matching pair of event is shifted
a little.

##  7 Conclusions

We have presented sufficient conditions for a class of automata to guarantee
the coincidence of history-determinism and guidability, and used them to show
that this is the case for many standard automata classes on infinite words. As
a result, we get algorithms to decide guidability for many of these classes.
Guidable automata allow for simple model-checking procedures, and once
guidability check is simple, one can take advantage of it whenever applicable.
For example, consider a specification modelled by a Büchi or coBüchi automaton
${\mathcal{A}}$. Model-checking whether a system ${\mathcal{S}}$ satisfies
${\mathcal{A}}$ is ${\sc PSpace}$-hard. Using our results, one can check first
in ${\sc PTime}$ whether ${\mathcal{A}}$ is guidable, and in the fortunate
cases that it is, conclude the model checking in ${\sc PTime}$, by checking
whether ${\mathcal{A}}$ simulates ${\mathcal{S}}$. We have also demonstrated
automata classes for which guidability and history-determinism do not
coincide.

We believe that our positive results extend to additional automata classes,
such as register automata [15], which behave quite similarly to timed
automata. Furthermore, we believe them to extend to additional families of
automata classes:

  * •

Finite words. We have focused on automata over infinite words, which in this
context, are better behaved. Ends of words bring additional complications to
our constructions, but overall we believe our approach to be amenable to the
analysis of finite word automata.

  * •

Quantitative automata. In quantitative automata, transitions carry additional
information in the form of weights. As a result, there is an additional
difference between the letter game and simulation game, which makes extending
our analysis to the quantitative setting particularly relevant. We believe
that many of our techniques adapt to that setting.

One could argue that for model-checking, the more interesting property is
whether a (not necessarily safety) automaton is guidable by just safety
automata, since we typically represent specifications by safety automata.
Interestingly, this property often coincides with guidability w.r.t. the full
class of automata, as demonstrated in by our third criterion (Theorem 1.1.3):
if Adam’s strategies in the letter game can be translated into automata, these
automata are safety ones, and therefore guidability w.r.t. safety automata is
just as hard as guidability w.r.t. the full class of automata with the more
complex acceptance conditions.

## References

  * [1] Rajeev Alur and P. Madhusudan.  Visibly pushdown languages.  In László Babai, editor, Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004, pages 202–211. ACM, 2004.  doi:10.1145/1007352.1007390.
  * [2] Marc Bagnol and Denis Kuperberg.  Büchi good-for-games automata are efficiently recognizable.  In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), page 16, 2018.
  * [3] Udi Boker.  Why these automata types?  In Proceedings of LPAR, pages 143–163, 2018.
  * [4] Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak.  On succinctness and recognisability of alternating good-for-games automata.  arXiv preprint arXiv:2002.07278, 2020.
  * [5] Udi Boker and Karoliina Lehtinen.  Token games and history-deterministic quantitative automata.  In FoSSaCS, pages 120–139, 2022.  A submitted journal version is available at https://arxiv.org/abs/2110.14308.
  * [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] Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke.  History-deterministic timed automata, 2023.  arXiv:2304.03183.
  * [8] Thomas Colcombet.  Fonctions régulières de coût.  Habilitation à diriger les recherches, École Doctorale de Sciences Mathématiques de Paris Centre, 2013.
  * [9] Thomas Colcombet and Christof Löding.  The non-deterministic mostowski hierarchy and distance-parity automata.  In Proc. of ICALP, volume 5126, pages 398–409, 2008.  doi:10.1007/978-3-540-70583-3\\_33.
  * [10] Wladimir Fridman.  Formats of winning strategies for six types of pushdown games.  In Angelo Montanari, Margherita Napoli, and Mimmo Parente, editors, GANDALF 2010, volume 25 of EPTCS, pages 132–145, 2010.  doi:10.4204/EPTCS.25.14.
  * [11] Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann.  A bit of nondeterminism makes pushdown automata expressive and succinct.  Log. Methods Comput. Sci., 20(1), 2024.  doi:10.46298/LMCS-20(1:3)2024.
  * [12] Thomas Henzinger and Nir Piterman.  Solving games without determinization.  In Proceedings of CSL, pages 395–410, 2006.
  * [13] Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani.  Fair simulation.  Inf. Comput., 173(1):64–81, 2002.  doi:10.1006/inco.2001.3085.
  * [14] Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke.  History-deterministic timed automata.  In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 14:1–14:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
  * [15] Michael Kaminski and Nissim Francez.  Finite-memory automata.  Theoretical Computer Science, 134(2):329–363, 1994.  URL: https://www.sciencedirect.com/science/article/pii/0304397594902429, doi:10.1016/0304-3975(94)90242-9.
  * [16] Christof Löding, P. Madhusudan, and Olivier Serre.  Visibly pushdown games.  In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 408–420. Springer, 2004.  doi:10.1007/978-3-540-30538-5\\_34.
  * [17] Robert McNaughton.  Testing and generating infinite sequences by a finite automaton.  Information and Control, 9:521–530, 1966.
  * [18] Satoru Miyano and Takeshi Hayashi.  Alternating finite automata on $\omega$-words.  Theoretical Computer Science, 32:321–330, 1984.
  * [19] Damian Niwiński and Michał Skrzypczak.  On Guidable Index of Tree Automata.  In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), volume 202 of Leibniz International Proceedings in Informatics (LIPIcs), pages 81:1–81:14, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  URL: https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.81, doi:10.4230/LIPIcs.MFCS.2021.81.
  * [20] Aditya Prakash and K. S. Thejaswini.  On history-deterministic one-counter nets.  In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 218–239. Springer, 2023.  doi:10.1007/978-3-031-30829-1\\_11.

##  Appendix A Detailed Definitions

#### Automata

Here we give more detailed definitions of the automata we work with. Each type
of automaton induces an LTS of which the states are the configurations of the
automaton and the transitions enabled at each configuration updates it as
expected; runs and acceptance are defined uniformly from the induced LTS.

A pushdown automaton (PDA) $(\Sigma,Q,\iota,\Delta,\Gamma,\alpha)$ consists of
a finite set of states $Q$, a finite input alphabet $\Sigma$, an initial state
$\iota$, a transition relation $\Delta$ detailed hereafter, a finite stack
alphabet $\Gamma$, and an acceptance condition $\alpha$. A configuration
consists of a state from $Q$ and a string of stack variables in
$\Gamma^{*}\bot$ ending in $\bot$, a distinguished bottom-of-stack symbol. The
mode of a configuration $(q,XS)$, for $q\in Q$, $X\in\Gamma$ and
${\mathcal{S}}\in\Gamma^{*}\bot$, is $(q,X)$, and of $(q,\bot)$ is $(q,\bot)$,
namely the state and topmost stack symbol. The transitions of a PDA are
enabled at a mode and take the form
$(q,X)\xrightarrow{\sigma\mid\textsf{op}}q^{\prime}$ where
$X\in\Gamma\cup\\{\bot\\}$, $\sigma\in\Sigma\cup\\{\varepsilon\\}$,
$\textsf{op}\in\\{\textsf{push}\ Y,\textsf{pop},\textsf{noop}\\}$ for
$Y\in\Gamma$, and $q^{\prime}\in Q$. Transitions update the configuration as
follows. A $\textsf{push}\ Y$ transition adds $Y$ to the top of the
configuration stack, a pop transition removes the top of the stack and can not
be enabled at a mode $(q,\bot)$ indicating an empty stack, and a noop-
transition leaves the stack as is. A transition changes the configuration
state as expected.

A visibly pushdown automaton (VPA) is a pushdown automaton without
$\varepsilon$-transitions of which the input alphabet $\Sigma$ is partitioned
between $\textsf{push},\textsf{pop}$ and noop letters, which only occur in
push, pop and noop transitions, respectively.

A timed automaton ${\mathcal{T}}=(\Sigma,Q,\iota,C,\delta,\alpha)$ has a
finite alphabet $\Sigma$, a set of states $Q$ with an initial state $q_{0}$, a
set of clocks $C$, a transition function $\delta$ and acceptance condition
$\alpha$ as usual. Timed automata, as the name suggests, process _timed
words_. These are sequences of pairs $\\{\sigma_{i},d_{i}\\}_{i\geq 0}$ of
letters $\sigma_{i}\in\Sigma$ and non-negative time delays in $\mathbb{R}$. A
timed word may also get written as $\\{\sigma_{i},t_{i}\\}_{i\geq 0}$ where
$t_{i}$ is the timestamp of $\sigma_{i}$, that is, the sum of the delays up to
$i$. We then say that the event $\sigma_{i}$ occurs at time $t_{i}$, or after
the delay $d_{i}$. A _timed automaton_ is a finite automaton equipped with a
set of _clocks_ $C$ that measure the passage of time. Each transition
$(q,g,\sigma,X,q^{\prime})$ of a timed automaton checks the valuation of these
clocks using a _guard_ $g$, and resets the values of a subset of clocks $X$ to
0. These guards are Boolean combinations ${\mathcal{B}}(C)$ of clock
constrains of the form $c\lhd n$, where $c$ is the value of a clock, $n$ is a
natural number and $\lhd\in\\{\leq,<,=,\geq,>\\}$.

A configuration of a timed automaton is a pair in $Q\times\mathbb{R}^{C}$
consisting of a state and a clock valuation. A transition
$(q,g,\sigma,X,q^{\prime})$ can be taken over a timed letter $(\sigma,d)$ at
configuration $(q,\nu)$ if the valuation $\nu+d$, in which all clocks are
increased by $d$ from $\nu$, satisfies the guard $g$. The next configuration
is then $(q^{\prime},\nu+d[X])$, where the clocks in $X$ are reset to $0$. We
may use $\langle q,\nu\rangle\xrightarrow{\sigma,d}\langle
q,\nu+d\rangle\xrightarrow{g,X}\langle q^{\prime},\nu^{\prime}\rangle$ to
denote the transition we just described, splitting it into a ‘delay step’ and
a ‘reset step’. The induced LTS of ${\mathcal{A}}$ has as its states
configurations of ${\mathcal{A}}$ and as transitions those enabled at each
configuration, labelled with letter-delay pairs.

We consider timed automata with safety or reachability acceptance conditions,
which we denote by ${\mathcal{T}}=(\Sigma,Q,\iota,\delta,F)$ where $F$ is the
safe or target region respectively.

##  Appendix B Proofs of Section 4

See 4.1

######  Proof B.1.

$\mathrm{HD}$ always implies guidability: given ${\mathcal{A}}$ in $C$ that is
$\mathrm{HD}$, it is easy to see that Eve wins
$Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$ for all
${\mathcal{A}}^{\prime}\leq{\mathcal{A}}$, as the strategy that chooses
transitions in ${\mathcal{A}}$ according to the letter game on
${\mathcal{A}}$, ignoring Adam’s token in ${\mathcal{A}}^{\prime}$, is a
winning strategy.

For the other direction, consider ${\mathcal{A}}\in C$ that is guidable within
$C$, and let ${\mathcal{A}}^{\prime}\in C$ be an $\mathrm{HD}$ LTS equivalent
to ${\mathcal{A}}$. As ${\mathcal{A}}$ is guidable, it simulates, in
particular, ${\mathcal{A}}^{\prime}$. Eve can use her winning strategy
$\mathsf{s}$ in this simulation game, together with her winning strategy
$\mathsf{s}^{\prime}$ in the letter game on ${\mathcal{A}}^{\prime}$ to also
win the letter game on ${\mathcal{A}}$: when Adam provides a letter in the
letter game on ${\mathcal{A}}$, Eve uses the transition (or transition
sequence, in the presence of $\varepsilon$-transitions) $\rho$ chosen by
$\mathsf{s}^{\prime}$ in the letter game on ${\mathcal{A}}^{\prime}$ on the
same letter. She assumes Adam chooses the transition sequence $\rho$ on
${\mathcal{A}}^{\prime}$ in $Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$ as
well, and responds to Adam in the letter game on ${\mathcal{A}}$ with the move
suggested by $\mathsf{s}$ in $Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$. If
the word generated by Adam is accepting, then the run generated by
$\sigma^{\prime}$ in ${\mathcal{A}}^{\prime}$ is accepting, and therefore the
run generated in ${\mathcal{A}}$ in
$Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$ by $\sigma$ is also accepting.

##  Appendix C Proofs of Section 5

###  C.1 Uniform infinite state systems

See 5.4

######  Proof C.1.

Consider ${\mathcal{A}}=(\Sigma,Q,\iota,\Delta,F_{Q},F_{C})$ and
${\mathsf{Delay}}({\mathcal{A}})$ =
$(\Sigma,Q^{\prime},\iota,c_{0},\Delta^{\prime},F^{\prime}_{Q},F_{C})$ as per
Definition 5.3. We need to show that (i) Eve wins
$G_{1}({\mathsf{Delay}}({\mathcal{A}}),{\mathcal{A}})$, and (ii)
$L({\mathcal{A}})=L({\mathsf{Delay}}({\mathcal{A}}))$.

(i) We give a winning strategy for Eve in
$G_{1}({\mathsf{Delay}}({\mathcal{A}}),{\mathcal{A}})$. In the first round,
after Adam chooses a letter $\sigma_{0}$, Eve chooses the unique transition
$(\iota^{\prime},\sigma_{0},f_{id},(\iota,\sigma_{0}))$, and then Adam a
transition sequence
$\rho_{0}=(\iota,c_{0})\xRightarrow{\sigma_{0},\rho_{0}}(q_{1},c_{1})$. Eve
will then preserve in next rounds the following invariant: _Suppose Adam took
the transition sequence
$\rho_{i}=(q_{i-1},c_{i-1})\xRightarrow{\sigma_{i},\rho_{i}}(q_{i},c_{i})$ in
round $i$, then Eve’s configuration after $i$ rounds is given by
$((q_{i-1},\sigma^{\prime}_{i-1}),c_{i-1})$_.

The invariant clearly holds after the first round. Suppose that after $i>0$
rounds of play, the invariant holds. Eve preserves the invariant after $i+1$
rounds as follows:

In the $(i+1)^{th}$ round, suppose Adam selects the letter
$\sigma_{i}\in\Sigma$, after choosing the transition sequence
$\rho_{i}=(p^{0},c^{0})\xrightarrow{\varepsilon,f^{0}}(p^{1},c^{1})\xrightarrow{\varepsilon,f^{1}}\cdots(p^{k},c^{k})\xrightarrow{\sigma_{i-1},f^{k}}(p^{k+1},c^{k+1}\xrightarrow{\varepsilon,f^{k+1}}\cdots(p^{l},c^{l}))$
in the $i^{th}$ round, where $(p^{0},c^{0})=(q_{i-1},c_{i-1})$ and
$(p^{l},c^{l})=(q_{i},c_{i})$.

By construction of ${\mathsf{Delay}}({\mathcal{A}})$, it has a transition
sequence
$\rho^{\prime}_{i}=((p^{0},\sigma_{i-1}),c^{0})\xrightarrow{\varepsilon,f^{0}}\cdots((p^{k},\sigma_{i-1}),c^{k})\xrightarrow{\sigma_{i},f^{k}}((p^{k+1},\sigma_{i}),c^{k+1}$
$\xrightarrow{\varepsilon,f^{k+1}}\cdots((p^{l},\sigma_{i}),c^{l}))$ on
$\sigma_{i}$. We let Eve pick $\rho^{\prime}_{i}$ in $(i+1)^{th}$ round,
essentially copying Adam’s transition sequence in the $i^{th}$ round. Adam
selects a transition sequence
$(q_{i},c_{i})\xRightarrow{\sigma_{i},\rho_{i+1}}(q_{i+1},c_{i+1})$, and it is
clear that the invariant is preserved throughout. This implies that the run
Eve constructs in ${\mathsf{Delay}}({\mathcal{A}})$ is accepting whenever
Adam’s is accepting. Hence, Eve wins
$G_{1}({\mathsf{Delay}}({\mathcal{A}}),{\mathcal{A}})$.

(ii) $L({\mathcal{A}})\subseteq L({\mathsf{Delay}}({\mathcal{A}}))$ is clear,
as Eve wins $G_{1}({\mathsf{Delay}}({\mathcal{A}}),{\mathcal{A}})$. For the
other direction of the inclusion, let $w$ be a word accepted by
${\mathsf{Delay}}({\mathcal{A}})$ via a run
$\rho^{\prime}=(\iota^{\prime},c_{0})\xrightarrow{\sigma_{0},f_{id}}((\iota,\sigma_{0}),c_{0})\xRightarrow{\sigma_{1},\rho^{\prime}_{0}}((q_{1},\sigma_{1}),c_{1})\xRightarrow{\sigma_{2},\rho^{\prime}_{1}}((q_{2},\sigma_{2}),c_{2})\cdots$,
such that $w=\sigma_{0}\sigma_{1}\sigma_{2}\cdots$. Then it is easy to see
that there is a run
$\rho=(\iota,c_{0})\xRightarrow{\sigma_{0},\rho_{0}}(q_{1},c_{1})$
$\xRightarrow{\sigma_{1},\rho_{1}}(q_{2},c_{2})\cdots$ of ${\mathcal{A}}$ on
$w$ that is accepting whenever $\rho^{\prime}$ is.

######  Lemma C.2.

Let ${\mathcal{A}}$ be an automaton in a uniform automata class. Eve wins
$G_{1}$ on ${\mathcal{A}}$ if and only if ${\mathcal{A}}$ is history-
deterministic.

######  Proof C.3.

Let ${\mathcal{A}}=(\Sigma,Q,\iota,c_{0},\delta,F_{Q},F_{C})$. When
${\mathcal{A}}$ has safety or synchronous reachability acceptance semantic,
Eve wins $G_{1}$ on ${\mathcal{A}}$ if and only if ${\mathcal{A}}$ is
$\mathrm{HD}$, since the one-token game characterises history-determinism on
all safety and reachability LTSs [5, 7].

For the case of ${\mathcal{A}}$ with acceptance by asynchronous reachability,
consider the reachability LTS ${\mathcal{B}}$, in which the states are given
by $(q,c,p_{1},p_{2})$, where $q$ is a state in ${\mathcal{A}}$ and
$c\in{\mathcal{C}}$, and $p_{1}$ and $p_{2}$ are flags that are either 0 or 1,
based on whether an accepting state in $F_{A}$ or $F_{C}$ is seen in the run
so far. The initial state is given by $(\iota,c_{0},0,0)$. The transitions of
${\mathcal{B}}$ are of the form
$(q,c,p_{1},p_{2})\xrightarrow{\sigma}(q^{\prime},c^{\prime},p^{\prime}_{1},p^{\prime}_{2})$,
such that $(q,\sigma,f,q^{\prime})$ is a transition in ${\mathcal{A}}$, where
$f(c)=c^{\prime}$, $p^{\prime}_{1}=1$ if $q^{\prime}\in F_{C}$ and
$p^{\prime}_{1}=p_{1}$ otherwise, and similarly, $p^{\prime}_{2}=1$ if
$c^{\prime}\in F_{C}$ and $p^{\prime}_{2}=p_{2}$ otherwise. The accepting
states of the LTS ${\mathcal{B}}$ are those in which both the flags are $1$,
i.e., states of the form $(q,c,1,1)$ where $q\in Q$ and $c\in{\mathcal{C}}$.

It is easy to see that a winning strategy for Eve in $G_{1}({\mathcal{A}})$ or
the letter game on ${\mathcal{A}}$ can be used to get a winning strategy for
Eve in $G_{1}({\mathcal{B}})$ or the letter game on ${\mathcal{B}}$,
respectively, and vice versa. As Eve wins $G_{1}$ on any reachability LTS if
and only if the LTS is $\mathrm{HD}$ [5, 7], we get that Eve wins $G_{1}$ on
${\mathcal{A}}$ if and only if ${\mathcal{A}}$ is $\mathrm{HD}$.

We represent various classes of automata as uniform automata classes. The
class of safety and reachability nondeterministic $\omega$-regular automata is
a uniform automata class, as it can be given by a
$({\mathcal{C}},{\mathcal{K}},{\mathcal{S}})$-automata class where
${\mathcal{C}}=\\{X\\}$ is a singleton set, ${\mathcal{K}}$ only consists of
the identity function, and ${\mathcal{S}}=\\{{\mathcal{C}}\\}$. Synchronous
and asynchronous reachability coincides in this setting. We show that the
classes of VASS, one-counter nets, and pushdown-, Parikh-, and one-counter-
automata are also uniform automata classes.

######  Definition C.4.

_Pushdown automata_ is a uniform automata class given by
$({\mathcal{C}},{\mathcal{K}},{\mathcal{S}})$, where
${\mathcal{C}}=\bot\Gamma^{*}$ is the set of possible _stack contents_ for
some set $\Gamma$ of _stack symbols_ , where $\bot\notin\Gamma$. Let
$\Gamma_{\bot}$ be $\Gamma\cup\\{\bot\\}$. The set ${\mathcal{K}}$ consists of
the following partial functions from ${\mathcal{C}}$ to ${\mathcal{C}}$:

  1. 1.

_Push transitions:_ Map $\gamma X$ to $\gamma XY$, where $\gamma
X\in\bot\Gamma^{*}$, $X\in\Gamma_{\bot}$ and $Y\in\Gamma$.

  2. 2.

_Pop transitions:_ Map $\gamma X$ to $\gamma$, where $\gamma\in\bot\Gamma^{*}$
and $X\in\Gamma$.

  3. 3.

_Noop transitions:_ Map $\gamma$ to $\gamma$ for each
$\gamma\in\bot\Gamma^{*}$.

The set ${\mathcal{S}}$ either equals $\\{{\mathcal{C}}\\}$, in which case the
acceptance is only state-based or equals $\\{\\{\bot\\}\\}$, the set
consisting of only the ‘empty stack’. Both these formalisms are known to be
equivalent for synchronous reachability PDA, while for safety PDA we consider
only the former, as the latter coincides with finite state automata.

_One-counter automata_ are restrictions of pushdown automata where
$\Gamma=\\{X\\}$ is a singleton set in Definition C.4 above. It is clear that
imposing this restriction yields another uniform automata class.

######  Definition C.5.

_Vector addition systems with states_ (VASS) is a uniform automata class given
by $({\mathcal{C}},{\mathcal{K}},{\mathcal{S}})$, where
${\mathcal{C}}=\mathbb{N}^{*}$ is the set of _vectors_. The set
${\mathcal{K}}$ consists of partial functions specified by
$\alpha\in\mathbb{Z}^{d}$ for some $d>0$ that maps a vector
$v\in\mathbb{N}^{d}$ to $v+\alpha$, provided $v+\alpha$ is in
$\mathbb{N}^{d}$. The set ${\mathcal{S}}$ equals $\\{{\mathcal{C}}\\}$, and
thus acceptance is only based on the accepting states of an automaton in this
class. The accepting condition is given by (synchronous) reachability or
safety semantics. Note that as synchronous reachability and asynchronous
reachability coincide here due to ${\mathcal{S}}$ consisting of only
${\mathcal{C}}$, we just use reachability VASS to denote synchronous
reachability VASS.

_$d$ -dimensional_ VASS are restrictions of VASS where
${\mathcal{C}}=\mathbb{N}^{d}$ for some $d>0$. It is easy to see that
$d$-dimensional VASSes are also a uniform automata class. The class of
$1$-dimensional VASS is called _one-counter nets_ (OCNs).

######  Definition C.6.

_Parikh automata_ is a uniform automata class given by
$({\mathcal{C}},{\mathcal{K}},{\mathcal{S}})$ where
${\mathcal{C}}=\mathbb{N}^{*}$ is the set of _vectors_. The set
${\mathcal{K}}$ consists of partial functions specified by
$\alpha\in\mathbb{N}^{d}$ for some $d>0$, that maps a vector
$v\in\mathbb{N}^{d}$ to $v+\alpha$. The set ${\mathcal{S}}$ is the union of
all semilinear ${\mathcal{S}}_{d}$, where ${\mathcal{S}}_{d}$ consists of all
the semilinear sets in $\mathbb{N}^{d}$. We consider acceptance conditions
based on safety, synchronous reachability and asynchronous reachability
semantics.

###  C.2 Visibly pushdown automata

######  Lemma C.7.

The class of $\omega$-VPAs is closed under $1$-token ghost.

######  Proof C.8.

Given an $\omega$-VPA ${\mathcal{A}}=(Q,\Sigma,\iota,\Delta,\Gamma,\alpha)$,
we build an $\omega$-VPA ${\mathcal{A}}^{\prime}$ that is a $1$-token ghost of
${\mathcal{A}}$, by morally delaying the transitions by one step, as in the
previous ${\mathsf{Delay}}$ constructions. However, there is a difficulty in
doing that, as ${\mathcal{A}}^{\prime}$ must operate on the stack at the same
rhythm as ${\mathcal{A}}$, rather than one step behind. In particular, when
${\mathcal{A}}^{\prime}$ reads a push-letter, it has to push something onto
the stack before it “knows” what to push, and when reading a pop\- or noop-
letter after a block of push-letters, it “wants” to push something to the
stack, as ${\mathcal{A}}$ did on the previous step, but it cannot.

To manage these local asynchronicities, we maintain a “semantic stack” in
${\mathcal{A}}^{\prime}$ that consists of the actual stack and one additional
letter that is embedded in the state space and stores, when necessary, the
letter that should have been in the top of the stack. At the bottom of the
semantic stack there are two symbols, $\bot\bot^{\prime}$, rather than just
$\bot$, so that when the semantic stack has a single element, stored in the
state-space, ${\mathcal{A}}^{\prime}$ is still able to read a pop-letter.

Consider a run $r$ of ${\mathcal{A}}$ on a word $w$, and let the stack of
${\mathcal{A}}$ after reading the $i$th letter of $w$ be $\bot
x_{1}x_{2}\cdots x_{k}$. Then the semantic stack of ${\mathcal{A}}^{\prime}$
after reading the $i+1$ letter of $w$ is $\bot\bot^{\prime}x_{1}x_{2}\cdots
x_{k}$. If the $i+1$ letter is a push-letter, then the actual stack is the
same as the semantic one, and the dedicated state-space letter that ends the
semantic stack is $\varepsilon$. If the $i+1$ letter is a pop\- or noop-
letter, then the actual stack is $\bot\bot^{\prime}x_{1}x_{2}\cdots x_{k-1}$,
and the dedicated state-space letter is $x_{k}$. More formally,
${\mathcal{A}}^{\prime}$ has:

  * •

States
$Q\times(\Sigma\cup\varepsilon)\times(\Gamma\cup\\{\varepsilon,\bot^{\prime}\\})$,
where $(q,\sigma,X)$ indicates the corresponding state of ${\mathcal{A}}$, the
last input letter (or, initially, $\varepsilon$), and the dedicated state-
space for the top of the semantic stack;

  * •

Alphabet $\Sigma$;

  * •

Initial state $(\iota,\varepsilon,\bot^{\prime})$;

  * •

Stack alphabet $\Gamma\cup\\{\bot^{\prime}\\}$

  * •

Transitions as detailed below.

  * •

Acceptance condition $\alpha$, where treating a state $(q,\sigma,X)$ of
${\mathcal{A}}^{\prime}$ as the state $q$ of ${\mathcal{A}}$.

The transitions of ${\mathcal{A}}^{\prime}$ are the following, where from each
state we consider the cases of $\sigma$, the previous letter, and
$\sigma^{\prime}$, the current letter, being push-, pop-, or noop-letters:

  * •

From the initial state:

    * –

$((\iota,\varepsilon,\bot^{\prime}),\bot)\xrightarrow{\sigma^{\prime}\mid\textsf{push}\bot^{\prime}}(\iota,\sigma^{\prime},\varepsilon)$;

    * –

No pop from an empty stack;

    * –

$((\iota,\varepsilon,\bot^{\prime}),\bot)\xrightarrow{\sigma^{\prime}\mid\textsf{noop}}(\iota,\sigma^{\prime},\bot^{\prime})$.

  * •

After a push, that is, for $\sigma$ a push-letter:

    * –

For each transition $(q,X)\xrightarrow{\sigma\mid\textsf{push}Y}q^{\prime}$ in
${\mathcal{A}}$ (where $X\in\Gamma$):

      * *

$((q,\sigma,\varepsilon),X)\xrightarrow{\sigma^{\prime}\mid\textsf{push}Y}(q^{\prime},\sigma^{\prime},\varepsilon)$;

      * *

$((q,\sigma,\varepsilon),X)\xrightarrow{\sigma^{\prime}\mid\textsf{pop}}(q^{\prime},\sigma^{\prime},X)$;

      * *

$((q,\sigma,\varepsilon),X)\xrightarrow{\sigma^{\prime}\mid\textsf{noop}}(q^{\prime},\sigma^{\prime},Y)$.

    * –

For each transition $(q,\bot)\xrightarrow{\sigma\mid\textsf{push}Y}q^{\prime}$
in ${\mathcal{A}}$:

      * *

$((q,\sigma,\varepsilon),\bot^{\prime})\xrightarrow{\sigma^{\prime}\mid\textsf{push}Y}(q^{\prime},\sigma^{\prime},\varepsilon)$;

      * *

$((q,\sigma,\varepsilon),\bot^{\prime})\xrightarrow{\sigma^{\prime}\mid\textsf{pop}}(q^{\prime},\sigma^{\prime},\bot^{\prime})$;

      * *

$((q,\sigma,\varepsilon),\bot^{\prime})\xrightarrow{\sigma^{\prime}\mid\textsf{noop}}(q^{\prime},\sigma^{\prime},Y)$.

  * •

After a pop or noop, that is, for $\sigma$ a pop\- or noop-letter:

    * –

For each transition $(q,X)\xrightarrow{\sigma\mid\textsf{pop}}q^{\prime}$ or
$(q,X)\xrightarrow{\sigma\mid\textsf{noop}}q^{\prime}$ in ${\mathcal{A}}$,
$X\in\Gamma$, $Y\in\Gamma\cup\\{\bot^{\prime}\\}$:

      * *

$((q,\sigma,X),Y)\xrightarrow{\sigma^{\prime}\mid\textsf{push}X}(q^{\prime},\sigma^{\prime},\varepsilon)$;

      * *

$((q,\sigma,X),Y)\xrightarrow{\sigma^{\prime}\mid\textsf{pop}}(q^{\prime},\sigma^{\prime},Y)$;

      * *

$((q,\sigma,X),Y)\xrightarrow{\sigma^{\prime}\mid\textsf{noop}}(q^{\prime},\sigma^{\prime},X)$;

    * –

For each transition $(q,\bot)\xrightarrow{\sigma\mid\textsf{noop}}q^{\prime}$
in ${\mathcal{A}}$:

      * *

$((q,\sigma,\bot^{\prime}),\bot)\xrightarrow{\sigma^{\prime}\mid\textsf{push}\bot^{\prime}}(q^{\prime},\sigma^{\prime},\varepsilon)$;

      * *

No pop from an empty stack;

      * *

$((q,\sigma,\bot^{\prime}),\bot)\xrightarrow{\sigma^{\prime}\mid\textsf{noop}}(q^{\prime},\sigma^{\prime},\bot^{\prime})$.

Observe that there is bijection between runs of ${\mathcal{A}}$ and
corresponding runs in ${\mathcal{A}}^{\prime}$, where the run in
${\mathcal{A}}^{\prime}$ is one letter behind and the stack of ${\mathcal{A}}$
is simulated by the semantic stack of ${\mathcal{A}}^{\prime}$. Therefore the
two automata recognise the same language.

Furthermore, $G_{1}({\mathcal{A}}^{\prime},{\mathcal{A}})$ since Eve can first
take the dummy transition from the initial state and then copy Adam’s
transitions to obtain a run that is accepting whenever Adam’s run is
accepting. We conclude that ${\mathcal{A}}^{\prime}$ is a $1$-token ghost of
${\mathcal{A}}$.

We proceed to show that history-determinism and guidability coincide for the
class of $\omega$-VPA. We shall do this using the criterion of Theorem 1.1.3,
that requires us to construct a safety-VPA recognising the plays of a winning
strategy of Adam in the letter game on an $\omega$-VPA, if the $\omega$-VPA is
not history-deterministic. Towards this, we use the so-called _stair-parity
VPAs_ as an intermediary.

#### Stair-parity automata

While deterministic parity VPAs are not as expressive as nondeterministic
parity VPAs, it is nevertheless possible to determinise nondeterministic
parity VPAs into deterministic _stair-parity_ VPAs. A stair-parity VPA has the
same components as a parity VPA, just that the acceptance condition is
different for run.

Given a run $\rho$ of a stair-parity VPA, consider the sequence
$\rho^{\prime}$ obtained by discarding configurations for which a future
configuration of smaller stack-height exists. Observe that this sequence
$\rho^{\prime}$ must be infinite. We write that the run $\rho$ satisfies the
stair-parity condition if $\rho^{\prime}$ satisfies the parity condition. A
stair-parity VPA ${\mathcal{A}}$ accepts a word $w$ iff there is a run of
${\mathcal{A}}$ on $w$ that satisfies the stair-parity condition.

We use the following two known results on stair-parity VPAs.

######  Lemma C.9.

  1. 1.

Every nondeterministic parity VPA can be determinised to a language-equivalent
deterministic stair-parity VPA [16, Theorem 1].

  2. 2.

Let ${\mathcal{G}}$ be a two-player turn-based game on a potentially infinite
arena between Adam and Eve whose winning condition for Eve is given by a
deterministic stair-parity VPA ${\mathcal{A}}$. Then, the winning player has a
winning strategy which can be implemented by a deterministic visibly pushdown
transducer ${\mathcal{M}}$, that takes as input the transitions $\Delta_{A}$
of ${\mathcal{A}}$. Furthermore, the transition on a push (resp. pop and noop)
letter of ${\mathcal{A}}$ in $\Delta_{A}$ is a push (resp. pop and noop)
letter of ${\mathcal{M}}$ [10, Theorem 9].

See 5.7

######  Proof C.10.

We will use the criterion of Theorem 1.1.3.

First, note that an $\omega$-VPA ${\mathcal{B}}$ with any $\omega$-regular
acceptance condition $\beta$ can be replaced by an $\omega$-VPA
${\mathcal{A}}$ with a parity condition, such that ${\mathcal{A}}$ accepts the
same language as ${\mathcal{B}}$, and furthermore, the nondeterministic
choices in ${\mathcal{A}}$ are exactly those of ${\mathcal{B}}$: we construct
${\mathcal{A}}$ by taking the product of ${\mathcal{B}}$ with a deterministic
parity automaton whose alphabet is the transitions of ${\mathcal{B}}$, and
which recognises the acceptance condition $\beta$. Such a deterministic parity
automaton always exists; see [3], for instance. As ${\mathcal{A}}$ and
${\mathcal{B}}$ are equivalent and have the same nondeterministic choices, the
letter games on them are isomorphic, and so are the simulation games and token
games. We can thus proceed with the proof, assuming that the considered
$\omega$-VPA has a parity acceptance condition.

We will describe the letter-game on an $\omega$-VPA with parity acceptance as
a game with a finite arena and an $\omega$-VPA winning condition to show that
Adam’s winning strategies can be implemented by visibly pushdown transducers.
We will then turn this transducer into an $\omega$-VPA recognising the plays
that agree with Adam’s strategy, to then apply Theorem 1.1.3.

The arena consists of the product of the state-space of ${\mathcal{A}}$ with
the input alphabet $\Sigma$, so that at every other turn, Adam chooses a
letter, and every other turn, Eve chooses a matching transition. It will be
technically convenient to only label Eve’s turns with the transition chosen by
Eve, which includes the letter played by Adam. A play then consists of the
sequence of transitions played by Eve, from which we can also read the word
read by Adam. Adam’s winning condition is the intersection between
$\\{w\leavevmode\nobreak\ |\leavevmode\nobreak\ $ the word component of $w$ is
in $L({\mathcal{A}})\\}$ and the set of Eve’s runs that are rejecting or
invalid. We argue that this is recognised by an $\omega$-VPA that is
synchronised with $\Sigma$. To check whether Eve’s run is rejecting or
invalid, we take a copy ${\mathcal{D}}$ of ${\mathcal{A}}$ that reads the
transitions chosen by Eve and deterministically simulates Eve’s run. It then
accepts if either Eve chooses an invalid transition (pop on an empty stack or
a transition that is not enabled at the right mode) or if the resulting run
fails the parity condition (which we can easily complement). Then, let
${\mathcal{A}}^{\prime}$ be the intersection of ${\mathcal{A}}$ and
${\mathcal{D}}$. Since $\omega$-VPAs are closed under intersection [1, Theorem
6], the result is still an $\omega$-VPA. By construction, it recognises Adam’s
winning condition.

The letter game on an $\omega$-VPA can therefore be seen as a finite-arena
game with an $\omega$-VPA winning condition for Adam, which can be
determinised into an equivalent deterministic stair-parity VPA (Lemma C.9).

Then, the game can be seen as a game played on the LTS of a deterministic
$\omega$-VPA with a stair parity winning condition. In such games, the winning
player has a winning strategy implemented by a deterministic visibly pushdown
transducer ${\mathcal{M}}$, of which the alphabet consists of the transitions
$\Delta_{\mathcal{A}}$ of ${\mathcal{A}}$, and $\textsf{push},\textsf{pop}$
and noop transitions of ${\mathcal{A}}$ are $\textsf{push},\textsf{pop}$ and
noop letter for ${\mathcal{M}}$, respectively [10, Theorem 9]. In other words,
projected onto the letters of the transitions, this alphabet is synchronised
with $\Sigma$.

We can now interpret this transducer ${\mathcal{M}}$ as a safety $\omega$-VPA
${\mathcal{B}}$ that recognises the plays of this winning strategy for Adam in
the letter game of ${\mathcal{A}}$, by interpreting the outputs of the
transducer as part of the input. In other words, the automaton
${\mathcal{B}}$, with alphabet $\Delta_{\mathcal{A}}\times\Sigma$ has the same
state-space as ${\mathcal{M}}$ and transitions
$q\xrightarrow{(t,a)}q^{\prime}$ if ${\mathcal{M}}$ has transition
$q\xrightarrow{t:a}q^{\prime}$ that produces $a$ when reading $t$ at state
$q$. To deal with the initial output of ${\mathcal{M}}$, the initial state of
${\mathcal{B}}$ only has outgoing transitions over $(t,a)$ such that $t$ is a
transition of ${\mathcal{A}}$ over the initial output of ${\mathcal{M}}$.
Then, ${\mathcal{B}}$, seen as a safety automaton, recognises the set of plays
of the letter game consistent with Adam’s strategy given by ${\mathcal{M}}$.

This automaton ${\mathcal{B}}$ is then as required for the application of
criterion Theorem 1.1.3, since $\omega$-VPAs are closed under $1$-token ghost
from Lemma C.7. We thus conclude that guidability and history-determinism
coincide for $\omega$-VPAs.

###  C.3 Timed automata

We define a ${\mathsf{Delay}}$ operation for timed automata and show that
${\mathsf{Delay}}({\mathcal{T}})$ is a 1-token ghost of the automaton
${\mathcal{T}}$ (Lemma C.16). As the one-token game characterises history-
determinism on safety/ reachability timed automata [7], we get by Theorem
1.1.2 that history-determinism and guidability coincide for them.

The timed alphabet is infinite and therefore unsuitable for a product
construction. Hence, we have to store the region that the previous timed
letter produces in the state space. Furthermore, because time does not wait
for our one-letter lag to advance, we duplicate each clock, using one copy for
comparisons in guards while the other is reset at each transition, just in
case the chosen transition actually resets this clock. The copy that is reset
at each transition is upgraded to be the clock used to check guards, while the
other one is now reset at each transition.

We first describe the regions formally. For each clock $x\in C$, let $c_{x}$
be the largest constant in any guard involving $x$ in ${\mathcal{T}}$. Let
$R_{x}$ be the set consisting of the following intervals in $\mathbb{R}$:

  * •

The points $i$, for each $i\in\mathbb{N}$ with $0\leq i\leq c_{x}$.

  * •

The open intervals $(i,i+1)$ for each $i\in\mathbb{N}$ with $0\leq i<c_{x}$.

  * •

The open interval $(c_{x},\infty)$, which consists of all values greater than
$c_{x}$.

We let ${\mathcal{R}}=\prod_{x\in C}R_{x}$ to be the set of regions. For each
region $r\in{\mathcal{R}}$, let $g_{r}\in{\mathcal{B}}(C)$ be a guard such
that a valuation $\nu$ belongs to the region $r$ if and only if $\nu$
satisfies the guard $g_{r}$, i.e. $\nu\models g_{r}$. Finally, we say a region
$r$ satisfies a guard $g$, denoted by $r\models g$ if and only if all
valuations $\nu\in r$ satisfy $g$.

As mentioned earlier, for each clock $x$ in ${\mathcal{T}}$, we will have two
clocks in ${\mathsf{Delay}}({\mathcal{T}})$ that we denote by $(x,0)$ and
$(x,1)$. Thus, the clocks in ${\mathsf{Delay}}({\mathcal{T}})$ are given by
$C\times\\{0,1\\}$. The states in ${\mathsf{Delay}}({\mathcal{T}})$, apart
from an additional initial state, are of the form $(q,\sigma,r,f)\subseteq
Q\times\Sigma\times{\mathcal{R}}\times\\{0,1\\}^{C}$, where
$f:C\xrightarrow{}\\{0,1\\}$ is a function. This is used to encode which clock
amongst $(x,0)$ and $(x,1)$ is _active_ in ${\mathsf{Delay}}({\mathcal{T}})$
at any given moment, for each clock $x$ in ${\mathcal{T}}$. For a valuation
$\mu:C\times\\{0,1\\}\xrightarrow{}\mathbb{R}$ at a state $(q,\sigma,r,f)$ in
${\mathsf{Delay}}({\mathcal{T}})$, the _active valuation_
$\left.\mu\right|_{f}=\mu(x,f(x))$ is the values of the clocks of the form
$(x,f(x))$. The clocks that are not active are called _passive_ , and these
are of the form $(x,1-f(x))$.

We also extend each guard $g\in{\mathcal{B}}(C)$ to guards for the active
clocks in $C\times\\{0,1\\}$: Let $g[f]\in{\mathcal{B}}(C\times\\{0,1\\})$ be
the guard obtained by replacing each instance of a clock $x$ in $g$ by
$(x,f(x))$. Finally, to deal with resets of clocks $X\subseteq C$, we need to
switch the active and passive clocks in ${\mathsf{Delay}}({\mathcal{T}})$
amongst the clocks that correspond to $X$. This is done by the function
$f^{X}$ obtained by swapping the active and passive clocks associated to $X$
in $f$. That is, $f^{X}(c)=f(c)$ if $c\notin X$, and $f^{X}(c)=1-f(c)$ if
$c\in X$.

Let us denote the active and passive clocks with respect to a function $f$ by
$A[f]$ and $P[f]$, respectively. If the set of clocks reset in the $i^{th}$
transition in ${\mathcal{T}}$ is $X$, then the following clocks would be reset
in the corresponding $(i+1)^{th}$ transition in
${\mathsf{Delay}}({\mathcal{T}})$:

  1. 1.

The passive clocks $\\{(c,1-f(c))\leavevmode\nobreak\ |\leavevmode\nobreak\
c\notin X\\}$ not in $X$.

  2. 2.

The active clocks $\\{(c,f(c))\leavevmode\nobreak\ |\leavevmode\nobreak\ x\in
X\\}$ of $X$.

We now formally define the construction of ${\mathsf{Delay}}({\mathcal{T}})$
described above:

######  Definition C.11.

Given a timed automaton ${\mathcal{T}}=(\Sigma,Q,q_{0},C,\delta,F)$, we define
the timed automaton
${\mathsf{Delay}}({\mathcal{T}})=(\Sigma,Q^{\prime},s,C,\delta^{\prime},F^{\prime})$,
where the set of states $Q^{\prime}$ consists of

  * •

The initial state, $s$

  * •

Tuples $(q,\sigma,r,f)\in Q\times\Sigma\times{\mathcal{R}}\times\\{0,1\\}^{C}$

The set $\delta^{\prime}$ consists of the following transitions:

  * •

The transitions $(s,\sigma,g_{r}[f_{0}],P[f_{0}],(q_{0},\sigma,r,f_{0}))$ for
each $\sigma\in\Sigma,r\in R$, where $f_{0}$ is the function
$f:C\xrightarrow{}\\{0,1\\}$ such that $f(x)=0$ for all $x\in C$.

  * •

The transitions $((q,\sigma,r,f),$
$\sigma^{\prime},g_{r^{\prime}}[f^{X}],P[f^{X}],(q^{\prime},\sigma^{\prime},r^{\prime},f^{X}))$
such that $r\models g$, for every transition $(q,\sigma,g,X,q^{\prime})$ in
${\mathcal{T}}$.

The set $F^{\prime}$ consists of states of the form $(q,\sigma,r,f)$ where
$q\in F$ is an accepting state in ${\mathcal{T}}$, as well as the state $s$ if
$q_{0}$ is in $F$.

We show next, via the following two lemmas, that
${\mathsf{Delay}}({\mathcal{T}})$ is a one-token ghost of ${\mathcal{T}}$.

######  Lemma C.12.

Let ${\mathcal{T}}=(\Sigma,Q,q_{0},C,\delta,F)$ be a safety/reachability timed
automaton. Then, Eve wins
$G_{1}({\mathsf{Delay}}({\mathcal{T}}),{\mathcal{T}})$.

######  Proof C.13.

We show that Eve can copy the $i^{th}$ transition of ${\mathcal{T}}$ in her
$(i+1)^{th}$ transition of ${\mathsf{Delay}}({\mathcal{T}})$, to establish
that she wins the one-token game between ${\mathsf{Delay}}({\mathcal{T}})$ and
${\mathcal{T}}$.

In the first round, after Adam selects a letter $(\sigma_{0},d_{0})$, Eve’s
transition in ${\mathsf{Delay}}({\mathcal{T}})$ is deterministic:
$(s,\sigma_{0},g_{r}[f_{0}],P[f_{0}],(q_{0},\sigma_{0},r_{0},f_{0})$, where
$r_{0}$ is the unique region of the valuation $\nu:C\xrightarrow{}\mathbb{R}$
which maps all clock values to $d_{0}$. Then, Adam would select some
transition $(q_{0},\sigma_{0},g_{0},X,q_{1})$ in ${\mathcal{T}}$, resulting in
valuation $\nu_{0}$.

After $i>0$ rounds, suppose Eve’s token in ${\mathsf{Delay}}({\mathcal{T}})$
is in state $p_{i}=(q_{i-1},\sigma_{i-1},r_{i-1},f_{i-1})$, with valuation
$\mu_{i}$, and Adam’s token in ${\mathcal{T}}$ after $i-1$ rounds is at the
state $q^{\prime}$ with valuation $\nu_{i-1}$. We will show that Eve has a
strategy to preserve the following invariant:

  1. I1

Adam’s state $q^{\prime}$ after $i$ rounds is $q_{i-1}$, same as the component
of $Q$ in $p_{i}$.

  2. I2

The active valuation $\left.\mu_{i-1}\right|_{f_{i-1}}$ equals
$\nu_{i-1}+d_{i}$, while all the passive clocks in $\mu_{i}$ are assigned the
value $0$.

  3. I3

The region $r_{i-1}$ is the unique region of the active valuation
$\left.\mu_{i-1}\right|_{f_{i-1}}$.

It is clear that the invariant holds after the first round. Suppose it holds
after $i>0$ rounds. We will show that Eve has a strategy to preserve the
invariant after $i+1$ rounds:

Suppose, after $i$ rounds, Eve’s configuration is given by $\langle
p,\mu\rangle=\langle(q,\sigma,r,f),\mu\rangle$, while Adam’s transition in the
$i^{th}$ round was $\langle q,\nu\rangle\xrightarrow{\sigma,d}\langle
q,\nu+d\rangle\xrightarrow{g,X}\langle q^{\prime},\nu^{\prime}\rangle$. By the
invariant, we know that $\left.\mu\right|_{f}=\nu+d$, and $r$ is the region of
$\left.\mu\right|_{f}$. In the $(i+1)^{th}$ round of the play:

  1. 1.

Adam selects a timed letter $(\sigma^{\prime},d^{\prime})$.

  2. 2.

Eve the transition
$\langle(q,\sigma,r,f),\mu\rangle\xrightarrow{\sigma^{\prime},d^{\prime}}\langle(q,\sigma,r,g),\mu+d^{\prime}\rangle$
$\xrightarrow{g[f^{X}],P[f^{X}]}\langle(q^{\prime},\sigma^{\prime},r^{\prime},f^{X}),\mu^{\prime}\rangle$.
Note that this transition exists as, by the invariant, $r$ is the region of
$\left.\mu\right|_{f}=\nu+d$, which satisfies the guard $g$ due to Adam being
able to take his transition in the $i^{th}$ round.

  3. 3.

Adam a transition $\langle
q^{\prime},\nu^{\prime}\rangle\xrightarrow{\sigma^{\prime},d^{\prime}}\langle
q^{\prime},\nu^{\prime}+d^{\prime}\rangle\xrightarrow{g^{\prime},X^{\prime}}\langle
q^{\prime\prime},\nu^{\prime\prime}\rangle$.

It is clear that the invariant I1 is satisfied after the $(i+1)^{th}$ round.

As for the invariant I2, by the induction hypothesis, we know that
$\left.\mu\right|_{f}=\nu+d$. We need to show that
$\left.\mu^{\prime}\right|_{f^{X}}=\nu^{\prime}+d^{\prime}$. Note that
$\nu^{\prime}+d^{\prime}=(\nu+d)[X]+d^{\prime}$, which is,
$\nu(c)+d+d^{\prime}$ if $c\notin X$, and $d^{\prime}$ if $c\in X$. Let us
take a look at how the valuation $\mu^{\prime}$ is obtained. First, we add the
duration $d^{\prime}$ to the valuation $\mu$. This causes all active clocks
with respect to $f$ to have the value $\nu(c)+d^{\prime}+d$, and the passive
clocks to have the value $d^{\prime}$. Then, the function $f^{X}$ swaps active
and passive clocks of $X$ and resets the clocks that are now passive with
respect to $f^{X}$ to obtain $\mu^{\prime}$. Thus, we have that
$\mu^{\prime}(c,f^{X}(c))=\mu(c,f(c))+d^{\prime}=\nu(c)+d+d^{\prime}=[\nu^{\prime}+d^{\prime}](c)\text{
if $c\notin X$}$, and
$\mu^{\prime}(c,f^{X}(c))=d^{\prime}=[\nu^{\prime}+d^{\prime}](x)$ if $c\in
X$. This implies that
$\left.\mu^{\prime}\right|_{f^{X}}=\nu^{\prime}+d^{\prime}$. It is clear that
the passive clocks with respect to $f^{X}$ have value 0, as they were just
reset. Thus, the condition I2 is also an invariant.

The invariant I3 holds as $\left.\mu^{\prime}\right|_{f^{X}}$ must have
satisfied the guard $g_{r^{\prime}}[f^{X}]$ to have taken the transition,
which implies that $r^{\prime}$ is the unique region of
$\left.\mu^{\prime}\right|_{f^{X}}$.

Having shown that Eve has a strategy which preserves the invariants I1, I2 and
I3, it is easy to see that such a strategy is winning in
$G_{1}({\mathsf{Delay}}({\mathcal{T}}),{\mathcal{T}})$: By the invariant I1
and the construction of the accepting states of
${\mathsf{Delay}}({\mathcal{T}})$, Eve’s run in
${\mathsf{Delay}}({\mathcal{T}})$ is accepting if and only if Adam’s run in
${\mathcal{T}}$ is accepting.

We proceed with showing that
$L({\mathsf{Delay}}({\mathcal{T}}))=L({\mathcal{T}})$.

######  Lemma C.14.

Given a timed automaton ${\mathcal{T}}$, we have
$L({\mathsf{Delay}}({\mathcal{T}}))=L({\mathcal{T}})$.

######  Proof C.15.

$L({\mathcal{T}})\subseteq L({\mathsf{Delay}}({\mathcal{T}}))$ is clear by
Lemma C.12. As for $L({\mathsf{Delay}}({\mathcal{T}}))\subseteq
L({\mathcal{T}})$, consider a sequence $(\langle p_{i},\mu_{i}\rangle)_{i\geq
0}$ of states of ${\mathsf{Delay}}({\mathcal{T}})$ that forms a run on the
timed word $(\sigma_{i},d_{i})_{i\geq 0}$. Let $q_{j}$ be the state component
of $p_{j+1}$, and let $\nu_{j}:C\xrightarrow{}\mathbb{R}$ be obtained by
subtracting $d_{j}$ from $\left.\mu_{j+1}\right|_{f_{j+1}}$, the active
valuation of $\langle p_{j},\mu_{j+1}\rangle$, for each $j\geq 0$. Then, it is
easy to verify from construction that the sequence $(\langle
q_{i},\nu_{i}\rangle)_{i\geq 0}$ is a run in ${\mathcal{T}}$ on the timed word
$(\sigma_{i},d_{i})_{i\geq 0}$ which is accepting if and only if $(\langle
p_{i},\mu_{i}\rangle)_{i\geq 0}$ is an accepting run in
${\mathsf{Delay}}({\mathcal{T}})$.

From Lemmas C.12 and C.14, we can conclude:

######  Lemma C.16.

The classes of safety and reachability timed automata are closed under
$1$-token ghost.

As $G_{1}$ characterises history-determinism on safety and reachability timed
automata [7], by Theorem 1.1.2 history-determinism and guidability coincide:
See 5.9

###  C.4 Linear automata

See 5.13

######  Proof C.17.

History-determinism implies guidability with respect to all classes. For the
other direction, consider a linear automaton
${\mathcal{A}}=(\Sigma,Q,\iota,\Delta,\alpha)$ that is not $\mathrm{HD}$, and
let ${\mathcal{M}}=(\Delta,\Sigma,M,m_{0},\Delta_{M}:M\times\Delta\to
M,\gamma:M\to\Sigma)$ be a deterministic finite-state transducer representing
a finite-memory winning strategy $\mathsf{s}_{M}$ of Adam in the letter game.

Let ${\mathcal{P}}=(\Delta,M\times Q,p_{0},\Delta_{P})$ be the deterministic
safety automaton that is obtained by the composition of ${\mathcal{M}}$ with
${\mathcal{A}}$. It’s states are $Q\times M$, we have the transition
$(m,q)\xrightarrow{\delta}(m^{\prime},q^{\prime})$ if $\gamma(m)=\sigma$,
$\delta=q\xrightarrow{\sigma}q^{\prime}$ is a transition in ${\mathcal{A}}$,
and $m\xrightarrow{\delta}m^{\prime}$ is the unique transition in
${\mathcal{M}}$. Note that ${\mathcal{P}}$ recognises the set of plays that
can happen in the letter game on ${\mathcal{A}}$ if Adam plays according to
$\mathsf{s}_{M}$.

Let ${\mathcal{N}}=(\Sigma,N,n_{0},\Delta^{\prime})$ be the safety automaton
that results from taking the projection of ${\mathcal{P}}$ to the alphabet
$\Sigma$ of ${\mathcal{A}}$. Note that ${\mathcal{N}}$ need not be linear. For
each $q\in Q$, let $N_{q}$ be states in ${\mathcal{N}}$ of the form $(m,q)$
for some $m\in M$. Note that there is no cycle in ${\mathcal{N}}$ that visits
$N_{q}$ and $N_{q^{\prime}}$, for two different states $q,q^{\prime}\in Q$, as
${\mathcal{A}}$ is linear. Hence any cycle in ${\mathcal{N}}$ must be
contained entirely in one of the $N_{q}$’s. Let ${\mathcal{N}}_{q}$ be the
transition system that consists of all states in $N_{q}$ and transitions
between them.

We proceed by adapting ${\mathcal{N}}$ to a linear automaton
${\mathcal{N}}^{\prime}$ that will still correspond to a winning strategy of
Adam in the letter game, and will thus constitute a projection of a
deterministic automaton ${\mathcal{P}}^{\prime}$ onto the alphabet $\Sigma$,
where ${\mathcal{P}}^{\prime}$ is over the alphabet of transitions of
${\mathcal{A}}$ and recognises the plays of a winning strategy of Adam in the
letter game. Once achieving that, we can apply the ${\mathsf{Delay}}$
construction on ${\mathcal{N}}^{\prime}$ – it will not introduce, in this
case, non-self cycles, since the states of ${\mathcal{N}}^{\prime}$ (as the
states of ${\mathcal{N}}$), have outgoing transitions only on a single letter.
Hence, we satisfy Theorem 1.1.3, proving the stated claim.

We elaborate below on how we adapt ${\mathcal{N}}$ into
${\mathcal{N}}^{\prime}$.

Observe that since $M$ is a winning strategy for Adam in the letter game,
every word that ${\mathcal{N}}$ reads is accepting in ${\mathcal{A}}$, and
every run of ${\mathcal{N}}$ eventually remains in a component
${\mathcal{N}}_{q}$, where $q$ is a rejecting state of ${\mathcal{A}}$.

Therefore, if a component ${\mathcal{N}}_{q}$ contains a cycle, then $q$ must
be a rejecting state of ${\mathcal{A}}$. Furthermore, note that every state of
${\mathcal{N}}$, and thus of ${\mathcal{N}}_{q}$, has outgoing transitions on
a single alphabet, and that ${\mathcal{N}}_{q}$ is deterministic, as
${\mathcal{A}}$ has at most one self-loop at the state $q$ on any letter
$\sigma$. Hence, from each state $n$ of ${\mathcal{N}}_{q}$, there is at most
one infinite word $w_{n}$ that can be generated within ${\mathcal{N}}_{q}$.
The following claim will be the key to linearising ${\mathcal{N}}$ into
${\mathcal{N}}^{\prime}$.

Claim: there is a number $K\in\mathbb{N}$, such that for every state $n$ that
lies within a cycle of ${\mathcal{N}}_{q}$ and finite word $u$ over which
${\mathcal{N}}$ can reach $n$, there is a run $\rho$ in ${\mathcal{A}}$ on the
finite word $u\cdot w[0..K]$ such that $\rho$ ends in an accepting state $f$
of ${\mathcal{A}}$, and $f$ has self loops on all letters that appear in the
word $w[K{+}1..\infty]$.

######  Proof C.18 (Proof of the claim).

We will show that the result holds for $K=|N_{q}|\cdot 2^{|Q|}$. Let $v$ be
the unique shortest finite word whose unique run in ${\mathcal{N}}_{q}$ starts
at $n$ and ends at $n$. Note that the length of the word $v$ is at most
$|N_{q}|$. For every number $i\in\mathbb{N}$, let $X_{i}$ be the set of
${\mathcal{A}}$’s states that can be reached upon reading the finite word
$uv^{i}$ in ${\mathcal{A}}$.

By the pigeonhole principle, two of the subsets $X_{i}$ and $X_{j}$ for $i<j$
must be equal. Let $d$ be the difference between $j$ and $i$. It follows that
the sequence $\\{X_{l}\\}_{l\geq 0}$ is eventually periodic after $i$ with
period at most $d$, that is $X_{i+k}=X_{i+k+d}$ for all $k\geq 0$. As the word
$uv^{\omega}$ is accepting, there is an accepting state $f$ of ${\mathcal{A}}$
reached by some $uv^{l}$ that has a self-loop on all the letters of $v$. This
state $f$ must belong to all of $X_{l}$’s for all $l$ large enough. As the
sequence $\\{X_{k}\\}_{k\geq i}$ is periodic, it follows that $f\in X_{k}$ for
all $k\geq i$.

As the length of $v^{i}$ is at most $N_{q}\times 2^{|Q|}$, the state $f$ is
thus reached upon reading the finite word $w[0..K]$, and has self-loops on all
letters in the word $w[K{+}1..\infty]$.

We now use the claim for generating the required automaton
${\mathcal{N}}^{\prime}$ from ${\mathcal{N}}$, and thus completing the proof.
We shall modify ${\mathcal{N}}_{q}$ to have $K+1$ copies of the states in
${\mathcal{N}}_{q}$, that is $N^{\prime}_{q}=N_{q}\times[0..K]$. Then, for
each transition $n\xrightarrow{\sigma}n^{\prime}$ in ${\mathcal{N}}_{q}$, we
have the transition $(n,i)\xrightarrow{\sigma}(n^{\prime},i{+}1)$ for
$i\in[0..K)$, as well as the self-loop $(n,K)\xrightarrow{\sigma}(n,K)$ in the
last copy.

Then, in ${\mathcal{N}}^{\prime}$ we replace every component
${\mathcal{N}}_{q}$ with ${\mathcal{N}}^{\prime}_{q}$, while replacing a
transition $n^{\prime}\to n$ from a state $n^{\prime}\in N^{\prime}\setminus
N^{\prime}_{q}$ to a state $n\in N_{q}$ by the transition
$n^{\prime}\to(n,0)$, and adding for every transition $n\to n^{\prime}$ from a
state $n\in N_{q}$ to a state $n^{\prime}\in N^{\prime}\setminus
N^{\prime}_{q}$, the transitions $(n,i)\to n^{\prime}$, for every
$i\in[0..k]$.

The only cycles in ${\mathcal{N}}^{\prime}$ are self loops. Furthermore,
${\mathcal{N}}^{\prime}$ represents a winning strategy of Adam since: i) Every
run of ${\mathcal{N}}^{\prime}$ that does not eventually remain in
${\mathcal{N}}^{\prime}_{q}$ has a corresponding run in ${\mathcal{N}}$; and
ii) Every run of ${\mathcal{N}}^{\prime}$ that eventually remains in
${\mathcal{N}}^{\prime}_{q}$ is rejecting for Eve, as $q$ is a rejecting state
of ${\mathcal{A}}$, and it corresponds to a word in the language of
${\mathcal{A}}$, by the claim.

##  Appendix D Proofs of Section 6

###  D.1 Automata with bounded resources

See 6.1

######  Proof D.1.

Consider the Büchi automaton ${\mathcal{A}}$ depicted in Figure 2, accepting
words with a finite number of $a$’s. ${\mathcal{A}}$ is not history-
deterministic, as Adam can win the letter game by choosing $b$ whenever Eve is
in an odd state of ${\mathcal{A}}$, and $a$ whenever she is in an even state.

We now show that ${\mathcal{A}}$ can simulate every Büchi automaton
${\mathcal{A}}^{\prime}\leq{\mathcal{A}}$ with up to $2n$ states. Observe that
since ${\mathcal{A}}^{\prime}$ cannot accept a word with infinitely many
$a$’s, its maximally strongly connected components (MSCCs) cannot have both a
transition on $a$ and an accepting state. We call an MSCC accepting if it
contains an accepting state, and rejecting otherwise.

We define the following strategy for Eve in the simulation game between
${\mathcal{A}}$ and ${\mathcal{A}}^{\prime}$: If Adam is in an accepting MSCC
while she is in an odd state, she moves to the next even state. In other
cases, she remains in her state. We claim that Eve’s strategy is winning in
$Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$. Indeed, if Adam’s run is
accepting, he must eventually end in an accepting MSCC, and by Eve’s strategy,
so will she, unless she runs out of states. Since ${\mathcal{A}}^{\prime}$ can
have up to $2n$ MSCCs, Adam can move at most $n$ times from a rejecting MSCC
(or from the initial state of ${\mathcal{A}}^{\prime}$) to an accepting MSCC.
(If he starts in an accepting MSCC, he still needs at least $2n{+}1$ MSCCs in
order to have $n{+}1$ such moves to an accepting MSCC). Hence, Eve does not
run out of states and wins $Sim({\mathcal{A}},{\mathcal{A}}^{\prime})$.

#### Timed Automata with bounded clocks.

See 6.2

######  Proof D.2.

For technical convenience, in this proof we use timestamps rather than delays
to write timed words.

Consider the language of finite timed words
$L_{k}\subseteq(\\{a\\}\times\mathbb{R}_{\geq
0})^{+}\cdot(\\{b\\}\times\mathbb{R}_{\geq
0})\cdot(\\{a\\}\times\mathbb{R}_{\geq 0})^{+}$ over $\Sigma=\\{a,b\\}$ that
contain a subword $w$ of the form
$w=(a,t_{1})(a,t_{2})\cdots(a,t_{k})(b,t)(a,t_{1}{+}1)$ $(a,t_{2}{+}1)\cdots$
$(a,t_{k}{+}1),$ such that $t_{1}<t_{2}<\cdots<t_{k}<t<t_{1}{+}1$.

We construct a timed automaton ${\mathcal{T}}$ with clocks
$C\\!=\\!\\{c_{1},c_{2},\cdots\\!,c_{k}\\}$ that accepts $L_{k}$ and is
guidable in $\mathbb{T}_{k}$, but not $\mathrm{HD}$. The automaton
${\mathcal{T}}$ consists of two components: i) a nondeterministic component in
which all runs stay in till a $b$ is seen; and ii) a deterministic component
in which all runs of the timed automaton go to and stay in after a $b$ is
seen.

At a high level, the first component consists of states from where any set of
clocks may be non-deterministically reset, upon reading an $a$. Upon reading
$b$, the timed automaton moves to the second component. The second component
checks deterministically whether any clock value is 1 when an $a$ is read, and
it moves to an accepting sink when all clocks have tested positively for 1 at
least once.

We now describe the two components in detail. The first consists of states
$(S,1)$, where $S$ is a subset of $C$, and $1$ indicates the first component.
The set $S$ tracks which clocks are reset at least once in the run so far. The
state $(\emptyset,1)$ is the initial state in ${\mathcal{T}}$. The transitions
on $a$ in the first component are of the form
$((S,1),a,g_{\top},X,(S^{\prime},1))$, where $g_{\top}=\top$ is the guard that
accepts all clock valuations, $X$ is the set of clocks that are reset, and
$S^{\prime}=S\cup X$.

The second component consists of a rejecting sink ${\mathsf{Reject}}$ and
states of the form $(S,2)$, where $S$ is a subset of $C$ and $2$ indicates the
second component. The set $S$ tracks the clocks that have not positively
tested for $1$ at an $a$-transition yet. Naturally, the state $(\emptyset,1)$
is the only accepting state in ${\mathcal{T}}$. The transitions on $a$ in the
second component are:

  1. A1.

$((S,2),a,g[y],\emptyset,(S^{\prime},2))$, where $y\in[k]$ and
$g[y]=(c_{y}=1)\bigwedge_{z\in[k]\setminus\\{y\\}}(c_{z}\neq 1)$. The set
$S^{\prime}$ is then updated to be the set $S\setminus\\{c_{y}\\}$.

  2. A2.

$((S,2),a,g[2],\emptyset,{\mathsf{Reject}})$, where $g[2]=\bigvee_{1\leq
x<y\leq k}((c_{x}=1)\land(c_{y}=1))$.

  3. A3.

$((S,2),a,g[S\neq 1],\emptyset,(S,2))$, where $g[S\neq 1]=\bigwedge_{c\in
S}(c\neq 1)$.

  4. A4.

$({\mathsf{Reject}},a,g[\top],\emptyset,{\mathsf{Reject}})$, where
$g[\top]=\top$ is the guard that accepts all clock valuations.

A transition in A1 can be taken if a clock value is $1$. This is the case if
an $a$ is being repeated exactly one time-unit apart. Furthermore, the
condition that requires other clocks to be not equal to $1$ makes sure that
the $a$’s that are repeated occur at distinct times. If there are two clocks
that have their values equal to $1$, then the automaton moves to
${\mathsf{Reject}}$ via a transition in A2. The transitions in A3 are self
loops, which are taken when none of the clock values are 1. Finally, there are
additional self loops on the sink ${\mathsf{Reject}}$ state. Since the guards
$g[y]$ for each clock $y\in C$, $g[2]$ and $g[S\neq 1]$ are all disjoint, the
second component is deterministic.

Additionally, there are the following $b$-transitions from the first to the
second component:

  1. B1

$((C,1),b,(g[b]),\emptyset,(C,2))$, where $S=C$ and $g[b]=\bigwedge_{c\in
C}((c$ $>0)\land(c<1))$ is the guard that checks that all clocks have
valuation strictly between 0 and 1.

  2. B2

$((C,1),b,\neg g[b],\emptyset,{\mathsf{Reject}})$

  3. B3

$(S,1),b,g[\top],\emptyset,{\mathsf{Reject}})$, where $S\neq C$

Only the transition B1 above does not immediately move the run to
${\mathsf{Reject}}$, and can only be taken if the guard $g[b]$ is satisfied.
Morally, the guard $g[b]$ ensures that $t_{1}+1>t$ and $t_{k}<t$ in the
description of words belonging to $L_{k}$ given at the start of the proof.

We shall argue that:

  1. 1.

The timed automaton ${\mathcal{T}}$ accepts $L_{k}$.

  2. 2.

${\mathcal{T}}$ is not $\mathrm{HD}$

  3. 3.

${\mathcal{T}}$ simulates every ${\mathcal{T}}^{\prime}\leq{\mathcal{T}}$,
such that ${\mathcal{T}}^{\prime}$ has at most $k$ clocks.

####  $T$ accepts $L_{k}$.

Consider a word $w$ in $L_{k}$, and let $t_{1}<t_{2}<\cdots<t_{k}$ be
timestamps of $k$ distinct $a$’s that occur in $w$ which are repeated one
time-unit later, with the timed letter $(b,t)$ occurring in between, such that
$t_{1}+1>t>t_{k}$. We describe an accepting run $\rho$ of ${\mathcal{T}}$ on
the word $w$. The run $\rho$ resets the clock $c_{i}$ at time $t_{i}$, for
each $i\in[k]$. Thus, after the letter $(a,t_{k})$, $\rho$ is at the state
$(C,1)$. At the letter $(b,t)$, the transition B1 is taken to the state
$(C,2)$ since the guard $g[b]$ would be satisfied: The valuation of $c_{i}$ is
$t-t_{i}$ for each $i\in[k]$, and $0<t-t_{i}<t-t_{1}<1$. The clock $c_{i}$
then tests positively for 1 at $(a,t_{i}+1)$ for each $i\in[k]$ (in the
transition A1), and at the (first) occurrence of the timed letter
$(a,t_{k}+1)$, $\rho$ moves to $(\emptyset,2)$, and stays there. As the state
$(\emptyset,2)$ is accepting, the run $\rho$ is accepting.

Conversely, consider a word $w$ that is accepted by ${\mathcal{T}}$ via the
accepting run $\rho$. Then, all the $k$ clocks must have been reset at least
once in $\rho$ in the first component: let $(a,t_{i})$ be the last timed
letter at which the clock $c_{i}$ was reset. Without loss of generality, we
may assume $t_{1}\leq t_{2}\leq\cdots\leq t_{k}$. When the timed letter
$(b,t)$ is seen, $\rho$ must take the transition B1 to $(C,2)$ since it would
be rejecting otherwise. Since the guard $g[b]$ must be satisfied to take the
transition B1, we get that at the timed letter $(b,t)$, the valuation of each
clock is strictly between 0 and 1. Thus, $t-t_{1}<1$ and $t-t_{k}>0$. In the
second component, each clock $c_{i}$ in $C$ for $i\in[k]$ tests positively for
$1$ on a timed letter $(a,t_{i}+1)$ during a transition in A1, since $\rho$
eventually reaches the state $(\emptyset,2)$. Furthermore, whenever the
valuation of clock $c_{i}$ is 1 for the first time, we must have that the
value of clock $c_{j}$ for $j\neq 1$ is not $1$. This implies that
$t_{1}<t_{2}<\cdots<t_{k}$, and hence the word $w$ is in $L_{k}$.

####  ${\mathcal{T}}$ is not $\mathrm{HD}$.

We describe a winning strategy for Adam in the letter game on ${\mathcal{T}}$.
Adam starts with the timed letters $(a,\frac{1}{k+2}),(a,\frac{2}{k+2}),$
$\cdots,(a,\frac{k+1}{k+2}),(b,1)$ in the first $k+2$ rounds, regardless of
Eve’ transitions. After the $k+2$ rounds, Eve’s token can either be at
${\mathsf{Reject}}$, or at the state $(C,2)$. In the former case, Adam gives
the letters
$(a,1+\frac{1}{k+2}),(a,1+\frac{2}{k+2}),\cdots,(a,1+\frac{k}{k+2})$ in the
next $k$ rounds, and wins because the resulting word is in the language.
Otherwise, Eve resets all clocks at least once in the run on her token so far.
Consider the clock valuations after the transition corresponding to the timed
letter $(b,1)$. Then, either

  1. 1.

There are two clocks that have the same value, say $1-\frac{i}{k+2}$ due to
them being last reset at the letter $(a,\frac{i}{k+2})$. If Adam gives letters
$(a,1+\frac{1}{k+2}),(a,1+\frac{2}{k+2}),\cdots,(a,1+\frac{k+1}{k+2})$, the
resulting word would be in the language, but Eve’s token would eventually move
to a rejecting sink state; or

  2. 2.

All clocks have distinct values. Then there is a timed letter
$(a,\frac{j}{k+2})$ such that all clocks that were reset on
$(a,\frac{j}{k+2})$ were reset later. In particular, it could also be the case
that no clock was reset when the timed letter $(a,\frac{j}{k+2})$ was seen.
Let $i\neq j$ be an element in $[k+1]$. Since all the clocks have distinct
values, there is a clock $c$ with the value $a,1-\frac{i}{k+2}$ when the
transition on the timed letter $(b,1)$ is taken. Suppose Adam gives the timed
letters $(a,1+\frac{l}{k+2})$ for each $l\in[k+1]\setminus\\{i\\}$ in the next
$k$ rounds of the letter game. Then the resulting word is accepting, while the
valuation of clock $c$ is never 1 at any transition, causing the run in Eve’s
token to be rejecting.

Thus, Adam has a winning strategy in the letter game, and hence
${\mathcal{T}}$ is not $\mathrm{HD}$.

####  ${\mathcal{T}}$ is guidable in $\mathbb{T}_{k}$.

Let ${\mathcal{T}}^{\prime}$ be a timed automaton in $\mathbb{T}_{k}$
accepting the language $L^{\prime}$. We assume for convenience that
${\mathcal{T}}^{\prime}$ has exactly $k$ clocks denoted by the set
$C=\\{c_{1},c_{2},\cdots,c_{k}\\}$, same as that for ${\mathcal{T}}$. We give
a strategy $\sigma$ for Eve in the simulation game
$Sim({\mathcal{T}},{\mathcal{T}}^{\prime})$ between ${\mathcal{T}}$ and
${\mathcal{T}}^{\prime}$ such that if Eve loses
$Sim({\mathcal{T}},{\mathcal{T}}^{\prime})$ when playing according to
$\sigma$, then $L({\mathcal{T}}^{\prime})$ is not a subset of
$L({\mathcal{T}})$. This would imply that ${\mathcal{T}}$ is guidable in
$\mathbb{T}_{k}$.

Suppose that after $i$ rounds of the simulation game, Eve’s token is at the
state $(S,1)$ with the valuation $\nu$, while Adam’s token is at the state $q$
in ${\mathcal{T}}^{\prime}$ with the valuation $\nu^{\prime}$. In the
$(i+1)^{th}$ round, if Adam selects the letter $b$ then Eve’s transition in
${\mathcal{T}}$ is determined. Otherwise, suppose Adam selects the letter
$(a,t)$ with the duration being $d$, and the transition
$(q,a,g,X,q^{\prime})$. Let $X^{\prime}$ be the set of clocks that are
integers in the valuation $\nu^{\prime}+d$. Eve’s strategy $\sigma$ takes the
transition that resets the clocks $X\cup X^{\prime}$ in ${\mathcal{T}}$. As
the second component of ${\mathcal{T}}$ is determined, Eve has at most one
transition available to her from states of the simulation game, which is the
transition that $\sigma$ chooses.

We will show that $\sigma$ is a winning strategy, unless
$L({\mathcal{T}}^{\prime})\nsubseteq L({\mathcal{T}})$. For each valuation
$\nu:C\xrightarrow{}\mathbb{R}$, let
${\mathsf{Frac}}(\nu)=\langle{\mathsf{Frac}}(\nu(c_{1})),{\mathsf{Frac}}(\nu(c_{2}),$
$\cdots,{\mathsf{Frac}}(\nu(c_{k})))\rangle$ be the $k$-tuple that consists of
the fractional part of the clock valuations of $\nu$. An inductive argument
gives us that the strategy $\sigma$ described above preserves the invariant
that after each round of the simulation game, if Adam’s token is at
$q^{\prime}$ with valuation $\nu^{\prime}$ and Eve’s token is at the state
$(S,1)$ with valuation $\nu$ in ${\mathcal{T}}$, then
${\mathsf{Frac}}(\nu)={\mathsf{Frac}}(\nu^{\prime})$.

Suppose that there is a play of the simulation game that agrees with $\sigma$,
but which Adam wins. Let $w$ be a timed word accepted by
${\mathcal{T}}^{\prime}$ via the run $\rho^{\prime}$ that Adam constructs in
the simulation game; then Eve’s run $\rho$ in ${\mathcal{T}}$ constructed
according to $\sigma$ is rejecting.

We assume that $w$ is of the form $w=(a,t_{1})(a,t_{2})\cdots(a,t_{l})(b,t)$
$(a,t^{\prime}_{1})(a,t^{\prime}_{2})\cdots(a,t^{\prime}_{m})$, as otherwise
$L({\mathcal{T}}^{\prime})\nsubseteq L({\mathcal{T}})$. Let
$\\{\alpha_{1},\alpha_{2},\cdots,$ $\alpha_{n}\\}\in[l]$ be the largest set
such that the timed letters $(a,t_{\alpha_{i}})$ and $(a,t_{\alpha_{i}}+1)$
both occur in the word $w$, $t-1<t_{\alpha_{i}}<t$ for each $i\in[n]$, and
$t_{\alpha_{i}}\neq t_{\alpha_{j}}$ for all $1\leq i<j\leq n$. We say that $n$
is the number of _good pairs_ in the word $w$. If $n<k$, then $w\notin
L_{k}=L({\mathcal{T}})$, and hence $L({\mathcal{T}}^{\prime})\nsubseteq
L({\mathcal{T}})$. Hence, suppose $n\geq k$. We will show that there is a word
$\hat{w}$ that is accepted by ${\mathcal{T}}^{\prime}$ but has strictly less
than $k$ good pairs. This will imply that $L({\mathcal{T}}^{\prime})\nsubseteq
L({\mathcal{T}})$.

Let $\nu^{\prime}$ and $\nu$ be the valuations of the clocks in
$\rho^{\prime}$ and $\rho$ respectively, after the transition corresponding to
the timed letter $(a,t_{l})$ in the word $w$ is taken. Let Eve’s token be at
the state $(S,1)$ at this point, and $p$ be the maximum number of clocks in
$S$ such that all of them have distinct valuations in $\nu$ of the form
$t_{l}-t_{\alpha_{i}}$ for some $i$. Without loss of generality, suppose that
the valuations of these $p$ clocks are
$t_{l}-t_{\alpha_{1}},t_{l}-t_{\alpha_{2}},\cdots,t_{l}-t_{\alpha_{p}}$,
respectively. Note that the run $\rho$ on the suffix
$(b,t)(a,t^{\prime}_{1})(a,t^{\prime}_{2})\cdots(a,t^{\prime}_{m})$ is
uniquely determined in ${\mathcal{T}}$ from the state $(S,1)$ with valuation
$\nu$ and, by assumption, is rejecting. Hence, $p$ is strictly less than $k$.
Let $(a,t^{\prime}_{\beta})=(a,t_{\alpha_{i}}+1)$ for $\beta\in[m]$ be the
first occurrence of the timed letter $(a,t_{\alpha_{i}}+1)$ in the word $w$,
for an $i\in[n]\setminus[p]$. We claim that

######  Claim 1.

Each of the clocks in the valuation $\nu^{\prime\prime}$ after the delay step
of the transition on $(a,t^{\prime}_{\beta})$ in $\rho^{\prime}$ is non-
integral.

######  Proof D.3 (Proof of the claim).

For each clock $c$, let $(a,t_{c})$ be the last timed letter at which the
clock $c$ was reset in the run $\rho$. It follows that the clock $c$ was not
reset in $\rho^{\prime}$ after $(a,t_{c})$ while the run $\rho$ was in the
first component, i.e., at least until the timed letter $(b,t)$ is seen. If the
clock $c$ was reset in $\rho^{\prime}$ after $(b,t)$, then
$\nu^{\prime\prime}(c)\leq t_{\alpha_{i}}+1-t<1$. As $(a,t^{\prime}_{\beta})$
is the first occurrence of a timed letter of the form $(\sigma,t_{c})$, we
know that $\nu^{\prime\prime}(c)>0$. Thus $\nu^{\prime\prime}(c)$ is not an
integer.

Hence, suppose that $(a,t_{c})$ was the last timed letter at which the clock
$c$ was reset in $\rho^{\prime}$, before $(a,t^{\prime}_{\beta})$. Then
$\nu^{\prime\prime}(c)=t_{\alpha_{i}}+1-t_{c}$. If $\nu^{\prime\prime}(c)$ is
an integer, then $t_{\alpha_{i}}-t_{c}$ is also an integer. As $\sigma$ resets
a clock in $\rho$ in the first component whenever the valuation of the clock
is $1$, we get that the clock $c$ must have been last reset at a timed letter
of the form $(a,t_{\alpha_{i}})$ in the run $\rho$. Thus,
$\nu(c)=t_{l}-t_{\alpha_{i}}$, which is a contradiction to the fact that none
of the clock valuations in $\nu$ equals $t_{l}-t_{\alpha_{i}}$.

Since each clock has a non-integral valuation in the delay step on the first