Nash Equilibria in Concurrent Games with Lexicographic Preferences

1 Introduction

The last twenty years has seen considerable research directed at the use of game theoretic techniques in the analysis and verification of multi-agent systems. From this standpoint, processes in a multi-agent systems can be understood as players in a game, acting strategically and rationally in pursuit of delegated preferences; possible behaviours of agents correspond to the strategies of players. One important strand of work in this tradition is the development of techniques for reasoning about what properties players (or coalitions of players) can bring about (i.e., whether they have "winning strategies" for certain conditions) [Alur et al., 2002]. More recently, attention has shifted to the analysis of the equilibrium properties of such systems. A typical question is whether a temporal property holds under the assumption that players select strategies that form a Nash equilibrium. In this work, a key question is how the preferences of agents are represented, and one widely-adopted answer to this question is to associate with each player a qualitative goal/objective, usually given either by a temporal logic property or by a winning (acceptance) condition, such as reachability, safety, B¨uchi, LTL, etc [Pnueli and Rosner, 1989; Gutierrez et al., 2015; Bouyer et al., 2015]. This setting fits very naturally with the verification of discrete (multi-agent) systems. However, the preference structures that are induced in this way have a rather simple (dichotomous) structure: a player is simply either satisfied or unsatisfied; no distinction is made between outcomes that satisfy the player's objective, nor is any made between outcomes that do not satisfy the objective. This limits the applicability of such representations for modelling many situations of interest. Another alternative setting is given by games where instead of having a qualitative objective, players have quantitative goals-for instance, to minimize a given cost, or to maximise some reward [Ehrenfeucht and Mycielski, 1979; Ummels and Wojtczak, 2011; Kupferman et al., 2016]. A third possibility is to use preference models that combine qualitative and quantitative objectives [Chatterjee et al., 2005; Bloem et al., 2009]. To date, most models that combine qualitative and quantitative preferences in game-based multi-agent settings have only been studied in restricted settings (although see [Bulling and Goranko, 2013]).

∗ Partially supported by the INdAM research project 2017 "Logica e Automi per il Model Checking". S. Rubin was supported by a Marie Curie fellowship of the Istituto Nazionale di Alta Matematica (INdAM). J. Gutierrez, G. Perelli, and M. Wooldridge acknowledge with gratitude the financial support of the ERC Advanced Investigator grant 291528 ("RACE") at Oxford.

In this paper, we study this scenario and investigate a combination of quantitative and qualitative objectives not found in the literature. We study goals given by a lexicographic order, where a player first desires to satisfy its qualitative objective (given by a B¨uchi condition on the states of the system), and secondarily desires to minimise its costs (where costs are given by a quantitative mean-payoff objective). These games are studied in the context of settings with finite memory strategies, while the solution concept under consideration is strict Nash equilibrium. The focus on finite memory strategies is motivated by the fact that, in games with quantitative objectives, finite memory strategies can render decidable settings that would be undecidable otherwise [Ummels and Wojtczak, 2011]. Moreover, the combination of qualitative and quantitative objectives is natural for situations in which agents aim to satisfy some goal while minimising costs. For example, consider a robot whose task is to deliver packages around a factory environment: the primary goal of the robot is to deliver the packages (a qualitative objective), while secondarily minimising fuel consumption (a quantitative objective).

Our contributions are as follows. We show that, in a concurrent game with a lexicographic order of goals given by a B¨uchi (the primary goal) and a mean-payoff (the secondary goal) condition, deciding the existence of a finite-state strict Nash equilibrium is decidable in NP. Our results also show how to solve the rational synthesis problem [Fisman et al., 2010] and the rational verification problem [Wooldridge et al., 2016]. These two problems relate to establishing which properties (e.g., temporal, ω-regular, etc.) hold in a game, under the assumption that players in the game (i.e., system components) choose strategies in equilibrium.

2 Concurrent Graph-Games

In this section we introduce our game model. We make use of multi-player games played on finite graphs (rather than games in extensive-form or normal-form). Agents move concurrently (which includes the special sequential case), play deterministic (rather than randomised) and finite-state (instead of simply memoryless or infinite-memory) strategies, while trying to maximise their payoffs (equivalently, minimise costs), which are given as a lexicographic combination of a qualitative liveness property (of the form "visit some designated set of states infinitely often") and a quantitative long-term average of the rewards of its actions.

We fix some notation. If X is a set, then Xω is the set of all infinite sequences over X. If X and Y are sets, then XY is the set of all functions α : Y → X. We will often use uppercase Greek letters α, β, κ, · · · to name functions. Also, we will use tuple notation: we write αy ∈ X instead of α(y).

