Université Gustave Eiffel<EMAIL_ADDRESS>Université Libre de
Bruxelles<EMAIL_ADDRESS>Université Gustave Eiffel,
<EMAIL_ADDRESS>Léonard Brice, Jean-François
Raskin, Marie van den Bogaard Software and its engineering: Formal methods;
Theory of computation: Logic and verification; Theory of computation: Solution
concepts in game theory.

# On the Complexity of SPEs in Parity Games

Léonard Brice  Jean-François Raskin  Marie van den Bogaard

(2021)

###### Abstract

We study the complexity of problems related to subgame-perfect equilibria
(SPEs) in infinite duration non zero-sum multiplayer games played on finite
graphs with parity objectives. We present new complexity results that close
gaps in the literature. Our techniques are based on a recent characterization
of SPEs in prefix-independent games that is grounded on the notions of
requirements and negotiation, and according to which the plays supported by
SPEs are exactly the plays consistent with the requirement that is the least
fixed point of the negotiation function. The new results are as follows.
First, checking that a given requirement is a fixed point of the negotiation
function is an $\mathbf{NP}$-complete problem. Second, we show that the SPE
constrained existence problem is $\mathbf{NP}$-complete, this problem was
previously known to be $\mathbf{ExpTime}$-easy and $\mathbf{NP}$-hard. Third,
the SPE constrained existence problem is fixed-parameter tractable when the
number of players and of colors are parameters. Fourth, deciding whether some
requirement is the least fixed point of the negotiation function is complete
for the second level of the Boolean hierarchy. Finally, the SPE-verification
problem — that is, the problem of deciding whether there exists a play
supported by a SPE that satisfies some LTL formula — is
$\mathbf{PSpace}$-complete, this problem was known to be
$\mathbf{ExpTime}$-easy and $\mathbf{PSpace}$-hard.

###### keywords:

Games on graphs, subgame-perfect equilibria, parity objectives.

##  1 Introduction

_Nash equilibrium_ (NE) is one of the central concepts from game theory to
formalize the notion of rationality. It describes profiles of strategies in
which no player has an incentive to change their strategy unilaterally.
However, in sequential games, like games played on graphs, NEs are known to be
plagued by non-credible threats: players can threaten other players in
subgames with non-rational actions in order to force an equilibrium that
avoids these subgames. To avoid non-credible threats, subgame-perfect
equilibria are used instead. _Subgame-perfect equilibria_ (SPEs) are NEs that
are NEs in all subgames of the original game: the players must act rationally
in all subgames even after a deviation by another player.

In this paper, we study the complexity of decision problems related to SPEs in
sequential games played on graphs with parity objectives. In such a game, each
vertex of the game graph has one color per player, and each player wants the
least color they see infinitely often along a play, which is an infinite path
in the graph, to be even. Parity conditions, in games as well as in automata,
are canonical ways to represent $\omega$-regular constraints. It is known that
SPEs always exist in parity games, as shown in [15]. Unfortunately, the
precise complexity of the SPE constrained existence problem, i.e. the problem
of deciding whether there exists an SPE that generates payoffs between two
given thresholds, is left open in the literature: it is known to be
$\mathbf{ExpTime}$-easy and $\mathbf{NP}$-hard. We prove here that it is in
fact $\mathbf{NP}$-complete, and we provide several other new complexity
results on related problems of interest.

While previous attempts to solve this decision problem were based on
alternating tree automata ([9]), we obtain the new tight complexity results
starting from concepts that we have introduced recently in [2] to capture SPEs
in mean-payoff games: the notions of _requirements_ and _negotiation_. A
requirement is a function $\lambda$ that maps each vertex $v$ of the game
graph to a real value, that represents the lowest payoff that the player
controlling $v$ should accept when facing other rational players. A play
$\rho=\rho_{0}\rho_{1}\dots$ is _$\lambda$ -consistent_ if for each vertex
$\rho_{k}$, the player controlling $\rho_{k}$ gets at least the payoff
$\lambda(\rho_{k})$ in $\rho$. In Boolean games, such as parity games, we
naturally consider requirements whose values are either $0$ or $1$ ($1$
meaning that the player must achieve their objective, $0$ that they may not).

The negotiation function maps a requirement $\lambda$ to a requirement
$\mathrm{nego}(\lambda)$, which captures from any vertex $v$ the maximal
payoff that the corresponding player can ensure, against _$\lambda$ -rational_
players, that is, players who play in such a way that they obtain at least the
payoff specified by $\lambda$. Clearly, if $\lambda_{0}$ maps each vertex to
$0$, then every play is $\lambda_{0}$-consistent. Then, the requirement
$\mathrm{nego}(\lambda_{0})$ maps each vertex $v$ to its _antagonistic value_
, i.e. the best payoff that the player controlling $v$ can ensure against an
adversarial coalition of the other players (as any behavior of the other
players is $\lambda_{0}$-rational). It is the case that the
$\mathrm{nego}(\lambda_{0})$-consistent plays are exactly the plays supported
by NEs.

But then, the following natural question is: given $v$ and $\lambda$, can the
player who controls $v$ improve his worst-case value, if only plays that are
consistent with $\lambda$ are proposed by the other players? Or equivalently,
can this player enforce a better value when playing against players that are
not willing to give away their own worst-case value? which is clearly a
minimal goal for any rational adversary. So $\mathrm{nego}(\lambda)(v)$
returns this value; and this reasoning can be iterated. In [2], it is shown
that the least fixed point $\lambda^{*}$ of the negotiation function is
exactly characterizing the set of plays supported by SPEs, for all prefix
independent payoff functions with steady negotiation (which is the case for
parity objectives) .

Using that characterization of SPEs, we prove that SPEs always exist in parity
games (Theorem 2). That result had already been proved by Ummels in [15]: we
use the concepts of requirements and negotiation to rephrase his proof in a
more succinct way.

#### Main contributions

In order to get tight complexity results, we establish the links between the
negotiation function and a class of zero-sum two-player games, the _abstract
negotiation games_ (Theorem 3). Those games are played on an infinite arena,
but we show that the players can play simple strategies that have polynomial
size representation, while still playing optimally (Lemma 4). We show that a
non-deterministic polynomial algorithm can decide which player has a winning
strategy in that game, i.e. can decide whether $\mathrm{nego}(\lambda)(v)=0$
or $1$, for a given requirement $\lambda$ on a given vertex in a given game:
as a consequence, deciding whether the requirement $\lambda$ is a fixed point
of the negotiation function is $\mathbf{NP}$-easy (Lemma 5). We also show that
the computation of $\lambda^{*}$, and consequently the SPE constrained
existence problem, are fixed-parameter tractable if we fix the number of
players and colors in the game (Theorem 4).

Those algorithms can be exploited to obtain upper bounds for several problems
related to SPEs. Most classical of them, the problem of deciding whether there
exists an SPE generating a payoff vector between two given thresholds (SPE
constrained existence problem), is $\mathbf{NP}$-complete (Theorem 6). That
problem can be solved without computing the least fixed point of the
negotiation function: such a problem is $\mathbf{BH}_{2}$-complete, as well as
its decisional version — i.e. deciding whether a given requirement $\lambda$
is equal to $\lambda^{*}$ (Theorem 7). Finally, deciding whether there exists
an SPE play that satisfies some LTL formula (SPE-verification problem) is
$\mathbf{PSpace}$-complete (Theorem 8).

#### Related works

In [9], Ummels and Grädel solve the SPE constrained existence problem in
parity games, and prove that such games always contain SPEs. Their algorithm
is based on the construction of alternating tree automata, on which one can
solve the emptiness problem in exponential time. The SPE constrained existence
problem is therefore $\mathbf{ExpTime}$-easy, which was, to our knowledge, the
best upper bound existing in the literature. The authors also prove the
$\mathbf{NP}$-hardness of that problem. In what follows, we prove that it is
actually $\mathbf{NP}$-complete.

In [8], Flesch and Predtetchinski present a general non-effective procedure to
characterize the plays supported by an SPE in games with finitely many
possible payoff vectors, as parity games. That characterization uses the
abstract negotiation game, but does not use the notions of requirements and
negotiation, and as a consequence does not yield an effective algorithm —
their procedure requires to solve infinitely many games that have an
uncountable state space.

In [2], we solve the SPE constrained existence problem on mean-payoff games.
To that end, we define the notions of requirements and negotiation, and
highlight the links between negotiation and the abstract negotiation game.
Part of our results can be applied to every prefix-independent game with
steady negotiation, which includes parity games. But, in order to get tight
complexity results, we need here to introduce new notions, such as reduced
strategies and deviation graphs.

In [3], Brihaye et al. prove that the SPE constrained existence problem on
quantitative reachability games is $\mathbf{PSpace}$-complete. Their algorithm
updates continuously a function that heralds the notion of requirement, until
it reaches a fixed point, that we can interpret as the least fixed point of
the negotiation function.

In [4], Brihaye et al. give a characterization of NEs in cost-prefix linear
games, based on the worst-case value. Parity games are cost-prefix linear, and
the worst-case value is captured by our notion of requirement. The authors do
not study the notion of SPE in their paper.

In [12], Meunier proposes a method to decide the existence of SPEs generating
a given payoff, proving that it is equivalent to decide which player has a
winning strategy in a Prover-Challenger game. That method could be used with
parity games, but it would not lead to a better complexity than [15], and so
it would not yield our $\mathbf{NP}$-completeness result.

The applications of non-zero sum infinite duration games targeting reactive
synthesis problems have gathered significant attention during the recent
years, hence a rich literature on that topic. The interested reader may refer
to the surveys [1, 5] and their references.

#### Structure of the paper

In Section 2, we introduce the necessary background. In Section 3, we present
the concepts of requirements, negotiation and abstract negotiation game, and
show how they can be applied to characterize SPEs in parity games. In Section
4, we turn that characterization into algorithms that solve the aforementioned
problems, and deduce upper bounds for their complexities. In Section 5, we
match them with lower bounds, and conclude on the precise complexities of
those problems.

##  2 Background

In the sequel, we use the word _game_ for Boolean turn-based games played on
finite graphs.

######  Definition 1 (Game).

A _game_ is a tuple $G=(\Pi,V,(V_{i})_{i\in\Pi},E,\mu)$, where:

  * •

$\Pi$ is a finite set of _players_ ;

  * •

$(V,E)$ is a finite directed graph, whose vertices and edges are also called
_states_ and _transitions_ , and in which every state has at least one
outgoing transition;

  * •

$(V_{i})_{i\in\Pi}$ is a partition of $V$, where each $V_{i}$ is the set of
the states _controlled_ by player $i$;

  * •

$\mu:V^{\omega}\to\\{0,1\\}^{\Pi}$ is a _payoff function_ , which maps each
sequence of states $\rho$ to the tuple $\mu(\rho)=(\mu_{i}(\rho))_{i}$ of the
players’ payoffs: player $i$ _wins_ $\rho$ if $\mu_{i}(\rho)=1$, and _loses_
otherwise.

A play in such a game can be seen as an infinite sequence of moves of a token
on the graph $(V,E)$: when the token is on a given vertex, the player
controlling that vertex chooses the edge along which it will move. And then,
the player controlling the next vertex chooses where it moves next, and so on.

######  Definition 2 (Play, history).

A _play_ (resp. _history_) in the game $G$ is an infinite (resp. finite) path
in the graph $(V,E)$. We write $\mathrm{Plays}G$ (resp. $\mathrm{Hist}G$) for
the set of plays (resp. histories) in $G$. We write $\mathrm{Hist}_{i}G$ for
the set of histories in $G$ of the form $hv$, where $v\in V_{i}$. We write
$\mathrm{Occ}(\rho)$ (resp. $\mathrm{Occ}(h)$) for the set of vertices that
occur at least once in the play $\rho$ (resp. the history $h$), and
$\mathrm{Inf}(\rho)$ for the set of vertices that occur infinitely often in
$\rho$. We write $\mathrm{first}(h)$ (resp. $\mathrm{first}(\rho)$) the first
vertex of $h$ (resp. $\rho$), and $\mathrm{last}(h)$ its last vertex.

Often, we need to specify an initial state for a game.

######  Definition 3 (Initialized game).

An _initialized game_ is a pair $(G,v_{0})$, often written $G_{\upharpoonright
v_{0}}$, where $G$ is a game and $v_{0}\in V$ is the _initial vertex_. A play
(resp. history) of $G$ is a play (resp. history) of $G_{\upharpoonright
v_{0}}$ iff its first state is $v_{0}$. We write
$\mathrm{Plays}G_{\upharpoonright v_{0}}$ (resp.
$\mathrm{Hist}G_{\upharpoonright v_{0}}$, $\mathrm{Hist}_{i}G_{\upharpoonright
v_{0}}$) for the set of plays (resp. histories, histories ending in $V_{i}$)
in $G_{\upharpoonright v_{0}}$.

When the context is clear, we call _game_ both non-initialized and initialized
games.

######  Definition 4 (Strategy, strategy profile).

A _strategy_ for player $i$ in $G_{\upharpoonright v_{0}}$ is a function
$\sigma_{i}:\mathrm{Hist}_{i}G_{\upharpoonright v_{0}}\to V$ such that for
each history $hv\in\mathrm{Hist}_{i}G_{\upharpoonright v_{0}}$, we have
$v\sigma_{i}(hv)\in E$.

A _strategy profile_ for $P\subseteq\Pi$ is a tuple
$\bar{\sigma}_{P}=(\sigma_{i})_{i\in P}$ where each $\sigma_{i}$ is a strategy
for player $i$. When $P=\Pi$, the strategy profile is _complete_ , and we
usually write it $\bar{\sigma}$. For each $i\in\Pi$, we write $-i$ for the set
$\Pi\setminus\\{i\\}$. When $\bar{\tau}_{P},\bar{\tau}^{\prime}_{Q}$ are two
strategy profiles with $P\cap Q=\emptyset$, we write
$(\bar{\tau}_{P},\bar{\tau}^{\prime}_{Q})$ the strategy profile
$\bar{\sigma}_{P\cup Q}$ defined by $\sigma_{i}=\tau_{i}$ if $i\in P$, and
$\sigma_{i}=\tau^{\prime}_{i}$ if $i\in Q$. We write
$\Sigma_{i}G_{\upharpoonright v_{0}}$ (resp. $\Sigma_{P}G_{\upharpoonright
v_{0}}$) the set of all strategies (resp. strategy profiles) for player $i$
(resp. the set $P$) in $G_{\upharpoonright v_{0}}$.

