Natasha Alechina
email: n.a.alechina@uu.nl

Stéphane Demri
email: demri@lsv.fr

Brian Logan
email: brian.logan@nottingham.ac.uk

Parameterised Resource-Bounded ATL

It is often advantageous to be able to extract resource requirements in resource logics of strategic ability, rather than to verify whether a fixed resource requirement is sufficient for achieving a goal. We study Parameterised Resource-Bounded Alternating Time Temporal Logic where parameter extraction is possible. We give a parameter extraction algorithm and prove that the model checking problem is in 2EXPTIME.

Introduction

There has been a considerable amount of work on logics of strategic ability interpreted over structures where agents' actions consume resources, or both produce and consume resources. Examples include an extension of Coalition Logic where actions consume resources and coalitional modalities are annotated with resource bounds ('agents in coalition A have a strategy of cost at most b to achieve φ') (RBCL) [START_REF] Alechina | A logic for coalitions with bounded resources[END_REF]2011), a similar extension for Alternating Time Temporal Logic ATL (RB-ATL) [START_REF] Alechina | Resource-bounded alternating-time temporal logic[END_REF], extensions of Computation Tree Logic and Alternating Time Temporal Logic with both consumption and production of resources (RTL, RAL) (Bulling and Farwer 2010a;2010b), a variant of resource-bounded ATL where all resources are convertible to money and the amount of money is bounded (PRB-ATL) [START_REF] Della Monica | On a logic for coalitional games with priced-resource agents[END_REF]2013), an extension of PRB-ATL to µ-calculus (Della Monica and Lenzi 2012), a version of ATL with more general numerical constraints (QATL * ) [START_REF] Bulling | How to be both rich and happy: Combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract)[END_REF], and a version of RB-ATL where unbounded production of resources is allowed (RB±ATL) (Alechina et al. 2017b). These logics can express properties such as: 'a coalition of agents with n units of resource 1 and m units of resource 2 can reach a state where they can maintain property φ forever without spending any resources'. Essentially, such logics enable formulating and solving multi-agent conditional planning problems with resources, where the planning problems may be nested and involve invariant properties.

However, with one exception, these logics assume that the amount of resources available to the agents is fixed and Copyright c 2020, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. known in advance. Using these logics, it is possible to ask whether a strategy to achieve some goal exists if the agents start with e.g., 100 units of energy. It is not possible to ask what is the minimal amount of energy that makes some goal achievable (unless it is already known that it is achievable for some fixed cost). In other words, it is not possible to extract the values of resource parameters using model checking procedures for these logics. The only exception is the logic ParRB±ATL * (Parameterised RB±ATL * , Resource Bounded Alternating Time Temporal Logic) introduced in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]) that allows concrete values for resource parameters to be synthesised. Using ParRB±ATL * , we can ask what is the minimal amount of energy needed for achieving some goal, or for which values of x and y does it hold that coalition A has a strategy requiring at most x units of resource to enforce some temporal goal, and coalition A does not have a strategy to enforce another temporal goal with y units of resource. The function form of the model checking problem for ParRB±ATL * (return a set of constraints on the resource variables for which the formula is true) was shown to be decidable in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], but the upper bound on complexity of the problem was left open.

In this paper we study the model checking problem for the logic ParRB±ATL (Parameterised RB±ATL). ParRB±ATL is a fragment of ParRB±ATL * with the same syntax as RB±ATL (Resource Bounded ATL), but with variables instead of concrete values for resource amounts. We show that the complexity of the model checking problem for ParRB±ATL is 2EXPTIME-complete, and give an explicit algorithm to compute the set of assignments satisfying the formula. For positive formulas, this algorithm computes the set of Pareto optimal (non-dominated) resource bounds satisfying the formula.

