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.

# Subgame-perfect Equilibria in Mean-payoff Games

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

###### Abstract

In this paper, we provide an effective characterization of all the subgame-
perfect equilibria in infinite duration games played on finite graphs with
mean-payoff objectives. To this end, we introduce the notion of requirement,
and the notion of negotiation function. We establish that the plays that are
supported by SPEs are exactly those that are consistent with the least fixed
point of the negotiation function. Finally, we show that the negotiation
function is piecewise linear, and can be analyzed using the linear algebraic
tool box. As a corollary, we prove the decidability of the SPE constrained
existence problem, whose status was left open in the literature.

###### keywords:

Games on graphs, subgame-perfect equilibria, mean-payoff objectives.

##  1 Introduction

The notion of Nash equilibrium (NE) is one of the most important and most
studied solution concepts in game theory. A profile of strategies is an NE
when no rational player has an incentive to change their strategy
unilaterally, i.e. while the other players keep their strategies. Thus an NE
models a stable situation. Unfortunately, it is well known that, in sequential
games, NEs suffer from the problem of non-credible threats, see e.g. [18]. In
those games, some NE only exists when some players do not play rationally in
subgames and so use non-credible threats to force the NE. This is why, in
sequential games, the stronger notion of subgame-perfect equilibrium is used
instead: a profile of strategies is a subgame-perfect equilibrium (SPE) if it
is an NE in all the subgames of the sequential game. Thus SPE imposes
rationality even after a deviation has occured.

In this paper, we study sequential games that are infinite-duration games
played on graphs with mean-payoff objectives, and focus on SPEs. While NEs are
guaranteed to exist in infinite duration games played on graphs with mean-
payoff objectives, it is known that it is not the case for SPEs, see e.g. [19,
4]. We provide in this paper a constructive characterization of the entire set
of SPEs, which allows us to decide, among others, the SPE (constrained)
existence problem. This problem was left open in previous contributions on the
subject. More precisely, our contributions are described in the next
paragraphs.

Contributions.  First, we introduce two important new notions that allow us to
capture NEs, and more importantly SPEs, in infinite duration games played on
graphs with mean-payoff objectives111A large part of our results apply to the
larger class of games with prefix-independent objectives. For the sake of
readability of this introduction, we focus here on mean-payoff games but the
technical results in the paper are usually covering broader classes of games.:
the notion of requirement and the notion of negotiation function.

A requirement $\lambda$ is a function that assigns to each vertex $v\in V$ of
a game graph a value in $\mathbb{R}\cup\\{-\infty,+\infty\\}$. The value
$\lambda(v)$ represents a requirement on any play
$\rho=\rho_{0}\rho_{1}\dots\rho_{n}\dots$ that traverses this vertex: if we
want the player who controls the vertex $v$ to follow $\rho$ and to give up
deviating from $\rho$, then the play must offer a payoff to this player that
is at least $\lambda(v)$. An infinite play $\rho$ is $\lambda$-consistent if,
for each player $i$, the payoff of $\rho$ for player $i$ is larger than or
equal to the largest value of $\lambda$ on vertices occurring along $\rho$ and
controlled by player $i$.

We first use those notions to rephrase a classical result about NEs: if
$\lambda$ maps a vertex $v$ to the largest value that the player that controls
$v$ can secure against a fully adversarial coalition of the other players,
i.e. if $\lambda(v)$ is the zero-sum worst-case value, then the set of plays
that are $\lambda$-consistent is exactly the set of plays that are supported
by an NE (Theorem 1).

As SPEs are forcing players to play rationally in all subgames, we cannot rely
on the zero-sum worst-case value to characterize them. Indeed, when
considering the worst-case value, we allow adversaries to play fully
adversarially after a deviation and so potentially in an irrational way w.r.t.
their own objective. In fact, in an SPE, a player is refrained to deviate when
opposed by a coalition of rational adversaries. To characterize this
relaxation of the notion of worst-case value, we rely on our notion of
_negotiation function_.

The negotiation function $\mathrm{nego}$ operates from the set of requirements
into itself. To understand the purpose of the negotiation function, let us
consider its application on the requirement $\lambda$ that maps every vertex
$v$ on the worst-case value as above. Now, we can naturally formulate the
following question: given $v$ and $\lambda$, can the player who controls $v$
improve the value that they can ensure against all the other players, if only
plays that are consistent with $\lambda$ are proposed by the other players? In
other words, can this player enforce a better value when playing against the
other players if those players are not willing to give away their own worst-
case value? Clearly, securing this worst-case value can be seen as a minimal
goal for any rational adversary. So $\mathrm{nego}(\lambda)(v)$ returns this
value; and this reasoning can be iterated. One of the contributions of this
paper is to show that the least fixed point $\lambda^{*}$ of the negotiation
function is exactly characterizing the set of plays supported by SPEs (Theorem
2).

To turn this fixed point characterization of SPEs into algorithms, we
additionally draw links between the negotiation function and two classes of
zero-sum games, that are called abstract and concrete negotiation games (see
Theorem 3). We show that the latter can be solved effectively and allow, given
$\lambda$, to compute $\mathrm{nego}(\lambda)$ (Lemma 3). While solving
concrete negotiation games allows us to compute $\mathrm{nego}(\lambda)$ for
any requirement $\lambda$, and even if the function $\mathrm{nego}(\cdot)$ is
monotone and Scott-continuous, a direct application of the Kleene-Tarski fixed
point theorem is not sufficient to obtain an effective algorithm to compute
$\lambda^{*}$. Indeed, we give examples that require a transfinite number of
iterations to converge to the least fixed point. To provide an algorithm to
compute $\lambda^{*}$, we show that the function $\mathrm{nego}(\cdot)$ is
piecewise linear and we provide an effective representation of this function
(Theorem 4). This effective representation can then be used to extract all its
fixed points and in particular its least fixed point using linear algebraic
techniques, hence the decidability of the SPE (constrained) existence problem
(Theorem 6). Finally, all our results are also shown to extend to
$\varepsilon$-SPEs, those are quantitative relaxations of SPEs.

Related works.  Non-zero sum infinite duration games have attracted a large
attention in recent years, with applications targeting reactive synthesis
problems. We refer the interested reader to the following survey papers [2, 6]
and their references for the relevant literature. We detail below
contributions more closely related to the work presented here.

In [5], Brihaye et al. offer a characterization of NEs in quantitative games
for cost-prefix-linear reward functions based on the worst-case value. The
mean-payoff is cost-prefix-linear. In their paper, the authors do not consider
the stronger notion of SPE, which is the central solution concept studied in
our paper. In [7], Bruyère et al. study secure equilibria that are a
refinement of NEs. Secure equilibria are not subgame-perfect and are, as
classical NEs, subject to non-credible threats in sequential games.

In [20], Ummels proves that there always exists an SPE in games with
$\omega$-regular objectives and defines algorithms based on tree automata to
decide constrained SPE problems. Strategy logics, see e.g. [11], can be used
to encode the concept of SPE in the case of $\omega$-regular objectives with
application to the rational synthesis problem [15] for instance. In [12],
Flesch et al. show that the existence of $\varepsilon$-SPEs is guaranteed when
the reward function is lower-semicontinuous. The mean-payoff reward function
is neither $\omega$-regular, nor lower-semicontinuous, and so the techniques
defined in the papers cited above cannot be used in our setting. Furthermore,
as already recalled above, see e.g. [23, 4], contrary to the $\omega$-regular
case, SPEs in games with mean-payoff objectives may fail to exist.

In [4], Brihaye et al. introduce and study the notion of weak subgame-perfect
equilibria, which is a weakening of the classical notion of SPE. This
weakening is equivalent to the original SPE concept on reward functions that
are continuous. This is the case for example for the quantitative reachability
reward function, on which Brihaye et al. solve the problem of the constrained
existence of SPEs in [3]. On the contrary, the mean-payoff cost function is
not continuous and the techniques used in [4], and generalized in [9], cannot
be used to characterize SPEs for the mean-payoff reward function.

In [17], Meunier develops a method based on Prover-Challenger games to solve
the problem of the existence of SPEs on games with a finite number of possible
outcomes. This method is not applicable to the mean-payoff reward function, as
the number of outcomes in this case is uncountably infinite.

In [13], Flesch and Predtetchinski present another characterization of SPEs on
games with finitely many possible outcomes, based on a game structure that we
will present here under the name of _abstract negotiation game_. Our
contributions differ from this paper in two fundamental aspects. First, it
lifts the restriction to finitely many possible outcomes. This is crucial as
mean-payoff games violate this restriction. Instead, we identify a class of
games, that we call with steady negotiation, that encompasses mean-payoff
games and for which some of the conceptual tools introduced in that paper can
be generalized. Second, the procedure developed by Flesch and Predtetchinski
is not an algorithm in CS acceptation: it needs to solve infinitely many games
that are not represented effectively, and furthermore it needs a transfinite
number of iterations. On the contrary, our procedure is effective and leads to
a complete algorithm in the classical sense: with guarantee of termination in
finite time and applied on effective representations of games.

Structure of the paper.  In Sect. 2, we introduce the necessary background.
Sect. 3 defines the notion of requirement and the negotiation function. Sect.
4 shows that the set of plays that are supported by an SPE are those that are
$\lambda^{*}$-consistent, where $\lambda^{*}$ is the least fixed point of the
negotiation function. Sect. 5 draws a link between the negotiation function
and negotiation games. Sect. 6 establishes that the negotiation function is
effectively piecewise linear. Finally, Sect. 7 applies those results to prove
the decidability of the SPE constrained existence problem on mean-payoff
games, and adds some complexity considerations. All the detailed proofs of our
results can be found in a well-identified appendix and a large number of
examples are provided in the main part of the paper to illustrate the main
ideas behind our new concepts and constructions.

##  2 Background

In all what follows, we will use the word _game_ for the infinite duration
turn-based quantitative games on finite graphs with complete information.

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

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

  * •

$\Pi$ is a finite set of _players_ ;

  * •

$(V,E)$ is a finite directed graph, whose vertices are sometimes called
_states_ and whose edges are sometimes called _transitions_ , and in which
every state has at least one outgoing transition. For the simplicity of
writing, a transition $(v,w)\in E$ will often be written $vw$.

  * •

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

  * •

$\mu:V^{\omega}\to\mathbb{R}^{\Pi}$ is an _outcome function_ , that maps each
infinite word $\rho$ to the tuple $\mu(\rho)=(\mu_{i}(\rho))_{i\in\Pi}$ of the
players’ _payoffs_.

######  Definition 2 (Initialized game).

An _initialized game_ is a tuple $(G,v_{0})$, often written
$G_{\upharpoonright v_{0}}$, where $G$ is a game and $v_{0}\in V$ is a state
called _initial state_. Moreover, the game $G_{\upharpoonright v_{0}}$ is
_well-initialized_ if any state of $G$ is accessible from $v_{0}$ in the graph
$(V,E)$.

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

A _play_ (resp. history) in the game $G$ is an infinite (resp. finite) path in
the graph $(V,E)$. It is also a play (resp. history) in the initialized game
$G_{\upharpoonright v_{0}}$, where $v_{0}$ is its first vertex. The set of
plays (resp. histories) in the game $G$ (resp. the initialized game
$G_{\upharpoonright v_{0}}$) is denoted by $\mathrm{Plays}G$ (resp.
$\mathrm{Plays}G_{\upharpoonright
v_{0}},\mathrm{Hist}G,\mathrm{Hist}G_{\upharpoonright v_{0}}$). We write
$\mathrm{Hist}_{i}G$ (resp. $\mathrm{Hist}_{i}G_{\upharpoonright v_{0}}$) for
the set of histories in $G$ (resp. $G_{\upharpoonright v_{0}}$) of the form
$hv$, where $v$ is a vertex controlled by player $i$.

######  Remark.

In the literature, the word _outcome_ can be used to name plays, and the word
_payoff_ to name what we call here outcome. Here, the word _payoff_ will be
used to refer to outcomes, seen from the point of view of a given player – or
in other words, an _outcome_ will be seen as the collection of all players’
payoffs.

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

A _strategy_ for player $i$ in the initialized game $G_{\upharpoonright
v_{0}}$ is a function $\sigma_{i}:\mathrm{Hist}_{i}G_{\upharpoonright
v_{0}}\to V$, such that $v\sigma_{i}(hv)$ is an edge of $(V,E)$ for every
$hv$. A history $h$ is _compatible_ with a strategy $\sigma_{i}$ if and only
if $h_{k+1}=\sigma_{i}(h_{0}\dots h_{k})$ for all $k$ such that $h_{k}\in
V_{i}$. A play $\rho$ is compatible with $\sigma_{i}$ if all its prefixes are.

A _strategy profile_ for $P\subseteq\Pi$ is a tuple
$\bar{\sigma}_{P}=(\sigma_{i})_{i\in P}$, where for each $i$, $\sigma_{i}$ is
a strategy for player $i$ in $G_{\upharpoonright v_{0}}$. A _complete_
strategy profile, usually written $\bar{\sigma}$, is a strategy profile for
$\Pi$. A play or a history is _compatible_ with $\bar{\sigma}_{P}$ if it is
compatible with every $\sigma_{i}$ for $i\in P$.

When $i$ is a player and when the context is clear, we will often write $-i$
for the set $\Pi\setminus\\{i\\}$. We will often refer to
$\Pi\setminus\\{i\\}$ as the _environment_ against player $i$. When
$\bar{\tau}_{P}$ and $\bar{\tau}^{\prime}_{Q}$ are two strategy profiles with
$P\cap Q=\emptyset$, $(\bar{\tau}_{P},\bar{\tau}^{\prime}_{Q})$ denotes the
strategy profile $\bar{\sigma}_{P\cup Q}$ such that $\sigma_{i}=\tau_{i}$ for
$i\in P$, and $\sigma_{i}=\tau^{\prime}_{i}$ for $i\in Q$.

Before moving on to SPEs, let us recall the notion of Nash equilibrium.

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

Let $G_{\upharpoonright v_{0}}$ be an initialized game. The strategy profile
$\bar{\sigma}$ is a _Nash equilibrium_ — or _NE_ for short — in
$G_{\upharpoonright v_{0}}$ if and only if for each player $i$ and for every
strategy $\sigma^{\prime}_{i}$, called _deviation of $\sigma_{i}$_, we have
the inequality
$\mu_{i}\left(\langle\sigma^{\prime}_{i},\bar{\sigma}_{-i}\rangle_{v_{0}}\right)\leq\mu_{i}\left(\langle\bar{\sigma}\rangle_{v_{0}}\right)$.

To define SPEs, we need the notion of subgame.

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

Let $hv$ be a history in the game $G$. The _subgame_ of $G$ after $hv$ is the
initialized game $\left(\Pi,V,(V_{i})_{i},E,\mu_{\upharpoonright
hv}\right)_{\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}$.

######  Remark.

The initialized game $G_{\upharpoonright v_{0}}$ is also the subgame of $G$
after the one-state history $v_{0}$.

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

Let $G_{\upharpoonright v_{0}}$ be an initialized game. The strategy profile
$\bar{\sigma}$ is a _subgame-perfect equilibrium_ — or _SPE_ for short — in
$G_{\upharpoonright v_{0}}$ if and only if for every history $h$ in
$G_{\upharpoonright v_{0}}$, the strategy profile
$\bar{\sigma}_{\upharpoonright h}$ is a Nash equilibrium in the subgame
$G_{\upharpoonright h}$.

The notion of subgame-perfect equilibrium can be seen as a refinement of Nash
equilibrium: it is a stronger equilibrium which excludes players resorting to
non-credible threats.

######  Example 1.

In the game represented in Figure 1(a), where the square state is controlled
by player $\Box$ and the round states by player $\Circle$, if both players get
the payoff $1$ by reaching the state $d$ and the payoff $0$ in the other
cases, there are actually two NEs: one, in blue, where $\Box$ goes to the
state $b$ and then player $\Circle$ goes to $d$, and both win, and one, in
red, where player $\Box$ goes to the state $c$ because player $\Circle$ was
planning to go to $e$. However, only the blue one is an SPE, as moving from
$b$ to $e$ is irrational for player $\Circle$ in the subgame
$G_{\upharpoonright ab}$.

An $\varepsilon$-SPE is a strategy profile which is _almost_ an SPE: if a
player deviates after some history, they will not be able to improve their
payoff by more than a quantity $\varepsilon\geq 0$.

######  Definition 8 ($\varepsilon$-SPE).

Let $G_{\upharpoonright v_{0}}$ be an initialized game, and $\varepsilon\geq
0$. A strategy profile $\bar{\sigma}$ from $v_{0}$ is an $\varepsilon$-SPE if
and only if for every history $hv$, for every player $i$ and every strategy
$\sigma^{\prime}_{i}$, we have $\mu_{i}(\langle\bar{\sigma}_{-i\upharpoonright
hv},\sigma^{\prime}_{i\upharpoonright
hv}\rangle_{v})\leq\mu_{i}(\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v})+\varepsilon$.

Note that a $0$-SPE is an SPE, and conversely.

Hereafter, we focus on _prefix-independent_ games, and in particular _mean-
payoff_ games.

######  Definition 9 (Mean-payoff game).

A _mean-payoff game_ is a game $G=\left(\Pi,V,(V_{i})_{i},E,\mu\right)$, where
$\mu$ is defined from a function $\pi:E\to\mathbb{Q}^{\Pi}$, called _weight
function_ , by, for each player $i$:

$\mu_{i}:\rho\mapsto\underset{n\to\infty}{\liminf}\frac{1}{n}\underset{k=0}{\overset{n-1}{\sum}}\pi_{i}\left(\rho_{k}\rho_{k+1}\right).$

