Reichman University, Herzliya, Israel CNRS, Marseille-Aix Université,
Université de Toulon, LIS, Marseille, FranceUdi Boker and Karoliina
Lehtinen[300]Theory of computation Logic and verification

###### Acknowledgements.

We thank Jan Otop for discussing Borel definability in quantitative
automata.Mikołaj Bojańczyk and Chandra Chekuri 2 41st IARCS Annual Conference
on Foundations of Software Technology and Theoretical Computer Science (FSTTCS
2021) FSTTCS 2021 FSTTCS 2021 December 15–17, 2021 Virtual Conference 213 35

# History Determinism vs. Good for Gameness
in Quantitative Automata

Udi Boker  Karoliina Lehtinen

###### Abstract

Automata models between determinism and nondeterminism/alternations can retain
some of the algorithmic properties of deterministic automata while enjoying
some of the expressiveness and succinctness of nondeterminism. We study three
closely related such models – history determinism, good for gameness and
determinisability by pruning – on quantitative automata.

While in the Boolean setting, history determinism and good for gameness
coincide, we show that this is no longer the case in the quantitative setting:
good for gameness is broader than history determinism, and coincides with a
relaxed version of it, defined with respect to thresholds. We further identify
criteria in which history determinism, which is generally broader than
determinisability by pruning, coincides with it, which we then apply to
typical quantitative automata types.

As a key application of good for games and history deterministic automata is
synthesis, we clarify the relationship between the two notions and various
quantitative synthesis problems. We show that good-for-games automata are
central for “global” (classical) synthesis, while “local” (good-enough)
synthesis reduces to deciding whether a nondeterministic automaton is history
deterministic.

###### keywords:

Good for games, history determinism, alternation, quantitative automata

###### category:

##  1 Introduction

Boolean automata recognise languages of finite or infinite words, often used
in verification to describe system behaviours. In contrast, quantitative
automata define functions from words to values, and can describe system
properties such as energy usage, battery-life or costs. Like Boolean automata,
quantitative automata can have nondeterministic choices (disjunctions) and
universal choices (conjunctions), which make them more powerful than
deterministic models. Alternating automata combine both nondeterministic and
universal choices.

However, not all nondeterminism is born equal. Generally, nondeterminism
increases the expressiveness and succinctness of an automata model, but at the
cost of also increasing the complexity of algorithmic problems on it,
sometimes even rendering them undecidable. However, restricted forms of
nondeterministic and even alternating automata can enjoy some of the good
algorithmic properties of deterministic automata while also gaining in
expressiveness and succinctness.

We focus on three closely related restrictions on nondeterminism and
alternations, relevant to the synthesis problem. History determinism [11]
postulates that the choices in the automaton – whether they be
nondeterministic or universal – should not depend on the future of the input
word. That is, one should be able to construct runs letter by letter while
reading the input word, so that the resulting run is as good as one
constructed with the knowledge of the full word. The notion of good for games
automata comes from solving two-player games without determinisation [14]. It
postulates that the composition of such an automaton ${\cal A}$ with games
whose payoff function is described by ${\cal A}$ should be an equivalent game
– that is, one with the same winner in the Boolean setting, or the same value
in the quantitative setting. Finally, an automaton is determinisable by
pruning if it embeds an equivalent deterministic automaton and, at least in
the nondeterministic case, this notion can be seen as a (stronger) “semi-
syntactic” version of history determinism.

The three notions are well studied in the Boolean setting. There, history
determinism and good for gameness coincide, and are broader than
determinisability by pruning in general, but coincide with it for some
automata types [8].

We generalize these notions to the quantitative setting and study the
relations between them. Some versions of these notions already appear in the
literature with respect to quantitative automata, as we elaborate on in the
related-work paragraph, however not in a systematic and consistent way, and
without analysis of the relations between them.

We start with general results concerning arbitrary quantitative automata and
then provide a more specific analysis of the following most common types of
quantitative automata:
${\mathsf{Sum}},{\mathsf{Avg}},{\mathsf{Inf}},{\mathsf{Sup}}$, discounted sum
(${\mathsf{DSum}})$,
${\mathsf{LimInf}},{\mathsf{LimSup}},{\mathsf{LimInfAvg}}$ and
${\mathsf{LimSupAvg}}$.

Surprisingly, it turns out that good for gameness and history determinism no
longer coincide in the quantitative setting. The surprise comes from the fact
that the two names are used interchangeably in the Boolean setting and are
already starting to mix in the quantitative setting. (In the Boolean setting,
even the seminal paper of Henzinger and Piterman [14], which named the “good
for games” notion, defined history deterministic automata and showed that they
are indeed good for games, while the other direction was only shown later [8].
In the quantitative setting, [15, 16, 17] speak of good for games quantitative
automata, although their definition is closer to history determinism.)

We first observe that in the quantitative setting, the three notions need sub-
notions, relating to whether one considers automata/games equivalence with
respect to values or thresholds. (See Section 3 for the exact definitions.)

We then show that while good for gameness coincides with threshold good for
gameness, history determinism is stricter than threshold history determinism,
and only the latter, under some assumptions, is equivalent to good for
gameness. (See Figure 2 for a detailed scheme of the relations.) The
assumption for the equivalence of threshold history determinism and good for
gameness is that the “letter game” played on the quantitative automaton (which
defines whether or not it is history deterministic) is determined. We show
that this is guaranteed for quantitative automata whose threshold versions
define Borel sets.

Determinizability by pruning, which has an appealing structural definition, is
generally stricter than history determinism for nondeterministic automata,
already in the Boolean setting, while equivalent to it for some automata
types. We observe that the two notions are incomparable for alternating
automata, already in the Boolean setting (see Figure 5). We then analyse
general properties of value functions that guarantee the equivalence of
determinizability by pruning and history determinism for all nondeterministic
quantitative automata whose value function has these properties. We apply
these results to specific automata types. Specifically, we show the
equivalence for ${\mathsf{Sum}},{\mathsf{Avg}},{\mathsf{Inf}}$ and
${\mathsf{Sup}}$ automata on finite words and ${\mathsf{DSum}}$ automata on
finite and infinite words.

Finally, we discuss how the different notions are relevant for different
quantitative synthesis problems. In quantitative synthesis [9, 2], the
specification is a function $f$ that maps sequences of input-output pairs onto
values. The goal of the system is to respond to input letters by producing
output letters while maximising the value of the resulting input-output
sequence. Given a function $f$, one can ask several questions: (i) what is the
best value a system can guarantee over all inputs [4]? (ii) can it guarantee
at least a threshold value? (iii) can it guarantee for each input sequence $I$
the best value that an input-output sequence including $I$ has [12]? (iv) can
it achieve a threshold value $t$ for all inputs that appear in an input-output
sequence with value at least $t$? In a nutshell, we show that on one hand,
(threshold) good for games alternating quantitative automata can be used to
solve (i) and (ii) via a product construction similar to the one used for
deterministic automata [4]; and on the other hand, (iii) and (iv) for
(threshold) history deterministic nondeterministic automata are linearly
inter-reducible with deciding the (threshold) history-determinism of an
automaton.

##### Related work.

Thomas Colcombet’s original definition of history determinism [11] also
considered non-Boolean automata, namely cost automata. While the restriction
of his definition to $\omega$-regular automata coincides with the original
definition in [14] of good for games automata [8], in the quantitative setting
his definition is different from what we provide here. His notion can be
viewed as ‘approximated history-deterministic with respect to a threshold’ as
it asks for an approximation ratio that describes the difference between the
value achieved by a strategy without the knowledge of the full input word and
the actual value of the word. Another notion of approximative history
determinism appears in [15, 16, 17] under the name of $r$-GFGness, where $r$
is a bound on the difference of the two values. Zero-regret determinizability
[3, 16] on the other hand lies somewhere between approximative
determinizability by pruning and approximative history determinism. It
requires an automaton to be approximatively equivalent to a deterministic
automaton obtained by taking the product of the input automaton with a finite
memory, with both the size of the memory and permitted regret as parameters.
When both are set to zero, we have determinizability by pruning.

Observe that we use the term “quantitative automata” rather than “weighted
automata”. The latter usually relates to the algebraic definition, whereby the
value of a nondeterministic automaton on a word is the semiring sum (or
valuation-monoid sum) of its accepting runs’ values. It is generally not
defined for alternating automata. The former defines the value of a
nondeterministic or alternating automaton on a word to be the supremum/infimum
of its runs’ values, having the ‘choice’ and ‘obligation’ interpretation of
nondeterminism and universality, respectively. (See [5] for a discussion on
the differences between the two.) Since history determinism naturally relates
to ‘choice’ and ‘obligation’ in nondeterministic and alternating automata,
quantitative automata better fit the present work.

Due to space constraints, some of the proofs appear in the appendix.

##  2 Preliminaries

##### Words.

An _alphabet_ $\Sigma$ is a finite nonempty set of letters. A finite (resp.
infinite) _word_ $u=u_{0}\ldots u_{k}\in\Sigma^{*}$ (resp.
$w=w_{0}w_{1}\ldots\in\Sigma^{\omega}$) is a finite (resp. infinite) sequence
of letters from $\Sigma$. We write $\Sigma^{\infty}$ for
$\Sigma^{*}\cup\Sigma^{\omega}$. We use $[i..j]$ to denote a set
$\\{i,\ldots,j\\}$ of integers, $[i]$ for $[i..i]$, $[..j]$ for $[0..j]$, and
$[i..]$ for integers equal to or larger than $i$. We write $w[i..j],w[..j]$,
and $w[i..]$ for the infix $w_{i}\ldots w_{j}$, prefix $w_{0}\ldots w_{j}$,
and suffix $w_{i}\ldots$ of $w$. A _language_ is a set of words, and the empty
word is written $\varepsilon$.

##### Games.

We consider turn-based zero-sum games between Adam and Eve, with
$\Sigma$-labelled transitions. A play generates a word, and each word has a
value, given by the game’s payoff function. Eve tries to maximise the value of
the play, while Adam tries to minimise it. Formally, for a payoff function
$f$, an _$f$ game_ is defined on an _arena_
$(V,E,V_{E},V_{A},L:E\rightarrow\Sigma\cup\\{\varepsilon\\})$, which consists
of a (potentially infinite) set of positions $V$, partitioned into Eve’s
positions $V_{E}$ and Adam’s positions $V_{A}$, and a set of edges $E\subseteq
V\times V$, labelled by $L$ with letters from $\Sigma\cup\\{\varepsilon\\}$.
In infinite-duration games every position has at least one outgoing edge. A
play is a maximal path over $V$; its non-$\varepsilon$ labels induce a word
$w\in\Sigma^{*}$ or $\Sigma^{\omega}$. The payoff of a play is the value of
this word, given by the payoff function $f$.