A history or a play is _compatible with_ (or _supported by_) a strategy
$\sigma_{i}$ if for each of its prefixes $hv$ with $h\in\mathrm{Hist}_{i}G$,
we have $v=\sigma_{i}(h)$. It is compatible with a strategy profile
$\bar{\sigma}_{P}$ if it is compatible with $\sigma_{i}$ for each $i\in P$.
When a strategy profile $\bar{\sigma}$ is complete, there is one unique play
in $G_{\upharpoonright v_{0}}$ that is compatible with it, written
$\langle\bar{\sigma}\rangle_{v_{0}}$ and called the _outcome_ of
$\bar{\sigma}$.

A strategy $\sigma_{i}$ is _memoryless_ when for each state $v$ and every two
histories $h$ and $h^{\prime}$, we have
$\sigma_{i}(hv)=\sigma_{i}(h^{\prime}v)$. In that case, we liberally consider
that $\sigma_{i}$ is defined from every state, and write $\sigma_{i}(v)$ for
every $\sigma_{i}(hv)$.

Before defining the notion of SPEs, we need to define a weaker, but more
classical, solution concept: Nash equilibria. A Nash equilibrium is a strategy
profile such that no player can improve their payoff by deviating unilaterally
from their strategy.

######  Definition 5 (Nash equilibrium).

A complete strategy profile $\bar{\sigma}$ in $G_{\upharpoonright v_{0}}$ is a
_Nash equilibrium_ — or _NE_ for short — iff for each player $i$ and for every
strategy $\sigma^{\prime}_{i}$, we have
$\mu_{i}(\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}})\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \mu_{i}(\langle\bar{\sigma}\rangle_{v_{0}})$.

An SPE is an NE in all the subgames, in the following formal sense.

######  Definition 6 (Subgame, substrategy).

Let $hv$ be a history in $G_{\upharpoonright v_{0}}$. The _subgame_ of $G$
after $hv$ is the initialized game $G_{\upharpoonright
hv}=(\Pi,V,(V_{i})_{i},E,\mu_{\upharpoonright hv})_{\upharpoonright v}$, where
$\mu_{\upharpoonright hv}$ maps each play to its payoff in $G$, assuming that
the history $hv$ has already been played: formally, for every
$\rho\in\mathrm{Plays}G_{\upharpoonright hv}$, we have $\mu_{\upharpoonright
hv}(\rho)=\mu(h\rho)$. If $\sigma_{i}$ is a strategy in $G_{\upharpoonright
v_{0}}$, its _substrategy_ after $hv$ is the strategy
$\sigma_{i\upharpoonright hv}$ in $G_{\upharpoonright hv}$, defined by
$\sigma_{i\upharpoonright hv}(h^{\prime})=\sigma_{i}(hh^{\prime})$ for every
$h^{\prime}\in\mathrm{Hist}_{i}G_{\upharpoonright hv}$.

######  Definition 7 (Subgame-perfect equilibrium).

A complete strategy profile $\bar{\sigma}$ in $G_{\upharpoonright v_{0}}$ is a
_subgame-perfect equilibrium_ — or _SPE_ for short — iff for every history
$hv$ in $G_{\upharpoonright v_{0}}$, the substrategy profile
$\bar{\sigma}_{\upharpoonright hv}$ is a Nash equilibrium.

Throughout this paper, we mostly study _parity_ games.

######  Definition 8 (Parity game).

The game $G$ is a _parity game_ if there exists a tuple of _color functions_
$(\kappa_{i}:\leavevmode\nobreak\ V\leavevmode\nobreak\
\to\leavevmode\nobreak\ \mathbb{N})_{i\in\Pi}$, such that each play $\rho$ is
won by a given player $i$ — i.e. $\mu_{i}(\rho)=1$ — iff the least color seen
infinitely often by player $i$, i.e. the integer
$\min\kappa_{i}(\mathrm{Inf}(\rho))$, is even.

A _Büchi_ game is a parity game where all colors are either $0$ or $1$ — or
equivalently, a game in which the objective of each player is to visit
infinitely often a given set of vertices. A _coBüchi_ game is a parity game
where all colors are either $1$ or $2$ — or equivalently, a game in which the
objective of each player is to eventually avoid a given set of vertices.

######  Example 1.

Consider the (coBüchi) game represented by Figure 1: both players win the play
$ace^{\omega}$, and lose any other. A first NE in that game is the strategy
profile in which both players always go to the right: its outcome is
$ace^{\omega}$, which is won by both players, hence none can strictly improve
their payoff by deviating. A second NE is the strategy profile in which both
players always go down: its outcome is $ab^{\omega}$, which is lost by both
players. However, player $\Box$ cannot improve his strategy, because he never
plays; and player $\Circle$ cannot neither, because if she goes right, then
$\Box$ plans to go down, and she still loses. Only the first one is an SPE:
for player $\Box$, planning to go down from the state $c$ is a non-credible
threat.

$a$$b$$c$$d$$e$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{2}}$
Figure 1: A coBüchi game with two NEs and one SPE

An important property of parity games is that they are _prefix-independent_.

######  Definition 9 (Prefix-independent game).

The game $G$ is _prefix-independent_ iff for every history $h$, we have
$\mu_{\upharpoonright h}=\mu$.

In such games, we will present algorithms that solve the following problems.

######  Problem 1 (SPE constrained existence problem).

Given a parity game $G_{\upharpoonright v_{0}}$ and two thresholds
$\bar{x},\bar{y}\in\\{0,1\\}^{\Pi}$, is there an SPE $\bar{\sigma}$ in
$G_{\upharpoonright v_{0}}$ such that
$\bar{x}\leq\mu(\langle\bar{\sigma}\rangle_{v_{0}})\leq\bar{y}$?

The next problem requires a definition of the linear temporal logic, LTL.

######  Definition 10 (LTL formulas).

The _linear temporal logic_ — or _LTL_ for short — over the set of atomic
propositions $\mathbb{A}$ is defined as follows: syntactically, each
$a\in\mathbb{A}$ is an LTL formula, and if $\varphi$ and $\psi$ are LTL
formulas, then $\neg\varphi$, $\varphi\vee\psi$, $\mathbf{X}\varphi$, and
$\varphi\mathbf{U}\psi$ are LTL formulas.

Semantically, if $\nu=\nu_{0}\nu_{1}\dots$ is an infinite sequence of
valuations of $\mathbb{A}$, then:

  * •

$\nu\models a$ iff $\nu_{0}(a)=1$;

  * •

$\nu\models\neg\varphi$ iff $\nu\not\models\varphi$;

  * •

$\nu\models\varphi\vee\psi$ iff $\nu\models\varphi$ or $\nu\models\psi$;

  * •

$\nu\models\mathbf{X}\varphi$ iff $\nu_{1}\nu_{2}\dots\models\varphi$;

  * •

$\nu\models\varphi\mathbf{U}\psi$ iff there exists $k\in\mathbb{N}$ such that
$\nu_{k}\nu_{k+1}\dots\models\psi$, and for each $\ell<k$, we have
$\nu_{\ell}\nu_{\ell+1}\dots\models\varphi$.

We will also make use of the classical notations $\wedge$, $\top$, $\bot$,
$\Rightarrow$, $\mathbf{F}$ or $\mathbf{G}$ defined as abbreviations using the
symbols chosen here as primitives. In particular, we write $\top$ for
$a\vee\neg a$, $\mathbf{F}\varphi$ ("finally $\varphi$") for
$\top\mathbf{U}\varphi$, and $\mathbf{G}\varphi$ ("globally $\varphi$") for
$\neg\mathbf{F}\neg\varphi$. When we use LTL to describe plays in a game,
w.l.o.g. and for simplicity, the atom set is $\mathbb{A}=V$, and each play
$\rho$ is assimilated to the sequence of valuations $\nu$ defined by
$\nu_{k}(v)=1$ iff $\rho_{k}=v$. For example, when $u$ and $v$ are two
vertices, the play $(uv)^{\omega}$ is the only play satisfying the formula
$u\wedge\mathbf{G}\left((u\Rightarrow\mathbf{X}v)\wedge(v\Rightarrow\mathbf{X}u)\right)$.

######  Problem 2 (SPE-verification problem).

Given a parity game $G_{\upharpoonright v_{0}}$ and an LTL formula $\varphi$,
is there an SPE $\bar{\sigma}$ in $G_{\upharpoonright v_{0}}$ such that
$\langle\bar{\sigma}\rangle_{v_{0}}\models\varphi$?

######  Remark.

The natural problems of deciding whether _all_ SPEs generate a payoff vector
between two thresholds, or a play that satisfies some LTL formula, are the
duals of the aforementioned problems, and their complexities are obtained as
direct corollaries. For example, in a given parity game, all the outcomes of
SPEs satisfy the formula $\varphi$ if and only if there does not exist an SPE
whose outcome satisfies $\neg\varphi$. Since we will show that the SPE-
verification problem is $\mathbf{PSpace}$-complete, its dual will also be
$\mathbf{PSpace}$-complete. Similarly, the SPE constrained universality
problem is $\mathbf{coNP}$-complete as we will show that its dual, the SPE
constrained existence problem, is $\mathbf{NP}$-complete.

While we do not recall the definition of classical complexity classes here
(such as $\mathbf{NP}$, $\mathbf{coNP}$, or $\mathbf{PSpace}$, see [13]), we
recall the definition of the class $\mathbf{BH}_{2}$: the second level of the
Boolean hierarchy. For more details about the Boolean hierarchy itself, see
[16].

######  Definition 11 (Class $\mathbf{BH}_{2}$).

The complexity class $\mathbf{BH}_{2}$ is the class of problems of the form
$P\cap Q$, where $P$ is $\mathbf{NP}$-easy and $Q$ is $\mathbf{coNP}$-easy,
and both have the same set of instances. In other words, a
$\mathbf{BH}_{2}$-easy problem is a problem that can be decided with one call
to an $\mathbf{NP}$ algorithm, and one to a $\mathbf{coNP}$ algorithm.

######  Remark.

The class $\mathbf{BH}_{2}$ must not be mistaken with the class
$\mathbf{NP}\cap\mathbf{coNP}$, that gathers the problems that can be solved
by an $\mathbf{NP}$ algorithm _as well as_ by a $\mathbf{coNP}$ one: the
latter is included in $\mathbf{NP}$ and in $\mathbf{coNP}$, while the former
contains them.

To attach intuition to this definition, let us present a useful
$\mathbf{BH}_{2}$-complete problem.

######  Problem 3 ($\textsc{Sat}\times\textsc{coSat}$).

Given a pair $(\varphi_{1},\varphi_{2})$ of propositional logic formulas, is
it true that $\varphi_{1}$ is satisfiable and that $\varphi_{2}$ is not?

######  Lemma 1 (App. A).

The problem $\textsc{Sat}\times\textsc{coSat}$ is $\mathbf{BH}_{2}$-complete.

##  3 Negotiation in parity games

###  3.1 Requirements, negotiation, and link with SPEs

In the algorithms we provide, we make use of the characterization of SPEs in
prefix-independent games that has been presented in [2]. We recall here the
notions needed, slightly adapted to Boolean games.

######  Definition 12 (Requirement).

A _requirement_ on a game $G$ is a mapping $\lambda:\leavevmode\nobreak\
V\leavevmode\nobreak\ \to\leavevmode\nobreak\ \\{0,1,+\infty\\}$. The set of
the requirements on $G$ is denoted by $\mathrm{Req}G$, and is ordered by the
componentwise order $\leq$: we write $\lambda\leq\lambda^{\prime}$ when we
have $\lambda(v)\leq\lambda^{\prime}(v)$ for all $v$.

######  Definition 13 ($\lambda$-consistency).

Let $\lambda$ be a requirement on the game $G$. A play $\rho$ in $G$ is
_$\lambda$ -consistent_ iff for each player $i$ and every index $k$ such that
$\rho_{k}\in V_{i}$, we have
$\mu_{i}(\rho_{k}\rho_{k+1}\dots)\geq\lambda(\rho_{k})$. The set of
$\lambda$-consistent plays in $G_{\upharpoonright v_{0}}$ is denoted by
$\lambda\mathrm{Cons}(v_{0})$.

In this paper, we will consider specifically requirements that are
_satisfiable_.

######  Definition 14 (Satisfiability).

The requirement $\lambda$, on the game $G$, is _satisfiable_ iff for each
state $v\in V$, there exists at least one $\lambda$-consistent play from $v$.

######  Lemma 2.

Given a parity game $G$ and a requirement $\lambda$, deciding whether
$\lambda$ is satisfiable is $\mathbf{NP}$-easy.111It is actually
$\mathbf{NP}$-complete, as we can prove by slightly adapting the proof of
Theorem 5.

###### Proof.

Let us take as certificate of polynomial size a family $(h_{v},W_{v})_{v\in
V}$, where for each $v$, $h_{v}$ is a history without cycle starting from $v$
and $W_{v}$ is a subset of $V$ with $\mathrm{last}(h_{v})\in W_{v}$. The
family $(h_{v},W_{v})_{v\in V}$ testifies that $\lambda$ is satisfiable if for
each $v$: (1) $\lambda(v)\neq+\infty$; (2) the subgraph $(W_{v},E\cap
W_{v}^{2})$ is strongly connected; (3) for each vertex
$u\in\mathrm{Occ}(h_{v})\cup W_{v}$ such that $\lambda(u)=1$, if $i$ is the
player who controls $u$, then the color $\min\leavevmode\nobreak\
\kappa_{i}(W_{v})$ is even.

Indeed, if those three points are satisfied, then for each $v$, the play
$h_{v}c_{v}^{\omega}$, where $c_{v}$ is a cycle (not necessarily simple, but
which can be chosen of size at most $(\mathrm{card}W_{v})^{2}$) that visits
all the vertices of $W_{v}$ at least once and none other, is
$\lambda$-consistent. Conversely, if from each $v$, there exists a
$\lambda$-consistent play $\rho$, then the pair $(h_{v},W_{v})$, where
$W_{v}=\mathrm{Inf}(\rho)$ and $h_{v}$ is a prefix of $\rho$ ending in $W_{v}$
in which the cycles have been removed, satisfies those three properties —
those are decidable in polynomial time. ∎

