On the Boundary of (Un)decidability: Decidable Model-Checking for a Fragment of Resource Agent Logic

1 Introduction

There exist several formalisms that extend Alternating Time Temporal Logic (ATL), [Alur et al., 2002] with reasoning about resources available to agents and production and consumption of resources by actions, see, for example, [Bulling and Farwer, 2010; Alechina et al., 2010; Della Monica et al., 2013; Alechina et al., 2014; Bulling and Goranko, 2013]. When the production of resources is allowed, the modelchecking problem for many of these logics is undecidable [Bulling and Farwer, 2010; Bulling and Goranko, 2013]. Recently, however, it was shown that some resource logics with production of resources have a decidable model checking problem [Alechina et al., 2014]. In this paper, we investigate the reasons for decidability or undecidability of the modelchecking problem for resource logics. There is a quite bewildering variety of choices for the syntax and semantics of resource logics, for example, the precise definition of when a joint action is 'affordable' by a coalition of agents (can the agents pool their resources, and can they use resources produced by the joint action to offset the costs involved in the action). Many of these choices do not affect the decidability or otherwise of the model-checking problem. In particular, the decidability result of [Alechina et al., 2014] was proven in the presence of two major restrictions called, using the notion of [Bulling and Farwer, 2010], resource flat and proponent restricted. The former assumes that agents are always re-equipped with fresh resources when they reconsider their strategies; the latter assumes that only the proponents act under resource bounds. In addition to these restrictions, another choice in the semantics seems to be relevant for decidability. This choice, which is also related to the finitary and infinitary semantics of [Bulling and Farwer, 2010], stipulates whether in every model, agents always have a choice of doing nothing (executing an idle action) that produces and consumes no resources [Alechina et al., 2014]. Apart from the technical convenience for model-checking (intuitively it implies that any strategy to satisfy a next or until formula only needs to ensure the relevant subformula becomes true after finitely many steps, and after that the agents can always choose the idle action which does not increase the 'cost' of the strategy), this choice is motivated in [Alechina et al., 2010] by the properties of the logic, e.g., coalition monotonicity.

∗Acknowledgements: This work was supported by the Engineering and Physical Sciences Research Council [grant EP/K033905/1].

In this paper, we investigate the effects of various semantic choices such as idle on the decidability of the model-checking problem. First we show that the resource-flat as well as the proponent-restricted fragment of resource agent logic remain undecidable in the presence of idle actions. We then identify and motivate a significant, non resource-flat fragment that has a decidable model checking property in the presence of idle actions, and is not decidable otherwise. It follows that idle actions can make a difference for the decidability of model checking with respect to the semantics considered in this paper.

The paper is organised as follows. In Section 2 we introduce our version of resource agent logic, its models and the semantics. Afterwards, we put our setting in context with existing work, discussing the main differences and the main (un)decidability results. Based on this comparison we review results shedding light into different semantic choices. We give our first technical undecidability results and identify a new, non resource-flat fragment of resource agent logic. Section 4 presents our second technical result: a decidability result for the newly identified fragment. We conclude in Section 5.

2 Resource Agent Logic

In this section we define the logic resource agent logic RAL and resource-bounded models. We essentially follow [Bulling and Farwer, 2010], combined with aspects from [Alechina et al., 2014]. We point out the similarities and differences in more detail in Section 3.1.

Syntax. The logic is defined over a set of agents Agt, a set of resources types Res and a set of propositional symbols Π.

An endowment (function) η : Agt ×Res → N∞0 is used to assign resources to agents; ηa(r) = η(a, r) is the number of resources agent a has of resource type r. With En we denote the set of all possible endowments. Resource types can represent, for example, money, fuel, and battery power. Special minimal and maximal endowment functions are denoted by ¯0 and ¯∞, respectively. The former expresses that there are no resources at all, whereas the latter equips all agents with an infinite amounts of resources. The logic RAL is defined according to the grammar of ATL [Alur et al., 2002] where two types of cooperation modalities are available, the meaning of which is explained below. RAL-formulae are defined by:

where p ∈ Π is a proposition, A, B ⊆ Agt are sets of agents, and η is an endowment. We also define 〈〈A〉〉↓ and 〈〈A〉〉η as abbreviations for 〈〈A〉〉↓A and 〈〈A〉〉ηA, respectively. The operators X, U, and G denote the standard temporal operators expressing that some property holds in the next point in time, until some other property holds, and now and always in the future, respectively. Both types of cooperation modality, 〈〈A〉〉↓B and 〈〈A〉〉ηB , assume that all agents in A∪B consume and produce resources. The reading of 〈〈A〉〉ηB ϕ is that agents A have a strategy compatible with the endowment η to enforce ϕ. The formula 〈〈A〉〉↓B ϕ reads similarly but the strategy must be compatible with the resources currently available to the agents. In both cases compatible means that the strategy can be executed given the agents' resources. For both modalities it is necessary to keep track of resource production and consumption during the execution of a strategy. The evaluation of a modality 〈〈A〉〉ηB , however, (re-)equips all agents with a fresh amount of resources: the current resource endowment is overwritten by endowment η.

