In game theory, mechanism design is concerned with the design of
incentives so that a desired outcome of the game can be achieved. In this
paper, we study the design of incentives so that a desirable equilibrium is
obtained, for instance, an equilibrium satisfying a given temporal logic
property—a problem that we call equilibrium design. We base our study
on a framework where system specifications are represented as temporal logic
formulae, games as quantitative concurrent game structures, and players' goals
as mean-payoff objectives. In particular, we consider system specifications
given by LTL and GR(1) formulae, and show that implementing a mechanism to
ensure that a given temporal logic property is satisfied on some/every Nash
equilibrium of the game, whenever such a mechanism exists, can be done in
PSPACE for LTL properties and in NP/$\SigmaPTwo$ for GR(1) specifications. We
also study the complexity of various related decision and optimisation
problems, such as optimality and uniqueness of solutions, and show that the
complexities of all such problems lie within the polynomial hierarchy. As an
application, equilibrium design can be used as an alternative solution to the
rational synthesis and verification problems for concurrent games with
mean-payoff objectives whenever no solution exists, or as a technique to
repair, whenever possible, concurrent games with undesirable rational outcomes
(Nash equilibria) in an optimal way.

§ INTRODUCTION

Over the past decade, there has been increasing interest in the use of
game-theoretic equilibrium concepts such as Nash equilibrium in the
analysis of concurrent and multi-agent systems (see,
e.g., [3, 4, 8, 14, 16, 18, 24]).
This work views a concurrent system as a game, with system components
(agents) corresponding to players in the game, which are assumed to be
acting rationally in pursuit of their individual
preferences. Preferences may be specified by associating with each
player a temporal logic goal formula, which the player desires to see
satisfied, or by assuming that players receive rewards in each state
the system visits, and seek to maximise the average reward they
receive (the mean payoff). A further possibility is to combine
goals and rewards: players primarily seek the satisfaction of their
goal, and only secondarily seek to maximise their mean payoff. The key
decision problems in such settings relate to what temporal logic
properties hold on computations of the system that may be generated by
players choosing strategies that form a game-theoretic (Nash)
equilibrium. These problems are typically computationally complex,
since they subsume temporal logic synthesis [34]. If
players have goals, for example, then checking whether an formula holds on some Nash equilibrium path in a concurrent game is
2EXPTIME-complete [14, 17, 18],
rather than only PSPACE-complete as it is the case for model checking,
certainly a computational barrier for the practical analysis and automated
verification of reactive, concurrent, and multi-agent systems modelled as
multi-player games.

Within this game-theoretic reasoning framework, a key issue
is that individually rational choices can
cause outcomes that are highly undesirable, and concurrent games also
fall prey to this problem. This has motivated the development of
techniques for modifying games, in order to avoid bad equilibria, or
to facilitate good equilibria. Mechanism design is the problem of
designing a game such that, if players behave rationally, then a
desired outcome will be obtained [27]. Taxation and subsidy
schemes are probably the most important class of techniques used in
mechanism design. They work by levying taxes on certain actions (or
providing subsidies), thereby incentivising
players away from some outcomes towards others. The present paper
studies the design of subsidy schemes (incentives) for concurrent games,
so that a desired outcome (a Nash equilibrium in the game) can be obtained—a
problem that we call Equilibrium design.

We model agents as synchronously executing concurrent processes, with
each agent receiving an integer payoff for every state the overall system visits;
the overall payoff an agent receives over an infinite computation path
is then defined to be the mean payoff over this path. While agents (naturally) seek to maximise their individual mean payoff, the designer of the subsidy scheme wishes to see some temporal logic formula satisfied, either
on some or on every Nash equilibrium of the game.

With this model, we assume that the designer – an external principal – has a
finite budget that is available for making subsidies, and this budget can be
allocated across agent/state pairs. By allocating this budget
appropriately, the principal can incentivise players away from some
states and towards others. Since the principal has some temporal
logic goal formula, it desires to allocate subsidies so that players
are rationally incentivised to choose strategies so that the
principal's temporal logic goal formula is satisfied in the path that would result from
executing the strategies.  For this general problem,
following [25], we identify two variants of the principal's
mechanism design problem, which we refer to as Weak
Implementation and Strong Implementation. In the
Weak variant, we ask whether the principal can allocate the
budget so that the goal is achieved on some computation path that would be
generated by Nash equilibrium strategies in the resulting system; in
the Strong variation, we ask whether the principal can
allocate the budget so that the resulting system has at least one Nash
equilibrium, and moreover the temporal logic goal is satisfied on all paths that
could be generated by Nash equilibrium strategies. For these two
problems, we consider goals specified by formulae or
formulae [5], give algorithms for each case, and
classify the complexity of the problem.

While is a natural language for the specification of properties of concurrent
and multi-agent systems, is an fragment that can be used to
easily express several prefix-independent properties of computation paths of reactive systems,
such as $\omega$-regular properties often used in automated formal verification.

We then go on to study
variations of these two problems, for example considering
optimality and uniqueness of solutions, and show that the
complexities of all such problems lie within the polynomial hierarchy, thus
making them potentially amenable to efficient practical implementations.
Table <ref> summarises the main computational complexity results in the paper.

Spec.     Spec.

-complete (Thm. <ref>)     -complete (Thm. <ref>)

-complete (Cor. <ref>)     $ \SigmaPTwo $-complete (Thm. <ref>)

-complete (Thm. <ref>)     $ \FP^{\np} $-complete (Thm. <ref>)

-complete (Thm. <ref>)     $ \FP^{\SigmaPTwo} $-complete (Thm. <ref>)

-complete (Cor. <ref>)     $ \DP $-complete (Cor. <ref>)

-complete (Cor. <ref>)     $ \DPTwo $-complete (Cor. <ref>)

-complete (Cor. <ref>)     $ \DeltaPTwo $-complete (Cor. <ref>)

-complete (Cor. <ref>)     $ \DeltaPThree $-complete (Cor. <ref>)

Summary of main complexity results.

§ PRELIMINARIES

Linear Temporal Logic.
[33] extends classical propositional logic with two
operators, $\ltlnext$ (“next”) and $\until$ (“until”), that can be used to express properties of paths.  The syntax of is defined
with respect to a set $\AP$ of atomic propositions as follows:

$$ \phi ::=
\mathop\top \mid
p \mid
\neg \phi \mid\phi \vee \phi \mid
\ltlnext \phi \mid
\phi \until \phi

where $p \in \AP$.
As commonly found in the literature, we  use of the following abbreviations: $\phi_1 \wedge \phi_2 \equiv \neg (\neg \phi_1 \vee \neg \phi_2)$, $\phi_1 \to \phi_2 \equiv \neg \phi_1 \vee \phi_2$, $\sometime \phi \equiv \mathop\top \until \phi$, and $\always \phi \equiv \neg \sometime \neg \phi$.
We interpret formulae of with respect to pairs $(\alpha,t)$, where $\alpha \in (2^{\AP})^\omega$ is an infinite sequence of atomic proposition evaluations that indicates which propositional variables are true in every time point and $t \in \Nat$ is a
temporal index into $\alpha$.
Formally, the semantics of formulae is given by the following rules:

\begin{array}{lcl}
(\alpha,t)\models\mathop\top	\\
(\alpha,t)\models p 				&\text{ iff }&	p\in \alpha_t\\
(\alpha,t)\models\neg \phi			&\text{ iff }&   \text{it is not the case that $(\alpha,t) \models \phi$}\\
(\alpha,t)\models\phi \vee \psi		&\text{ iff }&	\text{$(\alpha,t) \models \phi$  or $(\alpha,t) \models \psi$}\\
(\alpha,t)\models\ltlnext\phi			&\text{ iff }&	\text{$(\alpha,t+1) \models \phi$}\\
(\alpha,t)\models\phi\until\psi	&\text{ iff }&   \text{for some $t' \geq t: \ \big((\alpha,t') \models \psi$  and }\\
&&\quad\text{for all $t \leq t'' < t': \ (\alpha,t'') \models \phi \big)$.}\\
\end{array}

If $(\alpha,0)\models\phi$, we write $\alpha\models\phi$ and say that
$\alpha$ satisfies $\phi$.

General Reactivity of rank 1.
The language of General Reactivity of rank 1, denoted $\GRone$, is the fragment of given by  formulae written in the following form [5]:

(\always \sometime \psi_1 \wedge \ldots \wedge \always \sometime \psi_m) \to (\always \sometime \phi_1 \wedge \ldots \wedge \always \sometime \phi_n)
\text{,}

where each subformula $\psi_i$ and $\phi_i$ is a Boolean combination of atomic propositions.

For a sequence $r \in \mathbb{R}^\omega$, let $\MP(r)$ be
the mean-payoff value of $r$, that is,

$$ \MP(r) = \lim \inf_{n \to \infty} \avg_n(r) $$

where, for $n \in \mathbb{N}\setminus\{0\}$, we define
$\avg_n(r) = \frac{1}{n}\sum_{j=0}^{n-1} r_j$, with $r_j$ the $(j\!+\!1)$th element of $r$.

An arena is a tuple

$ A = \tuple{\Ag,  \Ac, \St, s_0, \trnFun, \labFun} $

where $\Ag$, $\Ac$, and $\St$ are finite non-empty sets of players (write $N = \card{\Ag}$), actions, and states, respectively; if needed, we write $ \Ac_i(s) $, to denote the set of actions available to player $ i $ at $ s $; $s_0 \in \St$ is the initial state; $\trnFun : \St \times \AcProf \rightarrow \St$ is a transition function mapping each pair consisting of a state $s \in \St$ and an action profile $\jact \in \AcProf = \Ac^{\Ag}$, one for each player, to a successor state; and $\labFun: \St \to 2^{\AP}$ is a labelling function, mapping every state to a subset of atomic propositions.

We sometimes call an action profile $\jact = (\act_{1}, \dots, \act_{n}) \in \AcProf$ a decision, and denote $\act_i$ the action taken by player $i$.
We also consider partial decisions.
For a set of players $C \subseteq \Ag$ and action profile $\jact$, we let $\jact_{C}$ and $\jact_{-C}$ be two tuples of actions, respectively, one for all players in $C$ and one for all players in $\Ag \setminus C$.
We also write $\jact_{i}$ for $\jact_{\{i\}}$ and $ \jact_{-i} $ for $ \jact_{\Ag \setminus \{i\}} $.
For two decisions $\jact$ and $\jact'$, we write $(\jact_{C}, \jact_{-C}')$ to denote the decision where the actions for players in $ C $ are taken from $\jact$ and the actions for players in $ \Ag \setminus C $ are taken from $\jact'$.

