Answer: \(\mathrm{NP}\text{-hard}\), even with \(m=2\), \(|W|=2\), and a fixed rational next-step formula.
Theorem 4 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateThe global model checking problem for R-ATL over GCSP with short-sighted preferences is Ptime-complete.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite type set \(T\) with \(|T|=\tau\), rational mass vector \(\mu\in\mathbb Q_{\ge0}^{\tau}\), finite public state \(w\), finitely encoded anonymous clone-symmetric transition maps from \((w,\mu)\) and a type-action mass vector \(z\) to successor \((w',\mu')\), finitely encoded short-sighted preference preorders over each type's personal one-step outcomes, a valuation by rational polyhedral predicates, and an \(R\text{-ATL}\) formula \(\varphi\), decide exactly whether the atomless population satisfies \(\varphi\) at \((w,\mu)\) when coalitions are measurable subsets of \(\bigsqcup_{t\in T}[0,\mu_t)\) and rationality uses pointwise strong non-dominance almost everywhere.
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. Initial masses need not sum to one; their positive total is conserved. There are \(m\) action names and a nonempty finite public-state set \(W\).
The population consists of persistent individuals in \(X=\bigsqcup_{t\in T}[0,\mu_t)\), with Lebesgue measure. Each coalition named in the formula is a fixed measurable subset, possibly empty. Encode the joint membership patterns of all named coalitions by immutable attributes of types, with binary-rational masses; individuals may change their other type attributes, but never their coalition memberships.
At state \(s=(w,\mu)\), each type has a nonempty available-action set. Every measurable action profile is executable and induces real masses \(z_{ta}\geq0\) with \(\sum_a z_{ta}=\mu_t\); these masses are not restricted to rationals.
Transitions are deterministic and anonymous: input rules specify \(w'\) and each type-action group's next type \(q(t,a,s,z)\), preserving membership attributes, and \(\mu'_u=\sum_{t,a:q(t,a,s,z)=u}z_{ta}\). Individuals retain their identities. Successor masses may be zero; no types outside the input list appear.
Use finite guarded rational piecewise-affine descriptions: guards are Boolean combinations of rational linear equalities and strict or weak inequalities; available actions, public successors and next-type outputs are determined by such guards. Rules are promised total and single-valued on executable profiles. Atomic valuations and preference comparisons use the same predicate encoding.
Each type at each state has a total preference preorder over personal one-step outcomes \((q(t,a,s,z),w',\mu')\); later outcomes are irrelevant, and equal one-step outcomes are indifferent. No stability assumption is imposed.
An action is strongly dominated for an individual if another available action gives a strictly preferred one-step outcome against every measurable action profile of all other individuals. A unilateral deviation has zero mass, so it leaves \(z\) unchanged, while its personal next type is recomputed. Rationality means choosing an undominated action almost everywhere in the coalition.
Strategies are pure, measurable in individuals at every finite public-state history, and have perfect recall. Ordinary capability existentially quantifies a coalition strategy against all unrestricted complement strategies. Rational capability adds the preceding rationality condition at the state where the modality is evaluated; it does not impose rationality at later histories.
The language consists of Boolean combinations of atoms and ordinary or rational coalition modalities with \(\mathsf X\), \(\mathsf G\), and \(\mathsf U\). Along every resulting path \(s_0s_1\ldots\), \(\mathsf X\psi\) requires \(\psi(s_1)\); \(\mathsf G\psi\) requires \(\psi(s_k)\) for every \(k>0\); \(\psi\mathsf U\chi\) requires some \(k>0\) with \(\chi(s_k)\) and \(\psi(s_h)\) for \(1\leq h<k\).
Is exact satisfaction of an input \(R\text{-ATL}\) formula \(\varphi\) at an input state \((w,\mu)\) solvable in polynomial time, or is it \(\mathrm{NP}\)-hard? State running times in \(m\), \(\tau\), \(|W|\), \(|\varphi|\), and the total binary input length \(L\).
For explicitly represented finite concurrent games with short-sighted preferences, global \(R\text{-ATL}\) model checking is \(\mathrm{P}\)-complete ([source](https://arxiv.org/html/2502.12286v1#S7)). No result settling this precise atomless problem was located.
Exact satisfaction is \(\mathrm{NP}\)-hard, already with \(\ m=2\), \(\lvert W\rvert=2\), a fixed formula of constant length, unchanged type masses, and complete indifference between outcomes.
Consequently, a running time polynomial in \(\ m,\tau,\lvert W\rvert,\lvert\varphi\rvert,L\) would imply \(\mathrm P=\mathrm{NP}\). The proof applies to both ordinary and rational capability.
Let \(\ F=\bigwedge_{j=1}^{r}D_j\) be a Boolean formula in conjunctive normal form, with variables \(\ v_1,\ldots,v_n\), where each clause has at most three literals. Deciding satisfiability of these formulas is \(\mathrm{NP}\)-complete. We may assume \(\ n\geq1\): adding an unused variable preserves satisfiability.
Construct the following society.
The initial total mass is \(\ n\), which is permitted by the task.
For an executable profile, put \(\ x_i=z_{t_i,1}\). Feasibility gives
\(\ z_{t_i,0}=1-x_i,\qquad 0\leq x_i\leq1.\)
For a literal \(\ell\), define its affine value by
\(\ h_{v_i}(x)=x_i,\qquad h_{\neg v_i}(x)=1-x_i.\)
Define the guard
\(\ B_F(z)=\left(\bigwedge_{i=1}^{n}(x_i=0\ \lor\ x_i=1)\right)\land\left(\bigwedge_{j=1}^{r}\left(\sum_{\ell\in D_j}h_\ell(x)\geq1\right)\right).\)
This is a permitted Boolean combination of rational linear predicates. In particular, each clause contributes a single affine inequality involving at most three coordinates.
The public transition rules are:
Let the atom \(\ p\) hold exactly when the public state is \(\ w_1\). Use the fixed formula
\(\ \varphi=\langle\!\langle C\rangle\!\rangle^{\mathrm{rat}}\mathsf Xp.\)
Transitions and conservation. The guards \(\ B_F\) and \(\neg B_F\) are mutually exclusive and exhaustive, so the public transition is total and single-valued. Type outputs are constant, hence are valid guarded piecewise-affine descriptions. For each type,
\(\ \mu'_{t_i}=z_{t_i,0}+z_{t_i,1}=\mu_{t_i}.\)
Thus all masses remain positive and equal to their initial values. No new type appears, individuals retain their identities, and coalition membership is preserved.
Real profiles and measurability. Every vector \(\ x\in[0,1]^n\) is realizable by a pure measurable profile: in the interval belonging to type \(\ t_i\), assign action \(\ 1\) to \(\ [0,x_i)\) and action \(\ 0\) to \(\ [x_i,1)\). These sets are measurable and have the required masses.
Preferences and rationality. Universal indifference is a total preorder, represented by a constantly true comparison predicate. Its strict part is empty. Therefore no available action is strongly dominated: no alternative gives a strictly preferred outcome against any profile, let alone every profile. Every executable strategy is consequently rational at the initial state.
A chosen initial profile extends to a strategy by prescribing action \(\ 0\) at every later history. Availability is unconditional, and the resulting action assignment is measurable at every history.
We prove
\(\ F\text{ is satisfiable}\quad\Longleftrightarrow\quad(w_0,\mu)\models\varphi.\)
Forward direction. Let \(\ b\in\{0,1\}^n\) satisfy \(\ F\). Choose action \(\ b_i\) for every individual of type \(\ t_i\). Then \(\ x_i=b_i\), so all endpoint conditions hold.
For Boolean coordinates, \(\ h_\ell(b)\) equals \(\ 1\) exactly when literal \(\ell\) is true, and otherwise equals \(\ 0\). Each satisfied clause therefore has literal-value sum at least \(\ 1\). Thus \(\ B_F(z)\) holds, and the first successor has public state \(\ w_1\), where \(\ p\) is true.
The strategy is rational by complete indifference. Since \(\ C=X\), the complement is empty and has no choices. Determinism gives a unique resulting path. Hence the rational coalition enforces \(\mathsf Xp\).
Reverse direction. Suppose \(\ (w_0,\mu)\models\varphi\). The witnessing strategy supplies an executable initial profile, with real coordinates \(\ x_i=z_{t_i,1}\). Because the first successor satisfies \(\ p\), its public state is \(\ w_1\). From \(\ w_0\), this occurs only when \(\ B_F(z)\) holds.
Its endpoint conditions imply \(\ x_i\in\{0,1\}\) for every \(\ i\). Define the Boolean assignment \(\ b_i=x_i\). Every clause inequality says that the sum of its Boolean literal values is at least \(\ 1\), so at least one literal is true. Thus \(\ b\) satisfies every clause of \(\ F\).
This direction explicitly excludes fractional false positives: although arbitrary real splits are executable, a successful profile must satisfy every endpoint condition.
The equivalence also holds for \(\langle\!\langle C\rangle\!\rangle\mathsf Xp\), because rationality excludes no strategy.
Using sparse linear expressions and binary type indices, the construction has
\(\ m=2,\qquad\tau=n,\qquad\lvert W\rvert=2,\qquad\lvert\varphi\rvert=O(1),\qquad L=O((n+r)\log(n+1)).\)
There are \(\ O(n+r)\) predicate and rule occurrences. All numerical coefficients, constants, and initial masses have bounded binary length. Writing the construction takes \(\ O((n+r)\log(n+1))\) time under this encoding; in particular, the reduction is polynomial.
The restricted family constructed above is itself \(\mathrm{NP}\)-complete. A certificate consists of \(\tau\) Boolean choices, and checking the guard takes polynomial time in \(\ L\). Enumerating these choices gives a decision procedure for this family in \(\ O(2^\tau\operatorname{poly}(L))\) time. This is an upper bound for the restricted family, not for arbitrary temporal formulas in the full model.
Thus even a bound of the form \(\ f(m,\lvert W\rvert,\lvert\varphi\rvert)\operatorname{poly}(\tau,L)\) for the full problem would imply \(\mathrm P=\mathrm{NP}\), since those three arguments are fixed in the reduction.
The cited finite-game result establishes polynomial-time model checking for explicitly represented finite games with short-sighted preferences. [Li, Lorini, and Mittelmann, Section 7](https://arxiv.org/html/2502.12286v1#S7). Here, the guarded representation compactly encodes the search over Boolean profiles. The reduction proves that computing even this one-step capability from that representation is already \(\mathrm{NP}\)-hard.
⟨structured verdict parsed — rendered above⟩
The prover’s reduction is correct and resolves the requested complexity alternative: exact satisfaction is \(\mathrm{NP}\)-hard, even with two actions, two public states, a constant-length formula, invariant type masses, and universal indifference. No major or minor mathematical issues were found.
The output establishes a lower bound for the full problem and an upper bound only for its constructed restricted family. It does not claim that the full problem belongs to \(\mathrm{NP}\).
The source problem is satisfiability of conjunctive-normal-form Boolean formulas with at most three literals per clause, a standard \(\mathrm{NP}\)-complete problem. Adding an unused variable preserves satisfiability and ensures \(n\geq 1\).
The construction uses exactly \(n\) explicitly listed types, each of positive binary-rational mass \(1\). Thus \(\tau=n\) is genuinely the support size. The total mass is \(n>0\), which the task explicitly permits.
The grand coalition \(C=X\) is measurable. Giving every type its immutable membership attribute correctly represents this coalition.
Both actions are unconditionally available, so available-action sets are nonempty.
Every predicate in \(B_F\) is permitted:
The public-state rules are exhaustive and mutually exclusive. The absorbing rule at \(w_1\) completes the transition specification. Constant next-type outputs are permitted descriptions and preserve coalition membership.
The conservation calculation is correct:
\[
\mu'_{t_i}=z_{t_i,0}+z_{t_i,1}=\mu_{t_i}.
\]
Starting from the specified initial state, all type masses therefore remain \(1\). No new type appears, and individuals retain their identities.
The atomic valuation \(p\) depends only on the finite public-state component and is representable in the stipulated encoding.
At the initial state, executability gives
\[
z_{t_i,0}+z_{t_i,1}=1,
\qquad
0\leq x_i=z_{t_i,1}\leq 1.
\]
The stated interval partition realizes every such vector by a pure measurable profile. The endpoints \(x_i=0\) and \(x_i=1\) cause no difficulty: one of the two action sets is empty.
The extension prescribing action \(0\) at every later history is available and measurable. A strategy may ignore its history, so this extension satisfies the perfect-recall strategy specification. The initial choice requires no information about later masses or histories.
Universal indifference is a total preorder, respects the requirement that equal outcomes be indifferent, and has a constantly true comparison predicate.
Its strict part is empty. Consequently, no alternative action can give a strictly preferred outcome against every profile of the other individuals. The quantification over those profiles is nonempty because actions are unconditionally available.
Thus neither action is strongly dominated, and every executable initial profile is rational. The zero-mass unilateral-deviation convention introduces no additional issue: the preference comparison remains indifferent for every recomputed personal outcome.
Given a satisfying Boolean assignment \(b\), assigning action \(b_i\) to all individuals of type \(t_i\) produces \(x_i=b_i\). All endpoint conditions hold.
On Boolean coordinates, the literal values have exactly the stated truth interpretation. Hence each satisfied clause has literal-value sum at least \(1\), and \(B_F\) holds.
The first successor is therefore \(w_1\), where \(p\) holds. Because the coalition is the entire population, the complement has exactly one empty strategy assignment. Determinism gives a unique resulting path. Rationality was already verified, so the rational next-step modality is satisfied.
This uses precisely the task’s semantics of \(\mathsf X\), which evaluates the first successor.
A witnessing strategy supplies an executable initial profile. Satisfaction of \(\mathsf Xp\) forces the first successor’s public state to be \(w_1\). From the initial state \(w_0\), the transition rules permit this exactly when \(B_F\) holds.
The endpoint conjuncts then force every \(x_i\) to be Boolean. Each clause inequality implies that at least one of its Boolean literal values is \(1\). Therefore the assignment \(b_i=x_i\) satisfies \(F\).
This correctly excludes fractional false positives. No assumption that arbitrary executable masses are rational is used.
The same equivalence holds for ordinary capability because rationality removes no strategies.
The argument also handles unused variables, repeated literals, and tautological clauses. If empty clauses are allowed, their sum is \(0\), making the guard unsatisfiable as required. If there are no clauses, the clause conjunction is true, matching satisfiability of the empty conjunction.
The allowed empty-complement case is used legitimately; it does not change or evade the task’s capability semantics.
Under the explicitly stated sparse encoding with binary type indices, the bound
\[
L=O((n+r)\log(n+1))
\]
is justified. Each clause has at most three literal occurrences, all numerical constants and coefficients have bounded binary length, and duplicating the guard for complementary transition branches changes size only by a constant factor.
The claimed construction time is consistent with this output size and is polynomial.
For the constructed family, a certificate of \(\tau\) Boolean choices suffices, and guard evaluation takes polynomial time in \(L\). Together with the reduction, this supports the claimed \(\mathrm{NP}\)-completeness of that restricted family. Its enumeration bound
\[
O(2^\tau\operatorname{poly}(L))
\]
is correctly restricted to that family.
Because \(m\), \(|W|\), and \(|\varphi|\) are fixed in the reduction, both stated consequences for hypothetical polynomial algorithms follow.
The cited source states polynomial-time completeness of global model checking for finite concurrent games with short-sighted preferences in Section 7. The prover uses this only as context, not as a theorem applied to the atomless construction. That distinction is valid. [Li, Lorini, and Mittelmann, Section 7](https://arxiv.org/html/2502.12286v1#S7).
None. The write-up establishes the claimed hardness result without relying on a missing lemma or an unverified transfer from finite games.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.