In a mean-payoff game, the weight given by the function $\pi$ represents the
immediate reward that each action gives to each player. The final payoff of
each player is their average payoff along the play, classically defined as the
limit inferior over $n$ (since the limit may not be defined) of the average
payoff after $n$ steps.

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

A game $G$ is _prefix-independent_ if, for every history $h$ and for every
play $\rho$, we have $\mu(h\rho)=\mu(\rho)$. We also say, in that case, that
the outcome function $\mu$ is prefix-independent.

$a$$b$$c$$d$$e$$f$$g$ (a) Two NEs and one SPE

$a$$c$$b$$d$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{3}}$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{2}}$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{1}}$$(\lambda_{0})$$-\infty$$-\infty$$-\infty$$-\infty$$(\lambda_{1})$$1$$2$$1$$2$$(\lambda_{2})$$2$$2$$1$$2$$(\lambda_{3})$$2$$3$$1$$2$$(\lambda_{4})$$+\infty$$+\infty$$1$$2$
(b) A game without SPE

Figure 1: Two examples of games

Mean-payoff games are prefix-independent. We now recall a classical result
about two-player zero-sum games.

######  Definition 11 (Zero-sum game).

A game $G$, with $\Pi=\\{1,2\\}$, is _zero-sum_ if $\mu_{2}=-\mu_{1}$.

######  Definition 12 (Borel game).

A game $G$ is _Borel_ if the function $\mu$, from the set $V^{\omega}$
equipped with the product topology to the Euclidian space $\mathbb{R}^{\Pi}$,
is Borel, i.e. if, for every Borel set $B\subseteq\mathbb{R}^{\Pi}$, the set
$\mu^{-1}(B)$ is Borel.

######  Definition 13 (Determinacy).

Let $G_{\upharpoonright v_{0}}$ be an initialized zero-sum Borel game, with
$\Pi=\\{1,2\\}$. The game $G_{\upharpoonright v_{0}}$ is _determined_ if we
have the following equality:

$\sup_{\sigma_{1}}\leavevmode\nobreak\ \inf_{\sigma_{2}}\leavevmode\nobreak\
\mu_{1}(\langle\bar{\sigma}\rangle_{v_{0}})=\inf_{\sigma_{2}}\leavevmode\nobreak\
\sup_{\sigma_{1}}\leavevmode\nobreak\
\mu_{1}(\langle\bar{\sigma}\rangle_{v_{0}}).$

That quantity is called _value_ of $G_{\upharpoonright v_{0}}$, denoted by
$\mathrm{val}_{1}(G_{\upharpoonright v_{0}})$; _solving_ the game $G$ means
computing its value.

######  Proposition 1 (Determinacy of two-player zero-sum Borel games [16]).

Zero-sum Borel games are determined.

The following examples illustrate the SPE existence problem in mean-payoff
games.

######  Example 2.

Let $G$ be the mean-payoff game of Figure 1(b), where each edge is labelled by
its weights $\pi_{\scriptsize{\Circle}}$ and $\pi_{\Box}$. No weight is given
for the edges $ac$ and $bd$ since they can be used only once, and therefore do
not influence the final payoff. For now, the reader should not pay attention
to the red labels below the states. As shown in [8], this game does not have
any SPE, neither from the state $a$ nor from the state $b$.

Indeed, the only NE plays from the state $b$ are the plays where player $\Box$
eventually leaves the cycle $ab$ and goes to $d$: if he stays in the cycle
$ab$, then player $\Circle$ would be better off leaving it, and if she does,
player $\Box$ would be better off leaving it before. From the state $a$, if
player $\Circle$ knows that player $\Box$ will leave, she has no incentive to
do it before: there is no NE where $\Circle$ leaves the cycle and $\Box$ plans
to do it if ever she does not. Therefore, there is no SPE where $\Circle$
leaves the cycle. But then, after a history that terminates in $b$, player
$\Box$ has actually no incentive to leave if player $\Circle$ never plans to
do it afterwards: contradiction.

$a$$b$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{2}}$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{1}}$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{0}}$
(a) The game $G$

${\Circle}$${\Box}$12012 (b) The outcomes of plays and SPE plays in $G$

Figure 2: A game with an infinity of SPEs

######  Example 3.

Let us now study the game of Figure 2(a). Using techniques from [10], we can
represent the outcomes of possible plays in that game as in Figure 2(b) (gray
and blue areas).

Following exclusively one of the three simple cycles $a$, $ab$ and $b$ of the
game graph during a play yields the outcomes $01,10$ and $22$, respectively.
By combining those cycles with well chosen frequencies, one can obtain any
outcome in the convex hull of those three points. Now, it is also possible to
obtain the point $00$ by using the properties of the limit inferior: it is for
instance the outcome of the play $a^{2}b^{4}a^{16}b^{256}\dots
a^{2^{2^{n}}}b^{2^{2^{n+1}}}\dots$. In fact, one can construct a play that
yields any outcome in the convex hull of the four points $00,10,01$, and $22$.

We claim that the outcomes of SPEs plays correspond to the entire blue area in
Figure 2(b): there exists an SPE $\bar{\sigma}$ in $G_{\upharpoonright a}$
with $\langle\bar{\sigma}\rangle_{a}=\rho$ if and only if
$\mu_{\Box}(\rho),\mu_{\scriptsize{\Circle}}(\rho)\geq 1$. That statement will
be a direct consequence of the results we show in the remaining sections, but
let us give a first intuition: a play with such an outcome necessarily uses
infinitely often both states. It is an NE play because none of the players can
get a better payoff by looping forever on their state, and they can both force
each other to follow that play, by threatening them to loop for ever on their
state whenever they can. But such a strategy profile is clearly not an SPE.

It can be transformed into an SPE as follows: when a player deviates, say
player $\Box$, then player $\Circle$ can punish him by looping on $a$, not
forever, but a great number of times, until player $\Box$’s mean-payoff gets
very close to $1$. Afterwards, both players follow again the play that was
initially planned. Since that threat is temporary, it does not affect player
$\Circle$’s payoff on the long term, but it really punishes player $\Box$ if
that one tries to deviate infinitely often.

##  3 Requirements and negotiation

We will now see that SPEs are strategy profiles that respect some
_requirements_ about the payoffs, depending on the states it traverses. In
this part, we develop the notions of _requirement_ and _negotiation_.

###  3.1 Requirement

In the method we will develop further, we will need to analyze the players’
behaviour when they have some _requirement_ to satisfy. Intuitively, one can
see requirements as _rationality constraints_ for the players, that is, a
threshold payoff value under which a player will not accept to follow a play.
In all what follows, $\overline{\mathbb{R}}$ denotes the set
$\mathbb{R}\cup\\{\pm\infty\\}$.

######  Definition 14 (Requirement).

A _requirement_ on the game $G$ is a function
$\lambda:V\to\overline{\mathbb{R}}$.

For a given state $v$, the quantity $\lambda(v)$ represents the minimal payoff
that the player controlling $v$ will require in a play beginning in $v$.

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

Let $\lambda$ be a requirement on a game $G$. A play $\rho$ in $G$ is
_$\lambda$ -consistent_ if and only if, for all $i\in\Pi$ and $n\in\mathbb{N}$
with $\rho_{n}\in V_{i}$, we have
$\mu_{i}(\rho_{n}\rho_{n+1}\dots)\leavevmode\nobreak\ \geq\leavevmode\nobreak\
\lambda(\rho_{n})$. The set of the $\lambda$-consistent plays from a state $v$
is denoted by $\lambda\mathrm{Cons}(v)$.

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

Let $\lambda$ be a requirement on a mean-payoff game $G$. Let $i\in\Pi$. A
strategy profile $\bar{\sigma}_{-i}$ is _$\lambda$ -rational_ if and only if
there exists a strategy $\sigma_{i}$ such that, for every history $hv$
compatible with $\bar{\sigma}_{-i}$, the play
$\langle\bar{\sigma}_{\upharpoonright hv}\rangle_{v}$ is $\lambda$-consistent.
We then say that the strategy profile $\bar{\sigma}_{-i}$ is
$\lambda$-rational _assuming_ $\sigma_{i}$. The set of $\lambda$-rational
strategy profiles in $G_{\upharpoonright v}$ is denoted by
$\lambda\mathrm{Rat}(v)$.

Note that $\lambda$-rationality is a property of a strategy profile for all
the players but one, player $i$. Intuitively, their rationality is justified
by the fact that they collectively assume that player $i$ will, eventually,
play according to the strategy $\sigma_{i}$: if player $i$ does so, then
everyone gets their payoff satisfied. Finally, let us define a particular
requirement: the _vacuous requirement_ , that requires nothing, and with which
every play is consistent.

######  Definition 17 (Vacuous requirement).

In any game, the _vacuous requirement_ , denoted by $\lambda_{0}$, is the
requirement constantly equal to $-\infty$.

###  3.2 Negotiation

We will show that SPEs in prefix-independent games are characterized by the
fixed points of a function on requirements. That function can be seen as a
_negotiation_ : when a player has a requirement to satisfy, another player can
hope a better payoff than what they can secure in general, and therefore
update their own requirement.

######  Definition 18 (Negotiation function).

Let $G$ be a game. The _negotiation function_ is the function that transforms
any requirement $\lambda$ on $G$ into a requirement $\mathrm{nego}(\lambda)$
on $G$, such that for each $i\in\Pi$ and $v\in V_{i}$, with the convention
$\inf\emptyset=+\infty$, we have:

$\mathrm{nego}(\lambda)(v)=\underset{\bar{\sigma}_{-i}\in\lambda\mathrm{Rat}(v)}{\inf}\underset{\sigma_{i}}{\sup}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}\rangle_{v}).$

######  Remarks.

There exists a $\lambda$-rational strategy profile from $v$ against the player
controlling $v$ if and only if $\mathrm{nego}(\lambda)(v)\neq+\infty$. The
negotiation function is monotone: if $\lambda\leq\lambda^{\prime}$ (for the
pointwise order, i.e. if for each $v$, $\lambda(v)\leq\lambda^{\prime}(v)$),
then $\mathrm{nego}(\lambda)\leq\mathrm{nego}(\lambda^{\prime})$. The
negotiation function is also non-decreasing: for every $\lambda$, we have
$\lambda\leq\mathrm{nego}(\lambda)$.

In the general case, the quantity $\mathrm{nego}(\lambda)(v)$ represents the
worst case value that the player controlling $v$ can ensure, assuming that the
other players play $\lambda$-rationally.

######  Example 4.

Let us consider the game of Example 2: in Figure 1(b), on the two first lines
below the states, we present the requirements $\lambda_{0}$ and
$\lambda_{1}=\mathrm{nego}(\lambda_{0})$, which is easy to compute since any
strategy profile is $\lambda_{0}$-rational: for each $v$, $\lambda_{1}(v)$ is
the classical _worst-case value_ or _antagonistic value_ of $v$, i.e. the best
value the player controlling $v$ can enforce against a fully hostile
environment. Let us now compute the requirement
$\lambda_{2}=\mathrm{nego}(\lambda_{1})$.

From $c$, there exists exactly one $\lambda_{1}$-rational strategy profile
$\bar{\sigma}_{-{\scriptsize{\Circle}}}=\sigma_{\Box}$, which is the empty
strategy since player $\Box$ has never to choose anything. Against that
strategy, the best and the only payoff player $\Circle$ can get is $1$, hence
$\lambda_{2}(c)=1$. For the same reasons, $\lambda_{2}(d)=2$.

From $b$, player $\Circle$ can force $\Box$ to get the payoff $2$ or less,
with the strategy profile $\sigma_{\scriptsize{\Circle}}:h\mapsto c$. Such a
strategy is $\lambda_{1}$-rational, assuming the strategy
$\sigma_{\Box}:h\mapsto d$. Therefore, $\lambda_{2}(b)=2$.

Finally, from $a$, player $\Box$ can force $\Circle$ to get the payoff $2$ or
less, with the strategy profile $\sigma_{\Box}:h\mapsto d$. Such a strategy is
$\lambda_{1}$-rational, assuming the strategy
$\sigma_{\scriptsize{\Circle}}:h\mapsto c$. But, he cannot force her to get
less than the payoff $2$, because she can force the access to the state $b$,
and the only $\lambda_{1}$-consistent plays from $b$ are the plays with the
form $(ba)^{k}bd^{\omega}$. Therefore, $\lambda_{2}(a)=2$.

###  3.3 Steady negotiation

In what follows, we will often need a game to be _with steady negotiation_ ,
i.e. such that there always exists a worst $\lambda$-rational behaviour for
the environment against a given player.

######  Definition 19 (Game with steady negotiation).

A game $G$ is _with steady negotiation_ if and only if for every player $i$,
for every vertex $v$, and for every requirement $\lambda$, the set
$\left\\{\left.\sup_{\sigma_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}_{-i},\sigma_{i}\rangle_{v})\leavevmode\nobreak\
\right|\leavevmode\nobreak\
\bar{\sigma}_{-i}\in\lambda\mathrm{Rat}(v)\right\\}$ is either empty, or has a
minimum.

######  Remark.

In particular, when a game is with steady negotiation, the infimum in the
definition of negotiation is always reached.

It will be proved in Section 5 that mean-payoff games are with steady
negotiation.

###  3.4 Link with Nash equilibria

Requirements and the negotiation function are able to capture Nash equilibria.
Indeed, if $\lambda_{0}$ is the vacuous requirement, then
$\mathrm{nego}(\lambda_{0})$ characterizes the plays that are supported by a
Nash equilibrium (abbreviated by NE plays), in the following formal sense:

######  Theorem 1 (App. A).

Let $G$ be a game with steady negotiation. Then, a play $\rho$ in $G$ is an NE
play if and only if $\rho$ is $\mathrm{nego}(\lambda_{0})$-consistent.

######  Example 5.

Let us consider again the game of Example 2, with the requirement
$\lambda_{1}$ given in Figure 1(b). The only $\lambda_{1}$-consistent plays in
this game, starting from the state $a$, are $ac^{\omega}$, and
$(ab)^{k}d^{\omega}$ with $k\geq 1$. One can check that those plays are
exactly the NE plays in that game.

In the following section, we will prove that as well as
$\mathrm{nego}(\lambda_{0})$ characterizes the NEs, the requirement that is
the least fixed point of the negotiation function characterizes the SPEs.

##  4 Link between negotiation and SPEs

The notion of negotiation will enable us to find the SPEs, but also more
generally the $\varepsilon$-SPEs, in a game. For that purpose, we need the
notion of $\varepsilon$-fixed points of a function.

######  Definition 20 ($\varepsilon$-fixed point).

Let $\varepsilon\geq 0$, let $D$ be a finite set and let
$f:\overline{\mathbb{R}}^{D}\to\overline{\mathbb{R}}^{D}$ be a mapping. A
tuple $\bar{x}\in\mathbb{R}^{D}$ is a _$\varepsilon$ -fixed point_ of $f$ if
for each $d\in D$, for $\bar{y}=f(\bar{x})$, we have
$y_{d}\in[x_{d}-\varepsilon,x_{d}+\varepsilon]$.

######  Remark.

A $0$-fixed point is a fixed point, and conversely.

The set of requirements, equipped with the componentwise order, is a complete
lattice. Since the negotiation function is monotone, Tarski’s fixed point
theorem states that the negotiation function has a least fixed point. That
result can be generalized to $\varepsilon$-fixed points:

######  Lemma 1 (App. B).

Let $\varepsilon\geq 0$. On each game, the function $\mathrm{nego}$ has a
least $\varepsilon$-fixed point.

Intuitively, the $\varepsilon$-fixed points of the negotiation function are
the requirements $\lambda$ such that, from every vertex $v$, the player $i$
controlling $v$ cannot enforce a payoff greater than $\lambda(v)+\varepsilon$
against a $\lambda$-rational behaviour. Therefore, the $\lambda$-consistent
plays are such that if one player tries to deviate, it is possible for the
other players to prevent them improving their payoff by more than
$\varepsilon$, while still playing rationally. Formally:

######  Theorem 2 (App. C).

Let $G_{\upharpoonright v_{0}}$ be an initialized prefix-independent game, and
let $\varepsilon\geq 0$. Let $\lambda^{*}$ be the least $\varepsilon$-fixed
point of the negotiation function. Let $\xi$ be a play starting in $v_{0}$. If
there exists an $\varepsilon$-SPE $\bar{\sigma}$ such that
$\langle\bar{\sigma}\rangle_{v_{0}}=\xi$, then $\xi$ is
$\lambda^{*}$-consistent. The converse is true if the game $G$ is with steady
negotiation.

##  5 Negotiation games

We have now proved that SPEs are characterized by the requirements that are
fixed points of the negotiation function; but we need to know how to compute,
in practice, the quantity $\mathrm{nego}(\lambda)$ for a given requirement
$\lambda$. In other words, we need a algorithm that computes, given a state
$v_{0}$ controlled by a player $i$ in the game $G$, and given a requirement
$\lambda$, which value player $i$ can ensure in $G_{\upharpoonright v_{0}}$ if
the other players play $\lambda$-rationally.

###  5.1 Abstract negotiation game

We first define an _abstract negotiation game_ , that is conceptually simple
but not directly usable for an algorithmic purpose, because it is defined on
an uncoutably infinite state space.