Our results build on results and techniques developed in games on vector addition systems with states [START_REF] Courtois | Alternating vector addition systems with states[END_REF] and energy games [START_REF] Jurdzinski | Fixeddimensional energy games are in pseudo-polynomial time[END_REF]. In particular, we use the techniques designed to solve reachability problems with unknown initial credit for vector addition systems with states to model check formulas with the Until temporal operator, and techniques for solving non-termination problems with unknown initial credit for energy games for model checking invariant properties. The crux of establishing a 2EXPTIME upper bound for the ParRB±ATL model checking problem is showing that there is a maximal value of the amount of resource needed to reach a particular state or to enter and execute a non-resource-consuming loop, and this bound depends only on the model and not on the property to be checked. We briefly mention other related work here. The paper [START_REF] Juhl | Theories of Programming and Formal Methods -Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday[END_REF] deals with computing minimal winning vectors in multiweighted games. [START_REF] Juhl | Theories of Programming and Formal Methods -Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday[END_REF] states three decision problems and focuses on the second and third, that are less relevant for us (computing minimal upper bounds b such that on all infinite computations starting from 0, values stay below b). Their first problem, computing minimal winning vectors for multiweighted games when all the vectors in the infinite runs have non-negative values, is the most related to model-checking ParRB±ATL. At the time of [START_REF] Juhl | Theories of Programming and Formal Methods -Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday[END_REF], the best known approach to this problem was that given by [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF], which has upper bound (k-1)-EXPTIME, where k is the number of resource types. The paper [START_REF] Jurdzinski | Fixeddimensional energy games are in pseudo-polynomial time[END_REF] significantly improved on the results in [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF], which is why we use the results from [START_REF] Jurdzinski | Fixeddimensional energy games are in pseudo-polynomial time[END_REF] in our paper.

The main contribution of our paper is to show that the maximal value given in [START_REF] Jurdzinski | Fixeddimensional energy games are in pseudo-polynomial time[END_REF] transfers to ParRB±ATL, and to show how it can be used for nested temporal goals that include negations and a mixture of reachability and non-termination goals.

Syntax and Semantics of ParRB±ATL

In this section, we introduce the syntax and semantics of ParRB±ATL.

Let Agt = {a 1 , . . . , a n } be a set of n ≥ 1 agents and Res = {res 1 , . . . , res r } be a set of r ≥ 1 resource types, Π denote a set of propositions, and V ar a countably infinite set of variables.

We write ParRB±ATL(n,r) for the logic ParRB±ATL with n agents and r resources, interpreted over models with the same numbers of agents and resources. When talking about all possible n and r, we write ParRB±ATL.

Formulas of ParRB±ATL(n,r) are defined by the following syntax

ϕ ::= p | ¬ϕ | ϕ ∨ ψ | A x ϕ | A x ϕ | A x ϕ U ψ
where p ∈ Π is a proposition, A ⊆ Agt, and x is a sequence of variables x 1 , . . . , x r from V ar of length r, intuitively placeholders for amounts of resource 1 to resource r.

Since formulas contain variables, formulas are evaluated relative to a model, a state and an assignment of values to variables. Informally, a state s and assignment x 1 → b 1 , . . . , x r → b r where the b i 's are in N (which we will write as a mapping between vectors, x → b) satisfies A x ϕ if A has a joint action with cost at most b such that all outcomes of this action satisfy ϕ. Similarly, A x ϕ is satisfied if A has a strategy to ensure that ϕ is always true, and the cost of any computation generated by this strategy is at most b; A x ϕ U ψ is satisfied if A has a strategy to enforce ψ while maintaining the truth of ϕ, and the cost of this strategy is at most b.

The models of the logic ParRB±ATL are resourcebounded concurrent game structures (RB-CGS) introduced in [START_REF] Alechina | Resource-bounded alternating-time temporal logic[END_REF], which are also the models of RB±ATL. Definition 1. A resource-bounded concurrent game structure is a tuple M = (Agt, Res, S, Π, π, Act, d, c, δ) where:

• Agt is a non-empty set of n agents, Res is a non-empty set of r resources and S is a finite non-empty set of states. • Π is a finite set of propositional variables and π : Π → ℘(S) is a truth assignment which associates each proposition in Π with a subset of states where it is true. • Act is a non-empty set of actions which includes idle, and d : S ×Agt → ℘(Act) is a function which assigns to each s ∈ S a non-empty set of actions available to each agent a ∈ Agt. For every s ∈ S and a ∈ Agt, idle ∈ d(s, a).

We denote joint actions by all agents in Agt available at