Strategies for Adam and Eve map partial plays ending in a position $v$ in
$V_{A}$ and $V_{E}$ respectively to outgoing edges from $v$. A play or partial
play $\pi$ agrees with a strategy $s_{P}$, written $\pi\in s_{P}$, for a
player $P\in\\{A,E\\}$, if whenever its prefix $p$ ends in a position in
$V_{P}$, the next edge is $s_{P}(p)$. The value $f(s_{E})$ of a strategy
$s_{E}$ for Eve is $\inf_{\pi\in s_{E}}f(\pi)$ and the value $f(s_{A})$ of a
strategy $s_{A}$ for Adam is $\sup_{\pi\in s_{A}}f(\pi)$. Let $S_{E}$ and
$S_{A}$ be the sets of strategies for Eve and Adam respectively. If
$\sup_{s\in S_{E}}f(s)$ (the best Eve can do) coincides with $\inf_{s\in
S_{A}}f(s)$ (the best Adam can do), we say that $G$ is determined and
$\sup_{s\in S_{E}}f(s)=\inf_{s\in S_{A}}f(s)$ is called the value of $G$. Eve
wins the $t$-threshold game on $G$, for some $t\in\mathbb{R}$, if the value of
$G$ is at least $t$; else Adam wins. Eve wins the strict $t$-threshold game on
$G$ if the value of $G$ is greater than $t$. Two games are equivalent in this
context if they have the same value. We restrict the scope of this article to
determined games.

##### Quantitative Automata.

An _alternating quantitative automaton_ on words is a tuple ${\cal
A}=(\Sigma,Q,\iota,\delta)$, where: $\Sigma$ is an alphabet; $Q$ is a finite
nonempty set of states; $\iota\in Q$ is an initial state; and $\delta\colon
Q\times\Sigma\to{\mathsf{B}}^{+}(\mathbb{Q}\times Q)$ is a transition
function, where ${\mathsf{B}}^{+}(\mathbb{Q}\times Q)$ is the set of positive
Boolean formulas (_transition conditions_) over weight-state pairs.

A _transition_ is a tuple $(q,a,x,q^{\prime})\in
Q{\times}\Sigma{\times}\mathbb{Q}\times Q$, sometimes also written
$q\xrightarrow[]{a:x}q^{\prime}$. (Note that there might be several
transitions with different weights over the same letter between the same pair
of states111This extra flexibility of allowing for “parallel” transitions with
different weights is often omitted (e.g., in [10]) since it is redundant for
some value functions while important for others..) We write $\gamma(t)=x$ for
the weight of a transition $t=(q,a,x,q^{\prime})$.

An automaton ${\cal A}$ is nondeterministic (resp. universal) if all its
transition conditions are disjunctions (resp. conjunctions), and it is
deterministic if all its transition conditions are just weight-state pairs. We
represent the transition function of nondeterministic and universal automata
as $\delta\colon Q\times\Sigma\to 2^{(\mathbb{Q}\times Q)}$, and of a
deterministic automaton as $\delta\colon Q\times\Sigma\to\mathbb{Q}\times Q$.

We require that the automaton ${\cal A}$ is total, namely that for every state
$q\in Q$ and letter $a\in\Sigma$, there is at least one state $q^{\prime}$ and
a transition $q\xrightarrow[]{a:x}q^{\prime}$. For a state $q\in Q$, we denote
by ${\cal A}^{q}$ the automaton that is derived from ${\cal A}$ by setting its
initial state $\iota$ to $q$.

A run of the automaton on a word $w$ is intuitively a play between Adam and
Eve. It starts in the initial state $\iota$, and in each round, when the
automaton is in state $q$ and the next letter of $w$ is $a$, Eve resolves the
nondeterminism (disjunctions) of the transition condition $\delta(q,a)$ and
Adam resolves its universality (conjunctions), yielding a transition
$q\xrightarrow[]{a:x}q^{\prime}$. The output of a play is thus a sequence
$\pi=t_{0}t_{1}t_{2}\ldots$ of transitions. As each transition $t_{i}$ carries
a weight $\gamma(t_{i})\in\mathbb{Q}$, the sequence $\pi$ provides a weight
sequence $\gamma(\pi)=\gamma(t_{0})\gamma(t_{1})\gamma(t_{2})\ldots$. More
formally, given the automaton ${\cal A}=(\Sigma,Q,\iota,\delta)$ and a word
$w\in\Sigma^{*}$ (resp. $w\in\Sigma^{\omega}$), we define the arena $G({\cal
A},w)$ with positions
$Q\times\Sigma^{*}\times{\mathsf{B}}^{+}(\mathbb{Q}\times Q)$ (resp.
$Q\times\Sigma^{\omega}\times{\mathsf{B}}^{+}(\mathbb{Q}\times Q)$), the
initial position $(\iota,w,\delta(\iota,w[0]))$, $\varepsilon$-labelled edges
from $(q,u,b)$ to $(q,u,b^{\prime})$ when $b^{\prime}$ is an immediate
subformula of $b$, and $x$-labelled edges from $(q,u,(x,q^{\prime}))$ to
$(q^{\prime},u[1..],\delta(q^{\prime},u[1]))$. Conjunctive positions belong to
Adam while disjunctive ones belong to Eve.

A ${\mathsf{Val}}$ automaton (for example a ${\mathsf{Sum}}$ automaton) is one
equipped with a _value function_ ${\mathsf{Val}}:\mathbb{Q}^{*}\to\mathbb{R}$
or ${\mathsf{Val}}:\mathbb{Q}^{\omega}\to\mathbb{R}$. The corresponding game
is the ${\mathsf{Val}}$ game on the arena $G({\cal A},w)$: each run $\pi$
(play in $G({\cal A},w)$) has a real value ${\mathsf{Val}}(\gamma(\pi))$,
which we abbreviate by ${\mathsf{Val}}(\pi)$. When this game is determined, we
say that the value of ${\cal A}(w)$ is the value of $G({\cal A},w)$, and if
$G({\cal A},w)$ is determined for all $w\in\Sigma^{\omega}$, we say that
${\cal A}$ realizes a function from words to real numbers. We restrict the
scope of this article to automata realizing functions.

Two automata ${\cal A}$ and ${\cal A}^{\prime}$ are _equivalent_ , denoted by
${\cal A}\equiv{\cal A}^{\prime}$, if they realize the same function. For a
threshold $t\in\mathbb{R}$ and a ${\mathsf{Val}}$ automaton ${\cal A}$, we
also speak of a corresponding Boolean $t$-threshold ${\mathsf{Val}}$ automaton
${\cal A}^{\prime}$ that accepts the words $w$ such that ${\cal A}(w)\geq t$.

Observe that when ${\cal A}$ is nondeterministic, a run of ${\cal A}$ on a
word $w$ is a sequence $\pi$ of transitions, and the value of ${\cal A}$ on
$w$ is the supremum of ${\mathsf{Val}}(\pi)$ over all these runs $\pi$.

##### Value functions.

We list here the most common value functions for quantitative automata on
finite/infinite words, defined over sequences of rational weights222There are
also value functions that are more naturally defined over sequences of tuples
of rational numbers, for example discounted-summation with multiple discount
factors [6].:

  * •

For finite sequences $v=v_{0}v_{1}\ldots v_{n-1}$:

    * –

$\displaystyle{\mathsf{Sum}}(v)=\sum_{i=0}^{n-1}v_{i}$

    * –

$\displaystyle{\mathsf{Avg}}(v)=\frac{1}{n}\sum_{i=0}^{n-1}v_{i}$

  * •

For finite and infinite sequences $v=v_{0}v_{1}\ldots$:

    * –

$\displaystyle{\mathsf{Inf}}(v)=\inf\\{v_{n}\leavevmode\nobreak\
|\leavevmode\nobreak\ n\geq 0\\}$

    * –

$\displaystyle{\mathsf{Sup}}(v)=\sup\\{v_{n}\leavevmode\nobreak\
|\leavevmode\nobreak\ n\geq 0\\}$

    * –

For a discount factor $\lambda\in\mathbb{Q}\cap(0,1)$,
$\displaystyle{\mathsf{DSum}}(v)=\sum_{i\geq 0}\lambda^{i}v_{i}$

  * •

For infinite sequences $v=v_{0}v_{1}\ldots$:

    * –

$\displaystyle{\mathsf{LimInf}}(v)=\lim_{n\to\infty}\limits\inf\\{v_{i}\leavevmode\nobreak\
|\leavevmode\nobreak\ i\geq n\\}$

    * –

$\displaystyle{\mathsf{LimSup}}(v)=\lim_{n\to\infty}\limits\sup\\{v_{i}\leavevmode\nobreak\
|\leavevmode\nobreak\ i\geq n\\}$

    * –

$\displaystyle{\mathsf{LimInfAvg}}(v)\leavevmode\nobreak\
=\,{\mathsf{LimInf}}({\mathsf{Avg}}(v_{0}),{\mathsf{Avg}}(v_{0},v_{1}),{\mathsf{Avg}}(v_{0},v_{1},v_{2}),\ldots)$

    * –

$\displaystyle{\mathsf{LimSupAvg}}(v)={\mathsf{LimSup}}({\mathsf{Avg}}(v_{0}),{\mathsf{Avg}}(v_{0},v_{1}),{\mathsf{Avg}}(v_{0},v_{1},v_{2}),\ldots)$

(${\mathsf{LimInfAvg}}$ and ${\mathsf{LimSupAvg}}$ are also called
$\underline{{\mathsf{MeanPayoff}}}$ and $\overline{{\mathsf{MeanPayoff}}}$.)

##### Products.

The synchronized product of a $\Sigma$-labelled game $G$ and an automaton
${\cal A}$ over alphabet $\Sigma$ is (like in the Boolean setting, see e.g.,
[8, Definition 1]) a game $G\times{\cal A}$ obtained by taking the product of
the positions of $G$ and the states and transition conditions of ${\cal A}$,
and their corresponding transitions. Positions with nondeterminism are of Eve
and positions with universality are of Adam. Transitions carry their weight
from the corresponding transition in ${\cal A}$. The payoff function of the
game is the value function of ${\cal A}$.

##  3 Good For Gameness, History Determinism, and Determinizability By Pruning

In the Boolean setting, “good for gameness” and “history determinism”,
stemming from different concepts, coincide both for nondeterministic and
alternating automata [8].

We generalize these definitions to quantitative automata, observing that under
this setting they need some sub-variants, relating to whether one considers
automata/games equivalence with respect to all values or some threshold333For
a threshold $t\in\mathbb{R}$, we provide the definitions with respect to a
non-strict inequality $\geq t$ . Using strict inequality $>t$ instead, yields
the same relations between the notions, as stated in Theorem 4.1.. As shown in
Section 4, the two main notions, as well as some of their variants, are
generally not equivalent in the quantitative setting.

The notion of determinizability by pruning, which has an appealing structural
definition, is generally stricter than good for gameness and history
determinism in the setting of nondeterministic automata, already in the
Boolean setting, yet we show that for some value functions it is equivalent to
history determinism. For alternating automata, we show that it is incomparable
with history determinism and good for gameness.

######  Definition 3.1 (Good for gameness).

An automaton ${\cal A}$ realizing a function $f:\Sigma^{*}\to\mathbb{R}$ or
$f:\Sigma^{\omega}\to\mathbb{R}$ is

  * •

