Synthesis of Controllable Nash Equilibria in Quantitative Objective Game

1 Introduction

The synthesis problem for LTL (linear temporal logic) gets as input a specification in LTL and outputs a reactive system that satisfies it - if such exists [Pnueli and Rosner, 1989]. The specification is over input signals, controlled by the environment, and output signals, controlled by the system. The system should satisfy the specification in all environments. The environment with which the system interacts is often composed of other systems. For example, the clients interacting with a server are by themselves distinct entities (which we call agents). In the traditional approach to synthesis, the agents can be seen as if their only objective is to conspire to fail the system. Hence the term "hostile environment" that is traditionally used in the context of synthesis. In real life, however, many times agents have objectives of their own, other than to fail the system. The approach taken in the field of algorithmic game theory [Nisan et al., 2007] is to assume that agents interacting with a computational system are rational; i.e., agents act to achieve their own objectives.

∗The author is thankful for the the financial support of the ERC Advanced Investigator grant 291528 ("RACE") at Oxford.

In [Fisman et al., 2010], Fisman et al. introduced rational synthesis. The input to the rational-synthesis problem consists of LTL formulas specifying the objectives of the system and the agents that constitute the environment. The signals over which the objectives are defined are partitioned among the system and the agents, so that each of them controls a subset of the signals. There are two approaches to rational synthesis. In cooperative rational synthesis, the desired output is a strategy profile such that the objective of the system is satisfied in the computation that is the outcome of the profile, and the agents that constitute the environment have no incentive to deviate from the strategies suggested to them; that is, the profile is a Nash equilibrium (NE) [Nash, 1950]. Thus, in the cooperative setting, we assume that once we suggest to the agents strategies that constitute an equilibrium, they follow them. Then, in non-cooperative rational synthesis, studied in [Kupferman et al., 2016], the desired output is a strategy for the system such that its objective is satisfied in all NE profiles in which the system follows this strategy. Thus, in the non-cooperative setting, the agents are rational, but need not follow a suggested profile. The rational-synthesis problem for LTL in the cooperative setting is 2EXPTIME-complete [Fisman et al., 2010], as is traditional LTL synthesis. In the non-cooperative setting, the best known complexity is 3EXPTIME [Kupferman et al., 2016]. 1

Traditional games in game theory are finite and their outcome depends on the final position of the game [Nisan and Ronen, 1999; Nisan et al., 2007]. In contrast, the systems we reason about maintain an on-going interaction with their environment [Harel and Pnueli, 1985], and reasoning about their behavior refers not to their final state (in fact, we considers non-terminating systems, with no final state) but rather to the language of computations that they generate. While LTL specifications enable the description of rich on-going behaviors, the semantics of LTL is Boolean: a computation may satisfy a specification or it may not. As argued in [Almagor et al., 2016], the Boolean nature of LTL is a real obstacle in synthesis. Indeed, while many systems may satisfy a specification, they may do so at different levels of quality. Consequently, designers would be willing to give up manual design only after being convinced that the automatic procedure that replaces it generates systems of comparable quality. As argued in [Kupferman et al., 2016], the extension of the synthesis problem to the rational setting makes the quantitative setting even more appealing. Indeed, objectives in typical game-theory applications are quantitative, and interesting properties of games often refer to their quantitative aspects. In [Kupferman et al., 2016], the authors add a quantitative layer to LTL and studied rational synthesis for Objective LTL (OLTL, for short). There, each specification is a set Ψ of specifications, and a reward function maps each subset of Ψ to the reward gained when this subset of formulas is satisfied. In the rational synthesis problem for OLTL, the input consists of OLTL specifications for the system and the other agents, and the objective of the system is to maximize its reward with respect to environments that are in an equilibrium.

1 The complexity specified in [Kupferman et al., 2016] is actually 2EXPTIME-complete, yet the complexity analysis there misses one alternation between strategy quantifiers in the strategy-logic formula to which the problem is reduced. Taking this additional alternation into account, the complexity goes up to 3EXPTIME.

