Answer: \(\mathrm{NP}\text{-hard}\) for admissible, complete, grounded, preferred, stable, and coalition-structure semantics; all are in \(\Delta_2^{\mathrm P}\).
Corollary 7 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateIf Lsem,CF ∈NP (resp. NP-complete) then model checking ATLc is in ∆P 2 (resp. ∆P 2 -complete) with respect to sem. In [11] the complexity of credulous reasoning with re- spect to the preferred and stable extensions is analyzed and determined to be NP-complete. This is in the line with our result: there can be a polynomial number of calls to mcheck(M, q, ⟨|A|⟩ψ) (where ψ does not contain any cooper- ation modality ⟨|·|⟩).
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite-state game with types \(T\), rational masses \(\mu_t\), transitions specified over aggregate action masses, state-dependent type-level attack and preference frameworks, and an ATLc formula, decide whether state \(q\) satisfies the formula. A coalition is a mass vector \(x\) with \(0\leq x_t\leq\mu_t\); for seed mass \(a\), it is valid if \(a\leq x\) and its positive support is an extension under the chosen semantics, or if \(x=a\). In the strategic modality, mass \(x\) chooses actions against the remaining population.
A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
The input game has an explicitly listed nonempty state set \(Q\), proposition labels, an action alphabet of size \(m\), and nonempty available-action sets \(D_t(q)\). At each state, its deterministic transition function is encoded by a finite list of cells, each a conjunction of binary-rational linear equalities or strict or weak inequalities in aggregate type/action masses \(z_{t,b}\), labelled by a successor state. These cells must partition all feasible profiles \(z\geq0\) with \(\sum_{b\in D_t(q)}z_{t,b}=\mu_t\); unavailable-action coordinates are zero.
At each state, an explicitly given framework has a nonempty domain \(C_q\subseteq T\), an attack relation, and a preference preorder \(\preceq_q\). Type \(t\) defeats \(u\) exactly when it attacks \(u\) and \(u\) is not strictly preferred to \(t\), where strict preference is the strict part of \(\preceq_q\). Use standard Dung extension semantics on this defeat graph, with one fixed choice \(\sigma\) among admissible, complete, grounded, preferred, and stable; coalition-structure semantics means the unique grounded extension.
Coalitions are real vectors \(0\leq x\leq\mu\). For a binary-rational seed vector \(0\leq a\leq\mu\), coalition \(x\) is valid at \(q\) exactly when \(x=a\), or when \(a\leq x\) and \(\{t:x_t>0\}\) is a \(\sigma\)-extension of the framework at \(q\). Empty seeds and empty extensions are allowed.
A coalition strategy is a pure, perfect-information, memoryless choice at every state of real allocations \(y_{t,b}\geq0\) satisfying \(\sum_{b\in D_t(q)}y_{t,b}=x_t\). At every step its opponents may choose any real allocations \(v_{t,b}\geq0\) summing to \(\mu_t-x_t\), and the successor is determined by \(z=y+v\).
Formulas are standard ATL formulas with binary-rational mass vectors as coalition annotations, extended by \(\langle|a|\rangle\gamma\), where \(\gamma\) has the ATL forms next, always, or strong until. Ordinary strategic modalities quantify over the strategies just defined. The formation modality holds exactly when some coalition valid at the evaluation state can enforce \(\gamma\); that coalition stays fixed throughout the temporal objective, and validity is tested only at the evaluation state.
For each fixed \(\sigma\), is deciding \(M,q\models\varphi\) for this mass model in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? State running times in \(m\), \(\tau\), \(|Q|\), formula length \(\ell\), the number of transition cells \(r\), and total input bit length \(L\).
Discrete ATLc has a \(\Delta_2^{\mathrm P}\) upper bound when extension membership is in \(\mathrm{NP}\); the anchor additionally states completeness when membership is \(\mathrm{NP}\)-complete. [Source](https://aamas.csc.liv.ac.uk/Proceedings/aamas08/proceedings/pdf/paper/AAMAS08_0544.pdf)
A later CoalATL variant, with a different coalition-validity convention, proves \(\Delta_2^{\mathrm P}\)-completeness for stable semantics and \(\mathrm P\)-completeness for grounded semantics, and corrects preferred-extension membership to \(\mathrm{coNP}\)-complete. [Source](https://journal.iberamia.org/public/ia-old/articles/641/article%20%281%29.pdf)
No result settling this precisely specified mass model was located.
For every listed semantics, model checking this mass model is \(\mathrm{NP}\)-hard. This includes grounded semantics and coalition-structure semantics. Hardness already holds with two actions, three states, and a single empty-seed formation next modality.
All these model-checking problems also belong to \(\Delta_2^{\mathrm P}=\mathrm P^{\mathrm{NP}}\). Thus the answer to the requested dichotomy is \(\mathrm{NP}\)-hard for every semantics; polynomial-time solvability would imply \(\mathrm P=\mathrm{NP}\).
Let \(n=|Q|\), \(d=m\tau\), and \(r\) be the total number of transition cells across all states. Let \(L\) be the total input bit length and \(\ell\) the formula length. A deterministic upper bound proved below is
\(O\!\left(L+n\tau^3+\ell n^3 c_\sigma(r+L+d+2)^{O((d+1)^2)}\right)\),
where the constants implicit in the exponent are absolute, and
| Semantics | Classification | \(c_\sigma\) |
|---|---|---|
| Admissible | \(\mathrm{NP}\)-hard; in \(\Delta_2^{\mathrm P}\) | \(2^\tau\) |
| Complete | \(\mathrm{NP}\)-hard; in \(\Delta_2^{\mathrm P}\) | \(2^\tau\) |
| Grounded | \(\mathrm{NP}\)-hard; in \(\Delta_2^{\mathrm P}\) | \(1\) |
| Preferred | \(\mathrm{NP}\)-hard; in \(\Delta_2^{\mathrm P}\) | \(2^\tau\) |
| Stable | \(\mathrm{NP}\)-hard; in \(\Delta_2^{\mathrm P}\) | \(2^\tau\) |
| Coalition structure | Same as grounded | \(1\) |
In particular, model checking is polynomial-time solvable when both \(m\) and \(\tau\) are fixed. With \(m=1\), it is polynomial-time solvable without fixing \(\tau\).
The proofs below use the promised well-formedness of the transition partition.
Suppose \(0\leq x\leq x'\leq\mu\), coordinatewise. Fix a memoryless strategy \(y\) for coalition \(x\).
At each state \(q\), select an available action \(b_t(q)\in D_t(q)\) for each type \(t\). Define a strategy for \(x'\) by adding the extra mass \(x'_t-x_t\) to that action:
\(y'_{t,b}(q)=y_{t,b}(q)+(x'_t-x_t)\mathbf 1_{\{b=b_t(q)\}}\).
Its allocations sum to \(x'_t\), so it is legal. For any opponent allocation \(v'\) against \(x'\), put
\(v_{t,b}=v'_{t,b}+(x'_t-x_t)\mathbf 1_{\{b=b_t(q)\}}\).
Then \(v\) is legal against \(x\), and \(y'+v'=y+v\). Consequently, every outcome path of the new strategy is an outcome path of the original strategy.
Thus, for next, always, and strong until, if \(x\) can enforce the objective, then \(x'\) can enforce it. This conclusion does not require \(x'\) to be valid: it is a statement about strategic ability.
For \(E\subseteq T\), define the saturated coalition \(x^E\) by
\(x^E_t=\mu_t\) if \(t\in E\), and \(x^E_t=0\) otherwise.
Because every \(\mu_t\) is positive, its support is exactly \(E\).
If a valid coalition \(x\ne a\) has support \(E\), then \(E\) is a \(\sigma\)-extension and
\(a\leq x\leq x^E\).
Moreover, \(a\leq x^E\) is equivalent to \(\operatorname{supp}(a)\subseteq E\). By monotonicity, any objective enforceable by \(x\) is enforceable by \(x^E\), which is itself valid.
Therefore formation is equivalent to considering only:
This reduces the continuum of candidate coalitions to at most \(1+2^\tau\) candidates. For grounded semantics there is at most one extension candidate in addition to the seed.
Each candidate remains fixed throughout its temporal objective.
For the specified validity convention, these three semantics give the same truth value to every formation modality.
We justify the argumentation fact needed here. Write \(F(S)\) for the set of arguments defended by \(S\) in the defeat graph.
Every admissible set \(S\) in a finite framework is contained in a preferred extension: choose an inclusion-maximal admissible superset of \(S\). It is globally maximal, since any larger admissible set would also contain \(S\).
Every preferred extension \(P\) is complete. To see this, suppose \(u\in F(P)\setminus P\). The set \(P\cup\{u\}\) is conflict-free:
All members of \(P\cup\{u\}\) are defended by this set, because \(P\) already defends both its members and \(u\). Thus it is admissible, contradicting maximality. Hence \(F(P)=P\).
Now suppose a saturated admissible coalition \(x^E\) contains the seed and wins. Extend \(E\) to a preferred extension \(P\). Then \(x^E\leq x^P\), so \(x^P\) also wins and contains the seed. Conversely, complete and preferred extensions are admissible.
This proves the equivalence. The seed alternative is identical for all three semantics. Consequently, their entire formula semantics also coincide, by induction on formulas.
We reduce from satisfiability of a \(3\)-CNF formula \(F\) with variables \(X_1,\ldots,X_N\) and clauses \(K_1,\ldots,K_C\). We may restrict to \(N,C\geq1\) and clauses on distinct variables; this remains an \(\mathrm{NP}\)-hard restriction.
All numerical values in the construction are dyadic rationals. Thus the construction works even if “binary-rational” is read as requiring finite binary expansions.
Create variable types \(t_1,\ldots,t_N\), and one selector type \(s\). Put
\(k=\lceil\log_2(N+1)\rceil,\qquad \delta=2^{-k},\qquad \rho=1-N\delta\).
Each variable type has mass \(\delta\), and the selector type has mass \(\rho>0\). The masses sum to one.
There are two actions, \(0\) and \(1\), available to every type at every state. There are three states:
Each absorbing state has one unconditional transition cell.
Consider the coalition
\(x_{t_i}=\delta\quad(1\leq i\leq N),\qquad x_s=0\).
At \(q_0\), write
\(u_i=z_{t_i,1},\qquad w=z_{s,1}\).
For this coalition, \(u_i\) is controlled entirely by the coalition and lies in \([0,\delta]\). The selector coordinate \(w\) is controlled entirely by the opponents and can take any value in \([0,\rho]\).
There are \(J=N+C\) tests. The first \(N\) test Booleanity, and the remaining \(C\) test the clauses.
Let \(h=\lceil\log_2 J\rceil\). Define
\(\beta_j=j\rho/2^h\quad(0\leq j<J),\qquad \beta_J=\rho\).
Partition the selector range into nonempty intervals:
\(I_j=[\beta_{j-1},\beta_j)\quad(1\leq j<J),\qquad I_J=[\beta_{J-1},\rho]\).
Each interval is described by a conjunction of permitted linear inequalities. Its endpoints have polynomial binary bit length.
For the Booleanity test of variable \(i\), use three cells, each also requiring \(w\in I_i\):
| Additional constraints | Successor |
|---|---|
| \(u_i=0\) | \(g\) |
| \(u_i=\delta\) | \(g\) |
| \(0<u_i<\delta\) | \(b\) |
These cells partition the feasible profiles in that selector interval.
For clause \(K_j\), define the linear expression
\(S_j(u)=\sum_{X_i\text{ occurs positively in }K_j}u_i+\sum_{\neg X_i\text{ occurs in }K_j}(\delta-u_i)\).
Within selector interval \(I_{N+j}\), use two cells:
| Additional constraint | Successor |
|---|---|
| \(S_j(u)\geq\delta\) | \(g\) |
| \(S_j(u)<\delta\) | \(b\) |
The selector intervals partition \([0,\rho]\), and the cells inside each interval partition its feasible profiles. Therefore the entire transition list satisfies the required partition condition.
We claim
\(F\text{ is satisfiable}\quad\Longleftrightarrow\quad M,q_0\models\langle\!\langle x\rangle\!\rangle\mathbf Xp\).
If \(F\) has a satisfying assignment, allocate \(u_i=\delta\) for true variables and \(u_i=0\) for false variables. Every Booleanity test succeeds. Each satisfied clause has at least one literal contributing \(\delta\), so every clause test succeeds. Every opponent allocation therefore leads to \(g\).
Conversely, suppose the coalition can enforce \(\mathbf Xp\). Its allocation must pass every test, since opponents can select a point in every selector interval. The Booleanity tests imply \(u_i\in\{0,\delta\}\) for all \(i\). Interpret \(u_i=\delta\) as \(X_i\) being true.
For a Boolean allocation, each term in \(S_j\) equals \(\delta\) precisely when its literal is true, and equals zero otherwise. Hence \(S_j(u)\geq\delta\) means that clause \(K_j\) is satisfied. All clauses are therefore satisfied.
At every state, take the framework domain to be
\(C_q=\{t_1,\ldots,t_N\}\),
with no attacks and the identity preference preorder.
In an attack-free graph, the entire domain is an extension under every listed semantics. Indeed, every set is admissible, while the entire domain is the unique complete, grounded, preferred, and stable extension.
Use the zero seed. Every valid coalition has selector mass zero and is coordinatewise at most \(x\). Conversely, \(x\) is valid under every semantics. Monotonicity therefore gives
\(M,q_0\models\langle|0|\rangle\mathbf Xp \quad\Longleftrightarrow\quad M,q_0\models\langle\!\langle x\rangle\!\rangle\mathbf Xp\).
Thus the same reduction proves hardness for formation under every semantics.
The reduction has
\(m=2,\qquad \tau=N+1,\qquad |Q|=3,\qquad r=3N+2C+2\),
and polynomial total bit length. The formula has a single strategic modality; its explicitly represented zero annotation has \(\tau\) coordinates.
To prove the upper bounds, we must justify replacing real winning allocations by polynomial-size rational ones. Strict inequalities make this step substantive.
Fix a state, a rational coalition \(x\), and a target set of states \(S\). Remove unavailable coordinates and let their remaining number be \(d_q\leq d\).
For a legal coalition allocation \(y\), a transition cell is reachable by opponents exactly when it contains an aggregate profile \(z\) satisfying
\(z\geq y,\qquad \sum_{b\in D_t(q)}z_{t,b}=\mu_t\).
Indeed, \(v=z-y\) is then precisely a legal opponent allocation.
Call a cell bad if its successor lies outside \(S\). A winning allocation must make every bad cell unreachable.
For one bad cell, introduce a common slack variable \(\varepsilon\). Replace each strict inequality \(a_jz<b_j\) by
\(a_jz+\varepsilon\leq b_j\),
and impose \(0\leq\varepsilon\leq1\). Keep weak inequalities unchanged, and express equalities as pairs of weak inequalities.
Together with the aggregate-profile constraints, this gives a system
\(A\xi\leq h(y),\qquad \xi=(z,\varepsilon),\qquad h(y)=b+By\).
The coefficient matrix \(A\) is independent of \(y\). Whenever feasible, the system has a compact feasible set: the aggregate coordinates lie between zero and their type masses, and \(\varepsilon\in[0,1]\).
The original cell is reachable exactly when this system has a solution with \(\varepsilon>0\). For finitely many strict inequalities, their positive slacks have a positive minimum. If there are no strict inequalities, any feasible aggregate profile can be combined with \(\varepsilon=1\).
There are two ways the cell can be unreachable.
First, the closed system can be infeasible. By Farkas’ lemma, this is equivalent to the existence of
\(\lambda\geq0,\qquad A^{\mathsf T}\lambda=0,\qquad \mathbf1^{\mathsf T}\lambda=1,\qquad \lambda^{\mathsf T}h(y)<0\).
The normalized multiplier set is a compact polytope. If the last inequality holds somewhere, it holds at a vertex.
Second, the closed system can be feasible but have maximum slack zero. Let \(c\) select the \(\varepsilon\)-coordinate. Strong linear-programming duality applies because the primal is feasible and bounded. There is then a dual multiplier satisfying
\(\lambda\geq0,\qquad A^{\mathsf T}\lambda=c,\qquad \lambda^{\mathsf T}h(y)=0\).
An optimal vertex multiplier exists. One direct justification is to take an optimal multiplier with minimum positive support. Dependence among its supported columns would permit a support-reducing perturbation preserving feasibility and optimality, contradicting that choice.
Consequently, for finite vertex sets \(V_0,V_1\) depending only on \(A\), unreachability is exactly
\(\left(\bigvee_{\lambda\in V_0}\lambda^{\mathsf T}h(y)<0\right) \;\lor\; \left(\bigvee_{\lambda\in V_1}\lambda^{\mathsf T}h(y)\leq0\right)\).
The second disjunction is sufficient even when the closed system is infeasible, so this expression covers both cases.
The vector \(\xi\) has \(d_q+1\) coordinates. A vertex in \(V_0\) has at most \(d_q+2\) positive coordinates; a vertex in \(V_1\) has at most \(d_q+1\). Otherwise the corresponding columns admit a nonzero perturbation contradicting extremality.
Each vertex is therefore determined by a linear system of size at most \(d_q+2\). Clearing rational denominators and applying Cramer’s rule bounds its binary bit length by a polynomial in the input length and \(d_q\). The affine inequalities \(\lambda^{\mathsf T}h(y)<0\) and \(\lambda^{\mathsf T}h(y)\leq0\) inherit polynomial bit length.
Suppose a real winning allocation exists. For each bad cell, select one certificate inequality true at that allocation. Conjoin these inequalities with the legal-allocation constraints
\(y\geq0,\qquad \sum_{b\in D_t(q)}y_{t,b}=x_t\).
This is a feasible rational linear system with weak and strict inequalities and polynomial total description length.
It has a polynomial-size rational solution. To verify this, replace its strict inequalities by inequalities with a common slack \(\eta\), impose \(0\leq\eta\leq1\), and maximize \(\eta\). The legal-allocation domain is bounded. If strict inequalities are present, feasibility of the original system gives a positive optimum; an optimal vertex has polynomial bit length by the same determinant bound. Without strict inequalities, take a vertex of the bounded feasible polytope.
We have proved:
Rational-witness lemma. Whenever a real one-step winning allocation exists for a rational coalition and a specified successor target set, a rational winning allocation of polynomial binary bit length exists.
A guessed rational allocation can be verified in polynomial time: for each bad cell, solve the slack linear program above and check that no positive slack is feasible.
Suppose the state subformulas of a strategic modality have already been evaluated.
For a fixed rational coalition, guess a rational memoryless allocation at every state. For every transition cell, use linear programming to determine whether opponents can reach it. This constructs the finite outcome graph of the guessed strategy.
Every path in this graph is realizable by opponent allocations: each edge has a witnessing allocation, and opponents may choose it whenever that edge is taken.
The temporal objective can now be checked in polynomial time:
The last condition is equivalent to strong until. A reachable cycle permits an infinite outcome avoiding \(R\). Conversely, an infinite path avoiding \(R\) in a finite graph must repeat a state.
These certificates are complete. Given a winning real memoryless strategy, let \(S_q\) be its possible successor set at state \(q\). Apply the rational-witness lemma separately at each state to obtain rational allocations whose successor sets are contained in \(S_q\). The resulting outcome graph is a subgraph of the original one and therefore still satisfies the universal temporal objective.
Hence each fixed-coalition, labelled next, always, or until query belongs to \(\mathrm{NP}\).
By Section 1, it suffices to select either the seed or a saturated coalition.
Admissibility and stability are verifiable in polynomial time from the defeat graph. The grounded extension is computable by iterating the defence operator from the empty set; there are at most \(\tau\) strict increases, each computable in \(O(\tau^2)\) graph operations.
Combine the support certificate with the polynomial-size strategy certificate. Each labelled formation query therefore belongs to \(\mathrm{NP}\), including preferred semantics.
Finally, evaluate the formula bottom-up. There are at most \(O(\ell n)\) state/subformula queries, each to an \(\mathrm{NP}\) predicate; all other work is polynomial. Thus every listed model-checking problem belongs to
\(\mathrm P^{\mathrm{NP}}=\Delta_2^{\mathrm P}\).
This proves an upper bound, not \(\Delta_2^{\mathrm P}\)-completeness.
We give a deterministic implementation of the one-step predecessor test.
For a bad cell with \(s\) rows in its slack system, enumerate the supports of the vertex certificates from Section 3. The number of candidates is at most
\(2(s+1)^{d+2}\).
Here \(s=O(L+d)\). Across all cells, the resulting affine certificate inequalities have at most
\(K\leq2r\bigl(O(L+d)+1\bigr)^{d+2}\)
distinct boundary hyperplanes.
On each face of their arrangement, all certificate signs are constant. Hence whether an allocation makes every bad cell unreachable is constant on that face.
Enumerate the arrangement faces intersecting the legal-allocation polytope. An explicit procedure inserts hyperplanes one at a time and splits each current region into its negative, zero, and positive parts, retaining exactly the feasible parts by rational linear programming. In dimension at most \(d\), an arrangement of \(K\) hyperplanes has \((K+1)^{O(d)}\) faces, including faces of lower dimension.
The coefficient bit lengths are polynomial by Section 3. Testing the faces therefore decides a one-step predecessor query in time
\(A(d,r,L)=(r+L+d+2)^{O((d+1)^2)}\).
For a fixed coalition \(x\), let \(\operatorname{Pre}_x(W)\) denote the states from which \(x\) can force a successor in \(W\). The standard finite-state iterations are
\(W_0=P,\qquad W_{i+1}=P\cap\operatorname{Pre}_x(W_i)\)
for always, and
\(W_0=R,\qquad W_{i+1}=W_i\cup\bigl(P\cap\operatorname{Pre}_x(W_i)\bigr)\)
for strong until.
Each stabilizes after at most \(n\) strict changes. At the safety fixed point, choose allocations preserving the fixed point. In the until iteration, choose allocations decreasing the iteration rank until \(R\) is reached. These choices form memoryless winning strategies. Conversely, outside the safety fixed point opponents can decrease the removal rank until leaving \(P\); outside the until fixed point they can avoid it, and hence avoid \(R\), unless \(P\) already fails. Thus the iterations are exact.
A fixed-coalition objective requires \(O(n^2)\) predecessor tests. For formation, enumerate candidates separately at each evaluation state and run this computation with each candidate held fixed. This gives the claimed bound
\(O\!\left(L+n\tau^3+\ell n^3c_\sigma A(d,r,L)\right)\).
For complete and preferred semantics, enumeration uses admissible supports, justified by their formation equivalence. There is no preferred-membership test hidden in this bound.
The two-action reduction proves hardness when \(m=2\) and the support size \(\tau\) varies. Hardness is also possible with \(\tau=2\) and varying \(m\), as follows.
Give both types mass \(1/2\). One type belongs entirely to the coalition; the other is the opponent selector. Pad the Boolean variables to a power of two \(N'\geq2\). Give the coalition type two actions per variable, and put \(\delta=1/(2N')\).
The selector chooses among these tests:
Only successful cells lead to \(g\). All pair totals can simultaneously equal \(\delta\), since \(N'\delta=1/2\). Passing all tests is exactly a satisfying Boolean assignment. The selector needs only two available actions; the coalition type has \(2N'\) actions. Taking the framework domain to be the singleton coalition type again makes empty-seed formation equivalent to the saturated coalition’s ability.
This construction has \(\tau=2\), \(m=2N'\), three states, and \(7N'+2C+2\) cells. Thus fixing either \(m\) or \(\tau\) alone does not give a general polynomial-time bound.
For the degenerate case \(m=1\), every aggregate profile is fixed by \(\mu\), regardless of the coalition. Every state consequently has a unique successor. Formation introduces no additional condition because the seed is always valid. Evaluating the transition cells and then using the finite-state temporal iterations takes \(\operatorname{poly}(L)+O(\ell n^2)\) time.
The later discrete CoalATL paper states grounded polynomial-time completeness and corrects preferred-extension membership to \(\mathrm{coNP}\)-complete. [CoalATL paper](https://journal.iberamia.org/public/ia-old/articles/641/article%20%281%29.pdf) Those facts do not transfer directly to this encoding. Here the transition cells permit SAT to be implemented through continuous choices and opponent-selected tests. Conversely, preferred membership does not increase our upper bound, because monotonicity permits admissible witnesses to be extended to preferred ones.
⟨structured verdict parsed — rendered above⟩
The output resolves the task. The hardness reductions, rational-witness argument, oracle upper bound, and deterministic running-time bound are correct under the promised transition-partition condition. I found no major or minor issues requiring repair.
The added allocation is legal for the larger coalition. Transferring exactly that additional mass into the smaller coalition’s opponent allocation preserves the aggregate profile. This construction works at every state and preserves memorylessness.
Consequently, every outcome of the larger coalition’s constructed strategy is an outcome of the original strategy. This establishes the required monotonicity for next, always, and strong until. It does not assume that the larger coalition is valid.
Positive type masses ensure that the support of \(x^E\) is exactly \(E\). If a nonseed valid coalition has support \(E\), then its saturation contains both that coalition and the seed, and remains valid at the evaluation state.
The converse is also accounted for: every enumerated saturated candidate satisfying seed containment is valid. Keeping the seed as a separate candidate handles seeds whose supports are not extensions, including the zero seed. Empty extensions cause no difficulty.
The coalition remains fixed throughout each temporal objective, as required by the task.
The finite maximal-superset argument correctly shows that every admissible set is contained in a preferred extension.
The supplied proof that a preferred extension is complete checks all possible conflicts introduced by adding a defended argument, including self-defeat. Defence of the original members is preserved when the set grows. Thus the maximality contradiction is valid.
Combining extension containment with coalition monotonicity establishes the claimed formation equivalence. The seed alternative is unchanged, and structural induction legitimately extends the equivalence to formulas with nested formation modalities.
This also justifies the later use of admissible certificates for preferred formation; no preferred-extension membership test is being assumed polynomial.
The mass calculation gives \(N\delta<1\), hence \(\rho>0\), and the masses sum to one. All quantities used are dyadic rationals with polynomial encoding length.
The selector intervals are nonempty, disjoint, and cover the feasible selector range. In particular, \(\beta_{J-1}<\rho\), so the final interval is nonempty. The half-open endpoints prevent overlap.
Within each variable interval, the three cells partition its feasible coordinate range. Within each clause interval, the two threshold cells partition all feasible profiles. The absorbing-state cells complete a valid transition encoding.
Because the opponents control the entire selector type, they can select every test. Winning therefore forces each variable coordinate to be either zero or \(\delta\). Under that restriction, the clause threshold has exactly the stated Boolean interpretation. Both directions of the satisfiability equivalence follow.
The attack-free framework has the extension properties claimed. Under every listed semantics, the full variable coalition is valid, and every valid coalition has zero selector mass and is bounded by that full coalition. Monotonicity therefore establishes the formation equivalence, including the seed alternative.
The parameters \(m=2\), \(\tau=N+1\), \(|Q|=3\), and \(r=3N+2C+2\) are correct. Explicitly encoding the zero annotation remains polynomial in the reduction size.
After unavailable coordinates are removed, the conditions on \(z\) are exactly equivalent to the existence of a legal residual opponent allocation.
The common slack construction correctly distinguishes strict feasibility from feasibility of the closed system. Finitely many satisfied strict inequalities admit a positive common slack; the cap at one does not change that fact. When there are no strict inequalities, choosing slack one gives the required equivalence.
The two unreachability cases are exhaustive:
The optimal vertex-multiplier assertion is justified by the supplied support-reduction argument. The multiplier polyhedra depend only on the cell matrix, so their vertices yield fixed affine certificate inequalities in the coalition allocation.
The use of a weak certificate inequality in the second disjunction is sound: any such dual certificate prevents positive primal slack, whether or not the closed system is feasible.
The positive-support bounds and determinant estimates give polynomial bit lengths. Selecting one satisfied certificate per bad cell produces a rational system of polynomial total description length. The second common-slack optimization then supplies a polynomial-size rational allocation. Its boundedness follows from the legal-allocation constraints.
Thus the rational-witness lemma is established, rather than merely assumed.
A guessed rational memoryless strategy has polynomial total size. Cell reachability can be checked by the stated rational linear programs, producing a finite outcome graph.
The graph represents the outcomes faithfully: opponents may choose a witnessing allocation whenever an edge is taken. The next and always checks are correct. For strong until, restricting exploration to states before the first target visit and excluding reachable cycles correctly excludes every infinite target-avoiding outcome. An initial target state is handled by stopping exploration immediately.
Certificate completeness follows from the rational-witness lemma: at each state, the replacement allocation introduces no successor outside the original successor set. Removing possible outcomes preserves each universal temporal objective.
Formation adds only a polynomially verifiable support certificate, or computation of the grounded extension. The seed branch remains available even if stable extensions do not exist or the grounded extension fails seed containment.
Bottom-up evaluation makes only polynomially many adaptive queries to these NP predicates. Therefore the claimed \(\mathrm P^{\mathrm{NP}}=\Delta_2^{\mathrm P}\) containment is valid. The output correctly refrains from claiming completeness for that class.
The certificate-support counts follow from the established support bounds. Enumerating the corresponding affine hyperplanes and their arrangement faces decides the one-step predecessor predicate, including allocations lying on boundaries.
The arrangement procedure retains strict sign information through feasibility checks. The stated face bound applies in dimension at most \(d\), including lower-dimensional faces. Polynomial coefficient bit lengths and the certificate count yield the claimed bound
\(A(d,r,L)=(r+L+d+2)^{O((d+1)^2)}\).
The safety and until iterations use the appropriate greatest- and least-fixed-point constructions. Their strategy choices are memoryless. The converse rank arguments justify exactness, rather than only sufficiency.
Enumerating formation candidates separately at each evaluation state correctly accounts for state-dependent validity while holding each candidate fixed during its objective. The resulting bound
\(O(L+n\tau^3+\ell n^3c_\sigma A(d,r,L))\)
accounts for all requested parameters.
In the two-type construction, the pair-total tests and Booleanity tests jointly force a Boolean assignment. The padded mass identity \(N'\delta=1/2\) and cell count \(7N'+2C+2\) are correct. The selector mechanism from the preceding reduction applies.
When both \(m\) and \(\tau\) are fixed, the deterministic bound is polynomial. When \(m=1\), each available-action set is necessarily a singleton, so aggregate profiles and successors are independent of the coalition. The always-valid seed then makes formation impose no additional restriction. The stated polynomial bound follows.
The cited paper supports the reported grounded polynomial-time completeness and preferred-membership correction. These are contextual comparisons, not premises used to establish the mass-model classification. [CoalATL paper, Proposition 9 and Corollary 15](https://journal.iberamia.org/public/ia-old/articles/641/article%20%281%29.pdf)
No additional clarification is needed to verify the argument.
⟨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.