of $\top$. Further, let $f\colon{(V\cup E)}^{*}\cup{(V\cup
E)}^{\omega}\rightarrow V^{*}\cup V^{\omega}$ be the homomorphism induced by
$f(v)=v$ for $v\in V$ and $f(e)=\varepsilon$ for $e\in E$. Now, if
$\pi^{\prime}$ is a play (prefix) in $\mathcal{A}_{v^{*}}$ that does not visit
$\top$, then $f(\pi^{\prime})$ is a play (prefix) in $\mathcal{A}$ of the same
weight that induces the same sequence of colors (save for the occurrences of
the inconsequential minimal color zero at the vertices from $E$ that are
deleted by $f$).

Let $\pi^{\prime}$ be a play prefix in $\mathcal{A}_{v^{*}}$ that ends in a
vertex $v\in V_{0}^{\prime}=V_{0}$. We define
$\sigma^{\prime}(\pi^{\prime})=(v,\sigma(f((\pi^{\prime}))))$ and show that
$\sigma^{\prime}$ is winning for Player $0$ in $\mathcal{G}_{v^{*}}$ from
$v^{*}$. To this end, let $\rho^{\prime}$ be a play in $\mathcal{A}_{v^{*}}$
starting in $v^{*}$ that is consistent with $\sigma^{\prime}$. We consider two
cases, depending on whether or not the play $\rho^{\prime}$ visits the vertex
$\top$ infinitely often.

If $\rho^{\prime}$ visits $\top$ only finitely often, then $(\rho^{\prime})$
is an infinite play in $\mathcal{G}^{\prime}_{v^{*}}$ starting in $v^{*}$. By
definition of $f$ and construction of $\sigma^{\prime}$, the infinite play
$f((\rho^{\prime}))$ in $\mathcal{A}$ starts in $v^{*}$ and is consistent with
$\sigma$. Hence, $f((\rho^{\prime}))$ satisfies the bounded parity condition
with weights. Since this condition strengthens the parity condition with
weights and since the latter condition is $0$-extendable, we conclude that
$f(\rho^{\prime})$ satisfies the parity condition with weights as well. This,
in turn, implies that the complete play $\rho^{\prime}$ satisfies the parity
condition with weights due to the construction of $\mathcal{A}_{v^{*}}$

Now, assume that the play $\rho^{\prime}$ visits $\top$ infinitely often.
Then, $\rho^{\prime}$ is of the form
$\pi_{0}^{\prime}\top\pi_{1}^{\prime}\top\pi_{2}^{\prime}\top\cdots$, where
none of the $\pi_{j}^{\prime}$ visits $\top$. Hence, by definition of
$\mathcal{A}^{\prime}$, $f$, and $\sigma^{\prime}$, each play prefix
$f(\pi_{j}^{\prime})$ in $\mathcal{A}$ starts in $v^{*}$ and is consistent
with $\sigma$. Furthermore, every request in each $\pi_{j}^{\prime}$ is
answered by the next visit to the vertex $\top$ at the latest, i.e.,
$\rho^{\prime}$ satisfies the parity condition. Thus, it suffices to show that
the cost-of-response of all requests in $\rho^{\prime}$ is bounded. This
follows immediately from the fact that $\sigma$ only admits answered or
unanswered requests of cost at most $b$ when starting in $v^{*}$ and that each
$f(\pi_{j}^{\prime})$ starts in $v^{*}$ and is consistent with $\sigma$. This
property is inherited by the $\pi_{j}^{\prime}$ due to the construction of
$\mathcal{A}_{v^{*}}$. Thus, $\rho^{\prime}$ satisfies the parity condition
with weights, i.e., $\sigma^{\prime}$ is indeed winning for Player $0$ from
$v^{*}$.

To show the direction from right to left, we proceed by contraposition. Due to
the determinacy of both games, it suffices to show that
$v^{*}\in\mathcal{W}_{1}(\mathcal{G})$ implies
$v^{*}\in\mathcal{W}_{1}(\mathcal{G}_{v^{*}})$. Hence, let $\tau$ be a winning
strategy for Player $1$ in $\mathcal{G}$ from $v$. Further, let and $f$ be
defined as above.

Now, we define a strategy $\tau^{\prime}$ for Player $1$ from $v^{*}$ in
$\mathcal{G}_{v^{*}}$ that is controlled by a counter $\kappa$, which is
initialized with zero, and which is incremented during a play every time the
costs of some request exceed $\kappa$. We construct our strategy such that
each time $\kappa$ is updated, Player $1$ restarts the play by moving to
$\top$ and then to $v^{*}$.

Assume we have a play prefix $\pi^{\prime}$ in $\mathcal{A}_{v^{*}}$ that ends
in a vertex of Player $1$ and have to define $\tau^{\prime}(\pi^{\prime})$. We
consider several cases depending on the last vertex of $\pi^{\prime}$. If
$\pi^{\prime}$ ends in $\top$, then we define
$\tau^{\prime}(\pi^{\prime})=v^{*}$, which is the only successor of $\top$.

If $\pi^{\prime}$ ends in $v\in V_{1}\subseteq V_{1}^{\prime}$, then we define
$\tau^{\prime}(\pi^{\prime})=(v,\tau(f((\pi^{\prime}))))$, i.e., we discard
everything up to and including the last occurrence of $\top$. Finally, if
$\pi^{\prime}$ ends in $e=(v,v^{\prime})\in E\subseteq V_{1}^{\prime}$, then
we consider two cases. Let $\kappa$ be the current counter value. If
$(\pi^{\prime})$ contains a request such that the remaining part of
$\pi^{\prime}$ that starts at this request has amplitude greater than
$\kappa$, then we define $\tau^{\prime}(\pi^{\prime})=\top$ and increment
$\kappa$. Otherwise, we define $\tau^{\prime}(\pi^{\prime})=v^{\prime}$ and
leave $\kappa$ unchanged.

It remains to show that $\tau^{\prime}$ is winning in $\mathcal{G}_{v^{*}}$
from $v^{*}$. To this end, let $\rho^{\prime}$ be a play in
$\mathcal{G}_{v^{*}}$ that starts in ${v^{*}}$ and is consistent with
$\tau^{\prime}$. If $\rho^{\prime}$ visits $\top$ infinitely often, then
$\rho^{\prime}$ contains, for every $b\in\mathbb{N}$, a (different) request
that is answered or unanswered with cost at least $b$. Hence, $\rho^{\prime}$
violates the parity condition with costs.

Finally, if $\rho^{\prime}$ visits $\top$ only finitely often, then there is a
$b\in\mathbb{N}$ (the final value of $\kappa$, which is incremented only
finitely often in this case) such that every request in $\rho^{\prime}$ is
answered or unanswered with cost at most $b$. Furthermore, let $\rho$ be the
suffix of $\rho^{\prime}$ that starts after the last occurrence of $\top$. As
in the previous case, $f(\rho)$ is a play in $\mathcal{A}$ that starts in
$v^{*}$ and is consistent with $\tau$. As $\rho$ and $f(\rho)$ have
essentially the same evolution of the weights (save for the removed edges of
weight zero) and the same color sequence (save for the removed vertices of
color zero), every request in $f(\rho)$ is answered or unanswered with cost at
most $b$. However, as $\rho$ is consistent with $\tau$, it violates the
bounded parity condition with weights. This is, in this situation, only
possible by violating the parity condition. Hence $\rho$, and thus also
$\rho^{\prime}$, violates the parity condition as well. Therefore,
$\rho^{\prime}$ in particular violates the parity condition with weights.

In both cases, $\rho^{\prime}$ is winning for Player $1$, i.e.,
$\tau^{\prime}$ has the desired properties.

###  8.3. Relation to Mean-Payoff Parity Games

Recall that we have shown in Section 4 and Section 5 how to solve parity games
with weights by solving polynomially many energy parity games of polynomial
size. Subsequently, in Section 8.1 and Section 8.2 we have shown the converse
direction, i.e., how to solve energy parity games by solving polynomially many
parity games with weights, again of polynomial size. In summary, we have shown
the problem of solving parity games with weights and that of solving energy
parity games with weights to be polynomial time equivalent.

Due to this strong connection between the two games, we moreover obtain a
connection to another widely used class of games, so-called mean-payoff parity
games as introduced by Chatterjee, Henzinger, and Jurdziński [CHJ05]. A mean-
payoff parity game is played on a colored arena with weights. It is the task
of Player $0$ to not only satisfy the parity condition induced by the
coloring, but also to ensure that the average weight of the traversed edges is
nonnegative. Formally, given an arena with vertex set $V$ and set of edges
$E$, a coloring $\Omega$ of $V$, and a weight function $w$ over $E$, the mean-
payoff parity condition is defined as

$\mathrm{MeanPayoffParity}(\Omega,w)=\\{v_{0}v_{1}v_{2}\cdots\in
V^{\omega}\mid\liminf_{j\rightarrow\infty}\frac{1}{j}w(v_{0}\cdots v_{j})\geq
0\\}\cap\mathrm{Parity}(\Omega)\enspace.$

A game $(\mathcal{A},\mathrm{MeanPayoffParity}(\Omega,w))$ is called a mean-
payoff parity game.

Chatterjee and Doyen [CD12] showed that the problem of solving energy parity
games and that of solving mean-payoff parity games are logarithmic space
equivalent. [[CD12]] Let
$\mathcal{G}=(\mathcal{A},\mathrm{MeanPayoffParity}(\Omega,w))$ be a mean-
payoff parity game with $n$ vertices and let
$\mathcal{G}^{\prime}=(\mathcal{A},\mathrm{EnergyParity}(\Omega,w^{\prime}))$,
where $w^{\prime}(e)=w(e)+\frac{1}{1+n}$ for all edges $e$ of $\mathcal{A}$.
Then $\mathcal{W}_{0}(\mathcal{G})=\mathcal{W}_{0}(\mathcal{G}^{\prime})$.

Hence, we can use the techniques underlying Theorem 5 to reduce the problem of
solving parity games with weights to the problem of solving mean-payoff parity
games. In fact, it is Proposition 8.3 that underpins the proof of the second
part of Proposition 5.1, i.e., the proof that energy parity games can be
solved in pseudo-quasi-polynomial time.

######  Corollary 23.

The following decision problems are polynomial time equivalent:

> Given a parity game with weights $\mathcal{G}$ and a vertex $v$ of
> $\mathcal{G}$, does Player $0$ have a winning strategy from $v$ in
> $\mathcal{G}$?

> Given a mean-payoff parity game $\mathcal{G}$ and a vertex $v$ of
> $\mathcal{G}$, does Player $0$ have a winning strategy from $v$ in
> $\mathcal{G}$?