_good for games_ if for every determined444We discuss in the conclusion
questions that arise if this restriction is lifted game $G$ with a
$\Sigma$-labelled arena and payoff function $f$, we have that $G$ and
$G\times{\cal A}$ have the same value;

  * •

_good for $t$-threshold games_, for some $t\in\mathbb{R}$, if for every
determined game $G$ with a $\Sigma$-labelled arena and payoff function $f$,
Eve wins the $t$-threshold game on $G$ if and only if she wins the
$t$-threshold game on $G\times{\cal A}$;

  * •

_good for threshold games_ if it is good for $t$-threshold games for all
$t\in\mathbb{R}$.

An automaton is history deterministic if there are strategies to resolve its
nondeterminism and universality, such that for every word, the (threshold)
value remains the same.

######  Definition 3.2 (History-determinism).

Consider an alternating ${\mathsf{Val}}$ automaton ${\cal
A}=(\Sigma,Q,\iota,\delta)$ realizing a function $f:\Sigma^{*}\to\mathbb{R}$
or $f:\Sigma^{\omega}\to\mathbb{R}$. Formally, _history determinism_ is
defined via _letter games_ , detailed below.

  * •

${\cal A}$ is _history deterministic_ if Eve and Adam win their letter games.

  * •

${\cal A}$ is _$t$ -threshold history deterministic_, for some
$t\in\mathbb{R}$, if Eve and Adam win their $t$-threshold letter games.

  * •

${\cal A}$ is _threshold history deterministic_ if it is $t$-threshold history
deterministic for all $t\in\mathbb{R}$.

Eve’s (Adam’s) letter games are the following win-lose games, in which Adam
(Eve) chooses the next letter and Eve and Adam resolve the nondeterminism and
universality, aiming to construct a run whose value is (threshold) equivalent
to the generated word’s value.

Eve’s letter game:

A configuration is a pair $(\sigma,b)$ where $b\in{\mathsf{B}}^{+}(Q)$ is a
transition condition and $\sigma\in\Sigma\cup\\{\varepsilon\\}$ is a letter.
(We abuse $\varepsilon$ to also be an empty letter.) A play begins in
$(\sigma_{0},b_{0})=(\varepsilon,\iota)$ and consists of an infinite sequence
of configurations $(\sigma_{0},b_{0})(\sigma_{1},b_{1})\ldots$. In a
configuration $(\sigma_{i},b_{i})$, the play proceeds to the next
configuration $(\sigma_{i+1},b_{i+1})$ as follows.

  * •

If $b_{i}$ is a state of $Q$, Adam picks a letter $a$ from $\Sigma$, and
$(\sigma_{i+1},b_{i+1})=(a,\delta(b_{i},a))$.

  * •

If $b_{i}$ is a conjunction $b_{i}=b^{\prime}\land b^{\prime\prime}$, Adam
chooses between $(\varepsilon,b^{\prime})$ and
$(\varepsilon,b^{\prime\prime})$.

  * •

If $b_{i}$ is a disjunction $b_{i}=b^{\prime}\lor b^{\prime\prime}$, Eve
chooses between $(\varepsilon,b^{\prime})$ and
$(\varepsilon,b^{\prime\prime})$.

In the limit, a play consists of an infinite word $w$ that is derived from the
concatenation of $\sigma_{0},\sigma_{1},\ldots$, as well as an infinite
sequence $b_{0},b_{1},\ldots$ of transition conditions, which yields an
infinite sequence $\pi=t_{0},t_{1},\ldots$ of transitions.

If ${\cal A}$ is over infinite words, Eve wins a play in the letter-game if
${\mathsf{Val}}(\pi)\geq{\cal A}(w)$. In the $t$-threshold letter game, Eve
wins if ${\cal A}(w)\geq t\implies{\mathsf{Val}}(\pi)\geq t$. For ${\cal A}$
over finite words, Eve wins if ${\mathsf{Val}}(\pi[0..i])\geq{\cal
A}(w[0..i])$ or ${\cal A}(w[0..i])\geq t\implies{\mathsf{Val}}(\pi[0..i])\geq
t$ for all $i$.

Adam’s letter game

is similar to Eve’s game, except that Eve chooses the letters instead of Adam,
and Adam wins a play in his letter game if ${\mathsf{Val}}(\pi)\leq{\cal
A}(w)$ and in his $t$-threshold letter game if ${\cal
A}(w)<t\implies{\mathsf{Val}}(\pi)<{\cal A}(w)$. (The asymmetry of $<$ and
$\leq$ is intended).

Intuitively, an automaton is determinizable by pruning if it can be
determinized to an equivalent (w.r.t. a threshold) deterministic automaton by
removing some of its states and transitions. (In an alternating automaton,
“removing transitions” means removing some disjunctive and conjunctive
choices.)

######  Definition 3.3 (Determinizability by Pruning).

A ${\mathsf{Val}}$ automaton ${\cal A}$ is

  * •

_determinizable by pruning_ if there exists a deterministic ${\mathsf{Val}}$
automaton ${\cal A}^{\prime}$ that is derived from ${\cal A}$ by pruning, such
that ${\cal A}^{\prime}\equiv{\cal A}$;

  * •

_$t$ -threshold determinizable by pruning_ if there is a deterministic
${\mathsf{Val}}$ automaton ${\cal A}^{\prime}$ that is derived from ${\cal A}$
by pruning, such that for every word $w$, we have ${\cal A}^{\prime}(w)\geq t$
iff ${\cal A}(w)\geq t$;

  * •

_threshold determinizable by pruning_ if it is $t$-threshold determinizable by
pruning $\forall t\in\mathbb{R}$.

Observe that a ${\mathsf{Val}}$-automaton can be good for games, history
deterministic, or determinizable by pruning when interpreted on infinite
words, but not when interpreted on finite words, as demonstrated in Figure 1 .

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{4}$$0$$0$$1$$2$$0$$-1$$2$$0$ Figure 1:
A nondeterministic ${\mathsf{DSum}}$-automaton with discount factor
$\frac{1}{2}$ over a unary alphabet that is determinizable by pruning, good
for games, and history deterministic with respect to infinite words, but none
of them with respect to finite words: For the single infinite word, the
initial choice of going from $q_{0}$ to $q_{1}$ provides the optimal value of
$1$, making it all of the above. On finite words, on the other hand, it is not
even threshold history deterministic (and by Theorem 4.1 neither of the rest),
since in order to guarantee a value of at least $1$, the first transition
should be different for the word of length $1$ and the word of length $2$,
going to $q_{3}$ for the former and to $q_{1}$ for the latter.

##  4 The Relations Between Notions

Having defined these notions, we now establish which inclusions hold in
general, and which are conditional on characteristics of the value function,
as summarised in Figure 2.

######  Theorem 4.1.

(Threshold) good for gameness, (threshold) history determinism, and
(threshold) determinizability by pruning of quantitative automata are related
as described in Figure 2.

Good For Gameness $=$1 Threshold Good For Gameness $\cong$2 Threshold History
Determinism$\subsetneq$4(for nondet.)$\subsetneq$3Threshold Determinizability
by PruningHistory Determinism$\neq$5Determinizability by
Pruning$\subsetneq$3$\subsetneq$4(for nondet.)1\. Always holds (Lemma 4.2).2\.
The  $\leavevmode\nobreak\ \Longleftarrow\leavevmode\nobreak\ $implication
always holds (Lemma 4.3); The  $\leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ $implication holds at least forall
${\mathsf{Val}}$ automata whose threshold letter games are determined (Lemma
4.4),e.g., for
${\mathsf{Inf}},{\mathsf{Sup}},{\mathsf{LimInf}},{\mathsf{LimSup}},{\mathsf{DSum}}$
and all functions on finite words (Theorem 4.8).3\. Strict containment for all
non-trivial value functions with at least three values (Lemma 4.10);Equal (the
same notion) for value functions with two values.4\. Strict containment, in
general, for nondeterministic automata (Propositions 4.12 and 4.13);
Equivalent notions for some nondeterministic ${\mathsf{Val}}$ automata
(Section 4.1);Incomparable for alteranting automata (Proposition 4.14).5\.
Incomparable, in general, for value functions with at least three
values(Lemmas 4.10, 4.13 and 4.14);For value functions with two values, as
relation $4$ above. Figure 2: The relations between the different notions.

Considering good for gameness, if an automaton ${\cal A}$ is good for all
games then it is obviously good for all threshold games. The implication for
the other direction stems from the fact that every concrete game $G$ has a
single value $v$. Then for $G$, it is enough to be good for $v$-threshold
games, and for all automata, it is enough to be good for all threshold games.

######  Lemma 4.2.

Good for Gameness $\leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ $Threshold Good for Gameness.

For a $t$-threshold history deterministic automaton ${\cal A}$, Eve and Adam
have strategies to win their $t$-letter games on ${\cal A}$. Thus, whenever
Eve or Adam win some $t$-threshold game $G$, they can combine their two
winning strategies to win $G\times{\cal A}$.

######  Lemma 4.3.

Threshold History Determinism $\leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ $Threshold Good for Gameness

For the other direction, we generalize proofs from [7, 8]: assuming that the
automaton ${\cal A}$ is not threshold history deterministic we construct a
threshold game $G$ with respect to which ${\cal A}$ is not good for
composition (namely, the product of $G$ with ${\cal A}$ does not have the same
winner as $G$). However, to build this game, we assume that either Adam wins
Eve’s letter game on ${\cal A}$ or Eve wins Adam’s letter game on ${\cal A}$,
that is, we assume that the letter games on ${\cal A}$ are determined. We
later show that this determinacy requirement holds for all the specific value
functions that we consider in the paper, except for ${\mathsf{LimInfAvg}}$ and
${\mathsf{LimSupAvg}}$, on which we leave the determinacy question open.

######  Lemma 4.4.

For ${\mathsf{Val}}$ automata whose threshold letter games are determined,
Threshold Good for Gameness $\leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ $Threshold History Determinism.

######  Proof 4.5.

Consider a ${\mathsf{Val}}$ automaton ${\cal A}$ whose threshold letter games
are determined. Then, if ${\cal A}$ is not threshold history deterministic, it
follows that Adam wins Eve’s $t$-letter game on ${\cal A}$ for some threshold
$t$, or Eve wins Adam’s $t$-letter game on ${\cal A}$ for some $t$. We show
below that in both cases ${\cal A}$ is not good for threshold games, proving
the contra-positive of the claim.

Assume that Adam wins Eve’s $t$-letter game $G_{{\cal A},t}$ on ${\cal A}$ for
some threshold $t$ with a strategy $s$. We can build a one-player
$\Sigma$-labelled (infinite) game $G_{s}$ in which the positions, which all
belong to Adam, are the finite words that can be constructed along plays of
$G_{{\cal A},t}$ that agree with $s$, and where for every positions $u$ and
$u\cdot a$, there is an $a$-labelled edge from the position $u$ to the
position $u\cdot a$. The empty word $\varepsilon$ is the initial position. In
other words, this is the one-player arena in which plays correspond to
(infinite) words that occur in the letter game if Adam uses the strategy $s$.
Notice that since $s$ is a winning strategy in the $t$-letter game, all words
$w$ that are plays of $G_{s}$ have ${\cal A}(w)\geq t$. The $t$-threshold game
on $G_{s}$ is therefore winning for Eve.