An arena is a tuple

where Ag, Act, and St are finite non-empty sets of agents (write N = |Ag|), actions, and states, respectively; ι is the initial state; τ : St × ActAg → St is a transition function mapping each pair, consisting of a state and an action for each agent, namely a decision δ ∈ ActAg , to a successor state. A weighted arena is a tuple W = 〈A, κ, β〉 where A is an arena; κ : Ag → (Act → Z) is a weight function associating an integer weight to each action of each agent; β : Ag → 2St is a B¨uchi function associating a set of B¨uchi states to each agent.

Executions: A path π = s0δ0s1δ1 · · · is an infinite sequence over St × ActAg such that τ(si, δi) = si+1 for all i. In particular, δi(a) is the action of agent a in step i. An execution is a path with s0 = ι.

Let Exec denote the set of all executions. For each execution π = s0δ0s1δ1 · · · and each agent a, define

1. the sequence κa(π) = κa(δ0(a))κa(δ1(a)) · · · ,
2. the set INF(π) = {s ∈ St : ∃∞ms = sm}.

Payoffs: For a sequence α ∈ Rω , let mp(α) be the mean-payoff of α, that is, for every n ∈ N define

and then

This definition naturally extends to executions, i.e., define mpa(π) = mp(κa(π)).

For an execution π ∈ Exec and B ∈ 2St define

Define Buchia(π) = Buchiβ(a).

Let Ω = {⊥, ⊤} × R denote the set of payoffs. We define a total ordering on the set Ω of payoffs: (x, y) ≺lex (x′ , y′ ) iff, either (x = ⊥ and x′ = ⊤) or (x = x′ and y < y′ ).

Lexicographic games: A Lex(Buchi,mp) game is a tuple G = 〈W, pay〉 where A is a weighted arena and pay : Ag → (Exec → Ω) is the payoff function defined by paya(π) = (Buchia(π), mpa(π)).

Each agent is trying to maximise its payoff. In other words, agent a's primary goal is to see infinitely some state from the set βa infinitely often, and its secondary goal is to maximise it's mp-reward (which can be seen as minimising its cost).

Remark 1. We consider weights as rewards to be maximised. One may, instead, consider them as costs to be minimised. All our results hold for such cost-games. Indeed, given a weighted arena A with weights (κa)a∈Ag, define a weighted arena A′ in which all weights are replaced by their negation. Then agent a that maximises its payoff in A′ has the primary goal of making Buchia(·) true and the secondary goal of maximising mp(-κa(·)). But maximising mp(-κa(·)) = -mp(κa(·)) is the same as minimising mp(κa(·)).

Strategies: A history is a finite sequence s0δ0··· sn-1δn-1sn such that s0 = ι and τ(si, δi) = si+1 for i < n. The set of all histories is denoted Hst. A strategy for agent a ∈ Ag is a function Hst → Act. A strategy profile is a function σ : Ag → (Hst → Act). A strategy profile σ induces a unique execution πσ, i.e., the execution πσ = s0δ0s1δ1 · · · such that δi(a) = σ(a)(s0s1 · · · si) for i ≥ 0.

Finite-state strategies: A strategy σ is finite-state if it is generated by a deterministic finite automaton M with output, i.e., M = 〈Q, q0,∆, λ〉 where Q is a finite set of states, q0 ∈ Q is the initial state, ∆ : Q × (St ∪ ActAg ) → Q is the transition function, and λ : Q → Act is the output function, so that, on input h ∈ Hst, the automaton M reaches a state q such that λ(q) = ∆(h). A strategy profile is finite-state if every strategy σ(a) is finite-state. Observe that in this case, the unique execution πσ is ultimately periodic.

Strict ϵ Nash-equilibria: The solution concept we work with is strict ϵ Nash-equilibrium. This is a natural refinement of ϵ Nash-equilibrium, and includes strict Nash equilibrium as a special case. For ϵ ≥ 0 and (x, y) ∈ Ω, let (x, y) + ϵ denote (x, y + ϵ) ∈ Ω. A strategy profile σ is a strict ϵ Nash-equilibrium if for every agent a ∈ Ag, and every strategy profile σ′ that disagrees with σ on the a-th component (i.e., σ′ (a) ̸= σ(a) and σ′ (b) = σ(b) for all b ̸= a), we have that paya(πσ′) ≺lex paya(πσ) + ϵ. If ϵ = 0 then we call this a strict Nash equilibrium. We remark that an (ordinary) Nash equilibrium uses ⪯lex instead of ≺lex. By FSNEϵ (G) we denote the set of finite-state strict ϵ Nash equilibria in G. We emphasise that, in the definition of a finite-state strict ϵ Nash-equilibrium σ, the deviating strategies σ′ (a) need not be finite-state. This captures worst-case behaviour of the deviators.