Semantics. We define the models of RAL as in [Bulling and Farwer, 2010]. Following [Alechina et al., 2014] we also define a special case of these models in which agents have an idle action in their repertoire which neither consumes nor produces resources.

Definition 1 (RBM, iRBM). A resource-bounded model (RBM) is given by M = (Agt,Q,Π, π,Act, d, o,Res, t) where Agt = {1, . . . , k} is a set of agents; π : Q → ℘Π is a valuation of propositions; Act is a finite set of actions; and the function d : Agt × Q → ℘Act\{∅} indicates the actions available to agent a ∈ Agt in state q ∈ Q. We write da(q) instead of d(a, q), and use d(q) to denote the set d1(q) × . . . × dk(q) of action profiles in state q. Similarly, dA(q) denotes the action tuples available to A in q. o is a serial transition function which maps each state q ∈ Q and action profile α = 〈σ1, . . . , σk〉 ∈ d(q) (specifying a move for each agent) to another state q′ = o(q, α). Finally, the function t : Act ×Res → Z models the resources consumed and produced by actions. We define prod(σ, r) := max{0, t(σ, r)} (resp. cons(σ, r) := min{0, t(σ, r)}) as the amount of resource r produced (resp. consumed) by action σ. For α = 〈σ, . . . , σk〉, we use αA to denote the sub-tuple consisting of the actions of agents A ⊆ Agt.

An RBM with idle actions, iRBM for short, is an RBM

M such that for all agents a, all states q, and all resource types r in M, there is an action σ ∈ da(q) with t(σ, r) = 0. We refer to this action (or to one of them if there is more than one) as the idle action of a and denote it by idle.

A path λ ∈ Qω is an infinite sequence of states such that there is a transition between two adjacent states. A resourceextended path λ ∈ (Q × En)ω is an infinite sequence over Q × En such that the restriction to states (the first component), denoted by λ|Q, is a path in the underlying model. The projection of λ to the second component of each element in the sequence is denoted by λ|En. We define λ[i] to be the i + 1-th state of λ, and λ[i,∞] to be the suffix λ[i]λ[i + 1] . . .. A strategy for a coalition A ⊆ Agt is a function sA : Q+ → ActA such that sA(λq) ∈ dA(q) for λq ∈ Q+. Such a strategy gives rise to a set of (resourceextended) paths that can emerge if agents follow their strategies. A (η, sA,B)-path is a resource-extended path λ such that for all i = 0, 1, . . . with λ[i] := (qi, ηi ) there is an action profile α ∈ d(λ|Q[i]) such that: (1) η0 = η (η describes the initial resource distribution), (2) sA(λ|Q[0, i]) = αA (A follow their strategy), (3) λ|Q[i + 1] = o(λ|Q[i], α) (transition according to α), (4) for all a ∈ A ∪ B and r ∈ Res: ηia (r) ≥ cons(αa, r) (each agent has enough resources to perform its action), (5) for all a ∈ A ∪ B and r ∈ Res: ηi+1 a (r) = ηia (r) +prod(αa, r) - cons(αa, r) (resources are updated). (6) for all a ∈ Agt \ (A ∪ B) and r ∈ Res: ηi+1 a (r) = ηia (r) (resources remain unchanged for agents not in A ∪ B). The (η,B)-outcome of a strategy sA in q, out(q, η, sA,B), is defined as the set of all (η, sA,B)-paths starting in q. Truth is defined over an RBM M, a state q ∈ QM, and an endowment η. The semantics is given by the satisfaction relation |= where the cases for propositions, negation and conjunction are standard and omitted:

M, q, η |= 〈〈A〉〉ζB ϕ iff there is a strategy sA for A such that for all λ ∈ out(q, ζ, sA, B), M, λ, ζ |= ϕ

M, q, η |= ϕUψ iff there exists i with i ≥ 0 and M, λ|Q[i], λ|En[i] |= ϕ and for all j with 0 ≤ j < i M, λ|Q[j], λ|En[j] |= ψ

The model checking problem is stated as follows: does M, q, η |= ϕ hold? When the context is clear, we simply write q, η |= ϕ; if ϕ is only a propositional formula, we might also ignore η.

Observe that the standard ATL modalities 〈〈A〉〉 can be defined as 〈〈A〉〉 ¯∞ Agt , so the logic is a proper extension of ATL.

Remark 1. We refer to the semantics introduced above as infinitary semantics. In [Bulling and Farwer, 2010] the main semantics also allows for finite (maximal) paths. We refer to that semantics as finitary semantics. We note that both semantics coincide over iRBMs, as is is always possible to extend a path due to the idle actions.

