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

1 Introduction

The paradigm of rational verification is an important approach to verifying the possible behaviours of multi-agent systems [Gutierrez et al., 2017; Abate et al., 2021; Gutierrez et al., 2023b]. Rational verification draws inspiration from the well-known formal verification paradigm of model checking, which is concerned with automatically checking whether or not a given system satisfies certain properties, expressed as formulae of temporal logic [Baier and Katoen, 2008]. Rational verification differs frommodel checking in that it assumes that system components (agents) are rational actors, making choices in pursuit of their personal goals, and taking into account the strategic behaviours of other agents - goals are typically captured by associating with each agent a temporal logic formula that it desires to see satisfied. Since agents are assumed to be rational, game theory provides a natural framework through which to understand collective rational action: a classic decision problem in RV involves asking whether a given temporal logic property holds on some run of the system that arises by agents choosing strategies that constitute (for example) a Nash equilibrium [Abate et al., 2021].

Many variations of rational verification have now been studied [Gutierrez et al., 2018; Gutierrez et al., 2023b; Bruy`ere et al., 2022; Brice et al., 2023]. In this work, we introduce a variation of the problem in which agents act under energy resource bounds. Specifically, we assume agents are given some initial energy endowment, and subsequently, all actions that the agent performs are assumed to affect this endowment. Actions may generate energy (leading to an increase in the endowment) or consume energy (reducing the endowment). Crucially, agents can only perform actions for which they have sufficient energy. Note that energy plays a secondary role in agents' preferences: agents are concerned with achieving their goal, and energy affects preferences only indirectly (by affecting the actions they can perform).

To capture this setting, we introduce a variation of Reactive Modules Games (RMGs) [Gutierrez et al., 2017]. In our new variation, individual agent actions (specified via guarded commands) are associated with an energy value, which may either increase or decrease the agent's energy endowment. We begin our study by showing that this framework, while providing a very natural platform through which to model resource-bounded multi-agent systems, can in fact be reduced to "classic" RMGs, and as a consequence, the key non-cooperative and cooperative decision problems in rational verification for our new setting are no harder than in the "classic" setting.

We then study an extension of our model called Endogenous ERMGs, in which agents may transfer energy to other agents. Such offers change the possible actions that agents may perform, and hence may change the underlying strategic structure of the game: for example, it may make sense for me to "donate" energy to another agent so that it will choose actions that are of benefit to me. This leads to a two-stage game, with a pre-play "offer" phase. Such an exchange may facilitate equilibria that are impossible to achieve without such an exchange. We study the decision problem of whether a stable outcome and offer profile exists under both the Nash equilibrium and Core solution concepts, again showing that the complexities of the associated problems for both solution concepts in Endogenous ERMGs are also 2EXPTIME-c.

2 Preliminaries

We use classical propositional logic, defined over a finite and non-empty set Φ of Boolean variables. Each variable in Φ may take the values of truth ⊤ or falsity ⊥, which we represent with the binary values 1 and 0, respectively. Our language includes the classical propositional logic connectives ¬ ("not"), ∨ ("or"), ∧ ("and"), → ("implies"), and ↔ ("iff"). A valuation ⃗v ∈ {0, 1}|Φ| over Φ is a binary string representing an assignment of truth values to all variables in Φ. We say that a valuation ⃗v satisfies a propositional formula φ defined over Φ, written ⃗v |= φ, if φ is true under ⃗v. Where ⃗x = (x1, . . . , xn) is an n-tuple and A ⊆ {1, . . . , n}, we write ⃗xA = (xi)i∈A to denote the |A|-tuple consisting of the elements in ⃗x that are indexed by those in A. Similarly, we write ⃗x-A = (xi)i∈{1,...,n}\A to denote the tuple of elements in ⃗x which are not indexed by elements in A. Finally, where ⃗x and ⃗y are two disjoint tuples, we write (⃗x, ⃗y) for the tuple formed by merging ⃗x and ⃗y.

Linear Temporal Logic (LTL). We make extensive use of the standard framework of Linear Temporal Logic (LTL), which is an extension of propositional logic with tensed modal operators for expressing properties of infinite linear sequences of states [Pnueli, 1977]. Specifically, in addition to the usual stock of classical connectives as above, LTL includes the unary operators "X" (next), "F" (sometime), and "G" (always), and the binary "until" operator, "U". Given a set of variables Φ, let LTL(Φ) be the set of LTL formulae over Φ; where the variable set Φ is clear from the context, we simply write LTL. LTL formulae are interpreted with respect to infinite sequences of valuations, which we refer to as runs, typically denoted ρ, ρ′ , etc. Where ρ = ⃗v0⃗v1⃗v2 . . . is a run, and t ∈ N is a temporal index into ρ, we write (ρ, t) |= φ to mean that φ ∈ LTL is true at time t ∈ N on run ρ. Additionally, we use the notation ρ[t] to denote the valuation ⃗vt in ρ at time point t ∈ N. We write ρ |= φ as a shorthand for (ρ, 0) |= φ, in which case we say that ρ satisfies φ. The size of an LTL formula φ, written |φ|, is given by the number of subformulae in φ. We refer to the reader to [Emerson, 1990; Baier and Katoen, 2008] for full details on the syntax and semantics of LTL.

SimpleReactiveModules. We use an extension of the Simple Reactive Modules Language (SRML) [van der Hoek et al., 2006] to model agents, which we refer to as modules. An SRML module consists of:

1. An interface, which defines the module's name and the Boolean variables under the control of the module; and
2. Two sets of guarded commands, which define the choices available to the module at every state.

Interfaces are specified by the syntax module mi controls Φi, where mi is the name of the module and Φi ⊆ Φ is the set of variables under its exclusive control. Guarded commands consist of two parts: a precondition for executing the command, known as the guard, and the actual command, which specifies how the value of (some of) the variables under the module's control are updated when the command is executed.

In the extension of SRML we work with in this paper, we augment guarded commands with an additional energy value, which specifies how the module i's energy level at time t, denoted Et i , is changed if the command is executed. A positive energy value will increase available energy at time t + 1; a negative value will decrease available energy. Given this, the general form of a guarded command in our augmented SRML is of the form [energy] guard ⇝ command where energy is the associated energy cost/gain. More formally, a guarded command g for a module mi controlling Boolean variables Φi ⊆ Φ is an expression:

where e ∈ Z, φ and each ψj is a propositional logic formula over Φ, and every x′j represents the value of the variable xj ∈ Φj after the command is executed. The value of any variable in Φi that does not appear in a guarded command g is unchanged by the execution of g. We also require that x′a ̸= x′b for all a ̸= b ∈ {1, . . . , k}, i.e., no variable's value is reassigned twice in the same guarded command. For a guarded command g = [e] φ ⇝ x′1 :- ψ1; · · · ; x′k :- ψk, η(g) = e represents the change in energy level associated with g, guard(g) = φ represents the guard of g, and evl(g) = x′1 :- ψ1; · · · ; x′k :- ψk represents the command of g. For an agent i with energy level Ei and a valuation ⃗v, we say that a guarded command gi for i is enabled if both -Ei ≤ η(gi) and ⃗v |= guard(gi) and we write enablei(⃗v, Ei) for the set of all guarded commands gi which are enabled for i under ⃗v.

For example, the guarded command [-2] (p ∨ q) ⇝ p′ :- ⊥; q′ :- ⊤ for a module mi can be read as "if p or q are true and i has at least two units of energy, then one of the actions available to mi is to set p to ⊥ and q to ⊤, which incurs an energy cost of 2 units for mi."

There are two kinds of guarded commands for a module: those used to initialise the variables under the module's control, and those used to subsequently update the variables. These are represented as sets of guarded commands init and update, respectively.

To ensure that agents always have a well-defined action available, we assume that in each agent's init set, at least one initial guarded command has a non-negative energy value. We also equip every module with a skip guarded command as part of its update set, which is always available and does nothing to the variables under its control. This can be explicitly written as [eskip i ] ⊤ ⇝ ∅, where eskip i ∈ N (including 0) and we use ∅ to denote a command which does nothing to the variables under the module's control. We require that the energy cost for the skip command be nonnegative to ensure that at least one command is always available to every agent, which entails that runs are always wellspecified.

Formally, an SRML module, mi is given by a triple

• Φi ⊆ Φ is the set of variables controlled by mi;
• initi is a finite set of initialisation guarded commands for mi; and
• updatei is a finite set of update guarded commands for mi .

An SRML arena is then simply a collection of agents, their representative modules, and the specification of each agent's initial and maximum energy values:

where:

• N = {1, . . . , n} is a finite, non-empty set of agents;
• Φ = ⋃i∈N Φi is a finite, non-empty set of propositional variables, where the sets Φi are all pairwise disjoint;
• mi = (Φi, initi, updatei) is an SRML module over Φ that defines the choices available to agent i ∈ N;
• emax i ∈ N is the maximum energy capacity of agent i 1 ; and
• E0 i ∈ {0, . . . , emax i } is the initial energy level of i.

Figure 1: A Reactive Module

An agent module mi for an agent i is defined by augmenting the set of original variables Φi under their control with a set of command variables, which are used to identify precisely which action the agent took at each point in time. Given this, the agent module for i takes the following general form as in Figure 1:

(i) for any set Ψ ⊆ Φ of Boolean variables and a Boolean literal v ∈ {⊤,⊥}, Ψ :- v denotes the assignment where all variables in Ψ are set to v; (ii) for any ordered set Ψ = {p1, . . . , pm} ⊆ Φ of Boolean variables and a binary string B = b1b2 . . . bm, Ψ′ :- B denotes the assignment p′1 :- b1; p′2 :- b2; . . . ; p′m :- bm. Finally, for a given energy level Ei of an agent i, we let initi|E and updatei|E denote the set of initial and update guarded commands for i respectively whose corresponding energy values are at least -E:

These sets will be useful in identifying the set of guarded commands that are available to an agent, given their current energy level at any point in a run.

3 Energy Reactive Modules Games

With these definitions in place, we can define the model for concurrent games that we focus on in this study. Formally, an Energy Reactive Modules Game (ERMG) is a structure

1 We assume that each agent is equipped with a device that has a finite capacity for storing energy.

where A is an SRML arena and γi is the LTL goal of agent i ∈ N. At the beginning of a game, each agent i ∈ N selects an initial guarded command g0 i ∈ initi|E0 i . The energy level of each agent i at timestep 1 is then updated as E1 i = min(E0 i + η(g0 i ), emax i ) and the initial valuation ⃗v0 of the variables in Φ is set according to the commands chosen, i.e., evl(g0 i ). 2 Then, at every step t ∈ Z+ of the execution, each agent i selects an enabled update guarded command gt i ∈ updatei|Et i to execute, which updates the values of the variables in Φi according to evl(gt i ) and updates the agent's energy level from Et i to Et+1 i = min(Et i + η(gt i ), emax i ). This update gives rise to a new valuation ⃗vt, and then the next round proceeds in the same manner. This process repeats indefinitely, giving rise to a run, which in an ERMG is an infinite sequence of valuations ρ = ⃗v0⃗v1 . . . where for all t ∈ N, we have that ⃗vt+1 is obtained from the execution of enabled guarded commands by all agents i ∈ N. Note that given the restrictions on allowable actions at each time point, each agent's energy level will always be a non-negative integer throughout any run.

A particular class of games which can be represented using ERMGs are regular RMGs, which are exactly the same as ERMGs, except that no energy values are involved. Regular RMGs can thus be specified by an arena A = (N, Φ, (mi)i∈N ) and LTL goals (γi)i∈N . Key decision problems in rational verification under the Nash equilibrium solution concept for regular RMGs have been well-studied in prior work [Gutierrez et al., 2017].

We model strategies as deterministic Mealy machines, which are known to be sufficient for optimality in our setting [Gutierrez et al., 2017]. A strategy for a player i ∈ N with associated module mi = (Φi, initi, updatei) is a Mealy machine (i.e., a finite state machine with output) σi = (Qi, q0 i , δi, τi), where Qi is a finite set of machine states, q0 i is the initial state, and for all q ∈ Qi, ⃗v ∈ {0, 1}|Φ| , we have:

• δi : Qi × {0, 1}Φ → Qi is the strategy's deterministic state update function such that δi(q,⃗v) ̸= q0 i , i.e., the initial state is never revisited;
• τi(q,⃗v) ∈ enablei(⃗v,Ei) is the output function that specifies which enabled guarded command is selected by player i with energy level Ei, such that τi(q, ⃗v) ∈ initi iff q = q0 i , i.e., initial guarded commands are only selected at the started of the game;

For each player i ∈ N, we let Σi represent their set of possible strategies and write Σ = ∏i∈N Σi represent the set of all strategy profiles, i.e., tuples of strategies for each player. Since we consider deterministic strategies in this setting, a strategy profile ⃗σ deterministically generates a run ρ(⃗σ, G) in an ERMG G, which consists of the infinite sequence of valuations generated by the execution of enabled guarded commands by modules at each time step.

Given this, we are now in a position to define preferences and utility functions over runs in ERMGs. We assume that a player i ∈ N has the sole objective of satisfying their LTL

2 It is also possible to consider settings with unbounded energy capacities, but this is not physically realistic and is likely to lead to undecidable verification problems [Bulling and Farwer, 2010].

goal γi. Given this, we say that player i ∈ N prefers the run ρ over ρ′ , written ρ ⪰i ρ′ , if and only if ρ′ |= γi implies that ρ |= γi. This can be extended to the strict preference relation ≻i and the indifference relation ∼i in the usual manner (see [Maschler et al., 2013]). Finally, since strategy profiles give rise to fixed runs in an ERMG, we can write ⃗σ ⪰i ⃗σ′ as a shorthand for ρ(⃗σ, G) ⪰i ρ(⃗σ′ , G). Notice that energy does not feature in the definition of preferences: agents are only secondarily concerned about energy consumption, in the sense that it places restrictions on the choices they can make.

Finally, we can define the first solution concept considered in this study. A strategy profile ⃗σ is a Nash equilibrium (or Nash-stable strategy profile) of an ERMG G if for all players i ∈ N and all alternative strategies σ′i ∈ Σi, it holds that ⃗σ ⪰i (⃗σ-i, σ′i ). We let NE(G) denote the set of Nash Equilibria of an ERMG G and for an LTL formula φ, let NEφ(G) = {⃗σ ∈ NE(G) : ρ(⃗σ, G) |= φ}.

Example 1. Consider a scenario involving two robots, B1 and B2, and three locations: middle (M), left (L), and right (R). From each location, each robot can either stay in the same position by choosing the skip command or move to another location. From M, each robot can move to either L or R. However, from L or R, they can only return to M. A move from one location to another can only be initiated when both robots are at the same location. Initially, both robots are positioned at M. For B1, the cost of each move is -1. For B2, moving left costs -1 but moving right costs -2. B1 (resp. B2) is assigned to service L (resp. R) at least once. However, for the service to be carried out, both robots must be at the same location. After completing the service and returning to M, B1 and B2 receive an energy recharge equal to the amount they have spent. For example, if B1 and B2 both visit R and then return to M, B1 gains 1 unit of energy while B2 gains 2 units. For i ∈ {1, 2}, Bi is represented by the following module.

Each robot controls two variables li and ri. If these variables are set to true, it indicates that the robot moves to the left or right. Let E0Bi = emax B1 = 1,E0B2 = emax B2 = 2. Bi's goal is given by γBi = F si. A graphical representation of the game is shown in Fig. 2. Consider a strategy profile which gives rise to the initial sequence {}, {l1, l2}, {}, {r1, r2}. This is a Nash equilibrium (NE), as the run satisfies γB1 ∧ γB2 , and the robots have enough energy to execute this strategy profile. Now, consider the sequence of assignments {}, {l1, l2}, {}, {r1}. Although the robots also have enough energy to execute this run, it is not a NE. This is because B2 can choose to set r2 to true on the fourth round and achieve its goal.

4 Rational Verification

Before exploring mechanisms for agents to make energy transfers, we will briefly recapitulate the central questions of interest in rational verification, which are concerned with verifying whether a given temporal logic property holds in some or all rational outcomes of a multiplayer game. The crucial assumption here is that agents are rational and self-interested; that is, we can rule out executions of the game which are not stable with respect to deviations by individuals or coalitions of players.

4.1 Non-cooperative Games

The main non-cooperative rational verification problems we will deal with are as follows:

Given: Game G, strategy profile ⃗σ. NASH-MEMBERSHIP: Is it true that ⃗σ ∈ NE(G)?

Given: Game G, LTL goal φ.

E-NASH: Is it true that NEφ(G) ̸= ∅?

A-NASH: Is it true that NEφ(G) = NE(G)?

Using a polynomial time transformation from ERMGs into regular RMGs, we can establish that these rational verification problems are no harder than their counterparts in regular RMGs. Thus, we have the following results:

Proposition 1. NASH-MEMBERSHIP for ERMGs is PSPACE-c, while E-NASH and A-NASH for ERMGs are 2EXPTIME-c.

4.2 Cooperative Games

A central assumption in non-cooperative game theory is that agents act independently. In cooperative games, however, we assume that agents are able to form binding agreements with others - that is, agents can form coalitions, which may deviate from an outcome if it is mutually beneficial to do so. Here, we consider the well-known α-core, which was introduced in [Aumann, 1961], and remains a foundational solution concept in cooperative game theory. This solution concept assumes that any non-deviating players may respond to a coalitional deviation by trying to 'block' it, i.e., prevent the deviators from universally improving their utility.

Under this assumption, a strategy profile ⃗σ is said to be core-stable in G if for all coalitions C ⊆ N such that ρ(⃗σ, G) |= ∧i∈C ¬γi and partial strategy profiles ⃗σ′C = (σ′i )i∈C, there exists a response by the remaining players

⃗σ′-C = (σ′i )i∈N\C such that for some player i ∈ C, it holds that ρ((⃗σ′C , ⃗σ′-C ), G) ̸|= γi. We let CORE(G) denote the set of core-stable strategy profiles in G and define COREφ(G) = {⃗σ ∈ CORE(G) : ρ(⃗σ, G) |= φ}. In the same manner, as with the Nash equilibrium solution concept, we can now define the cooperative rational verification problems as follows:

Given: Game G, LTL goal φ.

E-CORE: Is it the case that COREφ(G) ̸= ∅?

A-CORE: Does it hold COREφ(G) = CORE(G)?

Example 2. To illustrate the difference between NE and the core, let us revisit Example 1. Consider a strategy profile where both robots remain at location M forever. This strategy profile is a NE (albeit a suboptimal one), as there is no unilateral deviation by Bi that satisfies γBi : any change in Bi's strategy would result in the game transitioning to state t. However, this strategy profile is not in the core, as the (grand) coalition {B1, B2} has a strategy profile that ensures the satisfaction of γB1 ∧ γB2 . In fact, all strategy profiles in the core satisfy γB1 ∧ γB2 . As a result, an A-NASH query with φ = γB1 ∧ γB2 would return a negative answer, while an A-CORE query would return a positive one.

Because no results exist for cooperative rational verification in the context of regular RMGs, we solve these problems by reductions to and from concurrent game structures, for which these problems have been studied [Gutierrez et al., 2023a]. Thus, we establish here the first results for cooperative rational verification in the RMGs model as well as in our extension to settings with bounded resources.

Proposition 2. E-CORE and A-CORE for ERMGs and regular RMGs are 2EXPTIME-c.

5 Endogenous ERMGs

We now turn to the primary focus of our study, which is to understand how energy offers can be strategically utilised by agents to achieve better outcomes in a stable manner. To this end, we first present a framework for modelling negotiations by introducing a pre-play offer phase, in which the agents can offer resource transfers to other agents before the game begins. Crucially, we maintain that such offers should be stable with respect to deviations by (coalitions of) players in the same way that strategies in the ensuing ERMGs are.

Formally, an offer by agent i is a function

The first condition states that the total amount of energy an agent offers to other agents does not exceed their initial endowment, and the second condition states that offers must be made within the capacity constraints of their recipients. An offer thus specifies how much energy agent i proposes to transfer to each other agent in the game in the pre-play negotiation phase. Denote by Ωi the set of all valid initial offers for an agent i ∈ N. Then, an offer profile ⃗ω = (ω1, . . . , ωn) is simply a tuple of offers for each agent i ∈ N, and we write

Ω = ∏i∈N Ωi for the set of all offer profiles. We write ⃗ω0 for the empty offer profile in which no players offer any energy to any other player.

Given this, an Endogenous Energy Reactive Modules Game (EERMG) proceeds in the following manner:

Stage 1: Each agent i ∈ N chooses a valid offer ωi, giving rise to an offer profile ⃗ω.

Stage 2: Each agent chooses a strategy σi in the ERMG G⃗ω = (A′ , γ1, . . . , γn), where A′ is exactly the same as A, except that for each i ∈ N, we update i's initial energy as E0′ i =min(E0 i -totoffi+∑j̸=i ωj (i), emax i ), for each agent i to reflect the resource transfer offers made in ⃗ω. The game G⃗ω is then played according to the strategy profile ⃗σ = (σi)i∈N .

Given this two-stage game, the notion of a stable outcome can be ambiguous. This is because agents make two types of decisions, the former affecting the latter. Here, we will assume that when agents reason about offer profiles, they consider the stable outcomes induced by such offers. We use the classical Nash equilibrium and core stability notions for each stage separately. This means that we require both the energy offers to be stable against the appropriate kind of deviations and the strategy profile in the resulting stage 2 game to be stable to deviations. Given that we consider both unilateral and coalitional deviations, this approach allows us to combine the different solution concepts in different ways for each stage. Specifically, this gives rise to four possible combinations: Nash-Nash, Nash-Core, Core-Nash, and Core-Core. This decoupling between stability concepts for the first and second stages of the game allows one greater flexibility in finding a suitable model for the situation that they are trying to capture, because agents may have differing capabilities for communicating with one another and coordinating their behaviours in different stages of a game.

5.1 Stable Offers

To define a notion of stability over offer profiles, we require a way for the agents to rank such offers in terms of preferability. However, this is difficult to specify precisely, because different offer profiles can induce different sets of stable strategy profiles in stage 2 of the game. Since we do not make assumptions about how the agents resolve the equilibrium selection problem, we propose a minimal preference relation ≻Si for each agent i ∈ N over offer profiles that we should expect such agents to have. This relation is defined based on whether (i) A stable stage 2 outcome exists, (ii) A stable stage 2 outcome exists which satisfies i's goal, and (iii) All (and at least one) stable stage 2 outcomes satisfy i's goal. More concretely, for an agent i ∈ N and a stability concept S ∈ {NASH, CORE}, let ∅Si :- {⃗ω ∈ Ω | Sγi (G⃗ω ) = ∅}, ∃Si :- {⃗ω ∈ Ω | S(G⃗ω ) ̸= Sγi (G⃗ω ) ̸= ∅}, and ∀Si :- {⃗ω ∈ Ω | S(G⃗ω ) = Sγi (G⃗ω ) ̸= ∅}.

Given any offer profiles ⃗ω1 ∈ ∅Si , ⃗ω2 ∈ ∃Si , and ⃗ω3 ∈ ∀Si , we define ≻Si such that ⃗ω3 ≻Si ⃗ω2 ≻Si ⃗ω1. Moreover, for any two offer profiles ⃗ω, ⃗ω′ in the same set (∅Si , ∃Si , or ∀Si ), we assume that i is indifferent between the two offer profiles, i.e., ⃗ω ∼Si ⃗ω′ . This preference relation captures the intuition that an agent should (i) prefer an offer profile in which it is possible for their goal to be achieved in some stable outcome over one in which it is not possible to do so, and (ii) prefer an offer profile in which their goal is guaranteed to be achieved in any stable outcome over one in which it is merely possible.

With this, we can define Nash equilibrium in the usual way. An offer profile ⃗ω is Nash-S-stable for the stage 1 negotiation phase if for all agents i ∈ N and all alternative offers ω′i ∈ Ωi, it holds that ⃗ω ⪰Si (⃗ω-i, ω′i ). For the case of core stability, the definition is not as immediate. The reason for this is that once a coalition C ⊆ N deviates by making alternative offers, we assume that the remaining players N \ C have the opportunity to respond and block the deviation from being profitable for all of the deviating players. In the context of offer profiles, however, a deviation can change the set of offers the remaining players can respond with. In this study, we will assume that a response takes into account the new offers made by the deviating players. However, we will also assume that for both the deviating and responding players, the option of withdrawing all previously made offers and re-allocating the withdrawn offers is always available. Given this, we will say that an offer profile ⃗ω is Core-Sstable for stage 1 if for all coalitions C ⊆ N and alternative partial offer profiles ⃗ω′A = (ω′i )i∈A, there is some response ⃗ω′-A = (ω′i )i∈N\A such that for some i ∈ N, it holds that ⃗ω ⪰Si (⃗ω′A, ⃗ω′-A).

Example 3. Consider the following modification of Example 1. Let E0B1 = E0B2 = 0 and for i ∈ {1, 2}, γBi = Fsi ∧ ∧2j=0 G(sj → X¬sj), i.e., both B1 and B2 also do not want to stay in the same location twice in a row. We then introduce two additional robots B3 and B4 with E0B3 = emax B3 = 2,E0B4 = emax B4 = 1. Unlike the other robots, these additional robots are immobile and can only transfer their energy to others. Suppose that their goals are defined as γB3 = Xs1, γB4 = Xs2 ∨ Xt. Consider the offer profile in which B3 offers B1 and B2 1 unit each, and B4 offers B2 1 unit of energy. This profile is CORE-CORE-stable, as any possible offer deviation by B3 does not result in γB3 being satisfied in all strategy profiles in the core of the second stage game (e.g., if B3 withdraws the offer to B2, B4 can counter by also withdrawing its offer). On the other hand, in this scenario, there is no NASH-CORE-stable offer profile, since any valid offer profile will eventually enter a cycle of deviations.

Example 3 illustrates that stable offer profiles may not exist in EERMGs. This example suggests that some games are inherently unstable during the first stage. Therefore, the stability of the negotiation phase becomes a critical issue to address. In the following sections, we examine some decision problems related to this and provide several algorithms for solving them. We demonstrate that solving such problems is no harder than standard rational verification.

5.2 Decision Problems

Now, we turn to the central question in this study, which is to determine whether a stable offer profile exists in a given EERMG. To this end, we introduce the following decision problems:

Given: Game G, agent i ∈ N, offer profiles ⃗ω1, ⃗ω2, solution concept S for stage 2.

S-OFFER-PREFERENCE: Is it true that ⃗ω1 ⪰Si ⃗ω2?

Given: Game G, solution concept S1 for stage 1, solution concept S2 for stage 2.

S1 -S2 -OFFER-EXISTENCE: Does there exist an S1 -S2 -stable offer profile ⃗ω in G?

It is worth noting that, in general, an EERMG is not guaranteed to have a NASH-S- or CORE-S-stable offer profile, since the preference relations ≻Si implicitly group offer profiles into more than two categories, thus allowing "deviation cycles" to exist.

Turning to S-OFFER-PREFERENCE, for the upper-bound, we employ an algorithm that simply runs a stable profile check over the give offer profiles. For the lower bound, we reduce the problem of deciding whether an S-stable strategy profile exists in a regular RMG, hereafter called the S-NONEMPTINESS problem.

Theorem 3. For S ∈ {NASH, CORE}, S-OFFERPREFERENCE is 2EXPTIME-c.

Using this result, we can settle the complexity of the remaining problems. We show that they are also 2EXPTIME-c, and hence, reasoning about the existence of stable offers with desirable properties is no harder than the underlying rational verification problems. The upper bound for the NASHS-OFFER EXISTENCE problem is established by checking, for every agent, whether there is no beneficial deviation from the given strategy profile, which can be done by employing a suitable variant of LTL synthesis. The lower bound again uses a reduction from the S-NON-EMPTINESS problem.

Theorem 4. For S ∈ {NASH, CORE}, NASH-S-OFFEREXISTENCE is 2EXPTIME-c.

Finally, we turn to the cooperative setting and study the existence of core-stable offer profiles. Here, we establish the upper bound with a reasoning similar to the one for NashS-Offer-Existence, and reduce from S-NON-EMPTINESS to obtain the lower bound. 3

Theorem 5. For S ∈ {NASH, CORE}, CORE-S-OFFEREXISTENCE is 2EXPTIME-c.

6 RelatedWork

Endogenous games and side-payments: Jackson and Wilkie discuss the stability of transfers in their seminal work on endogenous games [Jackson and Wilkie, 2005]. In their work, transfers are dependent on the outcome of the resulting game and thus allow agents to make conditional offers to each other. In the context of infinite games, however, energy values may constrain the set of strategies that are available to players in an ERMG, so transfers should be made before the game begins to be of use to the agents. This motivates the consideration of unconditional energy transfers in the setting we study. One could also extend our model to settings involving dynamic energy transfers, where each agent can transfer energy to other agents at every round of the game. We leave this as an open problem for future investigation.

3 Note that although we reduce from the same decision problem in these three cases, the constructions required in each case are very distinct, due to the differences in the considered solution concepts as well as the fact that the S1 -S2 -OFFER-EXISTENCE problems require one to consider the set of all possible offer profiles.

Much work has been done on exploring pre-play negotiations and side payments in the context of strategic form games [Clercq et al., 2016; Goranko and Turrini, 2016; Goranko, 2022; Renou, 2009; Turrini, 2016]. Of these, our work aligns most closely with the study conducted by Turrini (2016) [Turrini, 2016]. These studies consider one-shot strategic-form or Boolean games as their focus. In contrast, RMGs are played for an infinite number of rounds, which allows agents' goals to be modelled using expressive logics like LTL. Furthermore, unlike the mentioned approaches, energy transfers in our model do not directly influence the utility functions of the recipient players. Instead, these transfers serve only to improve an agent's capability to achieve their goal. Thus, our study offers a different perspective and a complementary framework for examining resource transfers that primarily aid in goal achievement without being intrinsically valued or optimised by the agents.

Resource-bounded games and logics: Resource-bounded games have attracted considerable attention and have been explored in various contexts. Energy games [Chakrabarti et al., 2003; Bouyer et al., 2008] and their subsequent extensions are typically played in a two-player, turn-based, zero-sum setting. In energy parity games [Chatterjee and Doyen, 2012], the objective of Player 1 is to satisfy a qualitative parity condition while maintaining a positive energy level. This aligns closely with our model here, as LTL formulae can always be translated into parity conditions [Piterman, 2007]. However, the game graphs in [Chatterjee and Doyen, 2012] are singly-weighted, preventing a direct reduction of our games to theirs. Energy games with reachability [H´elou¨et et al., 2022] and ω-regular objectives [Amram et al., 2021] are also studied in the literature, but again focus only on two-player games. Energy games played on multi-weighted graphs are considered in [Velner et al., 2015; Kupferman and Halevy, 2022], but these settings only consider a quantitative condition, i.e., the players' energy levels. The work [Maubert et al., 2019] is also relevant, studying the existence of winning strategies for a team of agents to achieve some LTL formula in one form of concurrent game structures. This is very similar to the notion of a beneficial deviation in the cooperative setting we consider, but we focus on the existence of strategy profiles which are stable against deviations.

Many logics have been developed for reasoning about resource-bounded games (see [Alechina and Logan, 2020] for an extensive overview of such logics). For instance, pe-ATL [Della Monica and Murano, 2018] is an extension of the logic ATL, which can be used to reason about energy parity games involving multiple agents. Alechina et al. introduced RB-ATL [Alechina et al., 2010; Nguyen et al., 2018], another extension which assumed that resources could only be consumed and not replenished. This was then expanded by RB ± ATL(*) [Alechina et al., 2017; Alechina et al., 2018], allowing for both resource consumption and production. Pertaining to our work, note that while (RB ± )ATL* can encode statements about the core, it cannot express statements regarding the existence of Nash equilibria.

Rational Verification: Our work builds upon the existing literature on rational verification and synthesis [Fisman et al., 2010; Wooldridge et al., 2016; Kupferman et al., 2016; Almagor et al., 2018]. While many studies have used RMGs as the model for rational verification (e.g., [Gutierrez et al., 2017; Gutierrez et al., 2018; Najib, 2019; Steeples et al., 2021]), few have addressed resource-boundedness. Electric Boolean games [Harrenstein et al., 2015; Oualhadj and Troquard, 2016] consider resource-bounded games like our approach. While these models study resource redistributions, they operate under the assumption that a central authority exists that is capable of redistributing energy endowments. In contrast, the key novel aspect of our model is that we assume agents are independent and can choose their redistributions, giving rise to strategic considerations regarding transfers.

7 Conclusion

We have introduced ERMGs, a model of concurrent games with resource-constrained players using the reactive modules framework, and settled the complexity of both the key cooperative and non-cooperative rational verification questions for this model, showing that they are no harder than for regular RMGs. This therefore expands the range of practical applications which can be succinctly modelled using the reactive modules framework to analyse situations related to bounded resources, with almost no additional complexity cost. We then introduced Endogenous ERMGs, which include a preplay phase that allows players to make energy offers to one another, along with a notion of preferences over offer profiles. This preference relation enables us to study the stability of offers in both cooperative and non-cooperative settings. We then settled the problem of deciding whether a stable offer profile exists in a given game under all combinations of stability concepts, which remains 2EXPTIME-c. This initial study of the Endogenous ERMG model thus sheds light on the strategic considerations an agent faces when their actions in one stage of a game may affect the possible rational outcomes in the second stage of the game.

One natural extension of our work is to study how a topdown incentive designer [Gutierrez et al., 2019; Hyland et al., 2023] could modify the energy levels of agents to shape the set of resulting stable outcomes. Relatedly, one could take an approach akin to parameterised resource-bounded ATL [Alechina et al., 2018; Alechina et al., 2020], which can express formulae about the minimal amount of energy a coalition needs to achieve a particular goal, by asking whether energy subsidies or taxes can be introduced to enable specific outcomes. Finally, a direct next step would be to study whether some or all stable offer profiles induce games with (un)desirable properties. This becomes especially pertinent when considering the presence of malicious agents who might collude by exchanging energies to bring about an undesirable outcome. These results on the existence of stable offer profiles lay the groundwork for these future developments.

Acknowledgments

This research has been supported by the PNRR MUR project PE0000013-FAIR. Perelli was partially supported also by MUR under the PRIN 2020 projects PINPOINT and Sapienza University of Rome under the "Progetti Grandi di Ateneo" programme, grant RG123188B3F7414A (ASGARD - Autonomous and Self-Governing Agent-Based Rule Design). Wooldridge was supported by the UKRI under a Turing AI World Leading Research Fellowship (EP/W002949/1). Gutierrez was supported by the DARPA Assured Neuro Symbolic Learning and Reasoning (ANSR) program under award number FA8750-23-2-1016. The authors would like to extend special thanks to Paul Harrenstein for valuable feedback on an early draft of this paper.