We now argue that Adam wins the product game $G_{s}\times{\cal A}$. Indeed,
Adam can now use the strategy $s$ to choose directions in $G_{s}$ according to
the run constructed so far in ${\cal A}$, and resolve conjunctions in ${\cal
A}$ according to the history of the word and run so far. Since $s$ is a
winning strategy for Adam in the letter game, this guarantees that the
resulting run $\rho$ is such that ${\mathsf{Val}}(\rho)<t$. Then ${\cal A}$ is
not threshold-good-for-games, as witnessed by $G_{s}$.

By a similar argument, if Eve wins Adam’s $t$-letter game for some $t$ with a
strategy $s$, then we can construct a one-player game $G_{s}$ in which all
positions belong to Eve such that $G_{s}$ is winning for Adam (i.e., all words
have value strictly smaller than $t$), but in the product $G\times{\cal A}$,
Eve wins, i.e., can force value at least $t$.

Hence if either player has a winning strategy in the other player’s threshold
letter game for some threshold, then the automaton is not good for threshold
games.

We now show that letter games on ${\mathsf{Val}}$ automata whose threshold
variants define Borel sets are determined. This stems from the fact that their
winning condition is a union between two conditions that can be defined by
threshold ${\mathsf{Val}}$ automata or their complement.

######  Proposition 4.6.

If for some value function ${\mathsf{Val}}$, all threshold ${\mathsf{Val}}$
automata define Borel sets, then threshold letter games on ${\mathsf{Val}}$
automata are determined.

######  Proof 4.7.

Consider Eve’s $t$-letter game on a ${\mathsf{Val}}$ automaton ${\cal A}$, for
some threshold $t\in\mathbb{R}$. A play of the game generates a sequence
$\rho\in(\Sigma\times V)^{\omega}$, where $\Sigma$ is ${\cal A}$’s alphabet
and $V$ is the finite set of its weights. We may view $\rho$ as a pair of
sequences $(\rho_{\Sigma},\rho_{V})$, where $\rho_{\Sigma}\in\Sigma^{\omega}$
and $\rho_{V}\in V^{\omega}$. Then the winning set of Eve is
$\\{\rho\leavevmode\nobreak\ |\leavevmode\nobreak\
{\mathsf{Val}}(\rho_{V})\geq t\text{ or }{\cal A}(\rho_{\Sigma})<t\\}$.

Observe that the set $S_{V}=\\{\rho\leavevmode\nobreak\ |\leavevmode\nobreak\
{\mathsf{Val}}(\rho_{V})\geq t\\}$ can be defined by a $t$-threshold
deterministic ${\mathsf{Val}}$ automaton ${\cal B}$, in which the weight of a
transition over the input letter $(\sigma,v)$ is $v$. Let ${\cal A}^{\prime}$
be a $t$-threshold ${\mathsf{Val}}$ automaton that is identical to ${\cal A}$,
except that its alphabet is $\Sigma\times V$, while the transitions are
sensitive, as in ${\cal A}$, only to the $\Sigma$ component of the input. Then
the set $S_{\Sigma}=\\{\rho\leavevmode\nobreak\ |\leavevmode\nobreak\ {\cal
A}(\rho_{\Sigma})\geq t\\}$ is defined by ${\cal A}^{\prime}$.

As the winning condition of Eve’s letter game is the union of $S_{V}$ and the
complement of $S_{\Sigma}$, and as both are Borel sets, so is the winning
condition. Hence, by [19] the game is determined.

The argument regarding Adam’s letter game is analogous.

A direct corollary of Proposition 4.6 is that for most of the common
quantitative automata, we have that good for gameness is equivalent to
threshold history determinism. In particular, this is the case for all the
concrete value functions that are considered in this paper, except for
${\mathsf{LimInfAvg}}$ and ${\mathsf{LimSupAvg}}$, for which we leave this
equivalence question open. (While threshold limit-average functions define
Borel sets, and therefore limit-average (mean-payoff) games are determined, we
are not aware of a result showing that _nondeterministic_ threshold limit-
average automata define Borel sets. It is easy to see that deterministic such
automata do, but not necessarily nondeterministic ones. For nondeterministic
discounted-sum automata, we prove in Theorem 4.8 that they define Borel sets
by relying on the continuity of discounted-summation, which does not hold for
limit average.)

######  Theorem 4.8.

Good For Gameness $\leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ $Threshold History Determinism for all
${\mathsf{Val}}$ automata on finite words, and
${\mathsf{Inf}},{\mathsf{Sup}},{\mathsf{LimInf}},{\mathsf{LimSup}}$ and
${\mathsf{DSum}}$ automata on infinite words.

######  Proof 4.9.

It is enough to show that threshold automata of these types define Borel sets,
and then the claim directly follows from Lemmas 4.2, 4.3 and 4.6.

Automata on finite words.

Every threshold ${\mathsf{Val}}$ automaton on finite words defines a set of
finite words, which is a countable union of singletons and thus a Borel set.

${\mathsf{Inf}}$ and ${\mathsf{Sup}}$ automata.

Observe that ${\mathsf{Inf}},{\mathsf{Sup}}$ automata on infinite words are
“almost” like automata on finite words, in the sense that the value of the
automaton on a word is equal to its value on some prefix of the word.
Formally, for a ${\mathsf{Sup}}$ automaton ${\cal A}$, we have that the set of
infinite words $\\{w\in\Sigma^{\omega}\leavevmode\nobreak\
|\leavevmode\nobreak\ {\cal A}(w)\geq t\\}$ is equal to the set of infinite
words $\\{w\in\Sigma^{\omega}\leavevmode\nobreak\ |\leavevmode\nobreak\ \text{
exists }p\in\mathbb{N}\text{ such that }{\cal A}(w[..p])\geq t\\}$ (when
considering ${\cal A}$ to operate on finite words). Observe that it is indeed
a Borel set, since it is a countable union of open sets. The argument for
${\mathsf{Inf}}$-automata is analogous, having a countable intersection of
closed sets.

${\mathsf{LimInf}}$ and ${\mathsf{LimSup}}$ automata.

Observe that threshold ${\mathsf{LimInf}}$ and ${\mathsf{LimSup}}$ automata
are equivalent to coBüchi and Büchi automata, respectively, thus defining
$\omega$-regular languages, which are known to be Borel sets [21].

${\mathsf{DSum}}$ automata.

For ${\mathsf{DSum}}$ automata the argument stems from the continuity with
respect to the Cantor topology of functions defined by ${\mathsf{DSum}}$
automata.

Consider a ${\mathsf{DSum}}$ automaton ${\cal A}$ and a threshold
$t\in\mathbb{R}$. Define the following set of infinite words
$B_{t}=\\{w\in\Sigma^{\omega}\leavevmode\nobreak\ |\leavevmode\nobreak\ \text{
for every }n\in\mathbb{N}\text{ and }p_{0}\in\mathbb{N},\text{ there exists
}p>p_{0},\text{ such that }{\cal A}(w[..p])\geq t-\frac{1}{n}\\}$ (when
considering ${\cal A}$ to operate on finite words).

Observe that $B_{t}$ is a Borel set, since $\\{w\leavevmode\nobreak\
|\leavevmode\nobreak\ {\cal A}(w[..p])\geq t-\frac{1}{n}\\}$ is an open set,
and the existential and universal quantifiers can be defined by countable
unions and intersections.

We claim that $B_{t}$ is equivalent to the set $A_{t}=\\{w\leavevmode\nobreak\
|\leavevmode\nobreak\ {\cal A}(w)\geq t\\}$, which will prove the required
statement. One direction is immediate – if a word $w$ is in $A_{t}$ then by
the definition of ${\cal A}(w)$, there are runs of ${\cal A}$ on $w$ whose
supremum is at least $t$, admitting the membership of $w$ in $B_{t}$.

As for the other direction, we show that for every $n\in\mathbb{N}$, there is
a run $r$ of ${\cal A}$ on $w$, such that ${\mathsf{Val}}(r)\geq
t-\frac{1}{n}$, proving that $w$ is in $A_{t}$. (One can then even combine
these runs to create a single run that attains a value at least $t$.) Consider
some $n\in\mathbb{N}$, and let $R$ be the infinite set of finite runs
$r_{1},r_{2},\ldots$ that witness the membership of $w$ in $B_{t}$ with
respect to $2n$. That is, $r_{i}$ is a run on a prefix of $w$ of length at
least $i$, whose value is at least $t-\frac{1}{2n}$. We create a single run
$r$ from $R$ in a “Konig’s lemma” approach (for simplicity, we detail the
construction for a nondeterministic automaton, and later explain how to extend
it to an alternating automaton):

We choose the first transition $t_{1}$ in $r$ to be a transition that appears
as the first transition in infinitely many $r_{i}$’s. We then choose the next
transition $t_{2}$ to be a transition that appears as the second transition,
where $t_{1}$ is the first transition, in infinitely many $r_{i}$’s, and so
on. Notice that $r$ is indeed a run of ${\cal A}$ and its value is at least
$t-\frac{1}{n}$: By the discounted-sum value function, if the value of a long
enough prefix is at least $t-\frac{1}{2n}$, the value of the entire run cannot
be smaller than $t-\frac{1}{n}$.

Now, for an alternating automaton, rather than “choosing transitions” we need
to “resolve the nondeterminism”, while ensuring that the choice we make
appears in infinitely many runs after the previous nondeterministic and
_universal_ choices that were already made.

History determinism and determinizability by pruning obviously imply their
threshold versions; Figure 3 demonstrates that the converse does not hold.

######  Lemma 4.10.

  * •

History Determinism $\leavevmode\nobreak\ {}^{\Longrightarrow}_{\hskip
4.26773pt/\Longleftarrow}\leavevmode\nobreak\ $Threshold History Determinism;

  * •

Determinizability by Pruning $\leavevmode\nobreak\
{}^{\Longrightarrow}_{\hskip 4.26773pt/\Longleftarrow}\leavevmode\nobreak\
$Threshold Determinizability by Pruning;

  * •

History Determinism ${\hskip 4.26773pt/\Longleftarrow}\leavevmode\nobreak\
$Threshold Determinizability by Pruning

######  Proof 4.11.

The implications are straightforward: a winning strategy for each player in
their letter game is also a winning strategy in their $t$-threshold letter
game, for every threshold $t\in\mathbb{R}$; further, if an automaton ${\cal
A}^{\prime}$ that results from pruning ${\cal A}$ is equivalent to ${\cal A}$,
then for every threshold $t$ and word $w$, if ${\cal A}(w)\geq t$ then ${\cal
A}^{\prime}(w)\geq t$.