Syntactic fragments. Following [Bulling and Farwer, 2010] we define two fragments of the logic. The resourceflat fragment, rfRAL, only allows cooperation modalities of type 〈〈A〉〉ηB : agents are always (re-)equipped with a fresh set of resources whenever they re-consider their strategies. The proponent restricted fragment, prRAL, only allows cooperation modalities of types 〈〈A〉〉↓ and 〈〈A〉〉η : only the proponents are assumed to make use of resources. The fragment combining both restrictions is denoted by rfprRAL.

3 The Quest for Decidability

We first discuss differences and similarities to the original resource agent logics. We present the main idea underlying the undecidability of model-checking results from [Bulling and Farwer, 2010] and investigate the reasons for the (un)decidability. We present new undecidability results, and motivate a new fragment of RAL.

3.1 Two Related Logics

The logic presented here is based on the resource bounded logics of [Bulling and Farwer, 2010] and [Alechina et al., 2014]. The authors of the former paper introduce a very general framework. Several interesting special cases are identified, and the (un)decidability of their model checking problems investigated. In the interests of readability, we refer to the setting of [Bulling and Farwer, 2010] by S1 and to that of [Alechina et al., 2014] by S2. The language of RAL is almost identical to the setting of S1, except that we do not allow the release operator. Essentially, S2 corresponds to the resource-flat and proponent-restricted fragment of RAL. RBMs serve as models of S1, where S2 uses iRBMs. There are negligible differences in how the production and consumption of resources are handled. In S2 both are considered at the same time; here, actions first consume resources and afterwards produce them. However this is just a modelling issue. Most results of S1 are given in terms of the finitary semantics (cf. Remark 1). Finally, in S1 agents belonging to the same group-either to the proponents or the opponents-are allowed to share their resources, whereas in our setting each agent has its own resource balance. This change does not affect the (un)decidability results given here, but eases the presentation.

3.2 Investigating the Boundary of (Un)Decidability

In [Bulling and Farwer, 2010] it was shown that manyactually most-fragments of their resource agent logic are undecidable. However, an interesting case remained open: the resource-flat, proponent-restricted fragment. Just recently, this open problem has been shown to be decidable in [Alechina et al., 2014; Alechina et al., 2015]:

Observation 1. rfprRAL is decidable over iRBMs.

A natural question arises: Could we extend the decidability to more expressive fragments? We first show that proponent restrictedness is essential for decidability, including over iRBMs.

The Non-Proponent Restricted Fragment

In [Bulling and Farwer, 2010] it was shown that model checking formulae of type 〈〈1〉〉¯0 Agt Fhalt is undecidable over RBMs. However the decidability of this fragment was open over iRBMs. In Theorem 1, we show that undecidability continues to hold. Before we sketch the proof we present the basic idea underlying the reductions of [Bulling and Farwer, 2010].

The undecidability of the model checking problems is shown by reducing the halting problem for two counter machines (also called Minsky machines) [Hopcroft and Ullman, 1979]. A two-counter machine is essentially a pushdown automaton with two stacks. The stacks are represented as two counters over natural numbers. Each of the two counters (1 and 2) can be incremented, decremented (if non-zero), and tested for zero. The behaviour of such an automaton is specified by a transition relation (s, E1, E2)∆(s′ , C1, C2) with the following meaning: a transition from automaton state s to s′ is enabled if counter i ∈ {1, 2} satisfies condition Ei ∈ {zero, non-zero} (with the obvious meaning). If the transition is taken the automaton changes its control state from s to s′ , and counter i is updated by adding Ci ∈ {-1, 0,+1}. It is said that the automaton halts on empty input iff the halting state of the automaton is reached by subsequently taking enabled transitions. The main idea of the reduction of the halting problem is to encode the transition table of the automaton as an RBM. The two counters are simulated by two resource types. The model consists of two agents: the simulator agent 1 and the spoiler agent 2. Agent 1 is supposed to select transitions of the automaton where agent 2 is used to ensure that only enabled transitions are selected by agent 1. The basic modelling of a single transitions (s,E1,E2)∆(s′ ,C1,C2) is shown in Figure 1. The first action (E1,E2) of agent 1 is used to (partially) check whether a transition of the automaton is enabled. That is, if Ei = non-empty, agent 1 must have a resource of type i to execute the action. If such an action is taken, the system enters a "test state" sE1E2 . The purpose of the test state is to check whether a transition with Ei = empy is only selected by agent 1 if counter i is indeed zero, i.e. ensures a correct simulation. Note that, in general, nothing prevents agent 1 from executing such an action if it has resources available, although it should only be executed if no resources are available. Essentially, the problem is that it is not possible to directly test for zero in the model. 1 The workaround proposed in [Bulling and Farwer, 2010] is to use the spoiler agent 2 to perform the "zero test". The idea is that in test state sE1E2 , agent 2 must not be able to reach the fail state qe. Reaching the fail state is only possible if resources are available when there should not be any. This is encoded by action tE1 E2 in themodel. For example, if counter 1 should be empty, E1 = empty, the action tE1 E2 can only be executed if resources of type 1 are available. However, this also requires that agent 2 correctly mirrors agent 1's resource balance, i.e. 2 also simulates the counter values. This is achieved by making the model turn-based. Once agent 1 has executed an action (s′ ,C1,C2) an intermediate state is introduced in which agent 2 has a single choice with the same effect on the resources as agent 1's previous action (dotted rectangle in Fig. 1). Based on this encoding it is shown (using the finitary semantics) that the automaton A halts on the empty input if, and only if, M(A), qinit, ¯0 |= 〈〈{1}〉〉¯0 {1 ,2 } F halt where M(A) is the RBM constructed from A. The state corresponding to the automaton's accepting state is labelled halt. In order for the reduction to work over iRBMs the main difficulty is the correct mirroring of 1's resources by agent 2 in the presence of idle actions. The modified encoding of a transition (s,E1,E2)∆(s′ ,C1,C2) is illustrated in Figure 2.