A similar definition was given in [13], as a tool in a general method to
compute SPE plays in games whose payoff functions have finite range, which is
not the case of mean-payoff games. Here, linking that game with our concepts
of requirements, negotiation function and steady negotiation enables us to
present an effective algorithm in the case of mean-payoff games, by
constructing a finite version of the abstract negotiation game, the _concrete
negotiation game_ , and afterwards by analyzing the negotiation function with
linear algebra tools.

The abstract negotiation game from a state $v_{0}$, with regards to a player
$i$ and a requirement $\lambda$, is denoted by $\mathrm{Abs}_{\lambda
i}(G)_{\upharpoonright[v_{0}]}$ and opposes two players, _Prover_ and
_Challenger_ , as follows:

  * •

Prover proposes a $\lambda$-consistent play $\rho$ from $v_{0}$ (or loses, if
she has no play to propose).

  * •

Then, either Challenger accepts the play and the game terminates; or, he
chooses an edge $\rho_{k}\rho_{k+1}$, with $\rho_{k}\in V_{i}$, from which he
can make player $i$ deviate, using another edge $\rho_{k}v$ with
$v\neq\rho_{k+1}$: then, the game starts again from $v$ instead of $v_{0}$.

  * •

In the resulting play (either eventually accepted by Challenger, or
constructed by an infinity of deviations), Prover wants player $i$’s payoff to
be low, and Challenger wants it to be high.

That game gives us the basis of a method to compute $\mathrm{nego}(\lambda)$
from $\lambda$: the maximal outcome that Challenger — or $\mathbb{C}$ for
short — can ensure in $\mathrm{Abs}_{\lambda i}(G)_{\upharpoonright[v_{0}]}$,
with $v_{0}\in V_{i}$, is also the maximal payoff that player $i$ can ensure
in $G_{\upharpoonright v_{0}}$, against a $\lambda$-rational environment;
hence the equality $\mathrm{val}_{\mathbb{C}}\left(\mathrm{Abs}_{\lambda
i}(G)_{\upharpoonright[v_{0}]}\right)=\mathrm{nego}(\lambda)(v_{0}).$ A proof
of that statement, with a complete formalization of the abstract negotiation
game, is presented in Appendix D.

######  Example 6.

Let us consider again the game of Example 2: the requirement
$\lambda_{2}=\mathrm{nego}(\lambda_{1})$, computed in Section 3.2, is also
presented on the third line below the states in Figure 1(b). Let us use the
abstract negotiation game to compute the requirement
$\lambda_{3}=\mathrm{nego}(\lambda_{2})$.

From $a$, Prover can propose the play $abd^{\omega}$, and the only deviation
Challenger can do is going to $c$; he has of course no incentive to do it.
Therefore, $\lambda_{3}(a)=2$. From $b$, whatever Prover proposes at first,
Challenger can deviate and go to $a$. Then, from $a$, Prover cannot propose
the play $ac^{\omega}$, which is not $\lambda_{2}$-consistent: she has to
propose a play beginning by $ab$, and to let Challenger deviate once more. He
can then deviate infinitely often that way, and generate the play
$(ba)^{\omega}$: therefore, $\lambda_{3}(b)=3$. The other states keep the same
values. Note that there exists no $\lambda_{3}$-consistent play from $a$ or
$b$, hence
$\mathrm{nego}(\lambda_{3})(a)=\mathrm{nego}(\lambda_{3})(b)=+\infty$. This
proves that there is no SPE in that game.

The interested reader will find other such examples in Appendix N.

###  5.2 Concrete negotiation game

In the abstract negotiation game, Prover has to propose complete plays, on
which we can make the hypothesis that they are $\lambda$-consistent. In
practice, there will often be an infinity of such plays, and therefore it
cannot be used directly for an algorithmic purpose. Instead, those plays can
be given edge by edge, in a finite state game. Its definition is more
technical, but it can be shown that it is equivalent to the abstract one. In
order to make the definition as clear as possible, we give it only when the
original game is a mean-payoff game. However, one could easily adapt this
definition to other classes of prefix-independent games.

######  Definition 21 (Concrete negotiation game).

Let $G_{\upharpoonright v_{0}}$ be an initialized mean-payoff game, and let
$\lambda$ be a requirement on $G$, with either
$\lambda(V)\subseteq\mathbb{R}$, or $\lambda=\lambda_{0}$.

The _concrete negotiation game_ of $G_{\upharpoonright v_{0}}$ for player $i$
is the two-player zero-sum game $\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright
s_{0}}\leavevmode\nobreak\ =\leavevmode\nobreak\
\left(\\{\mathbb{P},\mathbb{C}\\},S,(S_{\mathbb{P}},S_{\mathbb{C}}),\Delta,\nu\right)_{\upharpoonright
s_{0}}$, defined as follows:

  * •

The set of states controlled by Prover is $S_{\mathbb{P}}=V\times 2^{V}$,
where the state $s=(v,M)$ contains the information of the current state $v$ on
which Prover has to define the strategy profile, and the _memory_ $M$ of the
states that have been traversed so far since the last deviation, and that
define the requirements Prover has to satisfy. The initial state is
$s_{0}=(v_{0},\\{v_{0}\\})$.

  * •

The set of states controlled by Challenger is $S_{\mathbb{C}}=E\times 2^{V}$,
where in the state $s=(uv,M)$, the edge $uv$ is the edge proposed by Prover.

  * •

The set $\Delta$ contains three types of transitions: _proposals_ ,
_acceptations_ and _deviations_.

    * –

The proposals are transitions in which Prover proposes an edge of the game
$G$:

$\mathrm{Prop}=\left\\{(v,M)(vw,M)\leavevmode\nobreak\
\left|\leavevmode\nobreak\ vw\in E,M\in 2^{V}\right.\right\\};$

    * –

the acceptations are transitions in which Challenger accepts to follow the
edge proposed by Prover (it is in particular his only possibility when that
edge begins on a state that is not controlled by player $i$) — note that the
memory is updated:

$\mathrm{Acc}=\left\\{(vw,M)\left(w,M\cup\\{w\\}\right)\leavevmode\nobreak\
\left|\leavevmode\nobreak\ j\in\Pi,w\in V_{j}\right.\right\\};$

    * –

the deviations are transitions in which Challenger refuses to follow the edge
proposed by Prover, as he can if that edge begins in a state controlled by
player $i$ — the memory is erased, and only the new state the deviating edge
leads to is memorized:

$\mathrm{Dev}=\left\\{(uv,M)(w,\\{w\\})\leavevmode\nobreak\
\left|\leavevmode\nobreak\ u\in V_{i},w\neq v,uw\in E\right.\right\\}.$

  * •

On those transitions, we define a multidimensional weight function
$\hat{\pi}:\Delta\to\mathbb{R}^{\Pi\cup\\{\star\\}}$, with one dimension per
player (_non-main_ dimensions) plus one special dimension (_main_ dimension)
denoted by the symbol $\star$. For each non-main dimension $j\in\Pi$, we
define:

    * –

on proposals: $\hat{\pi}_{j}\left((v,M)(vw,M)\right)=0$;

    * –

on acceptations and deviations:
$\hat{\pi}_{j}\left((uv,M)(w,N)\right)=2\left(\pi_{j}(uw)-\underset{v_{j}\in
M\cap V_{j}}{\max}\lambda(v_{j})\right)$;

and on the main dimension:

    * –

on proposals: $\hat{\pi}_{\star}\left((v,M),(vw,M)\right)=0$;

    * –

on acceptations and deviations:
$\hat{\pi}_{\star}\left((uv,M),(w,N)\right)=2\pi_{i}(uw)$.

For each dimension $d$, we write $\hat{\mu}_{d}$ the corresponding mean-payoff
function:

$\hat{\mu}_{d}(\rho)=\liminf_{n\in\mathbb{N}}\frac{1}{n}\sum_{k=0}^{n-1}\hat{\pi}_{d}(\rho_{k}\rho_{k+1}).$

Thus, the mean-payoff along the main dimension corresponds to player $i$’s
payoff, while the mean-payoff along a non-main dimension $j$ corresponds to
player $j$’s payoff… minus the maximal requirement player $j$ has to satisfy.

  * •

Then, the outcome function $\nu_{\mathbb{C}}=-\nu_{\mathbb{P}}$ measures
player $i$’s payoff, with a winning condition if the constructed strategy
profile is not $\lambda$-rational, that is to say if after finitely many
player $i$’s deviations, it can generate a play which is not
$\lambda$-consistent:

    * –

$\nu_{\mathbb{C}}(\eta)=+\infty$ if after some index $n\in\mathbb{N}$, the
play $\eta_{n}\eta_{n+1}\dots$ contains no deviation, and if
$\hat{\mu}_{j}(\eta)<0$ for some $j\in\Pi$;

    * –

$\nu_{\mathbb{C}}(\eta)=\hat{\mu}_{\star}(\eta)$ otherwise.

Like in the abstract negotiation game, the goal of Challenger is to find a
$\lambda$-rational strategy profile that forces the worst possible payoff for
player $i$, and the goal of Prover is to find a possibly deviating strategy
for player $i$ that gives them the highest possible payoff.

A play or a history in the concrete negotiation game has a projection in the
game on which that negotiation game has been constructed, defined as follows:

######  Definition 22 (Projection of a history, of a play).

Let $G$ be a prefix-independent game. Let $\lambda$ be a requirement and $i$ a
player, and let $\mathrm{Conc}_{\lambda i}(G)$ be the corresponding concrete
negotiation game. Let
$H=(h_{0},M_{0})(h_{0}h^{\prime}_{0},M_{0})\dots(h_{n}h^{\prime}_{n},M_{n})$
be a history in $\mathrm{Conc}_{\lambda i}(G)$: the _projection_ of the
history $H$ is the history $\dot{H}=h_{0}\dots h_{n}$ in the game $G$. That
definition is naturally extended to plays.

######  Remark.

For a play $\eta$ without deviations, we have $\hat{\mu}_{j}(\eta)\geq 0$ for
each $j\in\Pi$ if and only if $\dot{\eta}$ is $\lambda$-consistent.

The concrete negotiation game is equivalent to the abstract one: the only
differences are that the plays proposed by Prover are proposed edge by edge,
and that their $\lambda$-consistency is not written in the rules of the game
but in its outcome function.

######  Theorem 3 (App. E).

Let $G_{\upharpoonright v_{0}}$ be an initialized mean-payoff game. Let
$\lambda$ be a requirement and $i$ a player. Then, we have:

$\mathrm{val}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright
s_{0}}\right)=\inf_{\bar{\sigma}_{-i}\in\lambda\mathrm{Rat}(v_{0})}\leavevmode\nobreak\
\sup_{\sigma_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}\rangle_{v_{0}}).$

An example of concrete negotiation game is given in Appendix F.

###  5.3 Solving the concrete negotiation game

We now know that $\mathrm{nego}(\lambda)(v)$, for a given requirement
$\lambda$, a given player $i$ and a given state $v\in V_{i}$, is the value of
the concrete negotiation game $\mathrm{Conc}_{\lambda
i}(G)_{\upharpoonright(v,\\{v\\})}$. Let us now show how, in the mean-payoff
case, that value can be computed.

######  Definition 23 (Memoryless strategy).

A strategy $\sigma_{i}$ in a game $G$ is _memoryless_ if for all vertices
$v\in V_{i}$ and for all histories $h$ and $h^{\prime}$, we have
$\sigma_{i}(hv)=\sigma_{i}(h^{\prime}v)$.

For any game $G$ and any memoryless strategy $\sigma_{i}$, $G[\sigma_{i}]$
denotes the graph _induced_ by $\sigma_{i}$, that is the graph
$(V,E^{\prime})$, with $E^{\prime}=\left\\{vw\in E\leavevmode\nobreak\
|\leavevmode\nobreak\ v\not\in V_{i}\mathrm{\leavevmode\nobreak\
or\leavevmode\nobreak\ }w=\sigma_{i}(v)\right\\}.$ For any finite set $D$ and
any set $X\subseteq\mathbb{R}^{D}$, $\mathrm{Conv}X$ denotes the convex hull
of $X$.

We can now prove that in the concrete negotiation game constructed from a
mean-payoff game, Challenger has an optimal strategy that is memoryless.

######  Lemma 2 (App. G).

Let $G_{\upharpoonright v_{0}}$ be an initialized mean-payoff game, let $i$ be
a player, let $\lambda$ be a requirement and let $\mathrm{Conc}_{\lambda
i}(G)_{\upharpoonright s_{0}}$ be the corresponding concrete negotiation game.
There exists a memoryless strategy $\tau_{\mathbb{C}}$ that is optimal for
Challenger, i.e. such that:

$\underset{\tau_{\mathbb{P}}}{\inf}\leavevmode\nobreak\
\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}})=\mathrm{val}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda
i}(G)_{\upharpoonright s_{0}}\right).$

For every game $G_{\upharpoonright v_{0}}$ and each player $i$,
$\mathrm{ML}_{i}\left(G_{\upharpoonright v_{0}}\right)$, or
$\mathrm{ML}\left(G_{\upharpoonright v_{0}}\right)$ when the context is clear,
denotes the set of memoryless strategies for player $i$ in $G_{\upharpoonright
v_{0}}$. When $(V,E)$ is a graph, $\mathrm{SC}(V,E)$ denotes the set of its
simple cycles, and $\mathrm{SConn}(V,E)$ the set of its strongly connected
components. For any closed set $C\subseteq\mathbb{R}^{\Pi\cup\\{\star\\}}$,
the quantity $\min\\!^{\star}C=\min\left\\{x_{\star}\leavevmode\nobreak\
|\leavevmode\nobreak\ \bar{x}\in C,\forall j\in\Pi,x_{j}\geq 0\right\\}$ is
the _$\star$ -minimum_ of $C$: it will capture, in the concrete negotiation
game, the least payoff that can be imposed on player $i$ while keeping every
player’s payoff above their requirements, among a set of possible outcomes.

With Lemma 2, we can now solve the concrete negotiation game.

######  Lemma 3 (App. H).

Let $G_{\upharpoonright v_{0}}$ be an initialized mean-payoff game, and let
$\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright s_{0}}$ be its concrete
negotiation game for some $\lambda$ and some $i$. Then, the value of the game
$\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright s_{0}}$ is given by the
formula:

$\max_{\tau_{\mathbb{C}}\in\mathrm{ML}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda
i}(G)\right)}\leavevmode\nobreak\
\min_{\scriptsize{\begin{matrix}K\in\mathrm{SConn}\left(\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}]\right)\\\ \mathrm{accessible\leavevmode\nobreak\
from\leavevmode\nobreak\ }s_{0}\end{matrix}}}\mathrm{opt}(K),$

where $\mathrm{opt}(K)$ is the minimal value $\nu_{\mathbb{C}}(\rho)$ for
$\rho$ among the infinite paths in $K$.

If $K$ contains a deviation, then Prover can choose among its simple cycles
the one that minimizes player $i$’s payoff:

$\mathrm{opt}(K)=\underset{c\in\mathrm{SC}(K)}{\min}\leavevmode\nobreak\
\hat{\mu}_{\star}(c^{\omega}).$

If $K$ does not contain a deviation, then Prover must choose a combination of
its simple cycles that minimizes the main dimension while keeping the other
dimensions above $0$:

$\mathrm{opt}(K)=\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\leavevmode\nobreak\
\hat{\mu}(c^{\omega}).$

######  Corollary 1.

For each player $i$ and every state $v\in V_{i}$, the value
$\mathrm{nego}(\lambda)(v)$ can be computed with the formula given in Lemma 3
applied to the game $\mathrm{Conc}_{\lambda
i}(G)_{\upharpoonright(v,\\{v\\})}$

Another corollary of that result is that there always exists a best play that
Prover can choose, i.e. Prover has an optimal strategy; by Theorem 3, this is
equivalent to saying that:

######  Corollary 2.

Mean-payoff games are games with steady negotiation.

##  6 Analysis of the negotiation function in mean-payoff games

When one wants to compute the least fixed point of a function, the usual
method is to iterate it on the minimal element of the considered set, to go
until that fixed point. That approach is sufficient in many simple examples.
In Appendix I, we present its technical details, and an example on which it
does not enable to find the least fixed point in a finite number of
iterations; which is why another approach is necessary.

In this section, we will show that, in the case of mean-payoff games, the
negotiation function is a piecewise linear function from the vector space of
requirements into itself, which can therefore be computed and analyzed using
classical linear algebra techniques. Then, it becomes possible to search for
the fixed points or the $\varepsilon$-fixed points of such a function, and to
decide the existence or not of SPEs or $\varepsilon$-SPEs in the game studied.

######  Theorem 4 (App. K).

Let $G$ be a mean-payoff game. Let us assimilate any requirement $\lambda$ on
$G$ with finite values to the tuple
$\lambda\mspace{-10.0mu}\bar{\phantom{v}}=(\lambda(v))_{v\in V}$, element of
the vector space $\mathbb{R}^{V}$. Then, for each player $i$ and every vertex
$v_{0}\in V_{i}$, the quantity $\mathrm{nego}(\lambda)(v_{0})$ is a piecewise
linear function of $\lambda\mspace{-10.0mu}\bar{\phantom{v}}$, and an
effective expression of that function can be computed in 2-ExpTime.

######  Example 7.

Let us consider the game of Example 3. If a requirement $\lambda$ is
represented by the tuple $(\lambda(a),\lambda(b))$, the function
$\mathrm{nego}:\mathbb{R}^{2}\to\mathbb{R}^{2}$ can be represented by Figure
3(a), where in any one of the regions delimited by the dashed lines, we wrote
a formula for the couple
$(\mathrm{nego}(\lambda)(a),\mathrm{nego}(\lambda)(b))$. The orange area
indicates the fixed points of the function, and the yellow area the other
$\frac{1}{2}$-fixed points.

