15320 LABEL:LastPageJan. 10, 2019Aug. 23, 2019

# Parity Games with Weights

Sven Schewea  aUniversity of Liverpool, Liverpool, United Kingdom
<EMAIL_ADDRESS>,  Alexander Weinertb  bGerman
Aerospace Center (DLR), Intelligent and Distributed Systems, Köln, Germany
<EMAIL_ADDRESS>and  Martin Zimmermanna

###### Abstract.

Quantitative extensions of parity games have recently attracted significant
interest. These extensions include parity games with energy and payoff
conditions as well as finitary parity games and their generalization to parity
games with costs. Finitary parity games enjoy a special status among these
extensions, as they offer a native combination of the qualitative and
quantitative aspects in infinite games: The quantitative aspect of finitary
parity games is a quality measure for the qualitative aspect, as it measures
the limit superior of the time it takes to answer an odd color by a larger
even one. Finitary parity games have been extended to parity games with costs,
where each transition is labeled with a nonnegative weight that reflects the
costs incurred by taking it. We lift this restriction and consider parity
games with costs with arbitrary integer weights.

We show that solving such games is in $\textsc{NP}\cap\textsc{co-NP}$, the
signature complexity for games of this type. We also show that the protagonist
has finite-state winning strategies, and provide tight pseudo-polynomial
bounds for the memory he needs to win the game. Naturally, the antagonist may
need infinite memory to win. Moreover, we present tight bounds on the quality
of winning strategies for the protagonist.

Furthermore, we investigate the problem of determining, for a given threshold
$b$, whether the protagonist has a strategy of quality at most $b$ and show
this problem to be ExpTime-complete. The protagonist inherits the necessity of
exponential memory for implementing such strategies from the special case of
finitary parity games.

###### Key words and phrases:

Infinite Games, Quantitative Games, Parity Games

Supported by the EPSRC projects ‘Energy Efficient Control’ (EP/M027287/1) and
‘Solving Parity Games in Theory and Practice’ (EP/P020909/1).

Supported by the project “TriCS” (ZI 1516/1–1) of the German Research
Foundation (DFG) and the Saarbrücken Graduate School of Computer Science.
Major parts of this work were performed while the author was employed with the
Reactive Systems Group at Saarland University, Germany.

##  1\. Introduction

Finite games of infinite duration offer a wealth of challenges and
applications that has garnered a lot of attention. The traditional class of
games under consideration were games with a simple parity [Koz83, EL86, EJ91,
McN93, BCJ+97, Zie98, Jur98, Jur00, VJ00, JPZ08, Sch08, STV15, Sch17, CJK+17,
JL17, FJS+17, Leh18] or payoff [Pur95, ZP96, Jur98, BV07, STV15] objective.
These games form a hierarchy with very simple tractable reductions from parity
games through mean-payoff games [Pur95, ZP96, Jur98, BV07, STV15] and
discounted-payoff games [ZP96, Jur98, STV15] to simple stochastic games
[Con93].

More recently, games with a mixture of the qualitative parity condition and
further quantitative objectives have been considered, including mean-payoff
parity games [CHJ05] and energy parity games [CD12]. Finitary parity games
[CHH09] take a special role within the class of games with mixed parity and
payoff objectives. To win a finitary parity game, Player $0$ needs to enforce
a play with a bound $b$ such that almost all occurrences of an odd color are
followed by a higher even color within at most $b$ steps.

This is interesting, because it provides a natural link between the
qualitative and quantitative objective. One aspect that attracted attention is
that, as long as one is not interested in optimizing the bound $b$, these
games are the only games of the lot that are known to be tractable [CHH09].
However, minimizing the bound $b$ itself is also interesting: As the bounds
limit the response time, small bounds translate to high quality guarantees
[WZ17].

This property calls for a generalization to different cost models, and a first
generalization has been made with the introduction of parity games with costs
[FZ14]. In parity games with costs, the basic cost function of finitary parity
games—where each step incurs the same cost—is replaced with different
nonnegative costs for different edges. In this article, we generalize this
further to _general_ integer costs: We decorate the edges with integer
weights. The quantitative aspect in these parity games with weights consists
of having to answer almost all odd colors by a higher even color, such that
the amplitude of the accumulated weight on the path to this even color is
bounded by a bound $b$.

In addition to their conceptual charm, we show that parity games with weights
are PTime equivalent to energy parity games. This indicates that these games
are part of a natural complexity class, whereas the games with a plain
objective appear to form a hierarchy. We use the reduction from parity games
with weights to energy parity games to solve them. This reduction goes through
intermediate reductions to and from _bounded_ parity games with weights. These
games have the additional restriction that the limit superior of the absolute
weight of initial sequences of unanswered requests in a play is finite. These
bounded parity games with weights are then reduced to energy parity games. The
other direction of the reduction is through simple gadgets that preserve the
main elements of winning strategies in games that are extended in two steps by
very simple gadgets. As a result, we obtain the same complexity results for
parity games with weights as for energy parity games, i.e.,
$\textsc{NP}\cap\textsc{co-NP}$, the signature complexity for finite games of
infinite duration with parity conditions and their extensions. Thereby, we
obtain an argument that these games might be representatives of a natural
complexity class, lending a further argument for the relevance of two player
games with mixed qualitative and quantitative winning conditions. Furthermore,
Daviaud et al. recently showed that parity games with weights can even be
solved in pseudo-quasi-polynomial time [DJL18].

Naturally, parity games with weights subsume parity games (as a special case
where all weights are zero), finitary parity games (as a special case where
all weights are positive), and parity games with costs (as a special case
where all weights are nonnegative).

We show that the protagonist has finite-state winning strategies, and provide
tight pseudo-polynomial bounds for the memory he needs to win the game. We
also present tight bounds on the quality of winning strategies for the
protagonist. Naturally, the antagonist may need infinite memory to win.

Solving parity games with weights amounts to determining whether there exists
a bound $b$ such that the protagonist is able to enforce a play in which the
amplitude of the accumulated weight between almost all requests and their
corresponding answer is bounded by $b$. The value of $b$, however, may be
arbitrarily large, subject to the bounds on the quality of winning strategies.
Hence, it is natural to consider the threshold problem for parity games with
weights: “Given a parity game with weights $\mathcal{G}$ and a bound
$b\in\mathbb{N}$, is the protagonist able to enforce that the paths between
almost all requests and their respective answers have an amplitude of at most
$b$?” It is known that the threshold problem for finitary parity games and
parity games with costs is PSpace-complete [WZ17]. In this work, we show that
the complexity increases even further in the case of parity games with
weights, as the threshold problem for such games is ExpTime-complete. The
complexity of strategies witnessing the answer to the threshold problem,
however, does not increase: Both players require exponential memory in order
to ensure or violate the bound $b$, respectively, if they are able to do so at
all.

This paper is an extended version of work published at CSL 2018 [SWZ18].

##  2\. Preliminaries

We denote the nonnegative integers by $\mathbb{N}$, the integers by
$\mathbb{Z}$, and define $\mathbb{N}_{\infty}=\mathbb{N}\cup\\{\infty\\}$. As
usual, we have $\infty>n$, $-\infty<n$, $n+\infty=\infty$, and
$-\infty-n=-\infty$ for all $n\in\mathbb{Z}$.

An arena $\mathcal{A}=(V,V_{0},V_{1},E)$ consists of a finite, directed graph
$(V,E)$ and a partition $\\{V_{0},V_{1}\\}$ of $V$ into the positions of
Player $0$ (drawn as ellipses) and Player $1$ (drawn as rectangles). For
pronomial convenience, we refer to Player $0$ as he, and to Player $1$ as she.
The size of $\mathcal{A}$, denoted by $|\mathcal{A}|$, is defined as $|V|$. A
play in $\mathcal{A}$ is an infinite path $\rho=v_{0}v_{1}v_{2}\cdots$ through
$(V,E)$. To rule out finite plays, we require every vertex to be nonterminal.
We define $|\rho|=\infty$. Dually, for a finite play prefix $\pi=v_{0}\cdots
v_{j}$ we define $|\pi|=j+1$.

A game $\mathcal{G}=(\mathcal{A},\mathrm{Win})$ consists of an arena
$\mathcal{A}$ with vertex set $V$ and a set $\mathrm{Win}\subseteq V^{\omega}$
of winning plays for Player $0$. The set of winning plays for Player $1$ is
$V^{\omega}\setminus\mathrm{Win}$. A winning condition $\mathrm{Win}$ is
$0$-extendable if, for all $\rho\in V^{\omega}$ and all $w\in V^{*}$,
$\rho\in\mathrm{Win}$ implies $w\rho\in\mathrm{Win}$. Dually, $\mathrm{Win}$
is $1$-extendable if, for all $\rho\in V^{\omega}$ and all $w\in V^{*}$,
$\rho\notin\mathrm{Win}$ implies $w\rho\notin\mathrm{Win}$. Finally,
$\mathrm{Win}$ is prefix-independent, if it is both $0$-extendable and
$1$-extendable.

A strategy for Player $i\in\\{0,1\\}$ is a mapping $\sigma\colon
V^{*}V_{i}\rightarrow V$ such that $(v,\sigma(wv))\in E$ holds true for all
$wv\in V^{*}V_{i}$. We say that $\sigma$ is positional if
$\sigma(wv)=\sigma(v)$ holds true for every $wv\in V^{*}V_{i}$. A play
$v_{0}v_{1}v_{2}\cdots$ is consistent with a strategy $\sigma$ for Player $i$,
if $v_{j+1}=\sigma(v_{0}\cdots v_{j})$ holds true for every $j$ with $v_{j}\in
V_{i}$. A strategy $\sigma$ for Player $i$ is a winning strategy for
$\mathcal{G}$ from $v\in V$ if every play that starts in $v$ and is consistent
with $\sigma$ is won by Player $i$. If Player $i$ has a winning strategy from
$v$, then we say Player $i$ wins $\mathcal{G}$ from $v$. The winning region of
Player $i$ is the set of vertices, from which Player $i$ wins $\mathcal{G}$;
it is denoted by $\mathcal{W}_{i}(\mathcal{G})$. Solving a game amounts to
determining its winning regions. If
$\mathcal{W}_{0}(\mathcal{G})\cup\mathcal{W}_{1}(\mathcal{G})=V$, then we say
that $\mathcal{G}$ is determined.

Let $\mathcal{A}=(V,V_{0},V_{1},E)$ be an arena and let $X\subseteq V$. The
$i$-attractor of $X$ is defined inductively as
$\mathrm{Attr}_{i}(X)=\mathrm{Attr}_{i}^{|V|}(X)$, where
$\mathrm{Attr}_{i}^{0}(X)=X$ and

$\mathrm{Attr}_{i}^{j}(X)=\mathrm{Attr}_{i}^{j-1}(X)\cup\\{v\in
V_{i}\mid\exists v^{\prime}\in\mathrm{Attr}_{i}^{j-1}(X).\,(v,v^{\prime})\in
E\\}\\\ \cup\\{v\in V_{1-i}\mid\forall(v,v^{\prime})\in
E.\,v^{\prime}\in\mathrm{Attr}_{i}^{j-1}(X)\\}\enspace.$

Hence, $\mathrm{Attr}_{i}(X)$ is the set of vertices from which Player $i$ can
force the play to enter $X$: Player $i$ has a positional strategy $\sigma_{X}$
such that each play that starts in some vertex in $\mathrm{Attr}_{i}(X)$ and
is consistent with $\sigma_{X}$ eventually encounters some vertex from $X$. We
call $\sigma_{X}$ an attractor strategy towards $X$. Moreover, the
$i$-attractor can be computed in time linear in $|E|$ [NRY96]. When we want to
stress the arena $\mathcal{A}$ the attractor is computed in, we write
$\mathrm{Attr}_{i}^{\mathcal{A}}(X)$.

A set $X\subseteq V$ is a trap for Player $i$, if every vertex in $X\cap
V_{i}$ has only successors in $X$ and every vertex in $X\cap V_{1-i}$ has at
least one successor in $X$. In this case, Player $1-i$ has a positional
strategy $\tau_{X}$ such that every play starting in some vertex in $X$ and
consistent with $\tau_{X}$ never leaves $X$. We call such a strategy a trap
strategy.

######  Remark .

  1. (1)

The complement of an $i$-attractor is a trap for Player $i$.

  2. (2)

If $X$ is a trap for Player $i$, then $\mathrm{Attr}_{1-i}(X)$ is also a trap
for Player $i$.

  3. (3)

If $\mathrm{Win}$ is $i$-extendable and $(\mathcal{A},\mathrm{Win})$
determined, then $\mathcal{W}_{1-i}(\mathcal{A},\mathrm{Win})$ is a trap for
Player $i$.

A memory structure $\mathcal{M}=(M,\text{init},\mathrm{upd})$ for an arena
$(V,V_{0},V_{1},E)$ consists of a finite set $M$ of memory states, an
initialization function $\text{init}\colon V\rightarrow M$, and an update
function $\mathrm{upd}\colon M\times E\rightarrow M$. The update function can
be extended to finite play prefixes in the usual way:
$\mathrm{upd}^{+}(v)=\text{init}(v)$ and
$\mathrm{upd}^{+}(wvv^{\prime})=\mathrm{upd}(\mathrm{upd}^{+}(wv),(v,v^{\prime}))$
for $w\in V^{*}$ and $(v,v^{\prime})\in E$. A next-move function
$\mathrm{Nxt}\colon V_{i}\times M\rightarrow V$ for Player $i$ has to satisfy
$(v,\mathrm{Nxt}(v,m))\in E$ for all $v\in V_{i}$ and $m\in M$. It induces a
strategy $\sigma$ for Player $i$ with memory $\mathcal{M}$ via
$\sigma(v_{0}\cdots v_{j})=\mathrm{Nxt}(v_{j},\mathrm{upd}^{+}(v_{0}\cdots
v_{j}))$. A strategy is called finite-state if it can be implemented by a
memory structure. We define $|\mathcal{M}|=|M|$. Slightly abusively, we say
that the size of a finite-state strategy is the size of a memory structure
implementing it.

##  3\. Parity Games with Weights

Fix an arena $\mathcal{A}=(V,V_{0},V_{1},E)$. A weighting for $\mathcal{A}$ is
a function $w\colon E\rightarrow\mathbb{Z}$. We define $w(\varepsilon)=w(v)=0$
for all $v\in V$ and extend $w$ to sequences of vertices of length at least
two by summing up the weights of the traversed edges. Given a play (prefix)
$\pi=v_{0}v_{1}v_{2}\cdots$, we define the amplitude of $\pi$ as
$\mathrm{Ampl}(\pi)=\sup_{j<|\pi|}|w(v_{0}\cdots
v_{j})|\in\mathbb{N}_{\infty}$.

A coloring of $V$ is a function $\Omega\colon V\rightarrow\mathbb{N}$. The
classical parity condition requires almost all occurrences of odd colors to be
answered by a later occurrence of a larger even color. Hence, let
$\mathrm{Ans}({c})=\\{c^{\prime}\in\mathbb{N}\mid c^{\prime}\geq c\text{ and
$c^{\prime}$ is even}\\}$ be the set of colors that “answer” a “request” for
color $c$. We denote a vertex $v$ of color $c$ by $\nicefrac{{v}}{{c}}$.

Fijalkow and Zimmermann introduced a generalization of the parity condition
and the finitary parity condition [CHH09], the parity condition with costs
[FZ14]. There, the edges of the arena are labeled with _nonnegative weights_
and the winning condition demands that there exists a bound $b$ such that
almost all requests are answered with weight at most $b$, i.e., the weight of
the infix between the request and the response has to be bounded by $b$.

Our aim is to extend the parity condition with costs by allowing for the full
spectrum of weights to be used, i.e., by also incorporating negative weights.
In this setting, the weight of an infix between a request and a response might
be negative. Thus, the extended condition requires the weight of the infix to
be bounded from above and from below.111We discuss other possible
interpretations of negative weights in Section 10. To distinguish between the
parity condition with costs and the extension introduced here, we call our
extension the parity condition with weights.

Formally, let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play. We define the cost-of-
response at position $j\in\mathbb{N}$ of $\rho$ by

$\mathrm{Cor}(\rho,j)=\min\\{\mathrm{Ampl}(v_{j}\cdots v_{j^{\prime}})\mid
j^{\prime}\geq j,\Omega(v_{j^{\prime}})\in\mathrm{Ans}({\Omega(v_{j})})\\},$

where we use $\min\emptyset=\infty$. As the amplitude of an infix only
increases by extending the infix, $\mathrm{Cor}(\rho,j)$ is the amplitude of
the shortest infix that starts at position $j$ and ends at an answer to the
request posed at position $j$. We illustrate this notion in Figure 1.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$w$$v_{j}$$v_{j^{\prime}}$ Figure
1. The cost-of-response of some request posed by visiting vertex $v_{j}$,
which is answered by visiting vertex $v_{j^{\prime}}$.

We say that a request at position $j$ is answered with cost $b$, if
$\mathrm{Cor}(\rho,j)=b$. Consequently, a request with an even color is
answered with cost zero. The cost-of-response of an unanswered request is
infinite, even if the amplitude of the remaining play is bounded. In
particular, this means that an unanswered request at position $j$ may be
“unanswered with finite cost $b$” (if the amplitude of the remaining play is
$b\in\mathbb{N}$) or “unanswered with infinite cost” (if the amplitude of the
remaining play is infinite). In either case, however, we have
$\mathrm{Cor}(\rho,j)=\infty$.

We define the parity condition with weights as

$\mathrm{WeightParity}(\Omega,w)=\\{\rho\in
V^{\omega}\mid\limsup\nolimits_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)\in\mathbb{N}\\}\enspace.$

I.e., $\rho$ satisfies the condition if and only if there exists a bound
$b\in\mathbb{N}$ such that almost all requests are answered with cost less
than $b$. In particular, only finitely many requests may be unanswered, even
with finite cost. Note that the bound $b$ may depend on the play $\rho$.

| Complexity |  Mem. Pl. $0$/Pl. $1$ | Bounds
---|---|---|---
Parity Games [CJK+17] | quasi-poly. | pos./pos. | –
Energy Parity Games [CD12, DJL18] | pseudo-quasi-poly. |  $\mathcal{O}(ndW)$/pos. | $\mathcal{O}(nW)$
Finitary Parity Games [CHH09] | poly. | pos./inf. | $\mathcal{O}(nW)$
Parity Games with Costs [FZ14, MMS15] | quasi-poly. | pos./inf. | $\mathcal{O}(nW)$
Table 1. Characteristic properties of variants of parity games.