1 Testing for zero is a delicate property, the satisfaction of which seems crucial for the undecidability of other formalisms, such as Petri nets [Peterson, 1981].

Theorem 1. Model checking rfRAL over the class of iRBMs is undecidable, even for two agents and formulae of type 〈〈1〉〉¯0 {1 ,2 } Fp.

Proof sketch. We argue that the automaton A halts on the empty input iff M(A), qinit, ¯0 |= 〈〈1〉〉¯0 {1,2} Fhalt, where M is the encoding of the automaton following the idea shown in Figure 2. First, we observe that the execution of an idle action by agent 1 would immediately falsify the formula, as state qe would be reached. Similarly, if agent 2 does idle and agent 1 does not, the formula will be true. As we are looking for a winning strategy of 1 against all strategies of 2 we can neglect the cases where any of the agents performs the idle action. Again, the encoding describes the modelling of a transition (s,E1,E2)∆(s′ ,C1,C2). In this modelling the simulation of agent 1's resources by agent 2 is made explicit. In states sC′1C′2 j , agent 2 can only perform the same action (apart from the idle action) as the one selected by agent 1 in state sE1E2 with the same resource consumption and production. We briefly sketch the correctness of the reduction. (i)

A halts. Then, agent 1 simulates the transitions of the automaton's accepting run. Agent 2 will never be able to reach the fail state qe. Moreover, either agent 2's resources correctly simulate 1's resources, or agent 2 does the idle action. In both cases either the halting state or the auxiliary halting state qi, both labelled halt, are reached. The formula is true. (ii) Let the formula be true. Agent 1 must have a strategy that guarantees reaching a state labelled halt against all strategies of 2, including 2's strategy in which 2 never performs the idle action. This strategy of 2 correctly mirrors 1's resources and ensures that 1's strategy only selects enabled transitions. Thus, the strategy of 1 encodes an accepting run of the automaton.

The Proponent Restricted Fragment

Theorem 1 shows that the restriction of resource-flatness is not enough to obtain a decidable model checking property. We turn to the proponent-restricted fragment. Below we show, by adopting the undecidability proof of [Bulling and Farwer, 2010] for prRAL to work over iRBM's, that prRAL is also undecidable over iRBMs. This is a negative result; however, in contrast to Theorem 1, the formula used in the reduction is more complex, and leaves room for restricting the temporal structure of the language. Indeed, this is the motivation for the decidable fragment of prRAL that we introduce in Section 3.3.

Corollary 1 (of [Bulling and Farwer, 2010]). Model checking prRAL over the class of iRBMs is undecidable even in the case of a single agent.

Proof sketch. The undecidability proof for prRAL over RBMs of [Bulling and Farwer, 2010] essentially follows the encoding shown in Figure 1. The difference is that the second agent is removed (as well as the dotted box, implementing the resource mirroring behaviour), and agent 1 itself is used to perform the "zero test". This requires a slightly more sophisticated formula: the automaton A halts on the empty input if, and only if, M(A), qinit, ¯0 |= 〈〈{1}〉〉¯0 ((¬〈〈{1}〉〉↓Xfail)Uhalt). The main idea is that in test state sE1E2 , agent 1 must not be able to reach the fail state qe, which is expressed by ¬〈〈{1}〉〉↓X fail. Now, in order to extend the reduction to work over iRBMs, we add reflexive loops (dashed in the figure) which represent agent 1's idle actions. It is easy to see that the reduction still works. The agent would not be able to reach the halting state (labelled halt) if it had taken an idle loop forever, nor would it help the agent, in its role as opponent, to reach the fail state.

3.3 ADecidable Fragment of RAL

Following the observation made in the previous section, we define a proponent-restricted but not resource-flat fragment of RAL that has a decidable model checking property. Let us first introduce the positive fragment of RAL as the set of all RAL-formulae where no cooperation modality is under the scope of a negation symbol, and let the U-restricted fragment of RAL restrict the use of the until operator U such that the formulae ϕ1 on the left-hand-side of ϕ1Uϕ2 is purely propositional.