Solving parity games with weights by iteratively solving mean-payoff parity
games as sketched above, however, does not allow us to obtain the memory
bounds from Theorem 14. This is due to Player $0$, in general, requiring
infinite memory in order to win a mean-payoff parity game [CHJ05].

##  9\. The Threshold Problem

In Section 3, we have defined parity games with weights as a generalization of
parity games with costs. Up to this point, we have only considered the problem
of solving parity games with weights, i.e., deciding for a given parity game
with weights $\mathcal{G}$ and a vertex $v$ of $\mathcal{G}$, whether Player
$0$ has a strategy $\sigma$ such that all plays $\rho$ starting in $v$ and
consistent with $\sigma$ satisfy
$\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)<\infty$. We have shown this
problem to be a member of $\textsc{NP}\cap\textsc{co-NP}$ and that it can be
solved in pseudo-quasi-polynomial time.

While our algorithm for deciding the above decision problem yields a strategy
witnessing the ability of Player $0$ to eventually ensure a finite cost-of-
response, it does not provide any guarantee on the “quality” of the strategy
beyond the very general bound $b\in\mathcal{O}({(ndW)}^{2})$ due to Theorem
17. In particular, it may be the case that there exists a strategy
$\sigma^{\prime}$ such that all plays $\rho$ starting in $v$ and consistent
with $\sigma$ satisfy $\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)\leq
b^{\prime}<b$. Hence, in this section, we investigate the so-called threshold
problem for parity game with weights, i.e., the problem to decide, given a
parity game with weights $\mathcal{G}$, a vertex $v$ of $\mathcal{G}$, and a
bound $b\in\mathbb{N}$, whether there exists a strategy $\sigma$ for Player
$0$ such that for all plays $\rho$ starting in $v$ and consistent with
$\sigma$ satisfy $\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)\leq b$.

Weinert and Zimmermann [WZ17] have shown that the threshold problem for
finitary parity games as well as for parity games with costs is PSpace-
complete and that exponential memory is both necessary and sufficient for both
players to implement witnessing strategies. In this work, we show that the
threshold problem for parity games with weights is ExpTime-complete and that
the memory bounds remain unchanged in comparison to the case of parity games
with costs.

In order to simplify notation for the remainder of this section, if
$\mathcal{G}$ is clear from the context, for a given strategy $\sigma$ for
Player $0$ and a vertex $v$ of $\mathcal{G}$ we define

$\mathrm{Cost}_{v}(\sigma)=\sup_{\rho}\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)\enspace,$

where $\rho$ ranges over all plays $\rho$ of $\mathcal{G}$ that start in $v$
and that are consistent with $\sigma$. Dually, for a strategy $\tau$ for
Player $1$ and a vertex $v$, we define
$\mathrm{Cost}_{v}(\tau)=\inf_{\rho}\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)$,
where $\rho$ ranges over all plays $\rho$ of $\mathcal{G}$ that start in $v$
and that are consistent with $\tau$.

######  Remark 24.

Let $\sigma$ be a strategy for Player $0$, let $\tau$ be a strategy for Player
$1$, and let $v$ be a vertex. Then,
$\mathrm{Cost}_{v}(\sigma)\geq\mathrm{Cost}_{v}(\tau)$.

The main theorem of this section settles the complexity of the threshold
problem for parity games with weights.

######  Theorem 25.

The following decision problem is ExpTime-complete:

> Given a parity game with weights $\mathcal{G}$, some vertex $v$ of
> $\mathcal{G}$, and a bound $b\in\mathbb{N}$, does Player $0$ have a strategy
> $\sigma$ with $\mathrm{Cost}_{v}(\sigma)\leq b$ in $\mathcal{G}$?

The remainder of this section is organized as follows: First, in Section 9.1
we show the threshold problem for parity games with weights to be in ExpTime,
before showing ExpTime-hardness of the problem in Section 9.2. We conclude
this section by showing tight bounds on the memory requirements of witnessing
strategies for both players in Section 9.3.

###  9.1. ExpTime-Membership

In order to solve the threshold problem for parity games with weights, we
follow the approach used by Weinert and Zimmermann [WZ17] to solve the same
problem for parity games with costs. Given a parity game with costs
$\mathcal{G}$ and a threshold $b$, they construct a classical parity game
$\mathcal{G}_{b}$ that satisfies the following property:

> Player $0$ has a strategy of cost at most $b$ from some vertex $v$ in
> $\mathcal{G}$ if and only if he has a winning strategy from some designated
> vertex $v^{\prime}$ in $\mathcal{G}_{b}$.

We show how to lift the construction of Weinert and Zimmermann to the setting
of parity games with weights and show that this construction yields ExpTime-
membership of the threshold problem for parity games with weights. For the
remainder of this section, we fix some parity game with weights $\mathcal{G}$
with $n$ vertices, $d$ odd colors and a threshold $b\in\mathbb{N}$.

The idea behind the construction of $\mathcal{G}_{b}$ is to track, for each
odd color $c$ of $\mathcal{G}$, an overapproximation of the costs incurred by
all open requests for $c$ in the current play prefix. The authors then showed
that, if Player $1$ is able to violate the bound $b$ at least $n$ times, then
she can do so infinitely often. Thus, by additionally equipping
$\mathcal{G}_{b}$ with an $n$-bounded counter that counts the number of
violations of the given threshold, we obtain the desired property given above.

Recall that, in parity games with costs, all weights are nonnegative. Hence,
it suffices to track an upper bound on the cost of open requests, as these
costs are implicitly bounded from below by zero. In the setting of parity
games with weights, in contrast, we have to track both an upper as well as a
lower bound on the cost of open requests. To this end, we first define the set
of intervals

$I=\\{(l,h)\mid-b\leq l\leq h\leq b\\}\enspace.$

Clearly, we have

$|I|=(2b+1)+\cdots+1=(2b+1)(2b+2)/2=(4b^{2}+4b+2b+2)/2=2b^{2}+3b+1\enspace.$

Using the set of intervals, we now define request functions that enable the
overapproximation of the costs of open requests described above. To this end,
we denote the set of odd colors occurring in $\mathcal{G}$ by $D$. A
($b$-bounded) request function $r\colon D\rightarrow\\{\bot\\}\cup I$ is a
function mapping each odd color of $\mathcal{G}$ either to

  * •

$\bot$, denoting that currently no request for color $c$ is open, or to

  * •

some $(l,h)\in I$, denoting that

    * –

there exists an open request for color $c$ that has accumulated weight $l$,
that

    * –

there exists an open request for color $c$ that has accumulated weight $h$,
and that

    * –

all requests for color $c$ have accumulated weight at least $l$ and at most
$h$.

Given some request function $r$, we define the lower and upper residual
request functions $r_{\downarrow}$ and $r_{\uparrow}$ as $r_{\downarrow}(c)=l$
and $r_{\uparrow}(c)=h$, if $r(c)=(l,h)$, and as
$r_{\downarrow}(c)=r_{\uparrow}(c)=\bot$ if $r(c)=\bot$. We write $R$ to
denote the set of all request functions. We have
$|R|={(|I|+1)}^{|D|}={(2b^{2}+3b+2)}^{d}$, i.e., there exist exponentially
many request functions when measured in the size of the game $\mathcal{G}$,
but only polynomially many when measured in the bound $b$.

As stated above, Weinert and Zimmermann [WZ17] showed that it suffices for
Player $1$ to violate the threshold $b$ $n$ times in order to witness that she
can do so infinitely often. Hence, we now define a memory structure comprising
request functions and an “overflow counter” that, together with the game
$\mathcal{G}$, induces the desired parity game $\mathcal{G}_{b}$.

Recall that we fixed some parity game with weights $\mathcal{G}$ with $n$
vertices and $d$ odd colors as well as a bound $b\in\mathbb{N}$. Using the set
$R$ of request functions defined above, we define the set of memory states
$M=\\{0,\dots,n\\}\times R$. As we aim to track the cost of open requests
using the functions from $R$, we define the initial memory element
$\text{init}(v)=(0,r_{v})$, where $r_{v}$ is defined as

$r_{v}(c)=\begin{cases}(0,0)&\text{if $\Omega(v)$ is odd and $c=\Omega(v)$,
and}\\\ \bot&\text{otherwise.}\end{cases}$

We define the update function $\mathrm{upd}\colon M\times E\rightarrow M$
implementing the above intuition. Let $m=(o,r)\in M$ and let
$e=(v,v^{\prime})\in E$ with $w(e)=w$. This update function updates the memory
state via $\mathrm{upd}(m,e)=(o^{\prime},r^{\prime})$ by performing the
following steps in order:

Weight:

First, we resolve the effect of traversing the edge $e$ with weight $w$ by
defining $r^{\prime}_{\mathit{I}}$ as

$r^{\prime}_{\mathit{I}}(c)=\begin{cases}(r_{\downarrow}(c)+w(e),r_{\uparrow}(c)+w(e))&\text{if~{}$r(c)\neq\bot$,
and}\\\ \bot&\text{otherwise.}\end{cases}$

Overflow:

In a second step, we check whether some request has violated the bound $b$
during the move to $v^{\prime}$ and update the overflow counter if this is the
case. Thus, if there exists a color $c$ such that either
${(r^{\prime}_{\mathit{I}})}_{\downarrow}(c)<-b$ or
${(r^{\prime}_{\mathit{I}})}_{\uparrow}(c)>b$, then we define
$r^{\prime}_{\mathit{II}}(c)=\bot$ for all $c\in D$ and set $o^{\prime}$ to
the minimum of $o+1$ and $n$. Otherwise, we define
$r^{\prime}_{\mathit{II}}=r^{\prime}_{\mathit{I}}$ and $o^{\prime}=o$.

Request:

Finally, we resolve the effect of moving to the vertex $v^{\prime}$ with color
$\Omega(v^{\prime})$ as follows: If $\Omega(v^{\prime})$ is even, then we
define

$r^{\prime}_{\mathit{III}}(c)=\begin{cases}\bot&\text{if
$c\leq\Omega(v^{\prime})$, and}\\\
r^{\prime}_{\mathit{II}}(c)&\text{otherwise.}\end{cases}$

If, however, $\Omega(v^{\prime})$ is odd, then we define

$r^{\prime}_{\mathit{III}}(c)=\begin{cases}(\min\\{{(r^{\prime}_{\mathit{II}})}_{\downarrow}(\Omega(v^{\prime})),0\\},\max\\{{(r^{\prime}_{\mathit{II}})}_{\uparrow}(\Omega(v^{\prime})),0\\})&\text{if
$c=\Omega(v^{\prime})$, and}\\\
r^{\prime}_{\mathit{II}}(c)&\text{otherwise.}\end{cases}$