Each requirement induces a notion of rationality for a coalition of players.

######  Definition 15 ($\lambda$-rationality).

Let $\lambda$ be a requirement on the game $G$. A strategy profile
$\bar{\sigma}_{-i}$ is _$\lambda$ -rational assuming_ the strategy
$\sigma_{i}$ iff for every history $hv$ compatible with $\bar{\sigma}_{-i}$,
the play $\langle\bar{\sigma}_{\upharpoonright hv}\rangle_{v}$ is
$\lambda$-consistent. It is _$\lambda$ -rational_ if it is $\lambda$-rational
assuming some strategy. The set of $\lambda$-rational strategy profiles in
$G_{\upharpoonright v_{0}}$ is denoted by $\lambda\mathrm{Rat}(v_{0})$.

The notion of $\lambda$-rationality qualifies the _environment_ against player
$i$, i.e. the coalition of all the players except $i$: they play
$\lambda$-rationally if their strategy profile can be completed by a strategy
of player $i$, such that in every subgame, each player gets their requirement
satisfied.

But then, $\lambda$-rationality restrains the behaviours of the players
against player $i$: that one may be able to win against a $\lambda$-rational
environment while it is not the case against a fully hostile one. This is what
the _negotiation function_ captures.

######  Definition 16 (Negotiation).

The _negotiation function_ is a function that transforms every requirement
$\lambda$ into a requirement $\mathrm{nego}(\lambda)$, defined by, for each
$i\in\Pi$ and $v\in V_{i}$, and with the convention $\inf\emptyset=+\infty$:

$\mathrm{nego}(\lambda)(v)=\inf_{\bar{\sigma}_{-i}\in\lambda\mathrm{Rat}(v)}\leavevmode\nobreak\
\sup_{\sigma_{i}\in\Sigma_{i}(G_{\upharpoonright v})}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}_{-i},\sigma_{i}\rangle_{v}).$

The fixed points of the negotiation function characterize the SPEs of a game:
indeed, when some play $\rho$ is $\lambda$-consistent for some fixed point
$\lambda$, it means that it is won by every player who could ensure their
victory from a state visited by $\rho$, while playing against a rational
environment. Better: all the SPEs are characterized by the least fixed point
of the negotiation function, which exists by Tarski’s fixed point theorem, and
which we will write $\lambda^{*}$ in the rest of this paper. An equivalent
result exists for NEs, that are characterized by the requirement
$\mathrm{nego}(\lambda_{0})$, where $\lambda_{0}:v\mapsto 0$ is the _vacuous
requirement_.

######  Theorem 1.

In a prefix-independent Boolean game $G_{\upharpoonright v_{0}}$:

  * •

the set of NE plays is exactly the set of
$\mathrm{nego}(\lambda_{0})$-consistent plays;

  * •

the set of SPE plays is exactly the set of $\lambda^{*}$-consistent plays.

###### Proof.

By [2], this result is true for any prefix-independent game _with steady
negotiation_ , i.e. such that for every requirement $\lambda$, for every
player $i$ and for every vertex $v$, if there exists a $\lambda$-rational
strategy profile $\bar{\sigma}_{-i}$ from $v$, there exists one that minimizes
the quantity $\sup_{\sigma_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}_{-i},\sigma_{i}\rangle_{v}).$ In the case of
Boolean games, the function $\mu_{i}$ can only take the values $0$ and $1$,
hence this supremum is always realized. ∎

######  Example 2.

Let us consider again the game of Figure 1. Every play in that game — like in
every game — is $\lambda_{0}$-rational. The requirement
$\lambda_{1}=\mathrm{nego}(\lambda_{0})$ is equal to $1$ on the states $c$ and
$e$ (the states from which the player controlling those states can enforce the
victory), and to $0$ in each other one. Then, the $\lambda_{1}$-consistent
plays are exactly the plays supported by a Nash equilibrium: the play
$ace^{\omega}$, and the play $ab^{\omega}$.

Now, from the state $a$, the only strategy profile that can make player
$\Circle$ lose if she chooses to go to $c$ is $\sigma_{\Box}:ac\mapsto d$,
which was $\lambda_{0}$-rational but is not $\lambda_{1}$-rational: the play
$cd^{\omega}$ is not $\lambda_{1}$-consistent. Therefore, against a
$\lambda_{1}$-rational environment, player $\Circle$ can enforce the victory
by going to the state $c$, hence $\lambda_{2}(a)=1$, where
$\lambda_{2}=\mathrm{nego}(\lambda_{1})$. Then, the requirement $\lambda_{2}$
is a fixed point of the negotiation function, and consequently the least one,
hence the only play supported by an SPE from the state $a$ is the only play
that is $\lambda_{2}$-consistent, namely $ace^{\omega}$.

###  3.2 The existence of SPEs in parity games

In parity games, the existence of SPEs is guaranteed.

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

There exists an SPE in every parity game.

###### Proof sketch.

This theorem is a result due to Ummels. In App. B, we rephrase his proof in
terms of requirements and negotiation. Let us give here the main intuitions.
We define a decreasing sequence $(E_{n})_{n}$ of subsets of $E$, and an
associated sequence $(\lambda^{\prime}_{n})_{n}$ of requirements, keeping the
hypothesis that $E_{n}$ always contains at least one outgoing edge from each
vertex. First, $E_{0}=E$ and $\lambda^{\prime}_{0}$ is the vacuous
requirement. Then, for every $n$, for each player $i$ and each $v\in V_{i}$,
we define $\lambda^{\prime}_{n+1}(v)$ as equal to $1$ if and only if in the
game obtained from $G$ by removing the edges that are not in $E_{n}$, player
$i$ can enforce the victory from $v$, against a fully hostile environment.
Then, from each such state, we choose a memoryless winning strategy (which
always exists, see [11]), that is, we choose one edge to always follow to
ensure the victory, and we remove the other outgoing edges from $E_{n}$ to
obtain $E_{n+1}$. We prove that for each $n$, we have
$\lambda^{\prime}_{n+1}\geq\mathrm{nego}(\lambda^{\prime}_{n})$, hence the
sequence $(\lambda^{\prime}_{n})_{n}$ converges to a satisfiable fixed point
of the negotiation function — which is not necessarily the least one. ∎

As a consequence, in every parity game $G$, we have
$\lambda^{*}(v)\in\\{0,1\\}$: this is why in what follows, we only consider
requirements with values in $\\{0,1\\}$.

######  Example 3.

Let us consider the (Büchi) game of Figure 2(a): recall that the objective of
each player is to see infinitely often the color $0$. If we follow the
algorithm from [15], as presented above, we remove the edge $df$ — because
always going to $e$ is a winning strategy for player $\Diamond$ from $d$ — and
the edges $ba$ and $bd$ — because always going to $c$ is a winning strategy
for player $\Box$ from $b$. Then, the algorithm reaches a fixed point, see
Figure 2(b). Our proof states that every play that uses only the remaining
edges is a play supported by an SPE. Indeed, those plays are
$\lambda^{\prime}_{1}$-consistent, where $\lambda^{\prime}_{1}$ is the
requirement given in red on Figure 2(b): it is a fixed point of the
negotiation function. However, it is not the least one: for example, the play
$ab(dedf)^{\omega}$ is not $\lambda^{\prime}_{1}$-consistent, but it is also a
play that is supported by an SPE. The least fixed point is given in red on
Figure 2(a).

$a$$b$$c$$d$$e$$f$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{0}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{0}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{0}}$$(\lambda^{*})$$0$$1$$1$$1$$0$$0$
(a) A Büchi game

$a$$b$$c$$d$$e$$f$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{0}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{0}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{0}}$$(\lambda^{\prime}_{1})$$1$$1$$1$$1$$0$$0$
(b) Fixed point as computed in [15]

The interested reader will find in Appendix I an additional example of parity
game, on which we computed the iterations of the negotiation function.

###  3.3 Abstract negotiation game

Now, let us study how we can compute the negotiation function. The _abstract
negotiation game_ is a tool which already appeared in [8], and which has been
linked to the negotiation function in [2]. It opposes two players, _Prover_
and _Challenger_ : Prover constructs a $\lambda$-rational strategy profile by
proposing plays, and Challenger constructs player $i$’s response by accepting
those plays or deviating from them. We slightly simplify the definition here,
by considering only satisfiable requirements, which guarantees that Prover has
always a play to propose222In [2], a second sink state $\bot$ is added to
enable Prover to give up when she has no play to propose. Another purely
technical difference is the existence here of a mandatory transition from each
state $[hv]$ to the state $[v]$, instead of letting Prover propose a play
directly from the state $[hv]$: thus, there are few states from which Prover
has a choice to make, which will be useful in what follows..

######  Definition 17 (Abstract negotiation game).

Let $G$ be a parity game, let $\lambda$ be a satisfiable requirement, let
$i\in\Pi$ and let $v_{0}\in V_{i}$. The associated _abstract negotiation game_
is the two-player zero-sum game $\mathrm{Abs}_{\lambda
i}(G)_{\upharpoonright[v_{0}]}=\left(\\{\mathbb{P},\mathbb{C}\\},S,(S_{\mathbb{P}},S_{\mathbb{C}}),\Delta,\nu\right)_{\upharpoonright[v_{0}]}$
where:

  * •

the players $\mathbb{P}$ and $\mathbb{C}$ are called respectively _Prover_ and
_Challenger_ ;

  * •

Challenger’s states are of the form $[\rho]$, where $\rho$ is a
$\lambda$-consistent play of $G$;

  * •

Prover’s states are of the form $[hv]$, where
$h\in\mathrm{Hist}_{i}(G)\cup\\{\varepsilon\\}$ and $\mathrm{last}(h)v\in E$,
plus one additional sink state $\top$;

  * •

the set $\Delta$ contains the transitions of the forms:

    * –

$[v][\rho]$, where $\mathrm{first}(\rho)=v$: Prover proposes the play $\rho$;

    * –

$[\rho][\rho_{0}\dots\rho_{k}v]$, where $k\in\mathbb{N}$, $v\neq\rho_{k+1}$
and $\rho_{k}v\in E$: Challenger refuses and deviates;

    * –

$[hv][v]$ with $h\neq\varepsilon$: then, Prover has to propose a new play from
the vertex $v$;

    * –

$[\rho]\top$: Challenger accepts the proposed play;

    * –

$\top\top$: the game is over;

  * •

When $\pi$ is a play in the abstract negotiation game, we will use the
notation $\dot{\pi}$ to denote the play in the original game constructed by
Prover’s proposals and Challenger’s deviations. Thus, the play $\pi$ is won by
Challenger iff one of the following conditions is satisfied:

    * –

the play $\pi$ has the form
$[v_{0}][\rho^{0}][h^{0}v_{1}][v_{1}][\rho^{1}]\dots[h^{n-1}v_{n}][v_{n}][\rho^{n}]\top^{\omega},$
i.e. Challenger accepts a play proposed by Prover, and the play
$\dot{\pi}=h^{0}\dots h^{n-1}\rho^{n}$ is won by player $i$;

    * –

or the play $\pi$ has the form
$[v_{0}][\rho^{0}][h^{0}v_{1}][v_{1}][\rho^{1}][h^{1}v_{2}]\dots$, i.e.
Challenger always deviates from the play proposed by Prover, and the play
$\dot{\pi}=h^{0}h^{1}\dots$ is won by player $i$.

######  Theorem 3 ([2], Appendix E).

Let $G$ be a prefix-independant Boolean game, let $\lambda$ be a satisfiable
requirement, let $i\in\Pi$ and let $v_{0}\in V_{i}$. Then, we have
$\mathrm{nego}(\lambda)(v)=0$ if and only if Prover has a winning strategy in
the associated abstract negotiation game.333The non-existence of the sink
state $\bot$, in which Prover is supposed to get the payoff $-\infty$, does
not change this result: since $\lambda$ is assumed to be satisfiable, Prover
has always a strategy to get at least the payoff $0$, hence no optimal
strategy of Prover plans to follow a transition to $\bot$.

######  Example 4.

Let $G$ be the game from Figure 1. In this particular case, since there are
finitely many possible plays, the abstract negotiation games
$\mathrm{Abs}_{\lambda_{0}{\tiny{\Circle}}}G$ and
$\mathrm{Abs}_{\lambda_{1}{\tiny{\Circle}}}$ have a finite state space. They
are represented in Figure 3: the blue states are Prover’s states, and the
orange ones are Challenger’s. The dashed states belong to
$\mathrm{Abs}_{\lambda_{0}{\tiny{\Circle}}}G$ but not to
$\mathrm{Abs}_{\lambda_{1}{\tiny{\Circle}}}$. Observe that Prover has a
winning strategy in $\mathrm{Abs}_{\lambda_{0}{\tiny{\Circle}}}G$ (in red),
but not in $\mathrm{Abs}_{\lambda_{1}{\tiny{\Circle}}}G$.

$a$$ab^{\omega}$$acd^{\omega}$$ace^{\omega}$$ac$$\top$$ab$$c$$b$$cd^{\omega}$$ce^{\omega}$$b^{\omega}$
Figure 3: An abstract negotiation game

##  4 Algorithms

Let us now study how we can use the abstract negotiation game to solve the
problems presented in introduction. We first define an equivalence relation
between histories and between plays; then, we show that in the abstract
negotiation game, Prover can propose only plays that are simple
representatives of their equivalence class, and propose always the same play
from each vertex.

###  4.1 Reduced plays and reduced strategy

The equivalence relation that we use is based on the order in which vertices
appear.

######  Definition 18 (Occurrence-equivalence (histories)).

Two histories $h$ and $h^{\prime}$ are _occurrence-equivalent_ , written
$h\approx h^{\prime}$, iff $\mathrm{first}(h)=\mathrm{first}(h^{\prime})$,
$\mathrm{last}(h)=\mathrm{last}(h^{\prime})$ and
$\mathrm{Occ}(h)=\mathrm{Occ}(h^{\prime})$.

######  Definition 19 (Occurrence-equivalence (plays)).

Two plays $\rho$ and $\rho^{\prime}$ are _occurrence-equivalent_ , written
$\rho\approx\rho^{\prime}$, iff the three following conditions are satisfied:

  * •