Definition 2 (The fragment prRAL r ). The logic prRAL r is defined as the proponent-restricted, positive and U-restricted fragment of RAL.

The prRAL r -fragment allows us to express properties of coalitions of agents which re-consider their strategies without being re-equiped with fresh resources. An example of a property expressible in prRAL r (but not in a resourceflat fragment) is, for example, "given their initial battery charge, rescue robots A can safely get to a position from which they can perform rescue while in visual contact with the base". Formally, this can be specified by the formula 〈〈A〉〉ηinit (safeU(〈〈A〉〉↓ (visualUrescue))). Intuitively, this reflects the constraint that the robots cannot recharge their batteries after reaching the position where they can perform rescue while in visual contact with the base. Another example is given by the formula 〈〈1, 2〉〉ηinit F(rob ∧ 〈〈1〉〉↓F escape) expressing that the coalition {1, 2} can cooperate to eventually rob a bank and then agent 1 can ensure to escape on its own using only its remaining resources.

Before we show the decidability of prRAL r over iRBMs in the next section, we make the following observation which follows from [Bulling and Farwer, 2010, Theorem 6]:

Observation 2. Model checking prRAL r over RBMs is undecidable.

4 Model-checking prRAL r

In this section we introduce a model-checking algorithm for prRAL r and prove its correctness. In what follows, we assume that the function atl(φ) that returns the formula where each 〈〈A〉〉↓ and 〈〈A〉〉ζ in φ is replaced by 〈〈A〉〉.

Theorem 2. The model-checking problem for prRAL r over iRBMs is decidable.

To prove decidability, we give an algorithm which requires as input M, q, η, φ and returns true or false. We prove termination and correctness of the algorithm in Lemmas 1 and 2 below. Given φ, we produce a set of subformulas of φ, Sub(φ), in the usual way, except that 〈〈A〉〉↓ and 〈〈A〉〉ζ modalities are replaced by standard ATL modalities 〈〈A〉〉. Sub(φ) is ordered in increasing order of complexity. Note that if a state s is not annotated with the standard ATL modality 〈〈A〉〉, then it cannot satisfy 〈〈A〉〉↓ or 〈〈A〉〉ζ . Algorithm 1 simply labels the subformulas of φ using the standard ATL labelling algorithm [Alur et al., 2002]. It then calls the function STRATEGY to label states with φ. (Note that we do not label states with subformulas of φ involving 〈〈A〉〉↓ or 〈〈A〉〉ζ modalities as in [Alechina et al., 2014].)

Algorithm 1 Labelling φ

procedure LABEL(M, φ, η) for φ′ ∈ Sub(φ) do [φ′ ]M ← { q | q ∈ Q∧ ATL-LABEL(M, φ′ )} [φ]M ← { q | q ∈ Q ∧ STRATEGY(node0(q, η), φ)}

STRATEGY proceeds by depth-first and-or search, processing each coalition modality in turn starting from the outermost modality. Each temporal operator is handled by a

Algorithm 2 Strategy

function STRATEGY(n, φ) case φ is propositional return s(n) |= φ case φ = ψ1 ∧ ψ2 return STRATEGY(node0(s(n), e(n)), ψ1) ∧ STRATEGY(node0(s(n), e(n)), ψ2) case φ = ψ1 ∨ ψ2 return STRATEGY(node0(s(n), e(n)), ψ1) ∨ STRATEGY(node0(s(n), e(n)), ψ2) case φ = 〈〈A〉〉↓Xψ return X-STRATEGY(node0(s(n), e(n)), φ) case φ = 〈〈A〉〉ζ Xψ return X-STRATEGY(node0(s(n), ζ), φ) case φ = 〈〈A〉〉↓ψ1Uψ2 return U-STRATEGY(node0(s(n), e(n)), φ) case φ = 〈〈A〉〉ζ ψ1Uψ2 return U-STRATEGY(node0(s(n), ζ), φ) case φ = 〈〈A〉〉↓Gφ return G-STRATEGY(node0(s(n), e(n)), φ) case φ = 〈〈A〉〉ζ Gφ return G-STRATEGY(node0(s(n), ζ), φ)

separate function: X-STRATEGY for Xψ, U-STRATEGY for ψ1Uψ2, and G-STRATEGY for Gψ. We record information about the state of the search in a search tree of nodes. A node is a structure which consists of a state of M, the resources available to the agents A in that state (if any), and a finite path of nodes leading to this node from the root node. Edges in the tree correspond to joint actions by all agents. Note that the resources available to the agents in a state on a path constrain the edges from the corresponding node to be those actions α where for all proponent agents a, cons(α) is less than or equal to the available resources of agent a. We compare vectors of resources in a usual way, for example ζa ≥ cons(αa) stands for ζa(r) ≥ cons(αa, r) for all resources r. For an action tuple σ by A ⊆ Agt, we write cons(σ) to refer to the tuple (cons(σa))a∈A. For each node n in the tree, we have a function s(n) which returns its state, p(n) which returns the nodes on the path and e(n) which returns the resource availability for all agents as a result of following p(n). The function node0(s, η) returns the root node, i.e., a node n0 such that s(n0) = s, p(n0) = [ ] and e(n0) = η. The function node(n, s′ , α, A, ∗) where A ⊆ Agt is the current set of proponents and ∗ ∈ {↓, ζ} returns a node n′ where s(n′ ) = s′ , p(n′ ) = [p(n) · n] and