$\lambda(a)$$\lambda(b)$12012$(1,1)$$(1,\lambda(b))$$(\lambda(a),1)$$(2\lambda(b)-2,\lambda(b))$$(\lambda(a),2\lambda(a)-2)$$(\lambda(a),\lambda(b))$$(+\infty,+\infty)$
(a) Example 3

$\lambda(a)$$\lambda(b)$123012$(1,2)$$(2,2)$$(2,3)$$(1,3)$$(+\infty,+\infty)$
(b) Example 2

Figure 3: The negotiation function on the games of Examples 3 and 2

######  Example 8.

Now, let us consider the game of Example 2. If we fix $\lambda(c)=1$ and
$\lambda(d)=2$, and represent the requirements $\lambda$ by the tuples
$(\lambda(a),\lambda(b))$, as in the previous example. Then, the negotiation
function can be represented as in Figure 3(b). One can check that there is no
fixed point here, and even no $\frac{1}{2}$-fixed point — except
$(+\infty,+\infty)$.

##  7 Conclusion: algorithm and complexity

Thanks to all the previous results, we are now able to compute the least fixed
point, or the least $\varepsilon$-fixed point, of the negotiation function, on
every mean-payoff game, and to use it as a characterization of all the SPEs or
all the $\varepsilon$-SPEs. A direct application is an algorithm that solves
the _$\varepsilon$ -SPE constrained existence problem_, i.e. that decides,
given an initialized mean-payoff game $G_{\upharpoonright v_{0}}$, two
thresholds $\bar{x},\bar{y}\in\mathbb{Q}^{\Pi}$, and a rational number
$\varepsilon\geq 0$, whether there exists an SPE $\bar{\sigma}$ such that
$\bar{x}\leq\mu(\langle\bar{\sigma}\rangle_{v_{0}})\leq\bar{y}$.

We leave for future work the optimal complexity of that problem. However, we
can easily prove that it cannot be solved in polynomial time, unless
$\mathbf{P=NP}$.

######  Theorem 5 (App. L).

The $\varepsilon$-SPE constrained existence problem is NP-hard.

Given $G_{\upharpoonright v_{0}}$, by Theorem 4, computing a general
expression of the negotiation function as a piecewise linear function can be
done in time double exponential in the size of $G$. Then, for each linear
piece of $\mathrm{nego}$, computing its set of $\varepsilon$-fixed points is a
polynomial problem. Since the number of pieces is at most double exponential
in the size of $G$, computing its entire set of fixed points, and thus its
least $\varepsilon$-fixed point $\lambda$, can be done in double exponential
time.

Then, from the requirement $\lambda$ and the thresholds $\bar{x}$ and
$\bar{y}$, we can construct a multi-mean-payoff automaton
$\mathcal{A}_{\lambda}$ of exponential size, that accepts an infinite word
$\rho\in V^{\omega}$, if and only if $\rho$ is a $\lambda$-consistent play of
$G_{\upharpoonright v_{0}}$, and $\bar{x}\leq\mu(\rho)\leq\bar{y}$ — see
Appendix M for the construction of $\mathcal{A}_{\lambda}$.

Finally, by Theorem 2, there exists an SPE $\bar{\sigma}$ in
$G_{\upharpoonright v_{0}}$ with
$\bar{x}\leq\mu(\langle\bar{\sigma}\rangle_{v_{0}})\leq\bar{y}$ if and only if
the language of the automaton $\mathcal{A}_{\lambda}$ is nonempty, which can
be known in a time polynomial in the size of $\mathcal{A}_{\lambda}$ (see for
example [1]), i.e. in a time exponential in the size of $G$. We can therefore
conclude on the following result:

######  Theorem 6.

The $\varepsilon$-SPE constrained existence problem is decidable and
2-ExpTime-easy.

## References

  * [1] Rajeev Alur, Aldric Degorre, Oded Maler, and Gera Weiss.  On omega-languages defined by mean-payoff conditions.  In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5504 of Lecture Notes in Computer Science, pages 333–347. Springer, 2009.  doi:10.1007/978-3-642-00596-1\\_24.
  * [2] 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.
  * [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, Véronique Bruyère, Noémie Meunier, and Jean-François Raskin.  Weak subgame perfect equilibria and their application to quantitative reachability.  In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 504–518. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
  * [5] 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.
  * [6] 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.
  * [7] Véronique Bruyère, Noémie Meunier, and Jean-François Raskin.  Secure equilibria in weighted games.  In CSL-LICS, pages 26:1–26:26. ACM, 2014.
  * [8] Véronique Bruyère, Stéphane Le Roux, Arno Pauly, and Jean-François Raskin.  On the existence of weak subgame perfect equilibria.  CoRR, abs/1612.01402, 2016.
  * [9] Véronique Bruyère, Stéphane Le Roux, Arno Pauly, and Jean-François Raskin.  On the existence of weak subgame perfect equilibria.  In Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 145–161, 2017.
  * [10] Krishnendu Chatterjee, Laurent Doyen, Herbert Edelsbrunner, Thomas A. Henzinger, and Philippe Rannou.  Mean-payoff automaton expressions.  In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 269–283. Springer, 2010.
  * [11] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman.  Strategy logic.  Inf. Comput., 208(6):677–693, 2010.  doi:10.1016/j.ic.2009.07.004.
  * [12] János Flesch, Jeroen Kuipers, Ayala Mashiah-Yaakovi, Gijs Schoenmakers, Eilon Solan, and Koos Vrieze.  Perfect-information games with lower-semicontinuous payoffs.  Math. Oper. Res., 35(4):742–755, 2010.
  * [13] 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.  doi:10.1287/moor.2016.0843.
  * [14] 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.
  * [15] Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi.  Synthesis with rational environments.  Ann. Math. Artif. Intell., 78(1):3–20, 2016.  doi:10.1007/s10472-016-9508-8.
  * [16] Donald A. Martin.  Borel determinacy.  Annals of Mathematics, pages 363–371, 1975.
  * [17] Noémie Meunier.  Multi-Player Quantitative Games: Equilibria and Algorithms.  PhD thesis, Université de Mons, 2016.
  * [18] Martin J. Osborne.  An introduction to game theory.  Oxford Univ. Press, 2004.
  * [19] Eilon Solan and Nicolas Vieille.  Deterministic multi-player dynkin games.  Journal of Mathematical Economics, 39(8):911–929, 2003.
  * [20] Michael Ummels.  Rational behaviour and strategy construction in infinite multiplayer games.  In 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.
  * [21] Michael Ummels.  The complexity of nash equilibria in infinite multiplayer games.  In Roberto M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, volume 4962 of Lecture Notes in Computer Science, pages 20–34. Springer, 2008.  doi:10.1007/978-3-540-78499-9\\_3.
  * [22] Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin.  The complexity of multi-mean-payoff and multi-energy games.  Inf. Comput., 241:177–196, 2015.
  * [23] Nicolas Vieille and Eilon Solan.  Deterministic multi-player Dynkin games.  Journal of Mathematical Economics, Vol.39,num. 8:pp.911–929, November 2003.  URL: https://hal-hec.archives-ouvertes.fr/hal-00464953, doi:10.1016/S0304-4068(03)00021-1.

The following appendices are providing the detailed proofs of all our results.
They are not necessary to understand our results and are meant to provide full
formalization and rigorous proofs. They also provide further intuitions
through additional examples for the interested reader. To improve readability,
we have chosen to recall the statements that appeared in the main body of the
paper before giving their detailed proofs in order to ease the work of the
reader.

##  Appendix A Proof of Theorem 1

Theorem 1. _Let $G$ be a game with steady negotiation. Then, a play $\rho$ in
$G$ is an NE play if and only if $\rho$ is
$\mathrm{nego}(\lambda_{0})$-consistent._

###### Proof.

  * •

Let $\bar{\sigma}$ be a Nash equilibrium in $G_{\upharpoonright v_{0}}$, for
some state $v_{0}$, and let $\rho=\langle\bar{\sigma}\rangle_{v_{0}}$ : let us
prove that the play $\rho$ is $\mathrm{nego}(\lambda_{0})$-consistent.

Let $k\in\mathbb{N}$, let $i\in\Pi$ be such that $\rho_{k}\in V_{i}$, and let
us prove that
$\mu_{i}\left(\rho_{k}\rho_{k+1}\dots\right)\geq\mathrm{nego}(\lambda_{0})(\rho_{k})$.

For any deviation $\sigma^{\prime}_{i}$ of
$\sigma_{i\upharpoonright\rho_{0}\dots\rho_{k}}$, by definition of NEs,
$\mu_{i}\left(\langle\bar{\sigma}_{-i\upharpoonright\rho_{0}\dots\rho_{k}},\sigma^{\prime}_{i}\rangle_{\rho_{k}}\right)\leq\mu_{i}(\rho)$.
Therefore:

$\mu_{i}(\rho)\geq\sup_{\sigma^{\prime}_{i}}\leavevmode\nobreak\
\mu_{i}\left(\langle\bar{\sigma}_{-i\upharpoonright\rho_{0}\dots\rho_{k}},\sigma^{\prime}_{i}\rangle_{\rho_{k}}\right)$

hence:

$\mu_{i}(\rho)\geq\inf_{\bar{\tau}_{-i}}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}\left(\langle\bar{\tau}_{-i\upharpoonright\rho_{0}\dots\rho_{k}},\tau_{i}\rangle_{\rho_{k}}\right)$

i.e.:

$\mu_{i}(\rho)\geq\mathrm{nego}(\lambda_{0})(\rho_{k}).$

  * •

Let $\rho$ be a $\mathrm{nego}(\lambda_{0})$-consistent play from a state
$v_{0}$. Let us define a strategy profile $\bar{\sigma}$ such that
$\langle\bar{\sigma}\rangle_{v_{0}}=\rho$, by:

    * –

$\langle\bar{\sigma}\rangle_{v_{0}}=\rho$;

    * –

for all histories of the form $\rho_{0}\dots\rho_{k}v$ with $v\neq\rho_{k+1}$,
let $i$ be the player controlling $\rho_{k}$.

Since the game $G$ is with steady negotiation, the infimum:

$\inf_{\bar{\tau}_{-i}\in\lambda_{0}\mathrm{Rat}(\rho_{k})}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}\rangle_{\rho_{k}})$

is a minimum. Let $\bar{\tau}^{k}_{-i}$ be $\lambda_{0}$-rational strategy
profile from $\rho_{k}$ realizing that minimum, and let $\tau^{k}_{i}$ be some
strategy from $\rho_{k}$ such that $\tau^{k}_{i}(\rho_{k})=v$. Then, we
define:

$\langle\bar{\sigma}_{\upharpoonright\rho_{0}\dots\rho_{k}v}\rangle_{v}=\langle\bar{\tau}^{k}_{\rho_{k}v}\rangle_{v};$

    * –

for every other history $h$, $\bar{\sigma}(h)$ is defined arbitrarily.

Let us prove that $\bar{\sigma}$ is an NE: let $\sigma^{\prime}_{i}$ be a
deviation of $\sigma_{i}$, let
$\rho^{\prime}=\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}}$
and let $\rho_{0}\dots\rho_{k}$ be the longest common prefix of $\rho$ and
$\rho^{\prime}$. Let $v=\rho^{\prime}_{k+1}$.

Then, we have:

$\mu_{i}(\rho^{\prime})\leq\sup_{\tau_{i}^{k}}\leavevmode\nobreak\
\mu_{i}\left(\langle\bar{\tau}^{k}\rangle_{\rho_{k}}\right)=\mathrm{nego}(\lambda_{0})(\rho_{k}),$

and since $\rho$ is $\lambda_{0}$-consistent,
$\mathrm{nego}(\lambda_{0})(\rho_{k})\leq\mu_{i}(\rho)$, hence
$\mu_{i}(\rho^{\prime})\leq\mu_{i}(\rho)$.

∎

##  Appendix B Proof of Lemma 1

Lemma 1. _Let $G$ be a game, and let $\varepsilon\geq 0$. The negotiation
function has a least $\varepsilon$-fixed point._

###### Proof.

The following proof is a generalization of a classical proof of Tarski’s fixed
point theorem.

Let $\Lambda$ be the set of the $\varepsilon$-fixed points of the negotiation
function. The set $\Lambda$ is not empty, since it contains at least the
requirement $v\mapsto+\infty$. Let $\lambda^{*}$ be the requirement defined
by:

$\lambda^{*}:v\mapsto\inf_{\lambda\in\Lambda}\lambda(v).$

For every $\varepsilon$-fixed point $\lambda$ of the negotiation function, we
have then for each $v$, $\lambda^{*}(v)\leq\lambda(v)$, and
$\mathrm{nego}(\lambda^{*})(v)\leq\mathrm{nego}(\lambda)(v)$ since
$\mathrm{nego}$ is monotone; and therefore,
$\mathrm{nego}(\lambda^{*})(v)\leq\lambda(v)+\varepsilon$.

As a consequence, we have:

$\mathrm{nego}(\lambda^{*})(v)\leq\inf_{\lambda\in\Lambda}\lambda(v)+\varepsilon=\lambda^{*}(v)+\varepsilon.$

The requirement $\lambda^{*}$ is an $\varepsilon$-fixed point of the
negotiation function, and is therefore the least $\varepsilon$-fixed point of
the negotiation function. ∎

##  Appendix C Proof of Theorem 2

Theorem 2. _Let $G_{\upharpoonright v_{0}}$ be an initialized prefix-
independent game, and let $\varepsilon\geq 0$. Let $\lambda^{*}$ be the least
$\varepsilon$-fixed point of the negotiation function. Let $\xi$ be a play
starting in $v_{0}$. If there exists an $\varepsilon$-SPE $\bar{\sigma}$ such
that $\langle\bar{\sigma}\rangle_{v_{0}}=\xi$, then $\xi$ is
$\lambda^{*}$-consistent. The converse is true if the game $G$ is with steady
negotiation._

###### Proof.

First, let us recall that $\lambda^{*}$ exists by Lemma 1.

Then, our proof can be decomposed in two lemmas:

######  Lemma 4.

Let $G_{\upharpoonright v_{0}}$ be a well-initialized prefix-independent game,
and let $\varepsilon\geq 0$. Let $\bar{\sigma}$ be an $\varepsilon$-SPE in
$G_{\upharpoonright v_{0}}$. Then, there exists an $\varepsilon$-fixed point
$\lambda$ of the negotiation function such that for every history $hv$
starting in $v_{0}$, the play $\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v}$ is $\lambda$-consistent.

###### Proof.

Let us define the requirement $\lambda$ by, for each $i\in\Pi$ and $v\in
V_{i}$:

$\lambda(v)=\inf_{hv\in\mathrm{Hist}G_{\upharpoonright
v_{0}}}\mu_{i}(\langle\bar{\sigma}_{\upharpoonright hv}\rangle_{v}).$

Note that the set $\left\\{\mu_{i}(\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v})\leavevmode\nobreak\ |\leavevmode\nobreak\
hv\in\mathrm{Hist}G_{\upharpoonright v_{0}}\right\\}$ is never empty, since
the game $G_{\upharpoonright v_{0}}$ is well-initialized.

Then, for every history $hv$ starting in $v_{0}$, the play
$\langle\bar{\sigma}_{\upharpoonright hv}\rangle_{v}$ is $\lambda$-consistent.
Let us prove that $\lambda$ is an $\varepsilon$-fixed point of
$\mathrm{nego}$: let $i\in\Pi$, let $v\in V_{i}$, and let us assume towards
contradiction (since the negotiation function is non-decreasing) that
$\mathrm{nego}(\lambda)(v)>\lambda(v)+\varepsilon$, that is to say:

$\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(v)}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}\rangle_{v})>\inf_{hv\in\mathrm{Hist}G_{\upharpoonright
v_{0}}}\mu_{i}(\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v})+\varepsilon.$

Then, since all the plays generated by the strategy profile $\bar{\sigma}$ are
$\lambda$-consistent, and therefore since any strategy profile of the form
$\bar{\sigma}_{-i\upharpoonright hv}$ is $\lambda$-rational, we have:

$\inf_{hv}\leavevmode\nobreak\ \sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}_{-i\upharpoonright
hv},\tau_{i}\rangle_{v})>\inf_{hv}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}_{\upharpoonright hv}\rangle_{v})+\varepsilon.$

Therefore, there exists a history $hv$ such that:

$\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}_{-i\upharpoonright
hv},\tau_{i}\rangle_{v})>\mu_{i}(\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v})+\varepsilon,$

which is impossible if the strategy profile $\bar{\sigma}$ is an
$\varepsilon$-SPE. Therefore, there is no such $v$, and the requirement
$\lambda$ is an $\varepsilon$-fixed point of the negotiation function. ∎

######  Lemma 5.

Let $G_{\upharpoonright v_{0}}$ be a well-initialized prefix-independent game
with steady negotiation, and $\varepsilon\geq 0$. Let $\lambda$ be an
$\varepsilon$-fixed point of the function $\mathrm{nego}$. Then, for every
$\lambda$-consistent play $\xi$ starting in $v_{0}$, there exists an
$\varepsilon$-SPE $\bar{\sigma}$ such that
$\langle\bar{\sigma}\rangle_{v_{0}}=\xi$.

###### Proof.

  * •

_Particular case: if there exists $v$ such that $\lambda(v)=+\infty$._

