Answer: \(2\mathrm{EXPTIME}\)-complete, and hence \(\mathrm{NP}\)-hard.
Theorem 3 — class: hardness
Given a finite state set \(S\), initial state \(s_0\), state labels, finite types \(T\) with rational masses \(\mu_t>0\), action sets \(A_t\), an LTL goal \(\gamma_t\) for each type, an LTL query \(\varphi\), and a rational piecewise-polyhedral transition map \(\delta(s,x)\), where \(x_{t,a}\geq 0\) and \(\sum_{a\in A_t}x_{t,a}=\mu_t\), decide whether there exists a finite-state population strategy whose induced run satisfies \(\varphi\) and is in the population core. The core excludes any deviation by a nonzero submass vector \(\nu\in[0,\mu]\) for which every type with \(\nu_t>0\) loses on the baseline run and every response by the residual population of mass \(\mu-\nu\) makes each deviating type’s goal true.
A society is given by its support: a nonempty list \(T\) of \(\tau\) types, each with positive binary-rational mass \(\mu_t\). Here \(\tau=|T|\) is the support size, not the number of possible types; total mass need not equal \(1\).
The input also contains a nonempty finite state set \(S\), initial state \(s_0\), labels \(\lambda:S\to 2^{AP}\), nonempty finite action sets \(A_t\) available at every state, and LTL formulae \(\gamma_t\) and \(\varphi\) over \(AP\).
For any nonnegative mass vector \(r\), define \(D(r)=\{x\in\mathbb R_{\geq0}^{\sum_t|A_t|}:\sum_{a\in A_t}x_{t,a}=r_t\text{ for every }t\}\). The deterministic transition map \(\delta:S\times D(\mu)\to S\) is explicitly encoded, for each state, by finitely many disjoint cells covering \(D(\mu)\), each specified by rational linear strict or weak inequalities and assigned one successor state; boundary assignments are included.
A strategy for population mass \(r\) is a deterministic finite-state transducer observing only the public state history and outputting an allocation in \(D(r)\). Its finitely many output vectors may have real coordinates, and its memory size is unrestricted. Allocations are divisible masses, not randomised actions.
A baseline strategy \(\sigma\) for mass \(\mu\) induces a unique run \(\rho_\sigma\) from \(s_0\). A type wins exactly when its LTL goal holds on that run, and strictly prefers winning to losing.
A beneficial deviation consists of a fixed vector \(\nu\in\prod_{t\in T}[0,\mu_t]\), with \(\sum_t\nu_t>0\), and a strategy \(\eta\) for mass \(\nu\), such that every type with \(\nu_t>0\) loses on \(\rho_\sigma\), while every strategy \(\theta\) for residual mass \(\mu-\nu\) yields a run satisfying all those types’ goals. These runs restart at \(s_0\), with simultaneous allocations \(y\) and \(z\) and successor \(\delta(s,y+z)\); both sides use the strategy model just defined. The population core consists of baseline strategies admitting no beneficial deviation.
Is deciding whether there exists a population-core strategy \(\sigma\) with \(\rho_\sigma\models\varphi\) solvable in polynomial time, or is it \(\mathrm{NP}\)-hard? State running times in \(m=|S|\), \(\tau\), \(k=\sum_t|A_t|\), and the total binary input length \(L\), including transition guards and LTL formulae.
The discrete existential core-verification problem is \(\mathrm{PSPACE}\)-complete for one player and \(2\mathrm{EXPTIME}\)-complete for multiple players ([source](https://arxiv.org/html/2301.06157)). No complexity result for this exact population model was located in the literature search.
The decision problem is \(2\mathrm{EXPTIME}\)-complete, and hence \(\mathrm{NP}\)-hard.
The hardness holds already with \(\tau=2\), \(k=4\), unit masses, and transition guards consisting only of single-coordinate comparisons with \(\frac12\). Thus divisible allocations and small support do not yield a polynomial-time algorithm.
The proof below applies to the stated finite-state, public-history strategy model.
For a nonempty subset \(C\subseteq T\), define \(\mu^C_t=\mu_t\) when \(t\in C\), and \(\mu^C_t=0\) otherwise. Write \(\Gamma_C=\bigwedge_{t\in C}\gamma_t\).
Call \(C\) enforceable if some strategy for mass \(\mu^C\) ensures \(\Gamma_C\) against every strategy for mass \(\mu-\mu^C\), starting at \(s_0\).
Lemma. A baseline with losing-type set \(B\subseteq T\) admits a beneficial deviation if and only if some nonempty \(C\subseteq B\) is enforceable.
Proof. An enforceable \(C\subseteq B\) immediately gives a beneficial deviation with mass vector \(\mu^C\).
Conversely, suppose \((\nu,\eta)\) is a beneficial deviation. Put \(C=\{t:\nu_t>0\}\), so \(C\subseteq B\). Define \(e=\mu^C-\nu\), which is coordinatewise nonnegative.
Choose any fixed allocation \(w\in D(e)\). Such an allocation exists because every action set is nonempty. Define the enlarged coalition strategy by adding \(w\) to every output of \(\eta\).
For any residual strategy \(\theta'\) of mass \(\mu-\mu^C\), adding \(w\) to its outputs gives a strategy \(\theta\) of mass \(\mu-\nu\). At every public history, the combined allocations agree:
\(\displaystyle (\eta+w)+\theta'=\eta+(\theta'+w).\)
Consequently, the resulting runs agree. Since \(\eta\) ensures \(\Gamma_C\) against every \(\theta\), its enlargement ensures \(\Gamma_C\) against every \(\theta'\). Adding a fixed vector preserves finite memory and finitely many output vectors. Therefore \(C\) is enforceable. ∎
In particular, whether a baseline belongs to the core depends only on its losing-type set.
We reduce from the complement of LTL realizability.
The standard realizability problem asks whether a finite-state Mealy machine can ensure an LTL specification \(\psi\) when, in each round, the environment chooses the input valuation first and the machine then chooses the output valuation. This problem is \(2\mathrm{EXPTIME}\)-complete. Since this is a deterministic complexity class, its complement is also \(2\mathrm{EXPTIME}\)-complete. See [Pnueli and Rosner, *On the synthesis of a reactive module*](https://doi.org/10.1145/75277.75293).
Let the input and output propositions, together, be \(p_1,\ldots,p_q\), ordered with all input propositions first. Unused dummy propositions can ensure that both parts are nonempty.
Create two types, called system and environment. Each has mass \(1\) and actions \(\{0,1\}\). Thus \(\tau=2\) and \(k=4\).
The states are:
Thus \(m=2q+3\).
Introduce fresh propositions \(c,b\). Label \(M\) by \(\{c\}\), label \(B\) by \(\{b\}\), label \(V_{j,1}\) by \(\{p_j\}\), and give all other states the empty label.
At \(s_0\), the system type chooses between \(B\) and \(M\). At \(M\), the first bit is selected. At \(V_{j,\ell}\), for \(j<q\), the next bit is selected. Input bits are controlled by the environment type; output bits by the system type. Both \(V_{q,0}\) and \(V_{q,1}\) return deterministically to \(M\).
Every binary choice controlled by type \(t\) uses the two cells
\(\displaystyle x_{t,1}<\frac12,\qquad x_{t,1}\geq\frac12.\)
They select bit \(0\) and bit \(1\), respectively. At \(s_0\), these select \(B\) and \(M\), respectively.
These cells are disjoint and cover the allocation domain, including the boundary. Forced transitions use a single cell covering the entire domain. Every guard has constant size, apart from state identifiers.
A play entering \(M\) therefore consists of successive blocks, each comprising \(M\), followed by one state for each of the \(q\) bits. The environment selects all current input bits before the system selects the current output bits. Each selected bit becomes publicly visible.
Put \(h=q+1\). Define a translation \(H\) recursively, using the Boolean operators, next, and until as a syntax basis:
Here \(\mathsf X^j\) means \(j\) explicitly written next operators.
For every play in the round gadget, let \(w\) be its word of combined input/output valuations, one valuation per block. At the marker of block \(i\),
\(\displaystyle \rho,ih\models H(\alpha)\quad\Longleftrightarrow\quad w,i\models\alpha,\)
where positions are counted from the first \(M\).
This follows by structural induction. For an atom, its bit is exactly \(j\) positions after the marker. Next jumps exactly one block. For until, the right operand can hold only at a marker; before that marker, the left operand is required precisely at the preceding markers, because \(\neg c\) holds at every intermediate bit state.
The translation has size \(O(q|\psi|)\).
Set
\(\displaystyle \gamma_{\mathrm{sys}}=\mathsf X(c\wedge H(\psi)),\qquad \gamma_{\mathrm{env}}=\top,\qquad \varphi=\mathsf X b.\)
Every baseline satisfying \(\varphi\) enters \(B\) immediately. Its losing-type set is exactly \(\{\mathrm{sys}\}\). Such a baseline exists: the system mass can be allocated entirely to action \(0\) initially.
By the lemma, this baseline is in the core exactly when the full system type cannot enforce \(\gamma_{\mathrm{sys}}\).
The full system type can enforce \(\gamma_{\mathrm{sys}}\) exactly when \(\psi\) is realizable:
The restriction to finite-state residual strategies causes no gap. If a fixed finite-state system strategy has a violating input word, its product with a deterministic parity automaton for the objective is a finite graph with a rejecting infinite path. Such a graph has a rejecting ultimately periodic path: retain the recurrent odd extremal priority and repeat a suitable closed walk. Its input sequence can be generated by a finite-state environment strategy.
Therefore,
\(\displaystyle \text{a core baseline satisfying }\varphi\text{ exists} \quad\Longleftrightarrow\quad \psi\text{ is unrealizable}. \)
The reduction has \(\tau=2\), \(k=4\), \(m=2q+3\), and output binary length \(O(q|\psi|+q\log(q+2))\), hence polynomial length. This proves \(2\mathrm{EXPTIME}\)-hardness.
We next prove the matching upper bound for arbitrary valid inputs.
Fix a nonempty \(C\subseteq T\). For a state \(s\) and nonempty \(R\subseteq S\), define
\(\displaystyle F_C(s,R)\quad\Longleftrightarrow\quad \exists y\in D(\mu^C)\ \forall z\in D(\mu-\mu^C): \delta(s,y+z)\in R. \)
This is a sentence of linear real arithmetic. Membership in \(R\) is expressed by the disjunction of precisely those transition cells assigned a successor in \(R\). Strict and weak inequalities are retained exactly. The sentence has at most \(2k\) scalar variables and binary length \(O(L+k)\).
These sentences are decidable in doubly exponential time in their binary length. This follows from quantifier elimination for linear real arithmetic; the Ferrante–Rackoff procedure is described and verified in [Nipkow, *Reflecting Quantifier Elimination for Linear Arithmetic*](https://www21.in.tum.de/~nipkow/pubs/mod2007.pdf).
Construct a finite turn-based arena as follows:
There is always a legal coalition choice, because \(F_C(s,S)\) holds. This arena has at most \(m2^m\) vertices and \(O(m^2 2^m)\) edges.
Lemma. The coalition can ensure \(\Gamma_C\) in this finite arena exactly when \(C\) is enforceable in the population model.
Proof. First suppose it wins in the finite arena with finite memory. For every selected pair \((s,R)\), fix a witness allocation \(y_{s,R}\) for \(F_C(s,R)\). Output that allocation in the population model. Every possible residual allocation leads to a successor in \(R\), so every resulting public run is a permitted abstract run. The strategy uses finite memory and finitely many real output vectors.
For the converse, fix an enforceable finite-state population strategy \(\eta\). At each of its memory states and public states, its output is a fixed vector \(y\). Define its exact response set
\(\displaystyle R_s(y)=\{\delta(s,y+z):z\in D(\mu-\mu^C)\}. \)
This is nonempty and satisfies \(F_C(s,R_s(y))\). Choosing these sets defines a finite-state strategy in the abstract arena.
Suppose this abstract strategy were losing. Fixing its finite memory and taking the product with a deterministic parity automaton for \(\Gamma_C\) gives a finite graph containing a rejecting ultimately periodic path.
For each transition of that path to \(s'\in R_s(y)\), select an allocation \(z\) witnessing \(\delta(s,y+z)=s'\). A residual transducer can follow this finite prefix and repeating closed walk, outputting those witness allocations.
It needs only finite memory. It observes public states and can track the fixed strategy \(\eta\)'s memory from those states; thus it can determine \(y\) without observing allocations. The resulting population run violates \(\Gamma_C\), contradicting enforceability. ∎
For an LTL formula of length \(O(L)\), standard constructions provide a deterministic parity automaton with
\(\displaystyle D=2^{2^{O(L)}}\text{ states},\qquad d=2^{O(L)}\text{ priorities}.\)
The priority bound follows by translating first to an exponentially sized nondeterministic Büchi automaton and then applying [Piterman’s determinization](https://arxiv.org/abs/0705.2205).
Consequently, coalition enforcement reduces to a finite parity game with at most \(m2^mD\) vertices. Finite parity games admit positional winning strategies and can be solved in time \(N^{O(d)}\), where \(N\) is their number of vertices. Hence enforceability can be computed for all nonempty support subsets.
Construct a directed graph on \(S\) by including \(s\to s'\) exactly when
\(\displaystyle \exists x\in D(\mu):\delta(s,x)=s'.\)
This can be computed in polynomial time in \(m,k,L\), by testing the feasibility of each transition cell.
Strict inequalities are handled exactly: replace every strict inequality in a cell by its weak version with a common positive slack, constrain that slack to be at most \(1\), and maximize it. The original cell is feasible exactly when the optimum slack is positive.
For each candidate winner set \(W\subseteq T\), define
\(\displaystyle \Psi_W= \varphi\wedge \bigwedge_{t\in W}\gamma_t\wedge \bigwedge_{t\notin W}\neg\gamma_t. \)
This formula has length \(O(L)\). Test whether the baseline graph has a path from \(s_0\) satisfying \(\Psi_W\). An exponentially sized nondeterministic Büchi automaton and a product-graph emptiness test give time
\(\displaystyle \operatorname{poly}(m,k,L)\,2^{O(L)}.\)
This test exactly captures the finite-state baseline requirement. Every baseline generates a graph path. Conversely, a successful Büchi emptiness test yields an ultimately periodic public-state path. Fixing an allocation witnessing each edge of its finite prefix and repeating closed walk produces a finite-state baseline.
Accept exactly when some \(W\) passes this path test and no nonempty enforceable \(C\subseteq T\setminus W\) exists. The full-mass lemma proves correctness.
The subset condition for all winner sets can be precomputed in \(O(\tau2^\tau)\) time by propagating enforceability flags to supersets of losing-type sets.
Let \(A=2^{2^{p(L+k)}}\) bound one linear-real-arithmetic decision, for a fixed polynomial \(p\). Choose fixed constants so that \(D=2^{2^{O(L)}}\), \(d=2^{O(L)}\), and put \(N=m2^mD\).
A deterministic running-time bound is
\(\displaystyle 2^\tau\left[ m2^m A + N^{O(d)} + \operatorname{poly}(m,k,L)\,2^{O(L)} \right]. \)
The terms account for the enforcement queries, parity games, and baseline path tests, respectively. The subset propagation cost is absorbed by this bound.
Because the input is explicit, \(m,\tau,k\leq L\), so the bound is \(2^{2^{\operatorname{poly}(L)}}\). Together with the reduction, this establishes \(2\mathrm{EXPTIME}\)-completeness for the exact population model.
⟨structured verdict parsed — rendered above⟩
The argument is correct in substance, with two minor omissions in the upper-bound presentation. The reduction establishes the requested hardness, including the restrictions \(\tau=2\) and \(k=4\). The matching upper bound is also sound, subject to explicitly specifying the temporal semantics of the abstract arena and the binary-arithmetic accounting.
No major logical gap, false central statement, or counterexample was found.
Verified.
For a beneficial deviation \((\nu,\eta)\), the set \(C=\{t:\nu_t>0\}\) is nonempty and consists entirely of losing types. The vector \(e=\mu^C-\nu\) is coordinatewise nonnegative, including outside \(C\), where both terms vanish.
The construction uses the same fixed allocation \(w\in D(e)\) on opposite sides of the comparison:
The combined allocations agree at every public history. Determinism therefore gives identical runs. Adding a fixed vector preserves the observation restriction, finite memory, and finite output range.
The converse direction also satisfies the positive-total-mass requirement: \(C\) is nonempty and every \(\mu_t\) is positive.
Thus the lemma correctly handles arbitrary partial masses; it does not assume that total mass equals one.
Verified.
The source problem is ordinary infinite-word LTL realizability with input-first, Mealy semantics. The stated completeness result applies to this model; the same formulation is documented in [*LTL Reactive Synthesis with a Few Hints*](https://dipot.ulb.ac.be/dspace/bitstream/2013/360005/3/978-3-031-30820.pdf). Complementing the source problem preserves completeness because the deterministic complexity class is closed under complement.
Adding unused input and output propositions preserves realizability and avoids empty-part edge cases.
The constructed population instance meets the task’s requirements:
Only the controlling type’s coordinate affects each binary choice. Consequently, simultaneous allocations implement the intended sequence of publicly observable bit choices.
Verified.
At a round marker, the state encoding proposition \(p_j\) occurs exactly \(j\) positions later. The atomic translation is therefore correct.
The next translation advances exactly \(h=q+1\) positions, reaching the next marker.
For until, \(c\wedge H(\beta)\) restricts the witness position to a marker. At every intermediate bit state, \(\neg c\) makes the left operand true regardless of the value of \(H(\alpha)\). At earlier markers, the left operand requires precisely \(H(\alpha)\). This matches the until semantics on the block word, including a witness at the current marker.
Negation and conjunction preserve the induction. The notation counting positions from the first marker is explicitly stated, so the initial state introduces no indexing error.
The translation inserts at most a linear number of next operators per relevant syntax occurrence and does not duplicate recursively translated subformulae. Its claimed size \(O(q|\psi|)\) is valid.
Verified.
Every baseline satisfying \(\varphi=\mathsf X b\) enters the absorbing state \(B\). On that run, the environment wins because its goal is \(\top\), while the system loses because \(c\) is false immediately after the initial state.
Hence the losing-type set is exactly the system singleton. The full-mass lemma then gives the claimed equivalence between core membership and failure of system enforceability.
The strategy correspondence is compatible with public-history observation and finite memory:
The finite-state restriction on the residual environment is addressed correctly. After fixing a finite-state system strategy, the product with a deterministic parity automaton is finite. Any violating infinite path admits a rejecting ultimately periodic witness. Such an input sequence can be generated by a finite-state environment.
The reduction therefore establishes the displayed equivalence with unrealizability. Its output-length bound is polynomial, and the claimed hardness holds with constant support and action counts.
Verified, with a minor accounting omission.
The sentence \(F_C(s,R)\) has the correct quantifier order: the coalition fixes its allocation before all possible residual allocations are considered.
The domain restrictions are essential and are present in the definition. For restricted \(y\) and \(z\), their sum belongs to \(D(\mu)\), so the transition-cell disjunction faithfully expresses membership of the successor in \(R\). Strict inequalities and boundary assignments are retained.
The variable-count and formula-length bounds are valid up to the stated asymptotic constants.
The cited [Nipkow paper](https://www21.in.tum.de/~nipkow/pubs/mod2007.pdf), particularly Sections 4.4.2 and 6.4, supports the use of Ferrante–Rackoff elimination without repeated conversion to disjunctive normal form.
Minor issue: The write-up moves directly from that elimination procedure to a bound in total binary input length without explicitly accounting for rational coefficient growth and arithmetic costs.
Minimum clarification: State that the claimed bound is a binary bit-operation bound, and provide a precise supporting reference or routine coefficient-size accounting. This does not require a new mathematical argument about the population model.
Verified, with a minor semantic omission.
The abstract arena is finite and total. Both allocation domains are nonempty even when one side has zero mass, so \(F_C(s,S)\) holds.
For the forward direction, a witness allocation for each selected pair \((s,R)\) suffices. Only finitely many witnesses are needed, and real coordinates are expressly allowed by the task.
For the reverse direction, the exact response set is nonempty and legal. After fixing the coalition’s finite memory, a rejecting abstract path can be chosen ultimately periodic in the finite product graph. Every edge on that witness path has a residual allocation witnessing it.
The residual transducer can track the fixed coalition strategy’s memory using public states. Its dependence on the fixed strategy is legitimate under the quantifier order. It need not observe the coalition’s allocation during play.
Minor issue: The expanded turn-based arena introduces intermediate vertices representing \((s,R)\), but the write-up does not explicitly define how these vertices interact with LTL evaluation.
This matters because inserting positions can change a formula containing next. For example, \(\mathsf X p\) can change truth value if an intermediate position is read before the next public state.
Minimum clarification: Specify the objective on the projected public-state sequence and state exactly when the automaton advances, including its treatment of the initial label. Also specify the parity convention and treatment of intermediate vertices. The proof already reasons about public-state runs, so this is an expositional clarification.
Verified under the preceding semantic clarification.
The coalition conjunction has length \(O(L)\).
[Piterman’s Theorem 3.10](https://arxiv.org/pdf/0705.2205) gives a deterministic parity automaton with at most \(2n^n n!\) states and \(2n\) priorities from an \(n\)-state nondeterministic Büchi automaton. With the exponential LTL-to-Büchi bound, this supports both claimed bounds:
\[ D=2^{2^{O(L)}}, \qquad d=2^{O(L)}. \]
The arena is a finite, perfect-information, turn-based game with no dead ends. These are the relevant hypotheses for positional determinacy and the stated parity-game running-time bound.
The vertex and edge estimates are valid. In particular, adding the original state vertices to all nonempty-subset vertices still gives at most \(m2^m\) vertices.
Verified.
The baseline graph contains exactly the individually feasible transitions. Transition-cell feasibility is a rational linear-programming problem.
The common-slack treatment of strict inequalities is valid because each cell contains finitely many inequalities. The procedure must interpret an infeasible slack program as an infeasible cell; this is routine.
The formula \(\Psi_W\) specifies the winner set exactly, including when either conjunction is empty. Its length remains \(O(L)\).
Büchi emptiness supplies an ultimately periodic witness whenever a satisfying graph path exists. Choosing finitely many edge-witness allocations then yields a permitted finite-state baseline. Thus the graph test captures the strategy requirement rather than merely unrestricted path existence.
Finally, rejecting a winner set exactly when its losing set contains a nonempty enforceable coalition is justified by the full-mass lemma. Superset propagation correctly computes that condition.
Verified in substance.
The displayed running-time bound accounts for all coalition queries, parity games, and winner-set path tests. Arena construction and subset propagation are absorbed by the stated terms.
Since the input explicitly lists states, supported types, and actions, their counts are bounded by its total binary length. Substitution into the displayed bound gives deterministic doubly exponential time with a polynomial exponent.
The prover therefore resolves the requested hardness question and supports the stronger completeness claim. The two identified issues require presentation clarifications, not new population-model mathematics.
⟨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.