s by D(s) = d(s, a 1 ) × • • • × d(s, a n ). • c : S × Agt × Act → Z r
is a partial function which maps a state s, and agent a and an action α ∈ d(s, a) to a vector of integers where the integer in position i indicates consumption or production of resource res i by the action (positive value for consumption and negative value for production). We stipulate that c(s, a, idle) = 0 for all s ∈ S and a ∈ Agt where 0 = (0, . . . , 0) ∈ N r . • δ : (s, σ) → S is a function that for every s ∈ S and joint action σ ∈ D(s) gives the state resulting from executing σ in s.

Given an RB-CGS M , we denote the set of all infinite sequences of states (computations) by S ω and the set of nonempty finite sequences of states by S + . For a computation λ = s 0 s 1 . . . ∈ S ω , we use the notation λ[i] = s i and λ[i, j] = s i . . . s j where j ≥ i ≥ 0.

Given an RB-CGS M and a state s ∈ S, a joint action by a coalition A ⊆ Agt is a tuple σ = (σ a ) a∈A such that σ a ∈ d(s, a). The set of all joint actions for A at state s is denoted by D A (s). Given a joint action by the grand coalition σ ∈ D(s), σ A denotes the joint action executed by A: σ A = (σ a ) a∈A . The set of all possible outcomes of a joint action σ ∈ D A (s) at state s is:

out(s, σ) = {δ(s, σ ) | σ ∈ D(s) ∧ σ = σ A } The cost of a joint action σ ∈ D A (s) is defined as: cost(s, σ) = a∈A c(s, a, σ a ) Given an RB-CGS M , a strategy for a coalition A ⊆ Agt is a mapping F A : S + → Act |A| such that, for every λs ∈ S + , F A (λs) ∈ D A (s). A computation λ ∈ S ω is consistent with a strategy F A iff, for all i ≥ 0, λ[i + 1] ∈ out(λ[i], F A (λ[0, i])).
We denote by out(s, F A ) the set of all computations λ consistent with F A that start from s.

We use the usual point-wise notation for vector comparison and addition. In particular, (b

1 , . . . , b r ) ≤ (d 1 , . . . , d r ) iff b i ≤ d i for all i ∈ {1, . . . , r}, and (b 1 , . . . , b r ) + (d 1 , . . . , d r ) = (b 1 + d 1 , . . . , b r + d r ).
For convenience, let us denote the set of possible resource bounds by B

= N r . Given a bound b ∈ B, a computation λ ∈ out(s, F A ) is b-consistent with F A iff, for every i ≥ 0, i j=0 cost(λ[j], F A (λ[0, j])) ≤ b
Note that this definition implies that if agents start with resource allocation b, then on every prefix of the computation the amount of resources they have is never below 0. Furthermore, the constraint on b-consistent computations involves only action costs for agents from the coalition A (and not on the agents outside A).

The set of all b-consistent computations of

F A starting from state s is denoted by out(s, F A , b). F A is a b-strategy iff out(s, F A ) = out(s, F A , b) for any state s.
Given an RB-CGS M , a state s of M , the truth of a ParRB±ATL formula ϕ with respect to M , s and assignment v from the set of variables to N is defined inductively on the structure of ϕ as follows:

• M, s, v |= p iff s ∈ π(p); • M, s, v |= ¬φ iff M, s, v |= φ; • M, s, v |= φ ∨ ψ iff M, s, v |= φ or M, s, v |= ψ; • M, s, v |= A x φ iff there exists a v(x)-strategy F A such that for all λ ∈ out(s, F A ): M, λ[1], v |= φ; • M, s, v |= A x φ iff there exists a v(x)-strategy F A such that for all λ ∈ out(s, F A ) and i ≥ 0: M, λ[i], v |= φ; • M, s, v |= A x φ U ψ iff
γ := x ≥ b | | ⊥ | ¬γ | γ ∧ γ | γ ∨ γ
Clearly, if the function form of the problem is solvable, then both model checking problems for ParRB±ATL are decidable.

The following is an immediate consequence1 of Theorem 8 in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]): Theorem 1. The function form of the model checking problem for ParRB±ATL is decidable.