X-STRATEGY for 〈〈A〉〉↓Xψ and 〈〈A〉〉ζ Xψ formulas is shown in Algorithm 3 and is straightforward. After checking if the search should be terminated with false, we simply check if there is an action by A that is possible given current endowment, and where in all outcome states A has a strategy for ψ. G-STRATEGY for 〈〈A〉〉↓Gφ and 〈〈A〉〉ζ Gφ formulas is shown

Algorithm 3 X strategy (both types of modalities)

function X-STRATEGY(n, 〈〈A〉〉∗Xψ) if s(n) ̸|= atl (〈〈A〉〉∗Xψ) then return false ActA ← {σ ∈ dA(s(n)) | cons(σ) ≤ eA(n)} for σ ∈ ActA do Act = {α ∈ d(s(n)) | αA = σ} strat ← true for α ∈ Act do s′ ← out (s(n), α) strat ← strat ∧ STRATEGY(node(n, s′ , α, A, ∗), ψ) if strat then return true return false

in Algorithm 5. Again we check if the search should be terminated with false, either because the standard ATL modality doesn't hold, or because the current path terminates in a resource consuming cycle, or if the current endowment results in φ being false. We then check the path for productive loops, and update the endowment if we find one. arb denotes an arbitrary finite value that can be decremented, i.e., where arb - k < arb (unlike for infinity). e(n)(a, r) = arb indicates that the path p(n) terminates in a 'productive loop', which can be traversed multiple times to generate an arbitrary amount of resource r for agent a. 2 If the current path terminates in a nondecreasing loop, we return true. Otherwise we continue the search for a nondecreasing loop. U-STRATEGY for 〈〈A〉〉↓ψ1Uψ2 and 〈〈A〉〉ζ ψ1Uψ2 formulas is shown in Algorithm 4, and is similar to G-STRATEGY. First U-STRATEGY checks whether false should be returned because the ATL version of the formula is false, or the current path has an unproductive loop. We then check the path for productive loops, and update the endowment if we find one. If the ATL version of ψ2 is true, we try to find a strategy to enforce ψ2), and if we are successful U-STRATEGY returns true. Otherwise the search continues, because the node where STRATEGY(n, ψ2) returns true may be found later on the path. Note that if all resources are updated to arb and a repeated call to STRATEGY(n, ψ2) returns false, the algorithm will return false because of the first check for unproductive loops.

Lemma 1. Algorithm 2 terminates.

Proof. (sketch). The proof is by induction on the length of the formula. Calls for propositional formulas clearly terminate. For the inductive step, we need to show that a call for any connective terminates provided calls for lower complexity formulas terminate. Conjunction and disjunction are obvious. X-STRATEGY makes a recursive call to a STRATEGY of a smaller complexity formula after one step. For U-STRATEGY and G-STRATEGY, the recursion calls are infinite iff endowments (considered as a vector of size |Agt|×|Res|) are never comparable. However, it can be shown that they are always

2 In what follows, we denote by arbA : A × Res → {∞, arb} an arb or infinite endowment for agents in A ⊆ Agt.

Algorithm 4 U strategy

function U-STRATEGY(n, 〈〈A〉〉∗ψ1Uψ2) if s(n) ̸|= atl (〈〈A〉〉∗ψ1Uψ2) then return false if ∃n′ ∈ p(n) : s(n′ ) = s(n) ∧ eA(n′ ) ≥ eA(n)) then return false for (a, r) ∈ {a ∈ A, r ∈ Res | ∃n′ ∈ p(n) : s(n′ ) = s(n) ∧ eA(n′ ) ≤ eA(n) ∧ e(n′ )(a, r) < e(n)(a, r)} do e(n)(a, r) ← arb if s(n) |= atl(ψ2) then strat ← STRATEGY(n, ψ2) if strat then return true elseActA ← {σ ∈ dA(s(n)) | cons(σ) ≤ eA(n)} for σ ∈ ActA do Act = {α ∈ d(s(n)) | αA = σ} strat ← true for α ∈ Act do s′ ← out (s(n), α) strat ← strat ∧ U-STRATEGY(node(n, s′ , α, A, ∗), 〈〈A〉〉∗ψ1Uψ2) if strat then return true return false

Algorithm 5 G strategy