Decision Problems: The central decision problem of this work, called Rational Synthesis or Verification [Fisman et al., 2010; Gutierrez et al., 2015; Kupferman et al., 2016], asks if there exists a FSNEϵ so that the induced play πσ satisfies a given B¨uchi condition. Note that in case B = St, this amounts to the deciding the existence of a FSNEϵ .

Formally, for a rational ϵ ≥ 0 we consider the following decision problems for the class of Lex(Buchi,mp)-games:

1. FSNEϵ -emptiness is the problem of deciding, given a game G, if FSNEϵ (G) ̸= ∅.
2. E- FSNEϵ is the problem of deciding, given a game G and a set B ⊆ St, if there exists σ ∈ FSNEϵ (G) such that INF(πσ) ∩ B ̸= ∅.

3 E-FSNEϵ and FSNEϵ -Emptiness are Decidable, and in NP

In this section we establish our main technical result, i.e., that E - FSNEϵ is in NP. This immediately gives that FSNEϵ -emptiness is in NP.

Theorem 1. There is an NP algorithm that, given a rational ϵ ≥ 0, a Lex(Buchi, mp) game G, and a set B ⊆ St, decides whether there is σ ∈ FSNEϵ (G) such that INF(πσ) ∩ B ̸= ∅.

We first apply a pre-processing step that pushes the weights from the actions into the states, i.e., we can assume, without loss of generality, that the weight function is of the form κ : Ag → (St → Z). Since this step is standard and of polynomial complexity, we omit it.

We split the remainder of the proof into three steps.

1. We study two-agent zero-sum games with a Lex(Buchi,mp) objective (played on the same arena as G). We prove that every such game has a value opt, this value is computable in NP, and for every c > 0 there exists a finite-state strategy for the first agent that guarantees a payoff of at least opt - c, and similarly a finite-state strategy for the second agent that guarantees a payoff of at most opt + c.
2. We reduce the problem of whether FSNEϵ (G) ̸= ∅ to the problem of finding thresholds z ∈ ΩAg and an ultimately periodic path in a certain graph G[z] such that za ≺lex paya(π) + ϵ. More precisely, each za is a so-called "punishing value", i.e., the value of a two-agent zero-sum game with a Lex(Buchi,mp) objective played on the same arena as G, starting at some state s ∈ St, but with a trying to maximise its payoff and the the rest of the opponents (viewed as a single player) trying to minimise a's payoff. Such values can be computed by the previous step. Moreover, the proof of this characterisation makes use of the approximation result from the previous step.
3. We show how to find ultimately periodic paths π such that za ≺lex paya(π) + ϵ in graphs of the form G[¯ z]. We do this in Section 3.3 by adapting the linear programming approach for computing zero-cycles in mean-payoff graphs [Kosaraju and Sullivan, 1988].

In the rest of this section we sketch the technicalities of these steps, and then show how to establish the theorem.

3.1 Two-Agent Zero-SumLEX(Buchi,mp)-Games

We begin with a study of two-agent zero-sum Lex(Buchi, mp) games H = 〈A, κ,B〉 where A is an arena with Ag = {1, 2}, and κ : St → Z and B ⊆ St. Agent 1 is called "maximizer" and agent 2 is called "minimizer". Define pay(π) = (BuchiB(π),mp(κ(π))). The value of H is defined as val(H) = supσ infδ pay(π〈σ,δ〉) where σ ranges over strategies of the maximizer, δ ranges over strategies of the minimizer, and π〈σ,δ〉 is the unique execution determined by the profile 〈σ, δ〉.

Proposition 1. Every two-agent zero-sum Lex(Buchi,mp) game H has a value, denoted val(H) ∈ Ω. Moreover, this value can be computed in NP.

