| paper | d4-conf-atal-2019-0386 |
| authors | — |
| venue | ? |
| filed under | unclassified |
| judged by | gpt-6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | medium |
| authors would recognise it | yes |
NP-hard→NP-hard discrete result → its continuous mirror
Answer: \(2\mathrm{EXPTIME}\)-complete, and hence \(\mathrm{NP}\)-hard. · discrete side: hardness · adjudication: proved_with_minor_gaps
full proof & adversarial review →
Theorem 3
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.
An anonymous finite-state concurrent game with type masses \(\mu_t\) and a piecewise-rational transition map over aggregate action shares. Finite-state controllers assign action shares by type; coalitions control submasses \(\nu_t\) and face all responses by the remaining masses. The core retains the paper’s universal-response condition for beneficial deviations, and E-Core asks whether a core run satisfies an LTL query.
There is no formal map showing that aggregate transitions and fractional subcoalitions preserve the E-Core deviation structure, so the proposed population core may be a new solution problem rather than a high-multiplicity relaxation of the paper’s instances.
fatal: False
The mirror covers the E-Core component of Theorem 3’s paired E-Core and A-Core completeness result. It leaves A-Core as a separate problem, core membership and deviation checking, the strong core, non-emptiness results, and the mean-payoff section.
The strongest honest positive case is the paper’s qualitative E-Core question. Theorem 3, proved in the paper, says that E-Core and A-Core are PSpace-complete for one-player games and 2ExpTime-complete for games with more than one player. E-Core asks whether some core outcome satisfies a given LTL formula; the paper proves the bounds using reductions from earlier LTL-game problems. I would anchor only on its E-Core part. [Theorem 3 in *Cooperative Concurrent Games*](https://u.cs.biu.ac.il/~krauss/data/articles/CooperationAIJ23.pdf)
A plausible regime is a large fleet of residential battery controllers sharing a finite grid-state model. There might be hundreds of thousands of devices but only a few complete types, distinguished by their control capabilities, contracts, and temporal goals. Each type’s mass is its share of the fleet. At each round, the mass of a type can split among actions such as charging, discharging, or waiting; the shared grid state changes according to the aggregate action shares. This is a population model: the mass represents how many agents take each action, not uncertainty about a finite profile.
Here is a precise mirror. Call it Population E-Core. An instance has a finite state set \(S\), initial state, state labels, a finite set of types \(T\), rational masses \(\mu_t>0\) summing to \(1\), an action menu \(A_t\) and LTL goal \(\gamma_t\) for each type, an LTL query \(\varphi\), and a transition rule \(\delta\). The rule maps a state and aggregate action masses \(x_{t,a}\), where \(x_{t,a}\geq 0\) and \(\sum_{a\in A_t}x_{t,a}=\mu_t\), to the next state. Represent \(\delta\) by a finite rational polyhedral partition of the possible aggregate action vectors, with a next state assigned to each cell.
A population strategy is a finite-state controller that assigns action shares by type after each public history. A coalition chooses mass \(\nu_t\in[0,\mu_t]\) from each type, with \(\sum_t\nu_t>0\), and coordinates that mass’s action shares. The rest of the population chooses its own shares. Their combined action masses determine the next state through \(\delta\). A coalition has a beneficial deviation from a baseline strategy if every type with \(\nu_t>0\) fails its goal on the baseline path, and every response by the remaining population makes each of those types’ goals true after the deviation. The population core consists of baseline strategies admitting no such deviation. The decision problem asks: does there exist a population strategy whose path satisfies \(\varphi\) and is in this core? A solution is a finite-state mass-allocation strategy with that property.
The expected classification is hardness transfer, at least for a two-type subfamily. Theorem 3’s 2ExpTime lower bound already comes from a two-player LTL game, so the hard part lies in strategic temporal reasoning, not in having many players. A possible embedding treats each player’s role as a large homogeneous type bloc and sends partial within-type action splits to a sink where the relevant goals fail. That could preserve the original hard instance while letting each bloc stand for a large population. The full fractional-coalition model may still add continuum-specific difficulty; I would expect at least the lower bound to transfer, but would leave an exact complexity classification to the prover.
The authors could plausibly recognize this as their rational-verification question: is a temporal property realized by a stable cooperative outcome? The co-modification from individual action tuples to aggregate action shares is required by the population model. The mirror covers only the paper’s qualitative E-Core result, not A-Core as a separate problem, the strong core, or the mean-payoff section. It also generates questions about finite-memory sufficiency, preservation of core nonemptiness, and how the high-multiplicity problem relates to the finite-agent one.
The weakest point is that the paper’s transition function is defined over named players’ joint actions, while this mirror uses anonymous mass shares and allows partial-type coalitions. Its ATL* characterization and upper bounds therefore do not carry over automatically. That is a real semantic change. The positive case survives because the proposed problem still asks about the paper’s central object—stable cooperative behavior—and places it in a credible large-population regime with few complete agent types.
Theorem 3 gives a real anchor: E-Core asks whether some outcome in the core satisfies an LTL property, and the paper proves its complexity. The difficulty for a continuous mirror is that this is a result about a game with named players. Its transition function can depend arbitrarily on the full tuple of their actions, and its core tests coalitions of those players against all strategies of the remaining players. The paper does not describe a population by type masses or by aggregate behavior.
That matters when defining types. Two players with the same action menu and goal need not be interchangeable: the transition function may treat their action coordinates differently. To group them honestly, a type must include their role in the transition system as well as their preferences and actions. For arbitrary games in the paper, that can leave essentially one type per player, so increasing the population does not produce a compact distribution over types. A useful high-multiplicity regime would have to restrict attention to games with substantial symmetry.
The proposed battery-controller model is the strongest repair. It gives a credible population and an explicit aggregate transition rule, and fractional coalitions can sensibly choose action shares. But that rule adds a new semantic layer: the environment responds to distributions of actions, and coalitions and counter-responses are distributions too. The paper’s ATL* characterization is over discrete action tuples; it supplies no dictionary from its E-Core instances to these anonymous population games. The resulting question may be good, but it is not clearly the high-multiplicity version of the paper’s E-Core problem in the way the ChoCo programme seeks.
The proposed hardness embedding exposes the choice. If intermediate action shares are sent to a sink so that only pure shares matter, the aggregate model mostly encodes the original finite game and the continuum does little work. If intermediate shares have substantive effects, the mirror’s dynamics and deviation semantics depend on new population assumptions. That is a reason to doubt the connection to this paper, not a claim about what the continuous problem’s complexity or answer would be.
I cannot make the universal negative case airtight. Large anonymous fleets are plausible, and the authors might recognize population E-Core as a natural extension of rational verification. The case against rests on the missing bridge from their identity-sensitive transition model to an aggregate population model; it is weakest precisely for applications whose systems are anonymous by design.
The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.