We call a game $\mathcal{G}=(\mathcal{A},\mathrm{WeightParity}(\Omega,w))$ a
parity game with weights, and we define $|\mathcal{G}|=|\mathcal{A}|+\log(W)$,
where $W$ is the largest absolute weight assigned by $w$; i.e., we assume
weights to be encoded in binary. If $w$ assigns zero to every edge, then
$\mathrm{WeightParity}(\Omega,w)$ is a classical (max-) parity condition,
denoted by $\mathrm{Parity}(\Omega)$. Similarly, if $w$ assigns positive
weights to every edge, then $\mathrm{WeightParity}(\Omega,w)$ is equal to the
finitary parity condition over $\Omega$, as introduced by Chatterjee and
Henzinger [CH06]. Finally, if $w$ assigns only nonnegative weights, then
$\mathrm{WeightParity}(\Omega,w)$ is a parity condition with costs, as
introduced by Fijalkow and Zimmermann [FZ14]. In these cases, we refer to
$\mathcal{G}$ as a parity game, a finitary parity game, or a parity game with
costs, respectively. Dually, every parity game, finitary parity game, and
parity game with costs is a parity game with weights. We recall the
characteristics of these special cases in Table 1.

##  4\. Solving Parity Games with Weights

We now show how to solve parity games with weights. Our approach is inspired
by the classic work on finitary parity games [CHH09] and parity games with
costs [FZ14]: We first define a stricter variant of these games, which we call
bounded parity games with weights, and then show two reductions:

  * •

parity games with weights can be solved in polynomial time with oracles that
solve bounded parity games with weights (in this section); and

  * •

bounded parity games with weights can be solved in polynomial time with
oracles that solve energy parity games (Section 5).

Furthermore, we provide a polynomial time reduction from solving energy parity
games to solving parity games with weights in Section 8. We thereby show that
parity games with weights, bounded parity games with weights, and energy
parity games belong to the same complexity class.

The energy parity games that we reduce to are known to be efficiently
solvable, as they are in $\textsc{NP}\cap\textsc{co-NP}$ due to Chatterjee and
Doyen [CD12]. Moreover, they are LogSpace-equivalent to mean-payoff parity
games as introduced by Chatterjee, Henzinger, and Jurdziński [CHJ05]. Hence
they can be solved in pseudo-quasi-polynomial time, due to recent advances by
Daviaud, Jurdziński, and Lazić [DJL18].

We first introduce the  bounded parity condition with weights, which is a
strengthening of the parity condition with weights. Hence, it is also induced
by a coloring and a weighting:

$\mathrm{BndWeightParity}(\Omega,w)=\mathrm{WeightParity}(\Omega,w)\\\
\cap\\{\rho\in V^{\omega}\mid\text{no request in }\rho\text{ is unanswered
with infinite cost}\\}\enspace.$

Note that this condition allows for a finite number of unanswered requests, as
long as they are unanswered with finite cost.

We solve parity games with weights by repeatedly solving bounded parity games
with weights. To this end, we apply the following two properties of the
winning conditions: We have
$\mathrm{BndWeightParity}(\Omega,w)\subseteq\mathrm{WeightParity}(\Omega,w)$
as well as that $\mathrm{WeightParity}(\Omega,w)$ is $0$-extendable. Hence, if
Player $0$ has a strategy from a vertex $v$ such that every consistent play
has a suffix in $\mathrm{BndWeightParity}(\Omega,w)$, then the strategy is
winning for her from $v$ w.r.t. $\mathrm{WeightParity}(\Omega,w)$. Thus,

$\mathrm{Attr}_{0}(\mathcal{W}_{0}(\mathcal{A},\mathrm{BndWeightParity}(\Omega,w)))\subseteq\mathcal{W}_{0}(\mathcal{A},\mathrm{WeightParity}(\Omega,w))\enspace.$

The algorithm that solves parity games with weights repeatedly removes
attractors of winning regions of the bounded parity game with weights until a
fixed point is reached. We will later formalize this sketch to show that the
removed parts are a subset of Player $0$’s winning region in the parity game
with weights.

To show that the obtained fixed point covers the complete winning region of
Player $0$, we use the following lemma to show that the remaining vertices are
a subset of Player $1$’s winning region in the parity game with weights. The
proof is very similar to the corresponding one for finitary parity games and
parity games with costs.

######  Lemma 1.

Let $\mathcal{G}=(\mathcal{A},\mathrm{WeightParity}(\Omega,w))$ and let
$\mathcal{G}^{\prime}=(\mathcal{A},\mathrm{BndWeightParity}(\Omega,w))$. If
$\mathcal{W}_{0}(\mathcal{G}^{\prime})=\emptyset$, then
$\mathcal{W}_{0}(\mathcal{G})=\emptyset$.

######  Proof 4.1.

As bounded parity conditions with weights are Borel, bounded parity games with
weights are determined [Mar75]. Hence,
$\mathcal{W}_{0}(\mathcal{G}^{\prime})=\emptyset$ implies that, for every
vertex $v$ of $\mathcal{A}$, Player $1$ has a strategy $\tau_{v}$ that is
winning in $\mathcal{G}^{\prime}$ from $v$.

We combine these strategies into a single strategy $\tau$ for Player $1$ that
is winning in $\mathcal{G}$ from every vertex of $\mathcal{A}$. This strategy
is controlled by a vertex $v^{*}$ (initialized with the starting vertex of the
play) and a counter $\kappa$ ranging over $\mathbb{N}$ (initialized with
zero). The strategy $\tau$ mimics the strategy $\tau_{v^{*}}$ from $v^{*}$
until a request is followed by an infix without an answer and with amplitude
$\kappa$. This implies that the cost-of-response of this request is at least
$\kappa$. If such a situation is encountered, then $v^{*}$ is set to the
current vertex and $\kappa$ is incremented. Furthermore, the history of the
play is discarded at this point in the play, and $\tau$ behaves henceforth
like $\tau_{v^{*}}$ when starting at $v^{*}$ when this happens.

We now show that $\tau$ is winning for Player $1$ from every vertex in
$\mathcal{G}$. Consider a play $\rho$ that is consistent with this strategy.
If, on the one hand, $\kappa$ is updated infinitely often along $\rho$, then
$\rho$ contains, for every $b\in\mathbb{N}$, a request that has a cost-of-
response that is larger than $b$. Hence, it violates the parity condition with
weights.

If, on the other hand, $\kappa$ is only updated finitely often, then $\rho$
has a suffix $\rho^{\prime}$ that starts in some $v$, which is consistent with
$\tau_{v}$. As $\tau_{v}$ is winning for Player $1$ from $v$ in
$\mathcal{G}^{\prime}$, $\rho^{\prime}$ violates the bounded parity condition
with weights. Also, because $\kappa$ is updated only finitely often during the
suffix, there is a bound $b$ such that the amplitude of every suffix of
$\rho^{\prime}$ that starts at a request is bounded by $b$. Hence, the only
way for $\rho^{\prime}$ to violate the bounded parity condition with weights
is to violate the parity condition. Thus, the full play $\rho$ also violates
the parity condition, and therefore also the parity condition with weights,
which is a strengthening of the parity condition. Therefore, $\tau$ is indeed
winning for Player $1$ from every vertex in $\mathcal{G}$.

Lemma 1 implies that the algorithm for solving parity games with weights by
repeatedly solving bounded parity games with weights (see Algorithm 1) is
correct. Note that we use an oracle for solving bounded parity games with
weights. We provide a suitable algorithm in Section 5.

0: Parity game with weights $\mathcal{G}$ with arena $\mathcal{A}$, coloring
$\Omega$ and weighting $w$

1: $k=0$; $W_{0}^{k}=\emptyset$; $\mathcal{A}_{k}=\mathcal{A}$

2: repeat

3: $k=k+1$

4:
$X_{k}=\mathcal{W}_{0}(\mathcal{A}_{k-1},\mathrm{BndWeightParity}(\Omega,w))$

5: $W_{0}^{k}=W_{0}^{k-1}\cup\mathrm{Attr}_{0}^{\mathcal{A}_{k-1}}(X_{k})$

6:
$\mathcal{A}_{k}=\mathcal{A}_{k-1}\setminus\mathrm{Attr}_{0}^{\mathcal{A}_{k-1}}(X_{k})$

7: until $X_{k}=\emptyset$

8: return $W_{0}^{k}$

Algorithm 1 A fixed-point algorithm computing
$\mathcal{W}_{0}(\mathcal{A},\mathrm{WeightParity}(\Omega,w))$.

The loop terminates after at most $|\mathcal{A}|$ iterations (assuming the
algorithm solving bounded parity games with weights terminates), as, during
each iteration, at least one vertex is removed from the arena. The correctness
proof relies on Lemma 1 and is similar to the ones for finitary parity games
[CHH09] and for parity games with costs [FZ14]. The underlying argument only
relies on a few properties of the winning condition; it is very general—and
fairly standard. We use the same argument again later to establish the
correctness of Algorithm 2.

######  Lemma 2.

Algorithm 1 returns
$\mathcal{W}_{0}(\mathcal{A},\mathrm{WeightParity}(\Omega,w))$.

######  Proof 4.2.

Let $\mathcal{G}=(\mathcal{A},\mathrm{WeightParity}(\Omega,w))$ and let
$k^{*}$ be the final iteration when running the algorithm on $\mathcal{G}$,
i.e., its output is
$W_{0}^{k^{*}}=\bigcup_{0<k<k^{*}}\mathrm{Attr}_{0}^{\mathcal{A}_{k-1}}(X_{k})$.
First, we consider Player $0$ and show
$W_{0}^{k^{*}}\subseteq\mathcal{W}_{0}(\mathcal{G})$. For every vertex $v$
that is in some $X_{k}$, Player $0$ has a strategy $\sigma_{v}$ for
$\mathcal{G}_{k}=(\mathcal{A}_{k-1},\mathrm{BndWeightParity}(\Omega,w))$ that
is winning from $v$. Furthermore, for every attractor
$\mathrm{Attr}_{0}^{\mathcal{A}_{k-1}}(X_{k})$, he has a positional attractor
strategy $\sigma_{k}$. Now, we compose these strategies to a strategy $\sigma$
for Player $0$ in $\mathcal{A}$ via

$\sigma(v_{0}\cdots v_{j})=\begin{cases}\sigma_{k}(v_{j})&\text{if
}v_{j}\in\mathrm{Attr}_{0}^{\mathcal{A}_{k-1}}(X_{k})\setminus X_{k},\\\
\sigma_{v_{j^{\prime}}}(v_{j^{\prime}}\cdots v_{j})&\text{if }v_{j}\in
X_{k}.\\\ \end{cases}$

In the second case, $v_{j^{\prime}}\cdots v_{j}$ is the longest suffix of
$v_{0}\cdots v_{j}$ that only contains vertices from $X_{k}$, the set of
vertices from which Player $0$ has a winning strategy for $\mathcal{G}_{k}$.

Consider a play $\rho=v_{0}v_{1}v_{2}\cdots$ in $\mathcal{A}$ that starts in
$W_{0}^{k^{*}}$ and that is consistent with $\sigma$. For every $j$ there is a
unique $k_{j}$ in the range $0<k_{j}<k^{*}$ such that
$v_{j}\in\mathrm{Attr}_{0}^{\mathcal{A}_{k_{j}-1}}(X_{k_{j}})$. As
$\mathrm{BndWeightParity}(\Omega,w)$ is $1$-extendable, Items 2 and 3 of
Remark 2 imply that each $\mathrm{Attr}_{0}^{\mathcal{A}_{k-1}}(X_{k})$ is a
trap for Player $1$ in $\mathcal{A}_{k-1}$. Hence, we obtain
$k_{0}>k_{1}>k_{2}>\cdots$. As the $k_{j}$ are always greater than zero, the
sequence stabilizes eventually. This implies that $\rho$ has a suffix
$\rho^{\prime}=v_{j}v_{j+1}v_{j+2}\cdots$ that is consistent with
$\sigma_{v_{j}}$.

Hence, due to $\sigma_{v_{j}}$ being a winning strategy for Player $0$ in
$\mathcal{G}_{k}$ from $v_{j}$, we obtain
$\rho^{\prime}\in\mathrm{BndWeightParity}(\Omega,w)$. Hence,
$\rho\in\mathrm{WeightParity}(\Omega,w)$, since the bounded parity condition
with weights is a strengthening of its unbounded variant and due to
$0$-extendability of $\mathrm{WeightParity}(\Omega,w)$. Hence, $\sigma$ is
indeed winning from $W_{0}^{k^{*}}$.

Now, consider Player $1$. We show $V\setminus
W_{0}^{k^{*}}\subseteq\mathcal{W}_{1}(\mathcal{G})$. Then, determinacy of
parity games with weights (due to their winning conditions being Borel
[Mar75]) yields $W_{0}^{k^{*}}=\mathcal{W}_{0}(\mathcal{G})$ and $V\setminus
W_{0}^{k^{*}}=\mathcal{W}_{1}(\mathcal{G})$.

Due to $X_{k^{*}}$ being empty and bounded parity games with weights being
determined (again due to their winning conditions being Borel), Player $1$
wins the bounded parity game with weights $\mathcal{G}_{k^{*}}$ from every
vertex. Applying Lemma 1 shows that she also wins the parity game with weights
$(\mathcal{A}_{{k^{*}}-1},\mathrm{WeightParity}(\Omega,w))$ from every vertex.
Finally, as $V\setminus
W_{0}^{k^{*}}=\mathcal{W}_{1}(\mathcal{A}_{{k^{*}}-1},\mathrm{WeightParity}(\Omega,w))$
is a trap for Player $0$ in $\mathcal{A}$ by construction, he also wins
$\mathcal{G}=(\mathcal{A},\mathrm{WeightParity}(\Omega,w))$ from every vertex
in $V\setminus W_{0}^{k^{*}}$.

The winning strategy for Player $0$ defined in the proof of Lemma 2 can be
implemented by a memory structure of size $\max_{k<k^{*}}s_{k}$, where $s_{k}$
is the size of a winning strategy $\sigma_{k}$ for Player $0$ in the bounded
parity game with weights solved in the $k$-th iteration, and where $k^{*}$ is
the value of $k$ at termination. To this end, one uses the fact that the
winning regions $X_{k}$ are disjoint and are never revisited once left. Hence,
the implementations of the $\sigma_{k}$ can use the same states yielding the
upper bound $\max_{k<k^{*}}s_{k}$.

##  5\. Solving Bounded Parity Games with Weights

After having reduced the problem of solving parity games with weights to that
of solving (multiple) bounded parity games with weights, we reduce solving
bounded parity games with weights to solving (multiple) energy parity games
[CD12].

Similar to a parity game with weights, in an energy parity game, the vertices
are colored and the edges are equipped with weights. It is the goal of Player
$0$ to satisfy the parity condition, while, at the same time, ensuring that
the accumulated weight of every prefix, its so-called energy level, is bounded
from below. In contrast to a parity game with weights, however, the weights in
an energy parity game are not “tied” to the requests and responses denoted by
the coloring.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$\nicefrac{{v_{1}}}{{1}}$$\nicefrac{{v_{2}}}{{2}}$$-1$$-1$$\nicefrac{{v_{1}}}{{1}}$$\nicefrac{{v_{2}}}{{0}}$$\nicefrac{{v_{3}}}{{2}}$$0$$+1$$0$$0$
Figure 2. The difference between energy parity games and parity games with
weights.

Consider, for example, the games shown in Figure 2. In the game on the left-
hand side, players only have a single, trivial strategy. If we interpret this
game as a parity game with weights, Player $0$ wins from every vertex, as each
request is answered with cost one. If we, however, interpret that game as an
energy parity game, Player $1$ instead wins from every vertex, since the
energy level decreases by one with every move. In the game on the right-hand
side, the situation is reversed: When interpreting this game as a parity game
with weights, Player $1$ wins from every vertex, as she can easily unbound the
costs of the requests for color one by staying in vertex $v_{2}$ for an ever-
increasing number of cycles. Dually, when interpreting this game as an energy
parity game, Player $0$ wins from every vertex, since the parity condition is
clearly satisfied in every play, and Player $1$ is only able to increase the
energy level, while it is never decreased.

In Section 5.1, we introduce energy parity games formally and present how to
solve bounded parity games with weights via energy games in Section 5.2.
Finally, Sections 5.3.1 and 5.3.2 are dedicated to the correctness proof of
the construction.

###  5.1. Energy Parity Games

An energy parity game $\mathcal{G}=(\mathcal{A},\Omega,w)$ consists of an
arena $\mathcal{A}=(V,V_{0},V_{1},E)$, a coloring $\Omega\colon
V\rightarrow\mathbb{N}$ of $V$, and an edge weighting $w\colon
E\rightarrow\mathbb{Z}$ of $E$. Note that this definition is not compatible
with the framework presented in Section 2, as we have not (yet) defined the
winner of the plays. This is because they depend on an initial credit, which
is existentially quantified in the definition of winning the game
$\mathcal{G}$. Formally, the set of winning plays with initial credit
$c_{0}\in\mathbb{N}$ is defined as

$\mathrm{EnergyParity}_{c_{0}}(\Omega,w)=\mathrm{Parity}(\Omega)\cap\\{v_{0}v_{1}v_{2}\cdots\in
V^{\omega}\mid\forall j\in\mathbb{N}.\,c_{0}+w(v_{0}\cdots v_{j})\geq
0\\}\enspace.$

Now, we say that Player $0$ wins $\mathcal{G}$ from $v$ if there exists some
initial credit $c_{0}\in\mathbb{N}$ such that he wins
$\mathcal{G}_{c_{0}}=(\mathcal{A},\mathrm{EnergyParity}_{c_{0}}(\Omega,w))$
from $v$ (in the sense of the definitions in Section 2). If this is not the
case, i.e., if Player $1$ wins $\mathcal{G}_{c_{0}}$ from $v$ for every
$c_{0}$, then we say that Player $1$ wins $\mathcal{G}$ from $v$. Note that
the initial credit is uniform for all plays, unlike the bound on the cost-of-
response in the definition of the parity condition with weights, which may, a
priori, depend on the play.

Unraveling these definitions shows that Player $0$ wins $\mathcal{G}$ from $v$
if there is an initial credit $c_{0}$ and a strategy $\sigma$, such that every
play that starts in $v$ and is consistent with $\sigma$ satisfies the parity
condition _and_ the accumulated weight over the play prefixes (the energy
level) never drops below $-c_{0}$. We call such a strategy $\sigma$ a winning
strategy for Player $0$ in $\mathcal{G}$ from $v$. Dually, Player $1$ wins
$\mathcal{G}$ from $v$ if, for every initial credit $c_{0}$, there is a
strategy $\tau_{c_{0}}$, such that every play that starts in $v$ and is
consistent with $\tau_{c_{0}}$ violates the parity condition _or_ its energy
level drops below $-c_{0}$ at least once. Thus, the strategy $\tau_{c_{0}}$
may, as the notation suggests, depend on $c_{0}$. However, Chatterjee and
Doyen [CD12] showed that using different strategies is not necessary: There is
a uniform strategy $\tau$ that is winning from $v$ for every initial credit
$c_{0}$.