In either case, we define $r^{\prime}=r^{\prime}_{\mathit{III}}$, which
concludes the definition of $m^{\prime}=(o^{\prime},r^{\prime})$. The
resulting $o^{\prime}$ is at most $n$ and the resulting function $r^{\prime}$
is an element of $R$. We combine these elements in the memory structure
$\mathcal{M}=(M,\text{init},\mathrm{upd})$.

Recall that throughout this section we fixed a parity game with weights
$\mathcal{G}$. Let
$\mathcal{G}=(\mathcal{A},\mathrm{WeightParity}(\Omega,w))$. We define the
($b$-)threshold game of $\mathcal{G}$

$\mathcal{G}_{b}=(\mathcal{A}^{\prime},\mathrm{Parity}(\Omega^{\prime}))\enspace,$

with
$\mathcal{A}^{\prime}=(V^{\prime},V^{\prime}_{0},V^{\prime}_{1},E^{\prime})$,
where $V^{\prime}=V\times M$, $V^{\prime}_{i}=V_{i}\times M$ for
$i\in\\{0,1\\}$, where $((v,m),(v^{\prime},m^{\prime}))\in E^{\prime}$ if and
only if $(v,v^{\prime})\in E$ and $\mathrm{upd}(m,(v,v^{\prime}))=m^{\prime}$,
and where

$\Omega^{\prime}(v,o,r)=\begin{cases}\Omega(v)&\text{if~{}$o<n$, and}\\\
1&\text{otherwise,}\end{cases}$

which concludes the definition of $\mathcal{G}_{b}$.

Via a straightforward adaptation of results by Weinert and Zimmermann [WZ17]
we obtain that this construction indeed satisfies the above property, i.e.,
that it suffices to solve $\mathcal{G}_{b}$ in order to solve the threshold
problem for $\mathcal{G}$:

######  Lemma 26.

Let $v^{*}$ be a vertex of $\mathcal{G}$. Player $0$ has a strategy $\sigma$
with $\mathrm{Cost}_{v^{*}}(\sigma)\leq b$ if and only if he wins
$\mathcal{G}_{b}$ from $(v^{*},\text{init}(v^{*}))$.

We split the proof of Lemma 26 into several lemmas. The direction from right
to left is relatively straightforward: Since $\mathcal{G}_{b}$ is a parity
game, if Player $0$ wins $\mathcal{G}_{b}$ from $(v^{*},\text{init}(v^{*}))$,
then she does so with a positional strategy $\sigma^{\prime}$. This strategy
assigns to each vertex $(v,o,r)$ of Player $0$ in $\mathcal{G}_{b}$ a unique
successor $(v^{\prime},o^{\prime},r^{\prime})$, where the values of
$o^{\prime}$ and $r^{\prime}$ are deterministic updates of $o$ and $r$ via the
update function $\mathrm{upd}$. Hence, $\sigma^{\prime}$ can be interpreted as
picking only a successor vertex $v^{\prime}$ of $v$ with respect to the
current memory state $(o,r)$. Thus, the choices of $\sigma^{\prime}$ can be
mimicked in $\mathcal{G}$.

######  Lemma 27.

If Player $0$ wins $\mathcal{G}_{b}$ from $(v^{*},\text{init}(v^{*}))$, then
she has a strategy $\sigma$ in $\mathcal{G}$ with
$\mathrm{Cost}_{v^{*}}(\sigma)\leq b$.

######  Proof 9.1.

Let $\sigma^{\prime}\colon V^{\prime}_{0}\rightarrow V^{\prime}$ be a
positional winning strategy for Player $0$ from $(v^{*},\text{init}(v^{*}))$
in $\mathcal{G}_{b}$. Since $\mathcal{G}_{b}$ is a parity game, such a
strategy exists by assumption. We define the finite-state strategy $\sigma$
for Player $0$ in $\mathcal{G}$ as the unique strategy induced by the memory
structure $\mathcal{M}$ and the next-move function $\mathrm{Nxt}$ defined as
$\mathrm{Nxt}(v,m)=v^{\prime}$, if
$\sigma^{\prime}(v,m)=(v^{\prime},m^{\prime})$ for some $m^{\prime}$. It
remains to show $\mathrm{Cost}_{v^{*}}(\sigma)\leq b$.

Let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play in $\mathcal{G}$ that begins in
$v^{*}$ and that is consistent with $\sigma$. Let

$\rho^{\prime}=(v_{0},o_{0},r_{0})(v_{1},o_{1},r_{1})(v_{2},o_{2},r_{2})\cdots$

be the unique play in $\mathcal{G}_{b}$ that satisfies both
$(o_{0},r_{0})=\text{init}(v_{0})$ as well as
$(o_{j},r_{j})=\mathrm{upd}((o_{j-1},r_{j-1}),(v_{j-1},v_{j}))$ for all $j>0$.

A straightforward induction shows that $\rho^{\prime}$ is consistent with
$\sigma^{\prime}$. As $\rho^{\prime}$ moreover starts in
$(v^{*},\text{init}(v^{*}))$ by definition, it is winning for Player $0$,
i.e., it satisfies the parity condition. This in particular implies that the
overflow counter along $\rho^{\prime}$ never saturates, i.e., that we have
$o_{j}<n$ for all $j\in\mathbb{N}$, since vertices with saturated overflow
counter form a losing sink for Player $0$. Hence, the plays $\rho$ and
$\rho^{\prime}$ coincide on their color sequences. Since $\rho^{\prime}$ is
winning for Player $0$ in $\mathcal{G}^{\prime}$, it satisfies the parity
condition, which in turn implies that $\rho$ satisfies the parity condition.
It remains to show that almost all requests in $\rho$ are answered with cost
at most $b$.

As argued above, the overflow counter along $\rho^{\prime}$ eventually
stabilizes at some value less than $n$. Moreover, since $\rho$ satisfies the
parity condition, all but finitely many requests are answered. Hence, there
exists a position $j$ such that $o_{j^{\prime}}=o_{j}<n$ and such that
$\mathrm{Cor}(\rho,j^{\prime})<\infty$ for every $j^{\prime}>j$. Assume
towards a contradiction that there exists some $j^{\prime}\geq j$ with
$b<\mathrm{Cor}(\rho,j^{\prime})<\infty$. Then, due to the construction of
$\mathcal{G}_{b}$, the overflow counter is incremented along the play
$\rho^{\prime}$ at some point after $j^{\prime}$. This, however, contradicts
the choice of $j$. Hence, we obtain that almost all requests in $\rho$ are
answered with cost at most $b$.

We now turn our attention to the other direction of the statement of Lemma 26,
i.e., we aim to show that, if Player $0$ has a strategy $\sigma$ in
$\mathcal{G}$ with $\mathrm{Cost}_{v^{*}}(\sigma)\leq b$, then she wins
$\mathcal{G}_{b}$ from $(v^{*},\text{init}(v^{*}))$. We show this claim via
contraposition: Assume that Player $0$ does not win $\mathcal{G}_{b}$ from
$(v^{*},\text{init}(v^{*}))$. Since $\mathcal{G}_{b}$ is a parity game, it is
determined. Hence, Player $1$ wins $\mathcal{G}_{b}$ from
$(v^{*},\text{init}(v^{*}))$, say with the positional strategy
$\tau^{\prime}$. Such a positional strategy for him exists again due to
$\mathcal{G}_{b}$ being a parity game. We construct a strategy $\tau$ for
Player $1$ in $\mathcal{G}$ that enforces
$\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)>b$ for each play $\rho$
starting in $v^{*}$ and consistent with $\tau$. Since this implies
$\mathrm{Cost}_{v^{*}}(\sigma)>b$ for each strategy $\sigma$ of Player $0$
(see Remark 24), this suffices to show the desired statement.

Recall that the overflow counter along each play starting in
$(v^{*},\text{init}(v^{*}))$ is monotonically increasing and bounded from
above by the number $n$ of vertices in $\mathcal{G}$. Hence, the value of the
overflow counter either stabilizes at some value less than $n$, or it
eventually saturates at value $n$. In the former case, $\tau^{\prime}$ has to
ensure that the resulting play violates the parity condition. Hence, it
suffices to mimic the moves made by $\tau^{\prime}$ in $\mathcal{G}$ ad
infinitum in this case, which results in a play with infinitely many
unanswered requests in $\mathcal{G}$. In the latter case, however, mimicking
$\tau^{\prime}$ does not yield a strategy in $\mathcal{G}$ with the desired
property, as $\tau^{\prime}$ does not necessarily prescribe “meaningful” moves
in $\mathcal{G}_{b}$ once the overflow counter saturates. This is due to the
fact that these vertices form a sink component that is trivially winning for
Player $1$. In order to leverage $\tau^{\prime}$ even after saturation of the
overflow counter, we intervene whenever the overflow counter is incremented,
by resetting it to the smallest possible value from which $\tau^{\prime}$ is
still winning, thereby ensuring that the sink component is never reached.
Hence, the strategy always mimics “meaningful” moves in $\mathcal{G}_{b}$.

Formally, we define the set $\mathcal{R}$ that contains all vertices $(v,o,r)$
that are visited by some play that starts in $(v^{*},\text{init}(v^{*}))$ and
that is consistent with $\tau^{\prime}$. Recall that we defined $r_{v}$ as the
function denoting the requests opened by visiting the vertex $v$. Given a
vertex $v$, we then define
$o_{v}=\min(\\{n\\}\cup\\{o\mid(v,o,r_{v})\in\mathcal{R}\\})$. In particular,
we have $o_{v^{*}}=0$, since
$(v^{*},\text{init}(v^{*}))=(v^{*},0,r_{v})\in\mathcal{R}$.

######  Lemma 28.

The strategy $\tau^{\prime}$ is winning for Player $1$ from $(v,o_{v},r_{v})$
in $\mathcal{G}_{b}$ for all $v\in V$.

######  Proof 9.2.

If $o_{v}=n$, then all plays starting in $(v,o_{v},r_{v})$ violate the parity
condition by construction of the arena of $\mathcal{G}_{b}$. Thus, for the
remainder of this proof, assume $o_{v}<n$. Let $(v,o_{v},r_{v})\rho$ be a play
starting in $(v,o_{v},r_{v})$ that is consistent with $\tau^{\prime}$.
Moreover, let $\pi$ be a play prefix starting in $(v^{*},\text{init}(v^{*}))$,
consistent with $\tau^{\prime}$, and ending in $(v,o_{v},r_{v})$. Such a play
prefix exists due to the definition of $o_{v}$ and due to the assumption of
$o_{v}<n$, which implies $(v,o_{v},r_{v})\in\mathcal{R}$.

Since $\tau^{\prime}$ is positional, the play $\pi\rho$ starts in
$(v^{*},\text{init}(v^{*}))$ and is consistent with $\tau^{\prime}$. Thus,
$\pi\rho$ violates the parity condition, which implies that $\rho$ violates
the parity condition due to prefix-independence.