$\mathrm{Inf}(\rho)=\mathrm{Inf}(\rho^{\prime})$;

  * •

for each history prefix of $\rho$, there exists a occurrence-equivalent
history prefix of $\rho^{\prime}$;

  * •

for each history prefix of $\rho^{\prime}$, there exists a occurrence-
equivalent history prefix of $\rho$.

######  Example 5.

Let us consider the game of Figure 2(a). In that game, the play
$ab(dedf)^{\omega}$ is occurrence-equivalent to the play
$abde(dedf)^{\omega}$, but not to the play $ab(dfde)^{\omega}$. Indeed, the
latter has the history $abdf$ as a prefix, which is not occurrence-equivalent
to any prefix of $ab(dedf)^{\omega}$, in which the state $f$ occurs only when
the state $e$ has already occurred.

######  Remark.

The operators $\mathrm{Occ}$, $\mathrm{Inf}$ and $\mu$ are stable by
occurrence-equivalence.

The interest of that equivalence relation lies in the finite number of its
equivalence classes, and by the existence of simple representatives of each of
them.

######  Lemma 3 (App. C).

Let $\rho$ be a play of $G$. There exists a lasso $hc^{\omega}\approx\rho$
with $|h|\leq n^{3}+n^{2}$ and $|c|\leq n^{2}$, where $n=\mathrm{card}V$.

We call such lassos _reduced plays_. For each $\rho$, we write $\tilde{\rho}$
for an arbitrary occurrence-equivalent reduced play. Then, operations such as
computing $\mu(\tilde{\rho})$, $\mathrm{Occ}(\tilde{\rho})$,
$\mathrm{Inf}(\tilde{\rho})$, or checking whether $\tilde{\rho}$ is
$\lambda$-consistent, can be done in time $O(n^{3})$.

######  Definition 20 (Reduced strategy).

A strategy $\tau_{\mathbb{P}}$ for Prover in $\mathrm{Abs}_{\lambda i}(G)$ is
_reduced_ iff it is memoryless, and for each state $v$, the play $\rho$ with
$[\rho]=\tau_{\mathbb{P}}([v])$ is a reduced play.

######  Example 6.

In Figure 3, Prover’s winning strategy, defined by the red arrows, is reduced.

If $\rho\approx\rho^{\prime}$, and if Challenger can deviate from $\rho$ after
the history $hv$, then he can also deviate in $\rho^{\prime}$ after some
history $h^{\prime}v$ that traverses the same states. Thus, Prover can play
optimally while proposing only reduced plays, and by proposing always the same
play from each vertex; that is, by following a reduced strategy.

######  Lemma 4 (App. D).

Prover has a winning strategy in the abstract negotiation game if and only if
she has a reduced one.

###  4.2 Checking that a reduced strategy is winning: the deviation graph

We have established that Prover is winning the abstract negotiation game if
and only if she has a reduced winning strategy. Such a strategy has polynomial
size and can thus be guessed in nondeterministic polynomial time. It remains
us to show that we can verify in deterministic polynomial time that a guessed
strategy is winning. For that purpose, we construct its _deviation graph_.

######  Definition 21 (Deviation graph).

Let $\tau_{\mathbb{P}}$ be a reduced strategy of Prover, and let $i\in\Pi$.
The _deviation graph_ associated to $\tau_{\mathbb{P}}$ and $v$ is the colored
graph $\mathrm{Dev}_{i}(\tau_{\mathbb{P}})$:

  * •

the vertices are the plays $\tau_{\mathbb{P}}([w])$, for every vertex $w$ of
the original game;

  * •

there is an edge from $[\tilde{\rho}]$ to $\tau_{\mathbb{P}}([w])$ with color
$c$ iff there exists $k\in\mathbb{N}$ such that $\tilde{\rho}_{k}\in V_{i}$,
$\tilde{\rho}_{k}w\in E$, $w\neq\tilde{\rho}_{k+1}$ and
$\min\kappa_{i}(\mathrm{Occ}(\tilde{\rho}_{0}\dots\tilde{\rho}_{k}))=c$.

Constructing the deviation graph associated to a memoryless strategy
$\tau_{\mathbb{P}}$ enables to decide whether $\tau_{\mathbb{P}}$ is a winning
strategy or not.

######  Lemma 5.

The reduced strategy $\tau_{\mathbb{P}}$ is winning in the abstract
negotiation game if and only if in the corresponding deviation graph, there
neither exists, from the vertex $\tau_{\mathbb{P}}([v_{0}])$:

  * •

a finite path to a vertex $[\tilde{\rho}]$ such that the play $\tilde{\rho}$
is winning for player $i$;

  * •

nor an infinite path along which the minimal color seen infinitely often is
even.

As a consequence, given a parity game $G$ and a requirement $\lambda$,
deciding whether $\lambda$ is a fixed point of the negotiation function is
$\mathbf{NP}$-easy.

###### Proof.

Given $G$ and $\lambda$, let $n$ be the number of states in $G$, and $m$ be
the number of colors. The deviation graph can be seen as the abstract
negotiation game itself, where one removed the transitions that were not
compatible with $\tau_{\mathbb{P}}$; removed the states that were not
accessible from $[v_{0}]$; and merged the paths
$[\tilde{\rho}][hv][v][\tilde{\rho}^{\prime}]$ into one edge
$[\tilde{\rho}][\tilde{\rho}^{\prime}]$ with color $\min\kappa_{i}(h)$.

Therefore, a path from the vertex $\tau_{\mathbb{P}}([v_{0}])$ can be seen as
a history (if it is finite) or a play (if it is infinite), compatible with the
strategy $\tau_{\mathbb{P}}$, in the abstract negotiation game. In particular,
the finite paths to a vertex $[\tilde{\rho}]$ with $\mu_{i}(\tilde{\rho})=1$
correspond to the histories that lead Prover to propose a play that is winning
for player $i$, that Challenger can accept to win. Similarly, the infinite
paths along which the minimal color infinitely often seen is even correspond
to the plays $\pi$ where Challenger deviates infinitely often, and constructs
the play $\dot{\pi}$ that is winning for player $i$. Such paths will be called
_winning paths_.

Now, the deviation graph has $n$ vertices, and at most $mn^{2}$ edges.
Constructing it requires a time $O(n^{4})$. Deciding the existence of a finite
winning path is a simple accessibility problem, and can be done in time
$O(mn^{2})$. Deciding the existence of an infinite winning path is similar to
deciding the emptiness of a parity automaton, and requires a time $O(mn^{3})$.
As a consequence, deciding whether a reduced strategy is winning can be done
in polynomial time — and it is an object of polynomial size.

Thus, an $\mathbf{NP}$ algorithm that decides whether the requirement
$\lambda$ is a fixed point of the negotiation function is the following: we
guess, at the same time, a certificate that proves that $\lambda$ is
satisfiable (Lemma 2), and a reduced strategy $\tau_{\mathbb{P}}^{v}$ for
Prover in $\mathrm{Abs}_{\lambda i}(G)_{\upharpoonright[v]}$, for each
$i\in\Pi$ and $v\in V_{i}$ such that $\lambda(v)=0$: by Lemma 4, there exists
such winning strategy if and only if $\mathrm{nego}(\lambda)(v)=0$. Both
certificates have polynomial size and can be checked in polynomial time. ∎

######  Example 7.

Let us consider the game of Figure 2(a), and the requirement $\lambda^{*}$,
presented on the same figure. Let $\tau_{\mathbb{P}}$ be the memoryless
strategy in the game
$\mathrm{Abs}_{\lambda^{*}{\tiny{\Circle}}}(G)_{\upharpoonright[a]}$ defined
by:

$\begin{matrix}\tau_{\mathbb{P}}([a])=ab(dedf)^{\omega}&\tau_{\mathbb{P}}([c])=c^{\omega}&\tau_{\mathbb{P}}([e])=(edfd)^{\omega}\\\
\tau_{\mathbb{P}}([b])=b(dedf)^{\omega}&\tau_{\mathbb{P}}([d])=(dedf)^{\omega}&\tau_{\mathbb{P}}([f])=(fded)^{\omega}.\end{matrix}$

The corresponding deviation graph is given by Figure 5. The purple edges have
color $0$, and the orange ones have color $1$. Observe that there is no
winning path from the vertex $\tau_{\mathbb{P}}([a])=ab(dedf)^{\omega}$: each
purple edge can be used at most once, and even though the play $c^{\omega}$ is
winning for player $\Circle$, the corresponding vertex is not accessible.
Therefore, the strategy $\tau_{\mathbb{P}}$ is winning in
$\mathrm{Abs}_{\lambda^{*}{\tiny{\Circle}}}(G)_{\upharpoonright[a]}$, which
proves the equality $\mathrm{nego}(\lambda^{*})(a)=\lambda^{*}(a)=0$.

###  4.3 Upper bounds

Let us now give the main problems for which the concepts given above yield a
solution.

$ab(dedf)^{\omega}$$b(dedf)^{\omega}$$c^{\omega}$$(dedf)^{\omega}$$(edfd)^{\omega}$$(fded)^{\omega}$

Figure 4: A deviation graph

$C_{1}$$x_{1}$$\neg x_{1}$$C_{2}$$x_{2}$$\neg x_{2}$$C_{3}$$x_{3}$$\neg
x_{3}$$C_{4}$$x_{4}$$\neg x_{4}$$C_{5}$$x_{5}$$\neg x_{5}$$C_{6}$$x_{6}$$\neg
x_{6}$$\bot$

Figure 5: The game $G_{\varphi}$

A first application is an algorithm for the SPE constrained existence problem.

######  Lemma 6.

The SPE constrained existence problem for parity games is $\mathbf{NP}$-easy.

###### Proof.

Given a parity game $G_{\upharpoonright v_{0}}$ and two thresholds $\bar{x}$
and $\bar{y}$, we first guess a reduced play $\tilde{\eta}$ from $v_{0}$, and
a requirement $\lambda$. Both have polynomial size. To check that
$\tilde{\eta}$ is an SPE play, using Theorem 1, we check that $\tilde{\eta}$
is $\lambda$-consistent in time $O(n^{3})$, and then, that $\lambda$ is a
fixed point of $\mathrm{nego}$, which is $\mathbf{NP}$-easy by Lemma 5. Then,
we check that $\bar{x}\leq\mu(\tilde{\eta})\leq\bar{y}$ in polynomial time. ∎

This algorithm does not need an effective characterization of all the SPEs in
a game, which is given by the least fixed point of the negotiation function
$\lambda^{*}$. Computing such a characterization can be done with a call to a
$\mathbf{NP}$ oracle and to a $\mathbf{coNP}$ oracle, i.e. it belongs to the
class $\mathbf{BH}_{2}$.

######  Lemma 7.

Given a parity game $G$, finding the least fixed point of the negotiation
function on $G$ can be done by a $\mathbf{BH}_{2}$ algorithm.

###### Proof.

By Lemma 5, there exists a non-deterministic algorithm that decides in
polynomial time, given a parity game $G$ and a requirement $\lambda$, whether
$\lambda$ is a fixed point of the negotiation function. This decision
algorithm can be turned into a function algorithm, if it guesses the
requirement $\lambda$ at the same time as it guesses the other data — it
yields a non-deterministic polynomial algorithm that finds one fixed point of
the negotiation function.

Then, deciding whether $\lambda$ is lesser than or equal to any fixed point
still needs to be done. This is a $\mathbf{coNP}$-easy problem, since a
negative instance can be recognized by guessing a lesser requirement
$\lambda^{\prime}$, and proving that it is a fixed point of the negotiation
function. ∎

Finally, SPE-verification requires polynomial space.

######  Lemma 8.

The SPE-verification problem is $\mathbf{PSpace}$-easy.

###### Proof.

Given a parity game $G_{\upharpoonright v_{0}}$ and an LTL formula $\varphi$,
by Lemma 5, the requirement $\lambda^{*}$ can be computed by a
$\mathbf{BH}_{2}$ algorithm, and therefore by a deterministic algorithm using
polynomial space — indeed, we have the inclusions
$\mathbf{NP}\subseteq\mathbf{PSpace}$ and
$\mathbf{coNP}\subseteq\mathbf{PSpace}$, hence an algorithm that uses one call
to an $\mathbf{NP}$ algorithm and then one to a $\mathbf{coNP}$ algorithm can
be transformed into a $\mathbf{PSpace}$ algorithm. Then, we can construct in
polynomial time into the LTL formula $\psi_{\lambda^{*}}$, that is satisfied
exactly by the $\lambda^{*}$-consistent plays:

$\psi_{\lambda^{*}}=\bigwedge_{i}\bigwedge_{v\in
V_{i},\lambda^{*}(v)=1}\left(\mathbf{F}v\Rightarrow\bigvee_{2k\leq
m}\left(\bigvee_{\kappa_{i}(w)=2k}\mathbf{G}\mathbf{F}w\wedge\bigvee_{\kappa_{i}(w)<2k}\mathbf{F}\mathbf{G}\neg
w\right)\right),$

where $m$ is the largest color appearing in $G$.

Then, deciding whether there exists an SPE play in $G_{\upharpoonright v_{0}}$
that satisfies the formula $\varphi$ is equivalent to decide whether there
exists a play in $G_{\upharpoonright v_{0}}$ that satisfies the formula
$\varphi\wedge\psi_{\lambda^{*}}$. As for any LTL formula, that can be done
using polynomial space: see for example [14]. ∎

###  4.4 Fixed-parameter tractability

We end this section by mentioning an additional complexity result on the SPE
constrained existence problem: it is fixed-parameter tractable.

######  Theorem 4 (App. E).

The SPE constrained existence problem on parity games is fixed-parameter
tractable when the number of players and the number of colors are parameters.
More precisely, there exists a deterministic algorithm that solves that
problem in time $O(2^{2^{pm}}n^{12})$, where $n$ is the number of vertices,
$p$ is the number of players and $m$ is the number of colors.

###### Proof sketch.

This result is obtained by constructing and solving a generalized parity game
on a finite arena, that is exponential in the number of players and polynomial
in the size of the original game. This game, called the _concrete_ negotiation
game, is equivalent to the abstract negotiation game. Its construction is
inspired by a construction that we have introduced in [2], for games with
mean-payoff objectives. The main idea of this construction is to decompose the
plays proposed by Prover, by passing them to Challenger edges by edges, and by
encoding the $\lambda$-consistence condition into a generalized parity
condition. Then, we can apply a FPT algorithm to solve generalized parity
games that was first proposed in [6]. While this deterministic algorithm does
not improve on the worst-case complexity of the deterministic
$\mathbf{ExpTime}$ algorithm of [15], it allows for a finer parametric
analysis. ∎