[[CD12]] Let $\mathcal{G}$ be an energy parity game. If Player $1$ wins
$\mathcal{G}$ from $v$, then she has a single positional strategy that is
winning from $v$ in $\mathcal{G}_{c_{0}}$ for every $c_{0}$.

We call such a strategy as in Proposition 5.1 a winning strategy for Player
$1$ from $v$. A play consistent with such a strategy either violates the
parity condition, or the energy levels of its prefixes diverge towards
$-\infty$.

Furthermore, Chatterjee and Doyen obtained an upper bound on the initial
credit necessary for Player $0$ to win an energy parity game, as well as an
upper bound on the size of a corresponding finite-state winning strategy.

[[CD12]] Let $\mathcal{G}$ be an energy parity game with $n$ vertices, $d$
colors, and largest absolute weight $W$. The following are equivalent for a
vertex $v$ of $\mathcal{G}$:

  1. (1)

Player $0$ wins $\mathcal{G}$ from $v$.

  2. (2)

Player $0$ wins $\mathcal{G}_{(n-1)W}$ from $v$ with a finite-state strategy
with at most $ndW$ states.

The previous proposition yields that finite-state strategies of bounded size
suffice for Player $0$ to win. Such strategies do not admit long expensive
descents, which we show via a straightforward pumping argument.

######  Lemma 3.

Let $\mathcal{G}$ be an energy parity game with $n$ vertices and largest
absolute weight $W$. Further, let $\sigma$ be a finite-state strategy of size
$s$, and let $\rho$ be a play that starts in some vertex, from which $\sigma$
is winning, and is consistent with $\sigma$. Every infix $\pi$ of $\rho$
satisfies

$w(\pi)>-(ns-1)W-1\enspace.$

######  Proof 5.1.

Let $\sigma$ be implemented by $\mathcal{M}=(M,\text{init},\mathrm{upd})$ and
let $\rho=v_{0}v_{1}v_{2}\cdots$. We assume towards a contradiction that there
is an infix $\pi=v_{j}\cdots v_{j^{\prime}}$ with $w(\pi)\leq-(ns-1)W-1$. We
assume w.l.o.g. $\pi$ to be minimal with this property, i.e., such that there
exists no proper prefix $\pi^{\prime}$ of $\pi$ with
$w(\pi^{\prime})\leq-(ns-1)W-1$.

We define a sequence $j_{0}<\cdots<j_{k}\leq j^{\prime}$ of positions by
starting with $j_{0}=j$. Inductively, for each $j_{k^{\prime}}$, we define
$j_{k^{\prime}+1}$ to be the minimal position strictly greater than
$j_{k^{\prime}}$ that satisfies $w(v_{j}\cdots
v_{j_{k^{\prime}+1}})<w(v_{j}\cdots v_{j_{k^{\prime}}})$. Intuitively, the
positions $j_{k^{\prime}}$ are those positions at which the weight of the
infix $v_{j}\cdots v_{j_{k^{\prime}}}$ reaches a new lower bound. Due to
minimality of $\pi^{\prime}$, we obtain $j_{k}=j^{\prime}$.

We now show that there are two positions $j_{k_{\ell}}$ and
$j_{k_{\ell^{\prime}}}$ such that the weight along the infix from the former
to the latter position decreases and such that we are able to pump that infix
while retaining consistency with the strategy $\sigma$. To this end, we define
$w_{\ell}=w(v_{j}\cdots v_{j_{\ell}})$ for all $\ell\in\\{0,\dots,k\\}$. In
particular, we have $w_{0}=0$. Since each edge has an absolute weight of at
most $W$, we obtain $w_{\ell+1}\geq w_{\ell}-W$ for all
$\ell\in\\{0,\dots,k-1\\}$, which in turn implies $w_{k}\geq-kW$. Moreover,
since we have $j_{k}=j^{\prime}$, we additionally obtain
$w_{k}\leq-(ns-1)W-1$. Rearranging the resulting inequality $-(ns-1)W-1\geq-
kW$ yields $kW\geq(ns-1)W+1$.

In order to obtain a lower bound for $k$, we briefly have to argue that $W>0$
holds true. First, we obtain $W\geq 0$ by definition of $W$. Furthermore, if
$W=0$ then we obtain $w(\pi)=0$, which contradicts $w(\pi)\leq-(ns-1)W-1=-1$.
Hence, we indeed have $W>0$, which yields $k>(ns-1)$ via the above inequality.
In particular, this implies that there exist at least $ns+1$ positions at
which the accumulated weight of the infix so far attains a new minimum, since
we start counting the number of positions at zero.

Due to the pigeon-hole-principle, we obtain that there exist indices $\ell$,
$\ell^{\prime}$ with $0\leq\ell<\ell^{\prime}\leq k$ such that
$v_{j_{\ell}}=v_{j_{\ell^{\prime}}}$ and such that
$\mathrm{upd}^{+}(v_{0}\cdots v_{j_{\ell}})=\mathrm{upd}^{+}(v_{0}\cdots
v_{j_{\ell^{\prime}}})$. Thus, the play $v_{0}\cdots v_{j}\cdots
v_{j_{\ell}}{(v_{j_{\ell}+1}\cdots v_{j_{\ell^{\prime}}})}^{\omega}$ obtained
by repeating the loop between $v_{j_{\ell}}$ and $v_{j_{\ell^{\prime}}}$ ad
infinitum is consistent with the strategy $\sigma$ and violates the energy
condition. This, however, contradicts $\sigma$ being a winning strategy from
$v_{0}$ for Player $0$.

Moreover, Chatterjee and Doyen gave an upper bound on the complexity of
solving energy parity games, which was recently supplemented by Daviaud et al.
[DJL18] with an algorithm solving them in pseudo-quasi-polynomial time.

[[CD12, DJL18]] The following problem is in $\textsc{NP}\cap\textsc{co-NP}$
and can be solved in pseudo-quasi-polynomial time: “Given an energy parity
game $\mathcal{G}$ and a vertex $v$ in $\mathcal{G}$, does Player $0$ win
$\mathcal{G}$ from $v$?”

###  5.2. From Bounded Parity Games with Weights to Energy Parity Games

Let $\mathcal{G}=(\mathcal{A},\mathrm{BndWeightParity}(\Omega,w))$ be a
bounded parity game with weights with vertex set $V$. Without loss of
generality, we assume $\Omega(v)\geq 2$ for all $v\in V$. We construct, for
each vertex $v^{*}$ of $\mathcal{A}$, an energy parity game
$\mathcal{G}_{v^{*}}$ with the following property:

> Player $1$ wins $\mathcal{G}_{v^{*}}$ from some designated vertex induced by
> $v^{*}$ if and only if she is able to unbound the amplitude for the request
> of the initial vertex of the play when starting from $v^{*}$.

This construction is the technical core of the fixed-point algorithm that
solves bounded parity games with weights via solving energy parity games.

The main obstacle towards this is that, in the bounded parity game with
weights $\mathcal{G}$, Player $1$ may win by unbounding the amplitude for a
request from above or from below, while she can only win the energy parity
game $\mathcal{G}_{v^{*}}$ by unbounding the costs from below. We model this
in $\mathcal{G}_{v^{*}}$ by constructing two copies of $\mathcal{A}$. In one
of these copies the edge weights are copied from $\mathcal{G}$, while they are
inverted in the other copy. We allow Player $1$ to switch between these copies
arbitrarily. To compensate for Player $1$’s power to switch, Player $0$ can
increase the energy level in the resulting energy parity game during each
switch.

First, we define the set of polarities $P=\\{+,-\\}$ as well as
$\overline{+}={-}$ and $\overline{-}={+}$. Given a vertex $v^{*}$ of
$\mathcal{A}$, define the “polarized” arena
$\mathcal{A}_{v^{*}}=(V^{\prime},V_{0}^{\prime},V_{1}^{\prime},E^{\prime})$ of
$\mathcal{A}=(V,V_{0},V_{1},E)$ with

  * •

$V^{\prime}=(V\times P)\cup(E\times P\times\\{0,1\\})$,

  * •

$V_{i}^{\prime}=(V_{i}\times P)\cup(E\times P\times\\{i\\})$ for
$i\in\\{0,1\\}$, and

  * •

$E^{\prime}$ contains the following edges for every edge $e=(v,v^{\prime})\in
E$ with $\Omega(v)\notin\mathrm{Ans}({\Omega(v^{*})})$ and every polarity
$p\in P$:

    * –

$((v,p),(e,p,1))$: The player whose turn it is at $v$ picks a successor
$v^{\prime}$. The edge $e=(v,v^{\prime})$ is stored as well as the polarity
$p$.

    * –

$((e,p,1),(v^{\prime},p))$: Then, Player $1$ can either keep the polarity $p$
unchanged and execute the move to $v^{\prime}$, or

    * –

$((e,p,1),(e,p,0))$: she decides to change the polarity, and another auxiliary
vertex is reached.

    * –

$((e,p,0),(e,p,0))$: If the polarity is to be changed, then Player $0$ is able
to use a self-loop to increase the energy level (see below), before

    * –

$((e,p,0),(v^{\prime},\overline{p}))$: he can eventually complete the polarity
switch by moving to $v^{\prime}$.

  * •

Furthermore, for every vertex $v$ with
$\Omega(v)\in\mathrm{Ans}({\Omega(v^{*})})$ and every polarity $p\in P$,
$E^{\prime}$ contains the self-loop $((v,p),(v,p))$.222This definition
introduces some terminal vertices, i.e., those of the form
$((v,v^{\prime}),p,i)$ with $\Omega(v)\in\mathrm{Ans}({\Omega(v^{*})})$.
However, these vertices also have no incoming edges. Hence, to simplify the
definition, we just ignore them.

Thus, a play in $\mathcal{A}_{v^{*}}$ simulates a play in $\mathcal{A}$,
unless Player $0$ stops the simulation by using the self-loop at a vertex of
the form $(e,p,0)$ ad infinitum, and unless an answer to $\Omega(v^{*})$ is
reached. We define the coloring and the weighting for $\mathcal{A}_{v^{*}}$ so
that Player $0$ loses in the former case and wins in the latter case.
Furthermore, the coloring is defined so that all simulating plays that are not
stopped have the same color sequence as the simulated play (save for
irrelevant colors on the auxiliary vertices in $E\times P\times\\{0,1\\}$).
Hence, we define

$\Omega_{v^{*}}(v)=\begin{cases}\Omega(v^{\prime})&\text{if
}v=(v^{\prime},p)\text{ with
}v^{\prime}\notin\mathrm{Ans}({\Omega(v^{*})})\enspace,\\\ 0&\text{if
}v=(v^{\prime},p)\text{ with
}v^{\prime}\in\mathrm{Ans}({\Omega(v^{*})})\enspace,\\\
1&\text{otherwise}\enspace.\end{cases}$

As desired, due to our assumption that $\Omega(v)\geq 2$ for all $v\in V$, the
vertices from $E\times P\times\\{0,1\\}$ do not influence the maximal color
visited infinitely often during a play, unless Player $0$ opts to remain in
some $(e,p,0)$ ad infinitum (and thereby violates the parity condition) or an
answer to the color of $v^{*}$ is reached (and thereby satisfies the parity
condition).

Moreover, recall that our aim is to allow Player $1$ to choose the polarity of
edges by switching between the two copies of $\mathcal{A}$ occurring in
$\mathcal{A}_{v^{*}}$. Intuitively, Player $1$ should opt for positive
polarity in order to unbound the costs incurred by the request posed by
$v^{*}$ from above, while she should opt for negative polarity in order to
unbound these costs from below. Since it is, broadly speaking, beneficial for
Player $1$ to move along edges of negative weight in an energy parity game, we
negate the weights of edges in the copy of $\mathcal{A}$ with positive
polarity. Thus, we define

$w_{v^{*}}(e)=\begin{cases}-w(v,v^{\prime})&\text{if
}e=((v,+),((v,v^{\prime}),+,1))\enspace,\\\ w(v,v^{\prime})&\text{if
}e=((v,-),((v,v^{\prime}),-,1))\enspace,\\\ 1&\text{if
}e=((e,p,0),(e,p,0))\enspace,\\\ 0&\text{otherwise}\enspace.\end{cases}$

This definition implies that the self-loops at vertices of the form $(v,p)$
with $\Omega(v)\in\mathrm{Ans}({\Omega(v^{*})})$ have weight zero. Combined
with the fact that these vertices have color zero, this allows Player $0$ to
win $\mathcal{G}_{v^{*}}$ by reaching such a vertex. Intuitively, answering
the request posed at $v^{*}$ is beneficial for Player $0$. In particular, if
$\Omega(v^{*})$ is even, then Player $0$ wins $\mathcal{G}_{v^{*}}$ trivially
from $(v^{*},p)$, as we then have
$\Omega(v^{*})\in\mathrm{Ans}({\Omega(v^{*})})$.

Finally, define the energy parity game
$\mathcal{G}_{v^{*}}=(\mathcal{A}_{v^{*}},\Omega_{v^{*}},w_{v^{*}})$. In the
following, we are only interested in plays starting in vertex $(v^{*},+)$ in
$\mathcal{G}_{v^{*}}$.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$\nicefrac{{v_{0}}}{{5}}$$\nicefrac{{v_{1}}}{{4}}$$\nicefrac{{v_{2}}}{{4}}$$\nicefrac{{v_{3}}}{{6}}$$0$$0$$+1$$0$$-1$$0$$0$$\nicefrac{{v_{0},+}}{{5}}$$\nicefrac{{v_{1},+}}{{4}}$$\nicefrac{{v_{2},+}}{{4}}$$\nicefrac{{v_{3},+}}{{0}}$$\nicefrac{{v_{0},-}}{{5}}$$\nicefrac{{v_{1},-}}{{4}}$$\nicefrac{{v_{2},-}}{{4}}$$\nicefrac{{v_{3},-}}{{0}}$+1+1+1+1+1+1+1+1-1+1+1+1+1+1-1+1
Figure 3. A bounded parity game with weights $\mathcal{G}$ (left) and the
associated energy parity game $\mathcal{G}_{v_{0}}$ (right). The unnamed
vertices of Player $1$ (Player $0$) are of the form $((v,v^{\prime}),p,1)$ (of
the form $((v,v^{\prime}),p,0)$) when between the vertices $(v,p)$ and
$(v^{\prime},p^{\prime})$. All missing edge weights in $\mathcal{G}_{v_{0}}$
are $0$.

Consider the bounded parity game with weights depicted on the left hand side
of Figure 3 and the associated energy parity game $\mathcal{G}_{v_{0}}$ on the
right side. First, let us note that all other $\mathcal{G}_{v}$ for $v\neq
v_{0}$ are trivial in that they all consist of a single vertex (reachable from
$(v,+)$), which has even color with a self-loop of weight zero. Hence, Player
$0$ wins each of these games from $(v,+)$.

Player $1$ wins $\mathcal{G}$ from $v_{0}$, where a request for color $5$ is
opened, which is then kept unanswered with infinite cost by using the self-
loop at $v_{1}$ or $v_{2}$ ad infinitum, depending on which successor Player
$0$ picks.

We show that Player $1$ wins $\mathcal{G}_{v_{0}}$ from $(v_{0},+)$: the
outgoing edges of $(v_{0},+)$ correspond to picking the successor $v_{1}$ or
$v_{2}$ as in $\mathcal{G}$. Before this is executed, however, Player $1$ gets
to pick the polarity of the successor: she should pick $+$ for $v_{1}$ and $-$
for $v_{2}$. Now, Player $0$ may use the self-loop at her “tiny” vertices ad
infinitum. These vertices have color one, i.e., Player $1$ wins the resulting
play. Otherwise, we reach the vertex $(v_{1},+)$ or $(v_{2},-)$. From both
vertices, Player $1$ can enforce a loop of negative weight, which allows him
to win by violating the energy condition.

Note that the winning strategy for Player $1$ for $\mathcal{G}$ from $v_{0}$
is very similar to that for her for $\mathcal{G}_{v_{0}}$ from $(v_{0},+)$. We
show that one direction holds in general: A winning strategy for Player $0$
for $\mathcal{G}_{v}$ from $(v,+)$ is “essentially” one for him in
$\mathcal{G}$ from $v$.

The other direction does, in general, not hold. This can be seen by extending
$\mathcal{G}$ in Figure 3 by a vertex $v_{-1}$ of color $3$ with a single
outgoing edge to $v_{0}$ (with arbitrary weight) and no incoming edges. We
call this extended bounded parity game with weights $\mathcal{G}^{\prime}$. In
the resulting energy parity game $\mathcal{G}^{\prime}_{v_{-1}}$, vertices of
the form $(v_{i},p)$ with $i\in\\{1,2\\}$ in $\mathcal{G}_{v_{-1}}$ are
winning sinks for Player $0$. Also, Player $0$ has a strategy to ensure that
such a sink is reached when starting in $(v_{-1},+)$. Hence, he wins
$\mathcal{G}^{\prime}_{v_{-1}}$ from $(v_{-1},+)$. However, he does not win
the extended bounded parity game with weights $\mathcal{G}^{\prime}$ from
$v_{-1}$, as Player $1$ can still win by remaining in either $v_{1}$ or
$v_{2}$ ad infinitum. By doing this, she keeps the request of color $5$, which
is opened when visiting $v_{0}$ at the second position of every play starting
in $v_{-1}$, unanswered with infinite cost.

The reason for the other direction failing is the special role the initial
request of the vertex $v$ inducing $\mathcal{G}_{v}$ plays in the
construction: It is the request Player $1$ aims to keep unanswered with
infinite cost. To overcome this and to complete our construction, we show a
statement reminiscent of Lemma 1: If Player $0$ wins $\mathcal{G}_{v}$ from
$(v,+)$ for every $v$, then she also wins $\mathcal{G}$ from every vertex.
With this relation at hand, one can again construct a fixed-point algorithm
solving bounded parity games with weights using an oracle for solving energy
parity games that is very similar to Algorithm 1.

Formally, we have the following lemma, which forms the technical core of our
algorithm that solves bounded parity games with weights by solving energy
parity games.

######  Lemma 4.

Let $\mathcal{G}$ be a bounded parity game with weights with vertex set $V$.

  1. (1)