We now define a new memory structure $\mathcal{M}^{\prime}$ implementing the
strategy $\tau$. Recall that we defined the memory structure
$\mathcal{M}=(M,\text{init},\mathrm{upd})$ during the construction of the
threshold game $\mathcal{G}_{b}$. Using the components of that memory
structure, we define $M^{\prime}=M=\\{0,\ldots,n\\}\times R$,
$\text{init}^{\prime}=\text{init}$, and

$\mathrm{upd}^{\prime}((o,r),(v,v^{\prime}))=\begin{cases}(o,r^{\prime})&\text{if
$\mathrm{upd}((o,r),(v,v^{\prime}))=(o,r^{\prime})$, and}\\\
(o_{v^{\prime}},r^{\prime})&\text{if
$\mathrm{upd}((o,r),(v,v^{\prime}))=(o+1,r^{\prime})$.}\\\ \end{cases}$

and combine these elements into the memory structure
$\mathcal{M}^{\prime}=(M^{\prime},\text{init}^{\prime},\mathrm{upd}^{\prime})$.

In the second case of the definition of $\mathrm{upd}^{\prime}$, we have
$r^{\prime}=r_{v^{\prime}}$ by definition of $\mathrm{upd}$. Finally, we
define the next-move function $\mathrm{Nxt}^{\prime}$ via
$\mathrm{Nxt}^{\prime}(v,m)=v^{\prime}$, if
$\tau^{\prime}(v,m)=(v^{\prime},m^{\prime})$ for some $m^{\prime}\in M$ and
let $\tau$ be the finite-state strategy implemented by $\mathcal{M}^{\prime}$
and $\mathrm{Nxt}^{\prime}$. We claim that for each play $\rho$ starting in
$v^{*}$ that is consistent with $\tau$ we have
$\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)>b$.

To show this claim, let $\rho=v_{0}v_{1}v_{2}\cdots$ be some play in
$\mathcal{G}$ that starts in $v^{*}$ and that is consistent with $\tau$.
Moreover, let

$\rho^{\prime}=(v_{0},o_{0},r_{0})(v_{1},o_{1},r_{1})(v_{2},o_{2},r_{2})\cdots$

be the unique play in $\mathcal{A}\times\mathcal{M}^{\prime}$ that satisfies
$(o_{0},r_{0})=\text{init}^{\prime}(v_{0})$ as well as
$(o_{j},r_{j})=\mathrm{upd}^{\prime}((o_{j-1},r_{j-1}),(v_{j-1},v_{j}))$ for
all $j>0$. We say that $j$ is a reset position if $j=0$ or if

$\mathrm{upd}((o_{j-1},r_{j-1}),(v_{j-1},v_{j}))=(o_{j-1}+1,r_{j})\enspace,$

i.e., if the second case in the definition of $\mathrm{upd}^{\prime}$ is
applied.

The play $\rho^{\prime}$ is not necessarily a play in $\mathcal{G}_{b}$, since
$\mathcal{G}_{b}$ is defined with respect to $\mathcal{M}$ instead of
$\mathcal{M}^{\prime}$, but every infix of $\rho^{\prime}$ that starts at a
reset position and does not contain another one, is a play infix in
$\mathcal{G}_{b}$ that is consistent with $\tau^{\prime}$. At every reset
position, instead of incrementing the overflow counter, we set it to $o_{v}$.

Via a straightforward induction leveraging the same arguments as Weinert and
Zimmermann [WZ17] we obtain $o_{j}<n$ for all $j\in\mathbb{N}$, i.e., the
overflow counter along $\rho^{\prime}$ never saturates. Intuitively, this
implies that the strategy $\tau$ always uses “meaningful” moves of
$\tau^{\prime}$ for its choice of move and thus allows us to subsequently
argue that $\tau$ is indeed winning for Player $1$. Moreover, while the set
$M^{\prime}$ of memory states as defined above is of size $(n+1)|R|$, the
above observation allows us to implement the strategy $\tau^{\prime}$ using a
set of memory states of size $n|R|$ by omitting the memory states indicating a
saturated overflow counter.

It remains to show that we indeed have
$\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)>b$. As argued above, this
then directly implies $\mathrm{Cost}_{v^{*}}(\sigma)>b$ for each strategy
$\sigma$ of Player $0$, concluding the proof of the direction from left to
right of Lemma 26.

######  Proof 9.3 (Proof of Lemma 26).

The direction from right to left is encapsulated in Lemma 27.

For the direction from left to right, recall that we defined a strategy $\tau$
for Player $1$, that we picked $\rho$ beginning in $v^{*}$ and consistent with
$\tau$ arbitrarily and that we defined
$\rho^{\prime}=(v_{0},o_{0},r_{0})(v_{1},o_{1},r_{1})(v_{2},o_{2},r_{2})\cdots$.
First assume that the overflow counter of $\rho^{\prime}$ eventually
stabilizes, i.e., there exists some $j\in\mathbb{N}$ such that
$o_{j^{\prime}}=o_{j}$ for all $j^{\prime}>j$. Then, there exists a suffix of
$\rho^{\prime}$ that is consistent with $\tau^{\prime}$, which therefore
violates the parity condition. Hence, it suffices to note that the color
sequences induced by $\rho^{\prime}$ and by $\rho$ coincide in this case since
the overflow counter along $\rho^{\prime}$ never saturates as argued above,
and due to the construction of $\mathcal{G}_{b}$, in which vertices of the
form $(v,o,r)$ inherit the coloring of the vertex $v$ for $o<n$. Thus, $\rho$
violates the parity condition and, in turn, also the parity condition with
weights with respect to any bound.

Now assume that the overflow counter of $\rho^{\prime}$ does not stabilize.
Then, there are infinitely many reset positions in $\rho^{\prime}$. We obtain
that there exist a request that incurs cost greater than $b$ between any two
adjacent such positions as a direct consequence of the construction of the
arena of $\mathcal{G}_{b}$. Hence, we obtain
$\limsup_{j\rightarrow\infty}\mathrm{Cor}(\rho,j)>b$, which concludes this
direction of the proof.

Lemma 26 allows us to decide the threshold problem for a parity game with
weights with $n$ vertices and $d$ odd colors by solving a classical parity
game of size $\mathcal{O}(nb^{d})$, i.e., the size of the parity game depends
on both the size of the parity game with weights as well as the threshold.
Lemma 18, however, allows us to bound the parameter $b$: If $b$ is at least
$nd(6n)(d+1)(W+1)W$, then solving the threshold problem reduces to solving the
parity game with weights. We formalize these observations as Algorithm 3.

0: Parity game with weights $\mathcal{G}$ with $n$ vertices, $d$ odd colors,
and largest absolute weight $W$, vertex $v$ of $\mathcal{G}$, bound
$b\in\mathbb{N}$.

1: if $b\geq nd(6n)(d+1)(W+1)W$ then

2: return $v\in\mathcal{W}_{0}(\mathcal{G})$ /* Requires solving
$\mathcal{G}$, e.g. via Algorithm 1 */

3: else

4: $\mathcal{G}_{b}=\text{$b$-threshold game of~{}$\mathcal{G}$}$ /*
$\mathcal{G}_{b}$ is explicitly constructed */

5: return $(v,0,r_{v})\in\mathcal{W}_{0}(\mathcal{G}_{b})$ /* Requires solving
$\mathcal{G}_{b}$ */

6: end if

Algorithm 3 An algorithm deciding whether or not Player $0$ has a strategy
$\sigma$ with $\mathrm{Cost}_{v}(\sigma)\leq b$ in a parity game with weights
$\mathcal{G}$.

Recall that our aim in this section is to argue that the threshold problem for
parity games with weights is in ExpTime. To this end, we have constructed
Algorithm 3, the correctness of which follows directly from Lemma 26. It
remains to argue that this algorithm runs in exponential time.

To this end, recall that parity games can be solved in polynomial time in the
number of vertices and in exponential time in the number of odd colors [Jur98,
CJK+17]. Moreover, recall that the ($b$-)threshold game $\mathcal{G}_{b}$ has
$\mathcal{O}(nb^{d})$ many vertices, where $n$ and $d$ are the number of
vertices and the number of odd colors in $\mathcal{G}$, respectively. As we
are able to bound the value of $b$ from above by a polynomial in $n$, $d$, and
the largest absolute weight $W$ of $\mathcal{G}$ due to Lemma 18, we obtain
that we are able to solve $\mathcal{G}_{b}$ in exponential time, which we
formalize in the following theorem.

######  Theorem 29.

The following problem is in ExpTime:

> Given a parity game with weights $\mathcal{G}$, a vertex $v$ of
> $\mathcal{G}$, and a bound $b\in\mathbb{N}$, does Player $0$ have a strategy
> $\sigma$ with $\mathrm{Cost}_{v}(\sigma)\leq b$?

######  Proof 9.4.

We show that Algorithm 3 witnesses the claimed membership in ExpTime. The
correctness of this algorithm follows directly from Lemma 18 and Lemma 26. It
remains to show that Algorithm 3 terminates in exponential time. Let $n$ be
the number of vertices of $\mathcal{G}$, let $d$ be the number of odd colors
of $\mathcal{G}$, and let $W$ be the largest absolute weight in $\mathcal{G}$.

If $b\geq nd(6n)(d+1)(W+1)W$, then the dominating factor for the runtime of
Algorithm 3 is the call to a solver for parity games with weights in Line 2.
This solver only has to solve the given parity game with weights as discussed
in Section 4. Due to Theorem 5, the problem of solving these games is in
$\textsc{NP}\cap\textsc{co-NP}$. Since $\textsc{NP}\subseteq\textsc{ExpTime}$,
we obtain the desired runtime in this case.

If, however, $b<nd(6n)(d+2)(W+1)W$, Algorithm 3 constructs and solves the
$b$-threshold game $\mathcal{G}_{b}$ of $\mathcal{G}$ in Line 4 and Line 5,
respectively. Let $n^{\prime}$ be the number of vertices of $\mathcal{G}_{b}$.
By construction of $\mathcal{G}_{b}$ we obtain

$n^{\prime}=n|\\{0,\dots,n\\}\times
R|=n(n+1){(2b^{2}+3b+2)}^{d}\in\mathcal{O}(n^{2}b^{2d})\enspace,$

where $R$ denotes the set of request functions as defined above.

Due to our case analysis based on the cardinality of $b$ in Line 1, we
furthermore obtain $b\in\mathcal{O}(n^{2}d^{2}W)$, which in turn implies

$n^{\prime}\in\mathcal{O}(n^{2}{(n^{2}d^{2}W)}^{2d})=\mathcal{O}(n^{2+4d}d^{4d}W^{2d})\enspace.$