In that case, for each $u$ such that $uv\in E$, if the player controlling $u$
chooses to go to $v$, no $\lambda$-consistent play can be proposed to them
from there, hence there is no $\lambda$-rational strategy profile against that
player from $u$, and $\mathrm{nego}(\lambda)(u)=+\infty$. Since $\varepsilon$
is finite and since $\lambda$ is an $\varepsilon$-fixed point of the
negotiation function, it follows that $\lambda(u)=+\infty$. Since
$G_{\upharpoonright v_{0}}$ is well-initialized, we can repeat this argument
and show that $\lambda(v_{0})=+\infty$; in that case, there is no
$\lambda$-consistent play $\xi$ from $u$, and then the proof is done.

Therefore, for the rest of the proof, we assume that for all $v$, we have
$\lambda(v)\neq+\infty$. As a consequence, since $\lambda$ is an
$\varepsilon$-fixed point of the function $\mathrm{nego}$, for all $v$, we
have $\mathrm{nego}(\lambda)(v)\neq+\infty$; and so finally, for each such
$v$, there exists a $\lambda$-consistent play starting from $v$.

  * •

_Preliminary result: a game with steady negotiation is also with subgame-
steady negotiation._

Recall that since $G$ is a game with steady negotiation, for every requirement
$\lambda$, for every player $i$ and for every state $v$, there exists a
$\lambda$-rational strategy profile $\bar{\tau}^{v}$ such that:

$\sup_{\tau^{v}_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}^{v}\rangle_{v})=\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(v)}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\ \mu_{i}(\langle\bar{\tau}\rangle_{v})$

i.e. there exists a worst $\lambda$-rational strategy profile against player
$i$ from the state $v$, with regards to player $i$’s payoff.

Our goal in this part of the proof is to show that $G$ is then also with
_subgame-steady negotiation_ , that is to say, for every requirement
$\lambda$, for every player $i$ and for every state $v$, there exists a
$\lambda$-rational strategy profile $\bar{\tau}^{v*}_{-i}$ such that for every
history $hw$ starting from $v$ compatible with $\bar{\tau}^{v*}_{-i}$, we
have:

$\sup_{\tau^{v*}_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}^{v*}_{\upharpoonright
hw}\rangle_{w})=\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(w)}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\ \mu_{i}(\langle\bar{\tau}\rangle_{w}),$

i.e. there exists a $\lambda$-rational strategy profile against player $i$
from the state $v$, that is the worst with regards to player $i$’s payoff in
any subgame, in other words a _subgame-worst_ strategy profile.

Let us construct inductively the strategy profile $\bar{\tau}^{v*}_{-i}$ and
the strategy $\tau^{v*}_{i}$ assuming which it is $\lambda$-rational. We
define them only on histories that are compatible with $\bar{\tau}^{v*}_{-i}$,
since they can be defined arbitrarily on any other histories. We proceed by
assembling the strategy profiles of the form $\bar{\tau}^{w}$, and the
histories after which we follow a new $\bar{\tau}^{w}$ will be called the
_resets_ of $\bar{\tau}^{v*}_{-i}$.

    * –

First, $\langle\bar{\tau}^{v*}\rangle_{v}=\langle\bar{\tau}^{v}\rangle_{v}$:
the one-state history $v$ is then the first reset of $\bar{\tau}^{v*}_{-i}$;

    * –

then, for every history $hw$ from $v$ such that $h$ is compatible with
$\bar{\tau}^{v*}_{-i}$ and ends in $V_{i}$, and such that
$w\neq\tau^{v*}_{i}(h)$: let us write $hw=h^{\prime}uh^{\prime\prime}$ so that
$h^{\prime}u$ is the longest reset of $\bar{\tau}^{v*}_{-i}$ among the
prefixes of $h$, and therefore so that the strategy profile
$\bar{\tau}^{v*}_{\upharpoonright h^{\prime}u}$ has been defined as equal to
$\bar{\tau}^{u}$ over the prefixes of $h^{\prime\prime}$ until $w$. Then, we
have:

$\sup_{\tau_{i}}\mu_{i}(\langle\bar{\tau}^{w}_{-i},\tau_{i}\rangle_{w})\leq\sup_{\tau_{i}}\mu_{i}(\langle\bar{\tau}^{u}_{-i\upharpoonright
uh^{\prime\prime}},\tau_{i}\rangle_{w})$

by prefix-independence of $G$ and since by its definition, the strategy
profile $\bar{\tau}^{w}_{-i}$ minimizes the quantity
$\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}^{w}_{-i},\tau_{i}\rangle_{w})$. Let us separate two
cases.

      * *

Suppose first that:

$\sup_{\tau_{i}}\mu_{i}(\langle\bar{\tau}^{w}_{-i},\tau_{i}\rangle_{w})=\sup_{\tau_{i}}\mu_{i}(\langle\bar{\tau}^{u}_{-i\upharpoonright
uh^{\prime\prime}},\tau_{i}\rangle_{w}).$

Then, $\langle\bar{\tau}^{v*}_{\upharpoonright
hw}\rangle=\langle\bar{\tau}^{u}_{\upharpoonright
uh^{\prime\prime}}\rangle_{w}$: the coalition of players against player $i$
keeps following their strategy profile so that player $i$ will have no more
than the payoff they can ensure.

      * *

Suppose now that:

$\sup_{\tau_{i}}\mu_{i}(\langle\bar{\tau}^{w}_{-i},\tau_{i}\rangle_{w})<\sup_{\tau_{i}}\mu_{i}(\langle\bar{\tau}^{u}_{-i\upharpoonright
uh^{\prime\prime}},\tau_{i}\rangle_{w}).$

Then, $\langle\bar{\tau}^{v^{*}}_{\upharpoonright
hw}\rangle=\langle\bar{\tau}^{w}\rangle_{w}$: player $i$ has done something
that lowers the payoff they can ensure, and therefore the other players have
to update their strategy profile in order to enforce that new minimum.

The history $hw$ is a reset of $\bar{\tau}^{v*}_{-i}$.

All the plays constructed are $\lambda$-consistent, hence
$\bar{\tau}^{v*}_{-i}$ is indeed $\lambda$-rational assuming $\tau^{v*}_{i}$.

Let us now prove that $\tau^{v*}_{i}$ is the subgame-worst $\lambda$-rational
strategy profile against player $i$. Let $hw$ be a history starting in $v$
compatible with $\bar{\tau}^{v*}_{-i}$, let $\tau^{\prime}_{i}$ be a strategy
from the state $w$, let $\eta=\langle\bar{\tau}^{v*}_{-i\upharpoonright
hw},\tau^{\prime}_{i}\rangle_{w}$ and let us prove that:

$\mu_{i}(\eta)\leq\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(w)}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\ \mu_{i}(\langle\bar{\tau}\rangle_{w}).$

Let us consider the sequence $(\alpha_{n})_{n\in\mathbb{N}}$, defined by:

$\alpha_{n}=\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(\eta_{n})}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}\rangle_{\eta_{n}}).$

That sequence is non-increasing. Indeed, for all $n$:

      * *

If $\eta_{n}\in V_{i}$, then no action of player $i$ can improve the payoff
player $i$ themself can secure against a $\lambda$-rational environment.

      * *

If $\eta_{n}\not\in V_{i}$, then:
$\eta_{n+1}=\bar{\tau}^{v*}_{-i}(h\eta_{0}\dots\eta_{n})=\bar{\tau}^{\eta_{k}}_{-i}(\eta_{k}\dots\eta_{n})$
for some $k$ such that, by construction of $\bar{\tau}^{v*}_{-i}$,
$\alpha_{k}=\dots=\alpha_{n}$. Since the strategy profile
$\bar{\tau}^{\eta_{k}}_{-i}$ is defined to realize the payoff
$\alpha_{k}=\alpha_{n}$, we have $\alpha_{n+1}=\alpha_{n}$.

Moreover, that sequence can only take a finite number of values (at most
$\mathrm{card}V$). Therefore, it is stationary: there exists
$n_{0}\in\mathbb{N}$ such that $(\alpha_{n})_{n\geq n_{0}}$ is constant, and
there are no resets of $\bar{\tau}^{v*}_{-i}$ among the prefixes of $\eta$ of
length greater than $n_{0}$.

Therefore, if we choose $n_{0}$ minimal (i.e., $n_{0}$ is the index of the
last reset in $\eta$), then the play $\eta_{n_{0}}\eta_{n_{0}+1}\dots$ is
compatible with the strategy profile $\bar{\tau}^{\eta_{n_{0}}}_{-i}$. Then,
we have:

$\mu_{i}(\eta)\leq\alpha_{n_{0}}\leq\alpha_{0},$

and:

$\alpha_{0}=\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(w)}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\ \mu_{i}(\langle\bar{\tau}\rangle_{w}),$

which proves that $\bar{\tau}^{v*}$ is the subgame-worst $\lambda$-strategy
profile against player $i$ from the state $w$, and therefore that the game $G$
is a game with subgame-steady negotiation.

  * •

_Construction of $\bar{\sigma}$._

Let $\mathcal{H}_{0}=\mathrm{Hist}G_{\upharpoonright v_{0}}$. Let us construct
inductively $\bar{\sigma}$ by defining all the plays
$\langle\bar{\sigma}_{\upharpoonright hv}\rangle_{v}$, for
$hv\in\mathcal{H}_{0}$, keeping the hypothesis that at any step $n$, the set
$\mathcal{H}_{n}$ contains exactly the histories $hv$ such that the play
$\langle\bar{\sigma}_{\upharpoonright hv}\rangle_{v}$ has been defined, and
that such a play is always $\lambda$-consistent: it will define a
$\lambda$-rational strategy profile, and we will then prove it is an
$\varepsilon$-SPE.

    * –

First, $\langle\bar{\sigma}\rangle_{v_{0}}=\xi$, which satisfies the induction
hypothesis. We remove then all the finite prefixes of $\xi$ form
$\mathcal{H}_{0}$ to obtain $\mathcal{H}_{1}$. Note that the only history of
length $1$ has been removed.

    * –

At the $n$-th step, with $n>0$: let us choose $hv\in\mathcal{H}_{n}$ of
minimal length, and therefore minimal for the prefix order: the strategy
profile $\bar{\sigma}$ has been defined on all the strict prefixes of $hv$,
but not on $hv$ itself, and $v\neq\bar{\sigma}(h)$. Let then $i$ be the player
controlling the last state of $h$ (which exists since all the histories of
$\mathcal{H}_{n}$ have length at least $2$). Let $\bar{\tau}^{v*}_{-i}$ be a
subgame-worst $\lambda$-rational strategy profile against player $i$ from $v$,
whose existence has been proved in the previous point, and let $\tau^{v*}_{i}$
be a strategy assuming which it is $\lambda$-rational.

Then, we define $\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v}=\langle\bar{\tau}^{v*}\rangle_{v}$, and inductively, for every
history $h^{\prime}w$ starting from $v$ and compatible with
$\bar{\sigma}_{-i\upharpoonright hv}$ as it has been defined so far, we define
$\langle\bar{\sigma}_{\upharpoonright
hh^{\prime}w}\rangle_{v}=\langle\bar{\tau}^{v*}_{\upharpoonright
h^{\prime}w}\rangle_{w}$. The strategy profile $\bar{\sigma}_{\upharpoonright
hv}$ is then equal to $\bar{\tau}^{v*}$ on any history compatible with
$\bar{\tau}^{v*}_{-i}$.

We remove all such histories from $\mathcal{H}_{n}$ to obtain
$\mathcal{H}_{n+1}$. All the plays we built are $\lambda$-consistent, which
was our induction hypothesis.

Since each step removes from $\mathcal{H}_{n}$ a history of minimal length,
and since there are finitely many histories of any given length, we have
$\bigcap_{n}\mathcal{H}_{n}=\emptyset$, and this process completely defines
$\bar{\sigma}$.

  * •

_Such $\bar{\sigma}$ is an $\varepsilon$-SPE._

Let $h^{(0)}w\in\mathrm{Hist}G_{\upharpoonright v_{0}}$, let $i\in\Pi$, let
$\sigma^{\prime}_{i}$ be a deviation of $\sigma_{i}$. Let
$\rho=h^{(0)}\langle\bar{\sigma}_{\upharpoonright h^{(0)}w}\rangle_{w}$ and
let $\rho^{\prime}=h^{(0)}\langle\sigma^{\prime}_{i\upharpoonright
h^{(0)}w},\bar{\sigma}_{-i\upharpoonright h^{(0)}w}\rangle_{w}$. We prove that
$\mu_{i}(\rho^{\prime})\leq\mu_{i}(\rho)+\varepsilon$.

If $\rho^{\prime}$ is compatible with $\sigma_{i}$, then $\rho^{\prime}=\rho$
and the proof is immediate. If it is not, we let $huv$ denote the shortest
prefix of $\rho^{\prime}$ such that $u\in V_{i}$ and $v\neq\sigma_{i}(hu)$.
The transition $uv$ can be considered as the first deviation of player $i$,
but note that $hu$ can be both longer or shorter than $h^{(0)}$: player $i$
may have already deviated in $h^{(0)}$.

Be that as it may, the history $hu$ is a common prefix of the play $\rho$ and
$\rho^{\prime}$, and if $\bar{\tau}^{v*}_{-i}$ denotes a subgame-worst
strategy profile against player $i$ from the state $v$, $\lambda$-rational
assuming a strategy $\tau^{v*}_{i}$, then $\bar{\sigma}_{\upharpoonright huv}$
has been defined as equal to $\bar{\tau}^{v*}$ on any history compatible with
$\bar{\sigma}_{-i\upharpoonright huv}$.

    * –

If $huv$ is a prefix of $\rho$: let $huh^{\prime}w^{\prime}$ be the longest
common prefix of $\rho$ and $\rho^{\prime}$. Necessarily, $w^{\prime}\in
V_{i}$. Then, by definition of $\bar{\tau}^{v*}_{-i}$, we have:

$\mu_{i}(\rho^{\prime})\leq\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(w^{\prime})}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}\rangle_{w^{\prime}})=\mathrm{nego}(\lambda)(w^{\prime}),$

and since $\lambda$ is an $\varepsilon$-fixed point of $\mathrm{nego}$:

$\mu_{i}(\rho^{\prime})\leq\lambda(w^{\prime})+\varepsilon.$

On the other hand, the play $\langle\bar{\sigma}_{\upharpoonright
h^{\prime}w^{\prime}}\rangle_{w^{\prime}}$, which is a suffix of $\rho$, is
$\lambda$-consistent, hence $\mu_{i}(\rho)\geq\lambda(w^{\prime})$.

Therefore, $\mu_{i}(\rho^{\prime})\leq\mu_{i}(\rho)+\varepsilon$.

    * –

If $huv$ is not a prefix of $\rho$: then,
$\rho=h\langle\bar{\sigma}_{\upharpoonright hu}\rangle_{u}$. Since $u\in
V_{i}$, we have:

$\mathrm{nego}(\lambda)(u)=\sup_{uv^{\prime}\in E}\leavevmode\nobreak\
\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(v^{\prime})}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}\rangle_{v^{\prime}}).$

In particular, we have:

$\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(v)}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\tau}\rangle_{v})\leq\mathrm{nego}(\lambda)(u)\leq\lambda(u)+\varepsilon.$

Then, for the same reason as above, we know that:

$\mu_{i}(\rho^{\prime})\leq\inf_{\bar{\tau}_{-i}\in\lambda\mathrm{Rat}(v)}\leavevmode\nobreak\
\sup_{\tau_{i}}\leavevmode\nobreak\ \mu_{i}(\langle\bar{\tau}\rangle_{v}).$

Finally, since the suffix $\langle\bar{\sigma}_{\upharpoonright
hu}\rangle_{u}$ of $\rho$ is $\lambda$-consistent, we have
$\mu_{i}(\rho)\geq\lambda(u)\geq\mathrm{nego}(\lambda)(u)-\varepsilon\geq\mu_{i}(\rho^{\prime})$.

The strategy profile $\bar{\sigma}$ is an $\varepsilon$-SPE.

∎

If $\bar{\sigma}$ is an $\varepsilon$-SPE, then by Lemma 4, there exists an
$\varepsilon$-fixed point $\lambda$ of the negotiation function such that all
the plays generated by $\bar{\sigma}$ after some history are
$\lambda$-consistent; in particular, the play $\xi$ is $\lambda$-consistent,
and therefore $\lambda^{*}$-consistent since $\lambda^{*}\leq\lambda$.

Conversely, if the game $G$ is with steady negotiation, and if the play $\xi$
is $\lambda^{*}$-consistent, then by Lemma 5, there exists an
$\varepsilon$-SPE $\bar{\sigma}$ such that
$\langle\bar{\sigma}\rangle_{v_{0}}=\xi$. ∎

##  Appendix D Abstract negotiation game

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

Let $G_{\upharpoonright v_{0}}$ be an initialized game, let $i\in\Pi$, and let
$\lambda$ be a requirement on $G$. The _abstract negotiation game_ of
$G_{\upharpoonright v_{0}}$ for player $i$ with requirement $\lambda$ is the
two-player zero-sum initialized 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:

  * •

$\mathbb{P}$ denotes the player _Prover_ and $\mathbb{C}$ the player
_Challenger_ ;

  * •

the states of $S_{\mathbb{C}}$ are written $[\rho]$, where $\rho$ is a
$\lambda$-consistent play in $G$;

  * •

the states of $S_{\mathbb{P}}$ are written $[hv]$, where $hv$ is a history in
$G$, with $h\in\mathrm{Hist}_{i}(G)$, or $[v]$ with $v\in V$, plus two
additional states $\top$ and $\bot$;

  * •

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

    * –