Let $v^{*}\in V$. If Player $1$ wins $\mathcal{G}_{v^{*}}$ from $(v^{*},+)$,
then $v^{*}\in\mathcal{W}_{1}(\mathcal{G})$.

  2. (2)

If Player $0$ wins $\mathcal{G}_{v^{*}}$ from $(v^{*},+)$ for all $v^{*}\in
V$, then $\mathcal{W}_{1}(\mathcal{G})=\emptyset$.

Before we prove this lemma, we first note that it is the main building block
for the algorithm that solves bounded parity games with weights by repeatedly
solving energy parity games, which is very similar to Algorithm 1. Indeed, we
just swap the roles of the players: We compute $1$-attractors instead of
$0$-attractors and we change the definition of $X_{k}$. Hence, we obtain
Algorithm 2.

0: Bounded parity game with weights $\mathcal{G}$ with arena $\mathcal{A}$,
coloring $\Omega$ and weighting $w$

1: $k=0$; $W_{1}^{k}=\emptyset$; $\mathcal{A}_{k}=\mathcal{A}$

2: repeat

3: $k=k+1$

4: $X_{k}=\\{v^{*}\mid\text{Player~{}$1$ wins the energy parity
game~{}$({(\mathcal{A}_{k-1})}_{v^{*}},\Omega_{v^{*}},w_{v^{*}})$ from
$(v^{*},+)$}\\}$

5: $W_{1}^{k}=W_{1}^{k-1}\cup\mathrm{Attr}_{1}^{\mathcal{A}_{k-1}}(X_{k})$

6:
$\mathcal{A}_{k}=\mathcal{A}_{k-1}\setminus\mathrm{Attr}_{1}^{\mathcal{A}_{k-1}}(X_{k})$

7: until $X_{k}=\emptyset$

8: return $W_{1}^{k}$

Algorithm 2 A fixed-point algorithm computing
$\mathcal{W}_{1}(\mathcal{A},\mathrm{BndWeightParity}(\Omega,w))$.

Algorithm 2 terminates after solving at most a quadratic number of energy
parity games of polynomial size. Furthermore, the proof of correctness is
analogous to the one for Algorithm 1, relying on Lemma 4. We only need two
further properties: the $1$-extendability of
$\mathrm{BndWeightParity}(\Omega,w)$, and an assertion that
$\mathrm{Attr}_{1}^{\mathcal{A}_{k-1}}(X_{k})$ is a trap for Player $0$ in
$\mathcal{A}_{k-1}$. Both are easy to verify.

After plugging Algorithm 2 into Algorithm 1, Proposition 5.1 yields our main
theorem, settling the complexity of solving parity games with weights.

######  Theorem 5.

The following problem is in $\textsc{NP}\cap\textsc{co-NP}$ and can be solved
in pseudo-quasi-polynomial time:

> “Given a parity game with weights $\mathcal{G}$ and a vertex $v$ in
> $\mathcal{G}$, does Player $0$ win $\mathcal{G}$ from $v$?”

It remains to prove Lemma 4. We do so in the following section.

###  5.3. Proof of Lemma 4

We prove the two assertions of Lemma 4 separately from each other: We first
show Item 1 of Lemma 4, before continuing to show Item 2. In order to prepare
for this, however, we first introduce some notation. Let $v^{*}\in V$ and
consider $\mathcal{G}_{v^{*}}$. We distinguish three types of plays in
$\mathcal{G}_{v^{*}}$:

Type -1:

Plays that have a suffix ${(e,p,0)}^{\omega}$ for some $e\in E$ and some $p\in
P$.

Type -0:

Plays that visit infinitely many vertices from both $V\times P$ and $E\times
P\times\\{0,1\\}$.

Type -1:

Plays that have a suffix ${(v,p)}^{\omega}$. Note that this implies
$\Omega(v)\in\mathrm{Ans}({\Omega(v^{*})})$.

Clearly, plays of Type $-1$ are losing for Player $0$ due to the coloring of
$\mathcal{G}^{\prime}_{v^{*}}$ labeling vertices of the form $(e,p,0)$ with
the odd color one. Dually, plays of Type $1$ are losing for Player $1$, since
$\Omega(v)\in\mathrm{Ans}({\Omega(v^{*})})$ implies that $(v,p)$ carries color
zero and its only outgoing edge is a self-loop of weight $0$. We formalize
this observation in the following remark.

######  Remark 6.

Let $\rho^{\prime}$ be a play in $\mathcal{G}_{v^{*}}$ that starts in
$(v^{*},p)$.

  1. (1)

If $\rho^{\prime}$ is consistent with a winning strategy for Player $0$ from
$(v^{*},p)$, then $\rho^{\prime}$ is not a play of Type $-1$.

  2. (2)

If $\rho^{\prime}$ is consistent with a winning strategy for Player $1$ from
$(v^{*},p)$, then $\rho^{\prime}$ is not a play of Type $1$.

In order to remove the added vertices of the form $E\times P\times\\{0,1\\}$
from plays in $\mathcal{G}_{v^{*}}$, we define the homomorphism
$\text{unpol}\colon{(V^{\prime})}^{*}\cup{(V^{\prime})}^{\omega}\rightarrow
V^{*}\cup V^{\omega}$ induced by $\text{unpol}(v,p)=v$ and
$\text{unpol}(e,p,i)=\varepsilon$ for $v\in V$, $e\in E$, $p\in P$, and
$i\in\\{0,1\\}$. Let
$\rho^{\prime}\in{(V^{\prime})}^{*}\cup{(V^{\prime})}^{\omega}$. We call
$\text{unpol}(\rho^{\prime})$ the unpolarization of $\rho^{\prime}$.

######  Remark 7.

Let $\rho^{\prime}$ be a play of Type $0$ in some $\mathcal{G}_{v^{*}}$. We
have $\rho^{\prime}\in\mathrm{Parity}(\Omega_{v^{*}})$ if and only if
$\text{unpol}(\rho^{\prime})\in\mathrm{Parity}(\Omega)$.

####  5.3.1. Proof of Item 1 of Lemma 4

Recall that we need to show that Player $1$ wins the bounded parity game with
weights $\mathcal{G}$ from $v^{*}$ if she wins the energy-parity game
$\mathcal{G}_{v^{*}}$ from $(v^{*},+)$. Thus, let $\tau_{v^{*}}$ be a winning
strategy for Player $1$ from $(v^{*},+)$ in $\mathcal{G}_{v^{*}}$. We define a
winning strategy $\tau$ for her from $v^{*}$ in $\mathcal{G}$ such that $\tau$
mimics the moves made by $\tau_{v^{*}}$. To this end, $\tau$ keeps track of a
play prefix $\mathcal{G}_{v^{*}}$. Formally, we define $\tau$ together with a
simulation function $h$ that satisfies the following invariant:

> If $\pi$ is a nonempty play prefix in $\mathcal{A}$ that starts in $v^{*}$,
> is consistent with $\tau$, and ends in some $v$, then $h(\pi)$ is a play
> prefix in $\mathcal{A}_{v^{*}}$ that starts in $(v^{*},+)$, is consistent
> with $\tau_{v^{*}}$, and ends in some $(v,p)$. Furthermore,
> $\text{unpol}(h(\pi))=\pi$.

Recall that, if $h$ has the properties described above, then, due to the
structure of $\mathcal{A}_{v^{*}}$, for each $\pi$, given $h(\pi)$, the
strategy $\tau_{v^{*}}$ prescribes a move to some vertex
$((v,v^{\prime}),p,1)$, where $(v,v^{\prime})\in E$. We can mimic this choice
by moving to $v^{\prime}$ in $\mathcal{G}$.

We now define $h$ and $\tau$ formally and begin with $h(v^{*})=(v^{*},+)$,
which clearly satisfies the invariant. Now let $\pi=v_{0}\cdots v_{j}$ be some
nonempty play prefix in $\mathcal{A}$ beginning in $v^{*}$ and consistent with
$\tau$ such that $h(\pi)$ is defined. Due to the invariant, $h(\pi)$ ends in
$(v_{j},p_{j})$ for some $p_{j}\in P$.

If $v_{j}\in V_{1}$, there is a unique vertex $v_{j+1}$ such that
$h(\pi)\cdot((v_{j},v_{j+1}),p_{j},1)$ is consistent with $\tau_{v^{*}}$. We
define $\tau(\pi)=v_{j+1}$. Such a $v_{j+1}$ exists, because $(v_{j},p_{j})$,
the last vertex of $h(\pi)$, satisfies
$\Omega(v_{j})\notin\mathrm{Ans}({\Omega(v^{*})})$ due to the invariant, Item
2 of Remark 6, and because the answering vertices are sinks. If, however,
$v_{j}\in V_{0}$, then let $v_{j+1}$ be an arbitrary successor of $v_{j}$ in
$\mathcal{A}$. In either case, it remains to define $h(\pi\cdot v_{j+1})$.

Since we want to simulate the move from $v_{j}$ to $v_{j+1}$ in $h(\pi\cdot
v_{j+1})$, we first move from $(v_{j},p_{j})$ to $((v_{j},v_{j+1}),p_{j},1)$.
Moreover, in order to satisfy the invariant, we aim to simulate the play
prefix $\pi\cdot v_{j+1}$ such that $h(\pi\cdot v_{j+1})$ is consistent with
$\tau_{v^{*}}$. This strategy may prescribe for Player $1$ to either preserve
the polarity $p_{j}$, or to switch it during the simulated move from $v_{j}$
to $v_{j+1}$.

In the former case, i.e., if
$\tau_{v^{*}}(h(\pi)\cdot((v_{j},v_{j+1}),p_{j},1))=(v_{j+1},p_{j})$, we
define

$h(\pi\cdot
v_{j+1})=h(\pi)\cdot((v_{j},v_{j+1}),p_{j},1)\cdot(v_{j+1},p_{j})\enspace.$

In the latter case, Player $0$ gets an opportunity to recharge the energy by
taking the self-loop of the vertex $((v_{j},v_{j+1}),p_{j},0)$ finitely often.
We opt to let her recover the energy lost so far in the play prefix, i.e., we
pick $c_{j}=\max\\{0,-w(h(\pi)\cdot((v_{j},v_{j+1}),p_{j},1))\\}$ and define

$h(\pi\cdot
v_{j+1})=h(\pi)\cdot((v_{j},v_{j+1}),p_{j},1)\cdot{((v_{j},v_{j+1}),p_{j},0)}^{c_{j}+1}\cdot(v_{j+1},\overline{p_{j}})$

in this case. Since $h(\pi\cdot v_{j+1})$ is consistent with $\tau_{v^{*}}$ in
either case, we satisfy the invariant in either case. This completes the
definition of $\tau$ and $h$.

It remains to show that $\tau$ is indeed winning from $v^{*}$ in
$\mathcal{G}$. To this end, let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play in
$\mathcal{A}$ that starts in $v^{*}$ and that is consistent with $\tau$. We
need to show $\rho\notin\mathrm{BndWeightParity}(\Omega,w)$.

Note that $h(v_{0}\cdots v_{j})$ is a strict prefix of $h(v_{0}\cdots vj+1)$
for every $j$. As each such $h(v_{0}\cdots v_{j})$ is a play prefix in
$\mathcal{A}_{v^{*}}$, there is a unique infinite play $\rho^{\prime}$ in
$\mathcal{A}_{v^{*}}$ such that each $h(v_{0}\cdots v_{j})$ is a prefix of
$\rho^{\prime}$, i.e, $\rho^{\prime}$ is the limit of the $h(v_{0}\cdots
v_{j})$ for increasing prefixes $v_{0}\cdots v_{j}$ of $\rho$. Due to the
invariant, $\rho^{\prime}$ starts in $(v^{*},+)$ and is consistent with
$\tau_{v^{*}}$. Moreover, due to the construction of $h$, we obtain
$\text{unpol}(\rho^{\prime})=\rho$. Finally, we have that $\rho^{\prime}$ is a
play of Type $0$ in $\mathcal{G}_{v^{*}}$. Hence, due to Remark 7, $\rho$
satisfies the parity condition if and only if $\rho^{\prime}$ satisfies the
parity condition.

As the play $\rho^{\prime}$ is consistent with the winning strategy
$\tau_{v^{*}}$ for Player $1$, we have
$\rho^{\prime}\notin\mathrm{EnergyParity}(\Omega_{v^{*}},w_{v^{*}})$, i.e.,
$\rho^{\prime}$ either violates the parity condition or the energy condition.
Hence, as argued above, if $\rho^{\prime}$ violates the parity condition, then
so does $\rho$, i.e., $\rho$ is indeed winning for Player $1$.

Now assume that $\rho^{\prime}$ violates the energy condition. Due to the
structure of $\mathcal{A}_{v^{*}}$ and the construction of $h$ we have

$\rho^{\prime}=\Pi_{j=0,1,2,\dots}(v_{j},p_{j})\cdot((v_{j},v_{j+1}),p_{j},1)\cdot{((v_{j},v_{j+1}),p_{j},0)}^{m_{j}}$

for some $m_{j}\in\mathbb{N}$. Since $\rho^{\prime}$ violates the energy
condition, we have
$\inf_{j\in\mathbb{N}}w((v_{0},p_{0})\cdots(v_{j},p_{j})\cdot((v_{j},v_{j+1}),p_{j},1))=-\infty$.
The restriction to play prefixes of this form suffices due to the structure of
$\mathcal{A}_{v^{*}}$ and, in turn, the structure of $\rho^{\prime}$.
Moreover, since Player $1$ wins $\mathcal{G}_{v^{*}}$ from $(v^{*},+)$, the
initial vertices $v^{*}$ and $(v^{*},+)$ of $\rho$ and $\rho^{\prime}$,
respectively, have the same odd color. Also, as $\rho^{\prime}$ is a play of
Type $0$, the request for the color $\Omega(v^{*})$ is never answered in
$\rho$ or $\rho^{\prime}$. We show that the request for $\Omega(v^{*})$ in
$\rho$ is unanswered with infinite cost, which concludes the proof.

To this end, we split $\rho^{\prime}$ into infixes of constant polarity. Given
a vertex $v=(v^{\prime},p)$ or $v=((v^{\prime},v^{\prime\prime}),p,i)$, we
call $p$ the polarity of $v$. Let
$\rho^{\prime}=\mu^{\prime}_{0}\mu^{\prime}_{1}\mu^{\prime}_{2}\cdots$, where
each $\mu^{\prime}_{j}$ is a maximal finite (or infinite) infix (or suffix) of
$\rho^{\prime}$, such that all vertices in $\mu^{\prime}_{j}$ have the same
polarity. We call an infix $\mu^{\prime}_{j}$ of $\rho^{\prime}$ an equi-
polarity infix (EPI) of $\rho^{\prime}$.

Since the polarity remains constant throughout each $\mu_{j}^{\prime}$, Player
$0$ only resets the energy via repeatedly traversing a self-loop of a vertex
in $\mathcal{A}_{v^{*}}$ at the last vertex visited in $\mu^{\prime}_{j}$, if
at all. Hence, the energy levels attained during $\mu^{\prime}_{j}$ and
$\text{unpol}(\mu_{j}^{\prime})$ are closely related.

######  Remark 8.

Let $\mu^{\prime}$ be an EPI beginning in $(v_{j},p_{j})$ and let
$\mu=\text{unpol}(\mu^{\prime})=v_{j}v_{j+1}v_{j+2}\cdots$. For each
$j^{\prime}$ with $j\leq j^{\prime}<j+|\mu|$, we have $|w(v_{j}\cdots
v_{j^{\prime}})|=|w((v_{j},p_{j})\cdots(v_{j^{\prime}},p_{j^{\prime}}))|$.

In particular, Remark 8, the structure of $\mathcal{A}_{v^{*}}$, and the
definition of $h$ imply that we have
$\mathrm{Ampl}(\text{unpol}(\mu^{\prime}))=\mathrm{Ampl}(\mu^{\prime})$ for
all EPIs $\mu^{\prime}$ of $\rho^{\prime}$. Thus, if there exist only finitely
many EPIs of $\rho^{\prime}$, let $\mu^{\prime}$ be the infinite final EPI of
$\rho^{\prime}$, let $\mu=\text{unpol}(\mu^{\prime})$, and note that, due to
$\mathrm{Ampl}(\rho^{\prime})=\infty$, we have
$\mathrm{Ampl}(\mu^{\prime})=\infty$. Due to Remark 8, we obtain
$\mathrm{Ampl}(\mu)=\infty$, which implies that the request posed at the
initial position of $\rho$ is unanswered with infinite cost due to the
reasoning above, as $\mu$ is a suffix of $\rho$.

If, however, there exist infinitely many EPIs of $\rho^{\prime}$, assume
towards a contradiction that the cost of answering the request posed at the
initial position of $\rho$ is finite. By construction of $\rho^{\prime}$, the
energy level is nonnegative at the end of each EPI. Since $\rho^{\prime}$
violates the energy condition, for each bound $b\in\mathbb{N}$ there exists an
EPI $\mu^{\prime}$ of $\rho^{\prime}$ with a prefix of weight strictly smaller
than $-b$. We obtain $\mathrm{Ampl}(\text{unpol}(\mu^{\prime}))>b$ via Remark
8. This contradicts the cost of answering the request posed at the initial
position of $\rho$ being bounded and concludes the proof of Item 1 of Lemma 4.

####  5.3.2. Proof of Item 2 of Lemma 4

To prove Item 2 of Lemma 4, we show that Player $0$ wins the bounded parity
game with weights $\mathcal{G}$ from every vertex, if he wins each energy-
parity game $\mathcal{G}_{v^{*}}$ from $(v^{*},+)$. To this end, we construct
a strategy $\sigma$ for Player $0$ in $\mathcal{G}$ that is winning for him
from each vertex $v\in V$. As winning regions are disjoint, this implies the
desired result.

For each energy parity game
$\mathcal{G}_{v}=(\mathcal{A}_{v},\Omega_{v},w_{v})$ we have
$n^{\prime}=|\mathcal{A}_{v}|\in\mathcal{O}(|\mathcal{A}|^{2})$, we have
$d^{\prime}=|\Omega_{v}(V^{\prime})|=|\Omega(V)|+2$, and we have
$W^{\prime}=\max(w(E^{\prime}))=\max(w(E)\cup\\{1\\})$, where $E$ and
$E^{\prime}$ are the sets of edges in $\mathcal{A}$ and the $\mathcal{A}_{v}$,
respectively. Note that the values $n^{\prime}$, $d^{\prime}$, and
$W^{\prime}$ of $\mathcal{G}_{v}$ are independent of the vertex $v$, which
explains our notation. Due to the assumption of the statement and Proposition
5.1, for each $v\in V$, there exists a finite-state strategy $\sigma_{v}$ with
at most $n^{\prime}d^{\prime}W^{\prime}$ states that is winning for Player $0$
from $(v,+)$ in $\mathcal{G}_{v}$.