Proof. Without loss of generality, we can consider H to be turn-based (see Remark 2). We compute val(H) by reducing to solving two-agent turn-based zero-sum games J with mean-payoff parity objectives [Chatterjee et al., 2005], which are known to be in NP [Bloem et al., 2009]. The games J = (W,R′ , pay+) are played on state-weighted arenas W = (A, κ, π) where κ : St → Z assigns weights and π : St → Z assigns priorities, with payoff set R′ = {-∞} ∪ R with its usual ordering <, and payoff function pay+ : Exec → R′ defined as follows: pay+(π) equals -∞ if parity(π) = ⊥, and mp(κ(π)) otherwise. Here parity(π) is defined to be ⊤ if the largest priority occuring infinitely often on π is even, and ⊥ otherwise. In words, the first player is trying to simultaneously make the parity condition hold and maximise its mean-payoff. The value val(J) is defined to be the maximum payoff that the first player can achieve. It follows from [Chatterjee et al., 2005] that values exist and can be computed. Note that the parity condition generalises the B¨uchi condition (i.e., states in B get priority 2 and all other states get priority 1), and the co-B¨uchi condition (i.e., states in B get priority 1 and all other states get priority 0).

Since mean-payoff parity games are asymmetric, we introduce their counterparts in which the first player is trying to ensure the largest priority occuring infinitely often is odd (instead of even) and, at the same time, trying to minimise (instead of maximise) the mean-payoff. Formally, these are games K = (W,R′ , pay-) where pay-(π) equals -∞ if parity(π) = ⊤, and mp(κ(π)) otherwise. The value val(K) is defined to be the minimum payoff that the first player can achieve. Such values exist and can be computed by reducing to mean-payoff parity games: val(K) = val(K∂ ) with K∂ = (W ∂ ,R′ , pay+) and W ∂ = (A, κ∂ , π∂ ) with κ∂ (s) = -κ(s) and π∂ (s) = π(s) + 1.

We use these facts to characterise and compute the value of two-agent zero-sum Lex(Buchi,mp) games as follows. Let J = (W,R′ , pay+) be the mean-payoff B¨uchi game on the same state-weighted arena as H. If val(J) ̸= -∞, then val(J) is the largest mean-payoff value that the first player can enforce while ensuring the B¨uchi condition holds. In this case val(H) = (⊤, val(J)). Indeed, if σ1 ensures val(J) then it also ensures that (⊤, val(J)) ⪯lex val(H). On the other hand, if (⊤, val(J)) ≺lex val(H) then there is some strategy σ′1 that ensures the B¨uchi condition holds and achieves mean-payoff higher than val(J), which contradicts the definition of val(J).

On the other hand, if val(J) = -∞ then the second player can enforce the failure of the B¨uchi condition. Yet, this strategy may not minimise the mean-payoff as required in the definition of Lex(Buchi, mp) games. Thus, consider the game K = (W, R′ , pay-) on the same state-weighted arena as H. As val(J) = -∞we have that val(K) ̸= -∞. Thus, val(H) = (⊥, val(K)) using similar reasoning as before.

Regarding the complexity, observe that the construction of the games J and K is linear in the size of H, and that we employ an NP procedure once per game. Thus the overall complexity computing val(H) is NP.

Remark 2. It is not hard to transform our two-player zero-sum concurrent game H into a two-player zero-sum turn-based H′ such that val(H) = val(H′ ).

To give an intuition, we replace every transition s (c1,c2) ----→ s′ by two transitions s c1 -→ sc1 c2 -→ s′ , in a way that all the original states belong to Player 1, while every extra state sc belongs to Player 2, and has the same weight and priority as s (and we do not change the B¨uchi sets). Note that such a construction depends on the ordering of players, i.e., in order to compute the value for Player 2, we need to employ a construction of a game H′′ that replaces s (c1,c2) ----→ s′ by s c2 -→ sc2 c1 -→ s′ .

It is not hard to see that in two-player zero-sum Lex(Buchi,mp)-games H, a player may need infinite memory to achieve the optimal value val(H) (Cfr. [Chatterjee et al., 2005, Figure 1]). However, as proven in [Bloem et al., 2009], for every mean-payoff parity game J and every ϵ > 0 there exists a finite-memory strategy σ (that depends on ϵ) such that for every strategy δ, it holds that pay(πσ,δ) ≥ val(J)-ϵ. Thus, using the same argument as in Proposition 1, we get:

Proposition 2. For every two-agent zero-sum Lex(Buchi,mp) game H and every ϵ > 0 there exists a finite-state strategy σ for minimzer such that for every strategy δ of the maximizer (not neccessarily finite-state), it holds that val(H) - ϵ ⪯lex pay(πσ,δ).

3.2 Reducing EquilibriumFinding to Path Finding