As for the non-implications, Figure 3 provides such counter examples, which
hold, with some variations, with respect to every non-trivial value function
with at least 3 values, and in particular with respect to all value functions
discussed in the paper.

Consider, for example, the automaton ${\cal A}$ of Figure 3 with respect to
the ${\mathsf{Sup}}$ value function. It is not history deterministic, since if
the nondeterminism in $q_{0}$ is resolved by going to $q_{1}$, the resulting
automaton is not equivalent to ${\cal A}$ with respect to the finite word $aa$
and infinite word $a^{\omega}$, and if it is resolved by going to $q_{2}$, the
resulting automaton fails on $ab$ and $ab^{\omega}$.

On the other hand, ${\cal A}$ is threshold determinizable by pruning and
threshold history deterministic: For a threshold up to $1$, the nondeterminism
is resolved by going to $q_{1}$ and for the threshold $2$ by going to $q_{2}$.

${\cal
A}$$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\Sigma\\!:\\!0$$\Sigma\\!:\\!0$$\Sigma\\!:\\!1$$a\\!:\\!2,b\\!:\\!0$$\Sigma\\!:\\!0$${\cal
B}$$s_{0}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$\Sigma\\!:\\!0$$\Sigma\\!:\\!0$$\Sigma\\!:\\!1$$a\\!:\\!2$$b\\!:\\!0$$\Sigma\\!:\\!2$$\Sigma\\!:\\!0$
Figure 3: Nondeterministic automata that are threshold history deterministic
and threshold determinizable by pruning, but not history deterministic and not
determinizable by pruning. The automaton ${\cal A}$ has this property with
respect, for example, to the ${\mathsf{Sum}}/{\mathsf{DSum}}/{\mathsf{Sup}}$
value functions, and ${\cal B}$ with respect, for example, to
${\mathsf{Avg}}/{\mathsf{LimSup}}/{\mathsf{LimInf}}/{\mathsf{LimSupAvg}}/{\mathsf{LimInfAvg}}$.

#### History Determinism $\neq$ Determinizability by Pruning

For nondeterministic automata, it is clear that determinizability by pruning
implies history determinism: the pruning provides a strategy for Eve in her
letter game.

######  Proposition 4.12.

For nondeterministic automata, determinizability by pruning
$\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ $history
determinism.

The converse was shown to be false for Büchi and coBüchi automata [7],
directly implying the same for ${\mathsf{LimSup}}$ and ${\mathsf{LimInf}}$
automata. Considering ${\mathsf{LimInfAvg}}$ and ${\mathsf{LimSupAvg}}$
automata, the automaton depicted in Figure 4, which is similar to the coBüchi
automaton in [7, Figure 3], is history deterministic but not determinizable by
pruning.

$a\\!:\\!1$$a\\!:\\!1$$b\\!:\\!0$$a\\!:\\!1$$a\\!:\\!0$$b\\!:\\!1$$a\\!:\\!1$$a\\!:\\!1$$b\\!:\\!0$$a\\!:\\!1$$a\\!:\\!0$$b\\!:\\!1$
Figure 4:  (Similar to [7, Figure 3].) A history deterministic
${\mathsf{LimInfAvg}}$ or ${\mathsf{LimSupAvg}}$ automaton that is not
determinizable by pruning. (Missing transitions lead to a sink with a
$0$-weighted self loop on both $a$ and $b$.) It is history deterministic by a
strategy that chooses in the initial state to go up if and only if it went
down the previous time. Following this strategy in the letter game, Eve
returns infinitely often to the initial state only on $(aaab)^{\omega}$,
getting a value $\frac{1}{2}$, which is also the automaton’s value on it. For
every other word, the run of Eve moves to the right part of the automaton,
which is deterministic, guaranteeing Eve the optimal value on the word. On the
other hand, every pruning of it yields an automaton whose value on either
$a^{\omega}$ or $(ab)^{\omega}$ is $\frac{1}{2}$ instead of $1$.

######  Proposition 4.13.

For nondeterministic ${\mathsf{LimInf}}$, ${\mathsf{LimSup}}$,
${\mathsf{LimInfAvg}}$, and ${\mathsf{LimSupAvg}}$ automata, history
determinism ${\hskip 4.26773pt/\Longrightarrow}\leavevmode\nobreak\
$determinizability by pruning.

For alternating automata, it turns out that (threshold) history determinism
and determinizability by pruning are incomparable, as demonstrated in Figure
5.

######  Proposition 4.14.

For (Boolean and quantitative) alternating automata, determinizability by
pruning ${\hskip 4.26773pt/\Longrightarrow}\leavevmode\nobreak\ $history
determinism, good for gameness.

######  Proof 4.15.

The claim holds for Boolean automata as well as quantitative automata with
every non-trivial value function. Consider the alternating finite automaton on
finite words (which can also be viewed, for example as a ${\mathsf{Sup}}$
automaton) in Figure 5. It does not accept any word, and can be determinized
by pruning the right nondeterministic transition. However, it is not history
deterministic: Eve wins Adam’s letter game, by choosing the right
nondeterministic transition.

$q_{0}$${\lor}$${\land}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{5}$$q_{6}$$\Sigma$$\Sigma$$a$$b$$b$$a$$\Sigma$$\Sigma$$\Sigma$
Figure 5: An alternating finite automaton on finite words that is
determinizable by pruning, but not history deterministic nor good for games.

###  4.1 When (History Determinism $=$ Determinizability by Pruning)

In general for nondeterministic automata, determinizability by pruning is
strictly contained in history determinism; here we study when the two notions
coincide. In the Boolean setting, they are equivalent for nondeterministic
finite automata on finite words (NFAs) [18] as well as for nondeterministic
weak automata on infinite words [20]. Here we analyse general properties of
value functions that guarantee this equivalence, and then consider specific
value functions on finite and infinite words. The general properties that we
analyze relate to how “sensitive” the value function is to the prefix, current
position, and suffix of the weight sequence.

We begin by defining cautious555Similar transitions are sometimes called
“residual” in the literature. strategies for Eve in the letter game, that we
then use to define value functions that are “present focused”. Intuitively, a
strategy is cautious if it avoids mistakes, that is, it only builds run
prefixes that can still achieve the maximal value of any continuation of the
word so far.

######  Definition 4.16 (Cautious strategies).

Consider Eve’s letter game on a ${\mathsf{Val}}$ automaton ${\cal A}$. A move
(transition) $t=q\xrightarrow{\sigma:x}q^{\prime}$ of Eve, played after some
run $\rho$ ending in a state $q$, is _non-cautious_ if for some word $w$,
there is a run $\pi^{\prime}$ from $q$ over $\sigma w$ such that
${\mathsf{Val}}(\rho\pi^{\prime})$ is strictly greater than the value of
${\mathsf{Val}}(\rho\pi)$ for any $\pi$ starting with $t$.

A strategy is _cautious_ if it makes no non-cautious moves.

We call a value function _present focused_ if, morally, it depends on the
prefixes of the value sequence, formalized by winning the letter game via
cautious strategies.

######  Definition 4.17 (Present-focused value functions).

A value function ${\mathsf{Val}}$, on finite or infinite sequences, is
_present focused_ if for all automata ${\cal A}$ with value function
${\mathsf{Val}}$, every cautious strategy in the letter game on ${\cal A}$ is
also a winning strategy in that game.

Value functions on finite sequences are present focused, as they can only
depend on prefixes.

######  Lemma 4.18.

Every value function ${\mathsf{Val}}$ on finite sequences is present focused.

######  Proof 4.19.

Assume Eve plays a cautious strategy $s$ in some letter game on an automaton
${\cal A}$ on finite words. Towards a contradiction, assume that there is a
finite play $\pi$, in which Adam plays some word $w$ and Eve plays a run
$\rho$ over $w$ such that ${\mathsf{Val}}(\rho)<{\cal A}(w)$. Then, let
$\rho^{\prime}$ be the longest prefix of $\rho$ such that the highest value of
a run over $w$ starting with $\rho^{\prime}$ is ${\cal A}(w)$. Since $\rho$ is
not a run with value ${\cal A}(w)$, $\rho^{\prime}$ is a strict prefix of
$\rho$. However, since $\rho^{\prime}$ is the longest prefix that could be
continued into a run with value ${\cal A}(w)$, Eve’s next move after
$\rho^{\prime}$ must be non-cautious, contradicting that $s$ never plays non-
cautious moves.

######  Remark 4.20.

Value functions on infinite sequences are not necessarily present focused. For
example, consider the automaton depicted in Figure 1, but viewed as a
${\mathsf{Sup}}$ automaton on infinite words rather than a ${\mathsf{DSum}}$
automaton. Observe that Eve can forever stay in $q_{0}$, always having the
potential to continue to an optimal run with value $2$, but never fulfilling
this potential.

We now define “suffix monotonicity” of value functions, which, with present-
focus, will guarantee the equivalence of history determinism and
determinizability by pruning.

######  Definition 4.21.

A value function ${\mathsf{Val}}$ is _suffix monotonic_ if for every finite
set $S\subset\mathbb{Q}$, sequence $\alpha\in S^{*}$ and sequences
$\beta,\beta^{\prime}\in S^{\infty}$, we have
${\mathsf{Val}}(\beta)\geq{\mathsf{Val}}(\beta^{\prime})$ iff
${\mathsf{Val}}(\alpha\beta)\geq{\mathsf{Val}}(\alpha\beta^{\prime})$.

Observe that the above definition does not consider arbitrary sequences of
rational numbers, but rather sequences of finitely many different rational
numbers, which is the case in sequences of weights that are generated by runs
of quantitative automata.

Value functions that are _suffix dependent_ (namely ${\mathsf{Val}}$ functions
such that for every finite set $S\subset\mathbb{Q}$, sequences
$\alpha,\alpha^{\prime}\in S^{*}$ and sequence $\beta\in
S^{\infty}\setminus\\{\varepsilon\\}$, we have
${\mathsf{Val}}(\alpha\beta)={\mathsf{Val}}(\alpha^{\prime}\beta)$) are
obviously suffix monotonic. Examples for such value functions are the
acceptance condition of NFAs (i.e, a “last” value function, that depends only
on the last weight of $0$ for rejection and $1$ for acceptance), all
$\omega$-regular conditions (which depend on the states/transitions that are
visited infinitely often), ${\mathsf{LimInf}}$, ${\mathsf{LimSup}}$,
${\mathsf{LimInfAvg}}$, and ${\mathsf{LimSupAvg}}$. Examples for value
functions that are suffix monotonic but not suffix dependent are
${\mathsf{Sum}},{\mathsf{Avg}}$ and ${\mathsf{DSum}}$, and examples for value
functions that are not suffix monotonic are ${\mathsf{Inf}}$ and
${\mathsf{Sup}}$.

We next show that suffix monotonicity together with present-focus guarantee
the equivalence of history determinism and determinizability by pruning. The
idea is that under these conditions, every cautious strategy in the letter
game can be arbitrarily pruned into a positional strategy (with respect to the
automaton states).

######  Theorem 4.22.