We construct the winning strategy $\sigma$ for Player $0$ in $\mathcal{G}$ by
“stitching together” the individual $\sigma_{v}$. To this end, given a play
prefix, we identify the request which should be answered most urgently. Say
this request was opened by visiting vertex $v$. The strategy $\sigma$ then
mimics the moves made by $\sigma_{v}$ when starting in $(v,+)$. Once the
request for $\Omega(v)$ is answered, $\sigma$ makes arbitrary moves until a
new request is opened.

Formally, given a play prefix $\pi=v_{0}\cdots v_{j}$, we say that a request
for color $c$ is open in $\pi$ if there exists a position $j^{\prime}$ with
$0\leq j^{\prime}\leq j$ such that $\Omega(v_{j^{\prime}})=c$ and, for all
positions $j^{\prime\prime}$ with $j^{\prime}\leq j^{\prime\prime}\leq j$, we
have
$\Omega(v_{j^{\prime\prime}})\notin\mathrm{Ans}({\Omega(v_{j^{\prime}})})$.
Clearly there is never an open request for an even color.

Due to monotonicity, answering an open request of color $c$ also answers all
smaller open requests. Hence, the most relevant request, i.e., the largest
color with an open request, is of special interest during a play. As alluded
to above, it is this color that guides the strategy we are about to construct.
To define it formally, we need to introduce some notation to refer to the
position where the most relevant request has been opened.

If there is no open request in $\pi$, the position of the most relevant
request is undefined and we write $\text{posMRR}(\pi)=\bot$. Otherwise, let
$c$ be the maximal color for which there is an open request in $\pi$. We
define $\text{posMRR}(\pi)$ as the smallest position $j^{\prime}$, such that
the request for color $c$ is open in all prefixes of $\pi$ of length greater
than $j^{\prime}$.

As an example, consider the play prefix shown in Figure 4 using the notation
$\nicefrac{{v}}{{\Omega(v)}}$. We mark a position $j$ with solid background if
$\text{posMRR}(v_{0}\cdots v_{j})=j$ and with dashed background if
$\text{posMRR}(v_{0}\cdots v_{j})=\bot$. Otherwise, i.e., if
$\bot\neq\text{posMRR}(v_{0}\cdots v_{j})<j$, we leave $j$ unmarked. For those
positions, $\text{posMRR}(v_{0}\cdots v_{j})$ is equal to the largest (i.e.,
last visited) earlier position marked in solid background. We furthermore
denote the value of $\text{posMRR}(v_{0}\cdots v_{j})$ by an arrow going from
position $j$ to position $\text{posMRR}(v_{0}\cdots v_{j})$.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$\nicefrac{{v_{0}}}{{0}}$$\nicefrac{{v_{1}}}{{0}}$$\nicefrac{{v_{2}}}{{2}}$$\nicefrac{{v_{3}}}{{1}}$$\nicefrac{{v_{4}}}{{0}}$$\nicefrac{{v_{5}}}{{1}}$$\nicefrac{{v_{6}}}{{3}}$$\nicefrac{{v_{7}}}{{1}}$$\nicefrac{{v_{8}}}{{4}}$$\nicefrac{{v_{9}}}{{0}}$$\nicefrac{{v_{10}}}{{2}}$$\nicefrac{{v_{11}}}{{1}}$$\nicefrac{{v_{12}}}{{1}}$$\cdots$$\mu_{0}$$\mu_{1}$$\mu_{2}$$\mu_{3}$$\mu_{4}$$\mu_{5}$$\mu_{6}$$\mu_{7}$$\mu_{7}$
Figure 4. A play $\rho$, its induced color sequence, its most relevant
requests, and the ESIs of $\rho$.

In order to leverage the moves made by the strategies for the
$\mathcal{G}_{v}$ in $\mathcal{G}$, we need to simulate play prefixes in the
latter game in the former ones. To this end, we again define $\sigma$ together
with a simulation function $h$. This function $h$ maps a play prefix
consistent with $\sigma$ to a sequence of vertices from $V^{\prime}$ (not
necessarily a play prefix) such that we are able to leverage the choices made
by the $\sigma_{v}$ in order to define $\sigma$. Our aim is to define $h$ such
that it satisfies the following invariant:

> Let $\pi=v_{0}\cdots v_{j}$ be a play prefix in $\mathcal{A}$ consistent
> with $\sigma$. Then $h(\pi)$ ends in some $(v_{j},p_{j})$. Moreover, if
> $\text{posMRR}(\pi)=j^{\prime}\neq\bot$, then $h(\pi)$ has a (unique) suffix
> $\pi^{\prime}=(v_{j^{\prime}},+)(v_{j^{\prime}+1},p_{j^{\prime}+1})\cdots(v_{j},p_{j})$
> that is consistent with $\sigma_{v_{j^{\prime}}}$ and satisfies
> $\text{unpol}(\pi^{\prime})=v_{j^{\prime}}\cdots v_{j}$.

We define $h$ and $\sigma$ inductively and begin with $h(v)=(v,+)$ for each
$v\in V$, which clearly satisfies the invariant. Now let $\pi=v_{0}\cdots
v_{j}$ be a nonempty play prefix in $\mathcal{A}$ and consistent with $\sigma$
such that $h(\pi)$ is defined. We again first determine a successor of
$v_{j}$, defining $\sigma(\pi)$ along the way if $v_{j}$ is a vertex of Player
$0$.

If $v_{j}\in V_{1}$, let $v_{j+1}$ be an arbitrary successor of $v_{j}$ in
$\mathcal{A}$, as Player $1$ may move to any successor of $v_{j}$. If,
however, $v_{j}\in V_{0}$, we distinguish two cases based on whether or not
$\text{posMRR}(\pi)$ is defined. If $\text{posMRR}(\pi)=\bot$, again let
$v_{j+1}$ be an arbitrary successor of $v_{j}$. This reflects the fact that
Player $0$ may move to an arbitrary successor if there is no open request. If,
however, $\text{posMRR}(\pi)=j^{\prime}\neq\bot$, then the invariant of $h$
yields a suffix $(v_{j^{\prime}},+)\cdots(v_{j},p_{j})$ of $h(\pi)$ that is
consistent with $\sigma_{v_{j^{\prime}}}$. Let $v_{j+1}$ be the unique vertex
such that
$(v_{j^{\prime}},+)\cdots(v_{j},p_{j})\cdot((v_{j},v_{j+1}),p_{j},1)$ is
consistent with $\sigma_{v_{j^{\prime}}}$. Such a vertex $v_{j+1}$ exists,
because the request posed by visiting $v_{j^{\prime}}$ is open in $\pi$ due to
$\text{posMRR}(\pi)=j^{\prime}$ and since the color sequences induced by
$v_{j^{\prime}}\cdots v_{j}$ and $(v_{j^{\prime}},+)\cdots(v_{j},p_{j})$
coincide, save for the irrelevant intermediate vertices of colors zero and
one. Hence, $(v_{j},p_{j})$ is not an accepting sink in
$\mathcal{G}_{v_{j^{\prime}}}$. Since $v_{j}\in V_{0}$, the vertex $v_{j+1}$
is unique. In both cases, we define $\sigma(\pi)=v_{j+1}$. This concludes the
definition of $\sigma$.

It remains to define $h(\pi\cdot v_{j+1})$ such that it satisfies the above
invariant. To this end, we use one of two operations. Firstly, we define the
discontinuous extension of $h(\pi)$ with $v_{j+1}$ as

$h(\pi)\cdot(v_{j+1},+)\enspace.$

Secondly, we define a simulated extension of $h(\pi)$ such that we obtain
$h(\pi\cdot v_{j+1})$ by simulating the move from $v_{j}$ to $v_{j+1}$ in some
$\mathcal{G}_{v}$. Formally, we define the simulated extension of $h(\pi)$
with $v_{j+1}$ and charge $m$ as

$h(\pi)\cdot((v_{j},v_{j+1}),p_{j},1)\cdot{((v_{j},v_{j+1}),p_{j},0)}^{m}\cdot(v_{j+1},p_{j+1})\enspace,$

where $p_{j+1}=p_{j}$ if $m=0$ and $p_{j+1}=\overline{p_{j}}$ otherwise. This
ensures that the extension is a play infix in some $\mathcal{G}_{v}$.

In order to define $h(\pi\cdot v_{j+1})$ we again distinguish whether or not
$\text{posMRR}(\pi)$ is defined. If $\text{posMRR}(\pi)=\bot$, we define
$h(\pi\cdot v_{j+1})$ to be the discontinuous extension of $h(\pi)$ with
$v_{j+1}$. This clearly satisfies the first condition of the invariant.
Moreover, the second condition of the invariant is satisfied as well: If
$\text{posMRR}(\pi\cdot v_{j+1})=\bot$, this condition holds true vacuously.
Otherwise, we have $\text{posMRR}(\pi\cdot v_{j+1})=j+1$ and observe that the
suffix $(v_{j+1},+)$ of $h(\pi\cdot v_{j+1})$ satisfies the second condition
of the invariant.

If, however, $\text{posMRR}(\pi)\neq\bot$, then let
$\text{posMRR}(\pi)=j^{\prime}$. By definition of posMRR we have
$\text{posMRR}(\pi\cdot v_{j+1})\in\\{\bot,j^{\prime},j+1\\}$. We distinguish
two sub-cases and first define $h(\pi\cdot v_{j+1})$ for the case that
$\text{posMRR}(\pi\cdot v_{j+1})\in\\{\bot,j+1\\}$. In this case, the move to
$v_{j+1}$ either answers the most relevant request in $\pi$, or the request
posed by visiting $v_{j+1}$ is itself the most relevant request of $\pi\cdot
v_{j+1}$: We have $\text{posMRR}(\pi\cdot v_{j+1})=\bot$ in the former case
and $\text{posMRR}(\pi\cdot v_{j+1})=j+1$ in the latter one. In either case,
we define $h(\pi\cdot v_{j+1})$ to be the discontinuous extension of $h(\pi)$
with $v_{j+1}$ and observe that the first condition of the invariant holds
true. If $\text{posMRR}(\pi\cdot v_{j+1})=\bot$, the second condition of the
invariant holds true vacuously. If, however, $\text{posMRR}(\pi\cdot
v_{j+1})=j+1$, then the suffix $(v_{j+1},+)$ witnesses that the second
condition of the invariant holds true.

Now assume that the move to $v_{j+1}$ neither opens a new most relevant
request, nor answers the existing one, i.e., that we have
$\text{posMRR}(\pi\cdot v_{j+1})=j^{\prime}$. In this case, we extend the
suffix of $h(\pi)$ that is consistent with $\sigma_{v_{j^{\prime}}}$ by
simulating the move from $v_{j}$ to $v_{j+1}$. Recall that we picked the
vertex $v_{j+1}$ such that
$(v_{j^{\prime}},+)\cdots(v_{j},p_{j})\cdot((v_{j},v_{j+1}),p_{j},1)$ is
consistent with $\sigma_{v_{j^{\prime}}}$. As we can freely choose whether or
not Player $1$ switches the polarity in the simulation, we follow the
intuition stated during the construction of the polarized arena: Recall that
both players currently play “with respect to” the request for
$\Omega(v_{j^{\prime}})$ opened by visiting $v_{j^{\prime}}$. Hence, we opt to
let Player $1$ move to positive polarity if the cost of the request for
$\Omega(v_{j^{\prime}})$ so far is nonnegative, and let him move to negative
polarity otherwise. To this end, we use the sign function $\mathrm{Sgn}$,
which is defined as

$\mathrm{Sgn}(n)=\begin{cases}+&\text{if~{}$n\geq 0$}\enspace,\\\
-&\text{otherwise}\enspace.\end{cases}$

If $\mathrm{Sgn}(w(v_{j^{\prime}}\cdots v_{j+1}))=p_{j}$, we define
$h(\pi\cdot v_{j+1})$ to be the simulated extension of $h(\pi)$ with $v_{j+1}$
and charge $0$, thus implementing the intuition as described above. Otherwise,
i.e., if $\mathrm{Sgn}(w(v_{j^{\prime}}\cdots v_{j+1}))=\overline{p_{j}}$, let
$m>0$ such that
$(v_{j^{\prime}},+)\cdots(v_{j},p_{j})\cdot((v_{j},v_{j+1}),p_{j},1)\cdot{((v_{j},v_{j+1}),p_{j},1)}^{m}\cdot(v_{j+1},\overline{p_{j}})$
is consistent with $\sigma_{v_{j^{\prime}}}$. Such an $m$ exists, as otherwise
the play
$(v_{j^{\prime}},+)\cdots(v_{j},p_{j})\cdot((v_{j},v_{j+1}),p_{j},1)\cdot{((v_{j},v_{j+1}),p_{j},0)}^{\omega}$
of Type $-1$ that starts in $(v_{j^{\prime}},+)$ would be consistent with the
winning strategy $\sigma_{v_{j^{\prime}}}$ from $(v_{j^{\prime}},+)$ for
Player $0$, contradicting Item 1 of Remark 6. We define $h(\pi\cdot v_{j+1})$
to be the simulated extension of $h(\pi)$ with $v_{j+1}$ and charge $m$. Since
we have $\text{posMRR}(v_{0}\cdots v_{j+1})=j^{\prime}$ by assumption, either
definition of $h(\pi\cdot v_{j+1})$ satisfies the invariant. This completes
the definition of $h$.

It remains to show that the strategy $\sigma$ is indeed winning for Player $0$
from $v^{*}$. To this end, fix some play $\rho=v_{0}v_{1}v_{2}\cdots$
consistent with $\sigma$ starting in $v^{*}$. Further, let $\rho^{\prime}$ be
the limit of the $h(\pi)$ for increasing prefixes $\pi$ of $\rho$, i.e., the
unique infinite sequence with prefix $h(\pi)$ for every prefix $\pi$ of
$\rho$.

By the construction of $h$ and $\rho^{\prime}$ we obtain
$\text{unpol}(\rho^{\prime})=\rho$. Hence, $\rho^{\prime}$ is of the form
$(v_{0},p_{0})\cdots(v_{1},p_{1})\cdots(v_{2},p_{2})\cdots$. We call a
position $j$ of $\rho$ a discontinuity of $\rho$ if either $j=0$ or if
$h(v_{0}\cdots v_{j})$ is the discontinuous extension of $h(v_{0}\cdots
v_{j-1})$ by $v_{j}$.

Let $j$ and $j^{\prime}$ be adjacent discontinuities of $\rho$. We call the
infix $v_{j}\cdots v_{j^{\prime}-1}$ of $\rho$ an equi-strategic infix (ESI)
of $\rho$. Moreover, if there only exist finitely many discontinuities of
$\rho$, let $j^{*}$ be its final discontinuity. We call the suffix
$v_{j^{*}}v_{j^{*}+1}v_{j^{*}+2}\cdots$ of $\rho$ the terminal ESI of $\rho$.

######  Remark 9.

Let $\mu=v_{j}v_{j+1}v_{j+2}\cdots$ be an ESI of $\rho$.

  1. (1)

If $\mu$ is finite, then the infix $\mu^{\prime}$ of $\rho^{\prime}$ starting
at position $|h(v_{0}\cdots v_{j})|-1$ and ending at position $|h(v_{0}\cdots
v_{j+|\mu|-1})|$ starts in $(v_{j},+)$, ends in some $(v_{j+|\mu|-1},p)$, and
is consistent with $\sigma_{v_{j}}$.

  2. (2)

If $\mu$ is infinite, then the suffix $\mu^{\prime}$ of $\rho^{\prime}$
starting at position $|h(v_{0}\cdots v_{j})|-1$ starts in $(v_{j},+)$ and is
consistent with $\sigma_{v_{j}}$.

For each position $j$ of $\rho$ we define $\text{ESI}(j)=k$ if the $k$-th ESI
of $\rho$ contains $v_{j}$. Moreover, if $\mu=v_{j}v_{j+1}v_{j+2}\cdots$ is an
ESI of $\rho$, then we call $\Omega(v_{j})$ the characteristic color of $\mu$.
By the construction of $h$, if the characteristic color of an ESI $\mu$ is
even, then $\mu$ consists only of a single vertex. If, however, the
characteristic color $c$ of an ESI $\mu$ is odd, then we have $\Omega(v)\leq
c$ for all vertices $v$ in $\mu$. Moreover, let $c^{\prime}$ be the
characteristic color of the ESI succeeding $\mu$, if $\mu$ is not the terminal
ESI of $\rho$. Due to the construction of $h$, we have $c^{\prime}>c$. If
$c^{\prime}$ is even, this observation implies
$c^{\prime}\in\mathrm{Ans}({\Omega(v)})$ for all vertices $v$ in $\mu$. As the
number of colors in $\mathcal{G}$ is finite, this in turn implies that the
number of ESIs between a request and its response (if a response exists at
all) is bounded.

######  Remark 10.

Let $j$ be some position in $\rho$ and let $k=\text{ESI}(j)$. Moreover, let
$d$ be the number of colors in $\mathcal{G}$.

  1. (1)

If the request at position $j$ is first answered at position $j^{\prime}$,
then $\text{ESI}(j^{\prime})<k+d$

  2. (2)

If the request at position $j$ is unanswered in $\rho$, then $\rho$ contains
less than $k+d$ many ESIs.

######  Proof 5.2.

1. Let $\text{ESI}(j^{\prime})=k^{\prime}$. If $\Omega(v_{j})$ is even, we obtain $k=k^{\prime}$ and the claim is trivial. Thus, assume that $\Omega(v_{j})$ is odd. Since the request at position $j$ is answered in the $k^{\prime}$-th ESI, define the sequence $j_{0}<\cdots<j_{k^{\prime}-k}$ inductively such that $j_{0}=\text{posMRR}(v_{0}\cdots v_{j})$ and such that, for each $\ell$ with $0\leq\ell\leq k^{\prime}-k$ the position $j_{\ell}$ is the unique position in $\rho$ with $\text{ESI}(j_{\ell})\neq\text{ESI}(j_{\ell-1})$. We claim that the requests opened by visiting the $v_{j_{\ell}}$ are answered at position $j^{\prime}$ at the earliest and show this by induction over $\ell$.

