1 Introduction
Synthesis is the automated construction of systems from their specifications [34]. Modern systems often consist of interacting components. The interaction is modeled by a multi-player game played on a finite graph. In the turn-based setting, the vertices of the game graph are partitioned among the players. A token is placed on an initial vertex, and in each turn, the player that owns the vertex with the token moves it to a successor vertex. Each player has a strategy that directs her how to move the token when it reaches vertices she own. A profile is a vector of strategies, one for each player. The outcome of profile is a play – an infinite path in the game graph, obtained when the players follow their strategies. The goal of each player is to direct the game into an outcome that is optimal from her point of view.
The simplest games are Boolean zero-sum games: the players compete with each other on the satisfaction of contradicting Boolean objectives. In particular, two-player zero-sum games model the interaction between a system that aims to satisfy a given specification and an environment that tries to violate the specification [8]. Researchers have studied several extensions of Boolean zero-sum games. One is to quantitative zero-sum games. There, the objectives or the game graph are multi-valued, and we seek strategies that satisfy the objectives in the highest possible value, maximize rewards, or minimize costs, possibly in a stochastic manner [2, 3, 7, 13, 14, 21, 38]. Another extension is to Boolean non-zero-sum games, namely when the objectives of the players may overlap [16, 36]. There, typical questions concern the stability of the game and the equilibria the players may reach [39]. The most common criterion for stability is the existence of a Nash equilibrium (NE) [30]. A profile of strategies is an NE if no (single) player can benefit from unilaterally changing her strategy. In particular, in rational synthesis, we seek an equilibrium in which the objectives of the players that model the system are satisfied [17, 19].
Anzeige
The two extensions above have been merged in non-zero-sum games with quantitative objectives. Specifically, in [4, 9, 24], the authors add a quantitative layer to LTL and studied rational synthesis for multi-valued extensions of LTL, and in [12, 37], the authors study equilibria in weighted games. The closest to our contribution are non-zero-sum games with multiple \(\omega \)-regular objectives. In particular, [10, 33] study games in which the underlying objectives are ordered, specifying priorities on different objectives.
We introduce and study non-zero-sum multi-player games with weighted multiple objectives. Consider a game graph with vertices in V. An objective in our game is specified by a tuple \(\langle \alpha ,w \rangle \) where \(\alpha =\{\alpha _1,\ldots ,\alpha _m\} \subseteq 2^V\), is a set of underlying Büchi objectives, and \(w: 2^{\alpha }\rightarrow \mathbb {Z}\) is a weight function that maps each subset X of \(\alpha \) to the utility obtained when exactly all the objectives in X are satisfied. More formally, for a play \(\rho \), let \(X \subseteq \alpha \) be the set of objectives in \(\alpha \) that \(\rho \) satisfies; that is, \(\rho \) visits infinitely often exactly all the sets in X. Then, the satisfaction value of the objective \(\langle \alpha ,w \rangle \) in the play \(\rho \) is w(X). We view \(\langle \alpha , w \rangle \) as a maximization objective, and refer to games with weighted multiple Büchi objectives as MaxWB games. Note that each player has her own objective. Thus, a k-player MaxWB game is \({\mathcal {G}}=\langle G,\alpha ,\{w_i\}_{i \in [k]} \rangle \), where for all \(i \in [k]=\{1,\ldots ,k\}\), we have that \(w_i\) is a weight function for Player \(i\).
Weighted objectives enable the user to conveniently prioritize different scenarios. The different objectives in \(\alpha \) may correspond, for example, to different types of grants given by a server or different storage options in the cloud. Using the weight function \(w_i\), Player \(i\) expresses the utility of different combinations of grants, storage options, locations, and more. Negative weights can be used to specify behaviors that are not desired, or assume-guarantee specifications. As a concrete example, consider robots that patrol a warehouse. The robots are operated by different companies, each having its own objectives. The setting can be modeled by a game graph whose vertices correspond to locations in the warehouse. Each robot is assigned with missions that combine the retrieval of items from appropriate shelves and logistical tasks such as repeatedly visiting or avoiding certain charging stations or areas covered by security cameras. Different sets of locations are associated with varying rewards and costs, reflecting diverse priorities related to requested items, specific shelves for retrieval, balance of the traffic in the different zones, and more logistical considerations for each robot.
In [26], the authors study zero-sum games with weighted multiple objectives. There, each objective also includes a threshold \(t \in \mathbb {Z}\), and a player satisfies a Boolean MaxWB (BMaxWB) objective \(\langle \alpha ,w,t \rangle \) if the weight of the satisfied objectives is at least t. The authors solve the problem of deciding the game and analyze its tight complexity and memory requirements. General weight functions enable BMaxWB objectives to express all Muller objectives [18, 29], which specify the exact set of vertices that repeat infinitely often in a play. By giving a positive weight to such sets and negative ones to the other sets, the translation from BMaxWB objectives to Muller objectives is straightforward, and implies that BMaxWB games can be decided in PSPACE [22, 31]. The connection to Muller games also implies a matching lower bound. The study in [26] then focuses on zero-sum BMaxWB games with restricted weight functions, for which the complexity is lower.
Anzeige
We partition the set [k] of players to a set S of system players, whose behavior is controllable, and the set \([k] \setminus S\) of environment players, which are rational and aim to maximize their utility. The main problem we consider, termed Desired NE (DNE, for short), is the existence and finding of stable profiles that satisfy some desired properties. Formally, a profile is stable if it is an S-fixed NE: no player in \([k] \setminus S\) has a beneficial deviation. The DNE problem gets as input a k-player MaxWB game \({\mathcal {G}}\), a set \(S\subseteq [k]\) of system players, and a predicate P describing desired utilities for the players. It returns an S-fixed NE \(\pi \) in \({\mathcal {G}}\) such that the utilities of the players in \(\pi \) satisfy P. The predicate P is given by a Boolean assertion with atoms that refer to the utilities of the players. For example, cooperative rational synthesis [19] is a special case of DNE in which P sets lower bounds on the utilities of the system players.
We start with the case \({\mathcal {G}}\) has general weight functions and show that the PSPACE complexity of zero-sum BMaxWB games is carried over to non-zero-sum MaxWB games. The ordered objectives studied in [33] are sets in a Muller objective, and so our results apply also to the setting studied there, where the tight complexity of finding an NE (a special case of DNE, with \(S=\emptyset \) and \(P=\textbf{true} \)) was left open. We then consider several restrictions on the weight function and the way they influence the expressive power of the weight functions and the complexity of the DNE problem. We consider the following restrictions: (1) Positive weight functions correspond to settings where players are only awarded for satisfying objectives, thus \(w(X) \ge 0\) for all \(X \subseteq \alpha \). (2) Non-decreasing weight functions correspond to settings with free disposal [32], thus for all sets \(X,X' \subseteq \alpha \), if \(X \subseteq X'\), then \(w(X) \le w(X')\). (3) Additive weight functions correspond to settings where the objectives are independent of each other, thus the weight of a set is the sum of the weights of its elements. Accordingly, an additive weight function is given by \(w:\alpha \rightarrow \mathbb {Z}\), and for every \(X\subseteq \alpha \), we have that w(X) is the sum of the weights of the objectives in X.
Studying the DNE problem for the various types of weight functions, we show that a key factor in the complexity is the existence of a memoryless strategy for the minimizing player in the corresponding zero-sum BMaxWB game. In particular, games with a non-decreasing weight functions enjoy this property, and the DNE problem for them is NP-complete. Also, while games with an additive weight function are PSPACE-complete, games with an additive weight function that is almost positive, namely when only one Büchi objective may not be positive, also satisfy the above property, making the DNE problem for them easier. The result is tight, in the sense that we cannot extend it to games in which a fixed number of Büchi objectives is non-positive. Our study completes the picture known for zero-sum BMaxWB games. In particular, the study in [26] concerns only positive additive weight functions, and we show that, surprisingly, (non-positive) additive weight functions can express all Muller objectives. The best translation between the two formalisms, however, is exponential in both directions. Back to non-zero-sum games, we also show that additive weight functions can be manipulated so that for every partition (S, E) of [k], we can make the game (S, E)-polar, in the sense that all the players in S agree on the polarity (i.e., whether it is positive or negative) of each of the underlying objectives, which is dual to the polarity of the objective for the players in E. Thus, the relative weights of the different objectives play a role that is more significant than their polarity.
We demonstrate the application of MaxWB games by introducing multi-player games with payments, where players can incentivize each other to follow strategies that are beneficial for the paying player. Consider for example a supercomputer that gets calculation requests from users. Payments from the users can be used in order to incentivize the supercomputer to perform certain calculations. For simplicity, assume that each player \(i \in [k]\) has a single Büchi objective \(\alpha _i\), with a weight \(R_i \in \text{ I }\) \(\text{ N }\), awarded in case \(\alpha _i\) is satisfied. Then, a game with payments includes a payment function \(p: [k]\times [k]\rightarrow \text{ I }\) \(\text{ N }\) that maps each two players \(i,j\in [k]\) to the amount Player \(i\) commits to pay Player \(j\) when \(\alpha _i\) is satisfied. It is not hard to see that a game with payments can be reduced to a MaxWB game with almost-positive weight functions. Indeed, the weight for each Büchi objective now takes into account both the reward and the payments to and from the other players. For general MaxWB games with payments, we suggest richer payment functions, and a reduction to MaxWB games is possible too. Beyond the application of MaxWB games for synthesizing strategies in games with payments, we study the monetary-based repair of systems, where we synthesize a payment function with which a desired stable outcome exists. Thus, unlike earlier work, where repairs are based on controlling the players [20, 23] or manipulating the objectives [1], our solution adds monetary incentives to the picture, which reflects the way equilibria are often achieved in real life.
Due to the lack of space, some examples and detailed proofs are missing, and are given in the full version, in the authors’ URLs.
2 Preliminaries
2.1 Multi-player games
For \(k\ge 1\), let \([k]=\{ 1,\ldots ,k \}\). A k-player game graph is \(G = \langle \{ V_i \}_{i\in [k]}, v_0, E \rangle \), where \(\{ V_i \}_{i\in [k]}\) are disjoint sets of vertices, each owned by a different player, and we let \(V=\bigcup _{i\in [k]}V_i\). Then, \(v_0 \in V\) is an initial vertex, and \(E \subseteq V\times V\) is a total edge relation, thus for every \(v\in V\), there is at least one \(u\in V\) such that \(\langle v,u \rangle \in E\).
In the beginning of a play in the game, a token is placed on \(v_0\). The players control the movement of the token in vertices they own: In each turn in the game, the player that owns the vertex with the token chooses a successor vertex and moves the token to it. Together, the players generate a play – an infinite path in G. Formally, a strategy for Player \(i\) is a function \(f_i:V^*\cdot V_i\rightarrow V\) that directs her how to move the token in vertices she owns. Thus, \(f_i\) maps prefixes of plays to possible extensions in a way that respects E: for every \(\rho \cdot v\) with \(\rho \in V^*\) and \(v\in V_i\), we have that \(\langle v,f_i(\rho \cdot v) \rangle \in E\). The strategy \(f_i\) is memoryless if it depends only on the current vertex visited, in which case we describe it by a function \(f_i: V_i\rightarrow V\), and is finite-memory if it is possible to replace the unbounded histories in \(V^* \cdot V_i\) by a finite number of memories. A profile is a tuple \(\pi =\langle f_1,\ldots ,f_k \rangle \) of strategies, one for each player. The outcome of a profile \(\pi =\langle f_1,\ldots ,f_k \rangle \) is the play obtained when the players follow their strategies. Thus, \(\textsf{Outcome}(\pi ) = v_0, v_1, v_2, \ldots \) is such that for all \( j \ge 0\), we have that \(v_{j+1}=f_i(v_0,v_1,\ldots ,v_j)\), where \(i\in [k]\) is such that \(v_j\in V_i\).
A zero-sum two-player game is \({\mathcal {G}}= \langle G, \psi \rangle \), where \(G=\langle V_1,V_2,v_0,E \rangle \) is a 2-player game graph and \(\psi \subseteq V^\omega \) is an objective for Player 1, describing the set of outcomes in which Player 1 wins. The objective of Player 2 complements the one of Player 1, thus Player 2 wins when the outcome is not in \(\psi \). A strategy \(f_1\) is a winning strategy for Player 1 if for every strategy \(f_2\) for Player 2, we have that \(\textsf{Outcome}(\langle f_1,f_2 \rangle )\) satisfies \(\psi \). Dually, a strategy \(f_2\) for Player 2 is a winning strategy for Player 2 if for every strategy \(f_1\) for Player 1, we have that \(\textsf{Outcome}(\langle f_1,f_2 \rangle )\) does not satisfy \(\psi \). We say that Player \(i\) wins in \({\mathcal {G}}\) if she has a winning strategy.
Multi-player games may be non zero-sum, thus the objectives of the players may overlap. There, we consider quantitative objectives for the players and stable profiles. Formally, for \(k \ge 1\), a k-player game is a pair \({\mathcal {G}}=\langle G,\{\psi _i\}_{i \in [k]} \rangle \), where G is a k-player game graph, and for every \(i\in [k]\), we have that \(\psi _i:V^\omega \rightarrow \mathbb {Z}\) maps each play \(\rho \) in G to the (possibly negative) utility of Player \(i\) when the outcome is \(\rho \). Formally, the utility of Player \(i\) in a play \(\rho \), denoted \(\textsf{util}_i(\rho )\), is \(\psi _i(\rho )\). Then, for a profile \(\pi \), the utility of Player \(i\) in \(\pi \), denoted \(\textsf{util}_i(\pi )\), is \(\textsf{util}_i(\textsf{Outcome}(\pi ))\).
A profile \(\pi =\langle f_1,\ldots ,f_k \rangle \) is a Nash Equilibrium (NE, for short) [30] if no player can benefit from unilaterally changing her strategy. Formally, for \(i\in [k]\) and a strategy \(f_i'\) for Player \(i\), let \(\pi [i\leftarrow f_i'] = \langle f_1,\ldots ,f_{i-1},f_i',f_{i+1},\ldots ,f_k \rangle \) be the profile in which Player \(i\) deviates to the strategy \(f_i'\). We say that \(\pi \) is an NE if for every \(i\in [k]\) and strategy \(f'_i\), we have that \(\textsf{util}_i(\pi [i\leftarrow f_i']) \le \textsf{util}_i(\pi )\).
We say that two profiles \(\pi \) and \(\pi '\) are equivalent iff for all \(i \in [k]\), we have that \(\textsf{util}_i(\pi )=\textsf{util}_i(\pi ')\). For two sets of objectives \(\{\psi _i\}_{i \in [k]}\) and \(\{\psi '_i\}_{i \in [k]}\) over the same set V of vertices, we say that \(\{\psi _i\}_{i \in [k]}\) and \(\{\psi '_i\}_{i \in [k]}\) are equivalent if for every play \(\rho \in V^\omega \) and \(i \in [k]\), we have that \(\psi _i(\rho )=\psi '_i(\rho )\). Then, two games \({\mathcal {G}}=\langle G,\{\psi '_i\}_{i \in [k]} \rangle \) and \({\mathcal {G}}'=\langle G,\{\psi '_i\}_{i \in [k]} \rangle \) over the same game graph are equivalent iff \(\{\psi _i\}_{i \in [k]}\) and \(\{\psi '_i\}_{i \in [k]}\) are equivalent.
2.2 Weighted multiple objectives
In the definitions above, we used \(\psi \subseteq V^\omega \) and \(\psi _i:V^\omega \rightarrow \mathbb {Z}\) to denote Boolean and quantitative objectives. We now define weighted multiple objectives, which specify \(\psi \) and \(\psi _i\) succinctly.
For a play \(\rho =v_0,v_1,\ldots \), let \(\textit{reach}(\rho )\) denote the set of vertices visited along \(\rho \) and \(\textit{inf}(\rho )\) denote the set of vertices visited infinitely often along \(\rho \). That is, \(\textit{reach}(\rho )=\{ v\in V : \text {there is } i\ge 0 \text { such that } v_i = v \}\), and \(\textit{inf}(\rho )=\{ v\in V : \text {there are infinitely many } i\ge 0 \text { such that } v_i = v \}\). For a set of vertices \(\alpha \subseteq V\), a play \(\rho \) satisfies the Büchi objective \(\alpha \) iff \(\textit{inf}(\rho )\cap \alpha \ne \emptyset \).
A weighted Büchi objective is a pair \(\langle \alpha , w \rangle \), where \(\alpha =\{ \alpha _1,\ldots ,\alpha _m \}\) is a set of m Büchi objectives and \(w: 2^\alpha \rightarrow \mathbb {Z}\) is a weight function that maps subsets of objectives in \(\alpha \) to integer numbers.1 We assume that \(w(\emptyset ) = 0\). We say that w is positive if for all \(X \subseteq \alpha \), we have that \(w(X) \ge 0\). We say that w is non-decreasing if for every two sets \(X,X'\subseteq \alpha \), if \(X \subseteq X'\), then \(w(X)\le w(X')\). In the context of game theory, non-decreasing weight functions are very useful, as they correspond to settings with free disposal, namely when satisfaction of additional objectives does not decrease the utility [32]. Note that since \(w(\emptyset )=0\), a non-decreasing weight function is positive.
A weight function is additive if for every set \(X\subseteq \alpha \), the weight of X equals to the sum of weights of the singleton subsets that constitute X. That is, \(w(X) = \sum _{\alpha _l\in X} w(\{ \alpha _l \})\). An additive weight function is thus given by \(w:\alpha \rightarrow \mathbb {Z}\), and is extended to sets of objectives in the expected way, thus for every \(X\subseteq \alpha \), we have that \(w(X) = \sum _{\alpha _l\in X} w(\alpha _l)\).
For a play \(\rho \), let \(\textsf{sat}(\rho ,\alpha ) \subseteq \alpha \) be the set of objectives in \(\alpha \) that are satisfied in \(\rho \). The satisfaction value of \(\langle \alpha , w \rangle \) in \(\rho \) is then the weight of the set of objectives in \(\alpha \) that are satisfied in \(\rho \), namely \(w(\textsf{sat}(\rho ,\alpha ))\).
Since we view an objective \(\langle \alpha , w \rangle \) as a maximization objective, we refer to games with weighted Büchi objectives as MaxWB games. We assume that the objectives of all the players in the game are defined over the same set of underlying objectives. Thus, a MaxWB game is \({\mathcal {G}}=\langle G,\alpha ,\{w_i\}_{i \in [k]} \rangle \), where for all \(i \in [k]\), we have that \(w_i: 2^\alpha \rightarrow \mathbb {Z}\) is a weight function for Player \(i\). Then, the utility of Player \(i\) in a play \(\rho \) is \(w_i(\textsf{sat}(\rho ,\alpha ))\). Note that since the utilities for the players depend on the set of vertices that appear infinitely often in a play, if \(\pi \) and \(\pi '\) are profiles such that \(\textit{inf}(\textsf{Outcome}(\pi )) = \textit{inf}(\textsf{Outcome}(\pi '))\), then \(\pi \) and \(\pi '\) are equivalent.
A well-studied special case of MaxWB games is when the players have underlying Büchi objectives. There, each player has a single Büchi objective she wishes to satisfy. Formally, for all \(i \in [k]\), there is \(j \in [m]\) such that \(w_i(\alpha _j) > 0\), and for all \(l \in [m] \setminus \{j\}\), we have \(w_i(\alpha _l)=0\). We describe Büchi games by \({\mathcal {G}}=\langle G,\{\langle \alpha _i,R_i \rangle \}_{i \in [k]} \rangle \), where for all \(i \in [k]\), we have that \(\alpha _i\) is the objective she aims to satisfy, and \(R_i \ge 0\) is the reward for the satisfaction.
By adding a threshold to the weight function w, we can make the objective Boolean. Formally, a play \(\rho \) satisfies a Boolean MaxWB (BMaxWB, for short) objective \(\langle \alpha ,w,t \rangle \), for \(t \in \mathbb {Z}\), if \(w(\textsf{sat}(\rho ,\alpha ))\ge t\). By [26], two-player zero-sum BMaxWB games are determined, thus in every game, Player 1 or Player 2 wins.
We define the size of a game graph G as the size |E| of its edge relation, and define the size of an objective \(\psi =\langle \alpha ,w \rangle \) as the size of w, defined as \(\sum _{X \subseteq \alpha : w(X) \ne 0} w(X)\). Note that w can be encoded in |w| bits. In fact, for our upper bounds, the encoding of w(X) can be in either unary or binary. That is, the bounds stay valid even when the encoding of w(X) adds to the length of the input only \(\log w(X)\) bits. When w is additive, our bounds hold also when we define its length by \(\sum _{\alpha _l \in \alpha } w(\alpha _l)\).
2.3 Partially-Fixed Nash-Equilibria with Desired Utilities
We consider a setting in which the players model components of a system and its environment. Technically, we assume that [k] is partitioned to a set \(S \subseteq [k]\) of system players, whose behavior is controllable, and the set \([k] \setminus S\) of environment players, which are rational and aim for maximizing their utility. The basic problem we consider is the existence and finding of stable profiles that satisfy some desired properties.
We refine the notion of NEs to take into account our ability to control the system players. For a set \(S\subseteq [k]\) of system players and a profile \(\pi \), we say that \(\pi \) is an S-fixed NE if no player in \([k] \setminus S\) can benefit from unilaterally changing her strategy. Thus, for every \(i\in [k] \setminus S\) and strategy \(f'_i\), we have that \(\textsf{util}_i(\pi [i\leftarrow f_i']) \le \textsf{util}_i(\pi )\). Desired utilities of a k-player game are specified by a predicate \(P \subseteq \mathbb {Z}^{[k]}\). We describe such predicates by Boolean assertions with atoms of the form \(t_1 \le t_2\), for arithmetic terms \(t_1\) and \(t_2\) defined over \(\{u_1,\ldots ,u_k\} \cup \mathbb {Z}\), where for all \(i \in [k]\), the variable \(u_i\) stands for the utility of Player \(i\). A profile \(\pi \) then satisfies a predicate P if the assignment \(f:\{u_1,\ldots ,u_k\} \rightarrow \mathbb {Z}\) with \(f(u_i)=\textsf{util}_i(\pi )\) satisfies P. For example, the predicate \((u_1 \ge 8) \wedge (u_2 \ge u_3) \wedge (u_3+u_4 \le 20)\) requires the utility of Player 1 to be at least 8, the utility of Player 2 not to be smaller than that of Player 3, and the combined utilities of Players 3 and 4 to be at most 20.
The problem of partially-fixed NE with desired utilities (DNE, for short) gets as input a k-player game \({\mathcal {G}}\), a set \(S\subseteq [k]\) of system players, and a predicate \(P \subseteq \mathbb {Z}^{[k]}\) describing desired utilities. Given \(\langle {\mathcal {G}},S,P \rangle \), the goal is to return an S-fixed NE \(\pi \) in \({\mathcal {G}}\) such that the utilities of the players in \(\pi \) satisfy P. Below, we describe useful instances of the DNE problem.
-
In cooperative rational synthesis [19], the predicate P sets lower bounds on the utilities of the system players. For example, solutions to DNE with \(\langle {\mathcal {G}},\{1\}, u_1 \ge t \rangle \) are 1-fixed NEs in which the utility of the single system player is at least t.
-
Different wellness goals like total or fair wellness [32] can be specified by bounding the differences among the different utilities. For example, the predicate \(\bigwedge _{i \in [k]} ( 2k \cdot { avg} \le k \cdot u_i \le 4k \cdot { avg})\), with \({ avg}=\frac{\sum _{i \in [k]} u_i}{k}\), restricts the distance of each player’s utility from the average utility, and the predicate \(\bigwedge _{i,j \in [k]} (u_i \le 2 u_j)\) restricts the distance between each two players’ utilities.
-
Priorities among players can be specified by predicates like \(\bigwedge _{i\in [k-1]} (u_i \ge u_{i+1})\), which order the utilities, or \(u_1 \ge (u_2 + \cdots + u_k)\), which relates the utilities of sets of players.
We conclude this section with two useful lemmas. In the first, we consider zero-sum games that are used when a player may deviate from her current strategy and all the other players cooperate in order to make such a deviation non-beneficial. Formally, consider a MaxWB game \({\mathcal {G}}=\langle G,\alpha ,\{w_i\}_{i \in [k]} \rangle \), with \(G=\langle \{V_i\}_{i \in [k]},v_0,E \rangle \). For a player \(i\in [k]\), a vertex \(v \in V_i\), and a threshold t, we define the game from v against Player i with objective \((\alpha ,w_i,t)\) as the two-player zero-sum game \({\mathcal {G}}^v_{i,t}\) defined as follows. The game is played on G with initial vertex v, between Player \(i\) (who is Player 1 in \({\mathcal {G}}^v_{i,t}\)) and the players in \([k[\setminus \{i\}\) (who compose Player 2 in \({\mathcal {G}}^v_{i,t}\)). The objective of Player \(i\) is the set of plays in which her utility is at least t. Thus, \({\mathcal {G}}^v_{i,t}=\langle \langle V_i,V \setminus V_i,v \rangle ,\psi \rangle \), with \(\psi =\{\rho : w_1(\textsf{sat}(\rho ,\alpha )) \ge t\}\). The following lemma offers a useful characterization of NEs [17, 36].
Lemma 1
Consider a k-player game \({\mathcal {G}}\), a set \(S\subseteq [k]\), and a predicate \(P \subseteq \mathbb {Z}^{[k]}\). For every path \(\rho \) of G, there is a solution to the DNE problem for \(\langle {\mathcal {G}},S,P \rangle \) that has outcome \(\rho \) iff the \(\rho \) satisfies P and for every player \(i\in [k]\setminus {S}\) and vertex \(v \in V_i \cap \textit{reach}(\rho )\), Player \(i\) loses in the game \({\mathcal {G}}^v_{i,t}\) with \(t=\textsf{util}_i(\rho )+1\).
The second lemma states that when the weight functions are general, the non-zero-sum setting is at least as hard to reason about as the zero-sum setting.
Lemma 2
Given a zero-sum BMaxWB game \({\mathcal {G}}= \langle G, (\alpha , w, t) \rangle \), we can construct weight functions \(w_1\) and \(w_2\) such that Player 1 wins in \({\mathcal {G}}\) iff there is a DNE solution for \(\langle \langle G,\alpha , \{ w_1,w_2 \} \rangle ,\{1\}, u_1 \ge t \rangle \).
3 MaxWB Games
In this section, we study the DNE problem in MaxWB games with general weight functions. Thus, \({\mathcal {G}}=\langle G,\alpha ,\{w_i\}_{i \in [k]} \rangle \) is such that \(w_i: 2^\alpha \rightarrow {\mathbb {Z}}\), for every \(i\in [k]\). The techniques are similar to these used for reasoning about non-zero-sum games with Streett objectives or weighted reachability objectives [12, 36], and we give them for completeness. Essentially, the proof is based on Lemma 1: the DNE solution for \(({\mathcal {G}},S,P)\) has an outcome \(\rho \) such that for every vertex v in \(\rho \) that is owned by a player i not in S, the strategies of the players in \([k] \setminus \{i\}\) make sure that there is no beneficial deviation for Player \(i\) from v. We note that the existence of an NE in MaxWB games (that is, Theorem 1) follows also from the study of NEs in generalized Muller games [33]. Our proof, however, sets the stage to optimal algorithms for finding an NE.
Theorem 1
For every k-player MaxWB game \({\mathcal {G}}\), and set \(S \subseteq [k]\) of system players, there exists an DNE solution for \(\langle {\mathcal {G}},S, \textbf{true} \rangle \).
Clearly, once a predicate P is added, a desired S-fixed NE need not exist. Once, however, there is a DNE solution, there is also one with an outcome of polynomial length:
Theorem 2
Consider a k-player MaxWB game \({\mathcal {G}}\), a set \(S \subseteq [k]\) of system players, and a utility predicate P. If there exists a DNE solution \(\pi \) for \(\langle {\mathcal {G}},S,P \rangle \), then there also exists a DNE solution \(\pi '\) for \(\langle {\mathcal {G}},S,P \rangle \) such that all the following hold.
1.
\(\textsf{Outcome}(\pi ') = \rho _1\cdot \rho _2^\omega \), where \(\rho _1\) and \(\rho _2\) are of polynomial size.
2.
\(\textit{reach}(\textsf{Outcome}(\pi '))\subseteq \textit{reach}(\textsf{Outcome}(\pi ))\).
3.
\(\textit{inf}(\textsf{Outcome}(\pi ')) = \textit{inf}(\textsf{Outcome}(\pi ))\).
We continue to the complexity of the DNE problem. BMaxWB objectives are strongly related to Muller objectives. A Muller objective is defined with respect to a finite set \(\mathcal{C}\) of colors and is a pair \(\psi = \langle \mathcal {F},\chi \rangle \), where \(\mathcal {F}\subseteq 2^{\mathcal{C}}\) specifies desired subsets of colors and \(\chi : V\rightarrow \mathcal{C}\) colors the vertices in V. A play \(\rho \) satisfies \(\psi \) iff the set of colors visited infinitely often along \(\rho \) is in \(\mathcal {F}\). That is, \(\{ i\in \mathcal{C}: \textit{inf}(\rho ) \cap \chi ^{-1}(i)\ne \emptyset \} \in \mathcal {F}\). It is shown in [26] that every BMaxWB objective \(\psi =\langle \alpha ,w,t \rangle \) has an equivalent Muller objective of size \(|\{ X\subseteq \alpha : w(X)\ge t \}|\), and every Muller objective \(\psi =\langle \mathcal {F}, \chi \rangle \) has an equivalent BMaxWB objective of size \(|\psi |\). It follows that Muller games are polynomially reducible to BMaxWB games, and vice versa, and so zero-sum two-player BMaxWB games are PSPACE-complete. As detailed below, this implies a PSPACE completeness also for the DNE problem.
Theorem 3
Given a k-player MaxWB game \({\mathcal {G}}\), a set \(S \subseteq [k]\) of system players, and a utility predicate P, deciding whether there exists a DNE solution for \(\langle {\mathcal {G}},S,P \rangle \) is PSPACE-complete. Hardness in PSPACE already applies for \(k=2\).
4 MaxWB Games with Non-Decreasing Weight Functions
In this section, we study MaxWB games with non-decreasing weight functions. Thus, \({\mathcal {G}}=\langle G,\alpha ,\{w_i\}_{i \in [k]} \rangle \) is such that for all \(i \in [k]\) and \(X,X' \subseteq \alpha \) with \(X\subseteq X'\), we have that \(w_i(X) \le w_i(X')\). We show that every DNE solution for \({\mathcal {G}}\) has an equivalent DNE solution of polynomial size. Thus, while Theorem 2 only bounds the length of the outcome of an equivalent solution, the restriction to non-decreasing function also bounds the memory requirements for the players in the solution, making the problem easier.
Theorem 4
Consider a k-player MaxWB game \({\mathcal {G}}\) with non-decreasing weight functions, a set \(S \subseteq [k]\) of system players, and a utility predicate P. If there exists a DNE solution for \(\langle {\mathcal {G}},S,P \rangle \), then there also exists a DNE solution for \(\langle {\mathcal {G}},S,P \rangle \) of size polynomial in \({\mathcal {G}}\).
We continue to the complexity of the DNE problem. Note that the reduction in Lemma 2 involves negative weight functions, so we cannot apply it. We can still show a lower bound for \(k=2\), but the proof is more complicated and involves a composition and dualization of BMaxWB games.
Theorem 5
Given a k-player MaxWB game \({\mathcal {G}}\) with non-decreasing weight functions, a set \(S \subseteq [k]\) of system players, and a utility predicate P, deciding whether there exists a DNE solution for \(\langle {\mathcal {G}},S,P \rangle \) is NP-complete. Hardness in NP already applies for \(k=2\), positive and additive weight functions, and P that only refers to the utility of Player 1.
Proof
Memberships in NP is similar to the one for the problem of rational synthesis with Boolean Streett objectives [36].
For the lower bound, we describe a reduction from the problem of deciding whether Player 2 wins in a zero-sum BMaxWB game, known to be NP-hard already for positive and additive weight functions and threshold \(t \ge 1\) [26]. Consider a zero-sum BMaxWB game \({\mathcal {G}}= \langle G,\langle w,\alpha ,t \rangle \rangle \), with \(G = \langle V_1,V_2,v_0,E \rangle \). We construct a two-player non-zero-sum MaxWB game \({\mathcal {G}}' =\langle G', \alpha ', \{ w_1,w_2 \} \rangle \) with positive and additive weight functions such that there exists a DNE solution for \(({\mathcal {G}}', \{ 1 \}, \{ u_1 \ge 1 \})\) iff Player 2 wins in \({\mathcal {G}}\),
Intuitively, we define \({\mathcal {G}}'\) so that Player 2 chooses to help Player 1 to have utility 1 iff there is no winning strategy for Player 1 in G. Specifically, the game graph \(G'\) is as follows. From the initial vertex, Player 2 chooses between moving to a self-looped sink \(\bot \), and moving to a copy of G. In the copy of G, Player 2 aims to satisfy the BMaxWB objective of \({\mathcal {G}}\). Note that the original roles of Player 1 and Player 2 in G are switched in its copy in \(G'\). We define the weight functions so that Player 1 has utility 1 if the play reaches \(\bot \) and utility 0 otherwise, and Player 2 has utility \(t-1\) if the play reaches \(\bot \) and utility according to w and the outcome in G otherwise. Since \(t \ge 1\), the weight functions in \({\mathcal {G}}'\) are indeed positive and additive. Let \(S = \{ 1 \}\) and \(P = \{ u_1 \ge 1 \}\). Note that P is satisfied iff the play reaches the sink \(\bot \), thus there exists a DNE solution iff Player 1 can make sure Player 2 cannot benefit from moving to the copy of G, which holds iff Player 1 has a strategy in G that forces the satisfaction value of \(\langle \alpha ,w \rangle \) to be at most \(t-1\). Accordingly, there exists a DNE solution in \({\mathcal {G}}'\) iff Player 2 wins \({\mathcal {G}}\). \(\square \)
5 MaxWB Games with Additive Weight Functions
In this section, we study MaxWB games with additive weight functions. Thus, \({\mathcal {G}}=\langle G,\alpha ,\{ w_i \}_{i \in [k]} \rangle \) is such that for all \(i \in [k]\) and \(\alpha _j\in \alpha \), we have that \(w_i(\alpha _j) \in {\mathbb {Z}}\), and for \(X \subseteq \alpha \), we have that \(w_i(X)=\sum _{\alpha _l \in X} w_i(\alpha _l)\). Note that additive weight functions correspond to cases the objectives are independent of each other. In particular, ordered objectives, as in [10], can be specified using additive weight functions.
In [26], the authors study zero-sum BMaxWB games with positive and additive weight functions. In particular, they show that the problem of deciding the winner is co-NP-complete, thus the games are easier than these with general weight functions. We first complete the picture known for the zero-sum case and study zero-sum BMaxWB games with additive (but not necessarily positive) weight functions. Surprisingly, additive weight functions can express all Muller objectives:
Theorem 6
Consider a Muller objective \(\langle \mathcal {F},\chi \rangle \) defined over a set of colors [m] and vertices in V. There is a set \(\alpha \subseteq 2^V\) of underlying objectives and an additive weight function \(w:\alpha \rightarrow \mathbb {Z}\) such that the objectives \(\langle \mathcal {F},\chi \rangle \) and \(\langle \alpha ,w,0 \rangle \) are equivalent.
Proof
Consider a Muller objective \(\langle \mathcal {F},\chi \rangle \) defined over a set of colors [m], for \(m\in \text{ I }\) \(\text{ N }\). Let \(\alpha = \{ \alpha _C : C\subseteq [m], C\ne \emptyset \}\), where for every set of colors \(C\subseteq [m]\), we have that \(\alpha _C = \bigcup _{i\in C}\chi ^{-1}(i)\). We show that there exists an additive weight function \(w:\alpha \rightarrow \mathbb {Z}\) such that \(\langle \mathcal {F},\chi \rangle \) and \(\langle \alpha ,w,0 \rangle \) are equivalent. Note that the sets \(\alpha _C\) need not be singletons. The important thing is that that weight function w is defined for single objectives in \(\alpha \) and induces an additive function.
Note also that a play \(\rho \) with \(\chi (\textit{inf}(\rho )) = C\) satisfies exactly all the Büchi objectives \(\alpha _{C'} \in \alpha \) such that \(C\cap C' \ne \emptyset \). Accordingly, in order for \(\langle \alpha ,w,0 \rangle \) to be equivalent to \(\langle \mathcal {F},\chi \rangle \), the sum of weights of objectives \(\alpha _{C'}\) such that \(C\cap C' \ne \emptyset \) should be at least 0 when \(C \in \mathcal {F}\), and smaller than 0 otherwise. It is possible to specify these requirements by a system of linear equations that has an integral solution, inducing a matching weight function.
\(\square \)
The number of underlying Büchi objectives in the equivalent MaxWB objective generated in Theorem 6 is exponential in the number of colors. Also, while Muller objectives can refer to all subsets of objectives that are satisfied, such a reference is succinct in additive weight functions, and so the translation of BMaxWB objectives with additive weight functions to Muller objectives is also exponential. Thus, while the two formalisms are as expressive, the best translation between them is exponential in both directions, and we cannot easily lift known results about Muller games to games with MaxWB objectives with additive weight functions. We show that the complexity of MaxWB games with additive weight functions still coincides with the one of Muller games. Thus, the advantage of positive additive weight functions is lost. We start with zero-sum games. Essentially, the upper bound follows from the fact the PSPACE algorithm in [29] does not need an explicit representation of the Muller objective, and the lower bound follows from a careful examination of the PSPACE-hardness proof for Muller games [22], showing that the Muller objective used there can be specified as a BMaxWB objective with an additive weight function of polynomial size.
Theorem 7
Deciding whether Player 1 wins a zero-sum two-player BMaxWB game with an additive weight function is PSPACE-complete.
We continue to non-zero-sum games. The upper bound is similar to the one in Theorem 3, using Theorem 7 for the involved zero-sum BMaxWB games. The lower bound follows from Theorem 7 and Lemma 2.
Theorem 8
Given a k-player MaxWB game \({\mathcal {G}}\) with additive weight functions, a set \(S \subseteq [k]\) of system players, and a utility predicate P, deciding whether there exists a DNE solution for \(\langle {\mathcal {G}},S,P \rangle \) is PSPACE-complete. Hardness in PSPACE already applies for \(k=2\).
6 MaxWB Games with Restricted Additive Weight Functions
In Section 5, we saw that allowing negative weights increases the complexity of the DNE problem in MaxWB games with additive weight functions. Specifically, the complexity jumps from NP to PSPACE. In this section, we examine whether we can allow some use of negative weights in additive weight functions in a way that does not increase the complexity. We consider two cases. The first is when at most one objective is allowed to get a negative weight. The second is when the weights enjoy some polarity, making the setting closer to zero-sum games.
6.1 When at most one objective may be negative
An additive weight function \(w: \alpha \rightarrow {\mathbb {Z}}\) is almost positive if there exists \(l\in [m]\) such that for every \(j\in [m]\setminus \{ l \}\), we have that \(w(\alpha _j)\ge 0\). That is, at most one objective can have a negative weight. Note that different players may have different negative objectives.
In [26], it is shown that a BMaxWB objective with a positive weight function can be translated to an equivalent generalized Büchi objective.
Here, we show that a BMaxWB objective with an almost positive weight function can be translated to an equivalent Streett objective. A Streett objective is a set \(\psi = \{ \langle L_l,R_l \rangle \}_{l\in [m]} \subseteq 2^V\times 2^V\) of pairs of sets of vertices. A play \(\rho \) satisfies \(\psi \) iff for every \(l\in [m]\), if \(\rho \) visits \(L_l\) infinitely often, then it also visits \(R_l\) infinitely often. That is, \(\textit{inf}(\rho )\cap L_l = \emptyset \) or \(\textit{inf}(\rho )\cap R_l \ne \emptyset \). A generalized Büchi objective is a special case of Streett, with \(L_l = V\) for all \(l\in [m]\). The important point for us is that, as is the case with generalized Büchi objectives, zero-sum two-player Streett games are such that if Player 2 wins, then she has a memoryless winning strategy. Thus, handling of the single objective with negative weight involves a transition from generalized Büchi to Streett objectives, but still leaves us in the terrain of games in which Player 2 has a memoryless winning strategy.
Theorem 9
Consider a zero-sum MaxWB game \({\mathcal {G}}\) with an almost-positive weight function. Player 2 wins \({\mathcal {G}}\) iff she has a memoryless winning strategy.
One may be tempted to generalize the result in Theorem 9 to a fixed number of objectives that may have a negative weight. With more than one negative objective, however, a winning strategy of Player 2 may need to direct the outcome of an interaction into different successors of a vertex that repeats in the outcome. For a specific example, see Lemma 3.
Lemma 3
There is a zero-sum BMaxWB game \({\mathcal {G}}\) with an additive weight function in which exactly two objectives have negative weights and such that Player 2 wins \({\mathcal {G}}\), but Player 2 does not have a memoryless winning strategy in \({\mathcal {G}}\).
Theorem 9 enables us to lift the “polynomial DNE solution" property proved in Theorem 4 for non-decreasing weight functions to almost-positive weight functions. In order to also lift the NP solution in Theorem 5, we first need to find a solution in NP for zero-sum games. Guessing a memoryless strategy \(f_2\) is a first step for that, but one also needs to check \(f_2\) in polynomial time. The fact only one objective \(\alpha _l \in \alpha \) may get a negative weight makes it possible. Indeed, we only need to reason about the maximal strongly connected sets of the graph induced by \(f_2\), and its restrictions to vertices not in \(\alpha _l\), which can be done in linear time [35].
Theorem 10
Deciding whether Player 2 wins a zero-sum MaxWB game with an almost-positive weight function is NP-complete.
The considerations in the proof of Theorem 5 can now be applied for games with almost-positive weight functions. In particular, note that the weight function used in the lower bound there is positive and additive, and hence also almost-positive.
Theorem 11
Given a k-player MaxWB game \({\mathcal {G}}\) with almost-positive weight functions, a set \(S \subseteq [k]\) of system players, and a utility predicate \(P\subseteq {\mathbb {Z}}^{[k]}\), deciding whether there exists a DNE solution for \(\langle {\mathcal {G}},S,P \rangle \) is NP-complete. Hardness in NP already applies for \(k=2\).
6.2 Additive Weight Functions with Polarities
Consider a MaxWB game \({\mathcal {G}}= \langle G,\alpha ,\{ w_i \}_{i\in [k]} \rangle \) with an additive weight function. Let \(\alpha =\{\alpha _1,\ldots ,\alpha _m\}\). For an objective \(\alpha _l \in \alpha \) and a set \(A \subseteq [k]\) of players, we say that \(\alpha _l\) is good for A if for all \(i \in A\), we have that \(w_i(\alpha _l)>0\). Likewise, \(\alpha _l\) is bad for A if \(w_i(\alpha _l)<0\) for all \(i \in A\). Finally, \(\alpha _l\) is polar for A if \(\alpha _l\) is good or bad for A.
Consider a partition \(A,B \subseteq [k]\) of the players in [k]; thus \(A \cup B = [k]\) and \(A\cap B = \emptyset \). We say that (A, B) is a natural partition (to coalitions) of [k] if every objective \(\alpha _l \in \alpha \) is polar for A and for B, with dual polarity. That is, either \(\alpha _l\) is good for A and bad for B, or \(\alpha _l\) is bad for A and good for B
Games with a natural partition of [k] to coalitions may seem weaker than general games. Indeed, if (A, B) is a natural partition, it is tempting to merge all the players in A to a single player, aiming for the satisfaction of objectives with a positive polarity for them, and merge all the players in B to a single player, aiming for the satisfaction of the complementary set of objectives. Thus, games with a natural partition to coalitions seem related to zero-sum games.
As we show below, however, the relative weights of the different objectives play a role that is more significant than their polarity. Using these relative weights, we can turn each MaxWB game \({\mathcal {G}}\) to an equivalent game that has a natural partition to coalitions. Moreover, given any partition (A, B) of the players, we can turn \({\mathcal {G}}\) to an equivalent games in which (A, B) is a natural partition to coalitions. Thus, games with natural partitions are by no means easier than general ones.
Theorem 12
Consider a MaxWB k-player game \({\mathcal {G}}= \langle G,\alpha ,\{ w_i \}_{i\in [k]} \rangle \) with an additive weight function. For every partition (A, B) of [k], there is a game \({\mathcal {G}}'\) equivalent to \({\mathcal {G}}\) such that (A, B) is a natural partition to coalitions in \({\mathcal {G}}'\).
Proof
Consider a MaxWB k-player game \({\mathcal {G}}= \langle G,\alpha ,\{ w_i \}_{i\in [k]} \rangle \), and a partition (A, B) of [k]. Let \(m=|\alpha |\). We construct a MaxWB game \({\mathcal {G}}'\) equivalent to \({\mathcal {G}}\) such that (A, B) is a natural partition in \({\mathcal {G}}'\). The game \({\mathcal {G}}'=\langle G,\alpha ',\{ w'_i \}_{i\in [k]} \rangle \) is defined as follows. First, \(\alpha '\) consists of two copies2 of \(\alpha \). For \(l \in [m]\), let \(\alpha _l^1\) and \(\alpha _l^2\) denote the two copies of \(\alpha _l\) in \(\alpha '\). Then, for every player \(i\in A\), we define the weight function \(w_i':\alpha ' \rightarrow \mathbb {Z}\) as follows. Consider an objective \(\alpha _l \in \alpha \).
1.
If \(w_i(\alpha _l) \le 0\), then \(w_i'(\alpha _l^1) = 1\) and \(w_i'(\alpha _l^2) = w_i(\alpha _l)-1\).
2.
If \(w_i(\alpha _l) > 0\), then \(w_1'(\alpha _l^1) = w_i(\alpha _l)+1\) and \(w_i'(\alpha _l^2) = -1\).
Finally, for every player \(i\in B\), we define the weight function \(w_i':\alpha ' \rightarrow \mathbb {Z}\) as follows. Consider an objective \(\alpha _l \in \alpha \).
1.
If \(w_i(\alpha _l) \le 0\), then \(w_i'(\alpha _l^1) = w_i(\alpha _l)-1\) and \(w_i'(\alpha _l^2) = 1\).
2.
If \(w_i(\alpha _l) > 0\), then \(w_i'(\alpha _l^1) = -1\) and \(w_i'(\alpha _l^2) = w_i(\alpha _l)+1\).
Note that for all \(l \in [m]\), the objective \(\alpha _l^1\) is good for A and bad for B, and the objective \(\alpha _l^2\) is bad for A and good for B. Also, \(w_i(\alpha _l)=w'_i(\alpha _l^1)+w'_i(\alpha _l^2)\), and so we can express with \(w'\) the same utilities in \({\mathcal {G}}'\) expressed with w in \({\mathcal {G}}\). \(\square \)
7 Non-zero-Sum Games with Payments
In this section, we study non-zero-sum games in which each player \(i \in [k]\) may commit to pay the other players a certain amount for each of the underlying objectives that are satisfied. Clearly, such payments may incentive the other players to choose strategies that are preferable for Player \(i\).
We first study the setting for Büchi objectives, and then extend to MaxWB objectives. Consider a k-player Büchi game \({\mathcal {G}}=\langle G,\{ \alpha _i \}_{i\in [k]},\{ R_i \}_{i\in [k]} \rangle \). A payment function \(p: [k]\times [k]\rightarrow \text{ I }\) \(\text{ N }\) maps each two players \(i,j\in [k]\) to the amount Player \(i\) commits to pay Player \(j\) when \(\alpha _i\) is satisfied. We require that \(p(i,i) = 0\). When Player \(i\) does not commit to pay more than her reward, thus \(R_i \ge \sum _{j\in [k]} p(i,j)\), we say that p is positive. A k-player Büchi game with payments is a pair \(\langle G,p \rangle \), for a Büchi game \({\mathcal {G}}\) and a payment function p.
The utility of a player in a game with payments \(\langle {\mathcal {G}},p \rangle \) combines her reward in \({\mathcal {G}}\) with the payments she pays and receives from the other players. Formally, for a profile \(\pi \), let \(W(\pi )=\{j \in [k] : \alpha _j \in \textsf{sat}(\textsf{Outcome}(\pi ),\alpha )\}\). Thus, \(W(\pi )\) is the set of objectives satisfied in \(\pi \), which is also the set of players that has to fulfill their payment commitments. Then, the utility of Player \(i\) in \(\pi \) isStability in games with payments is defined with respect to the utilities that take payments into account. Note that the payment function is fixed and payments are not part of the player’s strategies. The DNE problem for games with payments gets as input a game \({\mathcal {G}}\), a payment function p, a set of players \(S\subseteq [k]\), and a utility predicate \(P\subseteq {\mathbb {Z}}^{[k]}\), and has to return an S-fixed NE in \(\langle {\mathcal {G}},p \rangle \) that satisfies P.
$$\textsf{util}_i(\pi )=\left[ \begin{array}{ll} R_i - \sum \nolimits _{j\in [k]} p(i,j) + \sum \nolimits _{j\in W(\pi )} p(j,i) & \text{ if } i \in W(\pi )\text{, }\\ \sum \nolimits _{j\in W(\pi )} p(j,i) & \text{ if } i \notin W(\pi )\text{. } \end{array} \right. $$
Theorem 13
For every k-player Büchi game \({\mathcal {G}}\) and payment function \(p: [k]\times [k]\rightarrow \text{ I }\) \(\text{ N }\), there is an equivalent k-player MaxWB game \({\mathcal {G}}'\) with almost-positive additive weight functions. If p is positive, then \({\mathcal {G}}'\) has positive additive weight functions.
Proof
Let \({\mathcal {G}}= \langle G,\alpha ,\{ R_i \}_{i\in [k]} \rangle \). We define \({\mathcal {G}}' = \langle G, \alpha ,\{ w_i \}_{i\in [k]} \rangle \), where for every \(i\in [k]\), we have that \(w_i(\alpha _i)=R_i - \sum _{j\in [k]} p(i,j)\), and for all \(l \in [k] \setminus \{i\}\), we have that \(w_i(\alpha _l)= p(l,i)\).
The correctness of the construction follows immediately from the definition of the utilities in games with payments. Indeed, for every profile \(\pi \) in G, the utilities of Player \(i\) in \(\pi \) coincide in \(\langle {\mathcal {G}},p \rangle \) and \({\mathcal {G}}'\). \(\square \)
Remark 1
[MaxWB games with payments] The definition of games with payments as well as the reduction in Theorem 13 can be easily extended to MaxWB games. The same way we study different classes of weight functions, one can define different classes of payment functions in MaxWB games. Consider a game \({\mathcal {G}}= \langle G,\alpha ,\{ w_i \}_{i\in [k]} \rangle \). The most general payment function is \(p:[k] \times [k]\times 2^\alpha \rightarrow \text{ I }\) \(\text{ N }\), mapping each two players \(i,j\in [k]\) and set \(X \subseteq \alpha \) of objectives to the amount Player \(i\) pays Player \(j\) when exactly all the objectives in X are satisfied. A payment function is additive if it induced by a function \(p:[k] \times [k] \times \alpha \rightarrow \text{ I }\) \(\text{ N }\), which describe payments for single objectives.
The construction in Theorem 13 can be extended to general MaxWB games. The classes of the weight functions in \({\mathcal {G}}\) and the payment function p influence the class of the weight functions in the MaxWB game obtained from \(\langle {\mathcal {G}},p \rangle \).
\(\square \)
The DNE problem for Büchi games without payments can be solved in polynomial time [36]3. Adding payments involves a transition to the DNE problem for MaxWB games with almost-positive weight functions, which has a computations cost. In Theorem 14 below, we show that this cost is unavoidable, in fact, already for the special case of cooperative rational synthesis.
Theorem 14
Given a k-player Büchi game with payments \(\langle {\mathcal {G}},p \rangle \), a set \(S \subseteq [k]\) of system players, and a utility predicate \(P \subseteq {\mathbb {Z}}^{[k]}\), deciding whether there exists a DNE solution for \(\langle {\mathcal {G}},p,S,P \rangle \) is NP-complete. NP-hardness applies already when p is positive, \(S=\{ 1 \}\), and \(P= \{ x_1\ge 1 \}\).
Proof
For the lower bound, we describe a reduction from 3SAT. Given a 3CNF formula \(\varphi \), we construct a Büchi game \({\mathcal {G}}\) and a positive payment function p such that there exists a DNE solution for \(\langle {\mathcal {G}},p,\{ 1 \}, u_1 \ge 1 \rangle \) iff \(\varphi \) is satisfiable. The idea of the reduction is as follows. Consider a 3CNF formula over variables in X. We define \({\mathcal {G}}\) as a \((2|X|+2)\)-player game among Player 1, Player 2, and literal players – one for each literal over X. Only Player 1 and Player 2 control vertices in the game graph. Initially, Player 2 may choose to direct the game into a sink vertex \(\bot \), which is the objective of Player 1, or proceed to a sub-game in which Player 1 is required to prove that \(\varphi \) is satisfiable. For that, Player 1 has to assign \(\textbf{true} \) to some of the literals – a literal l is assigned \(\textbf{true} \) if Player 1 visits a vertex associated with l infinitely often. The objective of a literal player l is to be assigned \(\textbf{true} \). The payment function p requires a literal player l to pay 1 to Player 2. When \(\varphi \) is satisfied, Player 1 may assign \(\textbf{true} \) to at most |X| literals, bounding the payments that Player 2 receives to |X|. In such a case, Player 2 prefers to go to the sink \(\bot \), and so Player 1 satisfies her objective iff \(\varphi \) is satisfiable.
\(\square \)
7.1 Monetary-based repair of Büchi games
Consider a k-player Büchi game \({\mathcal {G}}= \langle G, \{ \alpha _i \}_{i\in [k]}, \{ R_i \}_{i\in [k]} \rangle \). For a payment function \(p: [k]\times [k]\rightarrow \text{ I }\) \(\text{ N }\) and a set \(S\subseteq [k]\) of system players, we say that p incentivizes \([k]\setminus S\) if \(p(i,j)=0\) for all \(i \in [k]\setminus S\) and \(j \in [k]\). That is, only system players may suggest payments.
In the monetary-based system-repair problem, we are given a k-player game \({\mathcal {G}}\), a set of system players \(S\subseteq [k]\), and a utility predicate \(P\subseteq {\mathbb {Z}}^{[k]}\), and we seek a payment function that incentivizes \([k]\setminus S\) to follow strategies with which P is satisfied. Formally, a repair solution for \(({\mathcal {G}},S,P)\) is a pair \((p,\pi )\), where p is a payment function p that incentivizes \([k]\setminus S\) and \(\pi \) is a DNE solution for \(\langle \langle {\mathcal {G}},p \rangle ,S,P \rangle \). Note that since the system players are under our control (formally, \(\pi \) is an S-fixed NE), they need not be incentivized. Still, p may include transfers within the system players in order to satisfy P.
Theorem 15
Given a k-player game \({\mathcal {G}}\), a set \(S\subseteq [k]\) of system players, and a utility predicate \(P\subseteq {\mathbb {Z}}^{[k]}\), deciding whether there exists a repair solution for \(\langle {\mathcal {G}},S,P \rangle \) is NP-complete. Hardness in NP already applies when \(S = {1}\) and \(P = \{ u_1 \ge 1 \}\).
Proof
For the upper bound, an NP algorithm guesses a payment function p that incentivizes \([k]\setminus S\), and then finds a DNE solution for \(\langle {\mathcal {G}},p,S,P \rangle \), as described in Theorem 14. Note that the sum of payments that a given player offers is bounded by the sum of rewards of all the other players in the game, thus it is sufficient to guess a payment function that is polynomial in the input.
For the lower bound, we describe a reduction from 3SAT. Given a 3CNF formula \(\varphi \) over variables in X, we construct a Büchi game \({\mathcal {G}}\) such that there exist a payment function p that incentivizes \([k]\setminus \{1\}\) and a DNE solution for \(\langle {\mathcal {G}},p,\{ 1 \}, u_1 \ge 1 \rangle \) iff \(\varphi \) is satisfiable.
We define \({\mathcal {G}}\) as a \((2|X|+1)\)-player game among Player 1 and literal players – one for each literal over X. Unlike the reduction in the proof of Theorem 14, here all players own vertices in the game graph. A play in the graph starts by traversing a chain of vertices that ends in a sink \(\bot \) that serves as the objective of Player 1. The vertices along the chain are owned by the literal players, which may direct the play out of the chain, requiring Player 1 to prove that \(\varphi \) is satisfiable. Player 1 uses payments in order to incentivize the literal players to continue in the chain. The game is defined so that a literal player that is assigned \(\textbf{true} \) by Player 1 needs to be incentivized by a payment. Consequently, Player 1 can generate a play along the chain by paying to at most |X| literal players iff \(\varphi \) is satisfiable. Since the reward for Player 1 for reaching \(\bot \) is \(|X|+1\), it follows that there exists a repair solution for \(\langle {\mathcal {G}}, \{ 1 \}, \{ u_1 \ge 1 \} \rangle \) iff \(\varphi \) is satisfiable.
\(\square \)
8 Discussion
A major challenge in automated synthesis is the design of high-quality systems. The specification of such systems combines different aspects of the behavior of the system. Multiple weighted objectives enable a rich and convenient way to specify these combinations. We showed that the different classes of weight functions offer a hierarchy of expressiveness and complexity that is different from the one induced by the different classes of \(\omega \)-regular objectives, and that is very relevant in the context of high-quality synthesis. In particular, it brings the analysis closer to the one used in classic game theory (c.f., [32] Chapter 11). We showed that the different classes of weight functions offer a hierarchy of expressiveness and complexity that is different from the one induced by the different classes of \(\omega \)-regular objectives, and that is very relevant in the context of high-quality synthesis. In particular, it brings the analysis closer to the one used in classic game theory (c.f., [32] Chapter 11).
From a practical point of view, multiple weighted objectives also make it possible to calibrate expenses on different resources. In particular, it enables reasoning about settings in which money can be used as a resource. Such an approach is used, for example, when the system is composed from a library of priced components [6, 28], or when agents need to pay in order to sense a signal [15] or to take an action, as in bidding games [5] or networks with tolls [27]. Here, we suggested to use payments in order to repair systems, by incentivizing the environment to follow a strategy in which the objective of the system is satisfied. It is interesting to study additional types of monetary-based repair in non-zero-sum games, for example when payments are used in order to buy control [25] or generate coalitions [11].
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