##  5 Matching lower bounds

In this section, we provide matching complexity lower bounds for the problems
we adressed in the previous section. For that purpose, we first need the
following construction, inspired from a game designed by Ummels in [9] to
prove the $\mathbf{NP}$-hardness of the SPE constrained existence problem. Our
definition is slightly different: while Ummels defined one player per
variable, we need one player per literal. However, the core intuitions are the
same.

######  Definition 22 ($G_{\varphi}$).

Let $\varphi=\bigwedge_{j\in\mathbb{Z}/m\mathbb{Z}}C_{j}$ be a formula of the
propositional logic, constructed on the finite set of variables
$\\{x_{1},\dots,x_{n}\\}$. We define the parity game $G_{\varphi}$ as follows.

  * •

The players are the variables $x_{1},\dots,x_{n}$, their negations, and
_Solver_ , denoted by $\mathbb{S}$.

  * •

The states controlled by Solver are all the clauses $C_{j}$, and the sink
state $\bot$.

  * •

The states controlled by player $L=\pm x_{i}$ are the pairs $(C_{j},L)$, where
$L$ is a literal of $C_{j}$.

  * •

There are edges from each clause state $C_{j}$ to all the states $(C_{j},L)$;
from each pair state $(C_{j},L)$ to the state $C_{j+1}$, and to the sink state
$\bot$; and from the sink state $\bot$ to itself.

  * •

For Solver, every state has the color $\kappa_{\mathbb{S}}(v)=2$, except the
state $\bot$, which has color $1$.

  * •

For each literal player $L$, every state has the color $\kappa_{L}(v)=2$,
except the states of the form $(C,\overline{L})$, that have the color $1$.

######  Remark.

The game $G_{\varphi}$ is a coBüchi game: Solver has to avoid the sink state
$\bot$, and player $L$ the states of the form $(C,\overline{L})$. Therefore,
all the following theorems can also be applied to the more restrictive class
of coBüchi games.

######  Example 8.

The game $G_{\varphi}$, when $\varphi$ is the tautology
$\bigwedge_{j=1}^{6}(x_{j}\vee\neg x_{j})$, is given by Figure 5.

The game $G_{\varphi}$ is strongly linked with the satisfiability of
$\varphi$, in the following formal sense.

######  Lemma 9 (App. F).

The game $G_{\varphi}$ has the following properties.

  * •

The least fixed point of the negotiation function is equal to $0$ on the
states controlled by Solver, and to $1$ on the other ones.

  * •

For every SPE play $\rho$ in $G_{\varphi}$ that does not reach $\bot$, the
formula $\varphi$ is satisfied by:

$\nu_{\rho}:x\mapsto\left\\{\begin{matrix}1&\mathrm{if\leavevmode\nobreak\
}\exists C,(C,x)\in\mathrm{Inf}(\rho)\\\
0&\mathrm{otherwise}.\end{matrix}\right.$

  * •

Conversely, for every valuation $\nu$ satisfying $\varphi$, the play
$\rho_{\nu}=(C_{1}(C_{1},L_{1})\dots C_{m}(C_{m},L_{m}))^{\omega},$ where for
each $j$, the literal $L_{j}$ is satisfied by $\nu$, is an SPE play.

A first consequence is the lower bound on the complexity of deciding whether
some requirement is, or not, a fixed point of the negotiation function.

######  Theorem 5.

Given a parity game $G$ and a requirement $\lambda$, deciding whether
$\lambda$ is a fixed point of the negotiation function is
$\mathbf{NP}$-complete.

###### Proof.

Easiness is given by Lemma 5. For hardness, we proceed by reduction from the
$\mathbf{NP}$-complete problem Sat. Given a formula
$\varphi=\bigwedge_{j\in\mathbb{Z}/m\mathbb{Z}}C_{j}$ of the propositional
logic, we can construct the game $G_{\varphi}$ in polynomial time. Then, let
us define on $G_{\varphi}$ the requirement $\lambda$ that is constantly equal
to $1$, except in $\bot$, where it is equal to $0$. Since there is no winning
play for Solver from $\bot$, the requirement $\lambda$ is a fixed point of the
negotiation function if and only if there exists a $\lambda$-consistent play
from each vertex. If it is the case, then let $\rho$ be a $\lambda$-consistent
play from $C_{1}$. Since $\lambda\geq\lambda^{*}$, the play $\rho$ is also
$\lambda^{*}$-consistent, and is therefore an SPE play. It is also a play won
by Solver, since $\lambda(C_{1})=1$: therefore, it does not reach the state
$\bot$. Then, by Lemma 9, we can define the valuation $\nu_{\rho}$, which
satisfies $\varphi$.

Conversely, if $\nu$ is a valuation satisfying $\varphi$, then the play
$\rho_{\nu}$ is an SPE play from $C_{1}$, and it does not end in $\bot$, hence
it is won by Solver, and is therefore $\lambda$-consistent. If we consider the
suffixes of $\rho_{\nu}$, we find a $\lambda^{*}$-consistent play from each
state $C_{j}$; and from the states of the form $(C_{j},L)$, the play
$(C_{j},L)\bot^{\omega}$ is $\lambda^{*}$-consistent, hence there is a
$\lambda^{*}$-consistent play from each vertex: deciding whether $\lambda$ is
a fixed point of the negotiation function is $\mathbf{NP}$-hard. ∎

A similar proof ensures the same lower bound on the SPE constrained existence
problem.

######  Theorem 6.

The SPE constrained existence problem in parity games is
$\mathbf{NP}$-complete.

###### Proof.

Easiness is given by Lemma 6. For hardness, we proceed by reduction from the
problem Sat. Given a formula
$\varphi=\bigwedge_{j\in\mathbb{Z}/m\mathbb{Z}}C_{j}$ of the propositional
logic, we can construct the game $G_{\varphi}$ in polynomial time. By Lemma 9,
there exists an SPE play from $C_{1}$ and won by Solver, i.e. an SPE play from
$C_{1}$ that does not reach the sink state $\bot$, if and only if there exists
a valuation satisfying $\varphi$: the SPE constrained existence problem is
$\mathbf{NP}$-hard. ∎

Now, we show that the algorithm we presented to compute $\lambda^{*}$ is
optimal as well.

######  Theorem 7 (App. G).

Given a parity game $G$ and a requirement $\lambda$, deciding whether
$\lambda=\lambda^{*}$ is $\mathbf{BH}_{2}$-complete. Given a parity game $G$,
computing $\lambda^{*}$ can be done by a non-deterministic algorithm in
polynomial time iff $\mathbf{NP}=\mathbf{BH}_{2}$.

Finally, the LTL model-checking problem easily reduces to the SPE-verification
problem, which gives us the mathcing lower bound.

######  Theorem 8 (App. H).

The SPE-verification problem is $\mathbf{PSpace}$-complete.

## References

  * [1] Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas.  Non-zero sum games for reactive synthesis.  In Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings, volume 9618 of Lecture Notes in Computer Science, pages 3–23. Springer, 2016.
  * [2] Léonard Brice, Jean-François Raskin, and Marie van den Bogaard.  Subgame-perfect equilibria in mean-payoff games.  CoRR, 2021.
  * [3] Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, and Marie van den Bogaard.  The complexity of subgame perfect equilibria in quantitative reachability games.  In CONCUR, volume 140 of LIPIcs, pages 13:1–13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [4] Thomas Brihaye, Julie De Pril, and Sven Schewe.  Multiplayer cost games with simple nash equilibria.  In Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6-8, 2013. Proceedings, volume 7734 of Lecture Notes in Computer Science, pages 59–73. Springer, 2013.
  * [5] Véronique Bruyère.  Computer aided synthesis: A game-theoretic approach.  In Developments in Language Theory - 21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings, volume 10396 of Lecture Notes in Computer Science, pages 3–35. Springer, 2017.
  * [6] Véronique Bruyère, Quentin Hautem, and Jean-François Raskin.  Parameterized complexity of games with monotonically ordered omega-regular objectives.  In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 29:1–29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.  doi:10.4230/LIPIcs.CONCUR.2018.29.
  * [7] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman.  Generalized parity games.  In Helmut Seidl, editor, Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings, volume 4423 of Lecture Notes in Computer Science, pages 153–167. Springer, 2007\.  doi:10.1007/978-3-540-71389-0\\_12.
  * [8] János Flesch and Arkadi Predtetchinski.  A characterization of subgame-perfect equilibrium plays in borel games of perfect information.  Math. Oper. Res., 42(4):1162–1179, 2017.
  * [9] Erich Grädel and Michael Ummels.  Solution Concepts and Algorithms for Infinite Multiplayer Games.  In Krzysztof Apt and Robert van Rooij, editors, New Perspectives on Games and Interaction, volume 4 of Texts in Logic and Games, pages 151–178. Amsterdam University Press, 2008.  URL: http://www.logic.rwth-aachen.de/~ummels/knaw07.pdf.
  * [10] Eryk Kopczynski.  Half-positional determinacy of infinite games.  In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II, volume 4052 of Lecture Notes in Computer Science, pages 336–347. Springer, 2006.
  * [11] Ralf Küsters.  Memoryless determinacy of parity games.  In Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors, Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science, pages 95–106. Springer, 2001.  doi:10.1007/3-540-36387-4\\_6.
  * [12] Noémie Meunier.  Multi-Player Quantitative Games: Equilibria and Algorithms.  PhD thesis, Université de Mons, 2016.
  * [13] Christos H. Papadimitriou.  Computational complexity.  Academic Internet Publ., 2007.
  * [14] Philippe Schnoebelen.  The complexity of temporal logic model checking.  In Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev, editors, Advances in Modal Logic 4, papers from the fourth conference on "Advances in Modal logic," held in Toulouse, France, 30 September - 2 October 2002, pages 393–436. King’s College Publications, 2002\.
  * [15] Michael Ummels.  Rational behaviour and strategy construction in infinite multiplayer games.  In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 212–223. Springer, 2006.
  * [16] Gerd Wechsung.  On the boolean closure of NP.  In Lothar Budach, editor, Fundamentals of Computation Theory, FCT ’85, Cottbus, GDR, September 9-13, 1985, volume 199 of Lecture Notes in Computer Science, pages 485–493. Springer, 1985.

The following appendices are providing the detailed proofs of some results
given in the main body of this paper. They are not necessary to understand our
results and are meant to provide full formalization and rigorous proofs. To
improve readability, we have chosen to recall the statements that appeared in
the main body of the paper.

##  Appendix A Proof of Lemma 1

Lemma 1. _The problem $\textsc{Sat}\times\textsc{coSat}$ is
$\mathbf{BH}_{2}$-complete._

###### Proof.

Given a pair $(\varphi_{1},\varphi_{2})$, the problem
$\textsc{Sat}\times\textsc{coSat}$ can be decided by, first, deciding whether
$\varphi_{1}$ is satisfiable, which is $\mathbf{NP}$-easy, and second,
deciding whether $\varphi_{2}$ is not, which is $\mathbf{coNP}$-easy. The
problem $\textsc{Sat}\times\textsc{coSat}$ is therefore
$\mathbf{BH}_{2}$-easy.

Now, let us prove that it is $\mathbf{BH}_{2}$-hard; or in other words, that
any $\mathbf{BH}_{2}$-easy problem can be reduced to it in polynomial time.
Let $P\cap Q$ be a $\mathbf{BH}_{2}$-easy problem, where $P$ is
$\mathbf{NP}$-easy and $Q$ is $\mathbf{coNP}$-easy, and both are defined on
the instance set $I$.

Since Sat is $\mathbf{NP}$-complete, there exists a reduction function
$f:I\to\mathcal{F}$, where $\mathcal{F}$ is the set of the instances of Sat,
which is computable in polynomial time and such that for every instance $x\in
I$, we have $x\in P$ if and only if $f(x)$ is a satisfiable formula.
Identically, there exists a reduction function $g:I\to\mathcal{F}$ which is
computable in polynomial time and such that for every instance $x\in I$, we
have $x\in Q$ if and only if $f(x)$ is a non-satisfiable formula.

Then, we can define the function $h:x\mapsto(f(x),g(x))$, which is computable
in polynomial time, and which maps every instance $x$ of $P\cap Q$ to an
instance $h(x)$ of $\textsc{Sat}\times\textsc{coSat}$, such that $h(x)$ is a
positive instance of $\textsc{Sat}\times\textsc{coSat}$ if and only if $x$ is
a positive instance of $P\cap Q$. The problem
$\textsc{Sat}\times\textsc{coSat}$ is $\mathbf{BH}_{2}$-complete. ∎

##  Appendix B Proof of Theorem 2

Theorem 2. _There exists an SPE in every parity game._

###### Proof.

This result has already been proved by Ummels in [15]. Here, we present a
variation of his proof, that uses the concepts of requirements and
negotiation. Let $G$ be a parity game.

Let us define a decreasing sequence $(E_{n})_{n}$ of subsets of $E$, and an
associated sequence $(\lambda^{\prime}_{n})_{n}$ of requirements, keeping the
hypothesis that $E_{n}$ always contains at least one outgoing edge from each
vertex. First, $E_{0}=E$ and $\lambda^{\prime}_{0}$ is the vacuous
requirement. Then, for every $n$ and each player $i$, let us consider the two-
player zero-sum game $G_{i}^{n}$, defined as the game $G$ where each edge
$uv\not\in E_{n}$ has been removed, and where all the players $j\neq i$ are
coalized as one unique player $-i$, whose objective is to make player $i$
lose. As proved in [15], player $i$ has a memoryless uniformly optimal
strategy $\sigma^{n}_{i}$ in $G_{i}^{n}$, i.e. a memoryless strategy that is
winning from each state from which player $i$ has a winning strategy. We
define, for each state $v\in V_{i}$:

$\lambda^{\prime}_{n+1}(v)=\inf_{\bar{\tau}_{-i}\in\Sigma_{-i}(G_{i}^{n})}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}_{-i},\sigma^{n}_{i}\rangle_{v}),$

and:

$E_{n+1}=E_{n}\setminus\bigcup_{i}\\{uv\leavevmode\nobreak\
|\leavevmode\nobreak\ u\in
V_{i},\lambda^{\prime}_{n+1}(u)=1,\mathrm{\leavevmode\nobreak\
and\leavevmode\nobreak\ }\sigma^{n}_{i}(u)\neq v\\}.$

As desired, the set $E_{n+1}$ contains at least one outgoing edge from each
vertex.

Note that as a consequence, all the requirements $\lambda^{\prime}_{n}$ have
their values in $\\{0,1\\}$: we have $\lambda^{\prime}_{n+1}(v)=1$ if the
strategy $\sigma^{n}_{i}$ is winning from $v$, and $0$ otherwise.

We prove by induction that for each $n$, every play that contains only edges
from $E_{n}$ is $\lambda^{\prime}_{n}$-consistent. It is clear for $n=0$,
since every play is $\lambda_{0}$-consistent.

Now, if that property is true for some $n\in\mathbb{N}$, let $i\in\Pi$ and
$w\in V_{i}$ be such that $\lambda^{\prime}_{n+1}(w)\geq 1$: the strategy
$\sigma^{n}_{i}$ is winning from $w$ in the game $G^{n}_{i}$. Let then $\rho$
be a play in $G_{\upharpoonright w}$, that uses only edges from $E_{n+1}$:
seen as a play in $G^{n}_{i\upharpoonright w}$, it is compatible with the
strategy $\sigma^{n}_{i}$, and therefore winning for player $i$. Every play
using only edges from $E_{n+1}$ is $\lambda^{\prime}_{n+1}$-consistent.

Now, let us prove that for each $n$, we have
$\lambda^{\prime}_{n+1}\geq\mathrm{nego}(\lambda^{\prime}_{n})$. Let $i\in\Pi$
and $v\in V_{i}$ be a vertex such that $\lambda^{\prime}_{n+1}(v)=0$: in the
game $G^{n}_{i}$, the player $-i$ has a strategy $\sigma_{-i}$ against which
player $i$ cannot win. As a consequence, the strategy $\sigma_{-i}$ prevents
player $i$ to access to any state $w\in V_{i}$ such that
$\lambda^{\prime}_{n+1}(w)=1$; and therefore, to any state controlled by
player $i$ from which edges have been removed. In other words, player $i$
could not win against $\sigma_{-i}$ even using edges that are not in $E_{n}$.

The strategy $\sigma_{-i}$ can be seen as a strategy profile
$\bar{\sigma}_{-i}$ in the game $G$, which is $\lambda^{\prime}_{n}$-rational
by the previous result. Player $i$ cannot win in $G_{\upharpoonright v}$
against $\bar{\sigma}_{-i}$, hence $\mathrm{nego}(\lambda^{\prime}_{n})(v)=0$.

But then, since the sequence $(\lambda^{\prime}_{n})_{n}$ is made of
requirements with values in $\\{0,1\\}$, it necessarily reaches a limit
$\lambda$ with values in $\\{0,1\\}$. By the previous property, that limit is
such that $\lambda\geq\mathrm{nego}(\lambda)$, i.e. it is a fixed point of the
negotiation function; and since $\mathrm{nego}(\lambda)(v)<+\infty$ for each
$v$, it is a satisfiable requirement. Therefore, by Theorem 1, there always
exists an SPE in every parity game. ∎

##  Appendix C Proof of Lemma 3

Lemma 3. _Let $\rho$ be a play of $G$. There exists a lasso
$hc^{\omega}\approx\rho$ with $|h|\leq n^{3}+n^{2}$ and $|c|\leq n^{2}$, where
$n=\mathrm{card}V$._

###### Proof.

Let us write $W_{0}\subset\dots\subset W_{t}$ for all the sets of the form
$\mathrm{Occ}(\rho_{0}\dots\rho_{k})$ with $k\in\mathbb{N}$, without
repetition. Note that for each index $s\in\\{0,\dots,t-1\\}$, the set
$W_{s+1}$ contains the set $W_{s}$ plus one additional vertex.

Let us construct the history $h$ and the cycle $c$ as follows, maintaining the
hypothesis that for all $p$, the set $\mathrm{Occ}(h_{0}\dots h_{p})$ is equal
to $W_{s}$ for some $s$.

  * •

First, $h_{0}=\rho_{0}$, and $\\{h_{0}\\}=W_{0}$;

  * •

then, when the prefix $h_{0}\dots h_{p}$ is constructed: let $s$ be such that
$\mathrm{Occ}(h_{0}\dots h_{p})=W_{s}$, and let $k$ be the minimal integer
such that $\rho_{0}\dots\rho_{k}=W_{s}$.

Let $U$ be the set of all the vertices $u$ such that there exists $\ell$ with
$\mathrm{Occ}(\rho_{0}\dots\rho_{\ell})=W_{s}$ and $\rho_{\ell}=u$: any such
$\ell$ is greater than or equal to $k$, and $U\subseteq W_{s}$. Then, there
exists at least one path from $\rho_{k}=h_{p}$ that traverses all the vertices
of $U$ and only them. Let $h_{p}\dots h_{q}$ be such a path with minimal
length: it has at most length $n^{2}$.

If $s<t$, let now $\ell$ be the minimal index greater than $k$ such that
$\mathrm{Occ}(\rho_{0}\dots\rho_{\ell})=W_{s+1}$. Then, there exists a path
from $h_{q}\in W_{s}$ to $\rho_{\ell}$ that uses only vertices of $U$: let
$h_{q}\dots h_{r}$ be such a path with minimal length. Then, it traverses all
vertices at most once, and has therefore length at most $n$.

If $s=t$, let $h_{q}\dots h_{r}$ be a path of minimal length from $h_{q}$ to a
vertex $h_{r}\in\mathrm{Inf}(\rho)$: for the same reasons as above, such a
path exists and has length at most $n$. Then, we can stop here the
construction of $h$, and observe that the vertex $h_{r}$ belongs to the graph
$(\mathrm{Inf}(\rho),E\cap\mathrm{Inf}(\rho)^{2})$, which is strongly
connected. We can therefore choose a cycle $c$ that traverses all its vertices
and only them, and that has length at most $n^{2}$.

By construction, the lasso $hc^{\omega}$ is occurrence-equivalent to $\rho$,
and satisfies the desired size conditions. ∎

##  Appendix D Proof of Lemma 4

Lemma 4. _Prover has a winning strategy in the abstract negotiation game if
and only if she has a reduced one._

###### Proof.

Let us consider the _reduced negotiation game_ , i.e. the abstract negotiation
game in which one would have removed all the states but:

  * •

those of the form $[\tilde{\rho}]$, where $\tilde{\rho}$ is a reduced play;

  * •

those of the form $[hv]$, where $h$ is a prefix of a $\lambda$-consistent
reduced play $\tilde{\rho}$, and has minimal length among the occurrence-
equivalent prefixes of $\tilde{\rho}$.

By Lemma 3, if $G$ has $n$ vertices, then this game has at most
$n^{n^{3}+2n^{2}}(n^{3}+3n^{2})+1$.

Let us first notice a useful property of that game.

######  Lemma 10.

Either Prover or Challenger has a memoryless winning strategy in the reduced
negotiation game.

###### Proof.

By [10], this result is true if both Prover’s and Challenger’s objectives are
prefix-independent and _convex_ , on a game with finitely many states. By
_convex_ , we mean that for all winning plays $\pi,\pi^{\prime}$ and for any
two sequences $k_{1}<k_{2}<\dots$ and $\ell_{0}<\ell_{1}<\dots$, with
$\pi^{\prime}_{\ell_{p}}=\pi_{k_{q}}$ for all $p,q\in\mathbb{N}$, the play:

$\chi=\pi_{0}\dots\pi_{k_{1}}\pi^{\prime}_{1}\dots\pi^{\prime}_{\ell_{1}}\pi_{k_{1}+1}\dots\pi_{k_{2}}\pi^{\prime}_{\ell_{1}+1}\dots$

must also be winning. The plays of the form of $\chi$ are called _shufflings_
of $\pi$ and $\pi^{\prime}$.

If $\pi$ and $\pi^{\prime}$ are plays in the reduced negotiation game, we
observe that the play $\dot{\chi}$ is also a shuffling of the plays
$\dot{\pi}$ and $\dot{\pi}^{\prime}$. The convexity of Prover’s and
Challenger’s objectives is then a consequence of the convexity of parity
objectives: the minimal color seen infinitely often by player $i$ in
$\dot{\chi}$ is the minimum of the minimal colors seen infinitely often in
$\dot{\pi}$ and in $\dot{\pi}^{\prime}$. ∎

We can now prove our theorem by using the equivalence between the abstract and
the reduced negotiation game.

  * •

_If Prover has a winning strategy in the abstract negotiation game, she has
one in the reduced negotiation game._

Indeed, if Prover has no winning strategy in the reduced game, then, by Lemma
10, Challenger has a memoryless one: let us write it $\tau_{\mathbb{C}}$.

Now, let us extend $\tau_{\mathbb{C}}$ into a memoryless winning strategy
$\tau_{\mathbb{C}}^{\star}$ in the abstract game.

Let $[\rho]\in S_{\mathbb{C}}$, and let
$[hvw]=\tau_{\mathbb{C}}([\tilde{\rho}])$. By occurrence-equivalence, there
exists $k\in\mathbb{N}$ such that $\rho_{k}=v$, and
$\mathrm{Occ}(\rho_{0}\dots\rho_{k})=\mathrm{Occ}(hv)$. We then set
$\tau_{\mathbb{C}}^{\star}([\rho])=[\rho_{0}\dots\rho_{k}w]$. Note that the
states $\tau_{\mathbb{C}}^{\star}([\rho])=[\rho_{0}\dots\rho_{k}w]$ and
$\tau_{\mathbb{C}}([\tilde{\rho}])=[hvw]$ can be different, but they both have
as unique successor the state $[w]$.

Let us prove, now, that $\tau_{\mathbb{C}}^{\star}$ is winning: let
$\pi^{\star}$ be a play compatible with $\tau_{\mathbb{C}}^{\star}$. When
Prover proposes a play $\rho$, in the abstract game, against the strategy
$\tau_{\mathbb{C}}^{\star}$, and when she proposes the play $\tilde{\rho}$ in
the reduced game against the strategy $\tau_{\mathbb{C}}$, the same thing
happens in both cases: either Challenger accepts in both games, or he
deviates, and Prover has to propose a new play from the same state $w$.
Therefore, we can define from $\pi^{\star}$ a play $\pi$ compatible with
$\tau_{\mathbb{C}}$ in the reduced game, in which each Challenger’s state
$[\rho]$ is replaced by the state $[\tilde{\rho}]$, and Prover’s states are
replaced accordingly.

Since the play $\pi$ is compatible with $\tau_{\mathbb{C}}$, it is winning for
Challenger: let us then prove that so is $\pi^{\star}$. If $\pi^{\star}$ has
the form $H[\rho]\top^{\omega}$, then $\pi$ has the form
$H^{\prime}[\tilde{\rho}]\top^{\omega}$, hence $\tilde{\rho}$ is winning for
player $i$, and therefore $\rho$ is winning for player $i$ and $\pi^{\star}$
is winning for Challenger. If $\pi$ never reaches the state $\top$, then we
have $\dot{\pi}=h^{0}h^{1}\dots$ and
$\dot{\pi}^{\star}=h^{0\star}h^{1\star}\dots$ where, for every $k$, the
histories $h^{k}$ and $h^{k\star}$ are possibly different, but contain exactly
the same vertices. Then, the set of player $i$’s colors appearing infinitely
often in $\dot{\pi}$ and $\dot{\pi}^{\star}$ are the same, and the play
$\dot{\pi}^{\star}$ is winning for player $i$, i.e. the play $\pi^{\star}$ is
winning for Challenger: the strategy $\tau^{\star}_{\mathbb{C}}$ is winning.

  * •

_If Prover has a winning strategy in the reduced negotiation game, she has a
reduced one in the abstract negotiation game._

Indeed, let $\tau_{\mathbb{P}}$ be a winning strategy for Prover in the
reduced negotiation game. By Lemma 10, we can assume without loss of
generality that $\tau_{\mathbb{P}}$ is memoryless. Since in the abstract game,
the only states controlled by Prover where she has several possible choices
are the ones of the form $[v]$, for $v\in V$, we can see $\tau_{\mathbb{P}}$
as a reduced strategy in the abstract game: let us write it
$\tau_{\mathbb{P}}^{\star}$ in that case. We now have to prove that
$\tau_{\mathbb{P}}^{\star}$ is also a winning strategy.

Let $\pi^{\star}$ be a play in the abstract negotiation game compatible with
$\tau_{\mathbb{P}}^{\star}$. For any sequence of states
$[v][\tilde{\rho}][hw][w]$ that appears in $\pi^{\star}$, the history $h$ is
occurrence-equivalent to some prefix $\tilde{h}$ of $\tilde{\rho}$ such that
$[\tilde{h}w]$ is a state of the reduced game. Therefore, we can transform the
play $\pi^{\star}$ into a play $\pi$ of the reduced game, compatible with
$\tau_{\mathbb{P}}$, where each state of the form $[hw]$ have been replaced by
$[\tilde{h}w]$. Since $\tau_{\mathbb{P}}$ is a winning strategy in the reduced
negotiation game, the play $\pi$ is winning for Prover — let us prove that so
is $\pi^{\star}$.

If $\pi^{\star}$ has the form $H[\tilde{\rho}]\top^{\omega}$, then $\pi$ has
the form $H^{\prime}[\tilde{\rho}]\top^{\omega}$, and since $\pi$ is winning
for Prover, the play $\tilde{\rho}$ is losing for player $i$, and therefore
the play $\pi^{\star}$ is winning for Prover. If $\pi^{\star}$ has the form:

$\pi^{\star}=[v_{0}][\tilde{\rho}^{0}][h^{0}v_{1}][v_{1}][\tilde{\rho}^{1}][h^{1}v_{2}]\dots$

then:

$\pi=[v_{0}][\tilde{\rho}^{0}][\tilde{h}^{0}v_{1}][v_{1}][\tilde{\rho}^{1}][\tilde{h}^{1}v_{2}]\dots$