As we assume weights to be given in binary encoding, we additionally obtain
$W\in\mathcal{O}(2^{|\mathcal{G}|})$, which finally implies

$n^{\prime}\in\mathcal{O}(n^{2+4d}d^{4d}{(2^{|\mathcal{G}|})}^{2d})=n^{2+4d}d^{4d}{2^{2d|\mathcal{G}|}}\enspace,$

i.e., $\mathcal{G}_{b}$ contains only exponentially many vertices and
$d^{\prime}=\max\\{1,d\\}\in\mathcal{O}(d)$ many colors in terms of
$|\mathcal{G}|$. Recall that parity games can be solved in polynomial time in
the number of vertices and in exponential time in the logarithm of the number
of colors using, e.g., the recent algorithm by Calude et al. [CJK+17]. Hence,
$\mathcal{G}_{b}$ can indeed be solved in exponential time in $|\mathcal{G}|$,
which implies membership of the above problem in ExpTime.

Algorithm 3 furthermore yields an algorithm determining the optimal $b$ such
that Player $0$ has a strategy of cost at most $b$ from a given $v$: Given a
parity game with weights $\mathcal{G}$ with $n$ vertices, $d$ odd colors, and
largest absolute weight $W$, and a vertex $v$ of $\mathcal{G}$, we first solve
$\mathcal{G}$ and determine whether or not $v\in\mathcal{W}_{0}(\mathcal{G})$.
If this is not the case, then no such bound $b$ exists. Otherwise, the minimal
$b$ with the above property can be determined with a binary search over the
range $0,\dots,nd(6n)(d+1)(W+1)W$. This binary search requires deciding at
most $\log(nd(6n)(d+1)(W+1)W)$, i.e., polynomially many instances of the
threshold problem, each of which takes at most exponential time. Hence, the
optimal $b$ such that Player $0$ has a strategy of cost at most $b$ can be
determined in exponential time in the size of $\mathcal{G}$.

This concludes the proof of ExpTime-membership of the threshold problem for
parity games with weights. It remains to show that this bound is tight. To
this end, we show in the next section that the threshold problem is ExpTime-
hard via a reduction from the problem of solving countdown games.

###  9.2. ExpTime-Hardness

In the previous section we have shown ExpTime-membership of the threshold
problem for parity games with weights.

In this section we provide a matching lower bound by showing that the
threshold problem is ExpTime-complete. To this end, we reduce the ExpTime-hard
problem of solving countdown games to the threshold problem for parity games
with weights. Countdown games were introduced by Jurdziński, Laroussinie, and
Sproston [JLS08].

In a countdown game, some initial credit is fixed at the beginning of a play.
Both players then move in alternation in an arena whose edges are labeled with
negative weights. In each turn, first Player $0$ announces some weight, before
Player $1$ has to move along some edge of that weight, reducing the initial
credit by the weight of the traversed edge. If the credit at some point hits
zero, Player $0$ wins. If, however, the credit at some point turns negative,
Player $1$ wins. Since each edge has strictly negative weight, each play is
won by either player after finitely many moves.

When formulated in our framework of arenas and winning conditions, a countdown
game $\mathcal{G}=(\mathcal{A},\text{Countdown}(w,c^{*}))$ consists of an
arena $\mathcal{A}=(V,V_{0},V_{1},E)$, a weighting $w$ of $\mathcal{A}$, and
some initial credit $c^{*}\in\mathbb{N}$, which satisfies the following
conditions:

  1. (1)

There exists a designated sink vertex $v_{\bot}\in V_{1}$,

  2. (2)

we have

     * •

$E\subseteq(V_{0}\times V_{1})\cup(V_{1}\times
V_{0})\cup(\\{v_{\bot}\\}\times\\{v_{\bot}\\})$,

     * •

$V_{0}\times\\{v_{\bot}\\}\subseteq E$, and

     * •

$(v_{\bot},v_{\bot})\in E$,

  3. (3)

for each $e_{1}=(v,v^{\prime}_{1}),e_{2}=(v,v^{\prime}_{2})\in E$, with $v\in
V_{0}$ we have that $e_{1}\neq e_{2}$ implies $w(e_{1})\neq w(e_{2})$,

  4. (4)

for each $e\in E\cap(V_{0}\times V)$ we have $w(e)\begin{cases}=0&\text{if
$e\in(V_{0}\times\\{v_{\bot}\\})$, and}\\\ <0&\text{otherwise,
and}\end{cases}$

  5. (5)

for each $e\in E\cap(V_{1}\times V)$ we have $w(e)=0$.

As discussed above, a countdown game is played in turns. Each turn starts at a
vertex $v$ of Player $0$, from where Player $0$ first picks some outgoing edge
$e$ leading to vertex $v^{\prime}$ of Player $1$. That edge has unique weight
among the outgoing edges of $v$ due to the third requirement. Moreover, if
Player $0$ does not opt to end the play by moving to $v_{\bot}$, the weight of
the edge is negative due to the fourth condition. Subsequently, Player $1$
picks a successor of $v^{\prime}$ and moves to that successor along an edge of
weight zero due to the fifth requirement, where the next turn of the play
starts.

The countdown condition is defined as

$\text{Countdown}(w,c^{*})=\\{\rho=v_{0}v_{1}v_{2}\cdots\in
V^{\omega}\mid\exists j.\,v_{j}=v_{\bot}\text{ and
}c^{*}+w(\rho)=0\\}\enspace.$

Our definition of countdown games differs from the one given by Jurdziński,
Laroussinie, and Sproston [JLS08], as we adapted it to fit our framework of
games introduced in Section 2. It is, however, easy to see that our definition
and the one given by the authors are equivalent.

As countdown games are essentially of finite duration, we obtain that they are
determined due to Zermelo [Zer13].

######  Remark 30.

Countdown games are determined.

Jurdziński, Laroussinie, and Sproston showed that solving countdown games is
ExpTime-hard via a reduction from the word problem for alternating Turing
machines with polynomially bounded space. In order to concisely encode the
exponential number of configurations attainable by the Turing machine during
its run on the input word and the transitions between these configurations,
this reduction requires the weights along the edges of the countdown game as
well as the initial credit $c^{*}$ to be given in binary encoding.

[[JLS08]] The following problem is ExpTime-hard:

> Let $\mathcal{G}$ be a countdown game and let $v$ be a vertex of
> $\mathcal{G}$. Does Player $0$ have a winning strategy from $v$ in
> $\mathcal{G}$?

We reduce the problem of solving countdown games to the threshold problem for
parity games with weights. To this end, for the remainder of this section, fix
some countdown game $\mathcal{G}=(\mathcal{A},\text{Countdown}(w,c^{*}))$
where $\mathcal{A}=(V,V_{0},V_{1},E)$, as well as some initial vertex
$v^{*}\in V$.

Intuitively, we construct the parity game with weights $\mathcal{G}^{\prime}$
such that at the beginning of the play a single request is opened, which is
only answered upon visiting $v_{\bot}$. After visiting $v_{\bot}$, the play
returns to the initial vertex $v^{*}$ reopening the unique request of
$\mathcal{G}^{\prime}$ along the way.

In a countdown game, only Player $0$ may decide to move to $v_{\bot}$. Since
he should, intuitively, only do so after traversing a play prefix of weight
$-c^{*}$, we equip the edges leading from his vertices to $v_{\bot}$ with
weight $2c^{*}$. Thus, he can enforce “tallying the score” by moving to
$v_{\bot}$.

In order to afford Player $1$ the same possibility, we add edges that allow
her to move from his vertices to $v_{\bot}$. Furthermore, in order to
incentivize her to only take these edges once she has exceeded the lower bound
of $-c^{*}$, these edges have weight zero. All remaining weights remain
unchanged, thus the costs incurred by the unique request in
$\mathcal{G}^{\prime}$ model the remaining credit in the corresponding play in
$\mathcal{G}$.

Formally, let $v_{\top}$ be some vertex not occurring in $V$. We define the
parity game with weights
$\mathcal{G}^{\prime}=(\mathcal{A}^{\prime},\mathrm{WeightParity}(\Omega,w^{\prime}))$,
where
$\mathcal{A}^{\prime}=(V^{\prime},V^{\prime}_{0},V^{\prime}_{1},E^{\prime})$,
with

  * •

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

  * •

$E^{\prime}=(E\setminus\\{(v_{\bot},v_{\bot})\\})\cup(V_{1}\times\\{v_{\bot}\\})\cup\\{(v_{\bot},v_{\top}),(v_{\top},v^{*})\\}$.

Since there exists a unique outgoing edge of $v_{\bot}$ leading back to the
initial vertex $v^{*}$ of the countdown game via $v_{\top}$, the play is
restarted after visiting the sink vertex.

Furthermore, we define the weight function

$w^{\prime}(e)=\begin{cases}w(e)&\text{ if $(v,v^{\prime})\in
E\setminus(V_{0}\times\\{v_{\bot}\\})$}\\\ 2c^{*}&\text{ if $e\in
V_{0}\times\\{v_{\bot}\\}$}\\\ 0&\text{ otherwise}\end{cases}$

as well as the coloring

$\Omega^{\prime}(v)=\begin{cases}1&\text{ if $v=v_{\top}$},\\\ 2&\text{ if
$v=v_{\bot}$},\\\ 0&\text{ otherwise}\end{cases}$

and claim that Player $0$ has a strategy $\sigma$ with
$\mathrm{Cost}_{v_{\top}}(\sigma)\leq c^{*}$ if and only if he wins
$\mathcal{G}$ from $v^{*}$. We illustrate this construction in Figure 9.

$\mathrm{Cor}(\rho,j)$$\mathrm{Cor}(\rho,j)$$\nicefrac{{v_{\top}}}{{1}}$$\nicefrac{{v^{*}}}{{0}}$$\nicefrac{{}}{{0}}$$\nicefrac{{}}{{0}}$$\nicefrac{{v_{\bot}}}{{2}}$$\cdots$$\mathcal{A}$$0$
$2c^{*}$ $0$ 0  Figure 9. Construction of the parity game with weights
$\mathcal{G}^{\prime}$ from a given countdown game $\mathcal{G}$. We omit
unchanged weights for the sake of readability.

We claim that this construction implements our intuition, i.e., that solving
$\mathcal{G}^{\prime}$ with respect to the bound $c^{*}$ is indeed equivalent
to solving $\mathcal{G}$.

######  Lemma 31.

Player $0$ wins $\mathcal{G}$ from $v^{*}$ if and only if he has a strategy
$\sigma$ with $\mathrm{Cost}_{v_{\top}}(\sigma)\leq c^{*}$ in
$\mathcal{G}^{\prime}$.

######  Proof 9.5.