However, the upper bound on complexity for this problem is not known. The method for proving decidability of the function form of the model checking problem for ParRB±ATL * is by reduction to parity games on singlesided VASS [START_REF] Abdulla | Solving Parity Games on Integer Vectors[END_REF]). In the next section, we give a direct algorithm model checking ParRB±ATL. Theorem 2. The lower bound on the complexity of the known initial assignment model checking problem for ParRB±ATL is 2EXPTIME.

Proof. From the result that the model checking problem for RB±ATL is 2EXPTIME-hard (Theorem 3, [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF])) when r is an input parameter 2 . Note that the proof of Theorem 3 in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF] does not require infinite bounds, so the result also holds for RB±ATL without infinite bounds. It is straightforward to reduce the model checking problem for RB±ATL to the known initial assignment model checking problem for ParRB±ATL.

Upper Bound on the Complexity of the Function Form of the ParRB±ATL Model Checking Problem

In this section, we first introduce the key concepts used in the model checking algorithm for ParRB±ATL, and in the process show that Until and Box formulas of ParRB±ATL that do not contain nested modalities can be model-checked in 2EXPTIME. Then we state the model checking algorithm and the general result on the upper bound on complexity of the function form of the model checking problem for ParRB±ATL.

Preliminaries and Definitions

The proof of 2EXPTIME upper bound for the function form of the ParRB±ATL model checking problem builds on results for reachability games with unknown initial credit for alternating vector addition systems with states (Courtois and Schmitz 2014) and non-termination energy games with unknown initial credit [START_REF] Jurdzinski | Fixeddimensional energy games are in pseudo-polynomial time[END_REF]. These results roughly correspond to model checking formulas of the form A x φ U ψ and A x φ, respectively, where φ and ψ do not in turn contain variables, i.e. these are propositional formulae.

First we introduce a notion of a witness for a successful A-strategy in enforcing a formula of the form A x φ U ψ. Informally, it is a finite tree with the root labelled Observe that a witness corresponds to a perfect recall bstrategy for A, because after reaching the leaf nodes satisfying ψ, the coalition can forever execute the idle action that consumes no resources.

A witness for M, s, x → b |= A x φ is defined similarly. Definition 6. A witness for M, s, x → b |= A x φ is a finite tree with root (s, b) where in every node the state satisfies φ, all resource allocations in the nodes are nonnegative, and for each leaf node (s , b ) there is exactly one other node (s , b ) on the same branch with the same state s and b ≤ b .

In other words, a witness for A x φ describes the initial prefix of a successful strategy for satisfying A x φ. It can be extended to a perfect recall b-strategy for A since it describes how to enforce a non-consuming loop on any computation.

Clearly, if there is a witness for M, s, x → b |= φ, then there is also a witness for M, s, x → b |= φ, where b ≤ b (the same strategy will work for a greater initial resource allocation). We will also talk about w being a witness for φ being true in M and s if there is some assignment v such that w is a witness for M, s, v |= φ, and about w being a witness for φ being true in M if there is some state s and assignment v such that w is a witness for M, s, v |= φ.

A norm of a vector b is the largest component of the vector (by absolute value), max(|b[i]|). This notion can be extended to the norm of a finite set of vectors. The largest value occurring in a description of an RB-CGS M is the norm of the set of costs of actions. We will denote this number by max M . Similarly, we can talk about the norm of a witness w, w . Let us call a witness w norm-minimal for some model-checking instance if there is no witness w for the same model-checking instance with w < w . Proposition 1. If a witness for A x φ being true in M, s exists, then there exists a witness w with w ≤ (4|S| • max M ) 2(r+2) 3 .

Proof. The proof uses two results from [START_REF] Jurdzinski | Fixeddimensional energy games are in pseudo-polynomial time[END_REF]. The first result (Lemma 3.1) is that if Player 1 has a winning strategy in a bounded energy game (ensuring non-termination, with counters remaining nonnegative and below a certain bound), then Player 1 has a strategy where the norm of any computation is bounded by