and since for each $k$, we have
$\mathrm{Occ}(h^{k})=\mathrm{Occ}(\tilde{h}^{k})$, we find
$\mathrm{Inf}(h^{0}h^{1}\dots)=\mathrm{Inf}(\tilde{h}^{0}\tilde{h}^{1}\dots)$
and therefore, if $\pi$ is winning for Prover, so is $\pi^{\star}$.

The strategy $\tau_{\mathbb{P}}^{\star}$ is a reduced winning strategy.

Therefore, if Prover has a winning strategy in the abstract negotiation game,
she has a reduced one. ∎

##  Appendix E Proof of Theorem 4

Theorem 4. _The SPE constrained existence problem on parity games is fixed-
parameter tractable when the number of players and the number of colors are
parameters. More precisely, there exists a deterministic algorithm that solves
that problem in time $O(2^{2^{pm}}n^{12})$, where $n$ is the number of
vertices, $p$ is the number of players and $m$ is the number of colors._

###### Proof.

Let $G$ be a parity game, let $i\in\Pi$, and let $v_{0}\in V_{i}$. Let us
assume, without loss of generality, that $m$ is even, and that the vertices of
$G$ or labelled by the colors $0,\dots,m-1$. Let $\lambda$ be a requirement.
The value of $\mathrm{nego}(\lambda)(v_{0})$ can be computed using the
following lemma.

######  Lemma 11.

We have $\mathrm{nego}(\lambda)(v_{0})=0$ if and only if Prover has a winning
strategy in the _concrete negotiation game_ $\mathrm{Conc}_{\lambda
i}(G)_{\upharpoonright s_{0}}$, defined as follows:

  * •

the two players are Prover, denoted by $\mathbb{P}$, and Challenger, denoted
by $\mathbb{C}$;

  * •

Prover’s states are the states of the form $(u,P)$, of which $u\in V$ is the
_current vertex_ and $P\subseteq\Pi$ is the _memory_ ;

  * •

Challenger’s states are the states of the form $(uv,P)$, with $uv\in E$ and
$P\subseteq\Pi$;

  * •

there is a transition from each state $(u,P)$ to each state $(uv,P)$ (such a
transition is called _proposal_), and from each state $(uv,P)$ to the state
$(v,P)$ if $\lambda(v)=0$ and $(v,P\cup\\{j\\})$ if $\lambda(v)=1$, where
$v\in V_{j}$ (_acceptation_), and to each state $(w,\\{j\\})$, with $w\in
V_{j}$, $w\neq v$ and $uw\in E$ (_deviation_);

  * •

the zero-sum Boolean outcome function $\nu$ is defined as follows: Prover wins
a play $\pi$ if and only if the color
$\min\hat{\kappa}_{d}(\mathrm{InfTr}(\pi))$ is even for each _dimension_
$d\in\Pi\cup\\{\star\\}$, where $\mathrm{InfTr}(\pi)$ is the set of the
transitions used infinitely often in $\pi$, and where the colors
$\hat{\kappa}_{d}$ are defined (on transitions) as follows:

    * –

if $d\in\Pi$ (a _non-main dimension_), then $\hat{\kappa}_{d}(st)=m$ when $st$
is a proposal, $\hat{\kappa}_{d}(st)=0$ when $st$ is a deviation, and:

$\hat{\kappa}_{d}((uv,P)(v,Q)=\left\\{\begin{matrix}\kappa_{d}(v)&\mathrm{if\leavevmode\nobreak\
}d\in P\\\ m&\mathrm{otherwise},\end{matrix}\right.$

when $(uv,P)(v,Q)$ is an acceptation;

    * –

if $d=\star$ (the _main dimension_), then $\hat{\kappa}_{d}(st)=m$ when $st$
is a proposal, and:

$\hat{\kappa}_{d}((uv,P),(w,Q))\leavevmode\nobreak\ =\leavevmode\nobreak\
\kappa_{i}(w)+1$

when $(uv,P)(w,Q)$ is an acceptation or a deviation;

  * •

the initial state is $s_{0}=(v_{0},\\{i\\})$ if $\lambda(v_{0})=1$, and
$s_{0}=(v_{0},\emptyset)$ otherwise.

###### Proof.

A similar tool has been defined for mean-payoff games in [2]. As a
consequence, this proof is very similar to the proof of Theorem 3 of the same
paper.

  * •

_If Prover has a winning strategy $\tau_{\mathbb{P}}$ in the concrete
negotiation game._ Let $\bar{\sigma}$ be the strategy profile in the original
game defined as follows. For every history $h_{0}\dots h_{k}$ compatible with
$\bar{\sigma}_{-i}$, let:

$H=(h_{0},P_{0})(h_{0}h^{\prime}_{0},P_{0})\dots(h_{k},P_{k})$

be the only history of that form that is compatible with the strategy
$\tau_{\mathbb{P}}$. Let $(h_{k}v,P_{k})=\tau_{\mathbb{P}}(H)$. We define
$\bar{\sigma}(h_{0}\dots h_{k})=v$. Thus, the strategy profile $\bar{\sigma}$
is defined after every history compatible with $\bar{\sigma}_{-i}$, and we
define it arbitrarily after the other histories.

The strategy profile $\bar{\sigma}_{-i}$ is $\lambda$-rational assuming
$\sigma_{i}$: indeed, let $hv=h_{0}\dots h_{k-1}v$ be a history compatible
with $\bar{\sigma}_{-i}$, and let $\rho=\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v}$. Let us assume that $\rho$ is not $\lambda$-consistent.
Without loss of generality, we assume that $\mu_{j}(\rho)=0$, where $j$ is the
player controlling the state $v$, while $\lambda(v)=1$ (if needed, we extend
$hv$ and shorten $\rho$). Then, the integer
$\min\kappa_{j}(\mathrm{Inf}(\rho))$ is odd.

Let us now consider, in the concrete negotiation game, the play:

$\pi=(h_{0},P_{0})(h_{0}h^{\prime}_{0},P_{0})\dots(h_{k-1}h^{\prime}_{k-1},P_{k-1})(v,P_{k})(v\rho_{1},P_{k})(\rho_{1},P_{k+1})\dots,$

compatible with $\tau_{\mathbb{P}}$. That play contains only proposals and
acceptations after the $2k$th step. Therefore, the memory $P_{k}$ is contained
in the memories $P_{\ell}$ for $\ell>k$, and it contains $j$ since $v\in
V_{j}$ and $\lambda(v)=1$, hence the transitions
$(\rho_{\ell}\rho_{\ell+1},P_{k+\ell-1})(\rho_{\ell+1},P_{k+\ell})$ have the
colors
$\hat{\kappa}_{j}(\rho_{\ell}\rho_{\ell+1},P_{k+\ell-1})=\kappa_{j}(\rho_{\ell}\rho_{\ell+1})$.
Thus, we have
$\min\hat{\kappa}_{j}(\mathrm{InfTr}(\pi))=\min\kappa_{j}(\mathrm{Inf}(\rho))$,
which is odd: the play $\pi$ is lost by Prover, which is a contradiction since
$\tau_{\mathbb{P}}$ was assumed to be a winning strategy.

Moreover, player $i$ cannot win against the strategy profile
$\bar{\sigma}_{-i}$. Indeed, let $\sigma^{\prime}_{i}$ be a strategy for
player $i$, and let
$\rho=\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}}$. Let us
consider the play:

$\pi=(\rho_{0},P_{0})(\rho_{0}\rho^{\prime}_{0},P_{0})(\rho_{1},P_{1})\dots,$

compatible with $\tau_{\mathbb{P}}$. Since $\tau_{\mathbb{P}}$ is a winning
strategy, the play $\pi$ is won by Prover, hence the color
$\min\hat{\kappa}_{\star}(\mathrm{InfTr}(\pi))$ is even. By definition of
$\hat{\kappa}_{\star}$, we have
$\min\hat{\kappa}_{\star}(\mathrm{InfTr}(\pi))=\min\kappa_{i}(\mathrm{Inf}(\rho))+1$,
hence the color $\min\kappa_{i}(\mathrm{Inf}(\rho))$ is odd. The play $\rho$
is lost by player $i$.

Therefore, there exists a $\lambda$-rational strategy profile from $v_{0}$
against which player $i$ cannot win, hence $\mathrm{nego}(\lambda)(v_{0})=0$.

  * •

_If $\mathrm{nego}(\lambda)(v_{0})=0$._ Let $\bar{\sigma}_{-i}$ be a strategy
profile, $\lambda$-rational assuming the strategy $\sigma_{i}$, against which
player $i$ cannot win.

Let $\tau_{\mathbb{P}}$ be the strategy for Prover, in the concrete
negotiation game, defined by:

$\tau_{\mathbb{P}}\left((h_{0},P_{0})(h_{0}h^{\prime}_{0},P_{0})\dots(h_{k},P_{k})\right)=(h_{k}v,P_{k}),$

where $v=\bar{\sigma}(h_{0}\dots h_{k})$. Let us prove that
$\tau_{\mathbb{P}}$ is a winning strategy.

Let:

$\pi=(\rho_{0},P_{0})(\rho_{0}\rho^{\prime}_{0},P_{0})(\rho_{1},P_{1})\dots$

be a play compatible with $\pi$.

Let us assume that $\pi$ is lost by Prover, i.e. that
$\min\hat{\kappa}_{d}(\mathrm{InfTr}(\pi))$ is odd for some dimension $d$.

If $d=\star$, then
$\min\hat{\kappa}_{d}(\mathrm{InfTr}(\pi))=\min\kappa_{i}(\mathrm{Inf}(\rho))+1$,
and the color $\min\kappa_{i}(\mathrm{Inf}(\rho))$ is even. Thus, the play
$\rho$ is won by player $i$, which is impossible for a play compatible with
$\bar{\sigma}_{-i}$.

If $d\in\Pi$, then the play $\pi$ contains finitely many deviations
(otherwise, we would have $\min\hat{\kappa}_{d}(\mathrm{InfTr}(\pi))=0$,
even). Let $k$ be the least index such that the suffix
$(\rho_{k},P_{k})(\rho_{k}\rho^{\prime}_{k},P_{k})(\rho_{k+1},P_{k+1})\dots$
of $\pi$ contains no deviation — which means that we have
$\rho_{k}\rho_{k+1}\dots=\langle\bar{\sigma}_{\upharpoonright\rho_{0}\dots\rho_{k}}\rangle_{\rho_{k}}$.
Then, the sequence $(P_{\ell})_{\ell\geq k}$ is non-decreasing, and for $\ell$
great enough, the set $P_{\ell}$ contains $d$ (otherwise, we would have
$\min\hat{\kappa}_{d}(\mathrm{InfTr}(\pi))\leavevmode\nobreak\
=\leavevmode\nobreak\ m$, even). Therefore, there exists $\ell\geq k$ such
that $\rho_{\ell}\in V_{d}$ and $\lambda(\rho_{\ell})=1$.

Thus, the colors
$\hat{\kappa}_{d}((\rho_{\ell^{\prime}}\rho_{\ell^{\prime}+1},P_{\ell^{\prime}})(\rho_{\ell^{\prime}+1},P_{\ell^{\prime}+1}))$,
for $\ell^{\prime}\geq\ell$, are equal to
$\kappa_{d}(\rho_{\ell^{\prime}}\rho_{\ell^{\prime}+1})$, and the color
$\min\hat{\kappa}_{d}(\mathrm{InfTr}(\pi))$, which we assumed to be odd, is
equal to the color $\min\kappa_{d}(\mathrm{Inf}(\rho))$, hence the play
$\rho_{k}\rho_{k+1}\dots$ is lost by player $d$…and is therefore not
$\lambda$-consistent: contradiction. The strategy $\tau_{\mathbb{P}}$ is a
winning strategy.

∎

If we add one state in the middle of each transition, i.e. if we decompose
each transition $st\in\Delta$ into two transitions $s\delta_{st}$ and
$\delta_{st}t$, that game matches with the framework of [7]. That paper
provides an algorithm that solves such games in time:

$O\left((\mathrm{card}S)^{2\mathrm{card}\Omega\mathrm{card}C}\mathrm{card}\Delta\right)\frac{(\mathrm{card}\Omega\mathrm{card}C)!}{(\mathrm{card}C)!^{\mathrm{card}\Omega}},$

where $S$ is the set of states, $\Delta$ the set of transitions, $\Omega$ the
set of parity conditions and $C$ the set of colors that appear in them. In our
case, we can therefore solve the concrete negotiation game in time:

$\begin{matrix}&O\left((2^{p}(n+n^{2}))^{2(p+1)(m+1)}2^{p}n^{3}\right)\frac{((p+1)(m+1))!}{(m+1)!^{p+1}}\\\
=&n^{O(p^{2}m)}\frac{((p+1)(m+1))^{(p+1)(m+1)}e^{(m+1)(p+1)}}{e^{(p+1)(m+1)}(m+1)^{(m+1)(p+1)}}\\\
=&n^{O(p^{2}m)}.\end{matrix}$

This method requires, therefore, an exponential time, which does not improve
the complexity known since [15].

However, the same game can also be interpreted as a Boolean Büchi game in the
sense of [6], i.e. a two-player zero-sum game in which the objective of the
first player (Prover) is to validate a Boolean formula whose atoms are Büchi
conditions. Indeed, Prover’s objective can be written:

$\bigwedge_{d\in\Pi\cup\\{\star\\}}\bigvee_{k=0}^{\frac{m}{2}}\left(\mathbf{B}\\{\delta_{st}\leavevmode\nobreak\
|\leavevmode\nobreak\
\kappa_{d}(st)=2k\\}\wedge\neg\mathbf{B}\\{\delta_{st}\leavevmode\nobreak\
|\leavevmode\nobreak\ \kappa_{d}(st)<2k\\}\right),$

where $\mathbf{B}(W)$ is the Büchi objective associated to the set $W$, i.e.
the objective of visiting infinitely often at least one vertex of $W$. That
formula has at most $dm$ atoms, and has size $dm$, in a game of size
$O(n^{2}2^{p})$, hence by Proposition 5 from [6], there exists a deterministic
algorithm that decides which player has a winning strategy in time:

$O\left(2^{2^{(p+1)m}}(p+1)m+\left(2^{(p+1)m2^{(p+1)m}}O(n^{2}2^{p})\right)^{5}\right)=2^{2^{O(pm)}}n^{10}.$