We first show the direction from left to right. To this end, let $\sigma$ be a
winning strategy for Player $0$ in $\mathcal{G}$ from $v^{*}$. Moreover, let
$\pi=v_{0}\cdots v_{j}$ be a play prefix in $\mathcal{G}^{\prime}$ starting in
$v_{\top}$ and let $j^{\prime}$ be the largest position in $\pi$ with
$v_{j^{\prime}}=v_{\top}$. We define the strategy $\sigma^{\prime}$ for Player
$0$ in $\mathcal{G}^{\prime}$ via
$\sigma^{\prime}(\pi)=\sigma(v_{j^{\prime}+1}\cdots v_{j})$ and claim
$\mathrm{Cost}_{v_{\top}}(\sigma^{\prime})\leq b$.

To prove this claim, let $\rho^{\prime}=v_{0}v_{1}v_{2}\cdots$ be a play in
$\mathcal{G}^{\prime}$ starting in $v_{\top}$ that is consistent with
$\sigma^{\prime}$. First assume towards a contradiction that $\rho^{\prime}$
only visits $v_{\top}$ finitely often. Then, due to the structure of the
arena, $\rho^{\prime}$ only visits $v_{\bot}$ finitely often. By construction
of $\sigma^{\prime}$, this implies that $\rho^{\prime}$ contains a suffix that
begins in $v^{*}$, is consistent with $\sigma$, but never visits $v_{\bot}$.
This contradicts $\sigma$ being a winning strategy for Player $0$ in
$\mathcal{G}$ from $v^{*}$. Hence, $\rho^{\prime}$ visits $v_{\bot}$
infinitely often.

Thus, $\rho^{\prime}$ is of the form

$\rho^{\prime}=v_{\top}\pi_{0}v_{\bot}\cdot v_{\top}\pi_{1}v_{\bot}\cdot
v_{\top}\pi_{2}v_{\bot}\cdots\enspace,$

where each $\pi_{j}$ starts in $v^{*}$ and is consistent with $\sigma$. We
first argue that, if $\pi_{j}$ ends in a vertex of Player $1$, then we have
$0\geq w^{\prime}(\pi_{j})\geq-c^{*}$: All weights in $\mathcal{G}^{\prime}$
except for those along the edges from $V_{0}\times\\{v_{\bot}\\}$ are
nonpositive. Hence, $0\geq w^{\prime}(\pi_{j})$ follows directly from the
construction of $\mathcal{G}^{\prime}$. Moreover, $w^{\prime}(\pi_{j})<-c^{*}$
would contradict $\pi_{j}$ being consistent with the winning strategy $\sigma$
for Player $0$ in $\mathcal{G}$, since Player $0$ would be unable to continue
the play prefix $\pi_{j}$ such that the resulting play is winning for her.
Hence, we have $0\geq w^{\prime}(\pi_{j})\geq-c^{*}$. Moreover, since all
edges leading from $v_{\top}$ and all edges leading to $v_{\bot}$ have weight
zero, and since $w^{\prime}(\pi)$ is decreasing for increasing prefixes $\pi$
of $\pi_{j}$ due to construction of $\mathcal{G}^{\prime}$, we obtain
$\mathrm{Ampl}(v_{\top}\pi_{j}v_{\bot})\leq c^{*}$.

If, however, $\pi_{j}$ ends in a vertex of Player $0$, then we have
$w^{\prime}(\pi_{j})=-c^{*}$—and therefore
$\mathrm{Ampl}(v_{\top}\pi_{j}v_{\bot})=c^{*}$—as $\pi_{j}$ is consistent with
the winning strategy $\sigma$ for Player $0$ in $\mathcal{G}$. In either case,
we obtain that the unique request in $v_{\top}\pi_{j}v_{\bot}$ posed by
visiting $v_{\top}$ is answered with cost at most $c^{*}$. Hence,
$\rho^{\prime}$ has cost at most $c^{*}$, which concludes this direction of
the proof.

We show the other direction of the statement via contraposition: Assume Player
$0$ does not win $\mathcal{G}$ from $v^{*}$. Since $\mathcal{G}$ is determined
due to Remark 30, Player $1$ wins $\mathcal{G}$ from $v^{*}$, say with
strategy $\tau$. We define a strategy $\tau^{\prime}$ for Player $1$ in
$\mathcal{G}^{\prime}$ that is winning for her from $v_{\top}$ via mimicking
moves made by $\tau$ until the initial credit is used up. At that point, we
define $\tau^{\prime}$ to prescribe moving to $v_{\bot}$ in order to witness
exceeding the initial credit and to restart the play.

Formally, let $\pi^{\prime}=v_{0}\cdots v_{j}$ be a play prefix in
$\mathcal{G}^{\prime}$ that starts in $v_{\top}$ and ends in some vertex of
Player $1$. Moreover, let $j^{\prime}\leq j$ be the largest position such that
$v_{j^{\prime}}=v_{\top}$. If $w(v_{j^{\prime}}\cdots v_{j})\geq-c^{*}$, we
define $\tau^{\prime}(\pi^{\prime})=\tau(v_{j^{\prime}+1}\cdots v_{j})$.
Otherwise, we define $\tau^{\prime}(\pi^{\prime})=v_{\bot}$. It remains to
show $\mathrm{Cost}_{v_{\top}}(\tau^{\prime})>c^{*}$, which concludes the
proof due to Remark 24.

To this end, let $\rho^{\prime}$ be a play in $\mathcal{G}^{\prime}$ starting
in $v_{\top}$ consistent with $\tau^{\prime}$. Due to the structure of
$\mathcal{A}^{\prime}$, every infix of $\rho^{\prime}$ that visits neither
$v_{\top}$ nor $v_{\bot}$ traverses edges of weight zero and negative weight
in alternation. Moreover, since $\tau^{\prime}$ prescribes moving to
$v_{\bot}$ once the play infix since the last visit to $v_{\top}$ has incurred
weight exceeding $-c^{*}$, the play $\rho^{\prime}$ is of the form

$\rho^{\prime}=v_{\top}\pi_{0}v_{\bot}\cdot v_{\top}\pi_{1}v_{\bot}\cdot
v_{\top}\pi_{2}v_{\bot}\cdots\enspace,$

where each $\pi_{j}$ starts in $v^{*}$ and is consistent with $\tau$.

We aim to show $\mathrm{Ampl}(v_{\top}\pi_{j}v_{\bot})>c^{*}$ for all $j$,
which implies $\limsup_{k\rightarrow\infty}(\rho^{\prime},k)>c^{*}$ due to the
construction of $\mathcal{G}^{\prime}$ and thus suffices to show the desired
statement. To this end, fix some $j\in\mathbb{N}$ and first consider the case
that $\pi_{j}$ ends in a vertex of Player $1$. Then we obtain
$w(\pi_{j})<-c^{*}$ by definition of $\tau^{\prime}$. This directly implies
the desired statement.

Now consider the case that $\pi_{j}$ ends in a vertex of Player $0$. We first
argue that $w^{\prime}(\pi_{j})\neq-c^{*}$ holds true. Towards a
contradiction, assume $w^{\prime}(\pi_{j})=-c^{*}$ and recall that $\pi_{j}$
starts in $v^{*}$ and is consistent with the winning strategy $\tau$ for
Player $1$ from $v^{*}$. Thus the play $\pi_{j}{(v_{\bot})}^{\omega}$ in
$\mathcal{G}$ is consistent with $\tau$. Hence, $w^{\prime}(\pi_{j})=-c^{*}$
contradicts $\tau$ being a winning strategy for Player $1$ from $v^{*}$.

It remains to show $\mathrm{Ampl}(v_{\top}\pi_{j}v_{\bot})>c^{*}$ for the case
that $\pi_{j}$ ends in a vertex of Player $0$. If
$w^{\prime}(\pi_{j})<-c^{*}$, we directly obtain
$\mathrm{Ampl}(v_{\top}\pi_{j}v_{\bot})>c^{*}$. If, however,
$w^{\prime}(\pi_{j})>-c^{*}$, we have $w^{\prime}(\pi_{j}v_{\bot})>c^{*}$,
since we defined $w^{\prime}(v,v_{\bot})=2c^{*}$ for each vertex $v$ of Player
$0$. Thus, we obtain $\mathrm{Ampl}(v_{\top}\pi_{j}v_{\bot})>c^{*}$ for each
infix $v_{\top}\pi_{j}v_{\bot}$ of $\rho^{\prime}$. Hence, each request posed
by visiting $v_{\top}$ is answered with cost greater than $c^{*}$. Since we
argued above that $\rho^{\prime}$ contains infinitely many visits to
$v_{\top}$, we obtain $\limsup_{k\rightarrow\infty}(\rho^{\prime},k)>c^{*}$.

Due to Lemma 31 we obtain a polynomial reduction from the problem of solving
countdown games to the threshold problem for parity games with weights. As the
former problem is ExpTime-hard due to Proposition 30, this implies ExpTime-
hardness of the latter problem.

######  Lemma 32.

The following decision problem is ExpTime-hard:

> Given a parity game with weights $\mathcal{G}$, some vertex $v^{*}$ of
> $\mathcal{G}$, and a bound $b\in\mathbb{N}$, does Player $0$ have a strategy
> $\sigma$ with $\mathrm{Cost}_{v^{*}}(\sigma)\leq b$ in $\mathcal{G}$?

######  Proof 9.6.

We reduce the problem of solving countdown games to the given problem. To this
end, let $\mathcal{G}=(\mathcal{A},\text{Countdown}(w,c^{*}))$ be a countdown
game and let $v^{*}$ be a vertex of $\mathcal{A}$. We construct the parity
game with weights $\mathcal{G}^{\prime}$ as described above. Due to Lemma 31,
Player $0$ wins $\mathcal{G}$ from $v^{*}$ if and only if he has a strategy
$\sigma$ with $\mathrm{Cost}_{v_{\top}}(\sigma)\leq c^{*}$. As the problem of
solving countdown games is known to be ExpTime-hard due to Proposition 30,
this implies the desired result.

In the following section, we consider the memory requirements of both players
when playing optimally.

###  9.3. Memory Requirements

Recall that, if Player $0$ just aims to win a parity game with weights with
$n$ vertices, $d$ odd colors, and largest absolute weight $W$, then a memory
structure of size polynomial in $n$, $d$, and $W$ suffices to implement a
winning strategy due to Theorem 14. Dually, Player $1$ requires, in general,
infinite memory in order to implement a strategy winning for her, again due to
Theorem 14.

In this section, we show that these bounds change significantly in the context
of the threshold problem: In order to implement a strategy that enforces cost
of at most $b$ in a parity game with weights with $d$ odd colors, memory of
size polynomial in $b$ and exponential in $d$ is both necessary and sufficient
for Player $0$. Dually, if Player $1$ just aims to enforce a cost of the
resulting play larger than some threshold $b$, strategies of size exponential
in $d$ suffice for her to do so. Both of these bounds are tight.