$[hv][v\rho]$, where $[hv]\in S_{\mathbb{P}}$ and $[v\rho]\in S_{\mathbb{C}}$
(Prover proposes a play);

    * –

$[\rho][\rho_{0}...\rho_{n}v]$, where $[\rho]\in
S_{\mathbb{C}},n\in\mathbb{N},\rho_{n}\in V_{i}$, and $v\neq\rho_{n+1}$
(Challenger makes player $i$ deviate);

    * –

$[\rho]\top$, where $[\rho]\in S_{\mathbb{C}}$ (Challenger accepts the
proposed play);

    * –

$\top\top$ (the game is over);

    * –

$[hv]\bot$ (Prover has no more play to propose);

    * –

$\bot\bot$ (the game is over).

  * •

$\nu$ is the outcome function defined by, for all
$\rho^{(0)},\rho^{(1)},\dots,h^{(1)}v_{1},h^{(2)}v_{2},\dots,k,H$:

$\begin{matrix}&\nu_{\mathbb{C}}\left([v_{0}]\left[\rho^{(0)}\right]\left[h^{(1)}v_{1}\right]\left[\rho^{(1)}\right]\dots\left[h^{(k)}v_{k}\right]\left[\rho^{(k)}\right]\top^{\omega}\right)\\\\[2.84526pt]
=&\mu_{i}\left(h^{(1)}\dots h^{(k)}\rho^{(k)}\right),\\\\[5.69054pt]
&\nu_{\mathbb{C}}\left([v_{0}]\left[\rho^{(0)}\right]\left[h^{(1)}v_{1}\right]\left[\rho^{(1)}\right]\dots\left[h^{(n)}v_{n}\right]\left[\rho^{(n)}\right]\dots\right)\\\\[2.84526pt]
=&\mu_{i}\left(h^{(1)}h^{(2)}\dots\right),\\\\[5.69054pt]
&\nu_{\mathbb{C}}\left(H\bot^{\omega}\right)=+\infty,\end{matrix}$

and by $\nu_{\mathbb{P}}=-\nu_{\mathbb{C}}$.

######  Proposition 2.

Let $G_{\upharpoonright v_{0}}$ be an initialized Borel game, let $\lambda$ be
a requirement on $G$ and let $i\in\Pi$. Then, the corresponding abstract
negotiation game satisfies:

$\inf_{\tau_{\mathbb{P}}}\leavevmode\nobreak\
\sup_{\tau_{\mathbb{C}}}\leavevmode\nobreak\
\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{[v_{0}]})=\inf_{\bar{\sigma}_{-i}\in\lambda\mathrm{Rat}(v_{0})}\leavevmode\nobreak\
\sup_{\sigma_{i}}\leavevmode\nobreak\
\mu_{i}\left(\langle\bar{\sigma}\rangle_{v_{0}}\right).$

###### Proof.

Let $\alpha\in\mathbb{R}$, and let us prove that the following statements are
equivalent:

  1. 1.

there exists a strategy $\tau_{\mathbb{P}}$ such that for every strategy
$\tau_{\mathbb{C}}$,
$\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{[v_{0}]})<\alpha$;

  2. 2.

there exists a $\lambda$-rational strategy profile $\bar{\sigma}_{-i}$ in the
game $G_{\upharpoonright v_{0}}$ such that for every strategy $\sigma_{i}$, we
have $\mu_{i}\left(\langle\bar{\sigma}\rangle_{v_{0}}\right)<\alpha$.

  * •

_( 1) implies (2)._

Let $\tau_{\mathbb{P}}$ be such that for every strategy $\tau_{\mathbb{C}}$,
$\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{[v_{0}]})<\alpha$.

In what follows, any history $h$ compatible with an already defined strategy
profile $\bar{\sigma}_{-i}$ in $G_{\upharpoonright v_{0}}$ will be decomposed
in:

$h=v_{0}h^{(0)}v_{1}h^{(1)}\dots h^{(n-1)}v_{n}h^{(n)},$

so that there exist plays $\rho^{(0)},\dots,\rho^{(n-1)},\eta$ and a history:

$[v_{0}]\left[\rho^{(0)}\right]\left[v_{1}h^{(1)}v_{2}\right]\dots\left[v_{n-1}h^{(n-1)}v_{n}\right]\left[v_{n}h^{(n)}\eta\right]$

in the game $\mathrm{Abs}_{\lambda i}(G)$ compatible with $\tau_{\mathbb{P}}$:
the existence and the unicity of that decomposition can be proved by
induction. Intuitively, the history $h$ is cut in histories which are prefixes
of plays that can be proposed by Prover.

Then, let us define inductively the strategy profile $\bar{\sigma}_{-i}$ by,
for every $h$ such that $\bar{\sigma}_{-i}$ has been defined on the prefixes
of $h$, and such that the last state of $h$ is not controlled by player $i$,
$\bar{\sigma}_{-i}(h)=\eta_{0}$ with $\eta$ defined from $h$ as higher. Let us
prove that $\bar{\sigma}_{-i}$ is the desired strategy profile.

    * –

_The strategy profile $\bar{\sigma}_{-i}$ is $\lambda$-rational._

Let us define $\sigma_{i}$ so that for every history $hv$ compatible with
$\bar{\sigma}_{-i}$, the play $\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v}$ is $\lambda$-consistent.

For any history:

$h=v_{0}h^{(0)}v_{1}h^{(1)}\dots h^{(n-1)}v_{n}h^{(n)}$

compatible with $\bar{\sigma}_{-i}$ and ending in $V_{i}$, let
$\sigma_{i}(h)=\eta_{0}$ with $\eta$ corresponding to the decomposition of
$h$, so that by induction:

$\langle\bar{\sigma}_{\upharpoonright v_{0}h^{(0)}v_{1}h^{(1)}\dots
h^{(n-1)}v_{n}}\rangle_{v_{n}}=v_{n}h^{(n)}\eta.$

Let now $hv$ be a history in $G_{\upharpoonright v_{0}}$, and let us show that
the play $\langle\bar{\sigma}_{\upharpoonright hv}\rangle_{v}$ is
$\lambda$-consistent. If we decompose:

$hv=v_{0}h^{(0)}v_{1}h^{(1)}\dots h^{(n-1)}v_{n}h^{(n)}$

with the same definition of $\eta$ (note that the vertex $v$ is now included
in the decomposition), then $\langle\bar{\sigma}_{\upharpoonright
hv}\rangle_{v}=v\eta$, and by definition of the abstract negotiation game,
$v_{n}h^{(n)}\eta$ is a $\lambda$-consistent play, and therefore so is
$v\eta$.

    * –

_The strategy profile $\bar{\sigma}_{-i}$ keeps player $i$’s payoff under the
value $\alpha$._

Let $\sigma_{i}$ be a strategy for player $i$, and let
$\rho=\langle\bar{\sigma}\rangle_{v_{0}}$. We want to prove that
$\mu_{i}(\rho)<\alpha$.

Let us define two finite or infinite sequences $\left(\rho^{(k)}\right)_{k\in
K}$ and $\left(h^{(k)}v_{k}\right)_{k\in K}$, where $K=\\{1,\dots,n\\}$ or
$K=\mathbb{N}\setminus\\{0\\}$, by for every $k\in K$:

$\left[\rho^{(k)}\right]=\tau_{\mathbb{P}}\left([v_{0}]\left[\rho^{(0)}\right]\dots\left[\rho^{(k-1)}\right]\left[h^{(k)}v_{k}\right]\right)$

and so that for every $k$, the history $h^{(k)}v_{k}$ is the shortest prefix
of $\rho$ that is not a prefix of $h^{(1)}\dots h^{(k-1)}\rho^{(k-1)}$ (or
equivalently, the history $h^{(k)}$ is the longest common prefix of $\rho$ and
$h^{(1)}\dots h^{(k-1)}\rho^{(k-1)}$).

Then, the length of the longest common prefix of $h^{(1)}\dots
h^{(k-1)}\rho^{(k)}$ and $\rho$ increases with $k$, and the set $K$ is finite
if and only if there exists $n$ such that $h^{(1)}\dots
h^{(n-1)}\rho^{(n)}=\rho$.

In the infinite case, let:

$\chi=[v_{0}]\left[\rho^{(0)}\right]\left[h^{(1)}v_{1}\right]\dots\left[\rho^{(k)}\right]\left[h^{(k)}v_{k}\right]\dots.$

The play $\chi$ is compatible with $\tau_{\mathbb{P}}$, hence
$\nu_{\mathbb{C}}(\chi)<\alpha$, that is to say:

$\mu_{i}\left(h^{(1)}h^{(2)}\dots\right)<\alpha,$

ie. $\mu_{i}(\rho)<\alpha$.

In the finite case, let:

$\chi=[v_{0}]\left[\rho^{(0)}\right]\left[h^{(1)}v_{1}\right]\dots\left[\rho^{(n)}\right]\top^{\omega}.$

For the same reason, $\nu_{\mathbb{C}}(\chi)<\alpha$, that is to say
$\mu_{i}\left(h^{(1)}\dots h^{(n)}\rho^{(n)}\right)=\mu_{i}(\rho)<\alpha$.

  * •

_( 2) implies (1)._

Let $\bar{\sigma}_{-i}$ be a strategy profile keeping player $i$’s payoff
below $\alpha$, $\lambda$-rational assuming a strategy $\sigma_{i}$. Let us
define a strategy $\tau_{\mathbb{P}}$ for Prover in the abstract negotiation
game.

Let
$H=[v_{0}]\left[\rho^{(0)}\right]\left[h^{(1)}v_{1}\right]\left[\rho^{(1)}\right]\dots\left[h^{(n)}v_{n}\right]$
be a history in the abstract game, ending in $S_{\mathbb{P}}$. Then, we
define:

$\tau_{\mathbb{P}}(H)=\left[\langle\bar{\sigma}_{\upharpoonright h^{(1)}\dots
h^{(n)}v_{n}}\rangle_{v_{n}}\right].$

If $H$ is a history ending in $\top$, then $\tau_{\mathbb{P}}(H)=\top$, and in
the same way if $H$ ends in $\bot$, then $\tau_{\mathbb{P}}(H)=\bot$.

Let us show that $\tau_{\mathbb{P}}$ is the strategy we were looking for. Let
$\chi$ be a play compatible with $\tau_{\mathbb{P}}$, and let us note that the
state $\bot$ does not appear in $\chi$. Then, the play $\chi$ can only have
two forms:

    * –

If
$\chi=[v_{0}]\left[\rho^{(0)}\right]\left[h^{(1)}v_{1}\right]\dots\left[\rho^{(n)}\right]\top^{\omega}$,
then we have:

$\rho^{(n)}=\langle\bar{\sigma}_{\upharpoonright h^{(1)}\dots
h^{(n)}v_{n}}\rangle_{v_{n}},$

and the history $h^{(1)}\dots h^{(n)}v_{n}$ in the game $G_{\upharpoonright
v_{0}}$ is compatible with $\bar{\sigma}_{-i}$. By hypothesis, we have:

$\mu_{i}\left(h^{(1)}\dots h^{(n)}\rho^{(n)}\right)<\alpha,$

hence $\nu_{\mathbb{C}}(\chi)<\alpha$.

    * –

If
$\chi=[v_{0}]\left[\rho^{(0)}\right]\dots\left[h^{(n)}v_{n}\right]\left[\rho^{(n)}\right]\dots$,
then the play $\rho=h^{(1)}h^{(2)}\dots$ is compatible with
$\bar{\sigma}_{-i}$, and by hypothesis $\mu_{i}(\rho)<\alpha$, hence
$\nu_{\mathbb{C}}(\chi)<\alpha$.

∎

######  Remark.

We have proven the equality:

$\inf_{\tau_{\mathbb{P}}}\leavevmode\nobreak\
\sup_{\tau_{\mathbb{C}}}\leavevmode\nobreak\
\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{\upharpoonright
v_{0}})=\inf_{\bar{\sigma}_{-i}\in\lambda\mathrm{Rat}(v_{0})}\leavevmode\nobreak\
\sup_{\sigma_{i}}\leavevmode\nobreak\
\mu_{i}\left(\langle\bar{\sigma}\rangle_{v_{0}}\right).$

To be absolutely rigorous, the left member can be written
$\mathrm{val}_{\mathbb{C}}\left(\mathrm{Abs}_{\lambda
i}(G)_{\upharpoonright[v_{0}]}\right)$ only if we prove that the abstract
negotiation game is determined. That will be a consequence of its equivalence
with the corresponding concrete negotiation game, which is Borel and therefore
determined.

##  Appendix E Proof of Theorem 3

Theorem 3. _Let $G_{\upharpoonright v_{0}}$ be an initialized mean-payoff
game. Let $\lambda$ be a requirement and $i$ a player. Then, we have:_

$\mathrm{val}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright
s_{0}}\right)=\inf_{\bar{\sigma}_{-i}\in\lambda\mathrm{Rat}(v_{0})}\leavevmode\nobreak\
\sup_{\sigma_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}\rangle_{v_{0}}).$

###### Proof.

First, let us define:

$A=\left\\{\left.\sup_{\sigma_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}\rangle_{v_{0}})\leavevmode\nobreak\
\right|\leavevmode\nobreak\
\bar{\sigma}_{-i}\in\lambda\mathrm{Rat}(v_{0})\right\\}$

and:

$B=\left\\{\left.\sup_{\tau_{\mathbb{C}}}\leavevmode\nobreak\
\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}})\leavevmode\nobreak\
\right|\leavevmode\nobreak\ \tau_{\mathbb{P}}\right\\}\setminus\\{+\infty\\}.$

We prove our point if we prove that $A=B$.

  * •

_$B\subseteq A$._

Let $\tau_{\mathbb{P}}$ be a strategy such that:

$\sup_{\tau_{\mathbb{C}}}\leavevmode\nobreak\
\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}})<+\infty,$

and let $\bar{\sigma}$ be the strategy profile defined by:

$\bar{\sigma}(\dot{H})=w$

for every history $H$ compatible with $\tau_{\mathbb{P}}$ (by induction, the
localized projection is injective on the histories compatible with
$\tau_{\mathbb{P}}$) with $\tau_{\mathbb{P}}(H)=(vw,\cdot)$, and arbitrarily
defined on any other histories.

    * –

_The strategy profile $\bar{\sigma}_{-i}$ is $\lambda$-rational_, assuming the
strategy $\sigma_{i}$. Indeed, let us assume it is not.

Then, there exists a history $h=h_{0}\dots h_{n}$ in $G_{\upharpoonright
v_{0}}$ compatible with $\bar{\sigma}_{-i}$ such that the play
$\dot{\rho}=\langle\bar{\sigma}_{\upharpoonright h}\rangle_{h_{n}}$ is not
$\lambda$-consistent. Then, let:

$Hs=\left(h_{0},M_{0}\right)\left(h_{0}\bar{\sigma}(h_{0}),M_{0}\right)\dots\left(h_{n},M_{n}\right)$

be the only history in $\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright s_{0}}$
compatible with $\tau_{\mathbb{P}}$ such that $\dot{H}=h$.

Let $\tau_{\mathbb{C}}$ be a strategy constructing the history $h$, defined
by:

$\tau_{\mathbb{C}}\left(H_{0}\dots H_{2k-1}\right)=H_{2k}$

for every $k$, and:

$\tau_{\mathbb{C}}\left(H^{\prime}(vw,M)\right)=(w,M\cup\\{w\\})$

for any other history $H^{\prime}(vw,M)$.

Then, the play $\eta=\langle\bar{\tau}\rangle_{s_{0}}$ contains finitely many
deviations (Challenger stops the deviations after having drawn the history
$h$), and the play $\dot{\eta}=h_{0}\dots h_{n-1}\dot{\rho}$ is not
$\lambda$-consistent, i.e. there exists a dimension $j\in\Pi$ such that:

$\mu_{j}(\dot{\eta})-\max_{v\in M_{n}\cap V_{j}}\lambda(v)<0$

i.e.:

$\hat{\mu}_{j}(\eta)<0$

and therefore $\nu_{\mathbb{C}}(\rho)=\nu_{\mathbb{C}}(\eta)=+\infty$, which
is false by hypothesis.

    * –

Now, let us prove the equality:

$\sup_{\sigma^{\prime}_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}})=\sup_{\tau_{\mathbb{C}}}\leavevmode\nobreak\
\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}}).$

For that purpose, let us prove the equality of sets:

$\left\\{\mu_{i}(\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}})\leavevmode\nobreak\
|\leavevmode\nobreak\
\sigma^{\prime}_{i}\right\\}=\left\\{\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}})\leavevmode\nobreak\
|\leavevmode\nobreak\ \tau_{\mathbb{C}}\right\\}.$

      * *

Let $\tau_{\mathbb{C}}$ be a strategy for Challenger, and let
$\rho=\langle\bar{\tau}\rangle_{s_{0}}$. Since
$\nu_{\mathbb{C}}(\rho)\neq+\infty$ by hypothesis, we have
$\nu_{\mathbb{C}}(\rho)=\hat{\mu}_{\star}(\rho)=\mu_{i}(\dot{\rho})$, which is
an element of the left-hand set.

      * *

Conversely, if $\sigma^{\prime}_{i}$ is a strategy for player $i$ and if
$\eta=\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}}$, let
$\tau_{\mathbb{C}}$ be a strategy such that for every $k$:

$\tau_{\mathbb{C}}\left((\eta_{0},\cdot)(\eta_{0}\cdot,\cdot)\dots(\eta_{k}\cdot,\cdot)=(\eta_{k+1},\cdot)\right),$

i.e. a strategy forcing $\eta$.