Therefore, by constructing the concrete negotiation game and applying that
algorithm on each vertex, it is possible to compute the requirement
$\mathrm{nego}(\lambda)$ in time $2^{2^{O(pm)}}n^{11}$. Thus, it is possible
to compute the iterations of the negotiation function on $\lambda_{0}$: since
$\mathrm{nego}$ is non-decreasing, its fixed point $\lambda^{*}$ will be
reached in at most $n$ steps, and will therefore be found in time
$2^{2^{O(pm)}}n^{12}$.

Once $\lambda^{*}$ has been computed, given two thresholds $\bar{x}$ and
$\bar{y}$, the SPE constrained existence problem can be solved by searching,
for each tuple $\bar{c}\in\\{0,\dots,m-1\\}^{\Pi}$ where $c_{i}$ whenever
$x_{i}=1$ and odd whenever $y_{i}=0$, a play $\rho$ in $G$ that avoids the
set:

$W_{\bar{c}}=\\{v\in V_{i}\leavevmode\nobreak\ |\leavevmode\nobreak\ c_{i}\in
2\mathbb{Z}\mathrm{\leavevmode\nobreak\ and\leavevmode\nobreak\
}\lambda^{*}(v)=1\\},$

and such that for each $i$, we have
$\min\kappa_{i}(\mathrm{Inf}(\rho))=c_{i}$. For a given tuple $\bar{c}$, the
existence of a play can be decided by removing all the states of $W_{\bar{c}}$
and the states $v$ such that $\kappa_{i}(v)<c_{i}$ for some $i$, then looking
for a strongly connected component that contains at least one vertex $v$ with
$\kappa_{i}(v)=c_{i}$ for each $i$, and finally check whether the vertices of
that strongly connected component are accessible from the initial state in $G$
without visiting the states of $W_{\bar{c}}$. All those computations can be
done in time $O(n)$. Thus, once $\lambda^{*}$ has be computed, the SPE
constrained existence problem can be solved in time $O(m^{p}n)$.

Given a parity game $G_{\upharpoonright v_{0}}$ and two thresholds $\bar{x}$
and $\bar{y}$, solving the SPE constrained existence problem can be done in
time $2^{2^{O(pm)}}n^{12}$, and is therefore fixed parameter tractable with
parameters $m$ and $p$. ∎

##  Appendix F Proof of Lemma 9

Lemma 9. _The game $G_{\varphi}$ has the following properties._

  * •

_The least fixed point of the negotiation function is equal to $0$ on the
states controlled by Solver, and to $1$ on the other ones._

  * •

_For every SPE play $\rho$ in $G_{\varphi}$ that does not reach $\bot$, the
formula $\varphi$ is satisfied by:_

$\nu_{\rho}:x\mapsto\left\\{\begin{matrix}1&\mathrm{if\leavevmode\nobreak\
}\exists C,(C,x)\in\mathrm{Inf}(\rho)\\\
0&\mathrm{otherwise}.\end{matrix}\right.$

  * •

_Conversely, for every valuation $\nu$ satisfying $\varphi$, the play
$\rho_{\nu}=(C_{1}(C_{1},L_{1})\dots C_{m}(C_{m},L_{m}))^{\omega},$ where for
each $j$, the literal $L_{j}$ is satisfied by $\nu$, is an SPE play._

###### Proof.

  * •

If $\lambda_{0}$ is the requirement constantly equal to $0$, then
$\lambda_{1}=\mathrm{nego}(\lambda_{0})$ is equal to $0$ in every state
controlled by Solver (she loses in $\bot$, and if all the other players choose
to always go to $\bot$, she loses from everywhere), and to $1$ in every other
state (from any state controlled by him, the player $L$ can go to $\bot$, and
win). This requirement is a fixed point of the negotiation function (the
strategy profile against Solver that chooses to always go to $\bot$ is
$\lambda_{1}$-rational), and is therefore the least one.

Therefore, the SPE plays are the plays consistent with that requirement, which
we will now write $\lambda^{*}$.

  * •

_If $\rho$ is an SPE play that does not reach the state $\bot$._

Then, let us prove that the valuation $\nu_{\rho}$ satisfies $\varphi$. Since
$\rho$ does not end in the sink state $\bot$, for each clause $C$ of
$\varphi$, the state $C$ is visited infinitely often in $\rho$, and therefore
so is at least one of its successors, which we will write $(C,L)$.

If $L$ is a positive literal, say $L=x$, then by definition of $\nu_{\rho}$ we
have $\nu_{\rho}(x)=1$ and the clause $C$ is satisfied.

If $L$ is a negative literal, say $L=\neg x$, then since $\lambda^{*}(C,L)=1$,
he must win as a player in $\rho$. Therefore, all the states of the form
$(C^{\prime},x)$ are visited finitely often, hence $\nu_{\rho}(x)=0$, and the
clause $C$ is also satisfied in that case.

The formula $\varphi$ is satisfied by the valuation $\nu_{\rho}$.

  * •

_If the valuation $\nu$ satisfies $\varphi$._

Then, the play $\rho_{\nu}$ is $\lambda^{*}$-consistent: the only states it
traverses on which $\lambda^{*}$ is equal to $1$ are the ones of the form
$(C_{j},L_{j})$, where $L_{j}$ is a literal of $C_{j}$ satisfied by $\nu$. But
then, that state is controlled by player $L_{j}$, who wins the play
$\rho_{\nu}$: since the literal $L_{j}$ is satisfied by $\nu$, the literal
$\overline{L}_{j}$ is not, hence no state of the form $(C,\overline{L}_{j})$
is ever traversed.

Therefore, the play $\rho_{\nu}$ is an SPE play.

∎

##  Appendix G Proof of Theorem 7

Theorem 7 _Given a parity game $G$ and a requirement $\lambda$, deciding
whether $\lambda=\lambda^{*}$ is $\mathbf{BH}_{2}$-complete. Given a parity
game $G$, computing $\lambda^{*}$ can be done by a non-deterministic algorithm
in polynomial time if and only if $\mathbf{NP}=\mathbf{BH}_{2}$._

###### Proof.

The $\mathbf{BH}_{2}$-easiness of the second problem is given by Lemma 7; it
of course implies the $\mathbf{BH}_{2}$-easiness of the first one.

Now, hardness needs to be shown only for the first problem, and it will imply
the $\mathbf{BH}_{2}$-hardness of the second one. We proceed by reduction from
the problem $\textsc{Sat}\times\textsc{coSat}$, which is
$\mathbf{BH}_{2}$-complete by Lemma 1.

Let $(\varphi_{1},\varphi_{2})$ be a pair of formulas. We construct in
polynomial time a parity game $G$ and a requirement $\lambda$ such that
$\lambda$ is the least fixed point of the negotiation function on $G$ if and
only if $\varphi_{1}$ is satisfiable and $\varphi_{2}$ is not.

First, we construct the games $G_{\varphi_{1}}$ and $G_{\varphi_{2}}$,
supposed to have disjoint state spaces. We add to each of them a new state,
written $v_{1}$ in $G_{\varphi_{1}}$ and $v_{2}$ in $G_{\varphi_{2}}$, and
inserted just before the first clause, as shown in Figure 6(a) for $v_{1}$.
Note that each of those two vertices has exactly one outgoing edge, so that
Challenger has absolutely no choice to make in any play: his defeat of victory
will be determined exclusively by the actions of the other players.

$C_{m},L_{1}$$C_{m},L_{k}$$v_{1}$$C_{1}$$\dots$$\dots$$\dots$ (a) The vertex
$v_{1}$ inserted in $G_{\varphi_{1}}$

$G_{\varphi_{1}}$$G_{\varphi_{2}}$$\bullet$$v_{1}$$0$$\bullet$$v_{2}$$1$ (b)
The game $G$

Figure 6: Construction of the game $G$

Those two vertices are controlled by an additional player, _Opponent_ ,
denoted by $\mathbb{O}$, and whose objective is to reach the state $\bot$ —
every state $v$ has the color $\kappa_{\mathbb{O}}(v)=1$, except $\bot$, which
has the color $\kappa_{\mathbb{O}}(v)=2$. Note that Opponent’s objective is
the exact complement of Solver’s one. The states $v_{1}$ and $v_{2}$ are
colored to $2$ for every other player than Opponent, so that their objectives
stay intuitively the same as in $G_{\varphi_{1}}$ and $G_{\varphi_{2}}$.

The game $G$ is made of those two modified versions of $G_{\varphi_{1}}$ and
$G_{\varphi_{2}}$, juxtaposed and not linked in any way, as shows Figure 6(b).
The requirement $\lambda$ is equal to $1$ on each state controlled by a
literal player, to $0$ on each state controlled by Solver, to $0$ on $v_{1}$
and to $1$ on $v_{2}$.

We already know that Solver can never enforce a payoff better than $0$ from
her states, and that all the literal players can always enforce the payoff $1$
— adding $v_{1}$ and $v_{2}$ did not change those facts. As a consequence, we
always have $\lambda^{*}(v)=\lambda(v)$ for every $v\neq v_{1},v_{2}$.

Now, by Lemma 9, there exists an SPE play from $v_{1}$ (resp. $v_{2}$) that is
lost by Opponent if and only the formula $\varphi_{1}$ (resp. $\varphi_{2}$)
is satisfiable: therefore, we have $\lambda=\lambda^{*}$ if and only if the
pair $(\varphi_{1},\varphi_{2})$ is a positive instance of the problem
$\textsc{Sat}\times\textsc{coSat}$. Deciding whether a given $\lambda$ is the
least fixed point of the negotiation function in a given parity game is
$\mathbf{BH}_{2}$-hard, and therefore so is computing that least fixed point.
∎

##  Appendix H Proof of Theorem 8

Theorem 8. _The SPE-verification problem is $\mathbf{PSpace}$-complete._

###### Proof.

Easiness is given by Lemma 8.

For hardness, we proceed by reduction from the $\mathbf{PSpace}$-complete
problem of model-checking in Kripke structures.

Let $\mathcal{M}=(\mathbb{A},S,R,(\nu_{s})_{s\in S})$ be a Kripke structure,
where $\mathbb{A}$ is a finite set of atoms, $S$ is a finite set of states,
$R\subseteq S\times S$ is a binary relation over $S$, and each $\nu_{s}$ is a
valuation over $\mathbb{A}$. Let $\varphi$ be an LTL formula over
$\mathbb{A}$.

We associate to $\mathcal{M}$ the game $G=(\Pi,V,(V_{i})_{i\in\Pi},E,\mu)$
where $\Pi=\\{\mathbb{S}\\}$, $V=V_{\mathbb{S}}=S$, $E=R$, and $\mu$ is
constantly equal to $1$ — the game $G$ is a parity game with all colors equal
to $2$. Then, every play in $G$ is an SPE play. To $\varphi$, we associate the
LTL formula $\psi$ over the atom set $V$, by replacing each atom $a$ in
$\varphi$ by the proposition:

$\bigvee_{\nu_{v}(a)=1}v.$

Then, there exists a path in $\mathcal{M}$ satisfying $\varphi$ if and only if
there exists an SPE play in $G$ satisfying $\psi$, which yields the desired
lower bound. ∎

##  Appendix I An example

Let $G$ be the parity game of Figure 7. Let us compute the iterations of the
negotiation function, i.e. the sequence
$(\lambda_{n})_{n}=(\mathrm{nego}^{n}(\lambda_{0}))_{n}$, on that game.

At first, the requirement $\lambda_{1}$ is equal to $1$ on each state that is
controlled by a player who has a winning strategy from that state: namely, the
states $b$, $f$, $j$, and $k$. It is equal to $0$ everywhere else.

At the second step, the requirement $\lambda_{2}$ is also equal to $1$ on the
state $i$, because from there, player $\Circle$ can go to the state $j$, from
which only a play winning for player $\Box$ can be proposed to her — that is,
only the play $jk^{\omega}$, which is winning for her too. For the same
reason, the requirement $\lambda_{2}$ is also equal to $1$ on the state $g$,
because the only $\lambda_{1}$-consistent losing play that could be proposed
to player $\Circle$ from there is $gehi^{\omega}$, which also enables her to
deviate and go to the state $j$. The requirement $\lambda_{2}$ is still equal
to $0$ on $a$, because the play $ab(cd)^{\omega}$, winning for player
$\Circle$, can be proposed to player $\Box$, without letting him the
possibility of deviating. It is also still equal to $0$ on $c$, $d$ and $h$,
because from $e$, the play $(efgeh)^{\omega}$, winning for player $\Circle$,
can be proposed to player $\Diamond$ — and the play $i^{\omega}$ if she
deviates and goes to $i$.

At the third step, though, if she deviates and goes to $i$, since
$\lambda_{2}(i)=1$, then the only $\lambda_{2}$-consistent play that can be
proposed to her is $ijk^{\omega}$, winning for her. As a consequence, the
requirement $\lambda_{3}$ is equal to $1$ on the states $c,d$, and $h$.

Then, from the state $a$, the play $ab(cd)^{\omega}$ is no longer
$\lambda_{3}$-consistent, but the play $abcd(ef)^{\omega}$ still is, as well
as the play $(ef)^{\omega}$ from $e$, hence $\lambda_{3}=\lambda^{*}$.

We sum up those results in the following table.

| $a$ | $b$ | $c$ | $d$ | $e$ | $f$ | $g$ | $h$ | $i$ | $j$ | $k$
---|---|---|---|---|---|---|---|---|---|---|---
$\lambda_{1}$ | $0$ | $1$ | $0$ | $0$ | $0$ | $1$ | $0$ | $0$ | $0$ | $1$ | $1$
$\lambda_{2}$ | $0$ | $1$ | $0$ | $0$ | $0$ | $1$ | $1$ | $0$ | $1$ | $1$ | $1$
$\lambda_{3}=\lambda^{*}$ | $0$ | $1$ | $1$ | $1$ | $0$ | $1$ | $1$ | $1$ | $1$ | $1$ | $1$

$a$$b$$c$$d$$e$$f$$g$$h$$i$$j$$k$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{3}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{0}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{2}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{2}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{2}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{3}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{1}}$$\stackrel{{\scriptstyle{\tiny{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{0}}\stackrel{{\scriptstyle\Diamond}}{{0}}$
Figure 7: A parity game