(4|S| • max M ) 2(r+2) 3
. The second result (Proposition 2.4) is that Player 1 has a winning strategy in a non-termination energy game if and only if Player 1 has a winning strategy in a bounded energy game on the same graph with resource-decrementing loops added to every state. To construct the winning strategy for the bounded game, resourcedecrementing loops can be used to keep the resource amounts below the upper bound, while the transitions in the non-termination energy game simply ignore decrementing loops (in particular, they may involve incrementing some resource forever in a loop). If all 'useful' (non-resourcedecrementing-loop transitions) in the bounded game can be accomplished without more than (4|S| • max M ) 2(r+2) 3 resources on any counter up to the point the 'final' loop is repeatedly executed, then the same applies to the original energy game, and hence to a witness for A x φ being true in M, s.

Proposition 2. If a witness for A x ψ 1 U ψ 2 being true in M, s exists, then there exists a witness w with w ≤ (4(|S| + 1)

• max M ) 2(r+3) 3 .
Proof. By contradiction, assume that in some model M , a norm-minimal witness w for

A x ψ 1 U ψ 2 being true in M, s has norm w > (4(|S| + 1) • max M ) 2(r+3) 3
. Produce a model M from M as follows. If any joint action by A which is involved in w is composed of only idle actions by all agents in A, add to M another 0 cost action α and replace idle with α in w. Add an extra resource type r +1, and let all actions by agents in A involved in w (apart from the idle action) consume one unit of r +1. Redirect all other transitions (not involved in w) to an additional new state s not satisfying ψ 2 . Note that M contains a witness w corresponding to w but with extra costs on the (r + 1)th resource, and w is still a minimal (and the only) witness for A x ψ 1 U ψ 2 . This is because the only state in M that is not part of w is s , and a ψ 2 state is not accessible from s . Note also that w does not contain any non-resource-consuming loops on the branches leading to ψ 2 states because of the costs on the (r + 1)th resource. Now to complete the transformation of M into M , we add a new propositional variable p that holds in all w states but not in s , and add 0 cost self-loops by the idle action to all ψ 2 states. Consider the formula A x p. The only way to satisfy it in M , s is to use a strategy corresponding to w . (This is because the only way to reach a nonresource-consuming loop satisfying p is to reach a ψ 2 state, and w is a minimal witness to reaching a ψ 2 state while satisfying ψ 1 , hense while satisfying p). The norm of w is still the same as the norm of w (without loss of generality, we assume that the costs on r + 1 are less than w ), so the normminimal witness for A x p has the norm strictly greater than (4

(|S| + 1)• max M ) 2(r+3) 3
, that is, strictly greater than

(4|S |) • max M ) 2(r +2) 3
, where |S | = |S| + 1 is the number of states in M and r = r + 1 is the number of resource types in M . This contradicts Proposition 1.

Given that the norm of a norm-minimal witness is bounded by

B M = (4(|S| + 1) • max M ) 2(r+3) 3
, the height of a witness is bounded by an exponential in r and max M (since the model is encoded in binary). This means that all such potential witnesses can be generated and checked by an alternating Turing Machine in EXPSPACE. As pointed out in [START_REF] Courtois | Alternating vector addition systems with states[END_REF], this gives a naive algorithm for computing the Pareto frontier (all non-dominated initial resource allocations): all potential witnesses with resource allocations at the root starting from (0, . . . , 0) and up to (B M , . . . , B M ) can be explored in turn in AEX-PSPACE, and the non-dominated values b saved as constraints

x ≥ b. Since ASPACE(f (n)) = DTIME(2 O(f (n))
), AEXPSPACE=2EXPTIME, and this algorithm produces a description of satisfying assignments for non-nested Box and Until formulas in 2EXPTIME. In the next section, we show that this upper bound applies to the whole language.

Model checking algorithm

In this section, we present a 2EXPTIME algorithm to solve the function form of the ParRB±ATL model checking problem. Given a model M and a ParRB±ATL formula φ with variables x 1 , . . . , x n , the algorithm returns a set of pairs φ M of the form (s, γ) where s is a state and γ a constraint formula describing assignments v to x 1 , . . . , x n such that M, s, v |= φ.

Note that γ could be equivalent to ⊥ (unsatisfiable), in which case there is no assignment v such that M, s, v |= φ. We will say that γ is satisfiable iff there is at least one assignment v satisfying the constraints in γ.