In this section we reduce the problem of the existence of σ ∈ FSNEϵ (G) with INF(πσ) ∩ B ̸= ∅ in a Lex(Buchi, mp) game G to the existence of an ultimately periodic path in a certain subgraph of the weighted arena of G. To do this, we adapt the proof in [Ummels and Wojtczak, 2011, Section 6] that shows how to decide the existence of a (not neccessarily finite-state) Nash equilibrium for mean-payoff games.

We first need the notion of punishing values and strategies. For a ∈ Ag and s ∈ St define the punishing value pa(s) to be the ⪯lex-largest (x, y) that player a can achieve from state s by "going it alone", i.e., by playing against the coalition Ag \ {a}. These values can be computed by Proposition 1. Moreover, for every ϵ′ > 0, fix σϵ′ s,a from Proposition 2. We view σϵ′ s,a as a profile, i.e., σϵ′ s,a : Ag \ {a} → (Hst → Act), and call σϵ′ s,a (b) a ϵ′ -punishing strategy for agent b. Note that these ϵ′ -punishing strategies are finite-state.

For an agent a ∈ Ag and z ∈ Ω, a pair (s, δ) ∈ St×ActAg is z-secure for a if pa(tr(s, δ′ )) ⪯lex z for every δ′ ∈ ActAg that agrees with δ except possibly at a.

Proposition 3. For every Lex(Buchi, mp) game G, set B ⊆ St, and ϵ ≥ 0, the following are equivalent:

1. There exists σ ∈ FSNEϵ (G) with INF(πσ) ∩ B ̸= ∅.
2. There exists ¯ z ∈ Ω|Ag| where za ∈ {pa(s) : s ∈ St} and there exists an ultimately-periodic execution π = s0δ0s1δ1 · · · in G with INF(π) ∩ B ̸= ∅, such that for every agent a,

• (b) for all i ∈ N, the pair (si, δi) is za-secure for a.

Proof. For (1) implies (2), take σ ∈ FSNEϵ (G) and let π = πσ be the execution resulting from σ. Since σ is finite-state, π is ultimately periodic. Define ¯ z ∈ Ω|Ag| by za = max{pa(δ(sn, δ′n )) : n ∈ N, ∧b̸=aδ′n (b) = δn(b)}, i.e., za is the largest value player a can get by deviating from π. For every n ∈ N, (sn, δn) is za-secure for a (by definition of za and za-secure). Moreover, za ≺lex paya(π) + ϵ: indeed, let n be such that za = pa(δ(sn, δ′n )), and suppose that paya(π) + ϵ ⪯lex za; then player a would deviate at step n by playing δ′n (a) and following a strategy that achieves at least za from this point. Note that such a (possibly infinite-state) strategy exists by Proposition 1. But, due to prefix-independence of the payoff function, this is also the payoff of the whole play, contradicting the choice of π as the execution of a strict ϵ Nash-equilibrium.

For (2) implies (1), let ¯ z ∈ Ω|Ag| and π = s0δ0s1δ1 . . . be given with the stated properties. We build a strict ϵ Nash-equilibrium σ such that πσ = π. For b ∈ Ag, we define σ(b) as follows. For every history h = s0δ0 . . . sn-1δn-1sn (i.e., a prefix of π), define σb(h) = δn(b), i.e., follow π as long as no-one has deviated from π. For every agent a ̸= b and every history of the form h = s0δ0 . . . sn-2δn-2sn-1δ′n-1 s′n v where δ′n-1 equals δn-1 except for the action of a, define σb(h) = σϵ′ s,a (b)(s′n v) where ϵ′ > 0 is a constant with the property that pa(s′n ) + ϵ′ ≺lex paya(π)+ϵ (such a constant exists since, by assumptions 2(a) and 2(b), pa(s′n ) ⪯lex za ≺lex paya(π)+ϵ), i.e., punish a for deviating. For any other history h, define the value σb(h) to be some arbitrary but fixed action. Note that σ is finite-state since π is ultimately periodic. Finite memory is needed to remember if an agent has deviated and, if so, which agent has deviated. Moreover, σϵ′ s,a (b) is finite-state.

We show that σ ∈ FSNEϵ (G). Observe that πσ = π, and so paya(πσ) = paya(π). Suppose, for a contradiction, that there is an agent a and a strategy profile σ′ such that σ′ (b) = σ(b) for b ̸= a, and (*) paya(π) + ϵ ⪯lex paya(π′ ) where π′ is the execution determined by σ′ . Let h be the longest common prefix of π and π′ , and suppose hδs is the prefix of π and hδ′ s′ is the prefix of π′ . Then δa ̸= δ′a . Thus, from the history hδ′ s′ , each agent b ̸= a plays the strategy σϵs,a (b), and thus paya(π′ ) ⪯lex pa(s′ ) + ϵ′ . Combining this with (*)