For nondeterministic ${\mathsf{Val}}$ automata, where ${\mathsf{Val}}$ is a
present-focused and suffix-monotonic value function, we have that history
determinism $\leavevmode\nobreak\ \Longleftrightarrow\leavevmode\nobreak\
$determinizability by pruning.

######  Proof 4.23.

We show that Eve wins her letter game on ${\cal A}$ with a positional
strategy, which implies that ${\cal A}$ is determinizable by pruning.

Let $s$ be a cautious strategy for Eve in the letter game on ${\cal A}$. Let
$\hat{s}$ be an arbitrary positional strategy that only uses transitions also
used by $s$. We argue that $\hat{s}$ is also cautious. Indeed, if $\hat{s}$
chooses $\tau=q\xrightarrow{\sigma:x}q^{\prime}$ after a play
$(\hat{w},\hat{\rho})$ of the letter game, there is some play $(w,\rho)$ from
which $s$ plays $\tau$. Since $s$ is cautious, for every word $v$ and every
run $\pi^{\prime}$ from $q$ over $\sigma v$, there is a run $\pi$ from $q$
starting with $\tau$ such that
${\mathsf{Val}}(\rho\pi)\geq{\mathsf{Val}}(\rho\pi^{\prime})$. Thus, by suffix
monotonicity, we have ${\mathsf{Val}}(\pi)\geq{\mathsf{Val}}(\pi^{\prime})$,
and then again by the other direction of suffix monotonicity, we get that
${\mathsf{Val}}(\hat{\rho}\pi)\geq{\mathsf{Val}}(\hat{\rho}\pi^{\prime})$,
implying that $\hat{s}$ choosing $\tau$ is a cautious move.

Then ${\cal A}$ is determinisable by pruning: the subautomaton ${\cal
A}_{\hat{s}}$ that only has transitions used by $\hat{s}$ is equivalent to
${\cal A}$. Indeed, for every word $w$, ${\cal A}_{\hat{s}}(w)$ is
${\mathsf{Val}}(\rho_{w})$, where $\rho_{w}$ is the unique run of ${\cal
A}_{\hat{s}}$ over $w$. The run $\rho_{w}$ is also the run built by $\hat{s}$
in the letter game over $w$. Since $\hat{s}$ is cautious and ${\mathsf{Val}}$
is present focused, we have that $\hat{s}$ is a history-deterministic
strategy, which guarantees that ${\mathsf{Val}}(\rho_{w})={\cal A}(w)$, giving
us the equivalence of ${\cal A}$ and ${\cal A}_{\hat{s}}$.

######  Remark 4.24.

Both present-focus and suffix-monotonicity are necessary in Theorem 4.22. For
example ${\mathsf{LimInf}}$ is suffix monotonic, but ${\mathsf{LimInf}}$
automata are not determinizable by pruning. On the other hand, Figure 6
demonstrates a present-focused value function whose history deterministic
automata on finite words are not determinizable by pruning.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$a\\!:\\!0$$b\\!:\\!1$$\Sigma\\!:\\!0$$\Sigma\\!:\\!1$$\Sigma\\!:\\!0$$\Sigma\\!:\\!1$
Figure 6: A nondeterministic ${\mathsf{Val}}$ automaton ${\cal A}$ on finite
words with the value function ${\mathsf{Val}}(\rho)=1$ if $\rho$ has both even
and odd values, and $0$ otherwise. Notice that ${\mathsf{Val}}$ is present
focused and ${\cal A}$ is history deterministic but not determinizable by
pruning.

We now apply these results to specific value functions.

######  Theorem 4.25.

666A slightly weaker result is given in [3, Theorem 5.1]: a ${\mathsf{Sum}}$
automaton is history deterministic _with a finite-memory strategy for
resolving the nondeterminism_ if and only if it is determinizable by pruning.

For nondeterministic ${\mathsf{Sum}}$ and ${\mathsf{Avg}}$ automata (on finite
words), history determinism $\leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ $determinizability by pruning.

######  Proof 4.26.

From Lemmas 4.18 and 4.22 and the suffix monotonicity of these value
functions.

We continue with showing that ${\mathsf{DSum}}$ is present focused due to the
function’s continuity.

######  Lemma 4.27.

${\mathsf{DSum}}$ on infinite sequences is a present-focused value function.

######  Theorem 4.28 ([16, Section 5]).

For nondeterministic ${\mathsf{DSum}}$ automata on finite and infinite words,
history determinism $\leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ $determinizability by pruning.

######  Proof 4.29.

The claim, which was also proved in [16, Section 5], is a direct consequence
of Lemmas 4.18, 4.27 and 4.22 and the suffix monotonicity of the
${\mathsf{DSum}}$ value functions.

The ${\mathsf{Inf}}$ and ${\mathsf{Sup}}$ value function are not suffix
monotonic, and indeed the proof of Theorem 4.22 does not hold for them – not
every cautious transition of a history deterministic ${\mathsf{Sup}}$
automaton on finite words can be used for pruning it into a deterministic
automaton. Yet, also for ${\mathsf{Inf}}$ and ${\mathsf{Sup}}$ automata on
finite words we have that history determinism is equivalent to
determinizability by pruning, using other characteristics of these value
functions – we can prune the automaton, by choosing the transitions that are
used by the strategy of the letter game after reading words with minimal
values for ${\mathsf{Sup}}$ and maximal value for ${\mathsf{Inf}}$.

######  Theorem 4.30.

For nondeterministic ${\mathsf{Inf}}$ and ${\mathsf{Sup}}$ automata on finite
words, history determinism $\leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ $ determinizability by pruning.

##  5 Applications to Quantitative Synthesis

Establishing the non-equivalence of history determinism, good for gameness and
their threshold versions leaves us with the question of which definitions, if
any, are the most useful or interesting ones. We explore this question from
the perspective of quantitative synthesis.

In the Boolean setting, Church’s classical synthesis problem asks for a
transducer ${\cal T}$ that produces, letter by letter, for every input
sequence $I\in\Sigma_{I}^{\omega}$ an output sequence ${\cal
T}(I)\in\Sigma_{O}^{\omega}$ such that $I\otimes{\cal T}(I)\in L$ for some
specification language $L\in(\Sigma_{I}\otimes\Sigma_{O})^{\omega}$. This
synthesis requirement is _global_ , in the sense that the output of all input
sequences should satisfy the same constraint. A _local_ variant of the
problem, termed “good enough synthesis” in [1], considers each input sequence
$I$ separately, requiring that the output ${\cal T}(I)$ of the transducer on
the input $I$ satisfies $I\otimes{\cal T}(I)\in L$ only if $I\otimes O\in L$
for some sequence $O\in\Sigma_{O}^{\omega}$.

In quantitative synthesis, the specification is a function
$f:(\Sigma_{I}\times\Sigma_{O})^{\omega}\rightarrow\mathbb{R}$ (generalizing
languages
$L:(\Sigma_{I}\times\Sigma_{O})^{\omega}\rightarrow\\{\mathtt{true},\mathtt{false}\\}$
), and the two synthesis problems above naturally generalize into two
quantitative variants each – requiring either the best possible value or a
value matching a given threshold. We thus have four variants of quantitative
synthesis: Global/Local Threshold/Best-value synthesis. It turns out that good
for gameness is closely related to global synthesis, while history determinism
is closely related to local synthesis, both for the threshold and best-value
settings.

##### Global Threshold and Best-value Synthesis.

The global threshold variant is the closest to Church synthesis: given a
function $f$ and a threshold $t\in\mathbb{R}$, it requires that
$f(I\otimes{\cal T}(I))\geq t$ for all input sequences $I$. In the best-value
version, $t$ is not given and we are interested in what is the highest
threshold that the system can guarantee.

Analogously to the Boolean setting, a $t$-threshold good for games
${\mathsf{Val}}$ automaton ${\cal A}$ realizing $f$ can be used instead of a
deterministic automaton to solve the global threshold synthesis problem:
${\cal A}$ is turned into a $t$-threshold ${\mathsf{Val}}$ game $G_{\cal A}$,
in which Adam controls the input letters and Eve controls the output letters.
Then, the synthesis problem is realizable if and only if Eve has a winning
strategy in $G_{\cal A}$. If ${\cal A}$ is nondeterministic, Eve’s winning
strategy in $G_{\cal A}$ induces a transducer for the synthesis problem. In
the best-value case, the same is true, but ${\cal A}$ must be good for games,
rather than just for $t$-threshold games, and it is Eve’s optimal strategy, if
it exists, that induces the solution transducer.

##### Local Best-value and Threshold Synthesis.

We define $\mathtt{Best}_{f}(I)=\sup_{O\in\Sigma_{O}^{\omega}}f(I\otimes O)$
for $I\in\Sigma_{I}^{\omega}$, i.e., the best value that the input $I$ can
get, or converge to, according to $f$. The local best value synthesis problem
requires that for every $I\in\Sigma_{I}^{\omega}$, we have $f(I\otimes{\cal
T}(I))=\mathtt{Best}_{f}(I)$. Since $\mathtt{Best}_{f}(I)$ is a supremum, it
need not be attained by any word; then the synthesis problem is unrealisable,
even if the system could force a value arbitrarily close to
$\mathtt{Best}_{f}(I)$. The threshold variant requires that for every
$I\in\Sigma_{I}^{\omega}$, such that $\mathtt{Best}_{f}(I)\geq t$, we have
$f(I\otimes{\cal T}(I))\geq t$, for a given threshold $t\in\mathbb{R}$.

The local best value (or $t$-threshold) synthesis problem of a function given
by deterministic (or even history-deterministic nondeterministic) automata and
the problem of whether a nondeterministic automaton is ($t$-threshold) history
deterministic reduce to each other. The relationship between good-enough
synthesis [1] and history determinism was noted for visibly pushdown automata
in [13]; a similar reduction in [12] reduces the approximative local best-
value synthesis of deterministic quantitative automata over finite words by
finite transducers to the notion of $r$-regret determinisability, that is,
whether a nondeterministic automaton is close enough to a deterministic
automaton obtained by pruning its product with a finite memory. Our reductions
are in the same spirit, but relate the synthesis problem to history
determinism rather than determinisability, and obtain a two-way correspondence
for all history-deterministic nondeterministic quantitative automata. In the
alternating case, only one direction is preserved, and only for realisability,
rather than synthesis.

######  Proposition 5.1.

Deciding the local best value (resp. $t$-threshold) synthesis problem with
respect to a function $f$ given by a ($t$-threshold) history deterministic
nondeterministic ${\mathsf{Val}}$-automaton ${\cal A}$ and deciding whether a
nondeterministic ${\mathsf{Val}}$-automaton ${\cal A}^{\prime}$ is
($t$-threshold) history deterministic are linearly inter-reducible.
Furthermore, the witness of ($t$-threshold) history determinism of ${\cal
A}^{\prime}$ is implementable by the same computational models as a solution
to the best-value ($t$-threshold) synthesis of ${\cal A}$.

##  6 Conclusions