function G-STRATEGY(n, 〈〈A〉〉∗Gψ) if s(n) ̸|= 〈〈A〉〉∗Gψ then return false if ∃n′ ∈ p(n) : s(n′ ) = s(n)∧(∀r : er(n′ ) ≥ er(n)) ∧ (∃j : ej(n′ ) > ej(n)) or ¬STRATEGY(n, ψ) then return false for (a, r) ∈ {a ∈ A, r ∈ Res | ∃n′ ∈ p(n) : s(n′ ) = s(n) ∧ eA(n′ ) ≤ eA(n) ∧ e(n′ )(a, r) < e(n)(a, r)} do e(n)(a, r) ← arb if ∃n′ ∈ p(n) : s(n′ ) = s(n) ∧ eA(n′ ) ≤ eA(n)) then return true ActA ← {σ ∈ dA(s(n)) | cons(σ) ≤ eA(n)} for σ ∈ ActA do Act = {α ∈ d(s(n)) | αA = σ} strat ← true for α ∈ Act do s′ ← out (s(n), α) strat ← strat ∧ G-STRATEGY(node(n, s′ , α, A, ∗), 〈〈A〉〉∗Gψ) if strat then return true return false

going to become comparable after finitely many steps, using the technique in [Alechina et al., 2014] or [Reisig, 1985, p.70].

Lemma 2. Algorithm 2 is correct, that is, STRATEGY(n, φ) returns true iff s(n), e(n) |= φ.

Proof. (sketch). The proof is by induction on the modal depth of the formula. The base case (propositional formulas) is immediate. For the inductive step, we assume that the lemma holds for modal depth k, and show it for modal depth k + 1. The proof of the inductive step is by cases on the main connective of φ. The most difficult case is when φ = 〈〈A〉〉↓ψ′Uψ. We need to show that U-STRATEGY(node0(s(n), e(n)), φ) returns true iff iff s(n), e(n) |= 〈〈A〉〉↓ψ′Uψ.

(⇒) : Let T denote the search tree rooted at n0 = node0(s, η) when U-STRATEGY(node0(q, η), φ) returns true. Each node n in T is additionally annotated with the actual 3 endowment e′ (n) : Agt × Res → Z ∪ {∞} where (e′ (n0))i = ηi+∑n′∈p(n) t(ai(n′ )). Let sT denote the strategy for A where for each node n ∈ T with p(n) = n1 . . . n sT (s(n1) . . . s(n)) = (a(n))A for all n ∈ T and n1 . . . n = p(n). Note that, (e′ (n))i(r) can be negative for r and i which means sT is not a valid strategy. Then, there must be nodes n′ , n′′ ∈ p(n) such that (e(n′ ))r(i) = arb because of endowment in n′′ . Let n′ = stopr(n) and n′′ = startr(n). Let T(n) denote the subtree of T starting from n. For a resource r, if there is a node n with (e′ (n))i(r) < 0 for some i we extend T such that (e′ (n))i(r) ≥ 0 by repeating the branch between startr(n) and endr(n) finitely many times.

Case 1: n is the only node in T(startr(n)) with (e′ (n))r(a) < 0 as depicted by Figure 3a.

Assume that the path from startr(n) to endr(n) increases r by g. Then, it is necessary to repeat this path ⌈ |(e′ (n))r(a)| g ⌉ times, as depicted in Figure 3b.

Case 2: n is not the only node in T(startr(n)) with (e′ (n))r(a) < 0. Other nodes n′ are either in the subtree T(stopr(n)) (as depicted by Figures 4a) or in the subtree of T(startr(n)) but not T(stopr(n)) (as depicted by Figures 4b). Without loss of generality, we assume that startr(n) is the ancestor of startr(n′ ) for any of such n′ .

Again, assume that the path from startr(n) to endr(n) increases r by g. Then, it is necessary to repeat this path k = ⌈ |(e′ (n))r (a)| g ⌉ times, as depicted in Figure 5a. Note that this repetition will also repeat nodes n′ which are in the subtree of T(startr(n)) but not T(stopr(n)) and have (e′ (n′ ))r(a) < 0 as n′1 , . . . , n′k depicted in Figure 5b.

3 i.e., not containing arb.

Let T1 be the obtained tree. Then, the number of nodes n′′ in T1(nk-1) with (e′ (n′′ ))i(r) < 0 is strictly less than that in T(startr(n)). Therefore, we can reapply the above construction to obtain a tree T2 where all nodes n′′ in T2(nk-1) have (e′ (n′′ ))i(r) ≥ 0. These include node n′ as depicted in Figure 5a and n′k as depicted in Figure 5b. Then, we further apply step by step the above construction for nodes n′k-1 , . . . , n′1 and n′ in Figure 5b. Finally, we obtain a tree T3 where all nodes n′′ have (e′ (n′′ ))i(r) ≥ 0. This construction can be repeated for other resources r′ ̸= r and agents i′ ̸= i. Finally, we obtain a tree T4 where for all nodes n in T4, (e′ (n))i(r) ≥ 0 for all r and i.