we get paya(π) + ϵ ⪯lex pa(s′ ) + ϵ′ . By the choice of ϵ′ , we get paya(π) + ϵ ≺lex paya(π) + ϵ, a contradiction.

3.3 Path Finding inMulti-Weighted Graphs with LEX(buchi,mp) Payoffs

The following theorem, of interest in its own right, will be used to decide the existence of ultimately periodic paths in Proposition 3. A multi-weighted graph is a structure of the form (V,E, (wa)a∈A, (βa)a∈A) where V is a finite set of states, E ⊆ V 2 a set of edges, A is a finite index set, wa : V → Z and βa ⊆ V .

Theorem 2. Given a multi-weighted graph W = (V,E, (wa)a∈A, (βa)a∈A), a starting vertex ι ∈ V , and a vector of payoffs f ∈ ΩA, one can decide in polynomial time whether there exists an ultimately periodic π = v0v1 · · · in the graph with ι = v0 and fa ≺lex paya(π) for every a ∈ A.

Proof. Without loss of generality we may assume that fa ∈ {⊤, ⊥} × {0} (to see this, redefine wa(s) to be wa(s) - fa). Also, we may assume that every state in V is reachable from ι (to see this, restrict V to the states reachable from ι, computable in linear time). We now reduce the problem to finding certain cycles in W. A cycle is a finite path of the form s0s1 · · · sn (for some n ≥ 1) such that s0 = sn (note that cycles are not necessarily simple). Write s ∈ C to mean that s = si for some i ≤ n; similarly, for B ⊆ V , write C∩B for the set of s ∈ C such that c ∈ B. Define avga(C) = 1 n+1 Σnj=0wa(sj), and Buchia(C) = ⊤ iff C ∩ βa ̸= ∅. Given W and f ∈ ({⊤,⊥} × {0})A, the stated problem is equivalent to deciding if there exists a cycle C in W such that, for every a ∈ A, fa ≺lex 〈Buchia(C), avga(C)〉. However, writing suma(C) = Σn+1 j=0 wa(sj), we can replace avga(C) by suma(C) in this problem (since avga(C) > 0 iff suma(C) > 0). In order to decide the existence of such a cycle, we adapt the proof from [Kosaraju and Sullivan, 1988] that shows how to decide if there is a cycle C such that for every a ∈ A, suma(C) = 0.

A multicycle M is a non-empty multiset of cycles. Thus a cycle is a multicycle Mwith |M| = 1. A β-multicycle is a multicycle M such that for every a ∈ A, i) Buchia(C) = ⊤ for some C ∈ M, and ii) ΣC∈Msuma(C) > 0. We want to decide if there exists a β-cycle.

Now, one can decide if there exists a β-multicycle in polynomial time using linear programming. For every edge e introduce a variable xe. Informally, the value xe is the number of times that the edge e is used on a β-multicycle. Formally, let src(e) = {v ∈ V : ∃we = (v,w) ∈ E}; trg(e) = {v ∈ V : ∃w e = (w, v) ∈ E}; out(v) = {e ∈ E : src(e) = v} and in(v) = {e ∈ E : trg(e) = v}.

The linear program LP has the following inequalities and equations:

Eq1: xe ≥ 0 for each edge e - this is a basic consistency criterion;

Eq2: Σe∈Exe ≥ 1 - this ensures that at least one edge is chosen;

Eq3: for each a ∈ A, Σe∈Eκa(src(v))xe > 0- this enforces that the total sum is positive;

Eq4: for each a ∈ Asuch that fa = 〈⊤, 0〉, Σsrc(e)∩Ba̸=∅xe ≥ 1 - this ensures that the B¨uchi condition is satisfied;

Eq5: for each v ∈ V , Σe∈out(v)xe = Σe∈in(v)xe - this "preservation" condition says that the number of times one enters a vertex is equal to the number of times one leaves that vertex.

Clearly every β-multicycle determines an integer solution of the LP. Also, an integer solution of the LP determines a β-multicycle. This is due to Eq5 and Euler's Theorem, i.e., a directed graph is Eulerian if and only if it is connected and for every vertex v, the indegree of v is equal to the outdegree of v [Bang-Jensen and Gutin, 2008, Theorem 1.6.3].