First consider $\ell=0$. Since $\Omega(v_{j})$ is odd, we obtain
$j_{0}\neq\bot$ and, hence, that $\Omega(v_{j_{0}})$ is odd. Assume towards a
contradiction that the request at position $j_{0}$ is answered at position
$j^{\prime\prime}<j^{\prime}$. If $j^{\prime\prime}<j$, then this contradicts
our choice of $j_{0}$ as the position of the most relevant request of the play
prefix $v_{0}\cdots v_{j}$: Since $\Omega(v_{j})$ is odd, we would then obtain
$\text{posMRR}(v_{0}\cdots v_{j})>j^{\prime\prime}>0=\text{posMRR}(v_{0}\cdots
v_{j})$. If, however, $j<j^{\prime\prime}<j^{\prime}$, we obtain that the
request at position $j$ is answered at position $j^{\prime\prime}$, since
$\Omega(v_{j_{0}})\geq\Omega(v_{j})$ by definition of the most relevant
requests. Hence, we obtain $j^{\prime\prime}\geq j^{\prime}$.

Now consider $j_{\ell}$ for $0<\ell\leq k^{\prime}-k$: Since we have
$\Omega(v_{j_{\ell}})>\Omega(v_{j_{\ell-1}})$, an answer to the request posed
by $v_{j_{\ell}}$ would answer the request posed by $v_{j_{\ell-1}}$ as well.
Via the induction hypothesis we obtain that $v_{j_{\ell}}$ is answered at
position $j^{\prime}$ at the earliest.

Thus, the only possibility to switch the mimicked strategy and enter a new ESI
is by visiting a vertex of larger odd color than the vertex at the initial
position of the current ESI. Hence, the color of the $v_{j_{\ell}}$ is
strictly monotonically increasing, which implies $k^{\prime}<k+d$.

2. Since the request at position $j$ is unanswered, we obtain that $\Omega(v_{j})$ is odd. Again define the sequence $j_{0}<j_{1}<j_{2}<\cdots$ inductively such that $j_{0}=\text{posMRR}(v_{0}\cdots v_{j})$ and such that, for each $\ell>0$, the position $j_{\ell}$ is the unique position in $\rho$ with $\text{ESI}(j_{\ell})\neq\text{ESI}(j_{\ell-1})$. Due to similar reasoning as in the previous case, we obtain that the request posed at each $j_{\ell}$ is unanswered. Thus, the only possibility to enter a new ESI is again by visiting a vertex of higher odd color than the vertex at the initial position of the current ESI, which again implies that the number of ESIs in $\rho$ is bounded by $k+d$.

Recall that the bounded parity condition with weights requires the play $\rho$
to not only satisfy the parity condition, but also that the cost of almost all
requests is bounded and that there exists no unanswered request with infinite
cost in $\rho$. We first show that $\rho$ satisfies the classical parity
condition. In a second step, we then show that there exists a bound on the
cost of each (answered or unanswered) request in $\rho$. The former condition,
i.e., that $\rho$ satisfies the parity condition, is in large parts implied by
Remark 10.

######  Lemma 11.

The play $\rho$ satisfies the parity condition.

######  Proof 5.3.

If $\rho$ contains no unanswered requests, then it vacuously satisfies the
parity condition. Hence, let $j$ be the position of such an unanswered request
in $\rho$. Due to Remark 10, we obtain that there exist only finitely many
ESIs in $\rho$. Let $\mu=v_{j^{*}}v_{j^{*}+1}v_{j^{*}+2}\cdots$ be the
terminal ESI of $\rho$. By the construction of $h$, there exists a suffix
$\mu^{\prime}$ of $\rho^{\prime}$ with $\text{unpol}(\mu^{\prime})=\mu$. Due
to Item 2 of Remark 9, the suffix $\mu^{\prime}$ begins in $(v_{j^{*}},+)$ and
is consistent with the winning strategy $\sigma_{v_{j^{*}}}$ for Player $0$
from $(v_{j^{*}},+)$ in $\mathcal{G}_{v_{j^{*}}}$. Moreover, $\mu^{\prime}$ is
a play of Type $0$ due to $\mu^{\prime}$ being the terminal ESI of $\rho$ and
due to being consistent with $\sigma_{v_{j^{*}}}$. Hence, we obtain that $\mu$
satisfies the parity condition via Remark 7, which in turn implies that $\rho$
satisfies the parity condition.

It remains to show that the costs of requests in $\rho$ are bounded. Recall
that we defined $n^{\prime}=|\mathcal{A}_{v}|$, $d^{\prime}$ as the largest
color of a vertex in the $\mathcal{G}_{v}$, and $W^{\prime}$ as the largest
absolute weight of an edge. We claim that the costs of the most relevant
requests in $\rho$ are bounded by ${(n^{\prime}d^{\prime}W^{\prime})}^{2}$.
This implies that the cost of all requests is bounded: Due to Remark 10 we
obtain that the number of ESIs between a request and its response, if one
exists, is bounded by $d$. Hence, it suffices to show that each ESI
contributes at most a bounded amount to the cost of answering a request.

######  Lemma 12.

Let $\mu=v_{j}v_{j+1}v_{j+2}\cdots$ be an ESI of $\rho$. For each $j^{\prime}$
with $j\leq j^{\prime}<j+|\mu|$ we have $|w(v_{j}\cdots v_{j^{\prime}})|\leq
d^{\prime}{(n^{\prime}W^{\prime})}^{2}$.

######  Proof 5.4.

Since $\mu$ is an ESI, Player $0$ mimicks the choices of the strategy
$\sigma_{v_{j}}$, which is a winning strategy for him in the induced energy
parity game $\mathcal{G}_{v_{j}}$. Recall that $\sigma_{v_{j}}$ is of size at
most $n^{\prime}d^{\prime}W^{\prime}$. For the sake of readability, we define
$s=n^{\prime}d^{\prime}W^{\prime}$.

Now, towards a contradiction, let $j^{\prime}$ be a position with $j\leq
j^{\prime}<j+|\mu|$, such that we have $|w(v_{j}\cdots
v_{j^{\prime}})|>d^{\prime}{(n^{\prime}W^{\prime})}^{2}=n^{\prime}sW^{\prime}$.
We define $\pi=v_{j}\cdots v_{j^{\prime}}$ and assume
$w(\pi)>n^{\prime}sW^{\prime}$, i.e., that the infix $\pi$ violates the
claimed bound from above. The other case is dual. Let $j^{\prime\prime}$ be
the minimal position in $\mu$ such that the weight accrued by the ESI is
strictly positive starting at $j^{\prime\prime}$ until it reaches
$j^{\prime}$. Formally, we define $j^{\prime\prime}$ as the minimal position
that satisfies $w(v_{j}\cdots v_{k})>0$ for all
$k\in\\{j^{\prime\prime},\dots,j\\}$.

Due to the definition of $W$ we obtain $w(v_{j}\cdots
v_{j^{\prime\prime}})\leq W$. Since we furthermore have $w(\pi)=w(v_{j}\cdots
v_{j^{\prime}})>n^{\prime}sW^{\prime}$ by assumption, we obtain

$w(v_{j^{\prime\prime}}\cdots v_{j^{\prime}})=w(v_{j}\cdots
v_{j^{\prime}})-w(v_{j}\cdots
v_{j^{\prime\prime}})>n^{\prime}sW^{\prime}-W^{\prime}\geq
n^{\prime}sW^{\prime}-W^{\prime}+1\enspace.$

Now consider the unique infix
$\pi^{\prime}=(v_{j},p_{j})\cdots(v_{j^{\prime}},p_{j^{\prime}})$ of
$\rho^{\prime}$ that corresponds to the infix $\pi$ of $\rho$. Since $\pi$ is
an infix of a single ESI, $\pi^{\prime}$ is a play prefix in the energy parity
game $\mathcal{G}_{v_{j}}$ that is consistent with the strategy
$\sigma_{v_{j}}$, which is winning for Player $0$ from $(v_{j},p_{j})$.
Furthermore, since we have $w(v_{j}\cdots v_{k})>0$ for all
$k\in\\{j^{\prime\prime},\dots,j^{\prime}\\}$, the polarity of
$(v_{j^{\prime\prime}},p_{j^{\prime\prime}})\cdots(v_{j^{\prime}},p_{j^{\prime}})$
is constant and positive. Hence, by construction of $\rho^{\prime}$, we obtain

$w_{v_{j}}((v_{j^{\prime\prime}},p_{j^{\prime\prime}})\cdots(v_{j^{\prime}},p_{j^{\prime}}))=-w(v_{j^{\prime\prime}}\cdots
v_{j^{\prime}})\enspace.$

Due to the above inequality, this implies

$w_{v_{j}}((v_{j^{\prime\prime}},p_{j^{\prime\prime}})\cdots(v_{j^{\prime}},p_{j^{\prime}}))\leq-n^{\prime}sW^{\prime}+W^{\prime}-1=-(n^{\prime}s-1)W-1\enspace.$

As argued above, the infix
$(v_{j^{\prime\prime}},p_{j^{\prime\prime}})\cdots(v_{j^{\prime}},p_{j^{\prime}})$
is an infix of a play in the energy parity game $\mathcal{G}_{v_{j}}$ that
starts in $(v_{j},p_{j})$ and is consistent with the strategy $\sigma_{v_{j}}$
for Player $0$. Furthermore, $\sigma_{v_{j}}$ is winning for Player $0$ from
$(v_{j},p_{j})$ and is of size $s$. This yields the desired contradiction to
Lemma 3 on Page 3.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$w$$0$$\rho$$\Delta$$\Delta$$\mu_{j}$$\Delta$$\Delta$$\mu_{j+1}$$\Delta$$\Delta$$\mu_{j+2}$$\Delta$$\Delta$$\mu_{j+3}$$\Delta$$\Delta$$\mu_{j+4}$
Figure 5. Bounds on the cost of a request over time given by Lemma 12. We
write $\Delta=d^{\prime}{(n^{\prime}W^{\prime})}^{2}$.

Due to Lemma 12, each ESI strictly in-between a request and its response
contributes at most $d^{\prime}{(n^{\prime}W^{\prime})}^{2}$ to the cost
incurred by the request. Similarly, the ESI containing the request and its
response also contribute at most $d^{\prime}{(n^{\prime}W^{\prime})}^{2}$ each
to the cost of answering the given request. Hence, via Remark 10, we obtain
that each (answered or unanswered) request in $\rho$ incurs a cost of at most
${(d^{\prime}n^{\prime}W^{\prime})}^{2}$. We illustrate this argument in
Figure 5. Hence, $\sigma$ is a winning strategy for Player $0$ from $v^{*}$ in
$\mathcal{G}$, as each play that starts in $v^{*}$ and is consistent with
$\sigma$ satisfies the parity condition due to Lemma 11 and because no such
play contains a request that is unanswered with infinite cost, which concludes
the proof of Item 2 of Lemma 4.

Before we conclude this section, we formalize the above observation about the
winning strategy for Player $0$ uniformly bounding the costs of requests in
the following corollary. To this end, we use the upper bounds $n^{\prime}\leq
2n+4n^{2}$, $d^{\prime}\leq d+2$, and $W^{\prime}\leq W+1$.

######  Corollary 13.

Let $\mathcal{G}$ be a bounded parity game with weights with $n$ vertices, $d$
colors, and largest absolute weight $W$. There exists a strategy $\sigma$ for
Player $0$ that is winning from $\mathcal{W}_{0}(\mathcal{G})$, such that in
each play $\rho$ consistent with $\sigma$, each request is answered or
unanswered with cost at most ${((d+2)(2n+4n^{2})(W+1))}^{2}$.

Using arguments from Section 7, this bound can be improved to
${((d+2)(6n)(W+1))}^{2}$. However, as we only use Corollary 13 later to obtain
some upper bound on the quality of such strategies, we refrain from repeating
these arguments here.

##  6\. Memory Requirements

We now discuss the upper and lower bounds on the memory required to implement
winning strategies for either player. Recall that we use binary encoding to
denote weights, i.e., weights may be exponential in the size of the game. In
this section we show pseudo-polynomial bounds on the necessary and sufficient
memory for Player $0$ to win parity games with weights. In contrast, Player
$1$ requires infinite memory.

######  Theorem 14.

Let $\mathcal{G}$ be a parity game with weights with $n$ vertices, $d$ colors,
and largest absolute weight $W$ assigned to any edge in $\mathcal{G}$.

  1. (1)

Player $0$ has a winning strategy $\sigma$ from $\mathcal{W}_{0}(\mathcal{G})$
with $|\sigma|\in\mathcal{O}(nd^{2}W)$. This bound is tight.

  2. (2)

There exists a parity game with weights $\mathcal{G}$, such that Player $1$
has a winning strategy from each vertex $v$ in $\mathcal{G}$, but she has no
finite-state winning strategy from any $v$ in $\mathcal{G}$.

The proof of the second item of Theorem 14 is straightforward, since Player
$1$ already requires infinite memory to implement winning strategies in
finitary parity games [CHH09]. Since parity games with weights subsume
finitary parity games, this result carries over to our setting. We show the
game witnessing this lower bound on the right-hand side of Figure 2 on Page 2.

In contrast, pseudo-polynomial memory is sufficient, but also necessary, for
Player $0$. To show this claim, we first prove that the winning strategy for
him in a bounded parity game with weights constructed in the proof of Item 2
of Lemma 4 suffers at most a linear blowup in comparison to his winning
strategies in the underlying energy parity games. This is sufficient as we
have argued in Section 4 that the construction of a winning strategy for
Player $0$ in a parity game with weights suffers no blowup in comparison to
the underlying bounded parity games with weights.

######  Lemma 15.

Let $\mathcal{G}$ be a bounded parity game with weights and let $n$, $d$, and
$W$ be defined analogously to Theorem 14. Player $0$ has a finite-state
winning strategy of size at most $d(6n)(d+2)(W+1)$ from
$\mathcal{W}_{0}(\mathcal{G})$.

######  Proof 6.1.

Let $V$ and $E$ be the vertex and edge sets of $\mathcal{G}$ and recall that
we have defined $P=\\{+,-\\}$. In the proof of Item 2 of Lemma 4, we have
constructed an energy parity game $\mathcal{G}_{v}$ with vertices $(V\times
P)\cup(E\times P\times\\{0,1\\})$ for each vertex $v$ of $\mathcal{G}$. We
have then constructed a winning strategy $\sigma$ for Player $0$ for
$\mathcal{G}$ out of winning strategies for him in the $\mathcal{G}_{v}$. As
it is straightforward to implement $\sigma$ via the disjoint union of memory
structures implementing the constituent strategies, this approach yields an
upper bound of $n(2n+4n^{2})(d+2)(W+1)$ on the size of $\sigma$ due to the
upper bound on the size of winning strategies for Player $0$ in energy parity
games from Proposition 5.1.

In the construction of the $\mathcal{G}_{v}$, however, we only store the edges
chosen by the players in the vertices of the form $E\times P\times\\{0,1\\}$
for didactic purposes. In fact, it suffices to store the target vertex of an
edge instead, resulting in a vertex set of size $6n$ of the $\mathcal{G}_{v}$.
Moreover, recall that the definition of the $\mathcal{G}_{v}$ only takes the
color of $v$ into account: If the vertices $v$ and $v^{\prime}$ have the same
color, then the games $\mathcal{G}_{v}$ and $\mathcal{G}_{v^{\prime}}$ are
isomorphic. Further, Chatterjee and Doyen have shown that, if Player $0$ wins
an energy parity game $\mathcal{G}^{\prime}$ with $n^{\prime}$ vertices,
$d^{\prime}$ colors, and largest absolute weight $W^{\prime}$, then he has a
uniform strategy of size $n^{\prime}d^{\prime}W^{\prime}$ that is winning from
all vertices from which he wins $\mathcal{G}^{\prime}$ [CD12]. Hence, it
suffices to combine at most $d$ strategies, each of size $(6n)(d+2)(W+1)$, in
order to obtain a winning strategy for Player $0$ in $\mathcal{G}$.

Having established an upper bound on the memory required by Player $0$, we now
proceed to show that this bound is tight.

######  Lemma 16.

Let $n,W\in\mathbb{N}$. There exists a parity game with weights
$\mathcal{G}_{n,W}$ with $\mathcal{O}(n)$ vertices and largest absolute weight
$W$ such that Player $0$ wins $\mathcal{G}_{n,W}$ from every vertex, but each
winning strategy for him is of size at least $nW+1$.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$\nicefrac{{v_{\text{req}}}}{{3}}$$\nicefrac{{v^{\prime}_{\text{req},1}}}{{1}}$$\nicefrac{{v^{\prime}_{\text{req},n}}}{{1}}$$\nicefrac{{v_{\text{del}}}}{{1}}$$\nicefrac{{v^{\prime}_{\text{ans}}}}{{2}}$$\nicefrac{{v_{\text{ans}}}}{{4}}$0
$W$ $\cdots$$W$ $W$ $\cdots$$W$ $W$ $\cdots$$W$ $W$ $-1$ $0$ $0$ $n$ vertices
0 0  Figure 6. A game of size $\mathcal{O}(n)$ in which Player $0$ only wins
with strategies of size at least $nW+1$.

######  Proof 6.2.

We show the game $\mathcal{G}_{n,W}$ in Figure 6. This game has $n+4$ vertices
and the largest absolute weight of an edge is $W$ as required. The only
vertices with more than one successor are $v_{\text{del}}\in V_{0}$ and
$v^{\prime}_{\text{ans}}\in V_{1}$. Thus, the only choice of Player $0$ in
$\mathcal{G}_{n,W}$ consists in determining how often to take the self-loop of
vertex $v_{\text{del}}$ upon each visit. Dually, the only choice of Player $1$
consists of deciding whether or not to move from $v^{\prime}_{\text{ans}}$ to
$v^{\prime}_{\text{req},1}$, or to continue to $v_{\text{ans}}$.

Player $0$ wins $\mathcal{G}_{n,W}$ from each vertex by taking the self-loop
of $v_{\text{del}}$ $nW$ times upon each visit to $v_{\text{del}}$ and by
subsequently moving to $v^{\prime}_{\text{ans}}$. Each request in each play
that is consistent with this strategy is answered or unanswered with cost at
most $nW$, independent of the choices of Player $1$ in
$v^{\prime}_{\text{ans}}$. Moreover, as the only way to visit $v_{\text{req}}$
is to move there from $v_{\text{ans}}$, the play visits $v_{\text{ans}}$
infinitely often if and only if it visits $v_{\text{req}}$ infinitely often.
Further, the play visits $v^{\prime}_{\text{req},1}$ and
$v^{\prime}_{\text{ans}}$ infinitely often. Hence, almost all requests are
answered, i.e., this strategy is winning for Player $0$ from all vertices.
This strategy can be implemented by a counter that counts the number of self-
loops of $v_{\text{del}}$ taken so far, which is reset to zero upon leaving
$v_{\text{del}}$. As this counter is bounded by $nW$, the strategy is of size
$nW+1$.