We first argue that exponential memory indeed suffices for both players to
satisfy or violate a given threshold in a parity game with weights,
respectively. To this end, recall that, given a parity game with weights
$\mathcal{G}$ and a threshold $b$, we determined the solution of the threshold
problem by solving the $b$-threshold game $\mathcal{G}^{\prime}$ of
$\mathcal{G}$. This threshold game is a classical parity game whose arena
consists of the arena of $\mathcal{G}$ augmented with request functions and an
overflow counter that is bounded from above by $n$.

Furthermore recall that, in the proof of Lemma 26, we showed how to leverage a
winning strategy for either player in $\mathcal{G}_{b}$ in order to construct
a winning strategy for them in $\mathcal{G}$. To this end, we implemented the
strategy for Player $0$ in $\mathcal{G}$ using the set $\\{0,\dots,n\\}\times
R$ as memory states, where the set $\\{0,\dots,n\\}$ implements the overflow
counter and where $R$ denotes the set of request functions.

The first component of that memory structure is, however, irrelevant for
Player $0$: If he has a winning strategy whose behavior is dependent not only
on the current vertex and the request function, but also on the value of the
overflow counter, then he also has one that only depends on the current vertex
and the request function.

######  Lemma 33.

Let $\mathcal{G}$ be a parity game with weights containing $d$ odd colors and
let $b\in\mathbb{N}$. Moreover, let $v^{*}$ be a vertex of $\mathcal{G}$. If
Player $0$ has a strategy $\sigma$ in $\mathcal{G}$ with
$\mathrm{Cost}_{v^{*}}(\sigma)=b$, then he also has a strategy
$\sigma^{\prime}$ with $\mathrm{Cost}_{v^{*}}(\sigma^{\prime})\leq b$ and
$|\sigma^{\prime}|={(2b^{2}+b+2)}^{d}$.

######  Proof 9.7.

Recall that we argued previously that if Player $0$ has a strategy $\sigma$ in
$\mathcal{G}$ with $\mathrm{Cost}_{v^{*}}(\sigma)\leq b$, then he also has a
winning strategy from $(v^{*},\text{init}(v^{*}))$ in the threshold game
$\mathcal{G}_{b}$ as defined in Section 9.1. Moreover, since $\mathcal{G}_{b}$
is a parity game, we obtain that if Player $0$ wins $\mathcal{G}_{b}$ from
$(v^{*},\text{init}(v^{*}))$, then he also has a positional winning strategy
doing so. Thus, let $\sigma_{b}$ be a positional winning strategy for Player
$0$ from $(v^{*},\text{init}(v^{*}))$ in $\mathcal{G}_{b}$.

Let $\mathcal{R}$ be the set of vertices reached by plays starting in
$(v^{*},\text{init}(v^{*}))$ and consistent with $\sigma_{b}$. Since
$\sigma_{b}$ is positional, and since the parity condition is prefix-
independent, $\sigma_{b}$ is winning from all vertices in $\mathcal{R}$.
Furthermore, for each vertex $v$ and each request function $r$, we define

$o_{v,r}=\max(\\{0\\}\cup\\{o\mid(v,o,r)\in\mathcal{R}\\})\enspace,$

i.e., $o_{v,r}$ is the maximal value such that Player $0$ wins
$\mathcal{G}_{b}$ from $(v,o_{v,r},r)$ using $\sigma_{b}$, or zero, if no such
value exists.

We now define the strategy $\sigma^{\prime}$ for Player $0$ in $\mathcal{G}$
such that it has the above properties. To this end, recall that we defined the
memory structure $\mathcal{M}=(M,\text{init},\mathrm{upd})$ for the
construction of $\mathcal{G}_{b}$, where $M=\\{0,\dots,n\\}\times R$, and
where $R$ is the set of request functions. We define $M^{\prime}=R$, the
update function $\mathrm{upd}^{\prime}(r,(v,v^{\prime}))=r^{\prime}$, if
$\mathrm{upd}((o_{v,r},r),(v,v^{\prime}))=(o^{\prime},r^{\prime})$, as well as
the initialization function $\text{init}^{\prime}(v)=(o_{v,r_{v}},r_{v})$, if
$\text{init}(v)=(0,r_{v})$. Finally, we define the next-move function
$\mathrm{Nxt}^{\prime}(v,r)=v^{\prime}$, where $v^{\prime}$ is the unique
vertex that satisfies
$\sigma_{b}(v,o_{v,r},r)=(v^{\prime},o^{\prime},r^{\prime})$, and claim that
the strategy $\sigma^{\prime}$ implemented by
$\mathcal{M}^{\prime}=(M^{\prime},\text{init}^{\prime},\mathrm{upd}^{\prime})$
and $\mathrm{Nxt}^{\prime}$ has $\mathrm{Cost}_{v^{*}}(\sigma^{\prime})\leq
b$, which suffices to show the desired statement.

To prove this claim, let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play starting in
$v^{*}$ and consistent with $\sigma^{\prime}$ and let
$(v_{0},r_{0})(v_{1},r_{1})(v_{2},r_{2})\cdots$ be the unique play defined via
$r_{0}=\text{init}^{\prime}(v_{0})$ and
$r_{j}=\mathrm{upd}^{\prime}(r_{j-1},(v_{j},v_{j+1}))$ for all $j>0$.

A straightforward induction yields
$(v_{j},o_{v_{j},r_{j}},r_{j})\in\mathcal{R}$ for all $j\in\mathbb{N}$. We
first argue that we have $o_{v_{j},r_{j}}\leq o_{v_{j+1},r_{j+1}}$ for all
$j\in\mathbb{N}$. To this end, let
$(o,r)=\mathrm{upd}((o_{v_{j},r_{j}},r_{j}),(v_{j},v_{j+1}))$. By construction
of the arena of the threshold game we have $o\geq o_{v_{j},r_{j}}$ and
$r=r_{j+1}$. Moreover, since $(v_{j},o_{v_{j},r_{j}},r_{j})\in\mathcal{R}$ and
due to our definition of $\sigma^{\prime}$, we obtain
$(v_{j+1},o,r)=(v_{j+1},o,r_{j+1})\in\mathcal{R}$. Hence, $o\leq
o_{v_{j+1},r_{j+1}}$, which implies $o_{v_{j+1},r_{j+1}}\geq o_{v_{j},r_{j}}$.

Thus, the $o_{v_{j},r_{j}}$ are monotonically increasing. Furthermore, we
easily obtain $o_{v_{j},r_{j}}<n$ due to all $(v_{j},o_{v_{j},r_{j}},r_{j})$
being in $\mathcal{R}$, the definition of $\mathcal{R}$, and due to
$\sigma_{b}$ being winning for Player $0$ from $(v^{*},\text{init}(v^{*}))$.
Hence, the sequence of the $o_{v_{j},r_{j}}$ eventually stabilizes, i.e.,
there exists a $j\in\mathbb{N}$ such that
$o_{v_{j^{\prime}},r_{j^{\prime}}}=o_{v_{j},r_{j}}$ for all $j^{\prime}\geq
j$.

We argue that the play
$(v_{j},o_{v_{j},r_{j}},r_{j})(v_{j+1},o_{v_{j+1},r_{j+1}},r_{j+1})(v_{j+2},o_{v_{j+2},r_{j+2}},r_{j+2})\cdots$
is consistent with $\sigma_{b}$: Let $j^{\prime}\geq j$ be such that
$(v_{j^{\prime}},o_{v_{j^{\prime}},r_{j^{\prime}}},r_{j^{\prime}})\in
V^{\prime}_{0}$ and let
$\sigma_{b}(v_{j^{\prime}},o_{v_{j^{\prime}},r_{j^{\prime}}},r_{j^{\prime}})=(v_{j^{\prime}+1},o,r_{j^{\prime}+1})$.
We then clearly obtain $o\leq o_{v_{j^{\prime}+1},r_{j^{\prime}+1}}$ by
definition of the latter. Furthermore, we have
$o_{v_{j^{\prime}},r_{j^{\prime}}}\leq o$ due to the construction of the arena
of the threshold game, which yields $o=o_{v_{j^{\prime}+1},r_{j^{\prime}+1}}$
due to our assumption
$o_{v_{j^{\prime}},r_{j^{\prime}}}=o_{v_{j^{\prime}+1},r_{j^{\prime}+1}}$.

Thus, the play
$(v_{j},o_{v_{j},r_{j}},r_{j})(v_{j+1},o_{v_{j+1},r_{j+1}},r_{j+1})(v_{j+2},o_{v_{j+2},r_{j+2}},r_{j+2})\cdots$
starts in a vertex from $\mathcal{R}$, is consistent with $\sigma_{b}$, and
shares a color sequence with a suffix of $\rho$ due to $o_{j}\leq
o_{v_{j},r_{j}}<n$. The strategy $\sigma_{b}$ being winning for Player $0$
from $(v^{*},\text{init}(v^{*}))$, the construction of $\mathcal{G}_{b}$ and
prefix-independence of the parity condition with weights then yield
$w(\rho)\leq b$.

For Player $1$, in contrast, it is open whether one can omit the overflow
counter when implementing a strategy with cost at least $b$. Hence, we have to
include it in the resulting memory structure. Recall, however, that we have
argued in Section 9.1 that we are able to omit those memory states modeling a
saturated overflow counter, thus slightly reducing the size of the resulting
strategy in comparison to a naive implementation. The following upper bound
thus results directly from the results of Section 9.1.

######  Corollary 34.

Let $\mathcal{G}$ be a parity game with weights with $n$ vertices and $d$ odd
colors and let $b\in\mathbb{N}$. Moreover, let $v^{*}$ be a vertex of
$\mathcal{G}$. If Player $1$ has a strategy $\tau$ in $\mathcal{G}$ with
$\mathrm{Cost}_{v^{*}}(\tau)=b$, then she also has a strategy $\tau^{\prime}$
with $\mathrm{Cost}_{v^{*}}(\tau^{\prime})\geq b$ and
$|\tau^{\prime}|=n{(2b^{2}+3b+2)}^{d}$.

Having argued that exponential memory suffices for both players to implement
optimal strategies, we now turn our attention to providing matching lower
bounds. These exponential lower bounds are inherited from the special case of
finitary parity games, for which Weinert and Zimmermann [WZ17] showed that
both players require exponential memory in order to implement strategies that
ensure or violate a given threshold. We reprint these results here for the
sake of completeness.

[[WZ17]]

  1. (1)

For every $d\geq 1$ there exists a finitary parity game $\mathcal{G}_{d}$ with
a vertex $v^{*}$ such that

     * •