A path $\pi = (s_0, \jact^0), (s_1, \jact^1) \cdots$ is an infinite sequence in $(\St \times \AcProf)^{\omega}$ such that $\trnFun(s_k, \jact^k) = s_{k + 1}$ for all $k$.

Paths are generated in the arena by each player $i$ selecting a strategy $\strElm_i$ that will define how to make choices over
time.  We model strategies as finite state machines with output.
Formally, for arena $A$, a strategy
$\strElm_{i} = (Q_{i}, q_{i}^{0}, \delta_i, \tau_i) $ for player $i$
is a finite state machine with output (a transducer), where $Q_{i}$ is
a finite and non-empty set of internal states, $ q_{i}^{0} $ is
the initial state,
$\delta_i: Q_{i} \times \AcProf \rightarrow Q_{i} $ is a deterministic
internal transition function, andlet me
$\tau_i: Q_{i} \rightarrow \Ac_i$ an action function. Let $\StrSet_i$ be the set of strategies for player $i$. Note that this definition implies that strategies have perfect information[Mean-payoff games with imperfect information are generally undecidable [13].] and finite memory (although we impose no bounds on memory size).

A strategy profile $\strpElm = (\strElm_1, \dots, \strElm_n)$ is a vector of strategies, one for each player.
As with actions, $\strpElm_{i}$ denotes the strategy assigned to player $i$ in profile $\strpElm$.
Moreover, by $(\strpElm_{B}, \strpElm'_{C})$ we denote the combination
of profiles where players in disjoint $B$ and $C$ are assigned their corresponding strategies in $\strpElm$ and $\strpElm'$, respectively.

Once a state $s$ and profile $\strpElm$ are fixed, the game has an outcome, a path in $A$, denoted by $\pi(\strpElm, s)$.
Because strategies are deterministic, $\pi(\strpElm, s)$ is the unique path induced by $\strpElm$, that is, the sequence $s_0, s_1, s_2, \ldots$ such that

* $s_{k + 1} = \trnFun (s_k, (\tau_1(q^k_1), \ldots, \tau_n(q^k_n)))$, and

* $q^{k + 1}_i = \delta_i(s^k_i, (\tau_1(q^k_1), \ldots, \tau_n(q^k_n)))$, for all $k \geq 0$.

Furthermore, we simply write $ \pi(\strpElm) $ for $ \pi(\strpElm,s_0) $.

Arenas define the dynamic structure of games, but lack a central aspect of a game: preferences, which give games their strategic structure.
A multi-player game is obtained from an arena $A$ by
associating each player with a goal.
We consider multi-player games with $\MP$ goals.

A multi-player game is a tuple
$\Game = \tuple{A, (\wFun_{i})_{i \in \Ag}}$, where $A$ is an
arena and $\wFun_{i}: \St \to \SetZ$ is a function mapping, for every player $i$, every state
of the arena into an integer number.

In any game with arena $A$, a path $\pi$ in $A$ induces a sequence $\lambda(\pi) = \lambda(s_0) \lambda(s_1) \cdots$ of sets of atomic propositions; if, in addition, $A$ is the arena of an game, then, for each player $i$, the sequence $\wFun_i(\pi) = \wFun_i(s_0) \wFun_i(s_1) \cdots$ of weights is also induced.

Unless stated otherwise, for a game $ \Game $ and a path $\pi$ in it, the payoff of player $i$ is $\pay_i(\pi) = \MP(\wFun_{i}(\pi))$.

Nash equilibrium.
Using payoff functions, we can define the game-theoretic concept of Nash equilibrium [27].
For a multi-player game $\Game$, a strategy profile
$\strpElm$ is a Nash equilibrium of $\Game$ if, for every player $i$ and strategy $\strElm'_i$ for player $i$, we have

\pay_i(\pi(\strpElm))	\geq	\pay_i(\pi((\strpElm_{-i},\strElm'_i))) \ .

Let $\NE(\Game)$ be the set of Nash equilibria of $\Game$.

§ FROM MECHANISM DESIGN TO EQUILIBRIUM DESIGN

We now describe the two main problems that are our focus of study. As discussed in the introduction, such problems are closely related to the well-known problem of mechanism design in game theory.

Consider a system populated by agents ,
where each agent $ i \in \Ag $ wants to maximise its payoff $ \pay_i(\cdot) $.
As in a mechanism design problem, we assume there is an external principal who has a goal $ \phi $ that it
wants the system to satisfy, and to this end, wants to incentivise the agents to act collectively and rationally so as to bring about $ \phi $. In our
model, incentives are given by subsidy schemes and goals by temporal logic formulae.

Subsidy Schemes: A subsidy scheme defines additional
imposed rewards over those given by the weight function $ \wFun $.
While the weight function $ \wFun$ is fixed for any
given game, the principal is assumed to be at liberty to define a subsidy
scheme as they see fit. Since agents will seek to maximise their overall rewards,
the principal can incentivise agents away from performing visiting some states and
towards visiting others; if the principal designs the subsidy scheme
correctly, the agents are incentivised to choose a strategy profile $ \vec{\sigma} $
such that $ \pi(\strpElm) \models \phi $.

Formally, we model a subsidy scheme as a function $ \kappa: \Ag \to \St \to \mathbb{N} $, where the intended
interpretation is that $ \kappa(i)(s) $ is the subsidy in the form of a natural number $ k \in \mathbb{N}$ that would be imposed on player $ i $ if such a player visits state $ s \in \St $. For instance, if we have $ \wFun_{i}(s) = 1 $ and $ \kappa(i)(s) = 2 $, then player $i$ gets $1 + 2 = 3 $ for visiting such a state. For simplicity, hereafter we write $ \kappa_i(s) $ instead of $ \kappa(i)(s)$ for the subsidy for player $i$.

Notice that having an unlimited fund for a subsidy scheme would make some problems trivial, as the principal can always incentivise players to satisfy $ \phi $ (provided that there is a path in $ A $ satisfying $ \phi $). A natural and more interesting setting is that the principal is given a constraint in the form of budget $\beta\in\mathbb{N}$. The principal then can only spend within the budget limit. To make this clearer, we first define the cost of a subsidy scheme $ \kappa $ as follows.

Given a game $ \Game $ and subsidy scheme $ \kappa $, we let $ \cost(\kappa) = \sum_{i \in \Ag} \sum_{s \in \St} \kappa_i(s) $.

We say that a subsidy scheme $ \kappa $ is admissible if it does not exceed the budget $\beta$,  that is, if $ \cost(\kappa) \leq \beta $. Let $ \K(\Game,\beta) $ denote the set of admissible subsidy schemes over $ \Game $ given budget $ \beta \in \mathbb{N} $. Thus we know that for each $ \kappa \in \K(\Game,\beta)$ we have $\cost(\kappa) \leq \beta $. We write $ (\Game,\kappa) $ to denote the resulting game after the application of subsidy scheme $ \kappa $ on game $ \Game $. Formally, we define the application of some subsidy scheme on a game as follows.

Given a game $ \Game = \tuple{A,(\wFun_{i})_{i \in \Ag}} $ and an admissible subsidy scheme $ \kappa $, we define $ (\Game,\kappa) = \tuple{A, (\wFun'_{i})_{i \in \Ag}} $, where $ \wFun'_{i}(s) = \wFun_{i}(s) + \kappa_i(s)$, for each $ i \in \Ag $ and $ s \in \St $.

We now come to the main question(s) that we consider in the remainder of the paper. We ask whether the principal can find a subsidy scheme that will incentivise players to collectively choose a rational outcome (a Nash equilibrium) that satisfies its temporal logic goal $ \phi $. We call this problem equilibrium design. Following [25], we define two variants of this problem, a weak and a strong implementation of the equilibrium design problem. The formal definition of the problems and the analysis of their respective computational complexity are presented in the next sections.

§ EQUILIBRIUM DESIGN: WEAK IMPLEMENTATION

In this section, we study the weak implementation of the equilibrium design problem, a logic-based computational variant of the principal's mechanism design problem in game theory. We assume that the principal has full knowledge of the game $ \Game $ under consideration, that is, the principal uses all the information available of $ \Game $ to find the appropriate subsidy scheme, if such a scheme exists. We now formally define the weak variant of the implementation problem, and study its respective computational complexity, first with respect to goals (specifications) given by formulae and then with respect to formulae.

Let $ \WI(\Game,\phi,\beta) $ denote the set of subsidy schemes over $ \Game $ given budget $ \beta $ that satisfy a formula $ \phi $ in at least one path $ \pi $ generated by $ \strpElm \in \NE(\Game) $. Formally

$$ \WI(\Game,\phi,\beta) = \{ \kappa \in \K(\Game,\beta) : \exists \strpElm \in \NE(\Game,\kappa)~\textrm{s.t.}~\pi(\strpElm) \models \phi \}. $$

Given a game $\Game$, formula $\varphi$, and budget $ \beta $:

Is it the case that $ \WI(\Game,\phi,\beta) \neq \varnothing $?

In order to solve , we first characterise the Nash equilibria of a multi-player concurrent game in terms of punishment strategies. To do this in our setting, we recall the notion of secure values for mean-payoff games [36].

For a player $i$ and a state $s \in \St$, by $\pun_i(s)$ we denote the
punishment value of $i$ over $s$, that is, the maximum payoff that $i$
can achieve from $s$, when all other players behave adversarially.
Such a value can be computed by considering the corresponding
two-player zero-sum mean-payoff game [38].  Thus, it is in
$\np \cap \mathsf{co}\np$, and note that both player $i$ and coalition
$\Ag \setminus \{i\}$ can achieve the optimal value of the game using
memoryless strategies.

Then, for a player $i$ and a value $z \in \SetR$, a pair $(s, \jact)$ is $z$-secure for player $i$ if $\pun_i(\trnFun(s, (\jact_{-i}, \act'_i))) \leq z$ for every $\act'_i \in \Ac$. Write $\pun_{i}(\Game)$ for the set of punishment values for player $i$ in $\Game$.

For every game $\Game$ and ultimately periodic path $\pi = (s_0, \jact_{0}), (s_1, \jact^{1}), \ldots $, the following are equivalent:

* There is $\strpElm \in \NE(\Game)$ such that $\pi = \pi(\strpElm, s_0)$;

* There exists $ {z} \in \SetR^{\Ag}$, where $z_{i} \in \pun_{i}(\Game)$ such that, for every $i \in \Ag$

* for all $k \in \SetN$, the pair $(s_k, \jact^k)$ is $z_i$-secure for $i$, and

* $z_i \leq \pay_i(\pi)$.

The characterisation of Nash Equilibria provided in Theorem <ref> will allow us to turn the problem into a path finding problem over $(\Game,\kappa)$.

On the other hand, with respect to the budget $\beta$ that the principal has at its disposal, the definition of subsidy scheme function $\kappa$ implies that the size of $ \K(\Game,\beta) $ is bounded, and particularly, it is bounded by $\beta$ and the number of agents and states in the game $\Game$, in the following way.

Given a game $ \Game $ with $\card{N}$ players and $ \card{\St} $ states and budget $\beta$, it holds that

$$ \card{\K(\Game,\beta)} = \frac{\beta + 1}{m} \binom{\beta + m}{\beta + 1}\text{,}$$

with $m = \card{N \times \St}$ being the number of pairs of possible agents and states.

From Proposition <ref> we derive that the number of possible subsidy schemes is polynomial in the budget $\beta$ and singly exponential in both the number of agents and states in the game.

At this point, solving can be done with the following procedure:

* a subsidy scheme $ \kappa \in \K(\Game,\beta) $,

* a state $ s \in \St $ for every player $ i \in \Ag $, and

* punishment memoryless strategies $ (\strpElm_{-1},\dots,\strpElm_{-n}) $ for all players $ i \in \Ag $;

Compute $ (\Game,\kappa) $;

Compute $ z \in \SetR^{\Ag} $;

Compute the game $(\Game,\kappa){[z]}$ by removing the states $s$ such that $\pun_i(s) \leq z_i$ for some player $i$ and the transitions $(s, \jact_{-i})$ that are not $z_i$ secure for player $i$;

Check whether there exists an ultimately periodic path $ \pi $ in $ (\Game,\kappa){[z]}$ such that $ \pi \models \phi $ and $ z_i \leq \pay_i(\pi) $ for every player $ i \in \Ag $.

Since the set $ \K(\Game,\beta) $ is finitely bounded (Proposition <ref>), and punishment strategies only need to be memoryless, thus also finitely bounded, clearly step <ref> can be guessed nondeterministically. Moreover, each of the guessed elements is of polynomial size, thus this step can be done (deterministically) in polynomial space.
Step <ref> clearly can be done in polynomial time.
Step <ref> can also be done in polynomial time since, given $ (\strpElm_{-1},\dots,\strpElm_{-n}) $, we can compute $ z $ solving $|\Ag|$ one-player mean-payoff games, one for each player $ i $ <cit.>. For step <ref>, we will use Theorem <ref> and consider two cases, one for specifications and one for specifications. Firstly, for specifications, consider the formula

\phi_{\WI} := \phi \wedge \bigwedge_{i \in \Ag} (\MP(i) \geq z_i)

written in $\LTLlim$ [7], an extension of where statements about mean-payoff values over a given weighted arena can be made.
[The formal semantics of $\LTLlim$ can be found in  [7]. We prefer to give only an informal description here.]

The semantics of the temporal operators of $\LTLlim$ is just like the one for over infinite computation paths $\pi = s_0,s_1,s_3.\ldots$. On the other hand, the meaning of $\MP(i) \geq z_i$ is simply that such an atomic formula is true if, and only if, the mean-payoff value of $\pi$ with respect to player $i$ is greater or equal to $z_i$, a constant real value; that is, $\MP(i) \geq z_i$ is true in $\pi$ if and only if $\pay_i(\pi) = \MP(\wFun_{i}(\pi))$ is greater or equal than constant value $z_i$.

Formula $ \phi_{\WI} $ corresponds exactly to $ 2(b) $ in Theorem <ref>. Furthermore, since every path in $ (\Game,\kappa){[z]} $ satisfies condition $ 2(a) $ of Theorem <ref>, every computation path of $ (\Game,\kappa){[z]} $ that satisfies $ \phi_{\WI} $ is a witness to the problem.

with specifications is -complete.

Membership follows from the procedure above and the fact that model checking for $\LTLlim$ is -complete [7]. Hardness follows from the fact that model checking is a special case of . For instance, consider the case in which all weights for all players are set to the same value, say 0, and the principal has budget $ \beta = 0 $.

Case with $ \GRone $ specifications.
One of the main bottlenecks of our procedure to solve lies in step <ref>, where we solve an $ \LTLlim $ model checking problem. To reduce the complexity of our decision procedure, we consider with the specification $ \phi $ expressed in the $ \GRone $ sublanguage of . With this specification language, the path finding problem can be solved without model-checking the $ \LTLlim $ formula given before. In order to do this, we can define a linear program () such that the  has a solution if and only if $ \WI(\Game,\phi,\beta) \neq \varnothing $.

From our previous procedure, observe that step <ref> can be done nondeterministically in polynomial time, and steps <ref>–<ref> can be done (deterministically) in polynomial time. Furthermore, using , we also can check step <ref> deterministically in polynomial time.

For the lower-bound, we use [36] and note that if $\phi=\top$ and $ \beta = 0 $, then the problem reduces to checking whether the underlying game has a Nash equilibrium. Based on the above observations, we have the following result.

with $ \GRone $ specifications is -complete.

For the upper bound, we define an  of size polynomial in $(\Game,\kappa)$ having a solution if and only if there is an ultimately periodic path $ \pi $ such that $z_i \leq \pay_i(\pi) $ and satisfies the specification.

Recall that $\phi$ has the following form

\phi = \bigwedge_{l = 1}^{m} \always \sometime \psi_{l} \to \bigwedge_{r = 1}^{n} \always \sometime \theta_{r}\text{,}

and let $V(\psi_{l})$ and $V(\theta_r)$ be the subset of states in $(\Game,\kappa)$ that satisfy the Boolean combinations $\psi_{l}$ and $\theta_{r}$, respectively. Property $\phi$ is satisfied on $\pi$ if, and only if, either $\pi$ visits every state in $V(\theta_r)$ infinitely often or some of the states in $V(\psi_{l})$ only a finite number of times.

For the game $(\Game,\kappa){[z]}$, let $ W = (V, E, (\wFun_a)_{a \in \Ag})$ be the underlying multi-weighted graph, and for every edge $e\in E$ introduce a variable $x_e$. Informally, the value of $x_e$ is the number of times that $e$ is used on a cycle. Formally, let $\src(e) = \{v \in V : \exists w\, e = (v,w) \in E\}$; $\trg(e) = \{v \in V : \exists w\, e = (w,v) \in E\}$; $\OUT(v) = \{e \in E : \src(e) = v\}$; and $\IN(v) = \{e \in E : \trg(e) = v\}$.

Now, consider $\psi_{l}$ for some $1 \leq l \leq m$, and define the following linear program $\LP(\psi_{l})$:

$x_e \geq 0$ for each edge $e$
— a basic consistency criterion;

$\Sigma_{e \in E} x_e \geq 1$
— at least one edge is chosen;

for each $a \in \Ag$, $\Sigma_{e \in E} \wFun_a(\src(e)) x_e \geq 0$ — total sum of any solution is non-negative;

$\Sigma_{\src(e) \cap V(\psi_{l}) \neq \emptyset} x_e = 0$ — no state in $V(\psi_{l})$ is in the cycle associated with the solution;

for each $v \in V$, $\Sigma_{e \in \OUT(v)} x_e = \Sigma_{e \in \IN(v)} x_e$  — this condition says that the number of times one enters a vertex is equal to the number of times one leaves that vertex.

$\LP(\psi_{l})$ has a solution if and only if there is a path $\pi$ in $\Game$ such that $z_i \leq \pay_i(\pi) $ for every player $i$ and visits $V(\psi_{l})$ only finitely many times.

Consider now the linear program $\LP(\theta_{1}, \ldots, \theta_{n})$ defined as follows. Eq1–Eq3 as well as Eq5 are as in $\LP(\psi_{l})$, and:

for all $1 \leq r \leq n$, $\Sigma_{\src(e) \cap V(\theta_{r}) \neq \emptyset} x_e \geq 1$ —  this condition says that, for every $V(\theta_{r})$, at least one state in $V(\theta_{r})$ is in the cycle associated with the solution of the linear program.

In this case, $\LP(\theta_{1}, \ldots, \theta_{n})$  has a solution if and only if there exists a path $\pi$ such that $z_i \leq \pay_i(\pi) $ for every player $i$ and visits every $V(\theta_{r})$ infinitely many times.

Since the constructions above are polynomial in the size of both $(\Game,\kappa)$ and $\phi$, we can conclude it is possible to check in the statement that there is a path $\pi$ satisfying $\varphi$ such that $z_i \leq \pay_i(\pi) $ for every player $i$ in the game if and only if one of the two linear programs defined above has a solution.

For the lower-bound, we use [36] as discussed before.

We now turn our attention to the strong implementation of the equilibrium design problem. As in this section, we first consider specifications and then specifications.

§ EQUILIBRIUM DESIGN: STRONG IMPLEMENTATION

Although the principal may find $ \WI(\Game,\phi,\beta) \neq \varnothing $ to be good news, it might not be good enough. It could be that even though there is a desirable Nash equilibrium, the others might be undesirable. This motivates us to consider the strong implementation variant of equilibrium design. Intuitively, in a strong implementation, we require that every Nash equilibrium outcome satisfies the specification $ \phi $, for a non-empty set of outcomes. Then, let $ \SI(\Game,\phi,\beta) $ denote the set of subsidy schemes $ \kappa $ given budget $ \beta $ over $ \Game $ such that:

* $ (\Game,\kappa) $ has at least one Nash equilibrium outcome,

* every Nash equilibrium outcome of $ (\Game,\kappa) $ satisfies $ \phi $.

Formally we define it as follows:

\SI(\Game,\phi,\beta) = \{ \kappa \in \mathcal{K}(\Game,\beta) : \NE(\Game,\kappa) \neq \varnothing \wedge \forall \strpElm \in \NE(\Game,\kappa)~\textrm{s.t.}~\pi(\strpElm) \models \phi \}.

This gives us the following decision problem:

Given a game $\Game$, formula $\varphi$, and budget $ \beta $:

Is it the case that $ \SI(\Game,\phi,\beta) \neq \varnothing $?

can be solved with a 5-step procedure where the first four steps are as in , and the last step (step 5) is as follows:

Check whether:

* there is no ultimately periodic path $ \pi $ in $ (\Game,\kappa){[z]}$ such that $ z_i \leq \pay_i(\pi) $ for each $ i \in \Ag $;

* there is an ultimately periodic path $ \pi $ in $ (\Game,\kappa){[z]}$ such that $ \pi \models \lnot\phi $ and $ z_i \leq \pay_i(\pi) $, for each $ i \in \Ag $.

For step <ref>, observe that a positive answer to <ref>(a) or <ref>(b) is a counterexample to $ \kappa \in \SI(\Game,\phi,\beta) $. Then, to carry out this procedure for the problem with specifications, consider the following formulae:

\begin{align*}
\phi_{\exists} &= \bigwedge_{i \in \Ag} (\MP(i) \geq z_i);\\
\phi_{\forall} &= \phi_{\exists} \rightarrow \phi.
\end{align*}

Notice that the expression $ \NE(\Game,\kappa) \neq \varnothing $ can be expressed as “there exists a path $ \pi $ in $ \Game $ that satisfies formula $ \phi_{\exists} $”. On the other hand, the expression $ \forall \strpElm \in \NE(\Game,\kappa)~\textrm{such that}~\pi(\strpElm) \models \phi $ can be expressed as “for every path $ \pi $ in $ \Game $, if $\pi$ satisfies formula $ \phi_{\exists} $, then $\pi$ also satisfies formula $ \phi $”. Thus, using these two formulae, we obtain the following result.

with specifications is -complete.

Membership follows from the fact that step <ref>(a) can be solved by existential model checking, whereas step <ref>(b) by universal model checking—both clearly in by Savitch's theorem. Hardness is similar to the construction in Theorem <ref>.

Case with $ \GRone $ specifications.
Notice that the first part, i.e., $ \NE(\Game,\kappa) \neq \varnothing $ can be solved in [36]. For the second part, observe that
$$ \forall \strpElm \in \NE(\Game,\kappa)~\textrm{such that}~\pi(\strpElm) \models \phi $$
is equivalent to
$$ \neg\exists \strpElm \in \NE(\Game,\kappa)~\text{such that}~\pi(\strpElm) \models \lnot \phi. $$

Thus we have

\lnot\varphi = \bigwedge_{l = 1}^{m} \always \sometime \psi_{l} \wedge \lnot \big( \bigwedge_{r = 1}^{n} \always \sometime \theta_{r} \big)\text{.}

To check this, we modify the  in Theorem <ref>. Specifically, we modify Eq4 in $\LP(\theta_{1}, \ldots, \theta_{n})$ to encode the $ \theta $-part of $ \lnot \phi $. Thus, we have the following equation in $\LP'(\theta_{1}, \ldots, \theta_{n})$:

there exists $ r $, $1 \leq r \leq n$, $\Sigma_{\src(e) \cap V(\theta_{r}) \neq \emptyset} x_e = 0$ — this condition ensures that at least one set $V(\theta_{r})$ does not have any state in the cycle associated with the solution.

In this case, $ \LP'(\theta_{1}, \ldots, \theta_{n}) $ has a solution if and only if there is a path $ \pi $ such that $ z_i \leq \pay_i(\pi) $ for every player $ i $ and, for at least one $ V(\theta_{r}) $, its states are visited only finitely many times. Thus, we have a procedure that checks if there is a path $ \pi $ that satisfies $ \lnot \phi $ such that $ z_i \leq \pay_i(\pi) $ for every player $ i $, if and only if both linear programs have a solution. Using this new construction, we can now prove the following result.

with specifications  is $ \SigmaPTwo $-complete.

For membership, observe that by rearranging the problem statement, we have the following question:
Check whether the following expression is true

\begin{align*}
\exists \kappa \in \K(\Game,\beta)&,\tag{1}\\
&\exists \strpElm \in \strElm_1 \times \cdots \times \strElm_n,~\text{such that}~\strpElm \in \NE(\Game,\kappa),\tag{2}\\
&\forall \strpElm' \in \strElm_1 \times \cdots \times \strElm_n,~\text{if}~\strpElm' \in \NE(\Game,\kappa)~\text{then}~\pi(\strpElm') \models \phi.\tag{3}
\end{align*}

Statement $ (2) $ can be checked in (Theorem <ref>), whereas verifying statement $ (3) $ is in co; to see this, notice that we can rephrase $ (3) $ as follows: $ \neg \exists z \in \{ \pun_i(s) : s \in \St \}^{\Ag}  $ such that both $ \LP(\psi_{l}) $ and $ \LP'(\theta_1,\dots,\theta_{n}) $ have a solution in $ (\Game,\kappa){[z]} $. Thus, membership in $ \SigmaPTwo $ follows.

We prove hardness via a reduction from $ \QSAT_2 $ (satisfiability of quantified Boolean formulae with 2 alternations), which is known to be $ \SigmaPTwo $-complete  [30].

§ OPTIMALITY AND UNIQUENESS OF SOLUTIONS

Having asked the questions studied in the previous sections, the principal – the designer in the equilibrium design problem – may want to explore further information. Because the power of the principal is limited by its budget, and because from the point of view of the system, it may be associated with a reward (e.g., money, savings, etc.) or with the inverse of the amount of a finite resource (e.g., time, energy, etc.) an obvious question is asking about optimal solutions. This leads us to optimisation variations of the problems we have studied. Informally, in this case, we ask what is the least budget that the principal needs to ensure that the implementation problems have positive solutions. The principal may also want to know whether a given subsidy scheme is unique, so that there is no point in looking for any other solutions to the problem. In this section, we investigate these kind of problems, and classify our study into two parts, one corresponding to the problem and another one corresponding to the problem.

§.§ Optimality and Uniqueness in the Weak Domain

We can now define formally some of the problems that we will study in the rest of this section. To start, the optimisation variant for is defined as follows.

Given a game $\Game$ and a specification formula $\phi$:

What is the optimum budget $ \beta$ such that $ \WI(\Game,\phi,\beta) \neq \varnothing $?

Another natural problem, which is related to , is the “exact” variant – a membership question. In this case, in addition to $ \Game $ and $ \phi $, we are also given an integer $ b $, and ask whether it is indeed the smallest amount of budget that the principal has to spend for some optimal weak implementation. This decision problem is formally defined as follows.

Given a game $\Game$, a specification formula $\phi$, and an integer $ b $:

Is $b$ equal to the optimum budget for $ \WI(\Game,\phi,\beta) \neq \varnothing $?

To study these problems, it is useful to introduce some concepts first. More specifically, let us introduce the concept of implementation efficiency. We say that a (resp. ) is efficient if $ \beta = \cost(\kappa) $ and there is no $ \kappa' $ such that $ \cost(\kappa') < \cost(\kappa) $ and $ \kappa' \in \WI(\Game,\phi,\beta) $ (resp. $ \kappa' \in \SI(\Game,\phi,\beta) $). In addition to the concept of efficiency for an implementation problem, it is also useful to have the following result.

Let $ z_i $ be the largest payoff that player $ i $ can get after deviating from a path $\pi$. The optimum budget is an integer between 0 and $ \sum_{i \in \Ag} z_i \cdot (|\St|-1) $.

Using Proposition <ref>, we can show that both and can be solved in PSPACE for specifications. Intuitively, the reason is that we can use the upper bound given by Proposition <ref> to go through all possible solutions in exponential time, but using only nondeterministic polynomial space. Formally, we have the following results.

with specifications is -complete.

with specifications is -complete.

The fact that both and with specifications can be answered in, respectively, and does not come as a big surprise: checking an instance can be done using polynomial space and there are only exponentially many instances to be checked. However, for and with specifications, these two problems are more interesting.

with specifications is $ \FP^{\np} $-complete.

Membership follows from the fact that the search space, which is bounded as in Proposition <ref>, can be explored using binary search and as an oracle. More precisely, we can find the smallest budget $ \beta $ such that $ \WI(\Game,\phi,\beta) \neq \varnothing $ by checking every possible value for $ \beta $, which lies between 0 and $ 2^n $, where $ n $ is the length of the encoding of the instance. Since, due to the binary search routine, we need logarithmically many calls to the oracle (i.e., to ), in the end we have a searching procedure that would run in polynomial time.

For the lower bound, we reduce from TSP Cost (the optimal travelling salesman problem), which is $ \FP^{\np} $-complete [30].

with specifications is -complete.

For membership, observe that an input is a “yes” instance of if and only if it is a “yes” instance of  and a “yes” instance of (the problem where one asks whether $ \WI(\Game,\phi,\beta) = \varnothing $). Since the former problem is in and the latter problem is in co, membership in follows. For the lower bound, we use the same reduction technique as in Theorem <ref>, and reduce from Exact TSP, a problem known to be -hard [30, 31].

Following [29], we may naturally ask whether the optimal solution given by is unique. We call this problem . For some fixed budget $ \beta $, it may be the case that for two subsidy schemes $ \kappa, \kappa' \in \WI(\Game,\phi,\beta) $ – we assume the implementation is efficient – we have $ \kappa \neq \kappa'$ and $ \cost(\kappa) = \cost(\kappa') $. With specifications, it is not difficult to see that we can solve in polynomial space. Therefore, we have the following result.

with specifications is -complete.

For specifications, we reason about using the following procedure:

* Find the exact budget using binary search and as an oracle;

* Use an oracle once to guess two distinct subsidy schemes with precisely this budget; if no such subsidy schemes exist, return “yes”; otherwise, return “no”.

The above decision procedure clearly is in $ \DeltaPTwo $ (for the upper bound). Furthermore, since Theorem <ref> implies $ \DeltaPTwo $-hardness [23] (for the lower bound), we have the following corollary.

with specifications is $ \DeltaPTwo $-complete.

§.§ Optimality and Uniqueness in the Strong Domain

In this subsection, we study the same problems as in the previous subsection but with respect to the variant of the equilibrium design problem. We first formally define the problems of interest and then present the two first results.

Given a game $\Game$ and a specification formula $\phi$:

What is the optimum budget $ \beta$ such that $ \SI(\Game,\phi,\beta) \neq \varnothing $?

Given a game $\Game$, a specification formula $\phi$, and an integer $ b $:

Is $b$ equal to the optimum budget for $ \SI(\Game,\phi,\beta) \neq \varnothing $?

For the same reasons discussed in the weak versions of these two problems, we can prove the following two results with respect to games with specifications.

with specifications is -complete.

with specifications is -complete.

For specifications, observe that using the same arguments for the upper-bound of with specifications, we obtain the upper-bound for with specifications. Then, it follows that is in $ \FP^{\SigmaPTwo} $. For hardness, we define an $ \FP^{\SigmaPTwo} $-complete problem, namely $ \MWQSAT_2 $. Recall that in $ \QSAT_2 $ we are given a Boolean 3DNF formula $ \psi(\setx,\sety)$ and sets $\setx =\{ x_1,\dots,x_n \}, \sety = \{ y_1,\dots,y_m \} $, with a set of terms $T =\{ t_1,\dots,t_k \} $. Define $ \MWQSAT_2 $ as follows. Given $ \psi(\setx,\sety) $ and a weight function $ \cFun: \setx \to \mathbb{Z}^{\geq}$, $ \MWQSAT_2 $ is the problem of finding an assignment $ \vecx \in \{0,1\}^n $ with the least total weight such that $ \psi(\setx,\sety) $ is true for every $ \vecy \in \{0,1\}^m $. Observe that $ \MWQSAT_2 $ generalises $ \MQSAT_2 $, which is known to be $ \FP^{\SigmaPTwo[\log n]} $-hard [12], i.e., $ \MQSAT_2 $ is an instance of $ \MWQSAT_2 $, where all weights are 1.

$ \MWQSAT_2 $ is $ \FP^{\SigmaPTwo} $-complete.

Membership follows from the upper-bound of $ \MQSAT_2 $ [12]: since we have an exponentially large input with respect to that of $ \MQSAT_2 $, by using binary search we will need polynomially many calls to the $ \SigmaPTwo $ oracle. Hardness is immediate [12].

Now that we have an $ \FP^{\SigmaPTwo} $-hard problem in our hands, we can proceed to determine the complexity class of with specifications.
For the upper bound we one can use arguments analogous to those in Theorem <ref>. For the lower bound, one can reduce from $ \MWQSAT_2 $. Formally, we have:

with specifications is $ \FP^{\SigmaPTwo} $-complete.

with specifications is $ \DPTwo $-complete.

Membership follows from the fact that an input is a “yes” instance of (with specifications) if and only if it is a “yes” instance of  and a “yes” instance of , the decision problem where we ask $ \SI(\Game,\phi,\beta) = \varnothing $ instead. The lower bound follows from the hardness of and problems, which immediately implies -hardness <cit.>.

Furthermore, analogous to , we also have the following corollaries.

with specifications is -complete.

with specifications is $ \DeltaPThree $-complete.

§ CONCLUSIONS & RELATED AND FUTURE WORK

*Equilibrium design vs. mechanism design – connections with Economic theory.
Although equilibrium design is closely related to mechanism design, as typically studied in game theory [22], the two are not exactly the same. Two key features in mechanism design are the following. Firstly, in a mechanism design problem, the designer is not given a game structure, but instead is asked to provide one; in that sense, a mechanism design problem is closer to a rational synthesis problem [14, 17]. Secondly, in a mechanism design problem, the designer is only interested in the game's outcome, which is given by the payoffs of the players in the game; however, in equilibrium design, while the designer is interested in the payoffs of the players as these may need to be perturbed by its budget, the designer is also interested – and in fact primarily interested – in the satisfaction of a temporal logic goal specification, which the players in the game do not take into consideration when choosing their individual rational choices; in that sense, equilibrium design is closer to rational verification [18] than to mechanism design. Thus, equilibrium design is a new computational problem that sits somewhere in the middle between mechanism design and rational verification/synthesis. Technically, in equilibrium design we go beyond rational synthesis and verification through the additional design of subsidy schemes for incentivising behaviours in a concurrent and multi-agent system, but we do not require such subsidy schemes to be incentive compatible mechanisms, as in mechanism design theory, since the principal may want to reward only a group of players in the game so that its temporal logic goal is satisfied, while rewarding other players in the game in an unfair way – thus, leading to a game with a suboptimal social welfare measure. In this sense, equilibrium design falls short with respect to the more demanding social welfare requirements often found in mechanism design theory.

*Equilibrium design vs. rational verification – connections with Computer science.
Typically, in rational synthesis and verification [14, 17, 18, 24] we want to check whether a property is satisfied on some/every Nash equilibrium computation run of a reactive, concurrent, and multi-agent system. These verification problems are primarily concerned with qualitative properties of a system, while assuming rationality of system components. However, little attention is paid to quantitative properties of the system. This drawback has been recently identified and some work has been done to cope with questions where both qualitative and quantitative concerns are considered [3, 6, 9, 10, 11, 19, 21, 37]. Equilibrium design is new and different approach where this is also the case. More specifically, as in a mechanism design problem, through the introduction of an external principal – the designer in the equilibrium design problem – we can account for overall qualitative properties of a system (the principal's goal given by an or a specification) as well as for quantitative concerns (optimality of solutions constrained by the budget to allocate additional rewards/resources). Our framework also mixes qualitative and quantitative features in a different way: while system components are only interested in maximising a quantitative payoff, the designer is primarily concerned about the satisfaction of a qualitative (logic) property of the system, and only secondarily about doing it in a quantitatively optimal way.

*Equilibrium design vs. repair games and normative systems – connections with AI.
In recent years, there has been an interest in the analysis of rational outcomes of multi-agent systems modelled as multi-player games. This has been done both with modelling and with verification purposes. In those multi-agent settings, where AI agents can be represented as players in a multi-player game, a focus of interest is on the analysis of (Nash) equilibria in such games [8, 18]. However, it is often the case that the existence of Nash equilibria in a multi-player game with temporal logic goals may not be guaranteed [17, 18]. For this reason, there has been already some work on the introduction of desirable Nash equilibria in multi-player games [2, 32]. This problem has been studied as a repair problem [2] in which either the preferences of the players (given by winning conditions) or the actions available in the game are modified; the latter one also being achieved with the use of normative systems [32]. In equilibrium design, we do not directly modify the preferences of agents in the system, since we do not alter their goals or choices in the game, but we indirectly influence their rational behaviour by incentivising players to visit, or to avoid, certain states of the overall system. We studied how to do this in an (individually) optimal way with respect to the preferences of the principal in the equilibrium design problem. However, this may not always be possible, for instance, because the principal's temporal logic specification goal is just not achievable, or because of constraints given by its limited budget.

*Future work: social welfare requirements and practical implementation.
As discussed before, a key difference with mechanism design is that social welfare requirements are not considered [26]. However, a benevolent principal might not see optimality as an individual concern, and instead consider the welfare of the players in the design of a subsidy scheme. In that case, concepts such as the  utilitarian social welfare may be undesirable as the social welfare maximising the payoff received by players might allocate all the budget to only one player, and none to the others. A potentially better option is to improve fairness in the allocation of the budget by maximising the egalitarian social welfare. Finally, given that the complexity of equilibrium design is much better than that of rational synthesis/verification, we should be able to have efficient implementations, for instance, as an extension of EVE [20].

[1]
Gadi Aleksandrowicz, Hana Chockler, Joseph Y. Halpern, and Alexander Ivrii.
The computational complexity of structure-based causality.
J. Artif. Int. Res., 58(1):431–451, January 2017.

[2]
S. Almagor, G. Avni, and O. Kupferman.
Repairing Multi-Player Games.
In CONCUR, volume 42 of LIPIcs, pages 325–339. Schloss
Dagstuhl, 2015.

[3]
S. Almagor, O. Kupferman, and G. Perelli.
Synthesis of controllable Nash equilibria in quantitative objective
In IJCAI, pages 35–41, 2018.

[4]
B. Aminof, V. Malvone, A. Murano, and S. Rubin.
Graded Strategy Logic: Reasoning about Uniqueness of Nash
In AAMAS, pages 698–706. ACM, 2016.

[5]
R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa'ar.
Synthesis of reactive(1) designs.
Journal of Computer and System Sciences, 78(3):911–938, 2012.

[6]
A. Bohy, V. Bruyère, E. Filiot, and J. Raskin.
Synthesis from LTL Specifications with Mean-Payoff Objectives.
In TACAS, pages 169–184, 2013.

[7]
U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman.
Temporal Specifications with Accumulative Values.
ACM Transactions on Computational Logic, 15(4):27:1–27:25,

[8]
P. Bouyer, R. Brenguier, N. Markey, and M. Ummels.
Pure Nash Equilibria in Concurrent Deterministic Games.
Logical Methods in Computer Science, 11(2), 2015.

[9]
K. Chatterjee and L. Doyen.
Energy parity games.
Theoretical Computer Science, 458:49–60, 2012.

[10]
K. Chatterjee, L. Doyen, T. Henzinger, and J. Raskin.
Generalized Mean-payoff and Energy Games.
In FSTTCS, pages 505–516, 2010.

[11]
K. Chatterjee, T. A. Henzinger, and M. Jurdzinski.
Mean-Payoff Parity Games.
In LICS, pages 178–187. IEEE Computer Society, 2005.

[12]
H. Chockler and J. Halpern.
Responsibility and Blame: A Structural-Model Approach.
Journal of Artificial Intelligence Research, 22:93–115, 2004.

[13]
Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin,
and Szymon Toruńczyk.
Energy and mean-payoff games with imperfect information.
In Anuj Dawar and Helmut Veith, editors, Computer Science
Logic, pages 260–274, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.

[14]
D. Fisman, O. Kupferman, and Y. Lustig.
Rational Synthesis.
In TACAS, volume 6015 of LNCS, pages 190–204.
Springer, 2010.

[15]
M. Garey, R. Graham, and D. Johnson.
Some NP-complete Geometric Problems.
In STOC, pages 10–22. ACM, 1976.

[16]
J. Gutierrez, P. Harrenstein, G. Perelli, and M. Wooldridge.
Nash Equilibrium and Bisimulation Invariance.
In CONCUR, volume 85 of LIPIcs, pages 17:1–17:16.
Schloss Dagstuhl, 2017.

[17]
J. Gutierrez, P. Harrenstein, and M. Wooldridge.
Iterated Boolean Games.
Information and Computation, 242:53–79, 2015.

[18]
J. Gutierrez, P. Harrenstein, and M. Wooldridge.
From Model Checking to Equilibrium Checking: Reactive Modules for
Rational Verification.
Artificial Intelligence, 248:123–157, 2017.

[19]
J. Gutierrez, A. Murano, G. Perelli, S. Rubin, and M. Wooldridge.
Nash Equilibria in Concurrent Games with Lexicographic Preferences.
In IJCAI, pages 1067–1073, 2017.

[20]
J. Gutierrez, M. Najib, G. Perelli, and M. Wooldridge.
EVE: A Tool for Temporal Equilibrium Analysis.
In ATVA, volume 11138 of LNCS, pages 551–557.
Springer, 2018.

[21]
J. Gutierrez, M. Najib, G. Perelli, and M. Wooldridge.
On Computational Tractability for Rational Verification.
In IJCAI, 2019.
To appear.

[22]
L. Hurwicz and S. Reiter.
Designing Economic Mechanisms.
Cambridge University Press, 2006.

[23]
M. Krentel.
The Complexity of Optimization Problems.
Journal of Computer and System Sciences, 36(3):490 – 509,

[24]
O. Kupferman, G. Perelli, and M. Y. Vardi.
Synthesis with rational environments.
Annals of Mathematics and Artificial Intelligence, 78(1):3–20,

[25]
M. Wooldridge and U. Endriss and S. Kraus and J. Lang.
Incentive engineering for Boolean games.
Artificial Intelligence, 195:418 – 439, 2013.

[26]
M. Maschler, E. Solan, and S. Zamir.
Game Theory.
Cambridge University Press, 2013.

[27]
M.J. Osborne and A. Rubinstein.
A Course in Game Theory.
MIT Press, 1994.

[28]
C. Papadimitriou.
The Euclidean Travelling Salesman Problem is NP-complete.
Theoretical Computer Science, 4(3):237 – 244, 1977.

[29]
C. Papadimitriou.
On the Complexity of Unique Solutions.
Journal of the ACM, 31(2):392–400, 1984.

[30]
C. Papadimitriou.
Computational complexity.
Addison-Wesley, Reading, Massachusetts, 1994.

[31]
C. Papadimitriou and M. Yannakakis.
The complexity of facets (and some facets of complexity).
Journal of Computer and System Sciences, 28(2):244 – 259,

[32]
G. Perelli.
Enforcing equilibria in multi-agent systems.
In Proceedings of the 18th International Conference on
Autonomous Agents and MultiAgent Systems, AAMAS '19, pages 188–196, 2019.

[33]
A. Pnueli.
The Temporal Logic of Programs.
In FOCS, pages 46–57. IEEE, 1977.

[34]
A. Pnueli and R. Rosner.
On the Synthesis of a Reactive Module.
In POPL, pages 179–190. ACM Press, 1989.

[35]
S. Heubach and T. Mansour.
Combinatorics of Compositions and Words: Solutions Manual.
Chapman & Hall/CRC, 2009.

[36]
M. Ummels and D. Wojtczak.
The Complexity of Nash Equilibria in Limit-Average Games.
In CONCUR, pages 482–496, 2011.

[37]
Y. Velner, K. Chatterjee, L. Doyen, T. Henzinger, A. Rabinovich, and J. Raskin.
The Complexity of Multi-Mean-Payoff and Multi-Energy Games.
Information and Computation, 241:177–196, 2015.

[38]
U. Zwick and M. Paterson.
The Complexity of Mean Payoff Games on Graphs.
Theoretical Computer Science, 158(1):343 – 359, 1996.

§ PROOFS

*Proof of Theorem <ref>

For (1) implies (2): Let $ z_i $ be the largest value player $ i $ can get by deviating from $ \pi $. Let $ k \in \SetN $ be such that $ z_i = \pun_i(\trnFun(s_k,(\jact_{-i},\act'_i))) $. Suppose further that $ \pay_i(\pi) < z_i $. Thus, player $ i $ would deviate at $ s_k $, which is a contradiction to $ \pi $ being a path induced by a Nash equilibrium.

For (2) imples (1): Define strategy profile $ \strpElm $ that follows $ \pi $ as long as no-one has deviated from $ \pi $.
In such a case where player $ i $ deviates on the $k$-th iteration, the strategy profile $\strpElm_{-i}$ starts playing the $z_i$-secure strategy for player $i$ that guarantees the payoff of player $i$ to be less than $z_i$. Therefore, we have $\pay_i(\pi(\strpElm_{-i},\strElm'_{i})) \leq z_i \leq \pay_i(\pi)$, for every possible strategy $\strElm'_{i}$ of player $i$ (the second inequality is due to condition $2(b)$). Thus, there is no beneficial deviation for player $ i $ and $ \pi $ is a path induced by a Nash equilibrium.

*Proof of Proposition <ref>

For a fixed budget $b$, the number of subsidy schemes of budget exactly $b$ corresponds to the number of weak compositions of $b$ in $m$ parts, which is given by $\binom{b+m-1}{b}$ [35].
Therefore, the number of subsidy schemes of budget at most $\beta$ is the sum

\card{\K(\Game,\beta)} = \sum_{b=0}^{\beta}\binom{b+m-1}{b}\text{.}

We now prove that

$$\sum_{b=0}^{\beta}\binom{b+m-1}{b} = \frac{\beta + 1}{m} \binom{\beta + m}{\beta + 1}\text{.}$$

By induction on $\beta$, as base case, for $\beta = 0$, we have that

\binom{\beta + m - 1}{\beta} = 1 = \frac{\beta + 1}{m} \binom{\beta +m}{\beta +1}\text{.}

For the inductive case, let us assume that the assertion hold for some $\beta$ and let us prove for $\beta + 1$.
We have the following:

$$\sum_{b=0}^{\beta + 1}\binom{b+m-1}{b} = \sum_{b=0}^{\beta}\binom{b+m-1}{b} + \binom{\beta + m - \cancel{1} + \cancel{1}}{\beta + 1} = \frac{\beta + 1}{m} \binom{\beta + m}{\beta + 1} + \binom{\beta + m}{\beta + 1} \text{.}$$

Therefore we have

\begin{align*}
\frac{\beta + 1}{m} \binom{\beta + m}{\beta + 1} + \binom{\beta + m}{\beta + 1} & = \binom{\beta + m}{\beta + 1} \left(\frac{\beta + 1}{m} + 1\right) = \\
\binom{\beta + m}{\beta + 1} \frac{\beta + 1 + m}{m}
& = \frac{\beta + 1 + m}{m} \cdot \frac{(\beta + m)!}{(\beta + 1)!(\cancel{\beta} + m - \cancel{\beta} - 1)!} = \\
\frac{(\beta + m + 1)!}{(\beta + 1)!m!} = \frac{(\beta + m + 1)!}{(\beta + 1)!m!}\cdot \frac{\beta + 2}{\beta + 2} \cdot \frac{m}{m} & = \frac{\beta + 2}{m} \cdot \frac{(\beta + m + 1)!}{(\beta + 2)! (m - 1)!} = \\
\frac{\beta + 2}{m} \cdot \frac{(\beta + m + 1)!}{(\beta + 2)! (\beta + m + 1 - \beta - 2)!} & = \frac{\beta + 2}{m} \binom{\beta + m + 1}{\beta + 2}
\end{align*}

that proves the assertion.

*Proof of Theorem <ref>

We will define a linear program of size polynomial in $(\Game,\kappa)$ having a solution if and only if there exists an ultimately periodic path $ \pi $ such that $z_i \leq \pay_i(\pi) $ and satisfies the specification.

Recall that $\varphi$ has the following form

\varphi = \bigwedge_{l = 1}^{m} \always \sometime \psi_{l} \to \bigwedge_{r = 1}^{n} \always \sometime \theta_{r}\text{,}

and let $V(\psi_{l})$ and $V(\theta_r)$ be the subset of states in $(\Game,\kappa)$ that satisfy the boolean combinations $\psi_{l}$ and $\theta_{r}$, respectively. Observe that property $\varphi$ is satisfied over a path $\pi$ if, and only if, either $\pi$ visits every $V(\theta_r)$ infinitely many times or visits some of the $V(\psi_{l})$ only a finite number of times.

For the game $(\Game,\kappa){[z]}$, let $ W = (V, E, (\wFun_a)_{a \in \Ag})$ be the underlying multi-weighted graph, and for every edge $e\in E$ introduce a variable $x_e$. Informally, the value $x_e$ is the number of times that the edge $e$ is used on a cycle. Formally, let $\src(e) = \{v \in V : \exists w\, e = (v,w) \in E\}$; $\trg(e) = \{v \in V : \exists w\, e = (w,v) \in E\}$; $\OUT(v) = \{e \in E : \src(e) = v\}$; and $\IN(v) = \{e \in E : \trg(e) = v\}$.

Consider $\psi_{l}$ for some $1 \leq l \leq m$, and define the linear program $\LP(\psi_{l})$ with the following inequalities and equations:

$x_e \geq 0$ for each edge $e$
— a basic consistency criterion;

$\Sigma_{e \in E} x_e \geq 1$
— ensures that at least one edge is chosen;

for each $a \in \Ag$, $\Sigma_{e \in E} \wFun_a(\src(e)) x_e \geq 0$ — this enforces that the total sum of any solution is non-negative;

$\Sigma_{\src(e) \cap V(\psi_{l}) \neq \emptyset} x_e = 0$ — this ensures that no state in $V(\psi_{l})$ is in the cycle associated with the solution;

for each $v \in V$, $\Sigma_{e \in \OUT(v)} x_e = \Sigma_{e \in \IN(v)} x_e$  — this condition says that the number of times one enters a vertex is equal to the number of times one leaves that vertex.

By construction, it follows that $\LP(\psi_{l})$ admits a solution if and only if there exists a path $\pi$ in $\Game$ such that $z_i \leq \pay_i(\pi) $ for every player $i$ and visits $V(\psi_{l})$ only finitely many times.

In addition, consider the linear program $\LP(\theta_{1}, \ldots, \theta_{n})$ defined with the following inequalities and equations:

$x_e \geq 0$ for each edge $e$ —
a basic consistency criterion;

$\Sigma_{e \in E} x_e \geq 1$ —
ensures that at least one edge is chosen;

for each $a \in \Ag$, $\Sigma_{e \in E} \wFun_a(\src(e)) x_e \geq 0$ — this enforces that the total sum of any solution is non-negative;

for all $1 \leq r \leq n$, $\Sigma_{\src(e) \cap V(\theta_{r}) \neq \emptyset} x_e \geq 1$ — this ensures that for every $V(\theta_{r})$ at least one state is in the cycle;

for each $v \in V$, $\Sigma_{e \in \OUT(v)} x_e = \Sigma_{e \in \IN(v)} x_e$  — this
condition says that the number of times one enters a vertex is equal to the number of times one leaves that vertex.

In this case, $\LP(\theta_{1}, \ldots, \theta_{n})$  admits a solution if and only if there exists a path $\pi$ such that $z_i \leq \pay_i(\pi) $ for every player $i$ and visits every $V(\theta_{r})$ infinitely many times.

Since the constructions above are polynomial in the size of both $(\Game,\kappa)$ and $\phi$, we can conclude it is possible to check in the statement that there is a path $\pi$ satisfying $\varphi$ such that $z_i \leq \pay_i(\pi) $ for every player $i$ in the game if and only if one of the two linear programs defined above has a solution.

For the lower-bound, we use [36] and observe that if $\phi$ is true and $ \beta = 0 $, then the problem is equivalent to checking whether the game has a Nash equilibrium.

*Proof of Theorem <ref>

For membership, observe that by rearranging the problem statement, we have the following question:

Check whether the following expression is true

\begin{align*}
\exists \kappa \in \K(\Game,\beta)&,\tag{1}\\
&\exists \strpElm \in \strElm_1 \times \cdots \times \strElm_n,~\text{such that}~\strpElm \in \NE(\Game,\kappa),\tag{2}\\
&\forall \strpElm' \in \strElm_1 \times \cdots \times \strElm_n,~\text{if}~\strpElm' \in \NE(\Game,\kappa)~\text{then}~\pi(\strpElm') \models \phi.\tag{3}
\end{align*}

Statement $ (2) $ can be checked in (Theorem <ref>). Whereas, verifying statement $ (3) $ is in co; to see this, notice that we can rephrase $ (3) $ as follows: $ \not \exists z \in \{ \pun_i(s) : s \in \St \}^{\Ag}  $ such that both $ \LP(\psi_{l}) $ and $ \LP'(\theta_1,\dots,\theta_{n}) $ have a solution in $ (\Game,\kappa){[z]} $. Thus $ \SigmaPTwo $ membership follows.

We prove hardness by a reduction from $ \QSAT_2 $ (satisfiability of quantified Boolean formula with 2 alternations) [30]. Let $ \psi(\setx,\sety) $ be an $ n + m $ variable Boolean 3DNF formula, where $ \setx = \{x_1,\dots,x_n \} $ and $ \sety = \{ y_1,\dots, y_n \} $, with $ t_1,\dots,t_k $ terms. Write $ \term_j $ for the set of literals in $ j $-th term and $ \term_j^i $ for the $ i $-th literal in $ \term_j $. Moreover write $ x^j_i $ and $ y^j_i $ for variable $ x_i \in \setx $ and $ y_i \in \sety $ that appears in $ j $-th term, respectively. For instance, if the fifth term is of the form of $ (x_2 \wedge \lnot x_3 \wedge y_4) $, then we have $ \term_5 = \{ x^5_2, x^5_3, y^5_4 \} $ and $ \term_5^1 = x^5_2 $. Let $ \T = \{ \term_i \cap \sety : 1 \leq i \leq k \} $, that is, the set of subset of $ \term_i $ that contains only $ y $-literals.

For a formula $ \psi(\setx,\sety) $ we construct an instance of such that $ \SI(\Game,\phi,\beta) \neq \varnothing $ if and only if there is an $ \vecx \in \{0,1\}^n $ such that $ \psi(\setx,\sety) $ is true for every $ \vecy \in \{0,1\}^m $. Let $ \Game $ be such a game where

* $ \Ag = \{1,2\} $,

* $ \St = \{ \bigcup_{j \in [1,k]} (\term_j \times \{0,1\}^3) \} \cup \{\T \times \{0\}^3 \} \cup \{ \tuple{\source,\{0\}^3}, \tuple{\sink,\{0\}^3} \} $,

* $ s_0 = \source $,

* for each state $ s \in \St $

* $ \Ac_1(s) = \{ \{ \T \cup \{\sink \} \} \times \{0\}^3 \} $, $ \Ac_2(s) = \{ \varepsilon \} $, if $ s = \tuple{\source,\{0\}^3} $,

* $ \Ac_1(s) = \{ \term^1_i : s[0] \subseteq \term_i \wedge i \in [1,k] \} $, $ \Ac_2(s) = \{ 0,1 \}^{3}$, if $ s \in \{\T \times \{0\}^3 \} $,

* $ \Ac_1(s) = \{ \varepsilon \} $, $ \Ac_2(s) = \{ \varepsilon \} $, if $ s \in \bigcup_{j \in [1,k]} (\term_j \times \{0,1\}^3) $,

* for an action profile $ \jact = (\act_{1},\act_{2}) $

* $ \trnFun(s,\jact) = \act_{1} $, if $ s = \tuple{\source,\{0\}^3} $,

* $ \trnFun(s,\jact) = \tuple{\act_{1},\act_{2}} $, if $ s \in \{\T \times \{0\}^3 \} $,

* $ \trnFun(s,\jact) = \tuple{\term_j^{(i \bmod 3)+1 },s[1]} $, if $ s = \tuple{\term^i_j,s[1]} \in \bigcup_{j \in [1,k]} (\term_j \times \{0,1\}^3) $;

* $ \trnFun(s,\jact) = s $, otherwise;

* for each state $ s \in \St, \labFun(s) = s[0] $,

* for each state $ s \in \St $

* $ \wFun_1(s) = \frac{2}{3} $, if $ s[0] = \sink $[This can be implemented by a macrostate with three substates—2 substates with weight of 1, and 1 with weight of 0—forming a simple cycle.],

* $ \wFun_1(s) = 0 $, otherwise;

* the payoff of player $ i \in \Ag $ for an ultimately periodic path $ \pi $ in $ \Game $ is

* $ \pay_1(\pi) = \MP(\wFun_1(\pi)) $,

* $ \pay_2(\pi) = - \MP(\wFun_1(\pi)) $,

Furthermore, let $ \beta = |\setx| $ and the property to be $ \phi := \always \sometime~\lnot \sink $. Define a (partial) subsidy scheme $ \kappa : \setx \to \{0,1\} $. The weights are updated with respect to $ \kappa $ as follows:

for each $ s \in \St $ such that $ s[0] \in \term_j \setminus \sety $, that is, an $ x $-literal that appears in term $ t_j $

\[
\wFun_1(s) =
\begin{cases}
1, & \text{if } \kappa(s) = 1 \wedge s[0]~\text{is not negated in}~t_j \\
1, & \text{if } \kappa(s) = 0 \wedge s[0]~\text{is negated in}~t_j \\
0, & \text{if } \kappa(s) = 1 \wedge s[0]~\text{is negated in}~t_j \\
%	0, & \text{if } \kappa_1(\langle v,\top \rangle) = 0 \wedge v \not\in S \\
0, & \text{otherwise;}
\end{cases}
\]

for each $ s \in \St $ such that $ s[0] \in \term_j \setminus \setx $, that is, a $ y $-literal that appears in term $ t_j $, $ s[0] = \term^i_j $

\[
\wFun_1(s) =
\begin{cases}
1, & \text{if } s[1][i] = 1 \wedge s[0]~\text{is not negated in}~t_j \\
1, & \text{if } s[1][i] = 0 \wedge s[0]~\text{is negated in}~t_j \\
0, & \text{if } s[1][i] = 1 \wedge s[0]~\text{is negated in}~t_j \\
%	0, & \text{if } \kappa_1(\langle v,\top \rangle) = 0 \wedge v \not\in S \\
0, & \text{otherwise;}
\end{cases}
\]

the weights of other states remain unchanged.

The construction is now complete, and polynomial to the size of formula $ \psi(\setx,\sety) $. We claim that $ \SI(\Game,\phi,\beta) \neq \varnothing $ if and only if there is an $ \vecx \in \{0,1\}^n $ such that $ \psi(\setx,\sety) $ is true for every $ \vecy \in \{0,1\}^m $. From left to right, consider a subsidy scheme $ \kappa \in \SI(\Game,\phi,\beta) $ which implies that there exists no Nash equilibrium run in $ (\Game,\kappa) $ that ends up in $ \sink $. This means that for every action $ \jact_{2} \in \Ac_2(s), $ there exists $ \jact_1 \in \Ac_1(s), s \in \{\T \times \{0\}^3 \} $, such that $ \pay_1(\pi) = 1 $, where $ \pi $ is the resulting path of the joint action. Observe that this corresponds to the existence of (at least) a term $ t_i $, which evaluates to true under assignment $ \vecx $, regardless the value of $ \vecy $. From right to left, consider an assigment $ \vecx \in \{0,1\}^n $ such that for all $ \vecy \in \{0,1\}^m $, the formula $ \psi(\setx,\sety) $ is true. This means that for every $ \vecy $, there exists (at least one) term $ t_i $ in $ \psi(\setx,\sety) $ that evaluates to true. By construction, specifically the weight updating rules, for every $ \jact_{2} $ corresponding to assignment $ \vecy $, there exists $ \term_j $ such that $ \forall i \in [1,3], \wFun_1(\term^i_j) = 1 $. This means that player 1 can always get payoff equals to 1, therefore, any run that ends in $ \sink $ is not sustained by Nash equilibrium.

*Proof of Proposition <ref>

The lower-bound is straightforward. The upper-bound follows from the fact that the maximum value the principal has to pay to player $ i $ is when the path $ \pi $ is a simple cycle and formed from all states in $ \St $, apart from 1 deviation state.

*Proof of Theorem <ref>

Since the search space is bounded (Proposition <ref>), by using an an oracle we can iterate through every instance and return the smallest $ \beta $ such that $ \WI(\Game,\phi,\beta) \neq \varnothing $. Moreover, each instance is of polynomial size in the size of the input. Thus membership in follows. Hardness is straightforward.

*Proof of Theorem <ref>

Membership follows from the fact that the search space, which is bounded as in Proposition <ref>, can be fully explored using binary search and as an oracle. More precisely, we can find the smallest budget $ \beta $ such that $ \WI(\Game,\phi,\beta) \neq \varnothing $ by checking every possible value for $ \beta $, which lies between 0 and $ 2^n $, where $ n $ is the length of the encoding of the instance. Since we need logarithmically many calls to the oracle (to ), in the end we have searching procedure that runs in polynomial time.

For hardness we reduce from TSP Cost (optimal travelling salesman problem) that is known to be $ \FP^{\np} $-complete [30]. Given a TSP Cost instance $ \tuple{G, c} $, $ G = \tuple{V, E} $ is a graph, $ c : E \to \SetZ $ is a cost function. We assume that $ \WI(\Game,\phi,\beta) $ is efficient. To encode TSP Cost instance, we construct a game $ \Game $ and formula $ \phi $, such that the optimum budget $ \beta $ corresponds to the value of optimum tour. Let $ \Game $ be such a game where

* $ \Ag = \{ 1 \} $,

* $ \St = \{ \tuple{v,e} : v \in V \wedge e \in \IN(v) \} \cup \{ \tuple{\sink,\varepsilon} \} $,

* $ s_0 $ can be chosen arbitrarily from $ \St \setminus \{\tuple{\sink,\varepsilon}\} $,

* for each state $ \tuple{v,e} \in \St $ and edge $ e' \in E \cup \{\varepsilon\} $

* $ \trnFun(\tuple{v,e},e') = \tuple{\trg(e'),e'}, \text{if}~v \neq \sink~\text{and}~e' \neq \varepsilon, $

* $ \trnFun(\tuple{v,e},e') = \tuple{\sink,\varepsilon}, \text{otherwise}; $

* for each state $ \tuple{v,e} \in \St $

* $ \wFun_1(\tuple{v,e}) = \max\{c(e'): e' \in E \} - c(e) $, if $ v \neq \sink $,

* $ \wFun_1(\tuple{v,e}) = \max\{c(e'): e' \in E \} $, otherwise;

* the payoff of player 1 for a path $ \pi $ in $ \Game $ is $ \pay_1(\pi) = \MP[\wFun_1(\pi)] $,

* for each state $ \tuple{v,e} \in \St $, the set of actions available to player 1 is $ \OUT(v) \cup \{\varepsilon\} $,

* for each state $ \tuple{v,e} \in \St $, $ \labFun(\tuple{v,e}) = v $.

Furthermore, let $ \phi := \bigwedge_{v \in V} \always \sometime~v $. The construction is now complete, and is polynomial to the size of $ \tuple{G, c} $.

Now, consider the smallest $ \cost(\kappa), \kappa \in \WI(\Game,\phi,\beta) $. We argue that $ \cost(\kappa) $ is indeed the lowest value such that a tour in $ G $ is attainable. Suppose for contradiction, that there exists $ \kappa' $ such that $ \cost(\kappa') < \cost(\kappa) $. Let $ \pi' $ be a path in $ (\Game,\kappa') $ and $ z_1 = \wFun_1(\tuple{\sink,\varepsilon}) $ the largest value player 1 can get by deviating from $ \pi' $. We have $ \pay_1(\pi') < z_1 $, and since for every $ \tuple{v,e} \in \St $ there exists an edge to $ \tuple{\sink,\varepsilon} $, thus player 1 would deviate to $ \tuple{\sink,\varepsilon} $ and stay there forever. This deviation means that $ \phi $ is not satisfied, which is a contradiction to $ \kappa' \in \WI(\Game,\phi,\beta) $. The construction of $ \phi $ also ensures that the path is a valid tour, i.e., the tour visits every city at least once. Notice that $ \phi $ does not guarantee a Hamiltonian cycle. However, removing the condition of visiting each city only once does not remove the hardness, since Euclidean TSP is -hard [15, 28]. Therefore, in the planar case there is an optimal tour that visits each city only once, or otherwise, by the triangle inequality, skipping a repeated visit would not increase the cost. Finally, since $ \WI(\Game,\phi,\beta) $ is efficient, we have $ \beta $ to be exactly the value of the optimum tour in the corresponding TSP Cost instance.

*Proof of Theorem <ref>

The proof is analogous to that of Theorem <ref>.

*Proof of Theorem <ref>

Membership uses arguments analogous to those in Theorem <ref>. For hardness, we reduce $ \MWQSAT_2 $ to using the same techniques used in Theorem <ref> with few modifications. Given a
$ \MWQSAT_2 $ instance $ \tuple{\psi(\setx,\sety),\cFun} $, we construct a game $ \Game $ and formula $ \phi $, such that the optimum budget $ \beta $ corresponds to the value of optimal solution to $ \tuple{\psi(\setx,\sety),\cFun} $. To this end, we may assume that $ \SI(\Game,\phi,\beta) $ is efficient and construct $ \Game $ with exactly the same rules as in Theorem <ref> except for the following:

* clearly the value of $ \beta $ is unknown,

* the initial weight for each state $ s \in \St $

* $ \wFun_1(s) = \frac{2}{3} $, if $ s[0] = \sink $,

\[
\wFun_1(s) =
\begin{cases}
- \cFun(s[0]) + 1, & \text{if } s[0] \in \term_j \setminus \sety \wedge s[0] ~\text{is not negated in}~t_j \\
1, & \text{if } s[0] \in \term_j \setminus \sety \wedge s[0]~\text{is negated in}~t_j; \\
\end{cases}
\]

* $ \wFun_1(s) = 0 $, otherwise;

* given a subsidy scheme $ \kappa $, we update the weight for each $ s \in \St $ such that $ s[0] \in \term_j \setminus \sety $, that is, an $ x $-literal that appears in term $ t_j $

\[
\wFun_1(s) =
\begin{cases}
\wFun_1(s) + \kappa(s), & \text{if } s[0]~\text{is not negated in}~t_j \\
%		1, & \text{if } \kappa(s) = 0 \wedge s[0]~\text{is negated in}~t_j \\
%		0, & \text{if } \kappa(s) = 1 \wedge s[0]~\text{is negated in}~t_j \\
%		%	0, & \text{if } \kappa_1(\langle v,\top \rangle) = 0 \wedge v \not\in S \\
\wFun_1(s), & \text{otherwise;}
\end{cases}
\]

the construction is complete and polynomial to the size of $ \tuple{\psi(\setx,\sety),\cFun} $.

Let $ o $ be the optimal solution to $ \MWQSAT_2 $ given the input $ \tuple{\psi(\setx,\sety),\cFun} $. We claim that $ \beta $ is exactly $ o $. To see this, consider the smallest $ \cost(\kappa)$, $ \kappa \in \SI(\Game,\phi,\beta) $. We argue that this is indeed the least total weight of an assignment $ \vecx $ such that $ \psi(\setx,\sety) $ is true for every $ \vecy $. Assume towards a contradiction that $ \cost(\kappa) < o $. By the construction of $ \wFun_1(\cdot) $, there exists no $ \pi $ such that $ \pay_1(\pi) > \frac{2}{3} $. Therefore, any run $ \pi' $ that ends up in $ \sink $ is sustained by Nash equilibrium, which is a contradiction to $ \kappa \in \SI(\Game,\phi,\beta) $. Now, since $ \SI(\Game,\phi,\beta) $ is efficient, by definition, there exists no $ \kappa' \in \SI(\Game,\phi,\beta) $ such that $ \cost(\kappa') < \cost(\kappa) $. Thus we have $ \beta $ equals to $ o $ as required.

§ ALGORITHMS

Input: A game $\Game$, a specification formula $\varphi$, and budget $ \beta $.

$ \kappa \in \K(\Game,\beta), s \in \St,$ and $ (\strpElm_{-1},\dots,\strpElm_{-n}) \in \bigtimes_{j \in \Ag} (\times_{i \in \Ag \setminus {j}} \strElm_i) $
Compute $ (\Game,\kappa)$

$ i \in \Ag $
Compute $ z_i = \pun_i(s) $ using $ \strpElm_{-i} $

Compute $ (\Game,\kappa){[z]} $

there is $ \strpElm \in \NE((\Game,\kappa){[z]}) $ such that $ \pi(\strpElm) \models \phi $

Input: A game $\Game$, a specification formula $\varphi$, and budget $ \beta $.

$ \kappa \in \K(\Game,\beta)$
Compute $ (\Game,\kappa)$

$ i \in \Ag $ and $ s \in \St$
Compute $ \pun_i((\Game,\kappa)) $

$f_{\exists} \gets \bot $;
$f_{\forall} \gets \top $

${z} \in \{\pun_i(s): s \in \St\}^{\Ag}$
Compute $(\Game,\kappa){[z]}$

there exists $ \pi \in (\Game,\kappa){[z]}$ such that for each $ i \in \Ag, \pay_i(\pi) \geq z_i $

$f_{\exists} \gets \top $

${z} \in \{\pun_i(s): s \in \St\}^{\Ag}$
there exists $\pi \in (\Game,\kappa){[z]}$ such that for each $ i \in \Ag, \pay_i(\pi) \geq z_i \wedge \pi \models \lnot \phi $
$f_{\forall} \gets \bot $

$ (f_{\exists} \wedge f_{\forall}) $$ \mthfun{Accept} $