It remains to show that each finite-state winning strategy for Player $0$ has
at least $nW+1$ memory states. Towards a contradiction, let $\sigma$ be a
winning strategy for Player $0$ from some vertex $v$ with less than $nW+1$
memory states. We implement a strategy for Player $1$ using a counter $\kappa$
that is initialized with one if $v=v_{\text{req}}$ and with zero otherwise.
Upon each visit to $v_{\text{req}}$ we increment $\kappa$. After each visit to
$v_{\text{req}}$, the strategy $\tau$ prescribes moving from
$v^{\prime}_{\text{ans}}$ to $v^{\prime}_{\text{req},1}$ for the first
$\kappa$ visits to $v^{\prime}_{\text{ans}}$, and it prescribes moving from
$v^{\prime}_{\text{ans}}$ to $v_{\text{ans}}$ at the $(\kappa+1)$-th visit to
$v^{\prime}_{\text{ans}}$. Hence, after the $(\kappa+1)$-th visit to
$v^{\prime}_{\text{ans}}$, the vertex $v_{\text{req}}$ is visited again,
$\kappa$ is incremented, and the behavior of $\tau$ described above repeats
with incremented $\kappa$.

Let $\rho$ be a play consistent with $\sigma$ and $\tau$. Since $\sigma$ is
winning for Player $0$, the play $\rho$ does not remain in $v_{\text{del}}$
from some point onwards ad infinitum, as this would violate the parity
condition and thus contradict $\sigma$ being winning from $v$ for Player $0$.
Hence, playing consistently with $\tau$, Player $1$ enforces a play that
starts with a (possibly empty) finite prefix that ends before the first visit
to $v_{\text{req}}$ and that continues with infinitely many rounds, each
starting in $v_{\text{req}}$. The $j$-th round is of the form

$v_{\text{req}}\cdot\Pi_{k=0,\dots,j}(v^{\prime}_{\text{req},1}\cdots
v^{\prime}_{\text{req},n}\cdot{(v_{\text{del}})}^{\ell_{j,k}}\cdot
v^{\prime}_{\text{ans}})\cdot v_{\text{ans}}\enspace.$

We first show $\ell_{j,k}<nW+1$ for all $j,k$. Towards a contradiction, assume
$\ell_{j,k}\geq nW+1$ for some $j,k\in\mathbb{N}$. Since $\sigma$ is of size
less than $nW+1$, a straightforward pumping argument shows that the play
$\rho^{\prime}$ consisting of the finite prefix of $\rho$ ending before the
first visit to $v_{\text{req}}$ concatenated with the first $j-1$ rounds of
$\rho$, but ending with the infinite suffix

$v_{\text{req}}\cdot\Pi_{k^{\prime}=0,\dots,k-1}(v^{\prime}_{\text{req},1}\cdots
v^{\prime}_{\text{req},n}\cdot{(v_{\text{del}})}^{\ell_{j,k^{\prime}}}\cdot
v^{\prime}_{\text{ans}})\cdot v^{\prime}_{\text{req},1}\cdots
v^{\prime}_{\text{req},n}\cdot{(v_{\text{del}})}^{\omega}\ ,$

is consistent with $\sigma$. This, however, contradicts $\sigma$ being a
winning strategy for Player $0$ from $v$ as $v_{\text{del}}$ has the odd color
one, i.e., as the resulting play violates the parity condition. Hence, we
obtain $\ell_{j,k}<nW+1$ for all $j,k$, which, in turn, yields
$w({(v_{\text{del}})}^{\ell_{j,k}})>-nW$.

Since each edge
$(v^{\prime}_{\text{req},n^{\prime}},v^{\prime}_{\text{req},n^{\prime}+1})$
for $1\leq n^{\prime}<n$ as well as the edge
$(v^{\prime}_{\text{req},n},v^{\prime}_{\text{del}})$ has weight $W$, we
obtain

$w(v^{\prime}_{\text{req},1}\cdots
v^{\prime}_{\text{req},n}\cdot{(v_{\text{del}})}^{\ell_{j,k}}\cdot
v^{\prime}_{\text{ans}})>0$

for all $j,k$. This, in turn, implies

$w(v_{\text{req}}\cdot\Pi_{k=0,\dots,j}(v^{\prime}_{\text{req},1}\cdots
v^{\prime}_{\text{req},n}\cdot{(v_{\text{del}})}^{\ell_{j,k^{\prime}}}\cdot
v^{\prime}_{\text{ans}}))\geq j+1$

for each $j$. Since, as argued above, the play $\rho$ consistent with $\sigma$
consists of infinitely many rounds, we obtain that for each $b\in\mathbb{N}$
there exist infinitely many requests in $\rho$ that are answered with cost at
least $b$. Hence, the costs-of-requests along $\rho$ diverge, which
contradicts $\sigma$ being a winning strategy for Player $0$.

This concludes the study of memory requirements for both players in parity
games with weights. For Player $0$, the results from Theorem 14 also hold true
for bounded parity games with weights: Lemma 15 directly yields an upper bound
on the memory required by Player $0$ in order to win in bounded parity games
with weights, while it is easy to see that Player $0$ also wins the games
constructed in the proof of Lemma 16 when interpreting them as bounded parity
games with weights, but only using a strategy of size $nW+1$.

For Player $1$, however, these results do not directly carry over to the
setting of bounded parity games with weights. She has, in fact, a positional
winning strategy for the game witnessing necessity of infinite memory for her
in parity games with weights shown in Figure 2 on Page 2, when interpreted as
a bounded parity game with weights. Recall that, in the proof of the first
item of Lemma 4, for a given parity game with weights $\mathcal{G}$, we
construct a strategy $\tau$ that is winning for Player $1$ from a vertex $v$
out of a winning strategy $\tau_{v}$ for her in an induced energy parity game
$\mathcal{G}_{v}$ from a designated vertex $v^{\prime}$.

While $\tau_{v}$ can be assumed to be positional as shown by Chatterjee and
Doyen [CD12] (cf. Proposition 5.1), the strategy $\tau$ keeps track of play
prefixes in $\mathcal{G}_{v}$ and thus requires potentially infinitely many
memory states. In particular, in order to win $\mathcal{G}_{v}$ from
$v^{\prime}$, recall that it may be necessary to switch between two copies of
the arena of $\mathcal{G}$. Whether or not to perform this switch is governed
by the accumulated weight of the play prefix in $\mathcal{G}$ thus far.

Hence, our construction from the proof of that lemma does not directly allow
us to obtain positional or finite-state winning strategies for Player $1$ in
bounded parity games with weights. It remains open whether Player $1$ requires
infinite memory to win in bounded parity games with weights. Since she,
however, has finite-state winning strategies in the special case of bounded
parity games with costs as shown by Fijalkow and Zimmermann [FZ14], we
conjecture that she requires at most finite memory for winning strategies in
bounded parity games with weights as well.

We now turn our attention to the quantitative properties of this winning
condition. To this end, we provide tight bounds on the costs of requests that
Player $0$ can guarantee in a parity game with weights $\mathcal{G}$, if she
wins $\mathcal{G}$ at all.

##  7\. Quality of Strategies

We have shown in the previous section that finite-state strategies of bounded
size suffice for Player $0$ to win in parity games with weights, while Player
$1$ clearly requires infinite memory. However, as we are dealing with a
quantitative winning condition, we are not only interested in the size of
winning strategies, but also in their quality. More precisely, we are
interested in an upper bound on the cost of requests that Player $0$ can
ensure. In this section, we show that he can guarantee a pseudo-polynomial
upper bound on such costs. Dually, Player $1$ is required to unbound the cost
of responses.

######  Theorem 17.

Let $\mathcal{G}$ be a parity game with weights with $n$ vertices, $d$ colors,
and largest absolute weight $W$.

There exists a $b\in\mathcal{O}({(ndW)}^{2})$ and a strategy $\sigma$ for
Player $0$ such that, for all plays $\rho$ beginning in
$\mathcal{W}_{0}(\mathcal{G})$ and consistent with $\sigma$, we have
$\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)\leq b$. This bound is tight.

We first show that Player $0$ can indeed ensure an upper bound as stated in
Theorem 17. We obtain this bound via a straightforward pumping argument
leveraging the upper bound on the size of winning strategies obtained in Lemma
15.

######  Lemma 18.

Let $\mathcal{G}$, $n$, $d$, and $W$ be as in the statement of Theorem 17 and
let $s=d(6n)(d+2)(W+1)$. Player $0$ has a winning strategy $\sigma$ such that,
for each play $\rho$ that starts in $\mathcal{W}_{0}(\mathcal{G})$ and is
consistent with $\sigma$, we have
$\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)\leq nsW$.

######  Proof 7.1.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$w$$\rho$$j_{0}$$j^{\prime}_{0}$$j_{1}$$j^{\prime}_{1}$$j_{2}$$j^{\prime}_{2}$$nsW$$-nsW$PositivelysumptuousNegativelysumptuousPositivelysumptuous$\ell_{0}$$\ell^{\prime}_{0}$$\ell_{1}$$\ell^{\prime}_{1}$$\ell_{2}$$\ell^{\prime}_{2}$
Figure 7. Illustration of the approach to the proof of Lemma 18.

Let $\sigma$ be a winning strategy for Player $0$ in $\mathcal{G}$ from
$\mathcal{W}_{0}(\mathcal{G})$ of size at most $s$. Due to Lemma 15, such a
strategy exists. Let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play that starts in
$\mathcal{W}_{0}(\mathcal{G})$ and is consistent with $\sigma$. We call a
position $j\in\mathbb{N}$ sumptuous if $nsW<\mathrm{Cor}(\rho,j)<\infty$. Each
sumptuous position $j$ has some odd color $c$, and the request for $c$ posed
by visiting $v_{j}$ is eventually answered.

Assume towards a contradiction that there exist infinitely many sumptuous
positions. We define a sequence of positions that begins with the first
sumptuous position $j_{0}$. Let $j^{\prime}_{0}$ be the minimal position that
satisfies $\Omega(v_{j^{\prime}_{0}})\in\mathrm{Ans}({\Omega(v_{j_{0}})})$.
This position exists since $\mathrm{Cor}(\rho,j_{0})<\infty$ due to the
definition of sumptuous positions. We continue by defining $j_{1}$ as the
smallest sumptuous position greater than $j^{\prime}_{0}$ and by defining
$j^{\prime}_{1}$ as the minimal position that satisfies
$\Omega(v_{j^{\prime}_{1}})\in\mathrm{Ans}({\Omega(v_{j_{1}})})$. Continuing
in this manner, we obtain a sequence
$j_{0}<j^{\prime}_{0}<j_{1}<j^{\prime}_{1}<j_{2}<j^{\prime}_{2}<\cdots$, where
$j_{0}$ is the first sumptuous position of $\rho$, each $j^{\prime}_{k}$ for
$k\geq 0$ is the minimal position that satisfies both $j^{\prime}_{k}>j_{k}$
and $\Omega(v_{j^{\prime}_{k}})\in\mathrm{Ans}({\Omega(v_{j_{k}})})$, and each
$j_{k}$ for $k>0$ is the smallest sumptuous position greater than
$j^{\prime}_{k-1}$. Since there exist infinitely many sumptuous positions by
assumption and since each request posed at a sumptuous position is answered by
definition, the sequence
$j_{0}<j^{\prime}_{0}<j_{1}<j^{\prime}_{1}<j_{2}<j^{\prime}_{2}<\cdots$ is
indeed infinite.

Due to the definition of sumptuous positions and the $j^{\prime}_{k}$, we have
$\mathrm{Ampl}(v_{j_{k}}\cdots v_{j^{\prime}_{k}})>nsW$ for each
$k\in\mathbb{N}$. Since $\rho$ is consistent with the finite-state strategy
$\sigma$ of size $s$, we claim that in each such $v_{j_{k}}\cdots
v_{j^{\prime}_{k}}$ there exists an infix that can be repeated arbitrarily
often while retaining consistency with $\sigma$. To identify such infixes, we
partition the sumptuous positions $j_{k}$: We call a position $j_{k}$
positively sumptuous if there exists a $j^{\prime}$ with $j_{k}\leq
j^{\prime}\leq j^{\prime}_{k}$ such that $w(v_{j_{k}}\cdots
v_{j^{\prime}})>nsW$ and negatively sumptuous otherwise. In the latter case,
there exists a $j^{\prime}$ with $j_{k}\leq j^{\prime}\leq j^{\prime}_{k}$
such that $w(v_{j_{k}}\cdots v_{j^{\prime}})<-nsW$. See Figure 7 for an
illustration. In particular, note that the third sumptuous position is
positively sumptuous, although it exceeds both the bounds $nsW$ and $-nsW$.

Let $\sigma$ be implemented by $(M,\text{init},\mathrm{upd})$. As each edge
contributes cost at most $W$ to $\mathrm{Ampl}(v_{j_{k}}\cdots
v_{j^{\prime}_{k}})$, this implies that there exist positions $\ell_{k}$ and
$\ell^{\prime}_{k}$ with $j_{k}<\ell_{k}<\ell^{\prime}_{k}<j^{\prime}_{k}$
such that

  * •

$v_{\ell_{k}}=v_{\ell^{\prime}_{k}}$,

  * •

$\mathrm{upd}^{+}(v_{0}\cdots v_{\ell_{k}})=\mathrm{upd}^{+}(v_{0}\cdots
v_{\ell^{\prime}_{k}})$,

  * •

$w(v_{\ell_{k}}\cdots v_{\ell^{\prime}_{k}-1})>0$, if $j_{k}$ is positively
sumptuous, and such that

  * •

$w(v_{\ell_{k}}\cdots v_{\ell^{\prime}_{k}-1})<0$, if $j_{k}$ is negatively
sumptuous.

The positions $j_{k}$, $\ell_{k}$, $\ell^{\prime}_{k}$, and $j^{\prime}_{k}$
split $\rho$ into infixes
$\rho=\Pi_{k=0,1,2,\dots}\pi_{k,\mathit{I}}\cdot\pi_{k,\mathit{II}}\cdot\pi_{k,\mathit{III}}\cdot\pi_{k,\mathit{IV}}$,
where $\pi_{k,\mathit{I}}$, $\pi_{k,\mathit{II}}$, $\pi_{k,\mathit{III}}$, and
$\pi_{k,\mathit{IV}}$ start at $j_{k}$, $\ell_{k}$, $\ell^{\prime}_{k}$, and
$j^{\prime}_{k}$, respectively. Due to the definition of $\ell_{k}$ and
$\ell^{\prime}_{k}$, the play
$\rho^{\prime}=\Pi_{k=0,1,2,\dots}\pi_{k,\mathit{I}}\cdot{(\pi_{k,\mathit{II}})}^{k}\cdot\pi_{k,\mathit{III}}\cdot\pi_{k,\mathit{IV}}$
is consistent with $\sigma$. The costs-of-response of the requests opened by
visiting the $v_{j_{k}}$, however, diverge due to
$|w(\pi_{k,\mathit{II}})|=|w(v_{\ell_{k}}\cdots v_{\ell^{\prime}_{k}-1})|>0$.
Hence, $\rho^{\prime}$ violates the parity condition with weights, which
contradicts that $\sigma$ is a winning strategy of Player $0$.

Having thus shown that Player $0$ can indeed ensure a pseudo-polynomial upper
bound on the incurred cost, we now proceed to show that this bound is tight. A
simple example shows that there exists a series of parity games with weights
in which Player $0$ wins from every vertex, but in which he cannot enforce a
sub-pseudo-polynomial cost of any request.

######  Lemma 19.

Let $n,W\in\mathbb{N}$. There exists a parity game with weights
$\mathcal{G}_{n,W}$ with $n$ vertices and largest absolute weight $W$ such
that for each vertex $v\in\mathcal{W}_{0}(\mathcal{G})$ and for each winning
strategy for Player $0$ from $v$ there exists a play $\rho$ starting in $v$
and consistent with $\sigma$ with
$\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)\geq(n-1)W$.

######  Proof 7.2.

We show the game $\mathcal{G}_{n,W}$ in Figure 8. The arena of
$\mathcal{G}_{n,W}$ is a cycle with $n$ vertices of Player $1$, where each
edge has weight $W$. Moreover, one vertex is labeled with color two, its
directly succeeding vertex is labeled with color one. All remaining vertices
have color zero.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$\nicefrac{{v_{1}}}{{1}}$$\nicefrac{{v_{2}}}{{0}}$$\cdots$$\nicefrac{{v_{n-1}}}{{0}}$$\nicefrac{{v_{n}}}{{2}}$$W$$W$$W$$W$$W$
Figure 8. The game $\mathcal{G}_{n,W}$ witnessing a pseudo-polynomial lower
bound on the cost that Player $0$ can ensure.

Player $0$ only has a single strategy in this game and there exist only $n$
plays in $\mathcal{G}_{n,W}$, each starting in a different vertex of
$\mathcal{G}_{n,W}$. In each play, each request for color one is only answered
after $n-1$ steps, each contributing a cost of $W$. Hence, this request incurs
a cost of $(n-1)W$. Moreover, as this request is posed and answered infinitely
often in each play, we obtain the desired result.

While Player $0$ is able to bound the costs from above by

$d(6n^{2})(d+2)W(W+1)\in\mathcal{O}({(ndW)}^{2})\enspace,$

due to Lemma 18, we only obtain a sequence of examples witnessing a lower
bound of $(n-1)W\in\Omega(nW)$ on these costs due to Lemma 19. Thus, while
both the upper and the lower bound are pseudo-polynomial in the size of the
game, there remains a polynomial gap between the two bounds.

The upper bound on the costs is due to the pumping argument presented in Lemma
18 leveraging the upper bound on the memory Player $0$ requires to implement a
winning strategy due to Lemma 15. We have a lower bound of
$(n-4)W\in\Omega(nW)$ on the memory required by Player $0$ to implement a
winning strategy due to Lemma 15. Thus, even if we are able to improve the
upper bounds on the memory requirements for Player $0$, the pumping argument
leveraged in the proof of Lemma 18 can only improve the upper bound on the
cost incurred by Player $0$ to $d(n-4)W^{2}\in\mathcal{O}(ndW^{2})$. Hence,
the proof methods used in this section do not enable us to completely close
this gap between the upper and the lower bound on the cost Player $0$ is able
to enforce.

All bounds obtained in this section also hold for bounded parity games with
weights: The upper bound from Lemma 18 holds for bounded parity games with
weights since the bounded parity condition with weights strengthens its
unbounded variant. Analogously, the games constructed for the proof of the
lower bound on the incurred cost in Lemma 19 yield the same lower bound for
bounded parity games with weights.

##  8\. From Energy Parity Games to (Bounded) Parity Games with Weights