Then, since $\nu_{\mathbb{C}}(\rho)\neq+\infty$ by hypothesis on
$\tau_{\mathbb{P}}$, we have $\mu_{i}(\eta)=\nu_{\mathbb{C}}(\rho)$, which is
an element of the right-hand set.

  * •

_$A\subseteq B$._

Let $\bar{\sigma}_{-i}$ be a $\lambda$-rational strategy profile from $v_{0}$,
assuming the strategy $\sigma_{i}$; let us define a strategy
$\tau_{\mathbb{P}}$ by, for every history $H$ and for every $v\in V$:

$\tau_{\mathbb{P}}(H(v,\cdot))=\left(v\bar{\sigma}(\dot{H}v),\cdot\right).$

Let us prove the equality:

$\sup_{\sigma^{\prime}_{i}}\leavevmode\nobreak\
\mu_{i}(\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}})=\sup_{\tau_{\mathbb{C}}}\leavevmode\nobreak\
\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}}).$

For that purpose, let us prove the equality of sets:

$\left\\{\mu_{i}(\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}})\leavevmode\nobreak\
|\leavevmode\nobreak\
\sigma^{\prime}_{i}\right\\}=\left\\{\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}})\leavevmode\nobreak\
|\leavevmode\nobreak\ \tau_{\mathbb{C}}\right\\}.$

    * –

Let $\tau_{\mathbb{C}}$ be a strategy for Challenger, and let
$\rho=\langle\bar{\tau}\rangle_{s_{0}}$.

If $\nu_{\mathbb{C}}(\rho)=+\infty$, then $\dot{\rho}$ is compatible with
$\bar{\sigma}$ and not $\lambda$-consistent after finitely many steps, which
is impossible.

Therefore, $\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}})\neq+\infty$,
and as a consequence we have
$\nu_{\mathbb{C}}(\rho)=\hat{\mu}_{\star}(\rho)=\mu_{i}(\dot{\rho})$, which is
an element of the left-hand set.

    * –

Conversely, if $\sigma^{\prime}_{i}$ is a strategy for player $i$ and if
$\eta=\langle\bar{\sigma}_{-i},\sigma^{\prime}_{i}\rangle_{v_{0}}$, let
$\tau_{\mathbb{C}}$ be a strategy such that for all $k$:

$\tau_{\mathbb{C}}\left((\eta_{0},\cdot)(\eta_{0}\cdot,\cdot)\dots(\eta_{k}\cdot,\cdot)\right)=(\eta_{k+1},\cdot),$

i.e. a strategy forcing $\eta$.

Then, either $\nu_{\mathbb{C}}(\rho)=+\infty$, and therefore $\eta$ is not
$\lambda$-consistent, and is compatible with $\bar{\sigma}$ after finitely
many steps, which is impossible.

Or, $\mu_{i}(\eta)=\nu_{\mathbb{C}}(\rho)$, which is an element of the right-
hand set.

∎

##  Appendix F An example of concrete negotiation game

Let us consider again the game from Example 2.

Figure 4 represents the game
$\mathrm{Conc}_{\lambda_{1}{\scriptsize{\Circle}}}(G)$ (with
$\lambda_{1}(a)=1$ and $\lambda_{1}(b)=2$), where the dashed states are
controlled by Challenger, and the other ones by Prover.

$b,\\{a,b\\}$$ba,\\{a,b\\}$$a,\\{a,b\\}$$ab,\\{a,b\\}$$a,\\{a\\}$$ab,\\{a\\}$$c,\\{c\\}$$cc,\\{c\\}$$ac,\\{a\\}$$c,\\{a,c\\}$$cc,\\{a,c\\}$$b,\\{b\\}$$ba,\\{b\\}$$bd,\\{b\\}$$d,\\{b,d\\}$$dd,\\{b,d\\}$$ac,\\{a,b\\}$$c,\\{a,b,c\\}$$cc,\\{a,b,c\\}$$bd,\\{a,b\\}$$d,\\{a,b,d\\}$$dd,\\{a,b,d\\}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{-2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{0}}}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{-2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{0}}}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{2}}}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{2}}}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{4}}}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{-2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{2}}}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{4}}}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{0}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{0}}}$$\scriptsize{\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{-2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\Box}}{{2}}\leavevmode\nobreak\
\stackrel{{\scriptstyle\star}}{{0}}}$ Figure 4: A concrete negotiation game

The dotted arrows indicate the deviations, and the transitions that are not
labelled are either zero for the three coordinates, or meaningless since they
cannot be used more than once.

The red arrows indicate a (memoryless) optimal strategy for Challenger.
Against that strategy, the lowest outcome Prover can ensure is $2$.

Therefore, $\mathrm{nego}(\lambda_{1})(v_{0})=2$, in line with the abstract
game in Example 6.

##  Appendix G Proof of Lemma 2

Lemma 2. _Let $G_{\upharpoonright v_{0}}$ be an initialized mean-payoff game,
let $i$ be a player, let $\lambda$ be a requirement and let
$\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright s_{0}}$ be the corresponding
concrete negotiation game. There exists a memoryless strategy
$\tau_{\mathbb{C}}$ that is optimal for Challenger, i.e. such that:_

$\underset{\tau_{\mathbb{P}}}{\inf}\leavevmode\nobreak\
\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}})=\mathrm{val}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda
i}(G)_{\upharpoonright s_{0}}\right).$

###### Proof.

The structure of that proof is inspired from the proof of Lemma 14 in [22].

Let $\alpha\in\mathbb{R}$, and let $\Phi$ be the set of the plays $\rho$ in
$\mathrm{Conc}_{\lambda i}(G)$ such that:

  * •

$\underset{n\to\infty}{\liminf}\frac{1}{n}\underset{k=0}{\overset{n-1}{\sum}}\left(-\hat{\pi}_{\star}(\rho_{k}\rho_{k+1})\right)\geq-\alpha$;

  * •

and either:

    * –

$\rho$ contains infinitely many deviations;

    * –

or for each $j\in\Pi$, $\hat{\mu}_{j}(\rho)\geq 0$.

Note that the set of the plays $\rho$ such that
$\nu_{\mathbb{C}}(\rho)\leq\alpha$ could be defined almost the same way, but
with a limit superior instead of the limit inferior.

By [14], if Challenger can falsify the objective $\Phi$, he can falsify it
with a memoryless strategy, if $\Phi$ is _prefix-independent_ and _convex_.

_Convex_ objectives are defined as follows: the objective $\Phi$ is convex if
for all $\rho,\eta\in\Phi$ and for any decomposition:

$\rho_{0}\dots\rho_{k_{1}}\dots\rho_{k_{2}}\dots$

and:

$\eta_{0}\dots\eta_{\ell_{1}}\dots\eta_{\ell_{2}}\dots$

with $\eta_{\ell_{p}}=\rho_{k_{q}}$ for all $p,q\in\mathbb{N}$, we have:

$\chi=\rho_{0}\dots\rho_{k_{1}}\eta_{1}\dots\eta_{\ell_{1}}\rho_{k_{1}+1}\dots\rho_{k_{2}}\eta_{\ell_{1}+1}\dots\in\Phi.$

Let then be such two plays and decomposition, and let us prove that
$\chi\in\Phi$.

Let us write $\Phi=\Psi\cap(\mathrm{X}\cup\Xi)$, where:

  * •

$\Psi$ is the set of the plays $\rho$ such that:

$\underset{n\to\infty}{\liminf}\frac{1}{n}\underset{k=0}{\overset{n-1}{\sum}}\left(-\hat{\pi}_{\star}(\rho_{k}\rho_{k+1})\right)\geq-\alpha;$

  * •

$\mathrm{X}$ is the set of the plays containing infinitely many deviations;

  * •

$\Xi$ is the set of the plays $\rho$ such that for each $j\in\Pi$,
$\hat{\mu}_{j}(\rho)\geq 0$.

As shown in [22], a mean-payoff objective defined with a limit inferior is
convex: therefore, we can already say that $\chi\in\Psi$. Let us now prove
that $\chi\in\mathrm{X}\cup\Xi$.

  * •

_If $\rho\in\mathrm{X}$ or $\eta\in\mathrm{X}$._

Then, $\chi$ contains the deviations of $\rho$ and $\eta$, hence
$\chi\in\mathrm{X}$.

  * •

_If $\rho,\eta\in\Xi$._

Then, since mean-payoff objectives are convex, we have $\chi\in\Xi$.

In both cases, $\chi\in\mathrm{X}\cup\Xi$, so $\chi\in\Phi$: the objective
$\Phi$ is convex.

Therefore, if Challenger has some strategy to falsify the objective $\Phi$, he
has a memoryless one: let us write it $\tau_{\mathbb{C}}$.

Now, we want to prove that the memoryless strategy $\tau_{\mathbb{C}}$ is also
efficient when we replace the limit inferior of the definition of $\Phi$ by a
limit superior, even though this new objective is no longer convex.

By definition of $\tau_{\mathbb{C}}$, for every strategy $\tau_{\mathbb{P}}$,
we have $\langle\bar{\tau}\rangle_{s_{0}}\not\in\Phi$. Let us prove that
$\nu_{\mathbb{C}}(\langle\bar{\tau}\rangle_{s_{0}})>\alpha$.

In other words, let us prove that for every infinite path $\rho$ from $s_{0}$
in the graph $\mathrm{Conc}_{\lambda i}(G)[\tau_{\mathbb{C}}]$, we have
$\nu_{\mathbb{C}}(\rho)>\alpha$. Since $\rho\not\in\Phi$, we have either
$\rho\not\in\mathrm{X}\cup\Xi$ or $\rho\not\in\Psi$. In the first case, we
have $\nu_{\mathbb{C}}(\rho)=+\infty$, which ends the proof. In the second
case, we have:

$\underset{n\to\infty}{\limsup}\frac{1}{n}\underset{k=0}{\overset{n-1}{\sum}}\hat{\pi}_{\star}(\rho_{k}\rho_{k+1})>\alpha.$

We want to prove that $\nu_{\mathbb{C}}(\rho)>\alpha$, that is, since we
assume $\rho\in\mathrm{X}\cup\Xi$:

$\hat{\mu}_{\star}(\rho)=\underset{n\to\infty}{\liminf}\frac{1}{n}\underset{k=0}{\overset{n-1}{\sum}}\hat{\pi}_{\star}(\rho_{k}\rho_{k+1})>\alpha.$

Here, the play $\rho$ is an infinite path in the graph $\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}]$: by the description of the possible outcomes in a
mean-payoff game given in [10], the mean-payoff $\hat{\mu}_{\star}(\rho)$ is
then larger than or equal to the minimal mean-payoff $\hat{\mu}_{\star}$ we
get by looping on a simple cycle $c$ of that graph accessible from the state
$s$. Intuitively, a play can be seen as a combination of those cycles. That is
to say:

$\hat{\mu}_{\star}(\rho)\geq\underset{\tiny{\begin{matrix}c\in\mathrm{SC}\left(\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}]\right)\\\ \mathrm{accessible\leavevmode\nobreak\
from\leavevmode\nobreak\ }s\end{matrix}}}{\min}\hat{\mu}_{\star}(c^{\omega}).$

For each such cycle, since $c^{\omega}$ is a play compatible with
$\tau_{\mathbb{C}}$, we have:

$\underset{n\to\infty}{\limsup}\frac{1}{n}\underset{k=0}{\overset{n-1}{\sum}}\hat{\pi}_{\star}(c_{k}c_{k+1})>\alpha$

where the indices are taken in $\mathbb{Z}/|c|\mathbb{Z}$, i.e.:

$\underset{n\to\infty}{\lim}\frac{1}{n}\underset{k=0}{\overset{n-1}{\sum}}\hat{\pi}_{\star}(c_{k}c_{k+1})>\alpha,$

and therefore:

$\underset{n\to\infty}{\liminf}\frac{1}{n}\underset{k=0}{\overset{n-1}{\sum}}\hat{\pi}_{\star}(c_{k}c_{k+1})>\alpha,$

that is to say:

$\hat{\mu}_{\star}(c^{\omega})>\alpha,$

hence $\hat{\mu}_{\star}(\rho)>\alpha$. ∎

##  Appendix H Proof of Lemma 3

Lemma 3. _Let $G_{\upharpoonright v_{0}}$ be an initialized mean-payoff game,
and let $\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright s_{0}}$ be its concrete
negotiation game for some $\lambda$ and some $i$._

_Then, the value of the game $\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright
s_{0}}$ is given by the formula:_

$\max_{\tau_{\mathbb{C}}\in\mathrm{ML}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda
i}(G)\right)}\leavevmode\nobreak\
\min_{\scriptsize{\begin{matrix}K\in\mathrm{SConn}\left(\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}]\right)\\\ \mathrm{accessible\leavevmode\nobreak\
from\leavevmode\nobreak\ }s_{0}\end{matrix}}}\mathrm{opt}(K),$

_where $\mathrm{opt}(K)$ is the minimal value $\nu_{\mathbb{C}}(\rho)$ for
$\rho$ among the infinite paths in $K$._

  * •

_If $K$ contains a deviation, then Prover can simply choose the simple cycle
of $K$ that minimizes player $i$’s payoff:_

$\mathrm{opt}(K)=\underset{c\in\mathrm{SC}(K)}{\min}\leavevmode\nobreak\
\hat{\mu}_{\star}(c^{\omega}).$

  * •

_If $K$ does not contain a deviation, then Prover must choose a combination of
the simple cycles of $K$ that minimizes player $i$’s payoff while keeping the
non-main dimensions above $0$:_

$\mathrm{opt}(K)=\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\leavevmode\nobreak\
\hat{\mu}(c^{\omega}).$

###### Proof.

By Lemma 2, there exists a memoryless strategy $\tau_{\mathbb{C}}$ which is
optimal for Challenger among all his possible strategies.

It follows from Theorem 3 that the highest value player $i$ can get against a
hostile $\lambda$-rational environment is the minimal payoff of Challenger in
a path in the graph $\mathrm{Conc}_{\lambda i}(G)[\tau_{\mathbb{C}}]$. For any
such path $\rho$, there exists a strongly connected component $K$ of
$\mathrm{Conc}_{\lambda i}(G)[\tau_{\mathbb{C}}]$ accessible from $s_{0}$ such
that after a finite number of steps, $\rho$ is a path in $K$. The least payoff
of Challenger in such a path, for a given $K$, is $\mathrm{opt}(K)$; let us
prove that it is given by the desired formula.

There are, then, two cases to distinguish:

  * •

_If there is at least one deviation in $K$._

Then, for every play $\rho$ in $K$, it is possible to transform $\rho$ into a
play $\rho^{\prime}$ with $\hat{\mu}(\rho^{\prime})=\hat{\mu}(\rho)$, which
contains infinitely many deviations: it suffices to add round trips to a
deviation, endlessly, but less and less often. Therefore, the outcomes
$\nu_{\mathbb{C}}(\rho)$ of plays in $K$ are exactly the mean-payoffs
$\hat{\mu}_{\star}(\rho)$ of plays in $K$, and possibly $+\infty$; and in
particular, the lowest outcome Prover can get in $K$ is the quantity:

$\underset{c\in\mathrm{SC}(K)}{\min}\leavevmode\nobreak\
\hat{\mu}_{\star}(c^{\omega}),$

the least value of a simple cycle in $K$.

  * •

_If there is no deviation in $K$._

Let us first introduce a notation: for any finite set $D$ and any set
$X\subseteq\mathbb{R}^{D}$, $X^{\llcorner}$ denotes the set:

$X^{\llcorner}=\left\\{\left.\left(\min_{\bar{y}\in Y}y_{d}\right)_{d\in
D}\leavevmode\nobreak\ \right|\leavevmode\nobreak\ Y\subseteq
X\mathrm{\leavevmode\nobreak\ finite}\right\\}.$

For example, in $\mathbb{R}^{2}$, if $X$ is the blue area in Figure 5, then
$X^{\llcorner}$ is the union of the blue area and the gray area.

$x$$y$ Figure 5: An example for the operator $\cdot^{\llcorner}$

Let us already note that for all $X\in\mathbb{R}^{\Pi\cup\\{\star\\}}$,

$\begin{matrix}&\min\\!^{\star}X^{\llcorner}\\\
=&\min\left\\{x_{\star}\leavevmode\nobreak\ \left|\leavevmode\nobreak\
\begin{matrix}\bar{x}\in X^{\llcorner},\\\ \forall j\in\Pi,x_{j}\geq
0\end{matrix}\right.\right\\}\\\ =&\min\left\\{\underset{\bar{y}\in
Y}{\min}\leavevmode\nobreak\ y_{\star}\leavevmode\nobreak\
\left|\leavevmode\nobreak\ \begin{matrix}Y\subseteq
X\mathrm{\leavevmode\nobreak\ finite},\\\ \forall\bar{y}\in Y,\forall
j\in\Pi,y_{j}\geq 0\end{matrix}\right.\right\\}\\\
=&\min\left\\{y_{\star}\leavevmode\nobreak\ \left|\leavevmode\nobreak\
\begin{matrix}\bar{y}\in X,\\\ \forall\bar{y}\in Y,\forall j\in\Pi,y_{j}\geq
0\end{matrix}\right.\right\\}\\\ =&\min\\!^{\star}X.\end{matrix}$

Then, it has been proved in [10] that the set of possible values of
$\hat{\mu}(\rho)$ for all plays $\rho$ in $K$ is exactly the set:

$X=\left(\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})\right)^{\llcorner}.$