We have painted a picture of how definitions of good for gameness and history
determinism behave in the quantitative setting, and how they relate to
quantitative synthesis. Our work opens up many directions for further work, of
which we name a few.

  * •

The reductions between local synthesis and history determinism motivate
expanding methods used to decide history determinism of $\omega$-regular
automata to quantitative ones.

  * •

So far, we have restricted our attention to determined games, but one could
also consider more general classes of games and study the effect of
composition in that setting.

  * •

One appeal of good for games and history deterministic automata is that they
can be more expressive and more succinct than deterministic ones, while their
synthesis problems retain the same complexity. The expressivity and
succinctness of quantitative good for games and history deterministic automata
is open for most value functions.

  * •

It is natural to look at approximative versions of the discussed notions (as
has been done, see the related work section); we expect our results to also
generalise in that direction.

## References

  * [1] Shaull Almagor and Orna Kupferman.  Good-enough synthesis.  In CAV, volume 12225 of Lecture Notes in Computer Science, pages 541–563. Springer, 2020.
  * [2] Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, and Yaron Velner.  Quantitative assume guarantee synthesis.  In International Conference on Computer Aided Verification, pages 353–374. Springer, 2017.
  * [3] Benjamin Aminof, Orna Kupferman, and Robby Lampert.  Reasoning about online algorithms with weighted automata.  ACM Trans. Algorithms, 6(2):28:1–28:36, 2010.
  * [4] Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, and Barbara Jobstmann.  Better quality in synthesis through quantitative objectives.  In International Conference on Computer Aided Verification, pages 140–156. Springer, 2009.
  * [5] Udi Boker.  Quantitative vs. weighted automata.  In Proc. of Reachbility Problems, 2021.
  * [6] Udi Boker and Guy Hefetz.  Discounted-sum automata with multiple discount factors.  In Proc. of CSL, volume 183 of LIPIcs, pages 12:1–12:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
  * [7] Udi Boker, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak.  Nondeterminism in the presence of a diverse or unknown future.  In Proceedings of ICALP, pages 89–100, 2013.
  * [8] Udi Boker and Karoliina Lehtinen.  Good for games automata: From nondeterminism to alternation.  In Proceedings of CONCUR, volume 140 of LIPIcs, pages 19:1–19:16, 2019.
  * [9] Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas.  Non-zero sum games for reactive synthesis.  In Language and Automata Theory and Applications, pages 3–23. Springer, 2016.
  * [10] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger.  Alternating weighted automata.  In Proceedings of FCT, pages 3–13, 2009.
  * [11] Thomas Colcombet.  The theory of stabilisation monoids and regular cost functions.  In Proceedings of ICALP, pages 139–150, 2009.
  * [12] Emmanuel Filiot, Christof Löding, and Sarah Winter.  Synthesis from weighted specifications with partial domains over finite words.  In Nitin Saxena and Sunil Simon, editors, FSTTCS, volume 182 of LIPIcs, pages 46:1–46:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [13] Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann.  A bit of nondeterminism makes pushdown automata expressive and succinct.  arXiv preprint arXiv:2105.02611 (to appear in MFCS2021), 2021.
  * [14] Thomas Henzinger and Nir Piterman.  Solving games without determinization.  In Proceedings of CSL, pages 395–410, 2006.
  * [15] Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin.  Reactive synthesis without regret.  In Luca Aceto and David de Frutos-Escrig, editors, CONCUR, volume 42 of LIPIcs, pages 114–127, 2015.
  * [16] Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin.  Minimizing regret in discounted-sum games.  In Jean-Marc Talbot and Laurent Regnier, editors, CSL, volume 62 of LIPIcs, pages 30:1–30:17, 2016.
  * [17] Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin.  Reactive synthesis without regret.  Acta Informatica, 54(1):3–39, 2017.
  * [18] Orna Kupferman, Shmuel Safra, and Moshe Y Vardi.  Relating word and tree automata.  Ann. Pure Appl. Logic, 138(1-3):126–146, 2006.  Conference version in 1996.
  * [19] Donald A. Martin.  Borel determinacy.  Annals of Mathematics, 102(2), 1975.
  * [20] Gila Morgenstern.  Expressiveness results at the bottom of the $\omega$-regular hierarchy.  M.Sc. Thesis, The Hebrew University, 2003.
  * [21] Wolfgang Thomas.  Languages, automata, and logic.  In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 389–455. Springer, 1997.

Appendix

##  Appendix A Proofs of Section 4

######  Proof A.1 (Proof of Lemma 4.2).

One direction is immediate: if an automaton ${\cal A}$ is good for all games
then it is also good for all threshold games. Indeed, assuming that ${\cal A}$
is good for games, if the value of a game $G$ is $v$, then the value of the
product game $G\times{\cal A}$ is also $v$. Then, for all thresholds $t$, Eve
wins the $t$-threshold game on both $G$ and $G\times{\cal A}$ if and only if
$v\geq t$.

As for the other direction, assume ${\cal A}$ is good for threshold games. Let
$G$ be a game with value $v$. Since ${\cal A}$ composes with threshold games,
considering the $v$-threshold game on $G$, we know that Eve can achieve at
least $v$ in the product $v$-threshold game $G\times A$. Conversely, let
$v^{\prime}\geq v$ be the value of $G\times A$. Since Eve wins the
$v^{\prime}$-threshold game on $G\times A$, and ${\cal A}$ is good for
threshold games, Eve can also achieve at least $v^{\prime}$ in $G$, i.e.,
$v^{\prime}=v$, the value of $G$.

######  Proof A.2 (Proof of Lemma 4.3).

Consider a threshold history deterministic automaton ${\cal A}$ over an
alphabet $\Sigma$, realizing a function $f$. Then for every threshold
$t\in\mathbb{R}$, Eve has a winning strategy $s^{\prime}$ in the $t$-threshold
letter game on ${\cal A}$.

Now, consider a $\Sigma$-labelled $t$-threshold game $G$ with payoff function
$f$, in which Eve has a winning strategy $s$. Then in the product game
$G\times{\cal A}$, Eve can combine $s$ and $s^{\prime}$ into a strategy
$\hat{s}$, so that $s$ guarantees that any play $\pi=(w,\rho)$ that agrees
with $\hat{s}$ reads a word $w$ such that ${\cal A}(w)\geq t$, and
$s^{\prime}$ guarantees that ${\mathsf{Val}}(\rho)\geq t$ (since ${\cal
A}(w)\geq t$).

By a similar argument, if Adam has a winning strategy in his threshold letter
game, he can combine it with his winning strategy in a threshold game for
getting a winning strategy in the product threshold game.

###  A.1 Proofs of Section 4.1

######  Proof A.3 (Proof of Lemma 4.27).

Consider a $\lambda$-DSum ${\mathsf{Val}}$ automaton ${\cal A}$ and let $m$ be
the maximal absolute transition weight in ${\cal A}$. Observe that for every
word $w$ and state $q$ of ${\cal A}$, we have $|{\cal
A}^{q}(w)|\leq\frac{m}{1-\lambda}$.

Let $s$ be a cautious strategy of Eve in the letter game on ${\cal A}$. By the
definition of a cautious strategy, for every finite word $u$, playing
according to $s$ on $u$ generates a finite run $\rho$ that ends in some state
$q$, such that for every infinite word $v$, there is an infinite run $\pi$ on
$v$ from $q$, such that ${\mathsf{Val}}(\rho\pi)={\cal A}(uv)$.

Now, consider a word $w$, let $r$ be the run of ${\cal A}$ on $w$ that is
generated by following $s$, and let $r^{\prime}$ be an optimal run of ${\cal
A}$ on $w$. For every position $i$, let $q_{i}$ be the state that $r[0..i]$
ends in and $q^{\prime}_{i}$ be the state that $r^{\prime}[0..i]$ ends in. By
the cautiousness of $s$, for every position $i$, there is a run $\pi$ from
$q_{i}$ on $w[i+1..]$, such that for every run $\pi^{\prime}$ from
$q^{\prime}_{i}$ on $w[i+1..]$, we have
${\mathsf{Val}}(r[0..i])+\lambda^{i}{\mathsf{Val}}(\pi)\geq{\mathsf{Val}}(r^{\prime}[0..i])+\lambda^{i}{\mathsf{Val}}(\pi^{\prime})$.

Since ${\mathsf{Val}}(\pi)\leq\frac{m}{1-\lambda}$ and
${\mathsf{Val}}(\pi^{\prime})\geq-\frac{m}{1-\lambda}$, we get that
${\mathsf{Val}}(r^{\prime}[0..i])-{\mathsf{Val}}(r[0..i])\leq\frac{2m\cdot\lambda^{i}}{1-\lambda}$.
Since $\lim_{i\to\infty}\frac{2m\cdot\lambda^{i}}{1-\lambda}=0$, we get that
${\mathsf{Val}}(r)={\mathsf{Val}}(r^{\prime})$, implying that Eve wins the
letter game.

######  Proof A.4 (Proof of Theorem 4.30).

We provide the proof for ${\mathsf{Sup}}$ automata and then describe the
required changes for adapting it to ${\mathsf{Inf}}$ automata.

Consider a history deterministic ${\mathsf{Sup}}$ automaton ${\cal A}$ on
finite words in $\Sigma^{*}$, whose history determinism is witnessed by a
strategy $s$. We derive from $s$ a positional strategy $s^{\prime}$, by taking
for every state $q$ of ${\cal A}$ and letter $\sigma\in\Sigma$, the transition
that $s$ chooses over a minimal prefix, where minimality is with respect to
the ${\mathsf{Sup}}$ function.

Formally, for every state $q$, let $m(q)$ be a ${\mathsf{Sup}}$-minimal run
that reaches $q$ along $s$; namely $m(q)=\rho$, such that $\rho$ is a run of
${\cal A}$ that agrees with $s$ and ends in $q$, and such that for every run
$\rho^{\prime}$ of ${\cal A}$ that agrees with $s$ and ends in $q$, we have
${\mathsf{Sup}}(\rho)\leq{\mathsf{Sup}}(\rho^{\prime})$. (Notice that since
there are finitely many weights in ${\cal A}$, such a minimal run, which need
not be unique, always exists.) For every state $q$ of ${\cal A}$ and letter
$\sigma\in\Sigma$, we define $s^{\prime}(q,\sigma)=t$, such that $s$ chooses
$t$ over the prefix run $m(q)$ and current letter $\sigma$.

We claim that $s^{\prime}$ is cautious. Indeed, for the correctness proof, we
shall change $s$ into $s^{\prime}$ iteratively, considering in each iteration
a single state $q$ and letter $\sigma$. Assume by way of contradiction that
exists a word $u\in\Sigma^{*}$ on which $s^{\prime}$ generates a path $\tau$
that ends in a state $q$, such that $s^{\prime}(u\sigma)=t$ for a non-cautious
transition $t$. Without loss of generality, we may assume that this is not the
case for any strict prefix of $u$, as otherwise we can consider that prefix
instead of $u$.