To formulate the cases for A x ψ 1 U ψ 2 and A x ψ, we need to redefine the notion of a witness relative to ψ 1 M , ψ 2 M , and ψ M . A constrained witness for A x ψ 1 U ψ 2 being true in M, s is a finite tree where each leaf is a node of the form (s , b ) (for some b ) where s is such that (s , γ ) ∈ ψ 2 M and γ is satisfiable. All other nodes are of the form (s , b ) where (s , γ ) ∈ ψ 1 M and γ is satisfiable. A constrained witness w for A x ψ 1 U ψ 2 being true in M, s is exactly like a (non-constrained) witness for A x ψ 1 U ψ 2 being true in M, s, but instead of requiring states in the nodes to satisfy ψ 1 or ψ 2 , we require them to be in ψ i M with a satisfiable constraint formula γ . There is a point that needs to be made, namely why we do not require that b satisfies γ . Indeed, in the definition of γ(w) below, γ will be taken into account.

Similarly, a constrained witness for A x ψ is obtained from a witness by replacing the notion of a state s satisfying ψ with a requirement that (s , γ ) ∈ ψ M and γ is satisfiable.

We call a constrained witness w with the root (s, b) nondominated if it is norm-minimal and there is no constrained witness w with root (s, b ) such that b < b.

We denote the set of non-dominated constrained witnesses for (M, s, ψ) by W (M, s, ψ). This set is finite and each witness has height bounded by |S| • (B M + 1) r by Propositions 2 and 1 (because no two nodes on the same branch have the same state and resource vector, and the maximal value in resource vector is B M ).

Given a constrained witness w, we define a formula γ(w) describing constraints on the nodes in w. Intuitively, for formulas of the form A x ψ 1 U ψ 2 and A x ψ, the constraint on x is x ≥ b if the root of the witness is (s, b). There are however additional provisos. If some of the variables in x occur in proper subformulas of that formula, then there will be some more constraints on x arising from the constraints on the occurrences in proper subformulas. Also, constraint

x ≥ b is only tight (in the sense of M, s, v |= A x ψ 1 U ψ 2 iff v |= x ≥ b)
, if the witness is non-dominated. In addition to x, ψ 1 , ψ 2 and ψ may have other strategic modalities with variables y. The purpose of the formula γ(w) is to extract the constraint on y from the witness, by combining constraint formulas for the states in nodes of the witness.

For a constrained witness w for A x ψ 1 U ψ 2 with a root (s, b),

γ(w) = x ≥ b∧ s ∈leaves(w),(s ,γ )∈ ψ 2 M γ ∧ s ∈-leaves(w),(s ,γ )∈ ψ 1 M γ where s ∈ leaves(w) if (s , b ) is a leaf node of w and s ∈ -leaves(w) if (s , b ) is a non-leaf node of w.
For a constrained witness w for A x ψ with a root (s, b),

γ(w) = x ≥ b ∧ s ∈nodes(w),(s ,γ )∈ ψ M γ where s ∈ nodes(w) if (s , b ) for some b is a node of w.
For each subformula φ of φ 0 in increasing order of complexity, Algorithm 1 computes φ M . Theorem 3. On the input of M, φ 0 , Algorithm 1 returns a set of pairs φ 0 M such that (s, γ)