(⇐) : As q, η |= 〈〈A〉〉↓ψ′Uψ, there exists a strategy sA such that for all λ ∈ out(q, η, sA,A) : ∃0 ≤ iλ < |λ| : λ|Q[iλ] |= ψ and ∀0 ≤ j < iλ : λ|Q[j], λ|En[j] |= ψ′ . Let T = (V,E) be the tree induced by all runs λ[0, iλ] for λ ∈ out(q, η, sA,A), i.e., V = {λ[0, i] | λ ∈ out(q, η, sA,A), i ≤ iλ} and E = {(λ[0, i], λ′ [0, i + 1]) | λ, λ′ ∈ out(s, η, sA,A), λ[0, i] = λ′ [0, i], i < iλ}. We shall cut T into a search tree which shows that USTRATEGY(node0(q, η), φ) returns true. Note that T must be finite and each edge in E corresponds to a join action of all agents.

Initially, let T0 = T, then Tl+1 is constructed from Tl as follows.

• If there is a node λ[0, i] in Tl such that ∃0 ≤ j < k ≤ i : λ|Q[j] = λ|Q[k] ∧ λ|En[j] ≥ λ|En[k], then Tl+1 is constructed from Tl by replacing the subtree Tl[λ[j]] by Tl [λ[k]].
• If there is a node λ[0, i] such that (λ|En[i])A = arbA, then Tl+1 is constructed from Tl by replacing the subtree Tl[λ[i]] by the only node λ[i].
• If there is a node λ[0, i] in Tl such that ∃0 ≤ j < k ≤ i : λ|Q[j] = λ|Q[k]∧λ|En[j] ≤ λ|En[k]∧λ|En[j] ̸= λ|En[k],

then Tl+1 is constructed from Tl by replacing the endowment η′ of all nodes (q′ , η′′ ) in the subtree Tl[λ[k]] by η′′ where

• Otherwise, Tl+1 = Tl, i.e., no more change.

The construction stops when Tl+1 = Tl. Let the resulting tree Tl+1 = T ′ . For each node λ[0, i] in T ′ , we define a node nλ[0,i] where: s(nλ[0,i]) = λ|Q[i], p(nλ[0,i]) = λ|Q[0, i - 1] and e(nλ[0,i]) = λ|En[i]. In the following, we show by induction on the length of T ′ (λ[0, i]) that U-STRATEGY(nλ[0,i], φ) returns true.

Base case: Assume that λ[0, i] is a leaf of T ′ , then it is either a leaf from T or an internal node from T that has an arbA endowment for agents in A by the second cut. Then, the condition of the first if statement in U-STRATEGY(nλ[0,i], φ) is false, since λ|Q[i] |= ψ in the former case and λ|Q[i] |= 〈〈A〉〉ψ′Uψ in the latter case. The condition in the second if statement is also false since otherwise T ′ can be cut further. Similarly, the conditions of the third and fourth if statements are true; therefore, U-STRATEGY(nλ[0,i], φ) returns true.

Induction step: Assume that λ[0, i] is not a leaf of T ′ . Then the condition of the first if statement is false, since q |= 〈〈A〉〉ψ′Uψ. The condition of the second if statement is also false, since otherwise T ′ can be cut further. The condition of the third or fourth if statement is false since otherwise λ[0, i] must have been a leaf of T ′ . Therefore, the algorithm must enter the second for loop. For α = sA(λ|Q[0, i]) ∈ DA(λ[i]) we have that, for every s′ ∈ out(λ|Q[i], α) with n′ = node(nλ[0,i], s′ , α, A, ↓), there must be λ′ [0, i+1] in T ′ such that n′ = nλ′ [0,i+1]. By the induction hypothesis, U-STRATEGY(nλ′ [0,i+1], φ) returns true. Thus, U-STRATEGY(nλ[0,i], φ) also returns true.

Obviously, U-STRATEGY(node0(q, η), φ) returns true since nλ[0] = node0(q, η) for any λ[0, i] in T ′ .

The above proof can be adapted to the case φ = 〈〈A〉〉ζ ψ′Uψ by exchanging the role of η and ζ. Finally, for the case φ = 〈〈A〉〉∗Gψ, we can also apply the above proof strategy. In particular, if G-STRATEGY(node0(q, η), φ) returns true, we construct a strategy from the search tree T where each leaf n of T determines a subtree T(n′ ) where s(n′ ) = s(n) and eA(n′ ) ≤ eA(n) by the third if statement. Then, we can replace all leaves n with T(n′ ) repeatedly and end up with an infinite tree T ′ which induces a strategy sT ′ to satisfy φ. Conversely, if q, η |= φ, then φ is satisfied by some strategy sA, and we can cut the tree of computations by sA into a search tree which shows that G-STRATEGY(node0(q, η), φ) returns true.

5 Conclusion

In this paper we investigated the boundary of (un)decidable of logics for verifying resource bounded systems. We proved two undecidability results and identified a significant fragment of Resource Agent Logic with a decidable model checking property. From these results it also follows that the rather natural property on models - that agents can always decide to do nothing - can make model checking decidable.