By the definition of non-cautiousness, there exists a word $w$, such that the
maximal value of ${\mathsf{Sup}}(\tau\pi)$ for a run $\pi$ from $q$ over
$\sigma w$ starting with $t$ is strictly smaller than the maximal value of
${\mathsf{Sup}}(\tau\pi^{\prime})$ where $\pi^{\prime}$ is a run from $q$ over
$\sigma w$ that does not start with $t$.

It thus follows that ${\mathsf{Sup}}(\pi^{\prime})>{\mathsf{Sup}}(\tau)$ and
that for every run $\pi$ from $q$ over $\sigma w$ starting with $t$, we have
${\mathsf{Sup}}(\pi^{\prime})>{\mathsf{Sup}}(\pi)$. Now, let $\rho$ be a run
that witnesses $t$’s minimality in the definition of $s^{\prime}$, namely $s$
chooses $t$ when reading $\sigma$ after reaching $q$ over $\rho$, and for
every run $\rho^{\prime}$ that ends in $q$, we have
${\mathsf{Sup}}(\rho)\leq{\mathsf{Sup}}(\rho^{\prime})$.

Then, in particular, ${\mathsf{Sup}}(\rho)\leq{\mathsf{Sup}}(\tau)$. Hence,
${\mathsf{Sup}}(\pi^{\prime})>{\mathsf{Sup}}(\rho)$. Therefore, for every run
$\pi$ from $q$ over $\sigma w$ starting with $t$, we have
${\mathsf{Sup}}(\rho\pi^{\prime})>{\mathsf{Sup}}(\rho\pi)$, contradicting the
cautiousness of $s$.

Having that $s^{\prime}$ is cautious, we get from Lemma 4.18 that it is also
winning in the letter game, implying that the deterministic automaton that
results from pruning ${\cal A}$ along $s^{\prime}$ is indeed equivalent to
${\cal A}$.

Now, for ${\mathsf{Inf}}$ automata, the proof is analogous, choosing the
${\mathsf{Inf}}$-maximal run rather than the ${\mathsf{Sup}}$-minimal run,
switching between some $\geq$ and $\leq$ and between some $<$ and $>$, and
providing the following final argument: For every run $\pi$ from $q$ over
$\sigma w$ starting with $t$, we have
${\mathsf{Inf}}(\pi)<{\mathsf{Inf}}(\tau)$ and
${\mathsf{Inf}}(\pi)<{\mathsf{Inf}}(\pi^{\prime})$. Now, let $\rho$ be a run
that witnesses $t$’s maximality in the definition of $s^{\prime}$, namely $s$
chooses $t$ when reading $\sigma$ after reaching $q$ over $\rho$, and for
every run $\rho^{\prime}$ that ends in $q$, we have
${\mathsf{Inf}}(\rho)\geq{\mathsf{Inf}}(\rho^{\prime})$.

Then, in particular, ${\mathsf{Inf}}(\rho)\geq{\mathsf{Inf}}(\tau)$. Hence,
for every run $\pi$ from $q$ over $\sigma w$ starting with $t$, we have
${\mathsf{Inf}}(\pi)<{\mathsf{Inf}}(\rho)$ and
${\mathsf{Inf}}(\pi)<{\mathsf{Inf}}(\pi^{\prime})$. Hence, for every run $\pi$
from $q$ over $\sigma w$ starting with $t$, we have
${\mathsf{Inf}}(\rho\pi)<{\mathsf{Inf}}(\rho\pi^{\prime})$, contradicting the
cautiousness of $s$.

##  Appendix B Proofs of Section 5

######  Proof B.1 (Proof of Proposition 5.1).

$\Longrightarrow:$ Reducing the synthesis problem to the history-determinism
problem.

The idea of the reduction (both in the best-value and $t$-threshold case) is
to turn output letter choices in ${\cal A}$ into nondeterministic choices in
${\cal A}^{\prime}$. Then ${\cal A}^{\prime}$ maps $I\in\Sigma_{I}^{\omega}$
onto $\mathtt{Best}_{{\cal A}}(I)$. A solution to the synthesis problem for
${\cal A}$ corresponds exactly to a function that resolves the nondeterminism
of ${\cal A}^{\prime}$ on the fly to build a run with value
$\mathtt{Best}_{{\cal A}}(I)$, that is, a witnesses of the history determinism
of ${\cal A}^{\prime}$. If ${\cal A}$ is itself nondeterministic, then ${\cal
A}^{\prime}$ will have both the nondeterminism of ${\cal A}$ and the
nondeterminism that stems from the choice of output letters. As long as the
nondeterminism of ${\cal A}$ is history deterministic, the nondeterminism of
${\cal A}^{\prime}$ is history deterministic if and only if ${\cal A}$ is
local best value realisable.

More formally, first let us define formally the projection of ${\cal A}$ onto
its first component: ${\cal A}^{\prime}=(\Sigma_{I},Q,\iota,\delta^{\prime})$,
where $\delta^{\prime}(q,a)=\bigvee_{b\in\Sigma_{O}}\delta(q,(a,b))$. In other
words, the automaton ${\cal A}^{\prime}$ moves the $\Sigma_{O}$ letters from
the input word into a nondeterministic choice. It implements a mapping of
inputs $I\in\Sigma_{I}^{\omega}$ onto $\mathtt{Best}_{{\cal A}}(I)$. We now
argue that witnesses of history determinism for ${\cal A}^{\prime}$ coincide
with solutions to the best-value synthesis problem for ${\cal A}$. Let $s$ be
the witness of the history determinism of ${\cal A}$.

We first argue that a solution $s^{\prime}$ to the best-value synthesis
problem for ${\cal A}$, combined with $s$ is a witness that ${\cal
A}^{\prime}$ is history-deterministic. Indeed, in Eve’s letter game on ${\cal
A}^{\prime}$, Eve has two types of choices: a choice
$\bigvee_{b\in\Sigma_{O}}\delta(q,(a,b))$ of an $\Sigma_{O}$-letter, and the
choice in $\delta(q,(a,b))$ that stems from ${\cal A}$. Let $\hat{s}$ be the
strategy that after a run prefix $\rho$ ending in a state $q$ over a word
$w\in\Sigma_{I}$ chooses the letter $s^{\prime}(w)$, that is, the disjunct
$\delta(q,(a,s^{\prime}(w)))$ in the disjunction
$\bigvee_{b\in\Sigma_{O}}\delta(q,(a,b))$. Then, from
$\delta(q,(a,s^{\prime}(w)))$, $\hat{s}$ behaves as $s$ would after a run of
${\cal A}$ over $w\otimes\bar{s}(w)$.

First, observe that a run $\rho$ of ${\cal A}^{\prime}$ over
$I\in\Sigma_{I}^{\omega}$, labelled with the choices of $\Sigma_{O}$-letters
forming some $O\in\Sigma_{O}^{\omega}$, corresponds to a run of ${\cal A}$
over $I\otimes O$ with the same value.

Then, since $s^{\prime}$ is a solution to the best value synthesis problem, it
guarantees that given an input word $\Sigma_{I}$, the sequence of $\Sigma_{O}$
letters chosen by $\hat{s}$ is $\bar{s}(I)$, and ${\cal
A}(I\otimes\bar{s}(I))=\mathtt{Best}_{{\cal A}}(I)$. Then, as $s$ witnesses
the history determinism of ${\cal A}$, $\hat{s}$ guarantees that $\rho$ has
value ${\cal A}(I\otimes\bar{s}(I)$, that is, $\hat{s}$ witnesses the history
determinism of ${\cal A}^{\prime}$.

For the converse direction, assume ${\cal A}^{\prime}$ is history
deterministic, as witnessed by some strategy $s$. We claim that $s$ induces a
solution $s^{\prime}$ to the synthesis problem for ${\cal A}$ as follows:
after reading an finite sequence of inputs $Ia\in\Sigma_{I}^{*}$, $s$ has
built some run $\rho$ over $I$ that ends in a state $q$, after which $s$
resolves a disjunction $\bigvee_{b\in\Sigma_{O}}\delta(q,\binom{a}{b})$ by
choosing some $b\in\Sigma_{O}$. We then set $s^{\prime}(Ia)=b$. Then, as $s$
witnesses that ${\cal A}^{\prime}$ is history-deterministic, the run chosen by
$s$ over an input $I\in\Sigma_{I}^{\omega}$ has the value
$\mathtt{Best}_{{\cal A}}(I)$. By construction of ${\cal A}^{\prime}$ and
$s^{\prime}$, this is the value ${\cal A}(I\otimes\bar{s^{\prime}}(I)$, that
is, $s^{\prime}$ is indeed a solution to the synthesis problem on ${\cal A}$.
Furthermore, observe that an implementation of $s$ also implements
$s^{\prime}$ by ignoring the outputs of $s$ that do not choose $\Sigma_{O}$
letters, so the memory of the solution to the synthesis problem is bounded by
the memory required by a witness of history determinism.

$\Longleftarrow$: Reducing the history-determinism problem to the synthesis
problem.

Dually to the previous translation, we turn the nondeterminism in an automaton
${\cal A}$ into choices of output letters in the best-value synthesis problem.
We build a deterministic automaton ${\cal A}^{\prime}$ that is similar to
${\cal A}$ except that it reads both an input letter and a transition; then a
transition can only be chosen if it is the second element of the input (that
is, the output letter). Then ${\cal A}^{\prime}$ maps valid runs of ${\cal A}$
to their value and a solution to the local best value synthesis problem of
${\cal A}^{\prime}$ corresponds exactly to a witness of history-determinism
for ${\cal A}$.

Formally, let ${\cal A}^{\prime}$ be the ${\mathsf{Val}}$ automaton
$(\Sigma\times\Delta,Q,\iota,\delta^{\prime})$ where
$\delta^{\prime}(q,(a,q\xrightarrow{a:x}q^{\prime}))=(x,q^{\prime})$ if
$(x,q^{\prime})\in\delta(q,a)$. ${\cal A}^{\prime}$ maps valid runs of ${\cal
A}$ written as pairs $(w,r)$ where $r$ is a run of ${\cal A}$ over $w$, onto
${\mathsf{Val}}(r)$ and in particular $\mathtt{Best}_{{\cal
A}^{\prime}}(I)={\cal A}(I)$.

We claim that ${\cal A}^{\prime}$ is best-value realisable if and only ${\cal
A}$ is history-deterministic. Indeed, a solution $s$ to the best value
synthesis problem of ${\cal A}^{\prime}$ corresponds to a function building a
run of ${\cal A}$ over the input $I$ transition by transition such that the
value of the run is $\mathtt{Best}_{{\cal A}^{\prime}}(I)$. Since
$\mathtt{Best}_{{\cal A}^{\prime}}(I)$ is ${\cal A}(I)$, $s$ is precisely a
witness of history-determinism in ${\cal A}$. Similarly, a witness of history-
determinism in ${\cal A}$ induces a solution to the best value synthesis
problem for ${\cal A}^{\prime}$ since it builds a run of ${\cal A}$ over $I$
with value at least ${\cal A}(I)$, exactly what is required from a solution to
the best value synthesis.