$\mathcal{G}_{d}$ has $d$ odd colors and
$|\mathcal{G}_{d}|\in\mathcal{O}(d^{2})$,

     * •

Player $0$ has a strategy $\sigma$ in $\mathcal{G}_{d}$ with
$\mathrm{Cost}_{v^{*}}(\sigma)=d^{2}+2d$,

     * •

there exists no strategy $\sigma^{\prime}$ for Player $0$ with
$\mathrm{Cost}_{v^{*}}(\sigma^{\prime})<d^{2}+2d$, and

     * •

for every strategy $\sigma$ for Player $0$ in $\mathcal{G}_{d}$,
$\mathrm{Cost}_{v^{*}}(\sigma)=d^{2}+2d$ implies $|\sigma|\geq 2^{d-1}$.

  2. (2)

For every $d\geq 1$ there exists a finitary parity game $\mathcal{G}_{d}$ with
a vertex $v^{*}$ such that

     * •

$\mathcal{G}_{d}$ has $\mathcal{O}(d)$ many vertices and $2d$ odd colors,

     * •

Player $1$ has a strategy $\tau$ in $\mathcal{G}_{d}$ with
$\mathrm{Cost}_{v^{*}}(\tau)=5(d-1)+7$,

     * •

there exists no strategy $\tau^{\prime}$ for Player $1$ with
$\mathrm{Cost}_{v^{*}}(\tau^{\prime})>5(d-1)+7$, and

     * •

every strategy $\tau$ for Player $0$ in $\mathcal{G}_{d}$ with
$\mathrm{Cost}_{v^{*}}(\tau)=5(d-1)+7$ has size at least $2^{d}$.

##  10\. Conclusions and Future Work

We have established that parity games with weights and bounded parity games
fall into the same complexity class as energy parity games. This is
interesting, because, while solving such games has the signature complexity
class $\textsc{NP}\cap\textsc{co-NP}$, they are not yet considered a class in
their own right. It is also interesting because their properties appear to be
inherently different: While they both combine the qualitative parity condition
with quantified costs, parity games with weights _combine_ these aspects on
the property level, whereas energy parity games simply look at the
combined—and totally unrelated—properties. We show the characteristic
properties of parity games and of games with combinations of a parity
condition with quantitative conditions relevant for this work in Table 2.

| 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)$
Parity Games with Weights | pseudo-quasi-poly. |  $\mathcal{O}(nd^{2}W)$/inf. | $\mathcal{O}({(ndW)}^{2})$
Table 2. Characteristic properties of variants of parity games.

As future work, we are looking into the natural extensions of parity games
with weights to Streett games with weights [CHH09, FZ14], and at the
complexity of determining optimal bounds and strategies that obtain them
[WZ17]. We are also looking at variations of the problem. The two natural
variations are

  * •

to use a one-sided definition (instead of the absolute value) for the
amplitude of a play, i.e., using
$\mathrm{Ampl}(\pi)=\sup_{j<|\pi|}w(v_{0}\cdots v_{j})\in\mathbb{N}_{\infty}$
(instead of $\mathrm{Ampl}(\pi)=\sup_{j<|\pi|}|w(v_{0}\cdots
v_{j})|\in\mathbb{N}_{\infty}$), and

  * •

to use an arbitrary consecutive subsequence of a play, using the definition
$\mathrm{Ampl}(\pi)=\sup_{j\leq k<|\pi|}|w(v_{j}\cdots
v_{k})|\in\mathbb{N}_{\infty}$.

There are good arguments in favor and against using these individual
variations—and their combination to $\mathrm{Ampl}(\pi)=\sup_{j\leq
k<|\pi|}w(v_{j}\cdots v_{k})\in\mathbb{N}_{\infty}$—but we feel that the
introduction of parity games with weights benefit from choosing one of the
four combinations as _the_ parity games with weights.

We expect the complexity to rise when changing from maximizing over the
absolute value to maximizing over the value, as this appears to be close to
pushdown boundedness games [CF13], and we conjecture this problem to be
PSpace-complete.

## References

  * [BCJ+97] Anca Browne, Edmund M. Clarke, Somesh Jha, David E. Long, and Wilfredo R. Marrero.  An improved algorithm for the evaluation of fixpoint expressions.  Theor. Comp. Sci., 178(1–2):237–255, 1997.
  * [BV07] Henrik Björklund and Sergei Vorobyov.  A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games.  Discrete Appl. Math., 155(2):210–229, 2007.
  * [CD12] Krishnendu Chatterjee and Laurent Doyen.  Energy Parity Games.  Theor. Comp. Sci., 458:49–60, 2012.
  * [CF13] Krishnendu Chatterjee and Nathanaël Fijalkow.  Infinite-state games with finitary conditions.  In Simona Ronchi Della Rocca, editor, CSL 2013, volume 23 of LIPIcs, pages 181–196. Schloss Dagstuhl–LZI, 2013.
  * [CH06] Krishnendu Chatterjee and Thomas A. Henzinger.  Finitary winning in $\omega$-regular games.  In Holger Hermanns and Jens Palsberg, editors, TACAS 2006, volume 3920 of LNCS, pages 257–271. Springer, 2006.
  * [CHH09] Krishnendu Chatterjee, Thomas A. Henzinger, and Florian Horn.  Finitary winning in $\omega$-regular games.  Trans. Comput. Log., 11(1):1:1–1:27, 2009.
  * [CHJ05] Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński.  Mean-payoff parity games.  In LICS 2005, pages 178–187. IEEE Computer Society, 2005.
  * [CJK+17] C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan.  Deciding parity games in quasipolynomial time.  In STOC 2017, pages 252–263. ACM Press, 2017.
  * [Con93] Anne Condon.  On algorithms for simple stochastic games.  In Advances in Computational Complexity Theory, pages 51–73. American Mathematical Society, 1993.
  * [DG18] Anuj Dawar and Erich Grädel, editors.  LICS 2018. ACM, 2018.
  * [DJL18] Laure Daviaud, Marcin Jurdzinski, and Ranko Lazic.  A pseudo-quasi-polynomial algorithm for mean-payoff parity games.  In Dawar and Grädel [DG18], pages 325–334.
  * [EJ91] E. Allen Emerson and Charanjit S. Jutla.  Tree automata, $\mu$-calculus and determinacy.  In FOCS 1991, pages 368–377. IEEE Computer Society, 1991.
  * [EL86] E. Allen Emerson and Chin-Laung Lei.  Efficient model checking in fragments of the propositional $\mu$-calculus.  In LICS 1986, pages 267–278. IEEE Computer Society, 1986.
  * [FJS+17] John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan, and Dominik Wojtczak.  An ordered approach to solving parity games in quasi polynomial time and quasi linear space.  In SPIN 2017, pages 112–121. ACM, 2017.
  * [FZ14] Nathanaël Fijalkow and Martin Zimmermann.  Parity and Streett games with costs.  LMCS, 10(2), 2014.
  * [JL17] Marcin Jurdziński and Ranko Lazić.  Succinct progress measures for solving parity games.  In LICS 2017, pages 1–9. IEEE Computer Society, 2017.
  * [JLS08] Marcin Jurdziński, François Laroussinie, and Jeremy Sproston.  Model checking probabilistic timed automata with one or two clocks.  LMCS, 4(3), 2008.
  * [JPZ08] Marcin Jurdziński, Mike Paterson, and Uri Zwick.  A deterministic subexponential algorithm for solving parity games.  SIAM J. on Comp., 38(4):1519–1532, 2008.
  * [Jur98] Marcin Jurdziński.  Deciding the winner in parity games is in UP $\cap$ co-UP.  Inf. Proc. Lett., 68(3):119–124, November 1998.
  * [Jur00] Marcin Jurdziński.  Small progress measures for solving parity games.  In STACS 2000, volume 1770 of LNCS, pages 290–301. Springer, 2000.
  * [Koz83] Dexter Kozen.  Results on the propositional $\mu$-calculus.  Theor. Comp. Sci., 27:333–354, 1983.
  * [Leh18] Karoliina Lehtinen.  A modal $\mu$ perspective on solving parity games in quasi-polynomial time.  In Dawar and Grädel [DG18], pages 639–648.
  * [Mar75] Donald A. Martin.  Borel determinacy.  Annals of Mathematics, 102(2):363–371, 1975.
  * [McN93] Robert McNaughton.  Infinite games played on finite graphs.  Ann. Pure Appl. Logic, 65(2):149–184, 1993.
  * [MMS15] Fabio Mogavero, Aniello Murano, and Loredana Sorrentino.  On promptness in parity games.  Fundam. Inform., 139(3):277–305, 2015.
  * [NRY96] Anil Nerode, Jeffrey B. Remmel, and Alexander Yakhnis.  Mcnaughton games and extracting strategies for concurrent programs.  Ann. Pure Appl. Logic, 78(1-3):203–242, 1996.
  * [Pur95] Anuj Puri.  Theory of hybrid systems and discrete event systems.  PhD thesis, Computer Science Department, University of California, Berkeley, 1995.
  * [Sch08] Sven Schewe.  An optimal strategy improvement algorithm for solving parity and payoff games.  In CSL 2008, volume 5213 of LNCS, pages 368–383. Springer, 2008.
  * [Sch17] Sven Schewe.  Solving parity games in big steps.  J. of Comp. and Sys. Sci., 84:243–262, 2017.
  * [STV15] Sven Schewe, Ashutosh Trivedi, and Thomas Varghese.  Symmetric strategy improvement.  In ICALP 2015, volume 9135 of LNCS, pages 388–400. Springer, 2015.
  * [SWZ18] Sven Schewe, Alexander Weinert, and Martin Zimmermann.  Parity games with weights.  In CSL 2018, pages 36:1–36:17, 2018.
  * [VJ00] Jens Vöge and Marcin Jurdzinski.  A discrete strategy improvement algorithm for solving parity games.  In E. Allen Emerson and A. Prasad Sistla, editors, CAV 2000, volume 1855 of LNCS, pages 202–215. Springer, 2000.
  * [WZ17] Alexander Weinert and Martin Zimmermann.  Easy to win, hard to master: Optimal strategies in parity games with costs.  LMCS, 13(3), 2017.
  * [Zer13] Ernst Zermelo.  Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels.  In Proc. Fifth Congress of Mathematicians, Vol. 2, pages 501–504. Cambridge Press, 1913.
  * [Zie98] Wieslaw Zielonka.  Infinite games on finitely coloured graphs with applications to automata on infinite trees.  Theor. Comp. Sci., 200(1-2):135–183, 1998.
  * [ZP96] Uri Zwick and Mike S. Paterson.  The complexity of mean payoff games on graphs.  Theor. Comp. Sci., 158(1–2):343–359, 1996.