We have discussed in Sections 4 and 5 how to solve parity games with weights
via solving bounded parity games with weights and how to solve the latter
games by solving energy parity games, both steps with a polynomial overhead.
An obvious question is whether one can also solve energy parity games by
solving (bounded) parity games with weights. In this section, we answer this
question affirmatively: We show how to transform an energy parity game into a
bounded parity game with weights so that solving the latter also solves the
former. We then show how to transform a bounded parity game with weights into
a parity game with weights with the same relation: solving the latter also
solves the former. Both constructions here are gadget based and increase the
size of the arenas only quadratically. Hence, all three types of games are
interreducible with at most polynomial overhead.

###  8.1. From Energy Parity Games to Bounded Parity Games with Weights

In an energy parity game, Player $0$ wins if the energy increases without a
bound, as long as there is a lower bound. In a bounded parity game, in
contrast, he has to ensure both an upper and a lower bound. Thus, we show in a
first step how to modify an energy parity game so that Player $0$ still has to
ensure a lower bound on the energy, but can also _throw away_ unnecessary
energy during each transition, thereby also ensuring an upper bound. The most
interesting part of this construction is to determine when energy becomes
unnecessary to ensure a lower bound. Here, we rely on Lemma 3.

Formally, let $\mathcal{G}=(\mathcal{A},\Omega,w)$ be an energy parity game
with $\mathcal{A}=(V,V_{0},V_{1},E)$ where we assume w.l.o.g. that the minimal
color in $\Omega(V)$ is strictly greater than $1$. Now, we define
$\mathcal{G}^{\prime}=(\mathcal{A}^{\prime},\Omega^{\prime},w^{\prime})$ with
$\mathcal{A}=(V,V_{0},V_{1},E)$ where

  * •

$V^{\prime}=V\cup E$, $V_{0}^{\prime}=V_{0}\cup E$, and
$V_{1}^{\prime}=V_{1}$,

  * •

$E^{\prime}=\\{(v,e),(e,e),(e,v^{\prime})\mid e=(v,v^{\prime})\in E\\}$,

  * •

$\Omega^{\prime}(v)=\Omega(v)$ and $\Omega^{\prime}(e)=1$, and

  * •

$w^{\prime}(v,e)=w(e)$, $w^{\prime}(e,e)=-1$, and $w(e,v^{\prime})=0$ for
every $e=(v,v^{\prime})\in E$.

Intuitively, every edge of $\mathcal{A}$ is subdivided and a new vertex for
Player $0$ is added, where he can decrease the energy level. The negative
weight also ensures that he eventually leaves this vertex in order to satisfy
an energy condition.

We say that a strategy $\sigma$ for Player $0$ in $\mathcal{A}^{\prime}$ is
corridor-winning for him from some $v\in V$, if there is a $b\in\mathbb{N}$
such that every play $\rho$, which starts in $v$ and is consistent with
$\sigma$, satisfies the parity condition and $\mathrm{Ampl}(\rho)\leq b$.
Hence, instead of just requiring a lower bound on the energy level as in the
energy parity condition, we also require a uniform upper bound on the energy
level (where we assume w.l.o.g. these bounds to coincide).

######  Lemma 20.

Let $\mathcal{G}$ and $\mathcal{G}^{\prime}$ be as above and let $v\in V$.
Player $0$ has a winning strategy for $\mathcal{G}$ from $v$ if and only if he
has a corridor-winning strategy for $\mathcal{G}^{\prime}$ from $v$.

######  Proof 8.1.

We first show the direction from left to right. To this end, assume that
Player $0$ wins $\mathcal{G}$ from $v$. Due to Proposition 5.1, he has a
finite-state winning strategy $\sigma$ for $\mathcal{G}$ from $v$, say of size
$s$. Furthermore, there is an initial credit $c_{0}$ such that every play
prefix $\pi$ that starts in $v$ and is consistent with $\sigma$ satisfies
$w(\pi)\geq-c_{0}$. Finally, define $b=Wns$, where $n$ and $W$ denote the
number of vertices and the largest absolute weight occurring in $\mathcal{G}$,
respectively.

We define a strategy $\sigma^{\prime}$ for Player $0$ in
$\mathcal{G}^{\prime}$ such that it mimics the behavior of $\sigma$ and
additionally ensures that the energy level of a play prefix never exceeds $b$
by more than $W$. Formally, consider a play prefix $\pi^{\prime}$ in
$\mathcal{G}^{\prime}$ starting in $v$. If $\pi^{\prime}$ ends in some
$v^{\prime}\in V$, then we define
$\sigma^{\prime}(\pi)=(v^{\prime},\sigma(f(\pi)))$ where $f\colon{(V\cup
E)}^{*}\cup{(V\cup E)}^{\omega}\rightarrow V^{*}\cup V^{\omega}$ is the
homomorphism induced by $f(v)=v$ and $f(e)=\varepsilon$. On the other hand,
assume $\pi^{\prime}$ ends in some $e=(v^{\prime},v^{\prime\prime})\in E$. If
$w(\pi^{\prime})\leq b$, then we define
$\sigma^{\prime}(\pi^{\prime})=v^{\prime\prime}$, otherwise, we define
$\sigma^{\prime}(\pi^{\prime})=e$, i.e., the self-loop is used until the
energy level of the play prefix is exactly $b$. This completes the definition
of $\sigma^{\prime}$.

Now, consider a play $\rho^{\prime}$ in $\mathcal{G}^{\prime}$ that starts in
$v$ and is consistent with $\sigma^{\prime}$. By definition of
$\sigma^{\prime}$, $\rho^{\prime}$ visits infinitely many vertices in $V$.
Hence, by construction of $\mathcal{A}$, $\rho=f(\rho^{\prime})$ is a play in
$\mathcal{G}$ that starts in $v$. Further, $\rho$ is consistent with $\sigma$,
as $\sigma^{\prime}$ mimics $\sigma$. Hence, $f(\rho^{\prime})$ satisfies the
parity condition. As the vertices removed from $\rho^{\prime}$ all have color
one, and as all colors in $\Omega(V)$ are greater than one, we conclude that
$\rho^{\prime}$ satisfies the parity condition as well.

To conclude, we show that every prefix $\pi^{\prime}$ of $\rho^{\prime}$
satisfies $-c_{0}\leq w^{\prime}(\pi^{\prime})\leq b+W$. This implies that
$\sigma^{\prime}$ is indeed a corridor-winning strategy from $v$. The upper
bound $b+W$ is satisfied by construction of $\sigma^{\prime}$: As soon as the
weight exceeds $b$, it is decreased to $b$ by the strategy. As this correction
happens after each transition, the bound $b$ can be exceeded by at most $W$,
the largest absolute weight of an edge.

To conclude, we consider two cases: first, assume $\rho^{\prime}$ has no
prefix whose energy level exceeds $b$, then we have
$w^{\prime}(\pi^{\prime})=w(f(\pi))\geq-c_{0}$ for every prefix $\pi^{\prime}$
of $\rho^{\prime}$. Second, assume that $\rho^{\prime}$ has at least one
prefix whose weight exceeds $b$. Let $\pi$ be the shortest such prefix. For
every prefix $\pi^{\prime}$ shorter than $\pi$ we obtain $-c_{0}\leq
w^{\prime}(\pi^{\prime})\leq b+W$ via the above argument. We show that every
prefix longer than $\pi$ has nonnegative weight, which concludes the proof.

Towards a contradiction, assume that there is a longer suffix with negative
weight. Then there is an infix of $\rho^{\prime}$ of weight strictly smaller
than $-b$, such that Player $0$ never uses a self-loop in
$\mathcal{A}^{\prime}$ to throw away energy. Hence, $f(\rho)$ also has an
infix with weight strictly smaller than $-b$. This, however, contradicts Lemma
3 and thus concludes the proof of this direction.

We now show the other direction of the lemma. To this end, let
$\sigma^{\prime}$ be a corridor-winning strategy for Player $0$ in
$\mathcal{G}^{\prime}$ from $v$. Further, let $f$ be defined as above.

We define a strategy $\sigma$ for Player $0$ from $v$ in $\mathcal{G}$ that is
obtained by simulating play prefixes in $\mathcal{G}^{\prime}$. To this end,
we again use a simulation function $h$ that maps a play prefix $v_{0}\cdots
v_{j}$ in $\mathcal{G}$ that starts in $v$ and is consistent with $\sigma$ to
a play prefix $h(v_{0}\cdots v_{j})$ in $\mathcal{G}^{\prime}$ that starts in
$v$, is consistent with $\sigma^{\prime}$, and ends in $v_{j}$.

Hence, we define $h(v)=v$. Now, assume we have a play prefix $v_{0}\cdots
v_{j}$ in $\mathcal{G}$ that starts in $v$ and is consistent with $\sigma$.
From our construction, we obtain a play prefix $h(v_{0}\cdots v_{j})$ in
$\mathcal{G}^{\prime}$ that starts in $v$, is consistent with
$\sigma^{\prime}$, and ends in $v_{j}$. If $v_{j}\in V_{0}\subseteq
V_{0}^{\prime}$, then let $\sigma^{\prime}(h(v_{0}\cdots
v_{j}))=(v_{j},v_{j+1})$. We define $\sigma(v_{0}\cdots v_{j})=v_{j+1}$, which
is a legal move due to the construction of $\mathcal{A}^{\prime}$. If
$v_{j}\in V_{1}$, then let $v_{j+1}$ be an arbitrary successor of $v_{j}$ in
$\mathcal{A}$.

In both cases, we have to define $h(v_{0}\cdots v_{j}v_{j+1})$. As
$\sigma^{\prime}$ is a corridor-winning strategy for Player $0$ from $v$ in
$\mathcal{G}^{\prime}$, there is a unique play of the form $h(v_{0}\cdots
v_{j}){(v_{j},v_{j+1})}^{m}v_{j+1}$ that is consistent with $\sigma^{\prime}$.
We define $h(v_{0}\cdots v_{j}v_{j+1})$ to be equal to this play, which
satisfies the properties required above.

Let $b$ be the uniform bound on the amplitude of plays in
$\mathcal{G}^{\prime}$ consistent with $\sigma^{\prime}$ starting in $v$. Now,
fix a play $\rho$ in $\mathcal{G}$ starting in $v$ and consistent with
$\sigma$. Furthermore, let $\rho^{\prime}$ be the limit of the $h(\pi)$ for
increasing prefixes of $\rho$. By construction, $\rho^{\prime}$ starts in $v$
as well and is consistent with $\sigma^{\prime}$. Hence, $\rho^{\prime}$
visits infinitely many vertices from $V$ and never gets stuck in a self-loop
throwing away energy. This implies $f(\rho^{\prime})=\rho$. Furthermore, as
$\rho^{\prime}$ satisfies the parity condition, $\rho$ does as well: the
colors removed by applying $f$ are inconsequential in this situation.

Let $\pi_{j}$ be the prefix of length $j$ of $\rho$. A straightforward
induction proves that the energy level of $\pi_{j}$ is greater or equal to
that of $h(\pi_{j})$. As the latter is bounded from below by $b$, we conclude
that $\sigma$ is winning for Player $0$ in $\mathcal{G}$ from $v$ with initial
credit $b$.

Now, we turn $\mathcal{G}^{\prime}$ into a bounded parity game with weights.
In such a game, the cost-of-response of every request has to be bounded, but
the overall energy level of the play may still diverge to $-\infty$. To rule
this out, we open one unanswerable request at the beginning of each play,
which has to be unanswered with finite cost in order to satisfy the bounded
parity condition with weights. If this is the case, then the energy level of
the play is always in a bounded corridor, i.e., we obtain a corridor-winning
strategy.

Formally, for every vertex $v\in V$, we add a vertex $\overline{v}$ to
$\mathcal{A}^{\prime}$ of an odd color $c^{*}$ that is larger than every color
in $\Omega(V)$, i.e., the request can never be answered. Furthermore,
$\overline{v}$ has a single outgoing edge to $v$ of weight $0$, i.e., it is
irrelevant whose turn it is. Call the resulting arena
$\mathcal{A}^{\prime\prime}$, the resulting coloring $\Omega^{\prime\prime}$,
and the resulting weighting $w^{\prime\prime}$, and let
$\mathcal{G}^{\prime\prime}=(\mathcal{A}^{\prime\prime},\mathrm{BndWeightParity}(\Omega^{\prime\prime},w^{\prime\prime}))$.

######  Lemma 21.

Let $\mathcal{G}^{\prime}$ and $\mathcal{G}^{\prime\prime}$ be as above and
let $v\in V$. Player $0$ has a corridor-winning strategy for
$\mathcal{G}^{\prime}$ from $v$ if and only if
$\overline{v}\in\mathcal{W}_{0}(\mathcal{G}^{\prime\prime})$.

######  Proof 8.2.

We again first show the direction from right to left. To this end, let
$\sigma^{\prime}$ be a corridor-winning strategy for Player $0$ in
$\mathcal{G}^{\prime}$ from $v$. Further, let $b$ be the corresponding uniform
bound on the amplitude of plays that start in $v$ and are consistent with
$\sigma^{\prime}$. We define a strategy $\sigma^{\prime\prime}$ for Player $0$
from $\overline{v}$ via
$\sigma^{\prime\prime}(\overline{v}\pi)=\sigma^{\prime}(\pi)$.

Let $\overline{v}\rho$ be a play that is consistent with
$\sigma^{\prime\prime}$. By construction, $\rho$ starts in $v$ and is
consistent with $\sigma^{\prime}$. Hence, it satisfies the parity condition
and its amplitude is bounded by $b$. Thus, almost all requests in $\rho$ are
answered with cost at most $b$ and there is no unanswered request of infinite
cost. This implies that $\overline{v}\rho$ satisfies the bounded parity
condition with weights. Hence,
$\overline{v}\in\mathcal{W}_{0}(\mathcal{G}^{\prime\prime})$.

We now show the obverse direction of the lemma. To this end, let
$\sigma^{\prime\prime}$ and $b$ be a winning strategy for Player $0$ in
$\mathcal{G}^{\prime\prime}$ from $\overline{v}$ and a bound such that every
request in a play starting in $\overline{v}$ and consistent with
$\sigma^{\prime\prime}$ is answered or unanswered with cost at most $b$. Due
to Corollary 13, such a strategy $\sigma^{\prime\prime}$ exists. We define a
strategy $\sigma^{\prime}$ for Player $0$ from $v$ in $\mathcal{G}^{\prime}$
via $\sigma^{\prime}(\pi)=\sigma^{\prime\prime}(\overline{v}\pi)$.

Let $\rho$ be a play starting in $v$ that is consistent with
$\sigma^{\prime}$. By construction, $\overline{v}\rho$ is consistent with
$\sigma^{\prime\prime}$. Hence, $\overline{v}\rho$ satisfies the parity
condition and every request is answered or unanswered with cost at most $b$.
In particular, this holds true for the unanswered request posed by visiting
$\overline{v}$. Hence, the amplitude of $\overline{v}\rho$ (and thus also that
of $\rho$) is bounded by $b$.

Thus, $\rho$ satisfies the parity condition and the energy level of all its
prefixes is between $-b$ and $b$. As $\rho$ is picked arbitrarily, we have
that $\sigma^{\prime}$ is corridor-winning from $v$.

###  8.2. From Bounded Parity Games with Weights to Parity Games with Weights

Next, we show how to turn a bounded parity game with weights into a parity
game with weights so that solving the latter also solves the former. The
construction here uses the same restarting mechanism that underlies the proof
of Lemma 1: as soon as a request has incurred a cost of $b$, restart the play
and enforce a request of cost $b+1$, and so on. Unlike the proof of Lemma 1,
however, where Player $1$ could restart the play at any vertex, here we always
have to return to a fixed initial vertex we are interested in. While
resetting, we have to answer all requests in order to prevent Player $1$ to
use the reset to prevent requests from being answered. Assume $v^{*}\in V$ is
the initial vertex we are interested in. Then, we subdivide every edge in to
allow Player $1$ to restart the play by answering all open requests and then
moving back to $v^{*}$.

Formally, fix a bounded parity game with weights
$\mathcal{G}=(\mathcal{A},\mathrm{BndWeightParity}(\Omega,w))$ with
$\mathcal{A}=(V,V_{0},V_{1},E)$ and a vertex $v^{*}\in V$. We define the
parity game with weights
$\mathcal{G}_{v^{*}}=(\mathcal{A}_{v^{*}},\mathrm{WeightParity}(\Omega_{v^{*}},w_{v^{*}}))$
with
$\mathcal{A}_{v^{*}}=(V^{\prime},V_{0}^{\prime},V_{1}^{\prime},E^{\prime})$
where

  * •

$V^{\prime}=V\cup E\cup\\{\top\\}$, $V_{0}^{\prime}=V_{0}$, and
$V_{1}^{\prime}=V_{1}\cup E\cup\\{\top\\}$,

  * •

$E^{\prime}=\\{(v,e),(e,\top),(e,v^{\prime})\mid e=(v,v^{\prime})\in
E\\}\cup\\{(\top,v^{*})\\}$,

  * •

$\Omega_{v^{*}}(v)=\Omega(v)$, $\Omega_{v^{*}}(e)=0$ for every $e\in E$, and
$\Omega_{v^{*}}(\top)=2\max(\Omega(V))$, and

  * •

$w_{v^{*}}(v,e)=w(e)$ for $(v,e)\in V\times E$ and $w_{v^{*}}(e^{\prime})=0$
for every other edge $e^{\prime}\in E^{\prime}$.

######  Lemma 22.

Let $\mathcal{G}$ and $\mathcal{G}_{v^{*}}$ as above. Then,
$v^{*}\in\mathcal{W}_{0}(\mathcal{G})$ if and only if
$v^{*}\in\mathcal{W}_{0}(\mathcal{G}_{v^{*}})$.

######  Proof 8.3.

First, we show the direction from left to right. To this end, let $\sigma$ be
a winning strategy for Player $0$ for $\mathcal{G}$ from $v^{*}$ such that
there is a $b$, such that every request in a play that starts in $v^{*}$ and
is consistent with $\sigma$ is answered or unanswered with cost at most $b$.
Due to Corollary 13, such a strategy $\sigma$ exists.

We define a winning strategy $\sigma^{\prime}$ for Player $0$ from $v^{*}$ in
$\mathcal{G}^{\prime}_{v^{*}}$ as follows: Given a play or a play prefix
$\pi^{\prime}$ in $\mathcal{A}_{v^{*}}$ that does not end in vertex $\top$,
let $(\pi^{\prime})$ be the longest suffix of $\pi^{\prime}$ that does not
contain $\top$. Hence, if $\pi^{\prime}$ starts in $v^{*}$, then
$(\pi^{\prime})$ starts in $v^{*}$ as well, as $v^{*}$ is the unique successor