Paper deep dive

Alternating-Time Temporal Logic with Mean-Payoff Guarantees

Muhammad Najib

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 152

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%

Last extracted: 8/5/2026, 3:08:30 AM

Summary

The paper introduces ATL*_mp, an extension of Alternating-Time Temporal Logic (ATL*) that combines strategic temporal objectives with long-run mean-payoff constraints over weighted concurrent game structures. It analyzes the model checking complexity, showing it is 2EXPTIME-complete for one-dimensional constraints under perfect-recall and finite-memory semantics. The study highlights a strict hierarchy between memoryless, finite-memory, and perfect-recall strategies and provides bounds on the memory required to achieve specific payoff thresholds.

Entities (8)

ATL*_mp · logic · 98%2EXPTIME-complete · complexity-class · 95%ATL · logic · 95%Weighted Concurrent Game Structures · model · 92%Finite-Memory · strategy-type · 90%Mean-Payoff · metric · 90%Memoryless · strategy-type · 90%Perfect-Recall · strategy-type · 90%

Relation Signals (6)

ATL*_mp → extends → ATL

confidence 95% · We introduce ATL*_mp, an extension of ATL* over weighted concurrent game structures

Model Checking (ATL*_mp) → hascomplexity → 2EXPTIME-complete

confidence 95% · For one-dimensional constraints, model checking is 2EXPTIME-complete under both perfect-recall and finite-memory semantics

ATL*_mp → operateson → Weighted Concurrent Game Structures

confidence 92% · We introduce ATL*_mp, an extension of ATL* over weighted concurrent game structures

ATL*_mp → incorporates → Mean-Payoff

confidence 90% · each strategic modality carries a conjunctive mean-payoff constraint

Perfect-Recall → isstricterthan → Finite-Memory

confidence 85% · We show that memoryless, finite-memory, and perfect-recall abilities form a strict hierarchy

Finite-Memory → isstricterthan → Memoryless

confidence 85% · We show that memoryless, finite-memory, and perfect-recall abilities form a strict hierarchy

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Alternating-time temporal logic and its extensions provide several ways of combining strategic and quantitative reasoning. We study a particular combination: whether a coalition has a single strategy that enforces a temporal objective while guaranteeing given long-run mean-payoff thresholds. We introduce ATL*_mp, an extension of ATL* over weighted concurrent game structures in which each strategic modality carries a conjunctive mean-payoff constraint. The temporal and quantitative requirements must hold against every behaviour of the remaining agents, and the existence of such a strategy cannot in general be reduced to the two requirements considered separately. For one-dimensional constraints, model checking is 2EXPTIME-complete under both perfect-recall and finite-memory semantics, matching ATL*. For the pure quantitative fragment and fragments restricted to ATL or GR(1) temporal objectives, model checking has lower complexity. With multi-dimensional conjunctive constraints, model checking under finite-memory semantics remains 2EXPTIME-complete. We show that memoryless, finite-memory, and perfect-recall abilities form a strict hierarchy, while finite-memory strategies still achieve every threshold strictly below the perfect-recall supremum. We give tight linear upper and lower bounds on the required memory as a function of the denominator of the threshold, even when the game and temporal monitor are fixed. We give several examples of properties expressible in the logic, including temporal synthesis with performance guarantees and aggregate and multi-criteria objectives. We also relate the logic to cooperative rational verification, showing that it can express beneficial deviations from fixed payoff baselines, but not directly reproduce the standard ATL* encoding of the core for dichotomous preferences.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

150,546 characters extracted from source content.

Expand or collapse full text