∈ φ 0 M iff for all v M, s, v |= φ 0 iff v |= γ. Algorithm 1 Computing φ 0 1: function PARRB±ATL-MC(M, φ 0 ) 2: for φ ∈ Sub(φ 0 ) do 3: case φ = p 4: p M ← {(s, ) : s ∈ π(p)} ∪ {(s, ⊥) : s ∈ π(p)} 5: case φ = ¬ψ 6: ¬ψ M ← {(s, ¬γ) : (s, γ) ∈ ψ M } 7: case φ = ψ 1 ∧ ψ 2 8: ψ 1 ∧ ψ 2 M ← {(s, γ 1 ∧ γ 2 ) : (s, γ 1 ) ∈ ψ 1 M ∧ (s, γ 2 ) ∈ ψ 2 M } 9: case φ = ψ 1 ∨ ψ 2 10: ψ 1 ∨ ψ 2 M ← {(s, γ 1 ∨ γ 2 ) : (s, γ 1 ) ∈ ψ 1 M ∧ (s, γ 2 ) ∈ ψ 2 M } 11: case φ = A x ψ 12: A x ψ M ← {(s, γ) : γ = σ∈D A (s) (x ≥ cost(σ, s) ∧ s ∈out(s,σ),(s ,γ )∈ ψ M γ )} 13: case φ = A x ψ 1 U ψ 2 14: A x ψ 1 U ψ 2 ← {(s, γ) : γ = w∈W (M,s, A x ψ1 U ψ2) γ(w)} 15: case φ = A x ψ 16: A x ψ ← {(s, γ) : γ = w∈W (M,s, A x ψ) γ(w)} 17: return φ 0 M
Proof. The proof is by induction on the complexity of φ 0 . The inductive hypothesis is that (s, γ)

∈ φ M iff (M, s, v |= φ iff v |= γ).
Clearly this holds for atomic propositions: (s, ) ∈ p M iff M, s |= p, by line 4 of Algorithm 1. For booleans, the conditions on assignments are also straightforward (lines 6, 8, 10).

Consider A x ψ. M, s, v |= A x ψ iff v assigns to x the amount of resources sufficient to execute an action σ such that all outcomes of that action satisfy ψ under v. (This σ is the first action in the successful strategy, but just as in the case of Until, all subsequent actions in the strategy can be chosen to be idle, which means the strategy will not require more than v(x) resources.) By the inductive hypothesis, all outcomes of σ satisfy ψ under v iff for every state s in out(s, σ) such that (s , γ

) ∈ ψ M , v |= γ , that is, iff v |= s ∈out(s,σ),(s ,γ )∈ ψ M γ . Hence M, s, v |= A x ψ iff for some executable σ, v |= s ∈out(s,σ),(s ,γ )∈ ψ M γ . This is exactly what line 12 of Algorithm 1 requires for A x ψ M . M, s, v |= A x ψ 1 U ψ 2 iff
there is a strategy such that each computation on this strategy satisfies ψ 1 under v until it satisfies ψ 2 under v. This holds iff there is a witness w such that initial amount of resources is sufficient to execute the corresponding strategy and all nodes in the witness satisfy the corresponding formulas under v. By the inductive hypothesis, this holds iff for some witness rooted in (s, b) with b ≤ v(x), v |= w∈W (M,s, A x ψ1 U ψ2) γ(w), which is the constraint formula on line 14 of Algorithm 1.

Similarly for A x ψ: M, s, v |= A x ψ holds iff there is a strategy such that each computation on this strategy reaches a loop where no resources are consumed and every state on this computation satisfies ψ under v. By the inductive hypothesis, this holds iff for some witness w rooted in (s, b) with b ≤ v(x), v satisfies γ(w), iff v |= w∈W (M,s, A x ψ1) s ∈nodes(w),(s ,γ )∈ ψ M γ , which is the constraint formula on line 16 of Algorithm 1.

Observe that if φ is a positive formula (does not contain modalities in the scope of negations), then the corresponding constraint formula γ only has subformulas of the form x ≥ b. Since the constraint formula describes nondominated witnesses, it specifies the optimal values of resource parameters (the Pareto frontier). Proof. The set of non-dominated witnesses W (M, s, φ ) for each subformula φ of φ 0 can be computed in AEXSPACE. Hence the whole algorithm can be executed in AEXSPACE which is equivalent to 2EXPTIME.

Conclusions and Future Work

Algorithm 1 returns a set of states satisfying a ParRB±ATL formula together with a constraint formula describing the set of assignments to resource variables for which the ParRB±ATL formula is true in that state. The algorithm can be easily modified to return the witness (finite representation of the strategy). The complexity of the algorithm is very high (2EXPTIME). However, only the number of resource types and the log of the largest cost in the model (logmax M ) are in the exponent; the running time is polynomial in the number of states and transitions in the model.

