Endogenous Energy Reactive Modules Games: Modelling Side Payments among Resource-Bounded Agents

Julian Gutierrez, David Hyland, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge · IJCAI 2024 (ijcai24-00008)

mirror found
paperEndogenous Energy Reactive Modules Games: Modelling Side Payments among Resource-Bounded Agents
authorsJulian Gutierrez, David Hyland, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge
venueIJCAI 2024
filed undercoalition · hedonic
judged bygpt-5.6-luna / xhigh (triple__luna__xhigh__c2r1)
judge confidencemedium
authors would recognise ityes

The anchor — hardness

Theorem 5

For S ∈{NASH, CORE}, CORE-S-OFFER- EXISTENCE is 2EXPTIME-c.

statement extracted from the paper’s text layer

Every anchor argued

The continuous mirror question

Given a finite type set \(\Theta\), rational masses \(\mu\), finite reactive modules, bounded integer energy levels, LTL goals \(\gamma_\theta\), and an anonymous finite public-state transition rule, decide whether there exists a feasible measurable pre-play energy-transfer kernel \(x\), respecting donor budgets and recipient capacities, and a measurable population assignment of finite-state Mealy strategies such that the induced continuum game has a stage-2 core-stable population outcome and \(x\) is stage-1 Core-stable. Stage-2 deviations are by measurable positive-mass coalitions, with complement responses as in the paper; each agent's goal is evaluated on its induced run, and the paper's no/some/all stable-continuation preference is interpreted agentwise almost everywhere.

The model it lives in

An anonymous continuum Endogenous ERMG: \(\mu\) is mass over complete role-types \(\theta\); \(x\) is a rational mass transport of bounded energy offers; the state is a measure over local Boolean states, energy levels, and finite-state strategies; public transitions use aggregate action mass; utilities are per-agent LTL goal satisfaction; stability is against positive-measure coalitions at both stages.

The objection that survived

The mirror is not the literal high-multiplicity limit: it needs an anonymous aggregate transition system, a measure over continuation strategies, and precise almost-everywhere LTL and positive-measure-core semantics; the paper's \(2\mathrm{EXPTIME}\) reductions do not establish this lift.

fatal: False

What the mirror covers

The surviving mirror covers Theorem 5's CORE–CORE-OFFER-EXISTENCE in an anonymous typed population; it leaves literal named-agent ERMGs, Theorem 4's Nash–Nash mirror, Propositions 1 and 2, Theorem 3, and other non-offer results untouched.

Open questions for a prover

The case FOR (proponent)

I think this paper admits a genuine continuous mirror, although the strongest case is deliberately narrower than “replace every agent by a fluid.” The best mirror is its endogenous energy-transfer problem in an anonymous, high-multiplicity population of resource-bounded devices.

Take a finite type set \( \Theta \). A type \( \theta \) contains the complete information relevant to the game: its reactive module, local variables, guarded commands and energy changes, initial energy \(E^0_\theta\), capacity \(e^\max_\theta\), LTL goal \( \gamma_\theta \), and its communication or transfer role. A society is a rational distribution \( \mu\in\Delta(\Theta) \), where \( \mu_\theta \) is the fraction of devices of type \( \theta \).

The intended regime is, for example, a very large fleet of interchangeable robots, battery-backed sensors, or autonomous service devices. There may be millions of devices but only a few dozen role-types: identical devices have the same action repertoire, battery bounds, temporal mission, and transfer rules. This is a genuine high-multiplicity regime, not an arbitrary relabelling of named agents.

The continuous state records the mass of each type in each local Boolean state and energy level. Agents still have discrete Boolean variables, integer energy levels, guarded commands, finite-state Mealy strategies, and LTL objectives. Only the population measure and transfers are continuous. Interaction is anonymous: local modules may observe a finite public state, while that public state is updated from the aggregate mass of devices taking each action. This is the natural population quotient of the paper’s reactive-module model for fleets or cohorts.