We study the rational-synthesis problem for a much stronger quantitative formalism, namely LTL[F]. The logic LTL[F] is a multi-valued logic that augments LTL with quality operators [Almagor et al., 2016]. The satisfaction value of an LTL[F] formula is a real value in [0, 1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. The quality operators in F can prioritize different scenarios or reduce the satisfaction value of computations in which delays occur. For example, as in earlier work on multi-valued extensions of LTL (c.f., [Faella et al., 2008]), the set F may contain the min{x, y}, max {x, y}, and 1-x functions, which are the standard quantitative analogues of the ∧, ∨, and ¬ operators. The novelty of LTL[F] is the ability to manipulate values by arbitrary functions. For example, F may contain the weightedaverage function ⊕λ. The satisfaction value of the formula ϕ ⊕λ ψ is the weighted (according to λ) average between the satisfaction values of ϕ and ψ. This enables the specification of the quality of the system to interpolate different aspects of it. As an example, consider the LTL[F] formula G(req → (grant ⊕23 Xgrant)). The formula states that we want requests to be granted immediately and the grant to hold for two transactions. When this always holds, the satisfaction value is 23 + 13 = 1. We are quite okay with grants that are given immediately and last for only one transaction, in which case the satisfaction value is 2 3 , and less content when grants arrive with a delay, in which case the satisfaction value is 13 .

The extension to LTL[F] significantly strengthens the framework of rational synthesis. In addition, we study the stability of rational synthesis and additional game- and socialchoice theoretic aspects of it. We generalize the setting to an arbitrary partition of the set of agents to controllable and uncontrollable ones. In particular, the case there are no controllable agents corresponds to interactions with no authority. We refine the stability-inefficiency measures of price of stability (PoS) [Anshelevich et al., 2008] and price of anarchy (PoA) [Koutsoupias and Papadimitriou, 2009; Papadimitriou, 2001] to a setting where some of the agents are controllable. Essentially, these notions measure how much we lose from the absence of a central authority by comparing the utility of a social-optimum profile (that is, a profile that maximizes the profits of all agents together) with that of NE profiles. Our refinement enables a distinction between cases where the behavior of the controllable agents is fixed and cases it is not.

Studying the stability of rational synthesis, we prove that a rational-synthesis game need not have an NE, and that for some utility functions, the PoS and PoA may not be bounded. We relate the cooperative and non-cooperative settings with the two stability-inefficiency measures. In the cooperative setting, we may suggest to the agents a best NE, thus the cooperative setting corresponds to the PoS measure. On the other hand, in the non-cooperative setting, the agents may follow the worst NE, which corresponds to the PoA measure. This settles a discussion in the community about the necessity of both settings, and also implies that the profit to the controllable components in the non-cooperative setting may be unboundedly smaller than the profit in the cooperative setting.

We solve decision problems for rational synthesis with LTL[F] objectives. Our algorithms make use of strategy logic and decision procedures for it [?; Mogavero et al., 2010; 2012; 2014]. Thus, we are able to handle the richer quantitative setting using existing tools. In particular, we show that the cooperative and non-cooperative versions of LTL[F] rational synthesis are 2EXPTIME-complete and in 3EXPTIME, respectively, and that so are the problems of calculating the various stability-inefficiency measures, and other measures that quantify the game and its outcomes. Thus, the complexity of rational synthesis in the quantitative setting is not harder than the best known complexity in the Boolean setting. Due to the lack of space, some of the proofs are omitted and can be found in the full version, in the authors' URLs.

Related Work In [Gutierrez et al., 2015; Wooldridge et al., 2016], the authors introduce the problems of E-Nash and A-Nash for different classes of iterated games, which correspond to the special cases of cooperative and non-cooperative rational synthesis, respectively, in which there is no controllable player, showing that the problems are 2EXPTIMEcomplete. These problems have been analyzed also in different settings, e.g., imperfect information [Gutierrez et al., 2016; 2018], finite traces goals [Gutierrez et al., 2017b], and lexicographic objectives [Gutierrez et al., 2017a]. In [Condurache et al., 2016], the authors analyze the rational synthesis problem for qualitative goals whose complexity ranges from simple reachability to the full power of ω-regular expressions. In [Almagor et al., 2015], the authors study repair of specifications in multi-player games, where the goal is to reach specifications in which the uncontrollable players are in an NE, in both a cooperative and non-cooperative setting.

2 Preliminaries

The Temporal Logic LTL[F] The linear temporal logic LTL[F], introduced in [Almagor et al., 2016], generalizes LTL by replacing the Boolean operators of LTL with arbitrary functions over [0, 1]. The logic is actually a family of logics, each parameterized by a set F of functions.

Syntax. Let AP be a set of Boolean atomic propositions, and let F ⊆ {g : [0, 1]m → [0, 1] | m ∈ N} be a set of functions over [0, 1]. Note that the functions in F may have different arities. An LTL[F] formula is one of the following:

• True, False, or p, for p ∈ AP.
• g(ϕ1, ..., ϕm), Xϕ1, or ϕ1Uϕ2, for LTL[F] formulas ϕ1, . . . , ϕm and a function g ∈ F.

Semantics. The semantics of LTL[F] formulas is defined with respect to infinite computations over AP. A computation is a word ρ = ρ0, ρ1, . . . ∈ (2AP )ω . We use ρi to denote the suffix ρi, ρi+1, . . .. The semantics maps a computation ρ and an LTL[F] formula ϕ to the satisfaction value of ϕ in ρ, denoted [[ρ, ϕ]]. The satisfaction value is defined inductively as described in Table 1 below. 2

It is not hard to prove, by induction on the structure of the formula, that for every computation ρ and formula ϕ, it holds that [[ρ, ϕ]] ∈ [0, 1].

The logic LTL coincides with the logic LTL[F] for F that corresponds to the usual Boolean operators. For simplicity, we use the common such functions as abbreviation, as described below. In addition, we introduce notations for some useful functions. Let x, y, λ ∈ [0, 1]. Then,

To see that LTL indeed coincides with LTL[F] for F = {¬, ∨, ∧}, note that for this F, all formulas are mapped to {0, 1} in a way that agrees with the semantics of LTL.

Lemma 1 ([Almagor et al., 2016]). For every LTL[F] formula ϕ there exists a finite set V (ϕ) ⊆ [0, 1] of possible satisfaction values, such that for every computation ρ, it holds that [[ρ, ϕ]] ∈ V (ϕ) and |V (ϕ)| = 2O(ϕ) .

2 The observant reader may be concerned by our use of max and min where sup and inf are in order. As proved in [Almagor et al., 2016], there are only finitely many satisfaction values for a formula ϕ, thus the semantics is well defined.

The Rational-Synthesis Game Consider sets C and U of controllable and uncontrollable agents, respectively. Let A = C ∪ U. The rational-synthesis game (RS-game, for short) is played among the agents in A. For i ∈ A, agent i assigns values to a set Xi of Boolean atomic propositions. For all i ̸= j ∈ A, we have that Xi ∩Xj = ∅. Let X = ⋃i∈A Xi. Each agent i ∈ A has an objective - an LTL[F] formula ϕi over X.

A strategy for agent i is a function πi : (2X )∗ → 2Xi , mapping the history of the computation so far to an assignment to the atomic propositions of agent i. Let Πi be the set of possible strategies for agent i. A profile is a vector of strategies, one for each agent. Let Π =×i∈A Πi denote the set of all possible profiles. We assume that all agents move together. That is, given a profile P ∈ Π, the computation generated when all the agents follow their strategies in P is ρP = x1, x2, x3, . . . ∈ (2X )ω , where for all j ≥ 0, we have xj = ⋃i∈A πi(x1, x2, . . . , xj-1). We refer to ρP as the outcome of P. For i ∈ A, the profit of agent i in the profile P, denoted profiti(P), is the satisfaction value of ϕi in ρP . For a subset of the agents B ⊆ A, a partial profile is a vector of strategies for the agents in B, and we let ΠB =×i∈B Πi. For a profile P we denote by P|B ∈ ΠB its restriction to the agents in B. A profile P ∈ Π agrees with a partial profile P ′ ∈ ΠB if P|B = P ′ .

In addition to the profits of the individual agents, we are interested in the welfare of the controllable agents (typically, they model the authority) and of the society as a whole. A utility function is a function utility : [0, 1]|A| → [0, 1], which maps the profits of the agents to an overall utility of the society. For convenience, we sometimes refer to the utility function as utility : Π → [0, 1], namely as one that operates on profiles rather than on the vector of profits these profiles induce.

Remark 1. The restriction of the range of utility to [0, 1] is only to conform with the semantics of LTL[F]. Indeed, by Lemma 1, the domain of utility is finite, hence any range can be normalized to [0, 1]. We can thus view utility as an LTL[F] formula ϕutility, defined as ϕutility = utility(ϕ1, . . . , ϕk) where A = {1, . . . , k}.

Example 1. The richness of LTL[F] allows us to capture well-studied utility functions. We demonstrate this on several wellness objectives [Nisan et al., 2007]. Consider a subset B ⊆ A = {1, . . . , k}.

• In the B-utilitarian function, the utility is the sum of the profits of all the agents in B. By normalizing, this can be captured in LTL[F] by introducing the function utility(v1, . . . , vk) = ∑i∈B vi |B| .
• In the B-egalitarian function, the utility is the minimum among the profits of the agents in B. We capture this by utility(v1, . . . , vk) = mini∈B{vi}.
• The anti-B-utilitarian social welfare function concerns minimizing the social welfare of a subset of the hostile agents, and is captured by the function utility(v1, . . . , vk) = 1 - ∑i∈B vi |B| .
• The anti-B-egalitarian social welfare function again

concerns hostile agents, this time minimizing their lowest utility. We capture this by utility(v1, . . . , vk) = 1 - mini∈B{vi}.

For a profile P, an uncontrollable agent i ∈ U, and a strategy π′i ∈ Πi, let P[i ← π′i ] denote the profile obtained from P by replacing the strategy for agent i by π′i . A profile P ∈ Π is a controllable Nash equilibrium (CNE) if no uncontrollable agent can benefit from unilaterally deviating from his strategy in P to another strategy; i.e., for every agent i ∈ U and every strategy π′i ∈ Πi, it holds that profiti(P [i ← π′i ]) ≤ profiti(P ).

Definition 1 (Rational Synthesis). Consider a game G with agents A = C ∪ U, objectives ϕi for every agent i ∈ A, and a utility function utility : Π → [0, 1]. We are given a utility threshold t ∈ [0, 1], and for every agent i ∈ C we are also given a profit threshold ti ∈ [0, 1]. The weak (cooperative) rational synthesis problem is to synthesize a partial profile P C ∈ ΠC for the controllable agents, such that there exists a CNE P that agrees with P C , utility(P) ≥ t ,and for every i ∈ C, it holds that profiti(P) ≥ ti. The strong (non-cooperative) rational synthesis problem is to synthesize P C ∈ ΠC such that for all CNEs P that agree with P C , we have that utility(P) ≥ t and for every i ∈ C, it holds that profiti(P ) ≥ ti.

Consider a utility function utility : Π → [0, 1], a social optimum (SO, for short) is a profile that maximizes the utility. We denote its utility by OPT. Thus, OPT = maxP∈Π utility(P). It is well known that decentralized decision-making may lead to sub-optimal solutions from the point of view of society as a whole. We quantify the inefficiency incurred due to self-interested behavior according to the price of stability (PoS) and price of anarchy (PoA) [Nisan et al., 2007, Chapter 17] measures. The PoS measures the best-case inefficiency of a Nash equilibrium, while the PoA is the worst-case inefficiency of a Nash equilibrium. Traditionally, PoS (resp. PoA) is the ratio between OPT and the maximal (resp. minimal) NE in the game. In a setting where some of the agents are controllable, however, things become more intricate. In the following we consider two definitions of PoS and PoA for our setting.

Consider a partial profile P C ∈ ΠC. A P C -restricted social optimum (SO(P C ), for short) is a profile that agrees with P C and maximizes the utility. We denote its utility by OPT(P C ). Thus, OPT(P C ) = max{utility(P) : P|C = P C }. We denote by ΥG(P C ) the set of CNEs in G that agree with P C . Thus, P ∈ ΥG(P C ) iff P is a CNE and P|C = P C . Let ΥG denote the set of all CNEs in G.

Definition 2 (Price of Stability and Price of Anarchy). Let G be a family of games among controllable and uncontrollable agents, and let G be a game in G with sets C and U of agents.

• The uncontrollable price of stability of G is the ratio between the utility of the SO and the maximal utility of a CNE of G. That is, UPoS(G) = OPT maxP∈ΥG utility(P ) .
• The uncontrollable price of anarchy of G is the ratio between the utility of the SO and the minimal utility of a CNE of G. That is, UPoA(G) = OPT minP∈ΥG utility(P ) .
• The controllable price of stability of G is the minimal ratio between the utility of the SO and the maximal utility of a CNE in a fixed profile for the agents in C. That is,

• The controllable price of anarchy of G is the minimal ratio between the utility of the SO and the minimal utility of a CNE in a fixed profile for the agents in C. That is,

Intuitively, while in the controlled definitions the controlled agents fix their strategies in the SO and the CNE, in the uncontrollable ones they may use different strategies in each of the profiles.

Remark 2. In the definitions above, if the set of CNEs in the denominator is empty, or the denominator equals 0, we treat the value as ∞.

Lemma 2. For every game G, it holds that CPoS(G) ≤ UPoS(G) and CPoA(G) ≤ UPoA(G).

Proof. Consider a profile P C ∈ ΠC for which maxP∈ΥG(P C ) utility(P) = maxP∈ΥG utility(P). Then, clearly OPT(P C ) ≤ OPT , implying that

from which we conclude that CPoS(G) ≤ UPoS(G).

The proof that CPoA(G) ≤ UPoA(G) is analogous.

3 On the Stability of the RS Game

Theorem 1. There is an RS game with no CNE.

Proof. The theorem holds already for Boolean games [Harrenstein et al., 2001], no controllable agents, and the average utility function. Let X1 = {p}, X2 = {q}, ϕ1 = p XOR q, and ϕ2 = ¬(p XOR q). There is no CNE, as both agents 1 and 2 can always deviate to a strategy that results in a computation that satisfies their objective. Formally, for every profile P, if πP |= ϕ1, then agent 2 can deviate to a strategy in which the value of q is flipped, resulting in a profile P ′ for which πP ′ |= ϕ2, and similarly for the case πP |= ϕ2, where agent 1 has a beneficial deviation.

We now turn to consider stability inefficiency, and show that the prices of stability and anarchy are in general unbounded. The result holds already for games with no controllable agents. Note that there, the UPoS and CPoS measures coincide, and we denote them by PoS, and similarly for PoA.

Theorem 2. The PoA and PoS in the RS game are unbounded: For every k ≥ 2 and ϵ > 0, there exists a k-agent RS game GA such that PoA(GA) ≥ 1ϵ , and a k-agent RS game GS such that PoS(GS) ≥ 1-ϵ ϵ .

Proof. In both GA and GS, agent i, for 1 ≤ i ≤ k, controls an atomic proposition xi. In both, the utility function gives a profit of ϵ to agent k for satisfying her objective, a profit of

1-ϵ k-1 to agent i, for 1 ≤ i ≤ k-1, for satisfying her objective, and sums the profits of all agents.

Consider first GA. There, the objective of agent i, for 1 ≤ i ≤ k - 1, is xi ∧ ¬xk, and the objective of agent k is xk ∨ (∧k-1 i=1 xi). The profile in which xk = false and xi = true for all 1 ≤ i ≤ k - 1 is an SO in which all objectives are satisfied, thus OPT(GA) = 1. The profile in which xk = true and xi = false for every 1 ≤ i ≤ k - 1 is a CNE in which only agent k satisfies her objective. Thus, the utility in this profile is ϵ. Hence, PoA(GA) ≥ 1ϵ .

Consider now GS. There, the objective of agent i, for 1 ≤ i ≤ k - 1, is ∧ki=1 xi, and the objective of agent k is ∧k-1 i=1 xi ∧ ¬xk. In the profile in which xi = true for all 1 ≤ i ≤ k, agents 1, . . . , k - 1 satisfy their objectives and agent k does not. Thus, OPT(GS) ≥ 1 - ϵ. On the other hand, the only CNE profile is the one in which all x1, . . . , xk-1 are true and xk = false. There, only agent k satisfies her objective, thus the utility of the only CNE is ϵ. Thus, PoS(GS) ≥ 1-ϵ ϵ .

Note that while the objectives used in the games in the proof of Theorem 2 are LTL formulas, the utility function is not uniform. Alternatively, we could have defined a uniform utility function and use LTL[F] quality operators in order to weight the agents differently.

Finally, note that the SO profile in the game GA described in the proof of Theorem 2 is a CNE Since we can add a controllable agent whose objective is to maximize the number of satisfied uncontrollable agents, we can conclude with the following.

Theorem 3. The ratio between the PoS and PoA is unbounded, and so is the ratio between the profit of the controllable agents in the weak and strong settings of rational synthesis.

4 Decision Procedures for RS

In this section we solve several decision problems related to rational synthesis. Our main tools are decision procedures for Strategy Logic, and the translation of LTL[F] to automata.

Strategy Logic [Mogavero et al., 2014] (SL, for short) is a logic that allows to quantify over strategies in games as explicit first-order objects. Intuitively, such quantification, together with a syntactic operator called binding, enables the formula to quantify restricted classes of strategy profiles, inducing a subset of paths in which a temporal specification needs to be satisfied.

From a syntactic point of view, SL is an extension of LTL with disjoint sets of strategy variables V0, . . . , Vk, where Vi is a set of strategy variables for agent i, existential (〈〈xi〉〉) and universal ([[xi]]) strategy quantifiers, and a binding operator of the form (i, xi), which couples an agent i with one of its variables xi ∈ Vi.

We first introduce some technical notation. For a tuple t = (t0, . . . , tk), we denote by t[i ← d] the tuple obtained from t by replacing the i-th component with d. We use ⃗x as an abbreviation for the tuple (x0, . . . , xk) ∈ V0 × . . . × Vk. By 〈〈⃗x〉〉 = 〈〈x0〉〉 . . . 〈〈xk〉〉, [[⃗x]] = [[x0]] . . . [[xk]], and ♭(⃗x) = (0, x0) . . . (k, xk) we denote the existential and universal quantification, and the binding of all the agents to the strategy profile variable ⃗x, respectively. Finally, by ♭(⃗x-i, yi) = (0, x0) . . . (i, yi) . . . (k, xk) we denote the changing of binding for agent i from the strategy variable xi to the strategy variable yi in the global binding ♭(⃗x).

Here we define and use a slight variant of the Boolean-Goal fragment of SL, namely SL[BG], introduced in [Mogavero et al., 2014]. Formulas in SL[BG] are defined with respect to the set AP of atomic proposition, the set A of agents, and sets Vi of strategy variables for agent i ∈ A. The set of SL[BG] formulas is defined by the following grammar:

where, p ∈ AP is an atomic proposition and xi ∈ Vi is a variable for agent i.

The LTL part has the classical meaning. The formula 〈〈xi〉〉ϕ states that there exists a strategy for agent i such that the formula ϕ holds. The formula [[xi]]ϕ states that, for all possible strategies for agent i, the formula ϕ holds. Finally, the formula ♭(⃗x)ϕ states that the formula ϕ holds under the assumption that the agents in A adhere to the strategy evaluation of the variable xi coupled in ♭(⃗x).

For a more detailed definition of the semantics, the reader is referred to [Mogavero et al., 2014]

The alternation depth of an SL formula is the maximum number of quantifier switches 〈〈xi〉〉[[xj]] or [[xi]]〈〈xj〉〉 in the formula. As in first-order logic, the alternation depth plays an important role in the complexity:

Theorem 4. [Mogavero et al., 2014] The model-checking problem for SL[BG] can be solved in (d + 1)EXPTIME, with d being the alternation depth of the specification.

For LTL[F], we use the following:

Theorem 5. [Almagor et al., 2016] Let ϕ be an LTL[F] formula and V ⊆ [0, 1] be a predicate.

1. There exists a nondeterministic generalized-B¨uchi automaton Aϕ,V such that for every computation ρ ∈ (2AP )ω , it holds that [[ρ, ϕ]] ∈ V iff Aϕ,V accepts ρ. Furthermore, Aϕ,V has at most 2(|ϕ|2 ) states and its index is at most |ϕ|.
2. There exists an LTL formula Bool(ϕ, V ), of length at most exponential in ϕ, such that for every computation ρ ∈ (2AP )ω , it holds that [[ρ, ϕ]] ∈ V iff ρ |= Bool(ϕ, V ).

A particularly useful case of Theorems 5 is when V = [t, 1] (resp. V = [t, t]) for some threshold t. In this case, we denote Bool(ϕ, V ) by ϕ≥t (resp. ϕ=t ).

Solving Rational Synthesis We now turn to show how to solve the RS problem. Our solution relies on a combination of techniques for LTL[F] and SL. We first reduce the RS problem into a simpler form.

An RS game is simple if A = {α0} ∪ U, where α0 is a single controllable agent and its objective is a (Boolean) LTL formula ϕ0 with threshold t0 = 1. In addition, the game does not have a utility function; i.e., it is a constant function that can be ignored when solving the problem. It is not hard to transform a given RS game G into a simple one:

Lemma 3. Given an RS game G with LTL[F] objectives, we can construct a simple game G′ with LTL[F] objectives such that G has a solution for weak/strong RS iff G′ has a solution for weak/strong RS. Moreover, a solution G can be extracted from a solution in G′ .

We now solve the RS problems for simple games.

Theorem 6. Solving a simple weak or strong RS game with LTL[F] objectives can be reduced to model-checking an SL[BG] formula of alternation depth 1 or 2, respectively.

Proof. For an agent i ∈ U and its LTL[F] objective ϕi, consider the SL[BG] formula with free variables ⃗y and ⃗ y′ defined as Φi(⃗y, ⃗ y′ ) = ∧t∈V (ϕi) (♭(⃗y)ϕ=t i → ♭(⃗ y′ )ϕ≤t i ), and stating that, for every threshold value t, whenever the value of ϕi on the run generated by the profile ⃗y is t, then the value of ϕi on the run generated by the profile ⃗ y′ is less or equal than t. Observe that, by means of this formula, we can express the fact that ⃗y is an NE over the uncontrollable agents as ϕNE(⃗y) = [[⃗x]] ∧i∈U Φi(⃗y, (⃗y-i, xi)).

Now, we can specify solutions to the weak and strong RS problems by the following formulas: 3

• ΦwRS = 〈〈⃗yα0 〉〉〈〈⃗yU〉〉(ϕNE(⃗y) ∧ ♭(y)ϕ≥1 0 ), and
• ΦsRS = 〈〈⃗yα0 〉〉[[⃗yU ]](¬ϕNE(⃗y) ∨ ♭(y)ϕ≥1 0 ).

Note that that ΦwRS and ΦsRS are SL[BG] formulas of alternation depth at most 1 and 2, respectively. Indeed, the formula ϕNE(⃗y) contains only a sequence of universal quantifications that, combined with the existential quantifications on top of the formula ΦwRS , gives an alternation depth 1. For the case of strong RS, the formula ¬ϕNE contains a sequence of existential quantifications that, combined with the quantifications on top of ΦsRS , produces an alternation dept of 2.

Thus, weak and strong RS is reduced to model checking the SL formulas ΦwRS and ΦsRS , respectively.

We should, however, take care when analyzing the complexity of the procedure, for two reasons: first, the formulas Φi(⃗y, ⃗ y′ ), which occur in ΦwRS , involve a conjunction over the set of satisfaction values of every ϕi, and second, the formulas ϕ=t i and ϕ≤t i , as well as ϕ≥1 0 , may themselves be of exponential length, as per Theorem 5(2).

To overcome these additional exponential blow-ups, we proceed as follows. First, we notice that the model-checking algorithm in [Mogavero et al., 2014, Lemma 5.6] translates LTL into automata. Theorem 5(1) allows us to perform a similar translation from LTL[F] with only a single exponential blowup. To address the exponential conjunction in Φi(⃗y, ⃗ y′ ), we use universal automata, rather than nondeterministic ones. Thus, we take the intersection of an exponential number of universal automata of size exponential. The result is exponential, and we can then proceed with the algorithm of [Mogavero et al., 2014].

3 For simplicity, we assume that ⃗ yα0 and ⃗ yU are the vectors of the controllable and uncontrollable agents, respectively.

Hence, the overall complexity is that of exponentially many iterations of a doubly or triply exponential procedure, which remains doubly or triply exponential, respectively.

Combining Lemma 3, Theorem 6, Theorem 4, and the blow-ups and complexities in their proofs, we get a 2EXPTIME upper bound to the weak and a 3EXPTIME upper bound to the strong RS problems with LTL[F] objectives. A matching lower bound for the weak RS follows from hardness in 2EXPTIME to the problem for LTL [Kupferman et al., 2016].

Corollary 1. The weak and strong RS problems with LTL[F] objectives are 2EXPTIME-complete and in 3EXPTIME, respectively.

Computing PoS and PoA In this section we consider the problem of computing the stability measures UPoS, UPoA, CPoS and CPoA for an RS game G. Since the range of the utility function is finite, the possible values of the stability measures are also finite. We therefore focus on the decision version of the problem, namely deciding whether e.g., UPoS(G) ≤ t for a given threshold t. We show that while computing UPoS and UPoA can be reduced to the RS problem, computing CPoS and CPoA is more involved, as we have to go over all possible profiles of the controllable agents.

We start with the uncontrollable measures (i.e., UPoS and UPoA), and compute their value by separately computing OPT and maxP∈ΥG utility(P) (for UPoS) or minP∈ΥG utility(P) (for UPoA), as described below.

Theorem 7. Given an RS game G with LTL[F] objectives and a threshold t, deciding whether UPoS(G) ≤ t is 2EXPTIME-complete, while deciding whether UPoA(G) ≤ t can be solved in 3EXPTIME.

Proof. We consider the case of UPoS(G), handling UPoA(G) is analogous. Thus, we want to decide whether OP T maxP∈ΥG utility(P) ≤ t. We start by computing OPT, which amounts to computing the maximal satisfaction value of the LTL[F] formula utility(ϕ0, . . . , ϕn), where ϕ0, . . . , ϕn are the objectives for the players. By [Almagor et al., 2016], this can be done in PSPACE. Once OPT is computed, it remains to decide whether maxP∈ΥG utility(P) ≥ OPT t . This amount to solving the weak RS problem for G with threshold OP T t for the utility, and no thresholds (i.e., threshold 0) for the players.

The controllable setting poses a bigger challenge, as we have to fix the profile P C with which we compute OP T (P C ) and e.g., maxP∈ΥG(P C ) utility(P). We address this by formalizing the problem in SL.

Theorem 8. Given an RS game G with LTL[F] objectives and a threshold t, deciding whether CPoS(G) ≤ t is 2EXPTIME-complete, while deciding whether CPoA(G) ≤ t can be solved in 3EXPTIME.

Proof. We consider here the case of CPoS(G), handling CPoA(G) is similar. Thus, we want to decide whether there is a partial profile P C ∈ ΠC

such that OP T (P C ) maxP∈ΥG(PC) utility(P) ≤ t. Consider the set Range(utility) = {u1, . . . , um} of possible values of utility. By Lemma 1, we have that m is single exponential in the description of G. Let T = {(t1, t2) : t1, t2 ∈ Range(utility) ∧ t1/t2 ≤ t}. Then, CPoS(G) ≤ t iff there exist (t1, t2) ∈ T and a partial profile P C ∈ ΠC such that OPT(P C ) ≤ t1 and maxP∈ΥG(P C ) utility(P) ≥ t2. Equivalently, the latter condition means that there exists a CNE P ∈ Π that agrees with P C and for which utility(P) ≥ t2.

Accordingly, given (t1, t2) ∈ T, we can formulate the above in SL as follows: ΦCPoS (t1, t2) = 〈〈⃗xC 〉〉([[⃗yU ]]♭(xC , yU )ϕ<t1 0 ∧ 〈〈⃗zU〉〉♭(xC, zU)(ϕNE(zU) ∧ ϕ>t2 0 )). Finally, we can decide whether CPoS(G) ≤ t by model checking the formula ∨(t1,t2)∈T ΦCPoS (t1, t2). Note that this can be done in 2EXPTIME using similar arguments as those made in Section 4.

Remark 3. Recall the measures of B-utilitarian and Begalitarian (and their anti- variants) [Nisan et al., 2007] discussed in Example 1. As demonstrated there, for every game with LTL[F] objectives, and every measure ν, we can describe the utility function that corresponds to ν by an LTL[F] formula of linear size. Hence, calculation of the measures can be reduced to solving an RS game and is between 2EXPTIME and 3EXPTIME, according to which kind of RS is required to be used.

Acknowledgments

We are grateful to Bastien Maubert for the careful reading and for detecting an error in the complexity analysis of the strong rational-synthesis problem in an earlier version of this paper.