In future work we plan to implement the algorithm. Another direction of future work is a parametrised version of the fragment of Resource Agent Logic (RAL) with a decidable model checking problem that was described in (Alechina et al. 2017a). In ParRB±ATL, the resources needed for satisfying each strategic modality are independent, even if nested subformulas share variables. For example, A x U (q ∧ A x U p) means that there is a value for x, e.g., 5, such that given 5 units of the resource, A can enforce a state where q holds, and from where, given 5 units of the resource, A can enforce p. The second, nested, strategy does not use the amount of resource remaining from the execution of the first strategy, but starts from scratch with x resources, whatever value x happens to have. On the other hand, in RAL, there is an extra annotation for strategic modalities that means 'with the remaining resources'. For example, A x U (q ∧ A ↓ U p) means that there is a value for x, such that if A have this amount of resources, then they could enforce a state where q holds, and with remaining resources, they could enforce p. This logic can be used to solve model checking problems that involve nested goals that share a single allocation of resources.

  there exists a v(x)-strategy F A such that for all λ ∈ out(s, F A ), there exists i ≥ 0 such that M, λ[i], v |= ψ and M, λ[j], v |= φ for all j ∈ {0, . . . , i -1}.Note that along the evaluation of formula, the assignment v does not vary, and the formulae are evaluated on states and not on pairs of the form (s, b).The two decision forms of the model-checking problem for ParRB±ATL are as follows.Definition 2. The following problem is the unknown initial assignment model checking problem for ParRB±ATL.Input: n, r ≥ 1 (in unary), a formula ϕ in ParRB±ATL(n,r), a finite model M , and a state s. Question: Is there an assignment v such that M, s, v |= ϕ? Definition 3. The following problem is the known initial assignment model checking problem for ParRB±ATL. Input: n, r ≥ 1 (in unary), a formula ϕ in ParRB±ATL(n,r), a finite model M , a state s, and an assignment v. Question: Is it true that M, s, v |= ϕ? The function form of the model-checking problem is to compute the set of all satisfying assignments. Definition 4. The following problem is the function form of the ParRB±ATL(n,r) model checking problem. Input: n, r ≥ 1 (in unary), a formula ϕ in ParRB±ATL(n,r), a finite model M , and a state s. Output: Compute a formula γ describing the set of assignments v such that M, s, v |= ϕ, where γ is of the following form (for b ∈ N):

  (s, b), representing the result of executing a successful A-strategy from s under assignment x → b until ψ states are reached on all branches. Definition 5. Given a formula of the form A x φ U ψ, a state s in an RB-CGS M , and a vector of r natural numbers b, a finite tree with root (s, b) is a witness for M, s, x → b |= A x φ U ψ if • all nodes of the tree are of the form (s , b ) where s is a state (resulting from executing the joint action in the state of the parent node) and b the vector of resource amounts A have in s as a result, and b ≥ 0, • in all leaf nodes (s , b ) of the tree, s satisfies ψ (since ψ is propositional, this can be determined using only the truth assignment π), • in all non-leaf nodes (s , b ) of the tree, s satisfies φ (again, only the truth assignment π in needed here). In the first point of the definition, an edge (s, b) → (s , b ) is present in the tree because of some joint action σ ∈ D(s), such that δ(s, σ) = s , and for all i ∈ [1, r], we have b [i] = b[i] -(Σ a∈A c(s, a, σ(a))[i]). Note that in the expression above, the value c(s, a, σ(a))[i] is involved negatively.

Theorem 4 .

 4 The upper bound on the complexity of the function form of the model checking problem for ParRB±ATL is 2EXPTIME.

The set of assignments considered in(Alechina et al.

2018) is not of the form V ar → N but of the form V ar → N ∪ {∞}, and the constraint formula may include x = ∞. This is motivated by the connection between ParRB±ATL * and RB±ATL where modalities have bounds which may contain ∞. That in turn was motivated by the desire to make RB±ATL a conservative extension of ATL. However, the proof of Theorem 8 in[START_REF] Alechina | On the complexity of resource-bounded logics[END_REF] goes through for the case when assignments are of the form V ar → N, which is what we are interested in this paper.2 It is EXPTIME-hard for fixed r ≥ 4, see Corollary 1 in[START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]).