Since all the plays in $K$ contain finitely many deviations (actually none),
for every $\bar{x}=\hat{\mu}(\rho)\in X$, we have
$\nu_{\mathbb{C}}(\rho)=+\infty$ if and only if there exists $j\in\Pi$ such
that $x_{j}<0$. Then, the lowest outcome Prover can get in $K$ is:

$\min\left\\{x_{\star}\leavevmode\nobreak\ |\leavevmode\nobreak\ \bar{x}\in
X,\forall j\in\Pi,x_{j}\geq 0\right\\},$

that is to say:

$\min\\!^{\star}\left(\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})\right)^{\llcorner},$

i.e.
$\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})$.

Theorem 3 enables to conclude to the desired formula. ∎

##  Appendix I The negotiation sequence

We assume in that appendix that $G$ is a game on which the negotiation
function is _Scott-continuous_ , i.e. such that for every non-decreasing
sequence $(\lambda_{n})_{n}$ of requirements on $G$, we have:

$\mathrm{nego}\left(\sup_{n}\lambda_{n}\right)=\sup_{n}\mathrm{nego}(\lambda_{n}).$

By Kleene-Tarski fixed-point theorem, the least fixed point of the negotiation
function is, then, the limit of the _negotiation sequence_ , defined as the
sequence
$(\lambda_{n})_{n\in\mathbb{N}}=(\mathrm{nego}^{n}(\lambda_{0}))_{n}$.

In mean-payoff games, in particular, the hypothesis made above is true:

######  Proposition 3.

In mean-payoff games, the negotiation function is Scott-continuous.

A proof of that statement is given in Appendix J.

In many cases, the negotiation sequence is stationary, and in such a case, it
is possible to compute its limit: whenever a term is equal to the previous
one, we know that we reached it. But actually, the negotiation sequence is not
always stationary. The game of Figure 6 is a counter-example. Indeed, for all
$n$, we have:

$\lambda_{n}(a)=\lambda_{n}(b)=2-\frac{1}{2^{n-1}},$

which converges to $2$ but never reaches it.

$c$$d$$a$$b$$e$$f$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{2}}\stackrel{{\scriptstyle\Diamond}}{{0}}$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{0}}\stackrel{{\scriptstyle\Box}}{{1}}\stackrel{{\scriptstyle\Diamond}}{{0}}$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{2}}\stackrel{{\scriptstyle\Diamond}}{{0}}$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{1}}\stackrel{{\scriptstyle\Box}}{{0}}\stackrel{{\scriptstyle\Diamond}}{{0}}$$\stackrel{{\scriptstyle{\scriptsize{\Circle}}}}{{2}}\stackrel{{\scriptstyle\Box}}{{2}}\stackrel{{\scriptstyle\Diamond}}{{0}}$
Figure 6: A game where the negotiation sequence is not stationary

Let us give some details. Since all the $\Diamond$ weights are equal to $0$,
for all $n>0$, we have $\lambda_{n}(d)=\lambda_{n}(f)=0$. It comes that for
all $n>0$, we also have $\lambda_{n}(c)=\lambda_{n}(e)=0$. Moreover, by
symmetry of the game, we always have $\lambda_{n}(a)=\lambda_{n}(b)$.
Therefore, to compute the negotiation sequence, it suffices to compute
$\lambda_{n+1}(a)$ as a function of $\lambda_{n}(b)$, knowing that
$\lambda_{1}(a)=\lambda_{1}(b)=1$, and therefore that for all $n>0$,
$\lambda_{n}(a)=\lambda_{n}(b)\geq 1$.

From $a$, the worst play that player $\Box$ could propose to player $\Circle$
would be a combination of the cycles $cd$ and $d$ giving her exactly $1$. But
then, player $\Circle$ will deviate to go to $b$, from which if player $\Box$
proposes plays in the strongly connected component containing $c$ and $d$,
then player $\Circle$ will always deviate and generate the play
$(ab)^{\omega}$, and then get the payoff $2$.

Then, in order to give her a payoff lower than $2$, player $\Box$ has to go to
the state $e$. Since player $\Circle$ does not control any state in that
strongly connected component, the play he will propose will be accepted: he
will, then, propose the worst possible combination of the cycles $ef$ and $f$
for player $\Circle$, such that he gets at least his requirement
$\lambda_{n}(b)$. The payoff $\lambda_{n+1}(a)$ is then the minimal solution
of the system:

$\left\\{\begin{matrix}\lambda_{n+1}(a)=x+2(1-x)\\\
2(1-x)\geq\lambda_{n}(b)\\\ 0\leq x\leq 1\end{matrix}\right.$

that is to say
$\lambda_{n+1}(a)=1+\frac{\lambda_{n}(b)}{2}=1+\frac{\lambda_{n}(a)}{2}$, and
by induction, for all $n>0$:

$\lambda_{n}(a)=\lambda_{n}(b)=2-\frac{1}{2^{n-1}}.$

##  Appendix J Proof of Proposition 3

Proposition 3. _In mean-payoff games, the negotiation function is Scott-
continuous._

###### Proof.

Let $(\lambda_{n})_{n}$ be a non-decreasing sequence of requirements on a
mean-payoff game $G$, and let $\lambda=\sup_{n}\lambda_{n}$. We want to prove
that $\mathrm{nego}(\lambda)=\sup_{n}\mathrm{nego}(\lambda_{n})$.

Since the negotiation function is monotone, we already have
$\mathrm{nego}(\lambda)\geq\sup_{n}\mathrm{nego}(\lambda_{n})$. Let us prove
that $\mathrm{nego}(\lambda)\leq\sup_{n}\mathrm{nego}(\lambda_{n})$.

Let $\delta>0$: we want to find $n$ such that
$\mathrm{nego}(\lambda_{n})(v)\geq\mathrm{nego}(\lambda)(v)-\delta$ for each
$v\in V$.

Let:

$\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright
s_{0}}=\left(\\{\mathbb{P},\mathbb{C}\\},S,(S_{\mathbb{P}},S_{\mathbb{C}}),\Delta,\nu\right)_{\upharpoonright
s_{0}}$

be the concrete negotiation game of $G$ for $\lambda$ and player $i$
controlling $v$, and let:

$\mathrm{Conc}_{\lambda_{n}i}(G)_{\upharpoonright
s_{0}}=\left(\\{\mathbb{P},\mathbb{C}\\},S,(S_{\mathbb{P}},S_{\mathbb{C}}),\Delta,\nu^{\prime}\right)_{\upharpoonright
s_{0}}$

be the concrete negotiation game of $G$ for some requirement $\lambda_{n}$ in
$v$. Let us note that both have the same underlying graph, and that the only
difference are the weight functions $\hat{\pi}$ and $\hat{\pi}^{\prime}$, on
the non-main dimensions.

By Lemma 3, we have:

$\mathrm{nego}(\lambda)(v)=\max_{\tau_{\mathbb{C}}\in\mathrm{ML}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda
i}(G)_{\upharpoonright s_{0}}\right)}\leavevmode\nobreak\
\min_{\scriptsize{\begin{matrix}K\in\mathrm{SConn}\left(\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}]\right)\\\ \mathrm{accessible\leavevmode\nobreak\
from\leavevmode\nobreak\ }s_{0}\end{matrix}}}\mathrm{opt}(K)$

with:

$\mathrm{opt}(K)=\left\\{\begin{matrix}\mathrm{if\leavevmode\nobreak\
}K\mathrm{\leavevmode\nobreak\ contains\leavevmode\nobreak\
a\leavevmode\nobreak\ deviation}:\\\
\underset{c\in\mathrm{SC}(K)}{\min}\leavevmode\nobreak\
\hat{\mu}_{\star}(c^{\omega})\\\\[14.22636pt] \mathrm{otherwise}:\\\
\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\leavevmode\nobreak\
\hat{\mu}(c^{\omega}),\end{matrix}\right.$

and identically:

$\mathrm{nego}(\lambda_{n})(v)=\max_{\tau_{\mathbb{C}}\in\mathrm{ML}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda_{n}i}(G)_{\upharpoonright
s_{0}}\right)}\leavevmode\nobreak\
\min_{\scriptsize{\begin{matrix}K\in\mathrm{SConn}\left(\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}]\right)\\\ \mathrm{accessible\leavevmode\nobreak\
from\leavevmode\nobreak\ }s_{0}\end{matrix}}}\mathrm{opt}^{\prime}(K)$

with:

$\mathrm{opt}^{\prime}(K)=\left\\{\begin{matrix}\mathrm{if\leavevmode\nobreak\
}K\mathrm{\leavevmode\nobreak\ contains\leavevmode\nobreak\
a\leavevmode\nobreak\ deviation}:\\\
\underset{c\in\mathrm{SC}(K)}{\min}\leavevmode\nobreak\
\hat{\mu}_{\star}(c^{\omega})\\\\[14.22636pt] \mathrm{otherwise}:\\\
\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\leavevmode\nobreak\
\hat{\mu}^{\prime}(c^{\omega}).\end{matrix}\right.$

Let $\tau_{\mathbb{C}}$ be a memoryless strategy for Challenger in the game
$\mathrm{Conc}_{\lambda i}(G)_{\upharpoonright s_{0}}$; it can also be
considered as a memoryless strategy in the game
$\mathrm{Conc}_{\lambda_{n}i}(G)_{\upharpoonright s_{0}}$.

Let us now define:

$\gamma_{n}=\sup_{v\in V}(\lambda(v)-\lambda_{n}(v)).$

Then, the sequence $(\gamma_{n})_{n}$ is non-increasing and converges to $0$.
Moreover, for each transition $st\in\Delta$, we have:

$\hat{\pi}^{\prime}_{j}(st)\in[\hat{\pi}_{j}(st)-\gamma_{n},\hat{\pi}_{j}(st)].$

Let:

$\Gamma_{n}=\left\\{\left.\bar{x}\in\mathbb{R}^{\Pi\cup\\{\star\\}}\leavevmode\nobreak\
\right|\leavevmode\nobreak\ x_{\star}=0\mathrm{\leavevmode\nobreak\
and\leavevmode\nobreak\ }\forall j\in\Pi,x_{j}\in[0,\gamma_{n}]\right\\}.$

Then, let $K$ be a strongly connected component of the graph
$\mathrm{Conc}_{\lambda i}(G)[\tau_{\mathbb{C}}]$, without deviation,
accessible from $s_{0}$; we have:

$\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}^{\prime}(c^{\omega})\subseteq\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})+\Gamma_{n}.$

Let
$R=\left\\{\left.\bar{x}\in\mathbb{R}^{\Pi\cup\\{\star\\}}\leavevmode\nobreak\
\right|\leavevmode\nobreak\ \forall j\in\Pi,x_{j}\geq 0\right\\}$.

  * •

If $\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})\cap
R=\emptyset$, since
$\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})$ and $R$
are closed sets, if $\gamma_{n}$ is small enough, we have
$\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}^{\prime}(c^{\omega})\cap
R=\emptyset$. Therefore, if:

$\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})=+\infty,$

then, for $n$ great enough:

$\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}^{\prime}(c^{\omega})=+\infty.$

  * •

Otherwise, we have:

$\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}^{\prime}(c^{\omega})\geq\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})-\gamma_{n}\max_{\tiny\begin{matrix}c\in\mathrm{SC}(K)\\\
d\in\mathrm{SC}(K)\end{matrix}}\sum_{\tiny\begin{matrix}j\in\Pi,\\\
\hat{\mu}_{j}(c^{\omega})>\\\
\hat{\mu}_{j}(d^{\omega})\end{matrix}}\frac{\hat{\mu}_{\star}(c^{\omega})-\hat{\mu}_{\star}(d^{\omega})}{\hat{\mu}_{j}(c^{\omega})-\hat{\mu}_{j}(d^{\omega})}$

and if $\gamma_{n}$ is small enough, we have:

$\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}^{\prime}(c^{\omega})\geq\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})-\delta.$

In both cases, we find that there exists $\gamma_{n}$ small enough, i.e. $n$
great enough, to ensure:

$\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}^{\prime}(c^{\omega})\geq\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\hat{\mu}(c^{\omega})-\delta.$

We can find such $n$ for each strongly connected component $K$ without
deviation, and there exists a finite number of such components. Moreover, when
$K$ is a strongly connected component with a deviation, the quantity:

$\underset{c\in\mathrm{SC}(K)}{\min}\leavevmode\nobreak\
\hat{\mu}_{\star}(c^{\omega})$

is the same in $\mathrm{Conc}_{\lambda i}(G)$ and in
$\mathrm{Conc}_{\lambda_{n}i}(G)$. Therefore, there exists $n\in\mathbb{N}$
such that:

$\min_{\scriptsize{\begin{matrix}K\in\mathrm{SConn}\left(\mathrm{Conc}_{\lambda_{n}i}(G)[\tau_{\mathbb{C}}]\right)\\\
\mathrm{accessible\leavevmode\nobreak\ from\leavevmode\nobreak\
}s_{0}\end{matrix}}}\leavevmode\nobreak\
\mathrm{opt}(K)\geq\min_{\scriptsize{\begin{matrix}K\in\mathrm{SConn}\left(\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}]\right)\\\ \mathrm{accessible\leavevmode\nobreak\
from\leavevmode\nobreak\ }s_{0}\end{matrix}}}\leavevmode\nobreak\
\mathrm{opt}(K)-\delta.$

We find such $n$ for every memoryless strategy $\tau_{\mathbb{C}}$, and there
exists a finite number of such strategies. Therefore, there exists
$n\in\mathbb{N}$ such that:

$\mathrm{nego}(\lambda_{n})(v)\geq\mathrm{nego}(\lambda)(v)-\delta.$

Finally, since there are finitely many states $v\in V$, we can conclude to the
existence of $n\in\mathbb{N}$ such that for each $v\in V$, we have:

$\mathrm{nego}(\lambda_{n})(v)\geq\mathrm{nego}(\lambda)(v)-\delta.$

The negotiation function is Scott-continuous. ∎

##  Appendix K Proof of Theorem 4

Theorem 4. _Let $G$ be a mean-payoff game. Let us assimilate any requirement
$\lambda$ on $G$ with finite values to the tuple
$\lambda\mspace{-10.0mu}\bar{\phantom{v}}=(\lambda(v))_{v\in V}$, element of
the vector space of finite dimension $\mathbb{R}^{V}$. Then, for each player
$i$ and every vertex $v_{0}\in V_{i}$, the quantity
$\mathrm{nego}(\lambda)(v_{0})$ is a piecewise linear function of
$\lambda\mspace{-10.0mu}\bar{\phantom{v}}$, and an effective expression of
that function can be computed in time double exponential in the size of $G$._

###### Proof.

By Lemma 3, we have the formula:

$\mathrm{nego}(\lambda)(v_{0})=\max_{\tiny{\tau_{\mathbb{C}}\in\mathrm{ML}_{\mathbb{C}}\left(\mathrm{Conc}_{\lambda
i}(G)\right)}}\leavevmode\nobreak\
\min_{\tiny{\begin{matrix}K\in\mathrm{SConn}(\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}])\\\ \mathrm{accessible\leavevmode\nobreak\
from\leavevmode\nobreak\ }(v_{0},\\{v_{0}\\})\end{matrix}}}\mathrm{opt}(K).$

Let $\tau_{\mathbb{C}}$ be a memoryless strategy of Challenger, and let $K$ be
a strongly connected component of the graph $\mathrm{Conc}_{\lambda
i}(G)[\tau_{\mathbb{C}}]$. Let us prove that the quantity:

$\mathrm{opt}(K)=\left\\{\begin{matrix}\mathrm{if\leavevmode\nobreak\
}K\mathrm{\leavevmode\nobreak\ contains\leavevmode\nobreak\
a\leavevmode\nobreak\
dev.}:&\underset{c\in\mathrm{SC}(K)}{\min}\leavevmode\nobreak\
\hat{\mu}_{\star}(c^{\omega})\\\
\mathrm{otherwise}:&\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\leavevmode\nobreak\
\hat{\mu}(c^{\omega})\end{matrix}\right.$

is a piecewise linear function of $\lambda\mspace{-10.0mu}\bar{\phantom{v}}$.

When $K$ contains a deviation, the quantity:

$\underset{c\in\mathrm{SC}(K)}{\min}\leavevmode\nobreak\
\hat{\mu}_{\star}(c^{\omega})$

is independent of $\lambda$, and the result is then immediate. Let us now
study the case where $K$ does not contain any deviation, i.e. let us prove
that the quantity:

$f(\lambda)=\min\\!^{\star}\underset{c\in\mathrm{SC}(K)}{\mathrm{Conv}}\leavevmode\nobreak\
\hat{\mu}(c^{\omega})$

is a piecewise linear function of $\lambda$.

Let $M$ be the common memory of the states of $K$ (since $K$ does not contain
deviations). We know that for each $j\in\Pi$ and for every cycle
$c\in\mathrm{SC}(K)$, we have:

$\hat{\mu}_{j}(c^{\omega})=\mu_{j}(\dot{c}^{\omega})-\max_{v\in V_{j}\cap
M}\lambda(v).$

Let $C=\left\\{\dot{c}\leavevmode\nobreak\ |\leavevmode\nobreak\
c\in\mathrm{SC}(K)\right\\}$. Since there is no deviation in $K$, any cycle in
$C$ is a simple cycle of $G$. Then, the quantity $f(\lambda)$ is the minimal
$x_{i}$ for $\bar{x}$ in the set:

$X=\underset{c\in C}{\mathrm{Conv}}\leavevmode\nobreak\
\mu(c^{\omega})\cap\bigcap_{v\in M}\left\\{\bar{x}\leavevmode\nobreak\