Moreover, the program LP has a solution in the reals iff it has a solution in the rationals [Matousek and G¨artner, 2007]. Moreover, if (xe)e∈E is a solution to LP and k ∈ N\{0}, then (kxe)e∈E is also a solution to LP. Thus, the LP has a solution iff it has an integer solution. Thus, the LP has a solution iff the graph has a β-multicycle.

Recall that we want to decide if there is a β-multicycleM such that |M| = 1, i.e., contains a single cycle. Define a relation on V : v ≡ w iff v = w or there exists a β-multicycle M and C ∈ M such that v,w ∈ C. Note that ≡ is an equivalence relation: indeed, if u, v ∈ C for C ∈ M, and v,w ∈ C ′ for C ′ ∈M′ then u,w ∈ C ′′ for C ′′ ∈M′′ where C ′′ is formed by tracing C from w to w and then tracing C ′ fromw to w, andM′′ isM∪M′ \ {C,C ′ }.

Suppose ≡ has index 1, i.e., for all v,w ∈ V , v ≡ w. We claim that there exists a β-cycle. Indeed: for every v, v′ ∈ V let Mv,v′ be a β-multicycle containing a cycle C that visits v and v′ . ThenM= ∪v,v′∈VMv,v′ is a β-multicycle such that (*): for every v, v′ ∈ V there exists C ∈Msuch that v, v′ ∈ C. We now define two transformations of multicycles M ↦→ M′ that maintain the following invariants: a) sum(M) = sum(M′ ), b) if M satisfies (*) then so does M′ , c) |M′ | < |M| (i.e., the number of cycles decreases). Thus, repeatedly applying these transformation results in a β-cycle.

First, if C occurs more than once inM, say n times, then remove all occurences of C fromM and add the single C n formed by tracing C n-many times. Thus, we have that M is a set of cycles (i.e., not a proper multiset). Second, if M is not a single cycle, take C ̸= C ′ ∈M, v ∈ C, v′ ∈ C ′ and by (*) pick D ∈ M such that v, v′ ∈ D. There are three cases: if D ̸= C,D ̸= C ′ then form the cycle F by tracing C from v to v, then tracing "half" of D from v to v′ , then tracing C ′ from v′ to v′ , and then tracing the "other half" of D from v′ to v and let M′ be M∪ {F} \ {C,C ′ ,D}; if D = C (the case D = C ′ is symmetric), then v′ ∈ C and thus form F by tracing C from v′ to v′ and then tracing C ′ from v′ to v′ , and let M′ be M∪ {F} \ {C, C ′ }. Both transformations satisfy the invariants.

Thus, the following algorithm decides if there is a β-cycle: if |V | = 1, then output "yes" if ≡ has index 1, and "no" otherwise; else, compute ≡; if it has index 1 then output "yes"; else, for each ≡-class X, recurse on the subgraph induced by X. The algorithm is clearly sound, i.e., if it outputs "yes" then there is indeed a β-cycle. To see that it is complete, note if that C is a β-cycle, then for all v, w ∈ C, v ≡ w; and thus C is contained in an ≡-class.

Regarding the complexity, observe that the size of the LP is polynomial in the size of the graph. Moreover, computing the equivalence relation ≡ can be done with |E| linear programs, and hence is also polynomial in the size of the graph (Cfr. [Kosaraju and Sullivan, 1988]). Hence, the overall complexity of the problem is polynomial.

3.4 Putting the Steps Together

We can now finish the proof of Theorem 1. Consider a rational ϵ ≥ 0 and a Lex(Buchi,mp) game G with state-weighted arena W = 〈A, κ, β〉 where A = 〈Ag,Act, St, ι, τ〉, κ : Ag → (St → Z), and β : Ag → 2St . For every agent a ∈ Ag nondeterministically guess a state s ∈ St and, by Proposition 1 compute, in nondeterministic polynomial time, the punishing value pa(s). Let za = pa(s). Next, we can think of W as a multi-weighted graph (St, E, (κa)a∈A, (βa)a∈A) where E(s, s′ ) iff τ(s, δ) = s′ for some δ. For z ∈ Ω|Ag| , a pair (s, δ) is z-secure if it is za-secure for every agent a. Let G[z] be the multi-weighted graph formed by restricting W to the set of edges (s, s′ ) for which there exists δ such that τ(s, δ) = s′ and (s, δ) is z-secure. Thus, by Proposition 3, to decide if there exists σ ∈ FSNEϵ (G) such that INF(πσ) ∩ B ̸= ∅, we run the deterministic polynomial time decision procedure in Theorem 2 on the multi-weighted graph (St,E, (κ′a )a∈A′ , (βa)a∈A′) and threshold f ′ ∈ Ω|Ag|+1 defined as follows: A′ = A ∪ {b} (for a fresh symbol b); κ′a = κa for all a ∈ A, and κ′b (s) = 0 for all s ∈ St; β′a = βa for all a ∈ A, and β′b = B; and f ′ (a) = za - ϵ for a ∈ Ag, and f ′ (b) = (⊤,-1). Clearly, the overall procedure can be implemented with a NP algorithm.