Alternating-Time Temporal Logic with Mean-Payoff Guarantees Muhammad Najib 0000-0002-6289-5124 Heriot-Watt University, Edinburgh, UK m.najib@hw.ac.uk Abstract. Alternating-time temporal logic and its extensions provide several ways of combining strategic and quantitative reasoning. We study a particular combination: whether a coalition has a single strategy that enforces a temporal objective while guaranteeing given long-run mean-payoff thresholds. We introduce ATL∗ATL^*_ mp, an extension of ATL∗ATL^* over weighted concurrent game structures in which each strategic modality carries a conjunctive mean-payoff constraint. The temporal and quantitative requirements must hold against every behaviour of the remaining agents, and the existence of such a strategy cannot in general be reduced to the two requirements considered separately. For one-dimensional constraints, model checking is 2Exptime2 Exptime-complete under both perfect-recall and finite-memory semantics, matching ATL∗ATL^*. For the pure quantitative fragment and fragments restricted to ATLATL or GR(1)GR(1) temporal objectives, model checking has lower complexity. With multi-dimensional conjunctive constraints, model checking under finite-memory semantics remains 2Exptime2 Exptime-complete. We show that memoryless, finite-memory, and perfect-recall abilities form a strict hierarchy, while finite-memory strategies still achieve every threshold strictly below the perfect-recall supremum. We give tight linear upper and lower bounds on the required memory as a function of the denominator of the threshold, even when the game and temporal monitor are fixed. We give several examples of properties expressible in the logic, including temporal synthesis with performance guarantees and aggregate and multi-criteria objectives. We also relate the logic to cooperative rational verification, showing that it can express beneficial deviations from fixed payoff baselines, but not directly reproduce the standard ATL∗ATL^* encoding of the core for dichotomous preferences. Key words and phrases: alternating-time temporal logic, mean-payoff games, concurrent games, strategic ability, model checking, multi-agent systems 1. Introduction Alternating-time temporal logic (ATLATL) and its more expressive extension ATL∗ATL^* [4] are among the most widely used formalisms for reasoning about multi-agent systems. Their central construct is the strategic modality ⟨C⟩ψ \! C \! ψ, which states that the coalition C has a strategy enforcing the temporal property ψ, whatever the remaining agents do. This modality underlies much of the work on verification and synthesis for open and multi-agent systems, as well as more expressive languages such as Strategy Logic [21, 34]. ATLATL and ATL∗ATL^* cannot express the long-run performance associated with a coalition strategy. The formula ⟨C⟩ \! C \! \,safe states that C can keep the system safe, but says nothing about the energy consumed, the throughput maintained or the reward obtained. Mean-payoff games [25, 47] express such long-run quantities, but do not combine them with temporal requirements. We study whether a coalition has a single strategy that enforces a temporal objective and a mean-payoff threshold against every counter-strategy. This is stronger than requiring the two objectives to be enforceable separately, as 1 shows. We introduce ATL∗ATL^*_ mp, a conservative extension of ATL∗ATL^* interpreted over weighted concurrent game structures in which each strategic modality carries a mean-payoff constraint, ⟨C⟩Λψ,Λ::=⊤∣j≥q∣Λ∧Λ. \! C \! _ \,ψ, ::= _j≥ q . Setting Λ=⊤ = recovers ATL∗ATL^* exactly, while setting ψ=⊤ψ= yields a query about the payoff vectors a coalition can enforce, in the sense of multi-mean-payoff games [45, 22]. The combined case has both a non-trivial temporal objective and a non-trivial mean-payoff condition. For example, ⟨1,2⟩1≥0∧2≥0((r1→d1)∧(r2→d2)), \! \1,2\ \! _mp_1≥ 0\, \,mp_2≥ 0 (G(r_1 _1) (r_2 _2) ), states that the two agents have a joint policy that responds to every request of either type. The same policy must also keep both long-run rewards non-negative against every behaviour of the environment. Contributions. Our contributions are as follows. (1) Logic and semantics. We define weighted concurrent game structures and the logic ATL∗ATL^*_ mp over them (Section 3), and show that it conservatively extends ATL∗ATL^*. The combined modality cannot in general be reduced to the conjunction of an ATL∗ATL^* ability and a multi-mean-payoff ability: ⟨C⟩Λψ≢⟨C⟩ψ∧⟨C⟩Λ⊤. \! C \! _ ψ\; ≡\; \! C \! ψ \! C \! _ . Conjoining the corresponding separate queries therefore does not capture the requirement that a single coalition strategy enforce both objectives (1). (2) Game characterisation. The usual sequentialisation of a concurrent game introduces an intermediate state after each coalition move. This preserves mean payoff and stutter-invariant temporal objectives, but not arbitrary LTLLTL formulae containing X. We give a round-preserving sequentialisation in which the temporal automaton advances once per concurrent round, and establish strategy correspondence under perfect-recall and finite-memory semantics (5 and 7). (3) Model checking. We give a bottom-up algorithm which, for each strategic subformula, builds the product of the round-preserving sequentialisation with a deterministic parity automaton for the path formula and solves the resulting mean-payoff parity game [20, 19]. With one-dimensional constraints, model checking is 2Exptime2 Exptime-complete under both perfect-recall and finite-memory semantics (9), matching ATL∗ATL^* [4]. We give sharper bounds for restricted temporal fragments in Section 6. We then show that model checking with arbitrary conjunctive constraints remains 2Exptime2 Exptime-complete under finite-memory semantics; the corresponding perfect-recall problem remains open (Section 7). (4) Memory requirements. We show that memoryless, finite-memory and perfect-recall abilities form a strict hierarchy on positive formulae (17), while every threshold strictly below the perfect-recall supremum is achievable with finite memory (18). The required memory may grow linearly in the denominator of the threshold, and hence exponentially in its binary encoding; 19 gives matching bounds. (5) Applications and expressive limits. We give several examples of properties expressible in ATL∗ATL^*_ mp, including temporal synthesis with performance guarantees and aggregate and multi-criteria objectives. We also relate the logic to cooperative rational verification: beneficial deviations from fixed payoff baselines are expressible, but the standard ATL∗ATL^* encoding of the core for dichotomous preferences does not extend directly to mean-payoff preferences, since the relevant deviation thresholds depend on the payoff of the candidate profile (Section 9). Table 1 summarises the principal model-checking bounds. More refined bounds for restricted one-dimensional temporal fragments are given in Table 2. For a fixed number of dimensions, the quantitative, ATLATL_ mp and ATL∗[GR(1)]ATL^*_ mp[GR(1)] fragments are moreover pseudo-polynomial under finite-memory semantics (16). Table 1. Main model-checking complexity results, where “-c” abbreviates “-complete”. The entries for the full logic concern arbitrary nesting. Under memoryless semantics the PSpace bound holds for arbitrary conjunctive constraints, and hardness already holds when every constraint is ⊤ . The multi-dimensional quantitative entries concern strategic atoms ⟨C⟩Λ⊤ \! C \! _ ; under finite-memory and perfect-recall semantics, flat Boolean combinations of such atoms are in P∥NPP NP_ . Full ATL∗ATL^*_ mp Quantitative atoms Semantics one-dimensional multi-dimensional multi-dimensional Memoryless PSpace-c (Thm. 10) NP-c (Prop. 14) Finite memory 2Exptime2 Exptime-c (Thm. 9) 2Exptime2 Exptime-c (Thm. 15) coNP-c (Prop. 14) Perfect recall 2Exptime2 Exptime-c (Thm. 9) open (Open Prob. 7.4) coNP-c (Prop. 14) Related work. Bulling and Goranko [14, 15] study concurrent games with accumulated utilities and utility-dependent action guards. They identify arithmetic path constraints interpreted over mean payoffs as a direction for future work [15]. In contrast, the conditions considered here are prefix-independent. Resource-bounded variants of ATLATL [2, 13, 35] constrain a finite budget along a play. Energy constraints originate in weighted timed systems [9]; in graph games, energy objectives constrain the running balance [19, 17]. Resource constraints and energy objectives both depend on the preceding prefix. Boker et al. [8] study the related setting of LTLLTL with accumulative values and identify its decidability boundary. At the algorithmic level, 8 uses the corresponding relationship between finite-memory mean-payoff parity objectives and energy parity objectives. Quantitative variants that assign a degree of satisfaction to a formula, rather than evaluating a quantity along an outcome, have been studied for Strategy Logic [10] and for ATL∗ATL^* [36]. Murano, Neider and Zimmermann give a multi-valued semantics for the strategic and temporal operators of ATLATL and ATL∗ATL^*, designed to make satisfaction robust to small violations of assumptions. Model checking rATL∗rATL^* is also 2Exptime2 Exptime-complete, but its quantitative component measures degrees of satisfaction, whereas ATL∗ATL^*_ mp constrains the mean payoff of an outcome. Their analysis does not consider the distinctions between memoryless, finite-memory and perfect-recall strategies studied here. LTLLTL synthesis with mean-payoff objectives has been studied in two-player turn-based games [5, 7]. The problem reduces to mean-payoff parity games and is 2Exptime2 Exptime-complete. For mean-payoff parity games, exact optimality may require infinite memory, while finite-memory strategies suffice for ε -approximation [20]; this property carries over to LTLLTL synthesis with mean-payoff objectives [7]. Our setting allows arbitrary coalitions and nested strategic modalities, and the underlying game is concurrent rather than turn-based. Section 4 extends the corresponding game reduction to concurrent games and arbitrary coalitions. Rational verification asks which temporal properties hold in the stable outcomes of a multi-agent system [28, 31, 1]; most of that work uses Nash equilibrium and its refinements, with equilibria in limit-average games studied in [44] and rational-verification problems for memoryless mean-payoff games with ω-regular specifications in [43]. We compare ATL∗ATL^*_ mp with the cooperative, core-based formulations of [29, 30] in Section 9.3. Quantitative languages [18] provide an automata-theoretic account of long-run values without strategic modalities. Strategy Logic [21, 34] permits strategies to be quantified, named, and bound explicitly, but its standard form contains no payoff terms or mean-payoff objectives. Combining named strategy profiles with such payoff terms would allow the payoffs of a deviation to be compared with those of an enclosing profile, as required by the rational-verification application discussed in Section 9.3. 2. A motivating example The following example illustrates the combined temporal and quantitative requirement, the resulting threshold trade-off, and the need for memory. exa [Coordinated warehouse robots] Two mobile robots, 11 and 22, jointly transport oversized pallets from two loading bays to a dispatch area. Transporting a pallet requires both robots to select the same loading bay, L or R. The two bays feed different production lines, and both must be served repeatedly. An environment agent e represents other warehouse traffic and determines whether the shared transport aisle is clear. The arena is shown in Figure 1. At the staging state m each robot chooses between L and R, while the environment chooses between clear and blocked. If the robots agree on L and the aisle is clear, they complete a delivery from the left bay and the play moves to ℓ ; agreement on R similarly completes a delivery from the right bay and leads to r. If the robots choose different bays, or if the aisle is blocked, the system enters the recovery state c. From ℓ and r the robots return to the staging state. At c the warehouse safety controller guarantees that the aisle is cleared before the next attempt, so the environment has no blocked action there. Thus a blockage may delay a delivery but cannot prevent deliveries indefinitely. States are labelled over =d1,d2AP=\d_1,d_2\, where d1d_1 and d2d_2 record completion of a delivery from the left and right bays respectively: (ℓ)=d1lab( )=\d_1\, (r)=d2lab(r)=\d_2\ and (m)=(c)=∅lab(m)=lab(c)= . The two weight dimensions measure the long-run service obtained by the two production lines. Completing a delivery contributes 44 to the corresponding dimension, and entering recovery incurs a unit penalty in both: w(m)=(0,0),w(ℓ)=(4,0),w(r)=(0,4),w(c)=(−1,−1).w(m)=(0,0), w( )=(4,0), w(r)=(0,4), w(c)=(-1,-1). mmccℓ (L,L,)(L,L,clear)(R,R,)(R,R,clear)(∗,∗,)(*,*,blocked)or disagreement(L,L)(L,L)(R,R)(R,R)disagreement∗*∗* Figure 1. The warehouse arena of Section 2. An edge label (a1,a2,ae)(a_1,a_2,a_e) records the actions of the two robots and the environment. The symbol ∗* matches every available robot action, and “disagreement” abbreviates the two profiles in which the robots choose different loading bays. At c the aisle has been cleared, so the environment has only the action clear and the outgoing edge labels specify only the robots’ actions. Weights are w(m)=(0,0)w(m)=(0,0), w(ℓ)=(4,0)w( )=(4,0), w(r)=(0,4)w(r)=(0,4) and w(c)=(−1,−1)w(c)=(-1,-1). Write C=1,2C=\1,2\ for the coalition of robots, and consider ψ=d1∧d2andΛq=1≥q∧2≥q.ψ\;=\;GFd_1 _2 _q\;=\;mp_1≥ q _2≥ q. The temporal objective requires both production lines to be served infinitely often, while Λq _q places a lower bound on their long-run service levels once recovery penalties are taken into account. Alternating between the two loading bays satisfies ψ, while repeatedly serving one bay can provide a high payoff in the corresponding dimension. These properties may therefore be witnessed by different policies. The formula ⟨C⟩Λqψ \! C \! _ _qψ instead requires one joint policy to satisfy both, which by 1 cannot in general be decomposed into separate qualitative and quantitative abilities. The achievable thresholds depend on how service is divided between the two bays. Suppose the aisle is blocked whenever the environment is able to block it, that is, at every visit to m. A joint policy that always agrees and alternates between the two bays then produces the play (mcℓmcr)ω(m\,c\, \,m\,c\,r)^ω, whose weights sum over one cycle to (4,4)−(2,2)=(2,2)(4,4)-(2,2)=(2,2) in six steps, so both mean payoffs equal 13 13. Hence ,m⊧⟨C⟩Λ1/3ψG,m \! C \! _ _1/3ψ. No larger common threshold can be guaranteed against this environment. Every delivery is then preceded by a visit to c, so each delivery contributes at most 4−2=24-2=2 to the sum of the two dimensions over at least three states, and the long-run average of that sum is at most 23 23. Since lim infnan+lim infnbn≤lim infn(an+bn) _na_n+ _nb_n≤ _n(a_n+b_n), we get 1(π)+2(π)≤23mp_1(π)+mp_2(π)≤ 23 for every play π, so both mean payoffs exceeding 13 13 is impossible. Thus ,m⊧̸⟨C⟩ΛqψG,m \! C \! _ _qψ for every q>13q> 13. More generally, the enforceable threshold vectors are downward closed. Their Pareto boundary describes the trade-off between the two service levels. As Section 8 shows, a boundary threshold need not be attained by a finite-memory strategy. No memoryless joint policy satisfies ψ. Such a policy fixes the robots’ choices at both m and c. If they agree at m, the environment can always play clear, so only the bay selected at m is ever served. If they disagree at m, every visit to m leads to c, where the fixed joint action completes at most one of the two deliveries. Either way the environment can prevent one of d1d_1 and d2d_2 from recurring. A two-state controller suffices: its memory records the bay served most recently. 3. Models and logic Given any set X, we use X∗X^*, XωX^ω and X+X^+ for, respectively, the sets of finite, infinite, and non-empty finite sequences of elements in X. For Y⊆XY X we write X−YX_-Y for X∖YX Y and X−iX_-i if Y=iY=\i\. We extend this notation to tuples x→=(x1,…,xn) x=(x_1,…,x_n), writing x→C x_C for the restriction of x→ x to the indices in C and x→−C x_-C for its restriction to the complement. For a sequence v we write v[t]v[t] or vtv^t for the element in position t+1t+1, so that v[0]=v0v[0]=v^0 is the first element, and v≥kv^≥ k for the suffix v[k]v[k+1]⋯v[k]v[k+1]·s. Given two vectors a→,b→∈ℚd a, b ^d, the notations a→≥b→ a≥ b and a→>b→ a> b denote componentwise inequality. Rational numbers are represented in the usual binary encoding of numerator and denominator, and ‖q‖\|q\| denotes the size of that encoding. Mean-Payoff. For an infinite sequence of real numbers r0r1r2⋯∈ℝωr_0r_1r_2·s ^ω, its mean payoff is (r)=lim infn→∞1n∑t<nrt.mp(r)\;=\; _n→∞ 1n _t<nr_t. We use the lower long-run average throughout, as in the mean-payoff game models considered below [47, 20, 45]. Mean payoff is prefix-independent: (r)=(r≥k)mp(r)=mp(r^≥ k) for every k≥0k≥ 0. Temporal Logics. We use LTLLTL [39] with the usual temporal operators X (“next”) and U (“until”), and the derived operators G (“always”) and F (“eventually”). We also use GR(1)GR(1) [6], the fragment of LTLLTL consisting of formulae of the form (ψ1∧⋯∧ψm)→(ϑ1∧⋯∧ϑk)(GF _1 ·s _m)→(GF _1 ·s _k), where each ψℓ _ and ϑr _r is a Boolean combination of atomic propositions. We write α⊧φα to indicate that the infinite sequence α∈(2)ωα∈(2^AP)^ω satisfies φ under the standard semantics. 3.1. Weighted concurrent game structures defi [Arena] An arena is a tuple =⟨N,ii∈N,ii∈N,,s,,⟩A= N,\Ac_i\_i∈ N,\Av_i\_i∈ N,St,s_init,tr,lab where N=1,…,nN=\1,…,n\ is a finite non-empty set of players, iAc_i is the finite non-empty set of actions of player i, and St is a finite non-empty set of states with initial state s∈s_init ; i:→2i∖∅Av_i:St→ 2^Ac_i \ \ is the protocol function of player i, assigning to each state the non-empty set of actions available to i there; :→2lab:St→ 2^AP is a labelling function; and tr is a transition function mapping each pair consisting of a state s∈s and an action profile ac→∈→(s):=1(s)×⋯×n(s) ac∈ Ac(s):=Av_1(s)×·s×Av_n(s) to a successor state (s,ac→)∈tr(s, ac) . For C⊆NC N we write →C(s)=∏i∈Ci(s) Ac_C(s)= _i∈ CAv_i(s) for the set of joint actions of C at s, and →−C(s) Ac_-C(s) for those of the complement. As in standard concurrent game structures [4], protocol functions allow the available actions to depend on the state. In Section 2, for instance, the environment cannot play blocked at c. Turn-based games can be represented by giving every player other than the owner of a state a single available action there. A play from s∈s is an infinite sequence π=s0s1s2⋯∈ωπ=s^0s^1s^2·s ^ω with s0=s^0=s such that for every t≥0t≥ 0 there is ac→t∈→(st) ac^t∈ Ac(s^t) with (st,ac→t)=st+1tr(s^t, ac^t)=s^t+1. A history is a non-empty finite prefix of a play, and (h)last(h) denotes its last state. A play π induces the sequence of labels (π)=(s0)(s1)⋯lab(π)=lab(s^0)lab(s^1)·s. defi [Weighted concurrent game structure] A weighted concurrent game structure (WCGS) is a tuple =⟨,w⟩G= ,w where A is an arena and w:→ℤdw:St ^d is a weight function, for some d≥1d≥ 1. We write wjw_j for the j-th component of w, D=1,…,dD=\1,…,d\ for the set of dimensions, and W=max⁡|wj(s)|:j∈D,s∈W= \|w_j(s)|:j∈ D,s \. Given a play π and a dimension j, we write j(π)=(wj(π))mp_j(π)=mp(w_j(π)) where wj(π)=wj(s0)wj(s1)⋯w_j(π)=w_j(s^0)w_j(s^1)·s. We write |||G| for the size of a standard explicit representation of G, including its transition table; in particular |→(s)|≤||| Ac(s)|≤|G| for every s, and the weights are encoded in binary, so W may be exponential in |||G|. The number d of dimensions need not coincide with the number n of agents. A dimension may represent an individual utility or a system-level quantity such as energy consumption, latency, throughput, or social welfare. We attach weights to states, whereas mean-payoff games are often presented with edge weights [47, 20]. A state-weighted game can be transformed straightforwardly into a polynomial-size edge-weighted game by assigning w(s)w(s) to every edge leaving s, preserving the mean payoff of every play. defi [Mean-payoff constraint] A mean-payoff constraint over D is generated by the grammar Λ::=⊤∣j≥q∣Λ∧Λ, ::= \; \;mp_j≥ q\; \; , where j∈Dj∈ D and q∈ℚq . We write (Λ)dim( ) for the set of dimensions occurring in Λ , call Λ one-dimensional if |(Λ)|≤1|dim( )|≤ 1, and write ‖Λ‖\| \| for the size of its binary encoding. Satisfaction by a play is defined by: π⊧⊤π always; π⊧j≥qπ _j≥ q iff j(π)≥qmp_j(π)≥ q; and π⊧Λ1∧Λ2π _1 _2 iff π satisfies both. For a threshold q=a/bq=a/b in lowest terms with b>0b>0, we write Wq=b⋅W+|a|W_q=b· W+|a| for the largest absolute weight occurring after the normalisation that replaces wjw_j by b⋅wj−ab· w_j-a. This normalisation turns j≥qmp_j≥ q into j≥0mp_j≥ 0 and is used whenever we quote a pseudo-polynomial bound. For a constraint Λ we define WΛ=max⁡Wq:(j≥q) occurs in ΛW_ = \W_q:(mp_j≥ q) occurs in \, with W⊤=0W_ =0. In running-time bounds we write W^Λ=max⁡1,WΛ W_ = \1,W_ \, so that the unconstrained case Λ=⊤ = does not collapse a multiplicative bound to zero, and similarly W^φ=max⁡1,Wφ W_ = \1,W_ \. Constraints are conjunctions of non-strict lower bounds. A robust upper bound lim supn→∞1n∑t<nwj(st)≤q _n→∞ 1n _t<nw_j(s^t)\;≤\;q can be represented by adding the negated weight dimension and requiring its lower mean payoff to be at least −q-q. A cost can therefore be represented by negating the corresponding weight dimension. An upper bound on the lower mean payoff itself is not expressible in this way. The restriction to conjunctions reflects the intended reading of a constraint as a collection of guarantees that must all hold on every outcome. Allowing disjunction would give a different semantics: a coalition could satisfy Λ1∨Λ2 _1 _2 by satisfying different disjuncts against different counter-strategies. Consequently ⟨C⟩Λ1∨Λ2ψ \! C \! _ _1 _2ψ is not equivalent to ⟨C⟩Λ1ψ∨⟨C⟩Λ2ψ \! C \! _ _1ψ \! C \! _ _2ψ, and may hold when neither disjunct does. We also exclude strict inequalities. For fixed-baseline deviations under finite-memory semantics, 20 shows that they can be replaced by non-strict rational thresholds: a fixed finite-memory strategy induces a finite graph whose cycles determine a positive rational margin. The same argument does not apply to optimal values, since an optimum need not be attained by any cycle. 3.2. Strategies and memory defi [Strategies] A strategy for player i is a function σi:+→i _i:St^+ _i with σi(h)∈i((h)) _i(h) _i(last(h)) for every history h. Such a strategy is called perfect-recall, and we write Σipr _i^pr for the set of them. A strategy σi _i is a finite-memory strategy if it can be represented by a finite-state transducer σi=(Qi,qi0,δi,τi) _i=(Q_i,q_i^0, _i, _i), where QiQ_i is a finite non-empty set of internal states with initial state qi0q_i^0, δi:Qi×→Qi _i:Q_i×St→ Q_i is a deterministic update function, and τi:Qi×→i _i:Q_i×St _i is an action function with τi(q,s)∈i(s) _i(q,s) _i(s). The transducer is read as a Mealy machine: along a play s0s1⋯s^0s^1·s the internal state evolves by qit+1=δi(qit,st)q_i^t+1= _i(q_i^t,s^t) from qi0q_i^0, and the action taken at step t is τi(qit,st) _i(q_i^t,s^t). The size of the strategy is |Qi||Q_i|, and Σifm _i^fm denotes the set of finite-memory strategies. A memoryless strategy is one with |Qi|=1|Q_i|=1, equivalently a function σi:→i _i:St _i respecting iAv_i;111Under the Mealy convention, the action may depend on the current state, so one-state transducers coincide with state-based memoryless strategies. we write Σiml _i^ml for these. Clearly Σiml⊆Σifm⊆Σipr _i^ml _i^fm _i^pr. For C⊆NC N, a C-strategy is a tuple σ→C=(σi)i∈C σ_C=( _i)_i∈ C and a counter-strategy is a (N∖C)(N C)-strategy σ→−C σ_-C. A pair (σ→C,σ→−C)( σ_C, σ_-C) is a strategy profile σ→ σ. Since tr and all strategies are deterministic, a profile σ→ σ and a state s determine a unique play, denoted π(σ→,s)π( σ,s); we write π(σ→)π( σ) for π(σ→,s)π( σ,s_init). We write ΣCκ=∏i∈CΣiκ _C^κ= _i∈ C _i^κ for κ∈pr,fm,mlκ∈\pr,fm,ml\. Since all agents have perfect information, a C-strategy can equivalently be represented by a single function σ→C:+→⋃s→C(s) σ_C:St^+→ _s Ac_C(s) prescribing a joint action after each history. We use the two representations interchangeably and measure finite memory by the size of the corresponding joint transducer. 3.3. Syntax and semantics We now extend ATL∗ATL^* by allowing each coalition modality to carry a mean-payoff constraint. defi Fix a finite set AP of atomic propositions, a set N of agents and a set D of dimensions. The state formulae φ and path formulae ψ of ATL∗ATL^*_ mp are given by the mutual grammar φ ::=p∣¬φ∣φ∧φ∣⟨C⟩Λψ, ::=p\; \; \; \; \; \; \! C \! _ \,ψ, ψ ψ ::=φ∣¬ψ∣ψ∧ψ∣ψ∣ψ, ::= \; \; ψ\; \;ψ ψ\; \;Xψ\; \;ψ Uψ, where p∈p , C⊆NC N and Λ is a mean-payoff constraint over D. Formulae of ATL∗ATL^*_ mp are state formulae. We use the usual abbreviations ∨,→,ψ=⊤ψ ,→,Fψ= Uψ and ψ=¬¬ψGψ= ψ, and write ⟨C⟩ψ \! C \! ψ for ⟨C⟩⊤ψ \! C \! _ ψ and [[C]]ψ[\![C]\!]ψ for ¬⟨C⟩⊤¬ψ \! C \! _ ψ. We use [[C]][\![C]\!] only for the qualitative case: for a non-trivial Λ , negating [[C]]Λψ[\![C]\!]_ ψ yields a condition in which either the temporal objective or the mean-payoff bounds is violated. The latter introduces a disjunction of strict upper bounds, which is not expressible by the constraint grammar of Section 3.1. An occurrence of a strategic modality is positive if it lies under an even number of negations, and a formula is positive if all of its strategic modality occurrences are positive. We attach mean-payoff constraints to coalition modalities rather than admitting mean-payoff comparisons as path atoms. This keeps the quantitative component as a side condition on the outcomes of the chosen coalition strategy. Since mean payoff is prefix-independent, applying temporal operators directly to such a comparison would add no distinction on a fixed play: (j≥q),(j≥q),andj≥qF(mp_j≥ q), (mp_j≥ q), _j≥ q would all be equivalent. Thus, ⟨C⟩Λψ \! C \! _ ψ states directly that one coalition strategy must enforce both the temporal objective ψ and the mean-payoff constraint Λ . defi The size |φ|| | of a formula is the number of its subformulae plus the total size of the encodings of the constraints occurring in it. We write (φ)sub( ) for the set of state subformulae of φ , and WφW_ for the maximum of WΛW_ over the constraints Λ occurring in φ , with Wφ=0W_ =0 if every such constraint is ⊤ . Satisfaction is parameterised by a strategy class κ for the coalition and λ for its opponents. We write ⊧κ,λ ^κ,λ, and abbreviate ⊧⁣=⁣⊧pr,pr,⊧fm⁣=⁣⊧fm,fm,⊧ml⁣=⁣⊧ml,pr. \;=\; ^pr,pr, _fm\;=\; ^fm,fm, _ml\;=\; ^ml,pr. In the memoryless semantics only the proponent coalition is restricted, following the standard convention for memoryless ATLATL and ATL∗ATL^* [41, 12, 16]. Restricting the opponents as well can change the truth of a formula, since defeating a memoryless coalition strategy may require memory. defi Let G be a WCGS. State formulae are interpreted at states and path formulae at plays. The clauses below define ⊧κ,λ ^κ,λ; the superscripts are omitted where no ambiguity arises. For states, ,s ,s ⊧p p iffp∈(s); p (s); ,s ,s ⊧¬φ iff,s⊧̸φ; ,s ; ,s ,s ⊧φ1∧φ2 _1 _2 iff,s⊧φ1 and ,s⊧φ2; ,s _1 and G,s _2; and, writing πs(σ→C,σ→−C) _s( σ_C, σ_-C) for π((σ→C,σ→−C),s)π(( σ_C, σ_-C),s), ,s⊧⟨C⟩Λψ ,s \! C \! _ ψ iff∃σ→C∈ΣCκ∀σ→−C∈Σ−Cλ: ∃ σ_C∈ _C^κ\;∀ σ_-C∈ _-C^λ: ,πs(σ→C,σ→−C)⊧ψ and πs(σ→C,σ→−C)⊧Λ. , _s( σ_C, σ_-C) ψ\ and \ _s( σ_C, σ_-C) . For a play π, ,π ,π ⊧φ iff,π[0]⊧φ, for a state formula φ; ,π[0] , for a state formula ; ,π ,π ⊧¬ψ ψ iff,π⊧̸ψ; ,π ψ; ,π ,π ⊧ψ1∧ψ2 _1 _2 iff,π⊧ψ1 and ,π⊧ψ2; ,π _1 and G,π _2; ,π ,π ⊧ψ ψ iff,π≥1⊧ψ; ,π^≥ 1 ψ; ,π ,π ⊧ψ1ψ2 _1 U _2 iff∃k≥0:,π≥k⊧ψ2 and ∀ 0≤t<k:,π≥t⊧ψ1. ∃ k≥ 0:G,π^≥ k _2 and ∀\,0≤ t<k:G,π^≥ t _1. We write ⊧φG for ,s⊧φG,s_init . The temporal and quantitative conditions are evaluated on the same outcomes of the same coalition strategy, chosen before the counter-strategy. Taking Λ=⊤ = makes the second conjunct vacuous and leaves the ATL∗ATL^* clause of [4], so ATL∗ATL^*_ mp is a conservative extension of ATL∗ATL^*. Mean-payoff constraints are prefix-independent. Hence the truth of a strategic formula at s is independent of the history leading to s, and state subformulae can be evaluated bottom-up. This would not hold for accumulated payoff or energy constraints, whose value depends on the preceding history [15, 2]. The semantics requires the temporal and quantitative conditions to be enforced by the same coalition strategy. The following proposition shows that this requirement cannot in general be recovered by checking the two abilities separately. Proposition 1 (Non-decomposability). There exist a WCGS G, a state s, a coalition C, a path formula ψ and a one-dimensional constraint Λ such that ,s⊧⟨C⟩ψand,s⊧⟨C⟩Λ⊤,but,s⊧̸⟨C⟩Λψ.G,s \! C \! ψ ,s \! C \! _ , ,s \! C \! _ ψ. Hence the combined modality is not equivalent to the conjunction of the corresponding qualitative and quantitative modalities. Proof 3.1. Let N=C=1N=C=\1\, d=1d=1 and =pAP=\p\. The game has three states s,u,vs,u,v. At s, agent 11 chooses between actions a and b, leading respectively to the absorbing states u and v; at u and v only one action is available. Let (s)=(u)=p,(v)=∅,lab(s)=lab(u)=\p\, (v)= , and w(s)=w(u)=0w(s)=w(u)=0, w(v)=1w(v)=1. Take ψ=pψ=Gp and Λ=(1≥1) =(mp_1≥ 1). Playing a produces the play suωs\,u^ω, which satisfies pGp, while playing b produces svωs\,v^ω, whose mean payoff is 11. Hence ,s⊧⟨1⟩pG,s \! \1\ \! and ,s⊧⟨1⟩1≥1⊤G,s \! \1\ \! _mp_1≥ 1 . These are the only two plays from s; the first has mean payoff 0, and the second falsifies pGp from position 11. No single strategy therefore satisfies both requirements, even in a one-player game. 4. Round-preserving sequentialisation To evaluate ⟨C⟩Λψ \! C \! _ ψ we view C as player 11 and its complement as player 22. The coalition selects a joint action first, after which the complement chooses its response. This standard sequentialisation requires modification, because the inserted intermediate states affect temporal operators containing X. The difficulty does not arise in the synthesis setting of [5, 7], whose models are turn-based. The reduction is stated for LTLLTL objectives over atomic propositions. For a nested formula, state subformulae are evaluated from the inside out and replaced by fresh propositions labelling their extensions. The following lemma shows that this preserves satisfaction along every play. Lemma 2 (Substitution). Let ψ be a path formula with maximal state subformulae φ1,…,φk _1,…, _k. Let p1,…,pkp_1,…,p_k be fresh atomic propositions, extend lab by pi∈(s)p_i (s) iff s∈[[φi]]s∈[\![ _i]\!], and let ψ′ψ be obtained from ψ by replacing each φi _i by pip_i. Then for every play π of G, ,π⊧ψG,π ψ if and only if (π)⊧ψ′lab(π) ψ in the ordinary LTLLTL sense. Proof 4.1. By induction on ψ. For ψ=φiψ= _i the claim is that ,π⊧φiG,π _i iff pi∈(π[0])p_i (π[0]), which holds by Section 3.3 and the definition of the extended labelling; the substitution is sound because the truth of a state subformula at a state does not depend on the history leading to it. The cases of ¬,∧,, , ,X, U are immediate, since the semantics of these operators coincides with their LTLLTL semantics on the label sequence and commutes with taking suffixes. 4.1. Coalition sequentialisation defi Let =⟨,w⟩G= ,w be a WCGS and let C⊆NC N. The sequentialisation of G with respect to C is the turn-based two-player weighted arena C=⟨V1,V2,E,w^,^⟩G^C= V_1,V_2,E, w, lab where V1 V_1 =, =St, V2 V_2 =(s,α):s∈,α∈→C(s), =\(s,α):s ,\ α∈ Ac_C(s)\, and E consists of the edges (s,(s,α))(s,(s,α)) for every s∈s and α∈→C(s)α∈ Ac_C(s), together with the edges ((s,α),s′)((s,α),s ) such that (s,(α,β))=s′tr(s,(α,β))=s for some β∈→−C(s)β∈ Ac_-C(s). The weight and labelling functions are lifted by w^(s)=w^(s,α)=w(s) w(s)= w(s,α)=w(s) and ^(s)=^(s,α)=(s) lab(s)= lab(s,α)=lab(s). Player 11 owns V1V_1 and player 22 owns V2V_2. When C=NC=N the set →−C(s) Ac_-C(s) is a singleton and player 22 has no choice. The construction is polynomial: |V1|+|V2|≤||2|V_1|+|V_2|≤|G|^2, and E is read off the transition table. Plays of CG^C from a vertex in V1V_1 alternate strictly between V1V_1 and V2V_2, so they have the shape ρ=s0(s0,α0)s1(s1,α1)s2⋯ρ=s^0(s^0,α^0)s^1(s^1,α^1)s^2·s. defi The projection of a play ρ=v0v1v2⋯ρ=v^0v^1v^2·s of CG^C starting in V1V_1 is the sequence (ρ)=v0v2v4⋯∈ωpr(ρ)=v^0v^2v^4·s ^ω obtained by deleting the V2V_2-vertices. Proposition 3. Let s∈s . Projection maps every play of CG^C from s to a play of G from s, and every play of G from s is the projection of some play of CG^C from s. Moreover, projection preserves every mean-payoff dimension: (w^j(ρ))=j((ρ))mp( w_j(ρ))=mp_j(pr(ρ)) for every play ρ of CG^C and every dimension j. Projection need not be injective; however, after fixing a player 11 strategy, every play of G has at most one preimage consistent with that strategy. Proof 4.2. Legality of the projection follows from the definition of E: consecutive edges st→(st,αt)→st+1s^t→(s^t,α^t)→ s^t+1 witness some βt∈→−C(st)β^t∈ Ac_-C(s^t) with (st,(αt,βt))=st+1tr(s^t,(α^t,β^t))=s^t+1. A preimage is obtained by choosing, for each original transition, a witnessing action profile and retaining its C-component. Each original state weight is duplicated exactly twice in the sequentialised play, so the two sequences of running averages have the same limit inferior; the calculation is in Appendix B. Uniqueness under a fixed player 11 strategy follows by induction, since the intermediate joint action is then determined by the preceding history. 3 shows that the usual construction suffices for the quantitative fragment. It does not preserve arbitrary temporal objectives. Each original state is duplicated by an inserted vertex carrying the same label, so the sequentialised play is a stuttered copy of the original. Evaluating pXp at s0s^0 in G tests p at s1s^1, whereas evaluating it on the sequentialised play tests p at the intermediate vertex (s0,α0)(s^0,α^0), which is labelled like s0s^0. Similarly, pXXp tests p at s1s^1 rather than at s2s^2. LTLLTL without X is stutter-invariant, so those formulae are unaffected; the full logic requires the temporal specification to advance once per concurrent round rather than once per product vertex. 4.2. Round-preserving product We therefore evaluate the automaton on the projected play, realising the projection inside an automaton product. Recall that every LTLLTL formula ψ over AP can be translated into a deterministic parity automaton (DPA) ψ=(Q,2,q0,δ,)D_ψ=(Q,2^AP,q^0,δ,pri) with L(ψ)=ξ∈(2)ω:ξ⊧ψL(D_ψ)=\ξ∈(2^AP)^ω:ξ ψ\, |Q|∈22O(|ψ|)|Q|∈ 2^2^O(|ψ|) and |(Q)|∈2O(|ψ|)|pri(Q)|∈ 2^O(|ψ|) [40, 38, 26]. A run is accepting if the least priority occurring infinitely often is even. defi [Round-preserving product] Let G be a WCGS, C⊆NC N, ψ an LTLLTL formula over AP, and ψ=(Q,2,q0,δ,)D_ψ=(Q,2^AP,q^0,δ,pri) a DPA for ψ. The round-preserving product C⊗ψG^C _ψ is the two-player weighted parity arena ⟨U1,U2,F,w¯,¯⟩ U_1,U_2,F, w, pri with U1=×QU_1=St× Q and U2=V2×QU_2=V_2× Q, and with transitions ((s,q),((s,α),q)) ((s,q),\,((s,α),q) ) ∈F ∈ F for all α∈→C(s), all α∈ Ac_C(s), (((s,α),q),(s′,δ(q,(s)))) (((s,α),q),\,(s ,δ(q,lab(s))) ) ∈F ∈ F whenever ((s,α),s′)∈E, ((s,α),s )∈ E, where w¯(u)=w(s) w(u)=w(s) for any vertex u whose St-component is s, and ¯(s,q)=¯((s,α),q)=(q) pri(s,q)= pri((s,α),q)=pri(q). Player 11 owns U1U_1 and player 22 owns U2U_2; the initial vertex for a state s is (s,q0)(s,q^0). The automaton is updated once per concurrent round, on the label of the original state in which the round began. Its priority is copied to both product vertices of that round. The parity condition on a product play therefore agrees with acceptance of the automaton run on the projected play. Lemma 4 (Projection lemma). Let ρ¯ ρ be a play of C⊗ψG^C _ψ from (s,q0)(s,q^0), let ρ be its projection to CG^C and let π=(ρ)π=pr(ρ). Then: (1) the sequence of automaton components of ρ¯ ρ, read at the U1U_1-vertices, is exactly the run of ψD_ψ on (π)lab(π); (2) ρ¯ ρ satisfies the parity condition given by ¯ pri if and only if π⊧ψπ ψ; (3) (w¯j(ρ¯))=j(π)mp( w_j( ρ))=mp_j(π) for every dimension j. Proof 4.3. The automaton component is updated once per round, on the player 22 move, and reads (st)lab(s^t), so the U1U_1-vertices of ρ¯ ρ carry exactly the run of ψD_ψ on (π)lab(π), giving (1). Priorities are duplicated by the passage from U1U_1- to U2U_2-vertices but none is introduced or removed, so the least priority occurring infinitely often agrees with that of the automaton run; since ψD_ψ is deterministic and recognises the models of ψ, this gives (2). Weights depend only on the St-component, so (3) follows from 3. Details are in Appendix B. 4.3. Strategy correspondence Let A be a turn-based two-player arena whose vertices carry a priority function ¯ pri and a weight function w¯:V→ℤd w:V ^d. We write ParPar for the set of plays of A whose least priority occurring infinitely often is even, and, for a mean-payoff constraint Λ over the d dimensions, Par∧ΛPar for the set of plays satisfying both. A mean-payoff parity objective for player 11 is an objective of this form; the product C⊗ψG^C _ψ of Section 4.2 is the instance used here. Theorem 5 (Strategy correspondence). Let G be a WCGS, s∈s , C⊆NC N, Λ a mean-payoff constraint and ψ an LTLLTL formula over AP. Then, under perfect-recall semantics, ,s⊧⟨C⟩Λψiffplayer 1 wins C⊗ψ from (s,q0) for Par∧Λ.G,s \! C \! _ ψ ~$1$ wins G^C _ψ from (s,q^0) for Par . Proof 4.4. Write Π=C⊗ψ =G^C _ψ. By 4, a play of Π satisfies Par∧ΛPar iff its projection satisfies ψ∧Λψ . It therefore remains to relate the strategies in the two games. From G to Π . Let σ→C σ_C witness ,s⊧⟨C⟩ΛψG,s \! C \! _ ψ. At each product history, player 11 plays the joint action prescribed by σ→C σ_C on its projection. Any player 22 strategy then induces a counter-strategy in G: on each prefix of the projected play, choose an action profile of the complement witnessing the corresponding transition, and define the strategy arbitrarily elsewhere. The projected play is therefore an outcome of σ→C σ_C and satisfies ψ∧Λψ . From Π to G. Let σ1 _1 be winning in Π from (s,q0)(s,q^0). By 3, each history of G has at most one preimage consistent with σ1 _1. On such a history, let σ→C σ_C play the joint action prescribed by σ1 _1, and define it arbitrarily otherwise. Every counter-strategy in G induces a player 22 strategy in Π whose outcome projects to the corresponding outcome of σ→C σ_C. Since σ1 _1 is winning, 4 implies that this projected play satisfies ψ∧Λψ . The constructions are given in full in Appendix B. Remark 6 (Quantifier order). Although player 22 observes the coalition action αtα^t in CG^C, this does not add information unavailable to the complement in G. The counter-strategy is quantified after σ→C σ_C and can therefore compute αt=σ→C(ht)α^t= σ_C(h^t) from the history. The argument relies on deterministic strategies, deterministic transitions and perfect information; it does not extend directly to randomised strategies. Finite-memory strategies require some additional care. A strategy in the product updates its memory at both vertices of each sequentialised round, whereas a coalition strategy in G updates only once per original state. We must also show that, against a fixed finite-memory coalition strategy, finite-memory counter-strategies suffice. Theorem 7 (Finite-memory correspondence). Let Λ be a mean-payoff constraint, let ψ be an LTLLTL formula, and let Π=C⊗ψ =G^C _ψ, where ψD_ψ has state space Q. Then: (1) if a finite-memory C-strategy of size m enforces ψ∧Λψ from s against every counter-strategy, then player 11 has a finite-memory strategy of size m winning Par∧ΛPar in Π from (s,q0)(s,q^0); (2) if player 11 has a finite-memory strategy of size m winning Par∧ΛPar in Π from (s,q0)(s,q^0), then C has a finite-memory strategy of size at most m⋅|Q|m·|Q| enforcing ψ∧Λψ from s against every counter-strategy; (3) for every finite-memory C-strategy, if some counter-strategy produces an outcome from s violating ψ∧Λψ , then some finite-memory counter-strategy does. Consequently ⊧fm,fm ^fm,fm and ⊧fm,pr ^fm,pr agree on every ATL∗ATL^*_ mp formula, and ,s⊧fm⟨C⟩ΛψG,s _fm \! C \! _ ψ iff player 11 has a finite-memory strategy winning Par∧ΛPar in Π from (s,q0)(s,q^0). Proof 4.5. Items (1) and (2) refine the strategy translations of 5. For (1), let σ→C σ_C be represented by a transducer of size m. At a U1U_1-vertex whose state component is s′s , the induced player 11 strategy plays the joint action prescribed by σ→C σ_C at s′s and performs the corresponding memory update. At the following U2U_2-vertex it leaves its memory unchanged. Its memory at each U1U_1-vertex therefore agrees with the memory of σ→C σ_C on the projected history, and no additional memory is required. For (2), let σ1 _1 be represented by a transducer with memory set M. The translated coalition strategy stores a pair (r,q)∈M×Q(r,q)∈ M× Q, where r is the memory state of σ1 _1 and q is the current automaton state. At an original state s′s it plays the joint action α prescribed by σ1 _1 at (s′,q)(s ,q). It then simulates, in one update, the two product updates at (s′,q)(s ,q) and at ((s′,α),q)((s ,α),q), and stores the resulting memory state together with δ(q,(s′))δ(q,lab(s )). This yields a transducer of size at most m⋅|Q|m·|Q|. In both directions, correctness follows from 4. For (3), fix a finite-memory C-strategy and the induced player 11 strategy in Π . Fixing this strategy yields a finite graph H. If some counter-strategy produces an outcome violating ψ∧Λψ , its corresponding path in H satisfies ¬Par∨¬Λ . A parity violation in a finite graph has an ultimately periodic witness. Otherwise some conjunct j≥qjmp_j≥ q_j of Λ is violated. If every reachable cycle of H had mean at least qjq_j in dimension j, the usual decomposition of a finite path into cycles and a residual simple path would imply that every infinite path has lim inf mean at least qjq_j. Hence H contains a reachable cycle of mean below qjq_j, and a lasso reaching and repeating that cycle violates Λ . In either case a violating lasso is realised by a finite-memory player 22 strategy. Tracking this lasso together with the memory of the fixed coalition strategy gives a finite-memory counter-strategy in G. The agreement of ⊧fm,fm ^fm,fm and ⊧fm,pr ^fm,pr for arbitrary formulae follows by structural induction. For a strategic formula, the induction hypothesis gives the same extensions to its maximal state subformulae under both semantics; 2 therefore gives the same substituted LTLLTL objective, and item (3) applies. The final equivalence follows from items (1) and (2). Full details are given in Appendix B. 5. Model checking The model-checking problem is to decide, given a WCGS G, a state s, and an ATL∗ATL^*_ mp formula φ , whether ,s⊧φG,s . 5.1. Model-checking procedure The model-checking procedure follows the standard bottom-up evaluation of ATL∗ATL^* [4]. Strategic subformulae are evaluated by solving the games obtained from the construction of Section 4. We first treat perfect-recall and finite-memory semantics, which use the same product construction but different game-solving characterisations; memoryless semantics requires a separate argument and is considered in Section 5.3. Let φ be an ATL∗ATL^*_ mp formula. We compute the extension of each state subformula in increasing order of nesting depth, handling Boolean subformulae by complement and intersection. For a strategic subformula χ=⟨C⟩Λψχ= \! C \! _ ψ: (1) replace each maximal state subformula of ψ by a fresh atomic proposition labelling its previously computed extension; (2) translate the resulting LTLLTL formula ψ′ψ into a deterministic parity automaton ψ′D_ψ ; (3) construct the round-preserving product Π=C⊗ψ′ =G^C _ψ of Section 4.2; (4) compute the winning region for Par∧ΛPar , requiring a finite-memory winning strategy under finite-memory semantics; (5) set the extension of χ to the states s such that (s,q0)(s,q^0) is winning for player 11. After all state subformulae have been evaluated, the formula holds at s iff s∈[[φ]]s∈[\![ ]\!]. Correctness. The proof is by induction on the nesting depth of strategic modalities. The atomic and Boolean cases are immediate. Consider χ=⟨C⟩Λψχ= \! C \! _ ψ, and suppose that the extensions of the maximal state subformulae of ψ have already been computed. By 2, a play π satisfies ψ iff its label sequence satisfies the substituted LTLLTL formula ψ′ψ . By 4, the plays of Π=C⊗ψ′ =G^C _ψ satisfying Par∧ΛPar are exactly those whose projections satisfy ψ∧Λψ . The strategy correspondence of 5 therefore identifies the winning region of Π with the extension of χ. Under finite-memory semantics, the same conclusion follows from 7. 5.2. One-dimensional game solving For one-dimensional constraints, each strategic subformula reduces to a one-dimensional mean-payoff parity game. We recall the bounds needed for the complexity analysis. One-dimensional mean-payoff games are memorylessly determined, and their threshold problem lies in NP∩coNP NP∩ coNP [25, 47]. For mean-payoff parity games, deciding whether player 11 wins Par∧(≥q)Par (mp≥ q) is polynomially equivalent to solving an energy parity game and also lies in NP∩coNP NP∩ coNP [19, Theorem 4 and Corollary 1]. Player 22 has memoryless optimal strategies, whereas player 11 may require infinite memory [20]. The winning region can be computed in time O(|E|⋅c⋅|V|c+2⋅W^q⋅(|V|+1)),O (|E|· c·|V|^c+2· W_q·(|V|+1) ), (1) where c is the number of priorities [19, Corollary 2] and W^q=max⁡1,Wq W_q= \1,W_q\ for the normalised weight bound WqW_q of Section 3. The bound is therefore pseudo-polynomial in the encoding of the threshold as well as of the weights. A one-dimensional constraint may contain several bounds on the same dimension. If Λ≠⊤ ≠ , it is equivalent to j≥q∗mp_j≥ q^*, where q∗q^* is the largest threshold occurring in Λ . We assume this normal form throughout this section. We use this pseudo-polynomial bound below.222A pseudo-quasi-polynomial algorithm is given in [24], but the bound in 8 suffice for our purposes. The finite-memory case requires a different characterisation. Lemma 8. Let ∙G be a weighted parity game with one weight dimension, |V||V| vertices, c priorities and largest absolute weight W. Player 11 has a finite-memory strategy winning Par∧(≥0)Par (mp≥ 0) from v if and only if there exists a finite initial credit from which player 11 wins the energy parity game on the same arena from v. Consequently the finite-memory threshold problem is in NP∩coNP NP∩ coNP, and whenever a finite-memory winning strategy exists there is one of memory size O(|V|⋅c⋅W)O(|V|· c· W). Proof 5.1. Suppose first that player 11 wins the energy parity game with initial credit c0c_0. Along every consistent play each partial sum is at least −c0-c_0, and hence the lim inf mean payoff is at least 0; the same strategy satisfies the parity condition. Moreover, whenever the energy parity game is winning, player 11 has a strategy of memory size O(|V|⋅c⋅W)O(|V|· c· W) [19, Theorem 1]. Conversely, fix a finite-memory strategy winning Par∧(≥0)Par (mp≥ 0) and consider the finite graph obtained by fixing that strategy. Every reachable cycle has non-negative total weight: otherwise player 22 could reach and repeat a negative cycle, producing a consistent play with negative mean payoff. The running weight along every path is therefore bounded below, since each finite path decomposes into non-negative cycles and a residual simple path. The strategy thus wins the energy parity game from some finite initial credit. The NP∩coNP NP∩ coNP bound and the stated memory bound now follow from the corresponding results for energy parity games [19, Theorems 1 and 2]. Details are in Appendix C. The equivalence in 8 holds at threshold 0, without shifting the weights. For unrestricted mean-payoff parity games, the positive shift in [19, Theorem 4] is needed because an exact threshold may be achievable only with infinite memory. In the absence of a parity condition, the zero-threshold equivalence extends to multiple dimensions [17, Theorem 3]. Theorem 9. Model checking ATL∗ATL^*_ mp with one-dimensional constraints is 2Exptime2 Exptime-complete. This holds under both perfect-recall and finite-memory semantics. Proof 5.2. Upper bound. Put m=|φ|m=| | and n=||n_G=|G|. The procedure evaluates at most m strategic subformulae, and the labelling is extended by at most m fresh propositions, so the arena never grows. Fix one strategic subformula ⟨C⟩Λψ \! C \! _ ψ and let ψ′ψ be as by substitution, with |ψ′|≤m|ψ |≤ m. Determinisation produces a DPA with |Q|≤22O(m)|Q|≤ 2^2^O(m) states and c≤2O(m)c≤ 2^O(m) priorities [40, 38, 26]. The round-preserving product has |U1|+|U2|≤n2⋅|Q||U_1|+|U_2|≤ n_G^2·|Q| vertices. By (1), solving it takes time O((n2 22O(m))c+O(1)⋅W^φ)= 2 2O(m)+ 2O(m)log⁡n⋅poly(W^φ),O ( (n_G^2\,2^2^O(m) )^c+O(1)· W_ )\;=\;2^\,2^O(m)\,+\,2^O(m) n_G·poly( W_ ), using c≤2O(m)c≤ 2^O(m) and (22O(m))2O(m)=22O(m) (2^2^O(m) )^2^O(m)=2^2^O(m). The product arena is already doubly exponential, but it is raised only to a singly exponential number of priorities, and (22am)2bm=22(a+b)m (2^2^am )^2^bm=2^2^(a+b)m. Although n_G is raised to the number c of priorities, the resulting bound is doubly exponential in the combined input size n. Indeed c≤2O(m)c≤ 2^O(m), log⁡n≤n n_G≤ n and log⁡W^φ≤O(n) W_ ≤ O(n). Summing over at most m strategic subformulae preserves the bound. Finite memory. By 7 the truth of ⟨C⟩Λψ \! C \! _ ψ at s under ⊧fm _fm is equivalent to player 11 having a finite-memory winning strategy in Π . By 8 that question is decided by solving an energy parity game on Π . The arena and priority function are unchanged, and that problem has the same pseudo-polynomial dependence on WqW_q, so the same doubly exponential bound applies. Lower bound. Set every constraint to ⊤ and every weight to 0. By conservativity this gives a linear reduction from ATL∗ATL^* model checking over concurrent game structures. For such formulae, perfect-recall and finite-memory semantics coincide, since an ω-regular objective that can be enforced over a finite game has a finite-memory witness [4, 16]. As ATL∗ATL^* model checking is 2Exptime2 Exptime-hard [4], the 2Exptime2 Exptime lower bound holds under both semantics. 5.3. Memoryless semantics The product construction does not preserve memorylessness. A positional strategy in C⊗ψG^C _ψ may choose different actions at (s,q)(s,q) and (s,q′)(s,q ), whereas a memoryless strategy in G must choose the same action whenever the current game state is s. Translating such a product strategy therefore generally introduces finite memory. We instead give a direct model-checking procedure. Theorem 10. Model checking ATL∗ATL^*_ mp under memoryless semantics is PSpace-complete, already when every constraint is ⊤ . The PSpace upper bound holds for arbitrary conjunctive mean-payoff constraints. Proof 5.3. Upper bound. Evaluate state subformulae bottom-up. For a strategic subformula ⟨C⟩Λψ \! C \! _ ψ, replace the maximal state subformulae of ψ as in 2, obtaining an LTLLTL formula ψ′ψ . Guess a memoryless joint strategy fC(s)∈→C(s)f_C(s)∈ Ac_C(s) for each state s; this strategy has a representation polynomial in |||G|. Let [fC]G[f_C] be the graph with an edge s→s′s→ s whenever (s,(fC(s),β))=s′tr(s,(f_C(s),β))=s for some action β of the complementary coalition. Its paths from s are exactly the outcomes of fCf_C: every counter-strategy induces such a path, and every such path is realised by choosing a witnessing β after each prefix, which is legitimate by the quantifier-order argument of 6. It remains to check that every path from s satisfies ψ′∧Λψ . Universal LTLLTL model checking is in PSpace [42]. For each conjunct j≥qjmp_j≥ q_j, normalise the threshold to 0 by replacing wjw_j with b⋅wj−ab· w_j-a for qj=a/bq_j=a/b. Every path then has lim inf mean at least 0 in dimension j iff every cycle reachable from s has non-negative total weight in that dimension: a negative such cycle traversed forever is a violating lasso, and conversely the running sum along any prefix is bounded below by the contribution of a simple path. For each dimension j, the existence of a reachable cycle of negative total normalised weight can be checked in polynomial time—for example by Bellman–Ford negative-cycle detection, equivalently by Karp’s minimum-cycle-mean algorithm, after restricting [fC]G[f_C] to the vertices reachable from s—so all quantitative conjuncts are verified in time O(d⋅|V|⋅|E|)O(d·|V|·|E|) in the size of [fC]G[f_C]. Guessing fCf_C therefore gives an NPSPACENPSPACE procedure, and NPSPACE=PSpaceNPSPACE= PSpace. Repeating the argument bottom-up for all state subformulae preserves the bound. Lower bound. Take C=∅C= and Λ=⊤ = . The empty coalition has a unique strategy, and its outcomes are exactly the plays of the arena, each obtained by having every agent follow the play along its prefixes. Hence ⟨∅⟩ψ \! \! ψ holds at s iff every play from s satisfies ψ, which is universal LTLLTL model checking and PSpace-hard [42]. The same bound is known for memoryless ATL∗ATL^* model checking directly [12, Theorem 13]. 6. Refined bounds for one-dimensional fragments Throughout this section, constraints are one-dimensional. The 2Exptime2 Exptime upper bound of 9 is driven by the determinisation of the temporal objective. We now consider fragments in which the temporal component admits a smaller monitor or a direct game construction. Table 2 summarises the resulting bounds. We distinguish two independent restrictions: one on the form of the path objective, and one on the Boolean and nesting structure of strategic modalities. defi According to the form of the path objective, we distinguish: • ATL∗ATL^*_ mp, the full logic of Section 3.3; • ATLATL_ mp, the fragment in which every temporal operator occurs immediately within a strategic modality; equivalently, strategic modalities have the form ⟨C⟩Λφ,⟨C⟩Λφ,or⟨C⟩Λ(φ1φ2), \! C \! _ X , \! C \! _ G , \! C \! _ ( _1 U _2), where φ,φ1,φ2 , _1, _2 are state formulae; • ATL∗[GR(1)]ATL^*_ mp[GR(1)], in which every strategic modality is applied to a GR(1)GR(1) formula over state formulae; • the quantitative fragment, consisting of the Boolean combinations of atomic propositions and quantitative strategic atoms ⟨C⟩Λ⊤ \! C \! _ . Orthogonally, we call a formula a strategic atom if it is of the form ⟨C⟩Λψ \! C \! _ ψ with ψ free of strategic modalities; flat if it is a Boolean combination of atomic propositions and strategic atoms; and nested otherwise. Since the quantitative fragment fixes every path formula to ⊤ , it is flat and has no nested case. We write Mpg for the one-dimensional mean-payoff threshold problem on two-player turn-based games and Mpp for its mean-payoff parity counterpart. Both lie in NP∩coNP NP∩ coNP [47, 20, 19], and neither is known to be in PP. The notation PMpgP Mpg and PMppP Mpp denotes polynomial time with the corresponding oracle. Since an NP∩coNP NP∩ coNP atom has polynomial certificates for both truth and falsity, a polynomial-size Boolean combination of such atoms remains in NP∩coNP NP∩ coNP: guess the truth value of each atom together with the corresponding certificate, and then evaluate the Boolean combination. We use this closure property for flat formulae throughout. The argument does not apply directly to multi-dimensional atoms, which are treated separately in Section 7. Table 2. Refined complexity bounds for one-dimensional fragments. Entries are for the fragments of Section 6 with one-dimensional constraints, and hold under both perfect-recall and finite-memory semantics. Mpg and Mpp denote the threshold problems for one-dimensional mean-payoff games and mean-payoff parity games respectively. Fragment Strategic atom Flat formula Nested formula Quantitative, ψ=⊤ψ= NP∩coNP NP∩ coNP, Mpg-equivalent NP∩coNP NP∩ coNP — ATLATL_ mp NP∩coNP NP∩ coNP, Mpg-hard NP∩coNP NP∩ coNP PMppP Mpp ATL∗[GR(1)]ATL^*_ mp[GR(1)] NP∩coNP NP∩ coNP, Mpg-hard NP∩coNP NP∩ coNP PMppP Mpp ATL∗ATL^*_ mp 2Exptime2 Exptime-complete 2Exptime2 Exptime-complete 2Exptime2 Exptime-complete 6.1. Direct constructions For the quantitative fragment no temporal monitor is needed: taking ψ=⊤ψ= collapses the product to CG^C, so an atom is a one-dimensional mean-payoff threshold query on the sequentialised arena. In ATLATL_ mp each temporal operator occurs immediately within a strategic modality, so the doubly exponential LTLLTL translation is unnecessary: each of the three operators admits a direct construction. Lemma 11. Let φ,φ1,φ2 , _1, _2 be state formulae whose extensions are already computed and let Λ be one-dimensional. Then ⟨C⟩Λχ \! C \! _ χ can be decided at all states simultaneously by solving a single mean-payoff parity game with at most two priorities on an arena of size O(||2)O(|G|^2), for χ∈φ,φ,φ1φ2χ∈\X ,\ G ,\ _1 U _2\. Proof 6.1. For φX , compute the winning region R of the mean-payoff game on CG^C; a state s is winning iff the coalition has an action α with (s,α)∈R(s,α)∈ R and every successor of (s,α)(s,α) has state component in [[φ]][\![ ]\!]. For φG , compute the maximal region in which player 11 can keep the state component inside [[φ]][\![ ]\!], a safety region obtained by attractor computation; every strategy enforcing φG remains in this region, so it remains only to enforce Λ there. For φ1φ2 _1 U _2, use two copies recording whether φ2 _2 has been reached, with the initial copy recording whether φ2 _2 already holds at s, together with a losing sink for leaving φ1 _1 beforehand. The last construction uses two priorities and the first two use at most two, each on an arena of size O(||2)O(|G|^2). The constructions are given in Appendix D. GR(1)GR(1) is a widely used fragment for reactive synthesis [6, 32]. For such objectives the general LTLLTL determinisation can be replaced by a polynomial-size deterministic parity monitor. Lemma 12 (GR(1)GR(1) monitor). Let θ=(⋀ℓ=1mψℓ)→(⋀r=1kϑr),θ\;=\; ( _ =1^mGF _ )\;→\; ( _r=1^kGF _r ), where each ψℓ _ and ϑr _r is a Boolean formula over AP and m,k≥1m,k≥ 1. There is a symbolic deterministic parity automaton recognising the models of θ, with O(mk)O(mk) states and three priorities. Its transitions are represented by Boolean guards over AP and can be constructed in time polynomial in |θ||θ|. The cases m=0m=0 and k=0k=0 are immediate. Proof 6.2. Use a cyclic counter over 1,…,m\1,…,m\ to record the next assumption ψℓ _ to be witnessed. Whenever the current letter satisfies that assumption, the counter advances; let a denote the event that the counter completes a cycle. Then ⋀ℓψℓ _ GF _ holds iff aGFa. Similarly, a cyclic counter over the guarantees produces an event b such that ⋀rϑr _rGF _r holds iff bGFb. Thus θ≡¬a∨b.θ\;≡\;FG a\; \;GFb. Take the product of the two counters and record, in each automaton state, whether the most recent transition produced a, b, both, or neither. Assign priority 0 when b occurs, priority 11 when a but not b occurs, and priority 22 otherwise. If b occurs infinitely often, priority 0 is seen infinitely often. If b occurs only finitely often but a occurs infinitely often, the least priority seen infinitely often is 11. If both events occur only finitely often, the run eventually sees only priority 22. Hence the parity condition holds exactly when ¬a∨bFG a holds. The two counters give mkmk combinations, and recording the event adds only a constant factor. Transitions are computed by evaluating the relevant Boolean guards on the current letter, so the alphabet 22^AP need not be enumerated. Details are in Appendix D. 6.2. Complexity classification Theorem 13 (One-dimensional fragments). Let the constraints be one-dimensional. Under both perfect-recall and finite-memory semantics, the following hold. (1) Deciding a quantitative strategic atom ⟨C⟩Λ⊤ \! C \! _ is polynomial-time equivalent to Mpg, and every formula of the quantitative fragment is decidable in NP∩coNP NP∩ coNP. (2) ATLATL_ mp atoms and flat ATLATL_ mp formulae are decidable in NP∩coNP NP∩ coNP and are Mpg-hard; model checking ATLATL_ mp is in PMppP Mpp. Each strategic subformula is handled in time polynomial in |||G| and the numerical weight bound W^φ W_ , and hence in pseudo-polynomial time. (3) ATL∗[GR(1)]ATL^*_ mp[GR(1)] atoms and flat ATL∗[GR(1)]ATL^*_ mp[GR(1)] formulae are decidable in NP∩coNP NP∩ coNP and are Mpg-hard; model checking ATL∗[GR(1)]ATL^*_ mp[GR(1)] is in PMppP Mpp. Each strategic subformula is handled in time polynomial in |||G|, |φ|| | and W^φ W_ . Proof 6.3. (1) Taking ψ=⊤ψ= in 5 and 7, the atom holds at s iff the threshold of Λ is enforceable in the one-dimensional mean-payoff game CG^C; perfect-recall and finite-memory winning coincide there because such games are memorylessly determined [25]. The sequentialisation is polynomial by Section 4.1, and the threshold problem is in NP∩coNP NP∩ coNP [47]. Conversely, a turn-based mean-payoff game embeds as a WCGS by giving every inactive player a single action. For an edge-weighted input, first apply the edge-splitting construction of Appendix A and double the weights to preserve the threshold. The extension to the whole fragment follows by closure, since it is flat. (2) 11 reduces each strategic atom to one mean-payoff parity game with at most two priorities, giving the NP∩coNP NP∩ coNP bound. Closure under Boolean combinations gives the bound for flat formulae. Evaluating nested formulae bottom-up requires at most one Mpp query per strategic subformula, giving PMppP Mpp. Hardness is inherited from (1) by taking χ=⊤χ=G . (3) Instantiate the procedure of Section 5 with the automaton of 12 in place of the general LTLLTL determinisation. Since the automaton is kept symbolic and its counters are updated by evaluating the guards on (s)lab(s), the product arena has size O(||2⋅m⋅k)O(|G|^2· m· k) and three priorities, the one-dimensional game-solving bounds of Section 5.2—(1) for perfect recall and 8 for finite memory—give a pseudo-polynomial running time and membership in NP∩coNP NP∩ coNP. The bounds for atoms, flat formulae and nested model checking then follow as in item (2). Hardness is inherited from the quantitative fragment by taking a tautological GR(1)GR(1) objective. Consequently the quantitative fragment is in PP if Mpg is, and both ATLATL_ mp and ATL∗[GR(1)]ATL^*_ mp[GR(1)] are in PP if Mpp is. These bounds retain the one-dimensional restriction and vary the temporal component. We next lift that restriction and consider constraints over several weight dimensions. 7. Multi-dimensional mean-payoff constraints The main perfect-recall and finite-memory results above are one-dimensional. We now allow Λ to constrain several weight dimensions simultaneously. Under memoryless semantics, the full logic with arbitrary conjunctive constraints is already covered by 10. With conjunctive constraints over several dimensions, memoryless, finite-memory and perfect-recall semantics yield different answers even for pure mean-payoff objectives [45]. We first classify pure quantitative objectives under all three semantics, and then consider the full logic under finite-memory semantics. The corresponding perfect-recall problem with a non-trivial temporal objective remains open. 7.1. Quantitative objectives When ψ=⊤ψ= , the automaton ⊤D_ has a single state with an even priority, and the round-preserving product collapses to the coalition sequentialisation CG^C. Writing Λ=⋀j∈Jj≥qjandq→=(qj)j∈J, = _j∈ Jmp_j≥ q_j q=(q_j)_j∈ J, deciding ,s⊧⟨C⟩Λ⊤G,s \! C \! _ is therefore exactly the problem of whether player 11 can enforce the threshold vector q→ q in the multi-mean-payoff game CG^C, restricted to the dimensions occurring in Λ . Under finite-memory semantics, player 11 is correspondingly restricted to finite-memory strategies. Since player 11 moves only at vertices corresponding to states of G, its positional strategies in CG^C correspond exactly to memoryless C-strategies in G. Proposition 14 (Multi-dimensional quantitative objectives). Let Λ be an arbitrary conjunctive mean-payoff constraint. Deciding ⟨C⟩Λ⊤ \! C \! _ is NP-complete under memoryless semantics and coNP-complete under both finite-memory and perfect-recall semantics. Under either of the latter two semantics, model checking flat formulae in the quantitative fragment is in P∥NPP NP_ . Proof 7.1. Since the product reduces to the polynomial-size sequentialisation CG^C, the three atom bounds follow from the corresponding results for multi-dimensional mean-payoff games [45]; hardness transfers through the embedding used in 13(1). Under finite-memory and perfect-recall semantics each atom is decidable in coNP. A polynomial-time machine can query the falsity of all atoms of a flat formula in parallel and then evaluate its Boolean structure, giving the P∥NPP NP_ bound. Unless NP=coNP NP= coNP, the flat fragment is not contained in coNP, since it contains negations of coNP-hard atoms. The identical coNP bounds under finite-memory and perfect-recall semantics do not imply that the two semantics agree: they already differ in one dimension, as 17 shows. 7.2. Full logic under finite memory Applying the coNP characterisation of explicit multi-dimensional energy games to the doubly exponential product would give a triple-exponential deterministic upper bound. Instead, we use the deterministic algorithm for the arbitrary-initial-credit problem for multi-dimensional energy parity games [23, Corollary V.5], obtaining the sharper 2Exptime2 Exptime bound below. From mean payoff to arbitrary initial credit. An energy objective treats the accumulated weight in each dimension as a running balance. Given a play ρ=v0v1⋯ρ=v_0v_1·s of a weighted arena with weight function w and an initial-credit vector c→∈ℕd c ^d, the energy condition requires c→+∑t=0k−1w(vt)≥0→ c+ _t=0^k-1w(v_t)\;≥\; 0 componentwise for every k≥0k≥ 0. The arbitrary-initial-credit problem asks whether there exists an initial credit c→ c from which player 11 can enforce this condition together with the parity objective. For example, if every reachable cycle has non-negative weight but a path to such a cycle incurs a temporary loss of 55 in one dimension, an initial credit of 55 suffices to cover that loss; repeating the cycle thereafter cannot decrease the balance further. Under finite-memory strategies, this problem characterises conjunctive mean-payoff parity objectives. Fixing a finite-memory player 11 strategy yields a finite graph. The strategy guarantees non-negative mean payoff in every dimension only if every reachable cycle has non-negative total weight in every dimension: otherwise player 22 can reach and repeat a cycle with negative weight in some dimension, yielding negative mean payoff in that dimension and violating the corresponding constraint. Conversely, if every reachable cycle has componentwise non-negative weight, then every prefix consists of such cycles together with a residual simple path; the accumulated weight is therefore bounded below, and some finite initial credit covers every temporary loss. Consequently, after normalising the thresholds to zero, each strategic subformula under finite-memory semantics can be decided by solving an arbitrary-initial-credit multi-dimensional energy parity game on the product of Section 4. Theorem 15. Model checking ATL∗ATL^*_ mp with arbitrary conjunctive mean-payoff constraints under finite-memory semantics is 2Exptime2 Exptime-complete. Proof 7.2. Hardness follows from 9 by taking every constraint to be ⊤ . For the upper bound, evaluate the formula bottom-up as in Section 5. Consider a strategic subformula ⟨C⟩Λψ \! C \! _ ψ after substitution of its maximal state subformulae, and form the round-preserving product Π=C⊗ψ =G^C _ψ. By 7, the subformula holds at s iff player 11 has a finite-memory strategy winning Par∧ΛPar in Π from (s,q0)(s,q^0). Normalise every threshold in Λ to zero and move the state weights to the outgoing edges, which changes no mean payoff. We claim that player 11 has such a finite-memory strategy iff it wins the corresponding multi-dimensional energy parity game from some finite initial-credit vector. The reverse implication is immediate: a strategy maintaining non-negative energy from a finite initial credit has lim inf mean payoff at least 0 in every dimension and satisfies the same parity condition. For the forward implication, fix a finite-memory winning strategy; the induced graph is finite, and every reachable cycle has non-negative total weight in every dimension j∈(Λ)j ( ), since otherwise player 22 could reach and repeat a negative cycle, violating the corresponding mean-payoff constraint irrespective of whether the parity condition holds along that play. Every prefix decomposes into non-negative cycles and a residual simple path, so its accumulated weight is bounded below and some finite initial credit suffices. The parity condition is unchanged, since the strategy and its consistent paths are the same. This is the componentwise extension of the argument in 8; without parity, it is [17, Theorem 3]. It remains to bound the cost of solving that problem on Π . Let N be the number of product vertices, p the number of even priorities and d the number of dimensions; then N≤||2⋅22O(|φ|)N≤|G|^2· 2^2^O(| |) and p≤2O(|φ|)p≤ 2^O(| |). The arbitrary-initial-credit problem for multi-dimensional energy parity games is solvable deterministically in time (N⋅W^Λ)O((d+p)3log⁡(d+p))(N· W_ )^O((d+p)^3 (d+p)) [23, Corollary V.5]. Let n be the combined size of G and φ . Then d≤nd≤ n, p≤2O(n)p≤ 2^O(n), log⁡N≤2O(n) N≤ 2^O(n) and log⁡W^Λ≤poly(n) W_ (n), so the logarithm of the displayed bound is O((d+p)3log⁡(d+p))⋅(log⁡N+log⁡W^Λ)= 2O(n).O ((d+p)^3 (d+p) )· ( N+ W_ )\;=\;2^O(n). Hence the game can be solved in deterministic time 22O(n)2^2^O(n). Repeating the computation for all product vertices and for all strategic subformulae preserves the bound. 7.3. Fixed number of dimensions The constructions of Section 6 use only a bounded number of priorities. When the number of weight dimensions is also fixed, the exponent in the energy-parity algorithm becomes constant. Proposition 16 (Fixed dimension). Let the number d of dimensions be fixed. Under finite-memory semantics, model checking the quantitative, ATLATL_ mp and ATL∗[GR(1)]ATL^*_ mp[GR(1)] fragments with conjunctive constraints over those dimensions is decidable in pseudo-polynomial time, that is, in time polynomial in |||G|, |φ|| | and W^φ W_ . In particular these problems are in PP when the weights and the numerators and denominators of the thresholds are written in unary. Proof 7.3. Each fragment yields a game with a bounded number of priorities. The quantitative fragment has ψ=⊤ψ= , so the product collapses to CG^C and the parity condition is trivial. The constructions of 11 give at most two priorities on an arena of size O(||2)O(|G|^2); they do not touch the weights, and the safety restriction used for φG relies only on prefix independence, so they apply verbatim to a d-dimensional constraint. The monitor of 12 has three priorities and a product arena of size O(||2⋅m⋅k)O(|G|^2· m· k). In each case, reduce to the arbitrary-initial-credit problem for multi-dimensional energy parity games, as in 15. With d and the number p of even priorities both bounded, the exponent O((d+p)3log⁡(d+p))O((d+p)^3 (d+p)) of [23, Corollary V.5] is constant, so each game is solved in time polynomial in the arena size and in W^φ W_ , and the model-checking procedure makes at most |φ|| | such calls. Under a unary encoding W^φ W_ is polynomially bounded in the input size, so the running time is polynomial. 7.4. Perfect recall The argument of 15 fixes a finite-memory strategy and reasons about the resulting finite graph. That step is unavailable for perfect-recall strategies. oprob [Perfect recall in multiple dimensions] The decidability and complexity of multi-dimensional mean-payoff parity games under perfect-recall strategies remain unknown. Without parity the problem is coNP-complete [45], as used in 14. A solution would yield the corresponding model-checking bounds for ATL∗ATL^*_ mp by 5. Existing results cover finite-memory strategies with parity [22] and perfect-recall strategies without parity [45], but not their combination. The objective Par∧ΛPar is Borel, so the resulting turn-based perfect-information games are determined [33]; what is missing is an effective characterisation of the winning region. The undecidability result of [46] concerns arbitrary Boolean combinations of limit-average constraints, including disjunction and upper bounds. Since these operators are excluded from Section 3.1, that result does not directly apply to the fragment considered here. 8. Memory requirements We now study how the available strategy memory affects strategic ability. Standard ATL∗ATL^* over finite concurrent game structures does not distinguish perfect recall from finite memory: every enforceable ω-regular objective has a finite-memory witness [4, 16]. This equivalence fails for ATL∗ATL^*_ mp, even though mean-payoff constraints do not increase the worst-case model-checking complexity (9). The three subsections have different scope. The monotonicity and strict-hierarchy results apply to arbitrary conjunctive mean-payoff constraints, with strictness already witnessed in one dimension. We then establish finite-memory approximation for one-dimensional constraints combined with a temporal objective; for pure quantitative objectives the same approximation extends componentwise to several dimensions. Finally we give tight bounds on the memory required by finite-memory witnesses, for one-dimensional constraints. 8.1. Strict memory hierarchy For positive formulae, enlarging the coalition’s strategy class preserves satisfaction, whereas enlarging the opponents’ strategy class may only destroy it. The argument is independent of the number of weight dimensions and therefore applies to arbitrary conjunctive constraints Λ . Hence ⊧ml⁣⟹⁣⊧fm⁣⟹⁣⊧. _ml\; \; _fm\; \; . For the first implication, every memoryless coalition strategy is a finite-memory strategy, while ⊧fm _fm quantifies only over finite-memory opponents rather than all perfect-recall opponents. For the second, 7 shows that ⊧fm,fm ^fm,fm agrees with ⊧fm,pr ^fm,pr; enlarging the coalition strategy class from finite memory to perfect recall then preserves satisfaction. These implications extend from strategic atoms to positive formulae by structural induction. The restriction to positive formulae is necessary because negation reverses both directions. The following theorem shows that both implications are strict. Theorem 17 (Memory hierarchy). There is a two-state, one-player WCGS G with a single weight dimension, a state s, and two formulae φ2/3,φ1 _2/3, _1 of ATL∗[GR(1)]ATL^*_ mp[GR(1)] with one-dimensional constraints, such that ,s⊧fmφ2/3 ,s _fm _2/3 and,s⊧̸mlφ2/3, ,s _ml _2/3, ,s⊧φ1 ,s _1 and,s⊧̸fmφ1. ,s _fm _1. Thus, on positive ATL∗ATL^*_ mp formulae with arbitrary conjunctive constraints, ⊧ml⁣⟹⁣⊧fm⁣⟹⁣⊧, _ml\; \; _fm\; \; , and both implications are strict, already for one-dimensional ATL∗[GR(1)]ATL^*_ mp[GR(1)] formulae over a fixed two-state game. exa [Separating game] Let N=C=1N=C=\1\, d=1d=1, =pAP=\p\, and let G have two states s and u with (s)=plab(s)=\p\, (u)=∅lab(u)= , w(s)=0w(s)=0 and w(u)=1w(u)=1. Agent 11 has 1(s)=1(u)=,Av_1(s)=Av_1(u)=\stay,go\. At either state, stay is a self-loop and go moves to the other state. For q∈ℚq write φq=⟨1⟩1≥qp _q= \! \1\ \! _mp_1≥ q\,GFp. Proof 8.1 (Proof of 17). We use the game of 17 for both separations. Since C=NC=N, every strategy determines a unique play, and the opponent strategy class is irrelevant. Memoryless is weaker than finite memory. A memoryless strategy is a choice of action at s and a choice at u. If it plays stay at s, its choice at u is irrelevant and the outcome is sωs^ω, which satisfies pGFp but has mean payoff 0. If it plays go at s and stay at u, the play is suωs\,u^ω, which fails pGFp. If it plays go at both, the play is (su)ω(su)^ω, which satisfies pGFp with mean payoff 12 12. These cases are exhaustive, so the maximum mean payoff attainable by a memoryless strategy satisfying pGFp is 12 12, and ,s⊧̸mlφ2/3G,s _ml _2/3. A two-state transducer, on the other hand, realises the play (suu)ω(suu)^ω: it plays go at s, then stay on the first visit to u and go on the second, its memory recording whether the current visit to u is the first or the second since the last visit to s. This satisfies pGFp and has mean payoff 23 23, so ,s⊧fmφ2/3G,s _fm _2/3. Finite memory is weaker than perfect recall. On the i-th visit to s, for i≥1i≥ 1, the strategy moves to u, remains there for 2i2^i positions, and then returns to s. The resulting play visits s infinitely often, so pGFp holds. The number of visits to s grows only linearly, while the total play length grows exponentially, so the asymptotic density of the weight-0 state tends to 0. Concretely, after the i-th excursion the play has length Ti=i+2i+1−2T_i=i+2^i+1-2 and accumulated weight 2i+1−22^i+1-2, so the average over that prefix is 1−i/Ti→11-i/T_i→ 1. Between successive excursion endpoints the average can decrease only at the single visit to s, which contributes weight 0; immediately after that visit the average is 1−(i+1)/(Ti+1)1-(i+1)/(T_i+1), and it increases again for the rest of the excursion. The size of the decrease therefore tends to 0, so 1=1mp_1=1 and ,s⊧φ1G,s _1. Conversely, let σ1 _1 be a finite-memory strategy of size m. Since the game and the transducer are deterministic, the induced sequence of pairs consisting of a game state and a memory state is ultimately periodic, and so therefore is the induced play π: writing π=hλωπ=h\,λ^ω, we have |λ|=ℓ≤2m|λ|= ≤ 2m. If π⊧pπ then s occurs in λ, say c≥1c≥ 1 times, and by prefix-independence 1(π)=ℓ−cℓ≤ 1−1ℓ< 1,mp_1(π)\;=\; -c \;≤\;1- 1 \;<\;1, so the constraint 1≥1mp_1≥ 1 fails. If s does not occur in λ, then pGFp fails instead. Either way no finite-memory strategy witnesses φ1 _1. The two strict inclusions have different causes. A memoryless strategy must use the same action whenever the same state is revisited, and therefore cannot vary the length of successive excursions to u. A finite-memory strategy can realise longer periodic excursions, but every induced play is ultimately periodic; it cannot make the excursion lengths grow without bound, as required to attain mean payoff 11 while still visiting s infinitely often. The difference between finite memory and perfect recall is therefore confined to the boundary threshold. In 17, φq _q holds under both ⊧ and ⊧fm _fm for every q<1q<1: choosing ℓ sufficiently large and visiting s once every ℓ positions gives mean payoff 1−1/ℓ≥q1-1/ ≥ q. Both semantics fail for q>1q>1, while only perfect recall satisfies φ1 _1. The next theorem shows that this approximation from below holds generally in one dimension. 8.2. Finite-memory approximation The following result lifts the finite-memory approximation property of mean-payoff parity games [20, 19] to coalition abilities in weighted concurrent games, through the strategy correspondence of Section 4. Theorem 18 (Finite-memory approximation). Let G be a WCGS, s a state, C a coalition, ψ an LTLLTL formula and j a dimension. For all rationals q<q′q<q , ,s⊧⟨C⟩j≥q′ψ⟹,s⊧fm⟨C⟩j≥qψ.G,s \! C \! _mp_j≥ q ψ ,s _fm \! C \! _mp_j≥ qψ. Proof 8.2. By 5, player 11 can enforce Par∧(≥q′)Par (mp≥ q ) in Π=C⊗ψ =G^C _ψ from (s,q0)(s,q^0). For every δ>0δ>0, player 11 then has a finite-memory strategy enforcing the parity condition and mean payoff at least q′−δq -δ [19, proof of Theorem 4], a property established for mean-payoff parity games in [20]. Choose 0<δ<q′−q0<δ<q -q; the resulting strategy wins for Par∧(≥q)Par (mp≥ q), and 7(2) transfers it back to a finite-memory C-strategy witnessing the conclusion. Consequently, fix G, s, C, ψ and j, and let v=supq∈ℚ:,s⊧⟨C⟩j≥qψ.v= \q :G,s \! C \! _mp_j≥ qψ\. The same value is obtained under finite-memory semantics. Indeed, every finite-memory strategy is a perfect-recall strategy, so every threshold enforceable with finite memory is also enforceable with perfect recall. Conversely, let q<vq<v be rational. By the definition of v, there is a rational q′q with q<q′q<q that is enforceable with perfect recall. By 18, q is then enforceable with finite memory. Thus the two semantics agree on every rational threshold strictly below v. They may differ only in whether v itself is attained, when v∈ℚv : in 17, for example, both semantics enforce every q<1q<1, but only perfect recall enforces the boundary threshold 11. 18 is stated for a one-dimensional constraint because its proof uses the finite-memory approximation property of one-dimensional mean-payoff parity games. For pure quantitative objectives the statement extends componentwise. If player 11 wins a multi-dimensional mean-payoff game for the threshold vector 0→ 0, then for every α>0α>0 it has a finite-memory strategy securing at least −α-α in every dimension [45, Lemma 15]. Taking ψ=⊤ψ= , so that the product collapses to CG^C as in Section 7.1, and normalising the thresholds, this gives ,s⊧⟨C⟩⋀j∈Jj≥qj′⊤⟹,s⊧fm⟨C⟩⋀j∈Jj≥qj⊤G,s \! C \! _ _j∈ Jmp_j≥ q _j ,s _fm \! C \! _ _j∈ Jmp_j≥ q_j for all rational vectors q→<q→′ q< q\, ; choose 0<α≤minj⁡(qj′−qj)0<α≤ _j(q _j-q_j) and transfer the strategy back with 7(2). Consequently the perfect-recall and finite-memory threshold regions of a quantitative strategic atom have the same downward closure, and can differ only on their Pareto boundary. We do not establish the corresponding statement for multi-dimensional constraints combined with a non-trivial temporal objective; that case would need the approximation property for multi-dimensional mean-payoff parity games, which is also the setting of Section 7.4. 8.3. One-dimensional memory bounds Constraints are one-dimensional throughout this subsection. Even when the game and temporal objective are fixed, the memory required by a finite-memory witness may depend on the numerical threshold. As in Section 5, a one-dimensional conjunction is equivalent to its strongest conjunct, so it suffices to consider constraints of the form j≥qmp_j≥ q. Theorem 19 (Tight memory bounds). The following hold. (1) Let G be the fixed two-state game of 17 and, for every integer b≥2b≥ 2, put φb=⟨1⟩1≥1−1/bp. _b\;=\; \! \1\ \! _mp_1≥ 1-1/b\,GFp. Then ,s⊧fmφbG,s _fm _b, but every witnessing finite-memory strategy has at least ⌈b/2⌉ b/2 memory states. Thus the required memory may be exponential in the binary encoding of the threshold, even though the game and temporal objective are fixed. (2) Suppose ,s⊧fm⟨C⟩j≥qψG,s _fm \! C \! _mp_j≥ qψ, where q=a/bq=a/b is in lowest terms, and let ψD_ψ have state space Q and c priorities. Then there is a witnessing finite-memory C-strategy with O(||2⋅|Q|2⋅c⋅Wq)O (|G|^2·|Q|^2· c· W_q ) memory states, where Wq=bW+|a|W_q=bW+|a|. Proof 8.3. Lower bound. A b-state counter realises the periodic play (sub−1)ω(s\,u^b-1)^ω. This play satisfies pGFp and has mean payoff (b−1)/b=1−1/b(b-1)/b=1-1/b, so it witnesses φb _b. Conversely, let a finite-memory witness have m memory states. Since the game and the strategy are deterministic, the induced play is ultimately periodic, with a period λ of length ℓ≤2m ≤ 2m. The objective pGFp requires s to occur in λ; if it occurs r≥1r≥ 1 times, then 1=ℓ−rℓ≤ 1−1ℓ.mp_1\;=\; -r \;≤\;1- 1 . Satisfying the threshold 1−1/b1-1/b therefore requires ℓ≥b ≥ b. Hence 2m≥b2m≥ b, and thus m≥⌈b/2⌉m≥ b/2 . Upper bound. By 7, player 11 has a finite-memory strategy winning Par∧(≥q)Par (mp≥ q) in the product Π=C⊗ψ =G^C _ψ. This product has |V|=O(||2|Q|)|V|=O(|G|^2|Q|) vertices and c priorities. Normalising the threshold replaces the weights by b⋅w−ab· w-a, whose absolute value is at most WqW_q. By 8, player 11 therefore has a winning strategy in Π with O(|V|⋅c⋅Wq)=O(||2|Q|⋅c⋅Wq)O(|V|· c· W_q)=O(|G|^2|Q|· c· W_q) memory states. Translating this strategy back through 7 contributes a further factor of |Q||Q|, giving the claimed bound. Each member of C may implement a private copy of the resulting joint transducer and project its joint output to its own action. Any satisfiable non-trivial threshold may be taken in [−W,W][-W,W]: thresholds below −W-W are vacuous, while thresholds above W are unenforceable. For q=a/b∈[−W,W]q=a/b∈[-W,W] we have |a|≤bW|a|≤ bW, and hence Wq≤2bW_q≤ 2bW. Consequently, when the game and temporal monitor are fixed, the upper bound is O(b)O(b), matching the Ω(b) (b) lower bound in item (1). Thus the worst-case memory requirement is Θ(b) (b) and may be exponential in the binary size of the threshold. 9. Applications and expressive limits This section gives two direct applications of the quantitative modality: temporal synthesis with performance guarantees and multi-criteria coalition objectives. We then compare the logic with cooperative rational verification. The comparison exposes an expressive limitation: the logic can impose fixed payoff thresholds, but cannot compare the payoffs induced by two strategy profiles. 9.1. Synthesis and optimisation Let C be the controlled components and N∖CN C the environment. Then ⟨C⟩Λψ \! C \! _ ψ asks whether the controller can enforce the temporal specification ψ while guaranteeing the long-run performance bounds Λ against every environment strategy. Taking Λ=⊤ = gives qualitative temporal synthesis over the game structure, while taking ψ=⊤ψ= gives a multi-mean-payoff game. When both are non-trivial, this captures reactive-controller synthesis in which safety or liveness requirements must coexist with long-run performance guarantees, for example on resource use, throughput or service reward. It is the coalition-indexed concurrent-game counterpart of the qualitative–quantitative synthesis problems studied in [5, 7]. Repeated threshold queries also yield an optimisation procedure. For fixed G, s, C, ψ and a dimension j, define vC(s,ψ,j)=supq∈ℚ:,s⊧⟨C⟩j≥qψ,v_C(s,ψ,j)\;=\; \q :G,s \! C \! _mp_j≥ q\,ψ\, with sup∅=−∞ =-∞. If the set is non-empty, it is downward closed and its supremum lies in [−W,W][-W,W]. Bisection on this interval, using the procedure of 9 as a threshold oracle, therefore approximates vC(s,ψ,j)v_C(s,ψ,j) to any prescribed additive error. By 18, perfect-recall and finite-memory semantics yield the same supremum, although they may differ in whether it is attained; 17 gives such a case. 9.2. Aggregate and multi-criteria guarantees Dimensions need not represent individual agents. They may also record system-level quantities, such as total reward, energy consumption or throughput [22, 45]. In the player-indexed case d=nd=n, dimension i represents the utility of agent i. The sum and minimum of the individual utilities give utilitarian and egalitarian social-welfare criteria, respectively; these forms of aggregation have been considered in quantitative rational synthesis and temporal equilibrium analysis [3, 31]. An egalitarian guarantee is then expressed directly by ⟨C⟩⋀i∈Ni≥qψ, \! C \! _ _i∈ Nmp_i≥ q\,ψ, which requires C to enforce ψ while guaranteeing every agent a payoff of at least q. For a utilitarian guarantee, add a dimension w(s)=∑i∈Nwi(s)w_util(s)= _i∈ Nw_i(s) and require ≥qmp_util≥ q. Since the lower mean payoff is superadditive, (π)≥∑i∈Ni(π),mp_util(π)\;≥\; _i∈ Nmp_i(π), with equality when all individual running averages converge. Separate lower bounds therefore imply a corresponding aggregate bound, but the converse need not hold: high payoff in one dimension may compensate for low payoff in another. For example, suppose that a group of service robots must repeatedly complete a collection of tasks. An egalitarian guarantee requires every robot to receive a long-run average net payment of at least q, ruling out a policy that achieves high aggregate performance by systematically under-rewarding one robot. A utilitarian guarantee instead requires the robots’ combined long-run utility to exceed a given threshold, allowing gains to one robot to compensate for losses to another. Aggregate dimensions can also express system constraints. If pi(s)p_i(s) is the payment made to robot i at state s, defining w(s)=−∑i∈Npi(s)w_bud(s)\;=\;- _i∈ Np_i(s) and requiring ≥−Bmp_bud≥-B ensures that the long-run average total payment does not exceed B, while the temporal objective ψ requires the tasks themselves to be completed. We call this an aggregate budget guarantee rather than a utilitarian one: utilitarian welfare aggregates the agents’ utilities, whereas the budget dimension measures the system’s expenditure. Note that, since mean payoff ignores finite prefixes, this is a constraint on the long-run rate of payment and not on a finite cumulative budget. For fixed C, s and ψ, let VC(s,ψ)=x→∈ℚd:,s⊧⟨C⟩⋀j∈Dj≥xjψ.V_C(s,ψ)\;=\; \ x ^d\;:\;G,s \! C \! _ _j∈ Dmp_j≥ x_j\,ψ \. This set is downward closed: a strategy enforcing x→ x also enforces every x→′≤x→ x\, ≤ x. Its maximal points describe the trade-offs among the dimensions; Section 2 illustrates this in two dimensions. For ψ=⊤ψ= , the corresponding Pareto problem is studied in [11]. With a non-trivial temporal objective, 15 gives membership queries under finite-memory semantics, while the corresponding perfect-recall problem remains open (Section 7.4). We do not consider the computation of the Pareto boundary itself. 9.3. Cooperative rational verification Cooperative rational verification asks which temporal properties hold in profiles from which no coalition has a beneficial deviation [29, 30]. Since a beneficial deviation is itself a coalition-ability query, this suggests a connection with ATL∗ATL^*_ mp. For dichotomous preferences, the standard ATL∗ATL^* encoding of core existence uses an improvement threshold fixed by the objectives. Under mean-payoff preferences, the threshold instead depends on the payoff of the candidate profile. Consequently ATL∗ATL^*_ mp expresses deviations from a fixed payoff baseline, but does not directly reproduce the core encoding. The core originates in cooperative game theory [27, 37]. In the concurrent-game formulation of [29], a strategy profile is in the core if no coalition has a deviation making every member of that coalition strictly better off, whatever the agents outside it do. With dichotomous preferences the core is always non-empty [29, Theorem 1], whereas under mean-payoff preferences it may be empty [30]. We follow [30] and specialise to the player-indexed case d=nd=n, where wiw_i is the utility of agent i and i(σ→)=i(π(σ→,s)).pay_i( σ)\;=\;mp_i(π( σ,s_init)). We use finite-memory semantics throughout the subsection. Dichotomous preferences. Let γi _i be an LTLLTL objective for agent i, with payoff 11 when γi _i holds along the outcome and 0 otherwise. Strict improvement is therefore equivalent to changing γi _i from false to true. A coalition C has a beneficial deviation precisely when every member of C currently loses and C can jointly enforce all of their objectives. The latter condition is expressed by ⟨C⟩⋀i∈Cγi \! C \! _i∈ C _i [29, Theorem 2]. Gutierrez et al. [29, Theorem 3] use this observation to encode core existence. Writing N for the set of agents, the existence of a core profile whose outcome satisfies a given LTLLTL formula φ is expressed by ΦCore(φ)=⋁W⊆N(⟨N⟩(φ∧⋀i∈Wγi∧⋀j∈N∖W¬γj)∧⋀∅≠L⊆N∖W¬⟨L⟩⋀j∈Lγj). _Core( )\;=\; _W N ( \! N \! ( _i∈ W _i _j∈ N W _j )\; _ ≠ L N W \! L \! _j∈ L _j ). Each disjunct fixes a set W of winners. The grand-coalition modality selects a profile whose outcome satisfies φ and whose winners are exactly W. The remaining conjuncts exclude a beneficial deviation by every coalition of losers. Core non-emptiness is the case φ=⊤ = . The encoding works because the deviation test ⟨L⟩⋀j∈Lγj \! L \! _j∈ L _j is independent of the profile selected by the outer modality: the winning threshold is fixed by the objectives themselves. The formula expresses the existence of a core profile. It does not express membership of an externally supplied profile, since neither ATL∗ATL^* nor ATL∗ATL^*_ mp can name that profile. Mean-payoff preferences. Define xi=i(σ→)x_i=pay_i( σ) for i∈Ci∈ C. With mean-payoff preferences, a coalition C has a beneficial deviation from σ→ σ when it has a C-strategy σ→C′ σ\, _C with i(π((σ→C′,τ→−C),s))>xifor every i∈Cpay_i (π(( σ\, _C, τ_-C),s_init) )\;>\;x_i every i∈ C and every counter-strategy τ→−C τ_-C. The baseline x→ x is the payoff vector of σ→ σ, which varies with the profile the outer modality selects. An encoding in the style of ΦCore _Core would therefore need the thresholds of an inner modality to depend on the payoff of the outer profile. The syntax of ATL∗ATL^*_ mp provides only fixed rational thresholds: it cannot name a strategy profile or compare the payoffs of two outcomes. This rules out the direct encoding; it does not establish that core non-emptiness is inexpressible in ATL∗ATL^*_ mp. Fixed-baseline deviations. Once the baseline is fixed, the deviation test is expressible: under finite-memory semantics, a strict guarantee above the baseline is equivalent to a non-strict guarantee at some larger rational threshold. Proposition 20 (Fixed-baseline deviations). Let C⊆NC N, s∈s , ψ an LTLLTL formula and x→∈ℚC x ^C. The following are equivalent. (1) There is a finite-memory C-strategy that enforces ψ and guarantees every member i∈Ci∈ C a payoff strictly greater than xix_i against every counter-strategy. (2) There is a rational vector x→′>x→ x\, > x such that ,s⊧fm⟨C⟩⋀i∈Ci≥xi′ψ.G,s _fm \! C \! _ _i∈ Cmp_i≥ x _iψ. Proof 9.1. Item (2) implies item (1): we have x→′>x→ x\, > x, and by 7 a finite-memory witness against all finite-memory counter-strategies withstands all counter-strategies. Conversely, fix a finite-memory C-strategy σ→C σ_C satisfying item (1). By 7(1) it induces a finite-memory player 11 strategy in C⊗ψG^C _ψ. Let H be the finite graph obtained by fixing that strategy. The projections of the infinite paths of H from (s,q0)(s,q^0) are exactly the outcomes consistent with σ→C σ_C, and every such path satisfies the parity condition of ψD_ψ. Fix i∈Ci∈ C and let yiy_i be the minimum mean weight in dimension i among the reachable simple cycles of H. Since every simple cycle has length at most |H||H|, this is a minimum over finitely many rationals with denominator at most |H||H|. Every finite prefix of a path of H decomposes into simple cycles together with a residual simple path, whose total weight is bounded by |H|W|H|W independently of the length of the prefix. As each simple cycle has mean at least yiy_i, every infinite path of H has lower mean payoff at least yiy_i. Conversely, a lasso reaching and repeating a simple cycle attaining yiy_i has mean payoff exactly yiy_i in dimension i, and is the outcome of some counter-strategy. By item (1) that payoff is strictly greater than xix_i, so yi>xiy_i>x_i. Taking xi′=yix _i=y_i for every i∈Ci∈ C proves item (2). For fixed C, a fixed vector x→′ x\, and ψ=⊤ψ= , the formula in item (2) is a quantitative strategic atom, whose model-checking problem is coNP-complete by 14. The fixed-baseline deviation problem additionally existentially quantifies over a rational vector x→′>x→ x\, > x, which the syntax of ATL∗ATL^*_ mp cannot do. The problem Dominated of [30] existentially chooses the deviating coalition as well as the improved payoff vector. Coalitions could be enumerated by a disjunction over the 2n−12^n-1 non-empty subsets of N, at exponential cost in formula size, but ATL∗ATL^*_ mp has no quantifier over rational threshold vectors. 20 therefore captures deviations from a fixed coalition and a fixed payoff baseline. Core existence additionally quantifies over a candidate profile and binds the deviation thresholds to the payoff of that profile. A direct encoding would require strategy variables and bindings, as provided by Strategy Logic [21, 34], extended with payoff terms referring to the outcomes induced by named strategy profiles. 10. Concluding remarks We have introduced ATL∗ATL^*_ mp, in which a strategic modality requires one coalition strategy to satisfy a temporal objective and a mean-payoff guarantee simultaneously. This combined ability is not reducible to separate qualitative and quantitative modalities (1). A round-preserving sequentialisation reduces each strategic subformula to a mean-payoff parity game while ensuring that the temporal automaton advances once per original concurrent round (5). With one-dimensional constraints, model checking is 2Exptime2 Exptime-complete (9), matching ATL∗ATL^*; the upper bound is driven by LTLLTL determinisation. With arbitrary conjunctive constraints, it remains 2Exptime2 Exptime-complete under finite-memory semantics (15). Memoryless, finite-memory and perfect-recall abilities form a strict hierarchy (17), while finite memory achieves every threshold strictly below the perfect-recall supremum (18). The required memory may be exponential in the binary size of the threshold (19). For dichotomous LTLLTL preferences, ATL∗ATL^* can encode core existence because the improvement test is fixed independently of the candidate profile. Under mean-payoff preferences, the deviation threshold is the payoff of that profile, which ATL∗ATL^*_ mp cannot name. The logic nevertheless expresses deviations from a fixed payoff baseline (20). The main open question is the decidability of multi-dimensional mean-payoff parity games under perfect-recall strategies (Section 7.4). The strategy correspondence also relies on perfect information and on deterministic strategies and transitions (6); it does not directly extend to imperfect-information, randomised or stochastic models. Acknowledgement I thank Julian Gutierrez, Anthony W. Lin, Thomas Steeples and Michael Wooldridge for the joint work on cooperative concurrent mean-payoff games from which this paper grew. References [1] A. Abate, J. Gutierrez, L. Hammond, P. Harrenstein, M. Kwiatkowska, M. Najib, G. Perelli, T. Steeples, and M. Wooldridge (2021) Rational verification: game-theoretic verification of multi-agent systems. Applied Intelligence 51 (9), p. 6569–6584. External Links: Document Cited by: §1. [2] N. Alechina, B. Logan, H. N. Nguyen, and F. Raimondi (2017) Model-checking for resource-bounded ATL with production and consumption of resources. Journal of Computer and System Sciences 88, p. 126–144. External Links: Document Cited by: §1, §3.3. [3] S. Almagor, O. Kupferman, and G. Perelli (2018) Synthesis of controllable Nash equilibria in quantitative objective games. In Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI 2018), p. 35–41. External Links: Document Cited by: §9.2. [4] R. Alur, T. A. Henzinger, and O. Kupferman (2002) Alternating-time temporal logic. Journal of the ACM 49 (5), p. 672–713. External Links: Document Cited by: item 3, §1, §3.1, §3.3, §5.1, Proof 5.2, §8. [5] R. Bloem, K. Chatterjee, T. A. Henzinger, and B. Jobstmann (2009) Better quality in synthesis through quantitative objectives. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV 2009), Lecture Notes in Computer Science, Vol. 5643, p. 140–156. External Links: Document Cited by: §1, §4, §9.1. [6] R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa’ar (2012) Synthesis of reactive(1) designs. Journal of Computer and System Sciences 78 (3), p. 911–938. External Links: Document Cited by: §3, §6.1. [7] A. Bohy, V. Bruyère, E. Filiot, and J. Raskin (2013) Synthesis from LTL specifications with mean-payoff objectives. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Lecture Notes in Computer Science, Vol. 7795, p. 169–184. External Links: Document Cited by: §1, §4, §9.1. [8] U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman (2014) Temporal specifications with accumulative values. ACM Transactions on Computational Logic 15 (4), p. 27:1–27:25. External Links: Document Cited by: §1. [9] P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, and J. Srba (2008) Infinite runs in weighted timed automata with energy constraints. In Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2008), Lecture Notes in Computer Science, Vol. 5215, p. 33–47. External Links: Document Cited by: §1. [10] P. Bouyer, O. Kupferman, N. Markey, B. Maubert, A. Murano, and G. Perelli (2023) Reasoning about quality and fuzziness of strategic behaviors. ACM Transactions on Computational Logic 24 (3), p. 21:1–21:38. External Links: Document Cited by: §1. [11] R. Brenguier and J. Raskin (2015) Pareto curves of multidimensional mean-payoff games. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015), Lecture Notes in Computer Science, Vol. 9207, p. 251–267. External Links: Document Cited by: §9.2. [12] N. Bulling, J. Dix, and W. Jamroga (2010) Model checking logics of strategic ability: complexity. In Specification and Verification of Multi-Agent Systems, M. Dastani, K. V. Hindriks, and J. Ch. Meyer (Eds.), p. 125–159. External Links: Document Cited by: §3.3, Proof 5.3. [13] N. Bulling and B. Farwer (2010) On the (un-)decidability of model checking resource-bounded agents. In Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010), Frontiers in Artificial Intelligence and Applications, Vol. 215, p. 567–572. External Links: Document Cited by: §1. [14] N. Bulling and V. Goranko (2013) How to be both rich and happy: combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract). In Proceedings of the 1st International Workshop on Strategic Reasoning (SR 2013), EPTCS, Vol. 112, p. 33–41. External Links: Document Cited by: §1. [15] N. Bulling and V. Goranko (2022) Combining quantitative and qualitative reasoning in concurrent multi-player games. Autonomous Agents and Multi-Agent Systems 36 (1), p. 2. External Links: Document Cited by: §1, §3.3. [16] N. Bulling and W. Jamroga (2014) Comparing variants of strategic ability: how uncertainty and memory influence general properties of games. Autonomous Agents and Multi-Agent Systems 28 (3), p. 474–518. External Links: Document Cited by: §3.3, Proof 5.2, §8. [17] K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin (2010) Generalized mean-payoff and energy games. In Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), LIPIcs, Vol. 8, p. 505–516. External Links: Document Cited by: §1, §5.2, Proof 7.2. [18] K. Chatterjee, L. Doyen, and T. A. Henzinger (2010) Quantitative languages. ACM Transactions on Computational Logic 11 (4), p. 23:1–23:38. External Links: Document Cited by: §1. [19] K. Chatterjee and L. Doyen (2012) Energy parity games. Theoretical Computer Science 458, p. 49–60. External Links: Document Cited by: Proof C.1, Proof C.1, item 3, §1, §5.2, §5.2, §5.2, Proof 5.1, Proof 5.1, §6, §8.2, Proof 8.2. [20] K. Chatterjee, T. A. Henzinger, and M. Jurdziński (2005) Mean-payoff parity games. In Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), p. 178–187. External Links: Document Cited by: item 3, §1, §3, §3.1, §5.2, §6, §8.2, Proof 8.2. [21] K. Chatterjee, T. A. Henzinger, and N. Piterman (2010) Strategy logic. Information and Computation 208 (6), p. 677–693. External Links: Document Cited by: §1, §1, §9.3. [22] K. Chatterjee, M. Randour, and J. Raskin (2014) Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica 51 (3–4), p. 129–163. External Links: Document Cited by: §1, §7.4, §9.2. [23] T. Colcombet, M. Jurdziński, R. Lazić, and S. Schmitz (2017) Perfect half space games. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), p. 1–11. External Links: Document Cited by: §7.2, Proof 7.2, Proof 7.3. [24] L. Daviaud, M. Jurdziński, and R. Lazić (2018) A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), p. 325–334. External Links: Document Cited by: footnote 2. [25] A. Ehrenfeucht and J. Mycielski (1979) Positional strategies for mean payoff games. International Journal of Game Theory 8 (2), p. 109–113. External Links: Document Cited by: §1, §5.2, Proof 6.3. [26] J. Esparza, J. Křetínský, and S. Sickert (2020) A unified translation of linear temporal logic to ω-automata. Journal of the ACM 67 (6), p. 33:1–33:61. External Links: Document Cited by: §4.2, Proof 5.2. [27] D. B. Gillies (1959) Solutions to general non-zero-sum games. In Contributions to the Theory of Games IV, A. W. Tucker and R. D. Luce (Eds.), Annals of Mathematics Studies, Vol. 40, p. 47–85. External Links: Document Cited by: §9.3. [28] J. Gutierrez, P. Harrenstein, and M. Wooldridge (2017) From model checking to equilibrium checking: reactive modules for rational verification. Artificial Intelligence 248, p. 123–157. External Links: Document Cited by: §1. [29] J. Gutierrez, S. Kowara, S. Kraus, T. Steeples, and M. Wooldridge (2023) Cooperative concurrent games. Artificial Intelligence 314, p. 103806. External Links: Document Cited by: §1, §9.3, §9.3, §9.3, §9.3. [30] J. Gutierrez, A. W. Lin, M. Najib, T. Steeples, and M. Wooldridge (2024) Characterising and verifying the core in concurrent multi-player mean-payoff games. In Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), LIPIcs, Vol. 288, p. 32:1–32:25. External Links: Document Cited by: §1, §9.3, §9.3, §9.3. [31] J. Gutierrez, M. Najib, G. Perelli, and M. Wooldridge (2020) Automated temporal equilibrium analysis: verification and synthesis of multi-player games. Artificial Intelligence 287, p. 103353. External Links: Document Cited by: §1, §9.2. [32] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas (2009) Temporal-logic-based reactive mission and motion planning. IEEE Transactions on Robotics 25 (6), p. 1370–1381. External Links: Document Cited by: §6.1. [33] D. A. Martin (1975) Borel determinacy. Annals of Mathematics 102 (2), p. 363–371. External Links: Document Cited by: §7.4. [34] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi (2014) Reasoning about strategies: on the model-checking problem. ACM Transactions on Computational Logic 15 (4), p. 34:1–34:47. External Links: Document Cited by: §1, §1, §9.3. [35] D. D. Monica, M. Napoli, and M. Parente (2011) On a logic for coalitional games with priced-resource agents. In Proceedings of the 3rd International Workshop on Logical Aspects of Multi-Agent Systems (LAMAS 2011), ENTCS, Vol. 278, p. 215–228. External Links: Document Cited by: §1. [36] A. Murano, D. Neider, and M. Zimmermann (2023) Robust alternating-time temporal logic. In Proceedings of the 18th European Conference on Logics in Artificial Intelligence (JELIA 2023), Lecture Notes in Computer Science, Vol. 14281, p. 796–813. External Links: Document Cited by: §1. [37] M. J. Osborne and A. Rubinstein (1994) A course in game theory. MIT Press. Cited by: §9.3. [38] N. Piterman (2007) From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science 3 (3), p. 5:1–5:21. External Links: Document Cited by: §4.2, Proof 5.2. [39] A. Pnueli (1977) The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), p. 46–57. External Links: Document Cited by: §3. [40] S. Safra (1988) On the complexity of ω-automata. In Proceedings of the 29th Annual Symposium on Foundations of Computer Science (FOCS 1988), p. 319–327. External Links: Document Cited by: §4.2, Proof 5.2. [41] P. Schobbens (2004) Alternating-time logic with imperfect recall. In Proceedings of the 1st International Workshop on Logic and Communication in Multi-Agent Systems (LCMAS 2003), ENTCS, Vol. 85(2), p. 82–93. External Links: Document Cited by: §3.3. [42] A. P. Sistla and E. M. Clarke (1985) The complexity of propositional linear temporal logics. Journal of the ACM 32 (3), p. 733–749. External Links: Document Cited by: Proof 5.3, Proof 5.3. [43] T. Steeples, J. Gutierrez, and M. Wooldridge (2021) Mean-payoff games with ω-regular specifications. In Proceedings of the 20th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2021), p. 1272–1280. External Links: Document Cited by: §1. [44] M. Ummels and D. Wojtczak (2011) The complexity of Nash equilibria in limit-average games. In Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR 2011), Lecture Notes in Computer Science, Vol. 6901, p. 482–496. External Links: Document Cited by: §1. [45] Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J. Raskin (2015) The complexity of multi-mean-payoff and multi-energy games. Information and Computation 241, p. 177–196. External Links: Document Cited by: §1, §3, §7.4, Proof 7.1, §7, §8.2, §9.2. [46] Y. Velner (2015) Robust multidimensional mean-payoff games are undecidable. In Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), Lecture Notes in Computer Science, Vol. 9034, p. 312–327. External Links: Document Cited by: §7.4. [47] U. Zwick and M. Paterson (1996) The complexity of mean payoff games on graphs. Theoretical Computer Science 158 (1–2), p. 343–359. External Links: Document Cited by: §1, §3, §3.1, §5.2, Proof 6.3, §6. Appendix A State and transition weights Remark 21 (State weights versus transition weights). We attach weights to states rather than to transitions. State and transition weights are not interchangeable without adjusting the construction. The usual encoding of a transition-weighted game splits each transition s→s′s→ s through a fresh state carrying the weight of the transition, with the original states given weight 0→ 0. A play of the original game of length n then becomes a play of length 2n2n carrying the same total weight, so the mean payoff is halved, not preserved; thresholds must be scaled accordingly, or, equivalently, the transition weights doubled. Moreover the inserted states introduce stuttering and therefore do not preserve arbitrary LTLLTL formulae containing X. The scaling can be corrected by doubling the transition weights, or equivalently by scaling the thresholds; the stuttering can be handled by updating the temporal automaton only at the original states, as in the round-preserving product of Section 4. We avoid both adjustments by taking state weights as primitive. Appendix B Proofs for the strategy correspondence Proof B.1 (Proof of 3). We argue the three claims separately. Projection. By Section 4.1, each pair of consecutive edges st→(st,αt)→st+1s^t→(s^t,α^t)→ s^t+1 of a play ρ witnesses the existence of βt∈→−C(st)β^t∈ Ac_-C(s^t) with (st,(αt,βt))=st+1tr(s^t,(α^t,β^t))=s^t+1, so every consecutive pair of (ρ)pr(ρ) is a legal transition of G. Surjectivity. Given a play π=s0s1⋯π=s^0s^1·s of G, choose for each t an action profile ac→t∈→(st) ac^t∈ Ac(s^t) with (st,ac→t)=st+1tr(s^t, ac^t)=s^t+1 and put αt=ac→Ctα^t= ac^t_C; then s0(s0,α0)s1⋯s^0(s^0,α^0)s^1·s is a play of CG^C projecting to π. If a player 11 strategy σ1 _1 is fixed, the V2V_2-vertices of a play consistent with σ1 _1 are determined by σ1 _1 applied to the prefixes already built, so the preimage is unique by induction on t. Mean payoff. Write π=(ρ)=s0s1⋯π=pr(ρ)=s^0s^1·s. By construction the weight sequence of ρ is wj(s0)wj(s0)wj(s1)wj(s1)⋯w_j(s^0)\,w_j(s^0)\,w_j(s^1)\,w_j(s^1)·s, each value repeated twice, so for an even prefix length 2n2n, 12n∑t<2nw^j(ρ[t])=12n⋅2∑t<nwj(st)=1n∑t<nwj(st), 12n _t<2n w_j(ρ[t])\;=\; 12n· 2 _t<nw_j(s^t)\;=\; 1n _t<nw_j(s^t), and for an odd prefix length the two quantities differ by at most 2W/(2n+1)2W/(2n+1), which tends to 0. Hence the two sequences of running averages have the same lim inf . Proof B.2 (Proof of 4). (1) By induction on t. The U1U_1-vertices of ρ¯ ρ are (s0,q0),(s1,q1),…(s^0,q^0),(s^1,q^1),… where, by Section 4.2, qt+1=δ(qt,(st))q^t+1=δ(q^t,lab(s^t)); this is the defining recursion of the run of ψD_ψ on (s0)(s1)⋯=(π)lab(s^0)lab(s^1)·s=lab(π). (2) By (1), the set of automaton states visited infinitely often along ρ¯ ρ coincides with the set visited infinitely often by the run of ψD_ψ on (π)lab(π); the passage from U1U_1- to U2U_2-vertices duplicates each priority but introduces and removes none. Hence the least priority occurring infinitely often is the same on both sides, and since ψD_ψ is deterministic and recognises exactly the models of ψ, the two conditions agree. (3) The weight of a product vertex depends only on its St-component, so w¯j(ρ¯)=w^j(ρ) w_j( ρ)= w_j(ρ) and 3 applies. Proof B.3 (Proof of 5). Write Π=C⊗ψ =G^C _ψ and let ObjObj denote Par∧ΛPar . We write pr also for the composite projection from plays of Π to ωSt^ω. By 4, a play ρ¯ ρ of Π lies in ObjObj iff (ρ¯)⊧ψ∧Λpr( ρ) ψ . From G to Π . Let σ→C σ_C be a C-strategy such that every counter-strategy yields an outcome satisfying ψ and Λ . Define σ1 _1 in Π as follows: for a history h¯ h of Π ending in a U1U_1-vertex with automaton component q and state component s′s , put σ1(h¯)=((s′,α),q) _1( h)=((s ,α),q) where α=σ→C((h¯))α= σ_C(pr( h)). This is a legal move, since α∈→C(s′)α∈ Ac_C(s ). Let σ2 _2 be any player 22 strategy, let ρ¯ ρ be the resulting play from (s,q0)(s,q^0) and put π=(ρ¯)π=pr( ρ). By 3, π is a play of G, and by construction it is consistent with σ→C σ_C: the joint action taken at round t is σ→C(π[0]⋯π[t]) σ_C(π[0]·sπ[t]). It remains to exhibit a counter-strategy realising the complement’s moves. Since G and σ→C σ_C are deterministic, the histories ht=π[0]⋯π[t]h^t=π[0]·sπ[t] are pairwise distinct, having distinct lengths; define σ→−C(ht)=βt σ_-C(h^t)=β^t, where βt∈→−C(π[t])β^t∈ Ac_-C(π[t]) is any profile witnessing the edge ((π[t],σ→C(ht)),π[t+1])∈E((π[t], σ_C(h^t)),π[t+1])∈ E, and let σ→−C σ_-C be arbitrary on all other histories. Then πs(σ→C,σ→−C)=π _s( σ_C, σ_-C)=π, so by hypothesis π⊧ψ∧Λπ ψ and hence ρ¯∈Obj ρ . As σ2 _2 was arbitrary, σ1 _1 is winning. From Π to G. Let σ1 _1 be a winning player 11 strategy in Π from (s,q0)(s,q^0). By 3, every history h=s0⋯sth=s^0·s s^t of G from s has at most one preimage in Π consistent with σ1 _1 and ending in a U1U_1-vertex; write Phys.Rev.Eσ1(h) Phys.~Rev.~E_ _1(h) for that preimage when it exists. Explicitly, Phys.Rev.Eσ1(s0)=(s0,q0) Phys.~Rev.~E_ _1(s^0)=(s^0,q^0) and Phys.Rev.Eσ1(h⋅st+1)=Phys.Rev.Eσ1(h)⋅σ1(Phys.Rev.Eσ1(h))⋅(st+1,δ(q,(st))), Phys.~Rev.~E_ _1(h· s^t+1)\;=\; Phys.~Rev.~E_ _1(h)· _1( Phys.~Rev.~E_ _1(h))·(s^t+1,δ(q,lab(s^t))), where q is the automaton component of the last vertex of Phys.Rev.Eσ1(h) Phys.~Rev.~E_ _1(h); this is defined exactly when st+1s^t+1 is a tr-successor of sts^t under some completion of the joint action chosen by σ1 _1. Now set σ→C(h)=α σ_C(h)=α, where σ1(Phys.Rev.Eσ1(h))=(((h),α),q) _1( Phys.~Rev.~E_ _1(h))=((last(h),α),q), taking σ→C(h) σ_C(h) arbitrary on histories with no preimage. Let σ→−C σ_-C be any counter-strategy and put π=πs(σ→C,σ→−C)π= _s( σ_C, σ_-C). Every prefix of π has a preimage: at round t the coalition plays αt=σ→C(ht)α^t= σ_C(h^t), the complement plays some βtβ^t, and (π[t],(αt,βt))=π[t+1]tr(π[t],(α^t,β^t))=π[t+1] witnesses the player 22 edge in Π . Hence there is a player 22 strategy σ2 _2 whose play against σ1 _1 is Phys.Rev.Eσ1 Phys.~Rev.~E_ _1 applied to the prefixes of π. Since σ1 _1 is winning, that play lies in ObjObj, so π⊧ψ∧Λπ ψ by 4. As σ→−C σ_-C was arbitrary, σ→C σ_C witnesses ,s⊧⟨C⟩ΛψG,s \! C \! _ ψ. Proof B.4 (Proof of 7, items (1) and (2)). (1) The strategy σ1 _1 built in the proof of 5 consults σ→C σ_C on the projected history and otherwise needs only the current vertex, so a transducer of size m for σ→C σ_C yields one of size m for σ1 _1: the memory update reads the St-component of the current U1U_1-vertex, which is exactly the letter σ→C σ_C would read. (2) In the second half of the proof of 5, the joint action σ→C(h) σ_C(h) is determined by the memory state of σ1 _1 after Phys.Rev.Eσ1(h) Phys.~Rev.~E_ _1(h) together with the automaton component reached. The latter is not a function of (h)last(h), so σ→C σ_C must track ψD_ψ itself; the product of the two gives a transducer of size m⋅|Q|m·|Q|. Each agent of C can implement a private copy of the transducer. Proof B.5 (Proof of 7, item (3)). Suppose some counter-strategy σ→−C σ_-C produces an outcome π with π⊧̸ψ∧Λπ ψ . Let σ1 _1 be the player 11 strategy of 7(1), of memory size m, and let Π[σ1] [ _1] be the finite graph obtained from Π by fixing σ1 _1; its vertices are pairs of a Π -vertex and a memory state, so |Π[σ1]|≤m⋅|U1∪U2|| [ _1]|≤ m·|U_1∪ U_2|. The preimage of π is a path in Π[σ1] [ _1] violating Par∧ΛPar , that is, satisfying ¬Par∨¬Λ . Each disjunct admits an ultimately periodic witness in a finite graph. For ¬Par this holds because the condition is ω-regular. For ¬Λ , choose a conjunct j≥qjmp_j≥ q_j of Λ that this path violates; if every reachable cycle of Π[σ1] [ _1] had mean at least qjq_j in dimension j, then decomposing each finite prefix into cycles and a residual simple path would give every infinite path lim inf mean at least qjq_j; so such a path has lim inf mean below qjq_j only if some reachable cycle of Π[σ1] [ _1] has mean below qjq_j in that dimension, and traversing that cycle forever is an ultimately periodic witness. Fix such a lasso in Π[σ1] [ _1]; it is realised by a player 22 strategy of memory size at most |Π[σ1]|| [ _1]|. Translating that strategy back into a counter-strategy in G requires computing, at each round, the joint action σ→C σ_C prescribes; since σ→C σ_C has memory m, a counter-strategy of memory at most m⋅|Π[σ1]|m·| [ _1]| suffices. This is a finite-memory counter-strategy defeating σ→C σ_C, contrary to hypothesis. Proof B.6 (Proof of the final claim of 7). Item (3) concerns a single strategic formula with a fixed LTLLTL path formula, so the passage to arbitrary φ requires an induction. We argue by structural induction on φ , showing that the two relations give it the same extension [[φ]]⊆[\![ ]\!] . The atomic and Boolean cases are immediate, since neither relation quantifies over strategies there. Let φ=⟨C⟩Λψ = \! C \! _ ψ and let φ1,…,φk _1,…, _k be the maximal state subformulae of ψ. By the induction hypothesis each [[φi]][\![ _i]\!] is the same under both relations, so the extended labelling, and hence the LTLLTL formula ψ′ψ of 2, are the same under both. By that lemma, satisfaction of ψ along a play is then the fixed ω-regular condition (π)⊧ψ′lab(π) ψ , independent of the strategy classes. Applying item (3) of 7 to ψ′ψ gives that a finite-memory C-strategy defeats every finite-memory counter-strategy if and only if it defeats every counter-strategy, so the two relations agree at φ . For the second claim, combine this with 7(1) and (2). Appendix C Finite-memory mean-payoff parity games Proof C.1 (Proof of 8). (⇐ ) A strategy winning the energy parity game with initial credit c0c_0 keeps every partial sum of weights at least −c0-c_0 and satisfies the parity condition, so along any consistent play 1n∑t<nw(vt)≥−c0/n→0 1n _t<nw(v^t)≥-c_0/n→ 0 and hence ≥0mp≥ 0. Player 11 has such a strategy of memory size O(|V|⋅c⋅W)O(|V|· c· W) [19]. (⇒ ) Let σ1 _1 be a finite-memory strategy of size m winning Par∧(≥0)Par (mp≥ 0), and let H be the finite graph ∙[σ1]G [ _1] obtained by fixing σ1 _1, with at most |V|⋅m|V|· m vertices. Every reachable cycle of H has non-negative weight sum: a cycle of negative sum could be traversed forever by player 22, yielding a consistent play of mean payoff equal to that cycle’s mean, which is negative, contradicting the hypothesis. Hence along any path of H the running sum never drops below −|V|⋅m⋅W-|V|· m· W, since a prefix decomposes into simple cycles, each of non-negative sum, and a simple path of length at most |V|⋅m|V|· m. Hence σ1 _1 wins the energy parity game with initial credit |V|⋅m⋅W|V|· m· W. Membership in NP∩coNP NP∩ coNP and the memory bound are then those of energy parity games [19]. Appendix D Direct constructions for restricted fragments Proof D.1 (Proof of 11). We use throughout that Λ is prefix-independent. Next. Solve the one-priority mean-payoff game CG^C for the threshold of Λ and let R be player 11’s winning region. Then ,s⊧⟨C⟩ΛφG,s \! C \! _ X iff there is α∈→C(s)α∈ Ac_C(s) such that (s,α)∈R(s,α)∈ R and every s′s with ((s,α),s′)∈E((s,α),s )∈ E satisfies φ . Indeed, such an α lets the coalition force the next state into [[φ]][\![ ]\!] while retaining a strategy enforcing Λ from (s,α)(s,α) onwards, and conversely any witness prescribes such an α at s. Safety. Compute by attractor computation the maximal region R′R from which player 11 can keep the play inside [[φ]][\![ ]\!] forever in CG^C; this is a safety game, solvable in linear time. Restrict CG^C to R′R , removing player 11 moves that leave it. Any strategy enforcing φG stays in R′R , and any strategy staying in R′R enforces φG ; since Λ is prefix-independent it is unaffected by the restriction. The result is a one-priority mean-payoff game. Until. Take two copies of CG^C indexed by a bit recording whether a φ2 _2-state has already been visited, together with a self-looping sink. Throughout, a vertex of CG^C is said to satisfy a state formula when its St-component does, which lifts [[φ1]][\![ _1]\!] and [[φ2]][\![ _2]\!] to the intermediate vertices as well. The vertices are V×0,1V×\0,1\ together with ⊥ , and the initial vertex for a state s is ι(s)=(s,1)if s∈[[φ2]],(s,0)if s∈[[φ1]]∖[[φ2]],⊥otherwise. (s)\;=\; cases(s,1)&if s∈[\![ _2]\!],\\ (s,0)&if s∈[\![ _1]\!] [\![ _2]\!],\\ &otherwise. cases The case distinction is what makes the construction correct when φ2 _2 already holds at s, so that φ1φ2 _1 U _2 is satisfied with k=0k=0. From (v,0)(v,0) the play moves to (v′,1)(v ,1) if v′v satisfies φ2 _2, to (v′,0)(v ,0) if v′v satisfies φ1 _1 but not φ2 _2, and to ⊥ otherwise; from (v,1)(v,1) it moves to (v′,1)(v ,1) for every successor v′v . Priorities are ¯(v,0)=¯(⊥)=1 pri(v,0)= pri( )=1 and ¯(v,1)=0 pri(v,1)=0, and weights are inherited from the St-component, with ⊥ given weight 0. A play satisfies the parity condition iff it eventually enters the 11-indexed copy, that is, iff its projection satisfies φ1φ2 _1 U _2: a play remaining in the 0-indexed copy or entering ⊥ has least priority 11 occurring infinitely often and is losing, while a play entering the 11-indexed copy has priority 0 recurring. Note that the parity condition alone does the work; no additional penalty on ⊥ is needed, and none is imposed. Since Λ is prefix-independent and the tail of a winning play lies entirely in the 11-indexed copy, the mean payoff of a play equals that of its projection. The arena has 2|V|+12|V|+1 vertices and two priorities. Proof D.2 (Proof of 12). Write A=⋀ℓ≤mψℓA= _ ≤ mGF _ and B=⋀r≤kϑrB= _r≤ kGF _r, so θ=¬A∨Bθ= A B. A counter ℓ∈1,…,m ∈\1,…,m\ is incremented modulo m whenever ψℓ _ holds, and the event a is its wrap-around; then A holds iff a occurs infinitely often. The guarantees are treated the same way, with counter r and event b. The events a and b are produced by transitions, whereas Section 4.2 reads priorities off states, so the event is recorded in the state: a control state is a triple (ℓ,r,e)( ,r,e) with e∈,a,b,abe∈\ none,a,b,ab\ recording which wrap-arounds were caused by the letter just read. This multiplies the state count by four and leaves the bound O(mk)O(mk) unchanged. Assign priority 0 to states with e∈b,abe∈\b,ab\, priority 11 to states with e=ae=a, and priority 22 to states with e=e= none. The transition function is not tabulated over the alphabet 22^AP, which would be exponential in |||AP|. It is kept symbolic: each transition out of a control state is guarded by one of the Boolean formulae ψℓ _ or ϑr _r, and in the product of Section 4.2 the two counters are updated by evaluating those formulae on (s)lab(s), in time polynomial in |θ||θ| per transition.

Instant research discovery