An offer is a mass transport of energy before play. Formally, it is a feasible nonnegative transport plan \(x\) between the continuum of agents. Each donor may offer at most its initial energy, and each individual offer respects the recipient’s capacity condition; after transfers, the recipient’s energy is updated exactly as in the paper, including the capacity cap. In a finite type representation, \(x_{\theta,\theta'}\) is the total energy mass sent from type \( \theta \) to type \( \theta' \), together with rational masses of agents ending at each possible energy level. Thus the action variable is not “give one named robot two units,” but “move this much energy mass from one cohort to another.”

My lead anchor is Theorem 5, proved in this paper:

For \(S\in\{\mathrm{NASH},\mathrm{CORE}\}\), \(\mathrm{CORE}\)-\(S\)-OFFER-EXISTENCE is \(2\mathrm{EXPTIME}\)-complete.

I would mirror its \(S=\mathrm{CORE}\) case with the following problem.

Continuum Core–Core Offer Existence. An instance consists of a finite typed anonymous ERMG, rational type masses \( \mu_\theta \), the finite local modules and energy bounds, the public aggregate transition rule, and LTL goals \( \gamma_\theta \). The question is whether there exists a feasible energy-mass transport \(x\) such that:

A stage-2 continuum strategy population is core-stable if, for every measurable coalition \(A\) whose members currently fail their goals, and every alternative strategy assignment for \(A\), the remaining population can respond so that at least one member of \(A\) still fails its goal. The offer transport is stage-1 core-stable if no measurable coalition can replace its outgoing energy transfers in a way that makes every member strictly better in the paper’s three-level offer preference, after allowing the complement to respond.

A solution is therefore a rational mass-transfer plan \(x\), together with the induced finite-state population semantics, satisfying those two nested stability conditions. This is not merely fractional energy or fractional outcomes: the continuous object is the population and the transfer of energy mass among its types.

I expect this problem to be Class B: hardness should transfer. The paper’s lower bound for Theorem 5 comes from the underlying rational-verification problem, whose combinatorics lie in LTL strategy synthesis and coalition reasoning, not in the number of individually named agents. Those constructions can be represented by a bounded collection of role-types, with each role replicated by positive mass. Continuization therefore does not remove the source of the \(2\mathrm{EXPTIME}\) hardness. The interesting gain is elsewhere: once the population is typed, one can ask new optimization questions about the transfer layer, such as minimum transferred energy mass, maximum guaranteed goal-satisfying mass, or robustness after removing an \( \varepsilon \)-fraction of a type.

The paper’s Theorem 5 is a particularly good anchor because its central object is already a redistribution of a scarce resource before strategic play. The continuum interpretation is recognizably the same question for a large population: can stable energy-sharing arrangements exist among many interchangeable resource-bounded agents?

A second, independently defensible anchor is Theorem 4, also proved here:

For \(S\in\{\mathrm{NASH},\mathrm{CORE}\}\), \(\mathrm{NASH}\)-\(S\)-OFFER-EXISTENCE is \(2\mathrm{EXPTIME}\)-complete.

For \(S=\mathrm{NASH}\), the corresponding problem is Continuum Nash–Nash Offer Existence. The input is the same typed population and feasible energy-mass offer space. The question is whether there is an offer transport \(x\) such that no individual can improve its three-level offer preference by changing its own outgoing transfer, and the resulting continuum ERMG admits a Nash-stable strategy population. A Nash-stable population means that almost every agent has no alternative finite-state strategy that changes its goal from false to true against the induced aggregate trajectory.

This also belongs naturally in Class B. The LTL synthesis component remains, and the paper’s reduction from stable-strategy nonemptiness can be lifted to replicated role-types. It is a less robust mirror than the Core–Core version because atomless Nash introduces the familiar issue that one individual has zero effect on aggregate dynamics. That is a modelling feature rather than a fatal flaw: it says that an isolated device takes the population trajectory as given, while a positive-mass coalition is the object that changes the aggregate. Still, the exact relationship between this atomless Nash notion and Nash equilibria of large finite replicas would need to be proved.

These mirrors cover the paper’s endogenous-offer results, Theorems 4 and 5. They do not claim that every ERMG instance continuizes cleanly. In particular, they use the anonymous fragment in which repeated agents share local modules and interact through aggregate public state. They do not attempt to quotient arbitrary guards that refer to the identity of every other agent or arbitrary collections of individually named Boolean variables.

That restriction is also the weakest point. The original paper is formulated for a finite set of named agents, and its strategy semantics can depend on the exact joint valuation of all their variables. Replacing that by aggregate mass changes the deviation model: an infinitesimal deviation has no macroscopic effect, while a positive-mass deviation does. The continuum core is therefore not a theorem about the literal model with \(n\) agents; it is a well-motivated anonymous population extension of it.

I think the case survives because the proposed regime is not contrived. Large fleets, sensor cohorts, and distributed energy devices really do have repeated modules, repeated goals, repeated capacities, and pre-play resource allocation. The paper’s essential questions remain intact: whether energy constraints alter the strategy space, whether transfers enable otherwise impossible equilibria, and whether those transfers are stable under Nash or coalition deviations. The continuous mirror is thus computationally meaningful even though its baseline complexity is expected to remain \(2\mathrm{EXPTIME}\)-complete.

The case AGAINST (opponent, writing after the proponent)

The paper does contain named computational results, so “there is no theorem to mirror” is not available. The problem is more fundamental: neither proposed continuum problem is actually a limit of the games in Theorems 4 and 5.

In the paper, agents are not merely typed modules. Each module has its own Boolean variables, each strategy receives the entire named valuation \( \{0,1\}^{|\Phi|} \), and guards and LTL goals may refer to other agents’ variables. Thus two agents with identical code are not interchangeable: their histories, variable names, observations, and possible deviations remain distinct. Replicating a role therefore does not produce a high-multiplicity instance of the same game. Either every copy retains those identity-sensitive interactions, in which case the type space grows with the number of copies, or the guards and observations are replaced by anonymous aggregate rules, in which case one has introduced a different population game.

This defeats the proposed Nash–Nash mirror of Theorem 4 particularly sharply. In an atomless population, one individual’s offer or action has zero mass and cannot change the aggregate state, the offer transport, or the other agents’ continuation game. Consequently, “no individual has a profitable deviation” reduces to a best-response condition against a fixed population trajectory. The strategic effect that makes the paper’s Nash problem a Nash problem has disappeared. The same issue occurs in the pre-play offer phase: changing one individual’s outgoing transfer does not change the mass transport. If a deviation instead changes a positive mass of a type, it is a coalition or type-level deviation, not the paper’s unilateral Nash deviation.

This is not repaired by taking a limit of finite clone games. With \(q\) copies, one deviation changes the aggregate by \(1/q\); at \(q=\infty\), it changes it by zero. Since the objectives are Boolean LTL properties, an \(1/q\) change can nevertheless flip the truth of a formula at every finite \(q\). There is no canonical continuous limit of these deviations. Retaining the finite effect requires an identity-sensitive or threshold-scaled semantics; discarding it produces the atomless best-response problem above.

The Core–Core proposal from Theorem 5 is less immediately degenerate, because positive-mass coalitions can affect an aggregate trajectory. But its stated formulation is not yet a defined continuous analogue. A paper outcome is a single run \( \rho(\vec{\sigma},G) \), whereas a population with identical static types may split across different Mealy strategies and histories. One must therefore specify whether \( \gamma_\theta \) is required to hold for almost every agent, for all agents of a type, for a positive mass, or for the aggregate trajectory. These choices produce different cores.

The same problem affects the paper’s three-level offer preference. In the finite game, agent \(i\) asks whether all, some, or none of the stable continuation profiles satisfy \( \gamma_i \). In a continuum, an individual is null, while a type may contain agents following several strategies. “Some” and “all” could refer to continuation equilibria, to agents within a type, or to positive mass of agents; the paper does not select among these. If all copies of a type are forced to use one strategy, the model suppresses precisely the within-type deviations that the core quantifies over. If copies may use different strategies, the state is a measure over an unbounded set of strategy machines and histories, not the finite type-and-energy distribution described by the proponent.

The energy transport itself is not the decisive obstacle. With bounded integer energy, one could expand types by energy level and encode feasible transfers by a flow. But that only solves the accounting layer. It does not determine which agents receive which continuation strategies, how their local histories are correlated with transfers, or how coalition deviations alter the aggregate game.

The strongest charitable repair would be an anonymous fleet model: local modules observe a finite public aggregate state, population mass evolves by action flows, and “core” is explicitly redefined using positive-measure coalitions. That could be an interesting mean-field rational-verification problem. It would nevertheless be a new model, with new transition semantics, new LTL satisfaction semantics, and a new large-coalition stability concept. The reductions establishing Theorems 4 and 5 do not lift merely by replicating role-types, because their games use named joint valuations and arbitrary individual strategy deviations.

So Theorem 4’s proposed mirror fails outright: atomless Nash makes the individual strategic and offer deviations vacuous. Theorem 5 can be rescued only as a substantial re-modelling into a mean-field cooperative game, not as the continuous high-multiplicity version claimed here.

That is the strongest honest negative case. I cannot prove that no anonymous fleet model would ever be worthwhile; such a model is plausible. What fails is the claim that the paper’s endogenous-offer theorems already supply a well-posed continuous mirror of the kind ChoCo studies.

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.