4 RelatedWork

The main decision problem in this work concerns the existence of an equilibrium satisfying a system property in concurrent multiplayer games; this problem is called "rational synthesis" [Fisman et al., 2010] or "rational verification" (cf., E-NASH in [Wooldridge et al., 2016]) and includes NE-emptiness as a special case. We studied this verification problem, specifically, for Lex(Buchi,mp)-games and finite-state strict Nash equilibria.

Most other work in rational synthesis concerns ordinary (not neccessarily finite-state, nor strict) NE-emptiness. In particular, NE-emptiness has been studied for other objectives, notably mean-payoff (NP-complete) [Ummels and Wojtczak, 2011], B¨uchi (PTIME-complete) [Bouyer et al., 2015], and lexicographic order on B¨uchi objectives (in NP, but not known to be NP-complete) [Bouyer et al., 2015].

E-NASH for finite-state strategies has been studied on iterated Boolean Games (a simple form of infinite-duration multiplayer concurrent games) as follows: with LTL objectives, E-NASH is 2EXPTIME-complete [Gutierrez et al., 2015]; with objective-LTL, i.e., each agent has to optimise a reward based on the truth value of a finite number of fixed LTL formulas, E-NASH is 2EXPTIME-complete [Kupferman et al., 2016]. A special case of objective-LTL is the lexicographic order on a finite (but unbounded) number of components, each consisting of an LTL formula, also 2EXPTIME-complete. Actually, these lower-bounds are inherited from the fact that solving two-player zero-sum games with LTL objectives is already 2EXPTIME-complete [Rosner, 1991].

We remark that all these works (except objective-LTL) concern equilibria concepts in multiplayer games with either qualitative or quantitative objectives, but not a combination, as we do. Objective-LTL combines Boolean objectives (given as LTL formulas) in a weak way, i.e., there are only finitely many possible payoffs. In contrast, Lex(Buchi,mp) combines Boolean objectives (given as B¨uchi sets) with quantitative objectives (mean-payoff), and thus result in infinitely many possible payoffs.

Combinations of qualitative and quantitative objectives have been studied for two-player turn-based games, i.e., in the zero-sum case: mean-payoff parity games [Chatterjee et al., 2005; Bloem et al., 2009], energy parity games [Chatterjee and Doyen, 2012]; and in the non zero-sum case secure-equilibria (in which each player tries to maximise their own payoff and then minimise their opponent's payoff) for a host of quantitative objectives including mean-payoff [Bruy`ere et al., 2014]. In contrast, our work considers equilibria in multiplayer games.

Finally, we mention logics that combine qualitative and quantitative aspects, i.e., variants of resource-bounded alternating temporal-time logics [Alechina et al., 2015; Bulling and Goranko, 2013]. Although these works deal with multiple-players, they do not deal with Nash equilibria (except in so far as winning strategies form equilibria).

5 Conclusion

In the last twenty years large efforts have been devoted to analyze qualitative and, most recently, quantitative aspects of multi-agent systems. However, these two settings have often been investigated separately. As this is not appropriate in many natural scenarios, researchers have started looking at the combination of these two worlds. The achievements in this direction, however, are far from satisfactory, either because the settings are too weak, e.g., they cannot model important solution concepts such as Nash Equilibria [Bulling and Goranko, 2013], or because they are too expensive in terms of complexity, e.g., between ExpTime-Hard and undecidable [Alechina et al., 2015].

In this paper we introduce a model of multi-agent systems in which each agent's payoff is a lexicographic combination of qualitative (B¨uchi) and quantitative (mean-payoff) payoffs. We call these Lex(Buchi,mp) games. The solution concept we focus on is finite-state strict ϵ Nash equilibria (for ϵ ≥ 0). In this setting, we prove the rational-synthesis problem (a generalisation of the equilibrium existence problem) is decidable, and moreover is in NP. The proof characterises the equilibrium executions as certain ultimately periodic paths in a multi-weighted graph. To compute this graph we solve two-player zero-sum games with lexicographic objectives, and to find paths in such graphs we use linear-programming.