Francesco Belardinelli
email: francesco.belardinelli@imperial.ac.uk

Stéphane Demri
email: demri@lsv.fr

Strategic Reasoning with a Bounded Number of Resources: the Quest for Tractability

The resource-bounded alternating-time temporal logic RB±ATL combines strategic reasoning with reasoning about resources. Its model-checking problem is known to be 2exptime-complete (the same as its proper extension RB±ATL * ) and fragments have been identified to lower the complexity.

In this work, we consider the variant RB±ATL + that allows for Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL + restricted to a single agent and a single resource is ∆ P 2 -complete, hence the same as for the standard branching-time temporal logic CTL + . In this case reasoning about resources comes at no extra computational cost. When a fixed finite set of linear-time temporal operators is considered, the model-checking problem drops to ptime, which includes the special case of RB±ATL restricted to a single agent and a single resource. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the model-checking problem for RB±ATL + can be solved in exptime using a sophisticated Turing reduction to the parity game problem for alternating vector addition systems with states (AVASS).

Introduction

Reasoning about resources with ATL-like logics. Reasoning about multi-agent systems (MAS) -in which autonomous agents can interact and perform actions to reach (joint or individual) goals -has benefited from the model-checking approach with the development of ATL-like logics (see e.g., [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | MOCHA user manual[END_REF]). In recent years, logic-based languages for the specification and verification of the strategic behaviour of agents in MAS have been the object of increasing interest amongst researchers applying formal methods to artificial intelligence. A wealth of logics for strategies have been proposed in the literature, including Alternating-Time Temporal Logic ATL [START_REF] Alur | Alternating-time temporal logic[END_REF], possibly extended with strategy contexts [START_REF] Laroussinie | Augmenting ATL with strategy contexts[END_REF], Coalition Logic [START_REF] Pauly | A modal logic for coalitional power in games[END_REF], Strategy Logic [START_REF] Chatterjee | Strategy logic[END_REF][START_REF] Mogavero | Reasoning about strategies: On the model-checking problem[END_REF], among others. The expressive power of these formalisms has been thoroughly studied, as well as the corresponding verification problems, thus leading to model-checking tools for concurrent game structures and multi-agent systems [START_REF] Cermák | MCMAS-SLK: A model checker for the verification of strategy logic specifications[END_REF][START_REF] Lomuscio | MCMAS: an open-source model checker for the verification of multi-agent systems[END_REF][START_REF] Alur | jMocha: A model checking tool that exploits design structure[END_REF][START_REF] Kacprzak | Verics 2007 -a model checker for knowledge and real-time[END_REF].

It is worth noticing that the computational models underlying these logic-based languages share a common feature: actions are normally modelled as abstract objects (typically a labelling on transitions) that bear no computational cost. However, if logics for strategies are to be applied to concrete AI scenarios, it is key to account for the resources that actions might consume or produce. These considerations have prompted recently investigations in resource-aware logics for strategies [START_REF] Alechina | State of the art in logics for verification of resource-bounded multi-agent systems[END_REF][START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]. The need for managing resources in MAS has been identified quite early and many logical formalisms based on ATL have been introduced to endow actions with consumption or production of resources [START_REF] Bulling | On the (Un-)Decidability of Model-Checking Resource-Bounded Agents[END_REF][START_REF] Della Monica | On a logic for coalitional games with priced-resource agents[END_REF][START_REF] Bulling | How to be both rich and happy: Combining quantitative and qualitative strategic reasoning about multi-player games[END_REF][START_REF] Alechina | Decidable model-checking for a resource logic with production of resources[END_REF][START_REF] Alechina | On the boundary of (un)decidability: Decidable model-checking for a fragment of resource agent logic[END_REF]. Unsurprisingly, dealing with resources can lead to high complexity, even undecidable model-checking problems, which is best illustrated in [START_REF] Bulling | On the (Un-)Decidability of Model-Checking Resource-Bounded Agents[END_REF][START_REF] Bulling | How to be both rich and happy: Combining quantitative and qualitative strategic reasoning about multi-player games[END_REF][START_REF] Alechina | On the boundary of (un)decidability: Decidable model-checking for a fragment of resource agent logic[END_REF]. For instance, the ATL-like logics introduced in [START_REF] Bulling | How to be both rich and happy: Combining quantitative and qualitative strategic reasoning about multi-player games[END_REF] are quite rich and general, but it is not obvious which features are to be restricted to regain decidability. Still, decidable resource-aware logics have been identified, for instance by allowing only resource consumption [START_REF] Alechina | A logic for coalitions with bounded resources[END_REF]. The challenge for years has been to design resource-aware logics, general enough to allow consumption and production of resources, while having a decidable model-checking problem, possibly low complexity, to allow the implementation in model-checking tools.

From RB±ATL to RB±ATL * . Early decidability results for the model-checking problem for RB±ATL [START_REF] Alechina | Decidable model-checking for a resource logic with production of resources[END_REF][START_REF] Alechina | Model-checking for resource-bounded ATL with production and consumption of resources[END_REF] made use of a technique with high complexity (comparable to the complexity of building Karp-Miller trees for Petri nets, see e.g. [START_REF] Karp | Parallel program schemata[END_REF]). The logic RB±ATL is a resource-aware logical formalism that extends ATL by endowing actions with the consumption and production of resources [START_REF] Alechina | Decidable model-checking for a resource logic with production of resources[END_REF]. In [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], its model-checking problem is shown 2exptime-complete by using subroutines to solve decision problems for alternating vector addition systems with states (AVASS), see e.g., [START_REF] Courtois | Alternating vector addition systems with states[END_REF][START_REF] Jurdziński | Fixed-dimensional energy games are in pseudo-polynomial time[END_REF][START_REF] Abdulla | Solving Parity Games on Integer Vectors[END_REF]. The 2exptime-completeness has also been extended to RB±ATL * , the extension of RB±ATL in which path formulae are arbitrary LTL formulae, in the same way as the temporal logic CTL * extends CTL (see [START_REF] Demri | Temporal Logics in Computer Science[END_REF]Chapter 7]). The 2exptime upper bound proof for RB±ATL * reveals to be a bit more complex as it requires the determinisation of Büchi automata and a subroutine to solve the parity game problem for AVASS [START_REF] Colcombet | Perfect half space games[END_REF], as well as a refined analysis of the complexity function. Consequently, every logic syntactically between RB±ATL and RB±ATL * admits a 2exptime-complete model-checking problem and this also applies to RB±ATL + , the extension of RB±ATL in which path formulae are arbitrary Boolean combinations of LTL formulae of temporal depth one, in the same way as the temporal logic CTL + extends CTL (see, e.g., [START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF]). Although the model-checking problem for CTL (resp. CTL + , CTL * ) is known to be ptime-complete (resp. ∆ P 2 -complete, pspace-complete) and the one for ATL (resp. ATL + , ATL * ) ptime-complete [START_REF] Alur | Alternating-time temporal logic[END_REF] (resp. pspace-complete [START_REF] Bulling | Verifying agents with memory is harder than it seemed[END_REF][START_REF] Goranko | Game-theoretic semantics for ATL + with applications to model checking[END_REF], 2exptime-complete [START_REF] Alur | Alternating-time temporal logic[END_REF]), there is no difference in complexity for RB±ATL, RB±ATL + and RB±ATL * , as far as worst-case complexity is concerned.

Our motivation for the present contribution is threefold. Firstly, in the literature there are several gaps in the results available for the decidability and complexity related to the model-checking problem for RB±ATL [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]. For instance, if we assume two resources and two agents in our multi-agent systems, then the model-checking problem for RB±ATL is known to be pspace-hard [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF] and in exptime [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Cor. 1], but no tight complexity result is available. Our long-term aim is to fill all such gaps eventually. Secondly, while completing this picture, it is of interest to identify model-checking instances that are tractable. Although the notion of tractable decision problem is open to discussion, in the context of strategy and temporal logics a model-checking problem decidable in polynomial time (in the size of the formula and the concurrent game structure) falls certainly within the description, as it makes it amenable to implementation in a modelchecking tool. Thirdly, complexity results for resource-bounded ATL are proved by using a wealth of different techniques, thus hindering a clear vision of the state of the art. We aim at developing a unified framework based on general proof techniques. Vector addition systems with states (VASS) and their alternating version (AVASS) are key in this respect (see e.g. [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Courtois | Alternating vector addition systems with states[END_REF]). Thus, our main motivation consists in reducing the complexity gaps for many meaningful fragments of resource-bounded ATL, in identifying fragments with tractable model-checking, and in proposing optimal algorithms. Finally, we aim at developping proof methods based on counter machines, which happens to be quite natural in view of the nature of the resources.

Let us develop these lines a bit more. When identifying fragments of RB±ATL * of tractable complexity, with the aim of implementing model-checking algorithms in existing tools [START_REF] Lomuscio | MCMAS: an open-source model checker for the verification of multi-agent systems[END_REF], it may happen that RB±ATL, RB±ATL + , and RB±ATL * have distinct complexity when their fragments are considered, typically by restricting the number of resources or the number of agents. It is commonly accepted that the design of suitable fragments is essential to find a good compromise between the expressive power of the logical language and the computational complexity of the reasoning tasks. That is why the quest for subproblems of RB±ATL * obtained by limiting the temporal expressivity, the class of concurrent game structures, or the number of resources is important for practical use. In this paper, we study specifically the complexity of the model-checking problem for RB±ATL + (strict syntactic fragment of RB±ATL * ) restricted to a bounded number of resources, with a special attention to the case of a single resource. The same approach is also adopted for RB±ATL restricted to a single resource. It is worth noting that as the path formulae in CTL + (as well as in ATL + and in RB±ATL + ) are Boolean combinations of LTL formulae of temporal depth one, this provides a generic and natural way to design linear-time constraints. Surprisingly, this specific viewpoint considering fragments of RB±ATL + happens to be fruitful, not only for the identification of interesting fragments of lower complexity, but also in terms of proof techniques to solve the model-checking problem (see Section 4).

Our contribution. Based on the logics RB±ATL and RB±ATL * studied in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF] and for which the respective model-checking problems are 2exptime-complete, we identify tractable fragments and lower the worst-case complexity for other fragments. Details follow.

1. We introduce the logic RB±ATL + , similarly to the way ATL + (resp. CTL + ) extends ATL (resp. CTL). We prove that the model-checking problem for RB±ATL + restricted to a single agent and to a single resource is ∆ P 2 -complete (Theorem 11). The ∆ P 2 upper bound combines ingredients for model-checking CTL + with procedures in ptime for decision problems for vector addition systems with states (VASS) [START_REF] Karp | Parallel program schemata[END_REF] restricted to a single counter, newly introduced in this paper. Since CTL + model-checking is also ∆ P 2 -complete [START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF], we observe that the enhanced expressivity provided by reasoning about a single resource comes at no extra computational cost.

2. Related to point 1, we introduce the new generalised control-state reachability problem for VASS and show it to be in ptime when restricted to VASS with one counter (1-VASS) (Theorem 10). The same problem with an unrestricted number of counters can be easily shown to be expspace-complete, but its ptime subproblem with one counter is instrumental to get the above-mentioned ∆ P 2 -completeness result. This ptime upper bound for the generalised control-state reachability problem for 1-VASS is partly based on the complexity results for the state-reachability and nontermination problems in VASS with a single counter. As regards the latter problems, [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF] handles the boundedness problem in a way that can be adapted for the nontermination problem and [START_REF] Chatterjee | The cost of exactness in quantitative reachability[END_REF]Section 3.3] actually handles state-reachability for 1-VASS. In Section 3.2, we provide a uniform treatment (see Theorems 7 and 8) while introducting a few minor necessary updates to the proof of [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF]Theorem 3.4]. Hence, we believe that this part of the paper can be considered as self-standing contributions allowing us to design a fine-tuned algorithm to solve the generalised control-state reachability problem restricted to 1-VASS. [START_REF] Laroussinie | Augmenting ATL with strategy contexts[END_REF]. We prove that model-checking RB±ATL is ptime-complete when we reason about a single resource and a single agent. In the paper, this is done in two ways. First, we show the ptime upper bound when the model-checking problem for RB±ATL + is restricted to a single resource, a single agent, and a finite set of linear-time operators (Theorem 15). RB±ATL is then just a special case. The second method shows the ptime upper bound directly by using polynomial-time algorithms for the state-reachability and nontermination problems in VASS with a single counter as well as the ptime lower bound from CTL model-checking (see Section 5.2). Since we show that this setting is tantamount to the Computation Tree Logic CTL with a single resource (Theorem 19), our result means that we can reason about a single resource in CTL too at no extra computational cost.

4. Furthermore, we generalise point 1 by showing that the model-checking problem for RB±ATL + restricted to r resources (for a fixed r) can be solved in exptime (Theorem 13) by reduction to the parity game problem for AVASS [START_REF] Colcombet | Perfect half space games[END_REF]. Remarkably, the number of locations in the target AVASS is exponential in the input size, which makes a substantial difference w.r.t. what is done in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF] for RB±ATL * , where the number of locations is double exponential. Hence, the model-checking problem for RB±ATL + restricted to one resource is pspace-hard (inherited from ATL + [START_REF] Bulling | Verifying agents with memory is harder than it seemed[END_REF][START_REF] Goranko | Game-theoretic semantics for ATL + with applications to model checking[END_REF]) and in exptime. Apart from the complexity results that improve our understanding of fragments of RB±ATL * , we present reductions to the parity game problem for AVASS that can be of interest for their own sake.

Related Work. Resource-aware formalisms have a well-established tradition in mathematical logic, dating back at least to the work on substructural logics [START_REF] Girard | Linear logic[END_REF][START_REF] Engberg | Completeness Results for Linear Logic on Petri Nets[END_REF]35].

Hereafter we focus specifically on the several ATL-like formalisms that have been put forward in recent years, which are characterized by endowing actions with the consumption or production of resources [START_REF] Alechina | State of the art in logics for verification of resource-bounded multi-agent systems[END_REF][START_REF] Bulling | On the (Un-)Decidability of Model-Checking Resource-Bounded Agents[END_REF][START_REF] Della Monica | On a logic for coalitional games with priced-resource agents[END_REF][START_REF] Bulling | How to be both rich and happy: Combining quantitative and qualitative strategic reasoning about multi-player games[END_REF][START_REF] Alechina | Decidable model-checking for a resource logic with production of resources[END_REF][START_REF] Alechina | On the boundary of (un)decidability: Decidable model-checking for a fragment of resource agent logic[END_REF]. In this line of research, a remarkable breakthrough occurred with the design of the logic RB±ATL, with production (+) and consumption (-) of resources, whose model-checking problem was shown decidable in [START_REF] Alechina | Decidable model-checking for a resource logic with production of resources[END_REF]. Subsequently, fragments of RB±ATL have been designed with relatively low complexity (see, e.g., [START_REF] Alechina | Symbolic model checking for one-resource RB+-ATL[END_REF][START_REF] Alechina | Model-checking for resource-bounded ATL with production and consumption of resources[END_REF]). In the same line, [START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF] considers Resource Agent Logic (RAL), which extends ATL to verify properties of systems where agents act under resource constraints. Unlike RB±ATL, in RAL the agents do not necessarily re-equip their resources whenever new strategies are considered and resources are allowed to be updated based on actions taken by agents from the opponent coalition. In [START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF], the authors review existing (un)decidability results for fragments of RAL with unbounded production and consumption of resources, tighten some existing undecidability results, and identify several aspects which affect decidability of model-checking, including the availability of a 'do nothing', or idle action.

Similary, in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF] the authors revisit decidability results for resource-aware logics, with the notable difference of leveraging on decision problems for vector addition systems with states (VASS), in order to establish complexity characterisations of (decidable) modelchecking problems. In particular, they show that the model-checking problem for the logic RB±ATL is 2exptime-complete by using recent results on alternating VASS [START_REF] Courtois | Alternating vector addition systems with states[END_REF][START_REF] Colcombet | Perfect half space games[END_REF]. We refer to Tables 2-4 in Section 2 for a detailed list of the complexity results proved therein. Similarly to [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], in the present contribution we still leverage on VASS, but differently from [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF][START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF] we provide complexity results also for the extension RB±ATL + of RB±ATL. Moreover, our results do not rely on the availability of an idle action, differently from [START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF].

Finally, in [START_REF] Alechina | Symbolic model checking for one-resource RB+-ATL[END_REF] the authors give a symbolic model-checking algorithm for the 1RB±ATL fragment of RB±ATL that allows only one resource type. They evaluate the performance of an implementation of the algorithm on an example problem that can be scaled to large state spaces. Here, we do not tackle the problem of efficient implementation of the decision procedures we provide.

For a thorough discussion of the current state of the art in resource-bounded ATL, we refer to the survey paper [START_REF] Alechina | State of the art in logics for verification of resource-bounded multi-agent systems[END_REF].

Structure of the paper. The rest of the paper is structured as follows. In Section 2 we present the syntax and semantics of resource-bounded alternating-time temporal logic. In particular, we define the logic RB±ATL * and its fragments RB±ATL + and RB±ATL, we outline the state of the art on their model-checking problems, as well as the novel results we prove. In Section 3 we introduce some background notions on vector addition systems with states (VASS), specifically for the case of a single counter. For these 1-VASS, we define the nontermination and generalised reachability problems, which are used to provide a unified framework to solve the model-checking problem for RB±ATL + in Section 4, where we first consider the case of a single agent and a single resource (Section 4.1), and then the case for a fixed number r of resources (Section 4.2). Finally, in Section 5 we present some notable extensions of our results, specifically to a bounded number of temporal operators (Section 5.1) and to the fragment RB±ATL (Section 5.2). In Section 5.3, we provide a comparison with the logic RBTL from [START_REF] Bulling | On the (Un-)Decidability of Model-Checking Resource-Bounded Agents[END_REF][START_REF] Bulling | Expressing properties of resource-bounded systems: The logics RBTL * and RBTL[END_REF]. In short, RBTL can be understood as the variant of RB±ATL using only the full set of agents or the empty set as coalitions. We conclude in Section 6 by pointing to future lines of work.

Previous work by the same authors. This paper is a complete and extended version of the conference articles [START_REF] Belardinelli | Resource-bounded ATL: the quest for tractable fragments[END_REF] and [START_REF] Belardinelli | Reasoning with a bounded number of resources in ATL+[END_REF] by the same authors. However, we added several original contributions. In particular, the results pertaining to point 3 above, about the model-checking problem for RB±ATL + restricted to a single resource, a single agent, and a fixed finite set of linear-time operators, are all new and did not appear in [START_REF] Belardinelli | Resource-bounded ATL: the quest for tractable fragments[END_REF][START_REF] Belardinelli | Reasoning with a bounded number of resources in ATL+[END_REF]. Furthermore, the paper presents full proofs and extensive discussion of results and proof techniques, pointing to possible future extensions and applications.

Resource-Bounded Alternating-time Temporal Logics

The presentation below for resource-bounded alternating-time temporal logics follows closely [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF][START_REF] Belardinelli | Resource-bounded ATL: the quest for tractable fragments[END_REF][START_REF] Belardinelli | Reasoning with a bounded number of resources in ATL+[END_REF]. In the rest of the paper, N (resp. Z) is the set of natural numbers (resp. integers) and for m, m ∈ Z, [m, m ] is the set {j ∈ Z | m ≤ j ≤ m }. For a finite or infinite sequence w ∈ X * ∪ X ω of elements in some given set X, we write w i or w[i] for the (i + 1)-th element of w, i.e., w = w 0 w 1 . . .. For i ≥ 0, w ≤i = w 0 w 1 . . . w i is the prefix of w of length i + 1, while w ≥i = w i w i+1 . . . is the suffix of w starting at position i. The length of a (finite or infinite) sequence w ∈ X ω ∪ X * is denoted as |w|, where |w| = ω for w ∈ X ω .

The logic RB±ATL * and its fragments

To specify the strategic properties of agents in resource-bounded multi-agent systems, we present the logic RB±ATL * as well as its fragments RB±ATL + and RB±ATL, which are resource-aware extensions of the alternating-time temporal logics ATL * , ATL + , and ATL respectively, introduced in [START_REF] Alechina | Decidable model-checking for a resource logic with production of resources[END_REF][START_REF] Alechina | Symbolic model-checking for resource-bounded ATL[END_REF] to explicitly account for the production and consumption of resources by agents. In the rest of the paper, we assume a countably infinite set AP of atomic propositions (or atoms). Given a finite non-empty set Ag of agents and a number r ≥ 1 of resources (often called "resource types" in the literature), we write RB±ATL * (Ag, r) to denote the resource-bounded logic with agents from set Ag and r resources.

Syntax. The models of RB±ATL * (Ag, r) and its fragments are resource-bounded concurrent game structures (see a formal introduction in Definition 3) in which transitions are labelled by tuples of actions of length |Ag|, each agent performing one action. A notion of computation arises naturally as an infinite sequence of consecutive states.

Definition 1 (RB±ATL * ). The state formulae φ and path formulae Ψ in the logic RB±ATL * (Ag, r) are built according to the following BNF grammar:

φ ::= p | ¬φ | φ ∧ φ | A b Ψ Ψ ::= φ | ¬Ψ | Ψ ∧ Ψ | X Ψ | Ψ U Ψ where p ∈ AP, A ⊆ Ag, and b ∈ (N ∪ {ω}) r .
By RB±ATL * (Ag, r) formulae, by default we understand all and only the state formulae.

Similarly to the temporal logic CTL * , the syntax of RB±ATL * (Ag, r) distinguishes state formulae (interpreted on states) from path formulae (interpreted on computations). The main feature of RB±ATL * (Ag, r) are state formulae of the form A b Ψ, where A ⊆ Ag is a coalition (set of agents), Ψ is a path formula defining a property on computations, and b is an initial budget, i.e., a r-tuple over N ∪ {ω}, understood as a quantity for each resource type, where the value ω accounts for an infinite supply of the respective resource. Roughly speaking, A b Ψ is read as "the coalition A of agents has a joint strategy implementable with budget b such that all the computations respecting that strategy satisfy the linear-time property Ψ". The initial budget is relevant as in resource-bounded concurrent game structures, actions come with resource consumption and production. In particular, the operator A b quantifies over all computations such that the resource counters are non-negative provided the initial budget and the cost of actions in the relevant strategy. It is worth noting that a formula A b Ψ is interpreted as a property that alternates one existential quantification (over strategies) and one universal quantification (over computations), similarly to what is done in ATL [START_REF] Alur | Alternating-time temporal logic[END_REF].

The linear-time operators next X and until U from LTL have their standard readings; the propositional connectives ∨, ⇒, and the temporal operators eventually F and always G are introduced as usual. The dual operator

[[A b ]] is introduced as [[A b ]]Ψ def = ¬ A b ¬Ψ (in RB±ATL * (Ag,
r), path formulae are closed under negation, but this does not hold for all its fragments). Now let us introduce the fragments RB±ATL + (Ag, r) and RB±ATL(Ag, r) that are, along the lines of the definition of CTL + and CTL from CTL * . Definition 2 (RB±ATL + and RB±ATL). State formulae in RB±ATL + (Ag, r) are obtained from the BNF grammar for RB±ATL * (Ag, r) by restricting path formulae as follows:

Ψ ::= ¬Ψ | Ψ ∧ Ψ | X φ | φ U φ
Similarly, state formulae in RB±ATL(Ag, r) are obtained from the BNF grammar for the logic RB±ATL * (Ag, r) by restricting path formulae as follows:

Ψ ::= X φ | φ U φ | G φ
Notice that G φ is usually introduced as a shortcut for ¬( U ¬φ) in RB±ATL + , but it has to be assumed as a primitive symbol in RB±ATL.

The logics RB±ATL + (Ag, r) and RB±ATL(Ag, r) introduce increasing restrictions on the form of path formulae Ψ as goals in the scope of strategic operators. In RB±ATL(Ag, r) only simple goals of the form X φ, φ U φ, and G φ are allowed. In RB±ATL + (Ag, r), we can also have Boolean combinations thereof. Finally, RB±ATL * (Ag, r) allows any combination of linear-time operators as temporal goals. We will see that the increased expressivity has an impact on the complexity of the corresponding model-checking problems. We write RB±ATL * (r) to denote the set of formulae in RB±ATL * (Ag, r), for some fixed non-empty set Ag of agents. Similar definitions are used for RB±ATL + (r) and RB±ATL(r).

Semantics. We interpret the formulae in RB±ATL * (and therefore RB±ATL + and RB±ATL) by using resource-bounded concurrent game structures [START_REF] Alechina | Resource-bounded alternating-time temporal logic[END_REF][START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], i.e., concurrent game structures endowed with a weight function that assigns an integer to every action (hereafter understood as a gain).

Definition 3 (RB-CGS).

A resource-bounded concurrent game structure is a tuple M = Ag, r, S, Act, act, wf, δ, L such that • Ag is the finite, non-empty set of agents (by default Ag = [1, k] for some k ≥ 1);

• r ≥ 1 is the number of resources;

• S is a finite, non-empty set of states;

• Act is a finite, non-empty set of actions;

• act : S × Ag → (℘(Act) \ ∅) is the protocol function; • wf : S × Ag × Act → Z r is the (partial) weight function; that is, for s ∈ S, a ∈ Ag,
and a ∈ Act, wf (s, a, a) is defined only when a ∈ act(s, a);

• δ : S × (Ag → Act) → S is the (partial) transition function such that δ is defined for a state s and a joint action f : Ag → Act only if for every agent a ∈ Ag, f (a) ∈ act(s, a);

• L : AP → ℘(S) is the (partial) labelling function.
Intuitively, a resource-bounded CGS describes the interactions of a group Ag of agents, who perform the actions in Act according to the protocol function act. The execution of a joint action f : Ag → Act generates a transition in the system, as specified by the transition function δ. Moreover, on each transition the values of the r resources are updated according to the weights wf of the joint action. Definition 3 excludes the case with no resource types (r = 0) because in this paper we emphasize the use of resources. However, by convention, having zero resource types in RB-CGS corresponds to the standard concurrent game structures from [START_REF] Alur | Alternating-time temporal logic[END_REF]. It is worth noting that in Definition 3 we do not assume the existence of an idle action (with zero weight), which was first introduced in [START_REF] Alechina | Decidable model-checking for a resource logic with production of resources[END_REF][START_REF] Alechina | Model-checking for resource-bounded ATL with production and consumption of resources[END_REF] and it is often advantageous in terms of computational complexity (see, e.g. [START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF][START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]). In this paper we do not rely on the action idle to establish our complexity results, but of course, nothing prevents us from having such a distinguished action in our instances of the model-checking problem. The only exception for which we require the existence of the idle action is in Section 5.2. Indeed, the existence of such an action with no effect on resources allows us to extend computations from any state, which is helpful for solving control-state reachability problems.

An RB-CGS M is finite whenever L is restricted to a finite subset of AP. The size |M | of a finite RB-CGS M is the size of its encoding when integers are encoded in binary and maps and sets are encoded in extension using a reasonably succinct encoding. All the complexity results in the paper are about upper bounds. Using a binary encoding for integers, which is the common practice in computer science, usually requires a bit more efforts than a unary encoding. In this work, conciseness of the binary encoding for integers does not lead to substantial difficulties when proving complexity upper bounds. Now, we provide the necessary notions to interpret our languages on resource-bounded CGS. Given a coalition A ⊆ Ag and a state s ∈ S, a joint action available to A in s is a map f : A → Act such that for every agent a ∈ A, f (a) ∈ act(s, a). The set of all such joint actions is denoted as D A (s). Given joint actions f , g, we write f g if Dom(f ) ⊆ Dom(g), and for every agent a ∈ Dom(f ), g(a) = f (a). For a joint action f ∈ D A (s), out(s, f ) is the set of immediate outcomes:

out(s, f ) def = {δ(s, g) | for some g ∈ D Ag (s), f g}
Further, the weight of a transition from s by f (w.r.t. coalition A) is defined as

wf A (s, f ) def = a∈A wf (s, a, f (a))
A computation λ is a finite or infinite sequence s 0

f0 - → s 1 f1 - → s 2 . . . such that for all 0 ≤ i < |λ| -1 we have s i+1 = δ(s i , f i ).
To provide a formal semantics to the strategic operator A b based on RB-CGS, we need a notion of resource-bounded strategy.

Definition 4 (Strategy). A (memoryful) strategy F A for the coalition A is a map from the set of finite computations to the set of joint actions of A such that

F A (s 0 f0 -→ s 1 . . . s n-1 fn-1 ---→ s n ) ∈ D A (s n ). A computation λ = s 0 f0 - → s 1 f1 - → s 2 . . . respects the strategy F A iff for all i < |λ| -1, s i+1 ∈ out(s i , F A (s 0 f0 - → s 1 . . . s n-1 fi-1 --→ s i )).
A computation λ that respects F A is maximal if it cannot be extended further while respecting F A . Therefore, maximal computations starting in state s and respecting F A are infinite, and we denote the set of all such maximal computations by Comp(s, F A ).

Given a bound b ∈ (N ∪ {ω}) r and a computation λ = s 0 f0 -→ s 1 f1 -→ s 2 . . . in Comp(s, F A ), let the resource availability v i at step i ∈ N be defined as: v 0 = b and for i ≥ 0, v i+1 = wf A (s i , f i ) + v i (assuming n + ω = ω for every n ∈ Z). Then, λ is b-consistent iff for all i ∈ N, we have v i ∈ (N ∪ {ω}) r . A b-strategy F A with respect to s is a strategy such that all the maximal computations in Comp(s, F A ) are b-consistent. In particular, this means that resource quantities are non-negative along the corresponding computations. If b[i] = ω, we actually have an infinite supply of the i-th resource, thus not constraining the behaviour of agents with respect to that particular resource and effectively disregarding what happens about it. Since the resource availability depends only on the agents in coalition A, this is called the proponent restriction condition (see, e.g., [START_REF] Alechina | On the boundary of (un)decidability: Decidable model-checking for a fragment of resource agent logic[END_REF][START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]). This asymmetry between the proponent and the opponent coalitions is particularly helpful to guarantee decidability of the model-checking problem, though resources can be produced or consumed by the proponent coalition. The introduction of such a condition in [START_REF] Alechina | On the boundary of (un)decidability: Decidable model-checking for a fragment of resource agent logic[END_REF] is strongly motivated with the goal of getting decidable model-checking problems.

Definition 5 (Satisfaction). Given a state s ∈ S, an infinite computation λ, an atom p ∈ AP, a state formula φ and a path formula Ψ in RB±ATL * , the satisfaction relation |= is defined as follows:

(M, s) |= p iff s ∈ L(p) (M, s) |= ¬φ iff (M, s) |= φ (M, s) |= φ 1 ∧ φ 2 iff (M, s) |= φ i for i ∈ {1, 2} (M, s) |= A b Ψ iff for some b-strategy F A w.r.t. s, for all computations λ ∈ Comp(s, F A ), (M, λ) |= Ψ (M, λ) |= φ iff (M, λ[0]) |= φ (M, λ) |= ¬Ψ iff (M, λ) |= Ψ (M, λ) |= Ψ 1 ∧ Ψ 2 iff (M, λ) |= Ψ i for i ∈ {1, 2} (M, λ) |= X Ψ iff (M, λ ≥1 ) |= Ψ (M, λ) |= Ψ U Ψ iff
for some i ≥ 0, (M, λ ≥i ) |= Ψ , and for all 0 ≤ j < i, (M, λ ≥j ) |= Ψ Clearly, the alternating-time temporal logics ATL * , ATL + , and ATL can be seen as syntactic fragments of RB±ATL * , RB±ATL + , and RB±ATL respectively. In particular, the unindexed strategic operator A can be expressed as A ω . In order to stick to the definition of the original version of RB±ATL in [START_REF] Alechina | Decidable model-checking for a resource logic with production of resources[END_REF] (see also [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]) -as well as to provide more flexibility to the specification language -we keep the bound ω, but the way to handle it consists in reducing the dimension (i.e., eliminating the components where it appears, as it does not bring any quantitative constraint), which can be easily performed.

Remark. In the case of a single agent, that is, for Ag = {1}, in our languages we only have modalities Ag ]] corresponds to the meaning of the universal (A) and existential (E) path quantifiers in CTL * , where the weights in the RB-CGS are ignored because of the proponent restriction condition. Hence, RB±ATL * ({1}, r) can be thought of as a resource-bounded version of CTL * with r resources. In Section 5.3, we show that RB±ATL * for the single agent case is basically equivalent to a different resource-bounded logic RBTL * introduced in [START_REF] Bulling | Expressing properties of resource-bounded systems: The logics RBTL * and RBTL[END_REF].

We illustrate the formal machinery introduced so far, particularly the single-agent case, with two AI-oriented examples.

Example 1. We consider a scenario in which a rover is exploring an unknown area. At any time the rover can choose between two modes: either it moves around or it recharges its battery through a solar panel, but it cannot do both things at the same time. Moving around consumes one energy unit at every time step, whereas the rover can recharge of one energy unit at a time. Switching between these modes also requires one energy unit.

This simple scenario can be modelled as the resource-bounded CGS M = {rover}, 1, {s 1 , s 2 }, {move, recharge, switch}, act, wf, δ, L depicted in Fig. 1, where in particular:

• act(s 1 , rover) = {move, switch} and act(s 2 , rover) = {recharge, switch}; • wf (s 1 , rover, move) = wf (s 1 , rover, switch) = wf (s 2 , rover, switch) = -1 and wf (s 2 , rover, recharge) = +1;

• δ(s 1 , move) = s 1 , δ(s 1 , switch) = s 2 , δ(s 2 , recharge) = s 2
, and δ(s 2 , switch) = s 1 ;

• AP = {moving} and L(moving) = {s 1 }.

Even in such a simple scenario with a single agent, we can express interesting properties such as "no matter what the rover does, at any time it has a strategy, with an initial budget of b energy units, such that it will eventually be moving". This specification can be expressed as

[[{rover} ω ]] G( {rover} b F moving) (1)
It is worth noting that formula (1) is not in RB±ATL but the next formula is. I.e., it is easy to check that (1) above is logically equivalent to the following formula:

¬ {rover} ω F ¬( {rover} b F moving).
In Section 5.1 and 5.2 we show that specifications such as [START_REF] Alur | Alternating-time temporal logic[END_REF], concerning a single agent and a single resource, can be efficiently verified in ptime.

Here is another example, tailored to illustrate the expressive power of RB±ATL + formulae.

Example 2. We consider a scenario in which two drones, d 1 and d 2 , have to deliver two parcels to addresses (X 1 , Y 1 ) and (X 2 , Y 2 ) on a [-m, m] 2 grid for some m > 0. We assume that they both start from location (0, 0). At any time, each drone can choose between two modes: either it moves in one of the four directions (N, S, E, W) or it recharges its battery through a solar panel (charge), but it cannot do both actions at the same time. Moving around consumes one energy unit at every time step; whereas the drone can recharge one unit at a time. Each drone can carry one parcel at a time, and they can only pick them up from location (0, 0). This scenario can be modelled as a resource-bounded CGS

M = {d 1 , d 2 }, 1, [-m, m] 2 × [-m, m] 2 , {N, S, E, W, charge}, act, wf, δ, L
where in every state s, for i ∈ {1, 2} and D i ∈ {N, S, E, W}:

• act(s, d i ) = {N, S, E, W, charge}; • wf (s, d i , D i ) = -1 and wf (s, d i , charge) = +1;
• δ(((x 1 , y 1 ), (x 2 , y 2 )), (D 1 , D 2 )) = ((x 1 , y 1 ), (x 2 , y 2 )), where (x i , y i ) is obtained from (x i , y i ) by decrementing/incrementing either x i or y i depending on D i . Notice that on the frontier, movement in some directions is assumed to have no effect.

Similarly for δ(((x 1 , y 1 ), (x 2 , y 2 )), (D 1 , charge)) and δ(((x 1 , y 1 ), (x 2 , y 2 )), (charge, D 2 )).

Moreover, δ(s, (charge, charge)) = s. Even in such a simple scenario we can express interesting strategic properties in

• AP = {charge 1 , charge 2 , del 1 , del 2 } and L(del i ) = {(X i , Y i )},
RB±ATL + ({d 1 , d 2 }, 1). Consider a budget b = max{(|X 1 | + |Y 1 |), (|X 2 | + |Y 2 |
)} that allows any drone d to deliver a single parcel to the farthest address. We can check that in location ((0, 0), (0, 0)) the following formulae are true:

1. With budget b, every drone d i , for i ∈ {1, 2}, can deliver parcel 1 and can deliver parcel 2, without charging in the meantime:

{d i } b (¬charge U del 1 ) ∧ {d i } b (¬charge U del 2 ) (2)
2. With budget 2b, neither drone can deliver both parcel 1 and 2, without charging in the meantime (recall that drones have to pick parcels in location (0, 0)):

¬ {d i } 2b ((¬charge U del 1 ) ∧ (¬charge U del 2 )) (3)
3. Nonetheless, with budget 2b, the drones can cooperate to deliver both parcels, without charging in the meantime:

{d 1 , d 2 } 2b ((¬charge U del 1 ) ∧ (¬charge U del 2 )) (4)
Notice that formula (2) belongs to RB±ATL, but we make use of Boolean combinations of goals and the expressivity of RB±ATL + to formalize (3) and (4).

The model-checking problem: state of the art

Hereafter L is a (possibly trivial) fragment of RB±ATL * , typically RB±ATL, RB±ATL + or RB±ATL * , or some of its restrictions. In the sequel, we consider the following decision problem.

Definition 6 (Model-checking). Let M be a finite RB-CGS with Ag = [1, k] and r resources for some k, r ≥ 1, and let s be a state in M . Let φ be a formula in a logic L built over Ag and r resources. The model-checking problem amounts to decide whether (M, s) |= φ.

Given a logic L, we write MC(L) to denote the corresponding model-checking problem. Below, we summarize known complexity results for subproblems of MC(L), when L is either RB±ATL * , RB±ATL + , or RB±ATL, obtained by bounding the number k of agents and r of resources. We also identify the contributions made in this paper.

r\|Ag| ∞ ≥ 2 1 ∞ 2exptime-c. [

Complexity of MC(RB±ATL) and fragments

In Figure 2, we summarize the main complexity results available in the literature for RB±ATL(Ag, r). The ptime upper bound in boldface was originally presented by the authors in [START_REF] Belardinelli | Resource-bounded ATL: the quest for tractable fragments[END_REF], herein we provide the full proofs (see Sections 4.2, 5.2 and 5.2). It is worth noting that all the results are known to hold in the presence of the release operator R instead of the always operator G, except for the pspace upper bound from [19, Th. 2] (for which further investigations would be needed). The symbol '∞' corresponds to the case when either r or |Ag| is unbounded. By contrast, '≥ n' means that the number of either resources or agents is fixed, but greater than n. Moreover, some of the results assume the existence of an idle action (roughly, it has no effect on resources, but it can be choosen anytime by any agent). This assumption does not impact on the lower bounds, but it can make a difference for the upper bounds. We write '( †)' to indicate that the corresponding result is proved under the assumption of the idle action in the cited work (though further investigations might show that even without the idle action, the complexity upper bound is preserved).

We now discuss briefly the main results in Figure 2. For an unbounded number of resources and at least two agents, the model-checking problem is known to be 2exptimecomplete. This result follows from Theorem 2 (upper bound) and Theorem 3 (lower bound) in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]. When restricted to a single agent, the same problem becomes expspacecomplete [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Th. 4].

For a fixed number of resources greater or equal than four and at least two agents, the model-checking problem is exptime-complete. The upper bound follows from [12, Cor. 1], while the lower bound derives from the complexity of the control-state reachability problem for alternating VASS [START_REF] Courtois | Alternating vector addition systems with states[END_REF], which can be simulated by using at least two agents only [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Th. 3]. Further, for a fixed amount of resources greater or equal than two, and at least two agents, the model-checking problem is in exptime [12, Cor. 1]. In the case of a single agent, the same problem is in pspace [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Cor. 2]. Moreover, it is pspace-hard in both cases, as we can reduce to it the control-state reachability problem for 2-VASS, which is pspace-complete [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF]. It is worth noting that in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], all the RB-CGS are assumed to admit an idle action.

Finally, in the case of a single resource, the problem is known to be in pspace in general [START_REF] Alechina | Model-checking for resource-bounded ATL with production and consumption of resources[END_REF]Th. 2]. We observe that the case of a single resource can also capture situations in which r > 1 resources can be converted into a unique resource (e.g., money), possibly with different rates. Under the extra restriction of a single agent, model-checking is in ptime, which is our theoretical contribution in Section 5.1 based on results in Section 4.2 (see also Section 5.2).

r\|Ag| ∞ ≥ 2 1 ∞ 2exptime-c. [
It is therefore ptime-complete as the CTL model-checking problem is already ptimehard (see, e.g. [START_REF] Schnoebelen | The complexity of temporal logic model checking[END_REF][START_REF] Demri | Temporal Logics in Computer Science[END_REF]). The characterisation of the complexity for one resource and at least two agents is still open: currently, neither the proof of the ptime upper bound in Section 5.2, nor the pspace-hardness results from [START_REF] Jančar | A note on emptiness for alternating finite automata with a one-letter alphabet[END_REF] and [START_REF] Figueira | Polynomial-space completeness of reachability for succinct branching VASS in dimension one[END_REF]Sect. 5] could be advantageously used to close this complexity gap.

Complexity of MC(RB±ATL + ) and fragments

As regards RB±ATL + (see Figure 3), for an unbounded number of resources we have the same complexity results as for RB±ATL: 2exptime-completeness for at least two agents, and expspace-completeness in the single-agent case. Also, for a single agent, the problem is pspace-complete when considering at least two resources, just like RB±ATL. In this paper we provide the full proof that for single-agent, single-resource RB±ATL + , the model-checking problem is ∆ P 2 -complete. This result was originally stated in [START_REF] Belardinelli | Reasoning with a bounded number of resources in ATL+[END_REF]. In the case of at least two agents, the model-checking problem is here proved to be in exptime for a bounded number of resources. This result gives a tight complexity bound in the case of at least four resources, which is already known to be exptime-hard [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Cor. 1]. In all other cases there are no matching lower bounds, the problem is only known to be pspace-hard from ATL + [27].

Complexity of MC(RB±ATL * ) and fragments

Unlike RB±ATL and RB±ATL + , tight complexity bounds are known for all variations of RB±ATL * on the number of agents and resources (see Figure 4). For at least two agents, the model-checking problem is 2exptime-complete. The upper bound comes from [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Th. 7], whereas the lower bound follows from the 2exptime-hardness of ATL * , which is proved by using two agents only [START_REF] Alur | Alternating-time temporal logic[END_REF]. On the other hand, the problem restricted to a single agent becomes expspace-complete for an unbounded number of resources [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Th. 8]; while for a bounded number r, model-checking RB±ATL * ({1}, r) is pspacecomplete: the lower bound follows immediately from the pspace-hardness of the modelchecking problem for CTL * ; as for the upper bound, we derive it from the fact that model-checking RBTL * is in pspace [12, Cor. 2] and Theorem 19.

Decision Problems on 1-VASS

In this section, we present several decision problems for vector addition systems with states restricted to one counter (1-VASS) and we establish their ptime upper bound. These results are most relevant to analyse the complexity of the model-checking problems for RB±ATL and RB±ATL + restricted to a single resource and a single agent. Indeed, the restriction to a single agent entails that the strategy modalities state the existence of specific runs in 1-VASS. After recalling the main notions about VASS and 1-VASS, we present the nontermination and control-state reachability problems, and we introduce the new generalised control-state reachability problem. In particular, we prove that MC(RB±ATL + ({1}, 1)) is ∆ P 2 -complete (see Section 4.1) by using instances of this new generalised reachability problem on 1-VASS. We show that when restricted to a single counter, the new generalised control-state reachability problem can be solved in ptime, thus generalising Theorems 3.3 and 3.5 from [START_REF] Belardinelli | Resource-bounded ATL: the quest for tractable fragments[END_REF]. It is worth noting that the nontermination and control-state reachability problems are actually subproblems of the generalised problem. Nevertheless, their study and introduction have a two-fold motivation. Solving such problems is useful to solve the generalised problem and in particular to obtain the ptime upper bound when restricted to 1-VASS. Moreover, in Section 5.2, we present a polynomial-time algorithm for MC(RB±ATL({1}, 1)) based on instances of the nontermination and control-state reachability problems, which we believe it is promising to obtain an efficient implementation, besides the fact that we are able to provide a self-contained version of the algorithm. Still, computational improvements are expected by taking advantage of the recent algorithmic results presented in [START_REF] Almagor | Coverability in 1-VASS with Disequality Tests[END_REF].

Background on Vector Addition Systems with States

A vector addition system with states (VASS) [START_REF] Karp | Parallel program schemata[END_REF] is a structure V = Q, r, R , where Q is a finite set of locations (a.k.a., control states), r ∈ N is its dimension (also understood as its number of counters), R is a finite set of transitions in

Q × Z r × Q. A configuration in a VASS V is a pair q, x ∈ Q × N r .
Note that the counter values are required to be non-negative. Given configurations q, x , q , x and a transition t = q u -→ q , we write q, x t -→ q , x whenever x = u + x. A run is defined as a sequence ρ = q 0 , x 0

t1 - → q 1 , x 1 t2 - → q 2 , x 2 • • • of configurations, where q 0 , x 0 is the initial configuration. A run ρ is simple if no control state appears twice. A finite path is a sequence of contiguous transitions t 1 . . . t k .
It is worth stressing that paths do not take into account counter's values associated with transitions, while runs do. A simple path is a finite sequence of contiguous transitions t 1 . . . t k such that no control state occurs more than once. Hence, every finite run has an induced path but not every configuration q, x can trigger a path leading to a run because the counter values have to be non-negative A simple loop is a sequence of contiguous transitions t 1 . . . t k such that the first control state of t 1 is equal to the second control state of t k (and it occurs nowhere else) and no other control state occurs more than once. An r-VASS is a VASS with r ≥ 1 counters. By convention, a 0-VASS is a finite directed graph. In Figure 5, we present a graphical representation of a VASS with a single counter. The value on each edge corresponds to the update tuple/value.

VASS are known to be equivalent to Petri nets for many behavioural properties, which is particularly interesting, as Petri nets are ubiquitous computational models to handle concurrency. A famous result states that the reachability problem for Petri nets (and therefore for VASS) is decidable [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF][START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invari-ants[END_REF]. It has been the subject of the book [START_REF] Reutenauer | The mathematics of Petri nets[END_REF] and its original proof requires many non-trivial steps involving graph theory, logic, and the theory of well-quasi-orderings. Nevertheless, the exact complexity of the reachability problem was open for decades: we know it is expspace-hard from [START_REF] Lipton | The reachability problem requires exponential space[END_REF], but nonelementarity has been shown only recently [START_REF] Czerwinski | The reachability problem for Petri nets is not elementary[END_REF]. In this paper, we mainly deal with reachability questions for 1-VASS. So, the decision problems we consider are much more manageable than the general case with an arbitrary number of counters.

Nontermination and control-state reachability for 1-VASS

In order to show that the model-checking problem for the logic RB±ATL({1}, 1) is ptime-complete (the lower bound is inherited from ptime-hardness of CTL modelchecking, see e.g. [START_REF] Schnoebelen | The complexity of temporal logic model checking[END_REF][START_REF] Demri | Temporal Logics in Computer Science[END_REF]), we establish that two well-known decision problems on vector addition systems with states (VASS), when restricted to a single counter, can be solved in polynomial time. We provide formal proofs below as it will be also useful to design algorithms, see Section 5.2. Besides, an energy problem equivalent to CREACH(1-VASS) introduced below is shown in ptime in [START_REF] Chatterjee | The cost of exactness in quantitative reachability[END_REF]. We begin by presenting two standard decision problems on VASS that play a crucial role in solving the model-checking problem for RB±ATL({1}, 1) and RB±ATL + ({1}, 1).

Control-state reachability problem CREACH(VASS):

Input: a VASS V , a configuration q 0 , x 0 , and a control state q f . Question: is there a finite run with initial configuration q 0 , x 0 and with final configuration with state q f ? Nontermination problem NONTER(VASS):

Input: a VASS V and a configuration q 0 , x 0 .

Question: is there an infinite run with initial configuration q 0 , x 0 ?

In order to solve these problems, we need a few more definitions. In a 1-VASS, a simple loop is positive if the cumulated effect is positive. Given a run ρ = q 0 , x 0 , . . . , q k , x k , . . . and α ≥ 0, we write ρ +α to denote the sequence q 0 , x 0 + α , . . . , q k , x k + α , . . .. If ρ is a run, the sequence ρ +α is also a run (it is important to note that VASS have no zero-tests). The following lemma provides a characterisation of runs ending in a distinguished final state for 1-VASS. Lemma 1. Let V be an 1-VASS, q 0 , x 0 an initial configuration, and q f a location. There is a finite run from q 0 , x 0 to the configuration q f , x f , for some x f ≥ 0, iff (1) either q 0 = q f , or 2. there is a simple run q 0 , x 0 , . . . , q k , x k with k > 0 and q k = q f ; or

q 0 q 1 q 2 q 3 q 4 q 5 q f q 6 q 7 +3 +4 -8 -7 -3 -2 100 +1 0 +5 -1
Witness runs and path for (V , q 0 , 7 , q f ):

initial run: q 0 , 7 , q 2 , 11 , q 3 , 4 "> 0 loop": q 3 , 4 , q 5 , 1 , q 4 , 6 , q 3 , 5 final path: 3. we have that (a) there is a simple run q 0 , x 0 , . . . , q n , x n , (b) there is a positive simple loop t 1 . . . t β such that q n , x n t1...t β ---→ q n , x n + α is a run (α > 0), (c) there is a simple path starting at q n and ending at q f . Note that in Lemma 1(3), without loss of generality, we can asssume that n+β ≤ |Q|. As an illustration of Lemma 1(3), Figure 5 presents a 1-VASS V , and witness runs and path for the positive instance (V, q 0 , 7 , q f ) of CREACH(1-VASS). By contrast, the configuration q 0 , 5 cannot reach q f . Proof. First, it is not difficult to check that if either (1), ( 2) or (3) holds, then there is a finite run from q 0 , x 0 to a configuration q f , x f , for some x f ≥ 0. By way of example, firing the strictly positive simple loop at least |Q| × max{|u| : q u -→ q is a transition} times, allows us to pursue the run following the path from q n to q f . Conversely, let us suppose that ρ = q 0 , x 0 , . . . , q k , x k is a run with q k = q f . If q 0 = q f , then the witness run can be reduced to q 0 , x 0 . Otherwise, either ρ is a simple run and condition (2) holds, or there are 0 ≤ i < j ≤ k such that q i = q j . In case x i ≥ x j , the subrun q i , x i , . . . , q j , x j can be removed from ρ while leading to a run reaching q f . Typically, the suffix subrun q i , x i , . . . , q j , x j , . . . , q k , x k with ρ † = q j , x j , . . . , q k , x k is replaced by ρ +α † for α = x i -x j . Such a transformation can be performed as soon as the subruns correspond to the application of simple loops with negative effect. Hence, without loss of generality, we can assume that ρ has no loop with negative effect.

q 3 -3 -→ q 5 -2 100 ---→ q f
If ρ is not a simple run, there are 0 ≤ I < J ≤ |Q| such that q I = q J and x I < x J . We assume that I is minimal and we pick then a minimal J. Consequently, (a) there is a simple run q 0 , x 0 , . . . , q I , x I ;

(b) there is a strictly positive simple loop t I . . . t J-1 such that q I , x

I t I ...t J-1 ----→ q I , x I + (x J -x I ) ;
(c) there is a path from q J to q k = q f such that q J , x J , . . . , q k , x k is a run. Indeed,

suppose that q J , x J t J •••t k-1 ----→ q k , x k . Let t 1 • • • t l be the path obtained from t J • • • t k-1
by removing simple loops as much as possible. So, t 1 • • • t l is a simple path from q J to q k . As a result, condition (3) is satisfied and the lemma holds. The characterisation in Lemma 1 can be turned into an algorithm running in polynomial time that is used as a routine in the algorithm presented in Section 5.2.

Theorem 7. The problem CREACH(1-VASS) is in ptime.

Proof. Let V be an 1-VASS, q 0 , x 0 an initial configuration, and q f a location. If q 0 = q f , we are done. Otherwise, define values maxval i q for i ∈ [0, |Q|] and q ∈ Q such that if there is a run q 0 , x 0 , . . . , q j , x j with q j = q and j ≤ i, then the maximal value x j among all these runs is precisely maxval i q . When there is no such run, by convention maxval i q = -∞. Similar values have been considered to solve the boundedness problem for 1-VASS in [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF]. Note also that [START_REF] Chatterjee | The cost of exactness in quantitative reachability[END_REF]Section 3.3] shows that an energy problem equivalent to CREACH(1-VASS) can be solved in ptime by using a similar approach, but with slightly different objects. Let us compute the values maxval i q :

• maxval 0 q0 def = x 0 and maxval 0 q def = -∞ for all q = q 0 .

• For all q and i + 1

∈ [1, |Q|], maxval i+1 q def = max(maxval i q , {maxval i q + u ∈ N | q u - → q is a transition}).
The values maxval i q can be computed in polynomial time in the size of V (the number |Q| of locations being an essential parameter as well as the maximal absolute value |u| from updates -integers being written in binary). One can show that maxval i q is indeed the maximal value as specified above. The proof is by induction on i. The base case for i = 0 is obvious and for the induction step, suppose that for all j ≤ i and q ∈ Q maxval j q is the maximal counter value reaching q from q 0 , x 0 in at most j steps. Let us characterize the value maxval i+1 q , which is either the maximal value reached in at most i steps (i.e., equal to maxval i q by IH), or it is reached in exactly i + 1 steps and is therefore a value of the form maxval i q + u with some transition q u -→ q. This is precisely the way maxval i+1 q is computed above. Given q ∈ Q, let C q be the condition: there are a simple run q 0 , x 0 , . . . , q n , x n with q n = q, and a positive simple loop t 1 . . . t β such that q, x n t1...t β ---→ q, x n +α is a run with α > 0, β > 0 and n + β ≤ |Q|. Note that (3) from Lemma 1 is equivalent to the existence of some q ∈ Q such that C q holds and there is a simple path from q to q f . Moreover, observe that maxval

|Q| q f = -∞ implies (2) or (3) and that (2) implies maxval |Q| q f = -∞.
One can show that C q is equivalent to there being I < J ≤ |Q| such that: (a) maxval I q = -∞.

(b) maxval I q < maxval J q and auxval 0 q < auxval J-I q , where the values auxval i q (i ∈ [0, J -I], q ∈ Q) are defined as follows (similarly to what is done for maxval j q ):

auxval 0 q def = maxval I q and auxval 0 q def = -∞ for all q = q.

-For all q and i + 1 ∈ [1, J -I],

auxval i+1 q def = max(auxval i q , {auxval i q + u ∈ N | q u - → q is a transition}).
Consequently, C q can be checked in polynomial time in the size of V . Hence there is a finite run from q 0 , x 0 to the configuration q f , x f , for some x f ≥ 0 iff either q f = q 0 or maxval |Q| q f = -∞ or there is q ∈ Q such that C q holds and there is a simple path from q to q f . Obviously, maxval |Q| q f = -∞ can be checked in ptime, for each q ∈ Q, C q can be checked in ptime too with the above characterisation. Finally, existence of a path from q to q f is an instance of the standard graph reachability problem GAP that is in nlogspace. So, CREACH(1-VASS) is in ptime.

Remark. The values auxval i q in the proof of Theorem 7 are necessary to guarantee that the values maxval I q and maxval J q are obtained following a common subrun until reaching the configuration q, maxval I q . In the proof of [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF]Theorem 3.4] for solving the boundedness problem for 1-VASS in ptime, a similar argument was needed but was missing. Here, we fix that result too with the help of the values auxval i q . Now, let us turn to the characterisation of runs and paths witnessing nontermination.

Lemma 2. Let V be an 1-VASS and q 0 , x 0 an initial configuration. There is an infinite run starting at q 0 , x 0 iff 1. there is a simple run q 0 , x 0 , . . . , q n , x n ; and 2. there is a non-negative simple loop t

1 . . . t k such that q n , x n t1...t k ---→ q n , x n + α is a run (α ≥ 0).
Proof. Clearly, the satisfaction of the two conditions implies that there is an infinite run starting at q 0 , x 0 : just consider the run generated by (t 1 . . . t k ) ω from the configuration q n , x n . Let us prove the other direction, similarly to what is done in the proof of Lemma 1. Suppose that ρ = q 0 , x 0 , . . . , q k , x k , . . . is an infinite run. Without loss of generality, we can assume that ρ has no simple loop with negative effect. Unless (1) and (2) hold, there are n ≥ 0 and q ∈ Q such that q n = q, {i ∈ N | q i = q} is infinite and q 0 , x 0 , . . . , q n , x n is a simple run. Consider some J > I such that q J = q I = q (such indices I and J necessarily exist). Obviously, there is a non-negative simple loop t I . . . t J-1 such that q I , x I t I ...t J-1 ----→ q J , x J is a run. Hence, both conditions in the statement of the lemma hold.

Once more, the characterisation in Lemma 2 can be turned into an algorithm to check nontermination, running in polynomial time. Note also that in Lemma 2, without loss of generality, we can asssume that n + k ≤ |Q|.

Theorem 8. The problem NONTER(1-VASS) is in ptime.

The proof has similarities with the proof of Theorem 7 (it may even sound a bit simpler), but there are a few subtle differences described below.

Proof. Let V be an 1-VASS and q 0 , x 0 an initial configuration. Define the values maxval i q for i ∈ [0, |Q|] and q ∈ Q such that if there is a run q 0 , x 0 , . . . , q i , x i with q i = q (with i transitions), then the maximal value x i among all these runs is precisely maxval i q . Note that these values are not the same as those from the proof of Theorem 7 as we consider runs of length exactly i. When there is no such run, by convention maxval i q = -∞.

• maxval 0 q0 def = x 0 and maxval 0 q def = -∞ for all q = q 0 .

• For all q and i + 1 ∈ [1, |Q|],

maxval i+1 q def = max({maxval i q + u ∈ N | q u - → q is a transition, maxval i q = -∞}).
By convention, the maximal value of the empty set is -∞.

All the values maxval i q can be computed in polynomial time in the size of V . One can show that maxval i q is the maximal value as specified above. Finally, the characterisation in Lemma 2 is equivalent to: there are q ∈ Q and I < J ≤ |Q| such that maxval I q = -∞ and maxval I q ≤ maxval J q (this time, we do not require strictness, as in the proof of Theorem 7) and auxval 0 q ≤ auxval J-I q , where the values auxval i q (i ∈ [0, J -I], q ∈ Q) are defined as

• auxval 0 q def = maxval I
q and auxval 0 q def = -∞ for all q = q;

• for all q and i + 1 ∈ [1, J -I],

auxval i+1 q def = max{auxval j q + u ∈ N | j ≤ i, q u - → q is a transition}.
All conditions can be checked in polynomial time and therefore the nontermination problem for 1-VASS is in ptime.

More about computational complexity. Though we have shown that both problems restricted to 1-VASS are in ptime, the control-state reachability problem for VASS is expspace-complete in general [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. Despite the fact that the control-state reachability problem is a subproblem of the covering problem that has been quite studied, including variants (see, e.g., [START_REF] Atig | On Yen's path logic for Petri nets[END_REF][START_REF] Blockelet | Model-checking coverability graphs of vector addition systems[END_REF][START_REF] Demri | On selective unboundedness of VASS[END_REF]), [32, Section 3.3] handles the state-reachability problem for 1-VASS in ptime and the uniform treatment we provided for control-state reachability and nontermination problems are the building blocks to design a tailor-made algorithm to solve the generalised control-state reachability problem restricted to 1-VASS. Above, we provided formal arguments for tractability by appropriately tuning and correcting the proof technique dedicated to the boundedness problem for 1-VASS from [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF]. Note also that in [START_REF] Göller | A polynomial-time algorithm for reachability in branching VASS in dimension one[END_REF], the updates in the branching VASS (BVASS) are restricted to the set {-1, 0, +1} (see [START_REF] Göller | A polynomial-time algorithm for reachability in branching VASS in dimension one[END_REF]Def. 1]). Therefore the upper bound in [START_REF] Göller | A polynomial-time algorithm for reachability in branching VASS in dimension one[END_REF] does not extend to our present case where updates are arbitrary integers encoded in binary. When updates are arbitrary integers encoded in binary (as done herein), the relevant problems for 1-BVASS are known to be pspace-complete [START_REF] Figueira | Polynomial-space completeness of reachability for succinct branching VASS in dimension one[END_REF]. In the recent paper [START_REF] Almagor | Coverability in 1-VASS with Disequality Tests[END_REF], new results about 1-VASS and extensions have been shown. For instance, the control-state reachability problem for 1-VASS is shown in NC (subclass of ptime made of problems that can be solved in polylogarithmic parallel time), which is an improvement with respect to ptime. Similarly, this problem for 1-VASS augmented with disequality tests is shown in ptime [START_REF] Almagor | Coverability in 1-VASS with Disequality Tests[END_REF]. The algorithm leading to the NC upper bound might be helpful to boost further the algorithm provided in Section 5.2.

Generalised control-state reachability for 1-VASS

Now, we present a new decision problem on VASS that plays a crucial role in deciding the model-checking problem for RB±ATL + ({1}, 1). Before doing so, let us recall some helpful property about MC(RB±ATL + ({1}, 1)): verifying (M, s) |= {1} b Ψ with a single agent in M , amounts to check the existence of an infinite computation λ starting from s, with initial budget b ∈ N, satisfying Ψ. This latter requirement can be reformulated using the 1-VASS that can be constructed from M . Assuming that Ψ is a Boolean formula in negation normal form (NNF) built over atoms of the form X p or p U q, the satisfaction of Ψ on λ amounts to guess which atomic formulae in Ψ hold, and then to check that the guess is correct. As ¬(p U q) is logically equivalent to G ¬q ∨(¬q U ¬p∧¬q), ¬ X p is logically equivalent to X ¬p, and X and G distributes over ∧, guessing which atomic formulae in Ψ hold amounts to guess a conjunction of the form

X C 0 ∧ G C 0 ∧ (C 1 U C 1 ) ∧ • • • ∧ (C n U C n )
for some n ∈ N, where the C i 's and C j 's are arbitrary conjunctions of literals. The conjunct X C 0 can be checked at the first step, and handling G C 0 can be performed by restricting the model to states satisfying C 0 . The satisfaction of the atomic path formulae from the above conjunction (modulo the logical equivalences cited above) would make Ψ true propositionally. More precisely, let us define a natural satisfaction relation.

X |= C U C iff C U C ∈ X X |= X C iff X C ∈ X X |= G C iff G C ∈ X X |= Ψ 1 ∨ Ψ 2 iff X |= Ψ 1 or X |= Ψ 2 X |= Ψ 1 ∧ Ψ 2 iff X |= Ψ 1 and X |= Ψ 2
Indeed, Φ∈X Φ ⇒ Ψ is valid, whenever X |= Ψ. So, assuming that X |= Ψ, we can write Φ∈X Φ as a conjunction of the form

X C 0 ∧ G C 0 ∧ (C 1 U C 1 ) ∧ • • • ∧ (C n U C n ) since (X C ∧ X C ) ⇔ X(C ∧ C ) and (G C ∧ G C ) ⇔ G(C ∧ C ) are valid.
This clarification done, let us notice that the existence of an infinite computation λ starting from s, with initial budget b ∈ N, satisfying the conjunction is equivalent to the existence of an infinite run with positions satisfying C 1 , . . . , C n , while also imposing constraints on the satisfaction of the C i 's.

There might be less than n distinct distinguished positions, in which case some witness position may satisfy two distinct C i and C j . Similarly, the ordering of positions satisfying respectively C 1 , . . . , C n may not coincide with the ordering C 1 , . . . , C n . The definition of GREACH(VASS) below is designed based on these observations. Generalised control-state reachability problem GREACH(VASS):

Input: a VASS V , a configuration q 0 , x 0 , a sequence X 1 , h 1 , . . . , X α , h α for some α ≥ 0 such that X 1 ⊆ • • • ⊆ X α ⊆ Q and {h 1 , . . . , h α } ⊆ Q.
We also assume that |{q 0 } ∪ {h 1 , . . . , h α }| = α + 1.

Question: is there an infinite run q 0 , x 0 -→ q

1 , x 1 -→ q 2 , x 2 • • • with indices 0 < i 1 < i 2 < • • • < i α such that for all j ∈ [1, α], q ij = h j and {q k | k < i j } ⊆ X j ?
The condition |{q 0 } ∪ {h 1 , . . . , h α }| = α + 1 could be removed leading also to a ptime problem. However, it is included in our definition of GREACH(VASS) because, not only it simplifies technical developments, but more importantly, it is exactly what is needed in the proof of Theorem 11.

Here is an illustration of the witness run for α = 2.

{q0,...,qi 1 -1}⊆X1

q 0 , x 0 • • • q i1-1 , x i1-1 - → q i1 , x i1 • • • q i2-1 , x i2-1 {q0,...,qi 2 -1 }⊆X2 and X1⊆X2 - → q i2 , x i2 - → • • •
When α = 0, the question is about the existence of an infinite run from q 0 , x 0 , which can be solved in ptime for r = 1 by Theorem 8. Similarly, GREACH(VASS) restricted to 0-VASS (i.e., GREACH(0-VASS)) is nlogspace-complete as the Graph Accessibility Problem (GAP) can be reduced to it and the nlogspace upper bound can be established by showing that a positive instance requires the existence of a path of length at most |Q| × (α + 2) whose constraints can be checked on-the-fly in nlogspace.

Lemma 3. GREACH(0-VASS) is nlogspace-complete.
Proof. An instance of GREACH(0-VASS) takes as input a finite graph

V = Q, R with R ⊆ Q × Q, q 0 ∈ Q, a sequence X 1 , h 1 , . . . , X α , h α for some α ≥ 0 such that X 1 ⊆ • • • ⊆ X α ⊆ Q and {h 1 , . . . , h α } ⊆ Q. The instance is positive iff there is an infinite path q 0 - → q 1 - → q 2 - → • • • with indices 0 < i 1 < i 2 < • • • < i α such that for all j ∈ [1, α], q ij = h j and {q k | k < i j } ⊆ X j .
The existence of such an infinite path is actually equivalent to the existence of a finite path q

0 - → q 1 - → q 2 - → • • • - → q N , with indices 0 = i 0 < i 1 < i 2 < • • • < i α < N such that for all j ∈ [1, α], q ij = h j and {q k | k < i j } ⊆ X j with the following additional properties: 1. For j ∈ [0, α -1], q ij - → • • • - → q ij+1 is a simple path. 2. For some β > i α , q iα - → • • • - → q β is a simple path and q β - → • • • - → q N is a simple loop (whence, q N = q β ).
Consequently, N can be bounded by (α + 2)|Q|. Solving GREACH(0-VASS) requires to guess a path of length at most (α + 2)|Q| and one can check on-the-fly that it satisfies the relevant properties, whence the nlogspace upper bound. nlogspace-hardness is by a straightforward reduction from the Graph Accessibility Problem (GAP).

Unlike 0-VASS, the addition of counters forbids a similar reduction of an instance of GREACH(VASS) to reachability questions on finite graphs.

Let V , q 0 , x 0 and X 1 , h 1 , . . . , X α , h α be an instance of GREACH(1-VASS). When α > 0, one can show that the instance is positive iff either (A) or (B) below holds.

Before presenting conditions (A) and (B), let us introduce some useful notation. Given an 1-VASS

V = Q, r, R and Q ⊆ Q, we write V Q to denote the 1-VASS Q , r, R such that V Q is the restriction of V to Q , i.e., R def = {q u - → q ∈ R | q, q ∈ Q }.
Here are conditions (A) and (B).

(A) The following conditions hold:

(a) For all N ≥ 0, there is a run q 0 , z 0 • • • q n , z n with q 0 , z 0 = q 0 , x 0 , q n = h 1 , z n ≥ N , and {q 0 , . . . ,

q n-1 } ⊆ X 1 . (b) V , h 1 and X 2 , h 2 , . . . , X α , h α is a positive instance of GREACH(0-VASS)
where V is the directed graph underlying V (integers on transitions are simply removed). (c) There is a simple path from h α to some location q and there is a simple loop from q with a non-negative cumulated effect.

(B) (a) above does not hold, and there is a simple run q 0 , x 0 , . . . , q k , x k in V X1∪{h1} with q k = h 1 and V , h 1 , x max and X 2 , h 2 , . . . , X α , h α is a positive instance of GREACH(1-VASS) with x max the maximal counter value for reaching h 1 in V X1∪{h1} among all the simple runs from q 0 , x 0 .

We briefly explain why the characterisation is correct (details follow) and leads to a ptime upper bound. If (a) holds, one can reach the control state h 1 with a counter value as large as we want. The constraints in (b) on the subsequence X 2 , h 2 , . . . , X α , h α induce reachability questions in the underlying directed graph V . Similarly, the contraints in (c) express two simple reachability properties including the existence of a loop with non-negative cumulated effect. Otherwise, if (a) does not hold, the instance is positive only if there is a run ρ = q 0 , x 0 , . . . , q k , x k in V X1∪{h1} with q k = h 1 , and V , h 1 , x k and X 2 , h 2 , . . . , X α , h α is a positive instance of GREACH(1-VASS). However, if not (a), we can assume that ρ is a simple run and the best we can do is to pick x k equal to the maximal counter value for reaching h 1 among all the simple runs from q 0 , x 0 visiting only states in X 1 . Checking (a), (b), and (c) can be done in ptime (see Section 3.2). Similarly, computing x max in (B) can be done in ptime too.

Let us recapitulate about complexity. As GREACH(0-VASS)) is in nlogspace, checking (A) can be done in ptime. For checking (B), if (a) does not hold, then the computation of x max can be done in polynomial time. A recursive call to an instance of GREACH(1-VASS) with a sequence strictly smaller allows us to get forthcoming Theorem 10.

Lemma 4. Let V , q 0 , x 0 and X 1 , h 1 , . . . , X α , h α be an instance of GREACH(1-VASS) with α > 0. It is a positive instance iff either (A) or (B) holds.

Proof. Let V , q 0 , x 0 and X 1 , h 1 , . . . , X α , h α be an instance of GREACH(1-VASS) with α > 0. We show the following properties. (I) Assume that (A) holds. By the satisfaction of (b) and (c), there is a path in V (i.e., the underlying finite graph of V ), say q 0 -→ q 1 -→ q 2 -→ • • • -→ q L such that q 0 = h 1 and there are indices 0

< i 2 < • • • < i α with for all j ∈ [2, α], q ij = h j and {q k | k < i j } ⊆ X j . Moreover, for some β > i α , q iα - → • • • -→ q β is a sim- ple path, q β - → • • • - → q L is a simple loop, with non-negative effect if read from V . If q 0 - → q 1 - → q 2 - → • • • - → q β corresponds to the path t 1 • • • t β and q β - → • • • - → q L cor- responds to the simple loop t β+1 • • • t L , the ω-sequence t 1 • • • t β • (t β+1 • • • t L ) ω can lead (in V ) to an infinite run from location h 2 whenever the initial counter value is greater than ||R|| × (α + 2)|Q|, for ||R|| def = max{|u| : q u - → q ∈ R}. Indeed, once the sequence of transitions t 1 • • • t β • t β+1 • • • t L can be fired from some initial configuration h 1 , n , the non-negative effect of q β - → • • • - → q L allows
us to visit the loop infinitely. Having n at least equal to ||R|| × (α + 2)|Q| allows us to be on the safe side (to maintain the counter value non-negative), as each transition in

t 1 • • • t β • t β+1 • • • t L can
decrement the counter by at most ||R|| and L ≤ (α + 2)|Q|. The satisfaction of (a) insures that location h 1 can be reached from q 0 , x 0 with a counter value greater than ||R|| × (α + 2)|Q| while preserving the constraints on X 1 . The concatenation of the finite subrun leading to h 1 , z (thanks to (a)) followed by the infinite run from h 1 , z (thanks to (b),(c)) leads to an infinite run witnessing that the instance is positive.

(II) Assume that (B) holds. (a) does not hold and the control state h 1 can be reached with a maximal value x max while visiting only states from X 1 . Let q 0 , x 0 , . . . , q k , x k be the run in V X1∪{h1} with q k = h 1 and x k equal to x max . As V , h 1 , x max and X 2 , h 2 , . . . , X α , h α is a positive instance of GREACH(1-VASS), the concatenation of q 0 , x 0 , . . . , q k , x k with the infinite witness run for that instance of GREACH(1-VASS) leads to a witness run for the instance V , q 0 , x 0 and X 1 , h 1 , . . . , X α , h α .

(III) Now suppose that V , q 0 , x 0 and X 1 , h 1 , . . . , X α , h α is a positive instance of GREACH(1-VASS). Therefore, there is an infinite run q 0 , x 0 -→ q

1 , x 1 - → q 2 , x 2 • • • with indexes 0 < i 1 < i 2 < • • • < i α such that for all j ∈ [1, α], q ij = h j and {q k | k < i j } ⊆ X j .
We need to make a case analysis depending on whether (a) holds. Condition (a) states that h 1 can be reached from q 0 , x 0 with a counter value as great as desired, while visiting only states from X 1 . If condition (a) does not hold, then there is a maximal counter value x max and a run q 0 , y 0 • • • q n , y n in V with q 0 , y 0 = q 0 , x 0 , q n = h 1 , y n = x max , and {q 0 , . . . , q n-1 } ⊆ X 1 . Necessarily, we have x max ≥ x i1 . Let ρ be the run

q i1 , x i1 -→ • • • - → q i2 , x i2 • • • . Obviously, ρ +(xmax-xi 1 )
is also a run and actually it is a witness for the instance V , h 1 , x max and X 2 , h 2 , . . . , X α , h α . Consequently, condition (B) holds true.

In the case condition (a) holds,

q i1 - → q i1+1 - → • • • (the projection on Q of the suffix run q i1 , x i1 - → q i1+1 , x i1+1 - → • • • ) is a witness run for the instance V , h 1 and X 2 , h 2 , . . . , X α , h α of GREACH(0-VASS). Similarly, the suffix path ρ = q iα - → q iα+1 - → • • • is infinite (h α = q iα )
, and therefore some state q is repeated infinitely often. Consequently, there is a simple path from h α to q and a simple loop from q to q . It remains to show that the loop can be choosen to be non-negative so that condition (c) holds.

Suppose that the run ρ contains only loops with negative effects. There is a location q ∞ that occurs infinitely often in the run, and therefore this leads to a contradiction as N is well-founded (indeed any non-empty subrun starting by q ∞ and ending by q ∞ would decrease strictly the counter value). Consequently, ρ contains a subrun ρ = q L , x L -→ q L+1 , x L+1 -→ • • • q L , x L built over a non-negative loop and by removing from ρ the subruns corresponding to a negative loop, we can assume that ρ is built from a nonnegative simple loop (if ρ contains a subrun built over a simple non-negative loop, take it instead). So, we can assume w.l.o.g. that q L , x L -→ q L+1 , x L+1 -→ • • • q L , x L is a simple non-negative loop. Consequently, there is a simple path from h 1 to q L = q L and there is a simple non-negative loop from q L (the one obtained from ρ ), which entails (c).

Theorem 10. The problem GREACH(1-VASS) is in ptime.

Theorem 10 is one of the main contributions of the paper, as it is instrumental to determine the complexity of model checking RB±ATL + ({1}, 1).

Proof. Let V , q 0 , x 0 and X 1 , h 1 , . . . , X α , h α be an instance of GREACH(1-VASS) of size N . Here is a simple algorithm to solve GREACH(1-VASS).

• If condition (a) holds, then return 1 if (b),(c) hold, 0 otherwise.

• Otherwise ((a) does not hold), if there is no simple run q 0 , x 0 , . . . , q k , x k in V X1∪{h1} with q k = h 1 then return 0, otherwise, compute x max and return 1 if V , h 1 , x max and X 2 , h 2 , . . . , X α , h α is a positive instance of GREACH(1-VASS) (0 otherwise). Note that we perform here a recursive call with a strictly shorter sequence X 2 , h 2 , . . . , X α , h α .

The following problems can be solved in polynomial time.

• As explained in the proof of Lemma 4, GREACH(0-VASS) and (c) can be checked in polynomial time, say in time O(p 1 (N )).

• Checking whether (a) holds can be done in polynomial time by using the data structures introduced in Section 3.2, say in time O(p 2 (N )). Indeed, (a) is equivalent to the satisfaction of the conditions below:

(a ) there is a simple run q 0 , x 0 , . . . , q n , x n in V X1∪{h1} and its projection over

X 1 ∪ {h 1 } is in the regular language X * 1 (h 1 + ε); (b )
there is a positive simple loop t 1 . . . t β in V X1∪{h1} that can be fired from q n , x n ;

(c ) there is a simple path in V X1∪{h1} starting at q n , ending at h 1 ;

(d ) if h 1 occurs in the simple loop in (b ), then q n = h 1 .

Let us briefly show how (a )-(d ) entail (a). Roughly speaking, the subrun is constructed as follows. From q 0 , x 0 consider the simple run leading to q n , x n (condition (a )). Then, take the positive simple loop from (b ) ||R|| × |Q| times reaching the configuration q n , y with y ≥ ||R|| × |Q|. Then, consider the simple run from q n , y to h 1 , z based on the transitions of the simple path from the condition (c ). As this is a simple run, z ≥ 0 while preserving the constraints on X 1 . For the proof in the other direction, this boils down to detect a positive simple loop. The details are omitted here.

• Similarly, when the condition (a) does not hold, computing x max (if it exists) can also be computed in polynomial time using the proofs in Section 3.2, say in time O(p 3 (N )).

From the above algorithm, checking whether (a) holds is done at most α times, as well as computing x max . Consequently, the algorithm runs in time O(α(p 2 (N 2 ) + p 3 (N 2 )) + p 1 (N 2 )). The value N 2 is due to the fact that every time a new value x max is computed, it may add the initial size N (in the worst case) to the size of the new input and this can be done at most α times with α ≤ N .

The ptime upper bound in Theorem 10 is a drastic drop compared to the complexity for the general problem GREACH(VASS). Indeed, GREACH(VASS) is expspace-hard as the control-state reachability problem for VASS can be reduced to it (and then we use [START_REF] Lipton | The reachability problem requires exponential space[END_REF]). GREACH(VASS) is definitely in expspace by [START_REF] Habermehl | On the complexity of the linear-time mu-calculus for Petri nets[END_REF]Theorem 5.4] that deals with the linear-time µ-calculus on VASS. Besides, for all r ≥ 1, model-checking r-VASS with linear-time µ-calculus has been shown in pspace [58, Theorem 4.1] (pspace-hardness still holds with a unique counter, inherited from plain LTL model-checking [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]). Herein, we established that GREACH(1-VASS) behaves even better, as it can be solved in polynomial time only. Theorem 10 shall be essential for the results shown in Section 4 below.

The Model-Checking Problem for RB±ATL +

In this section, we mainly consider the model-checking problem for RB±ATL + ({1}, 1) as well as for RB±ATL + (r), for some fixed r ≥ 1.

To this end, we need to provide a few more introductory notions. Given an RB-CGS M = {1}, 1, S, Act, act, wf, δ, L with a single agent and a single resource, we define the 1-VASS V M = S, 1, R V such that q u -→ q ∈ R V iff there is some action a ∈ act(q, 1) such that δ(q, a) = q and wf (q, 1, a) = u. Similarly, we write K M = S, R, L to denote the Kripke-style structure such that q R q iff there is some action a ∈ act(q, 1) such that δ(q, a) = q . Observe that M and V M share the same labelling function L. We introduce Kripke-style structures as the modality {1} ω amounts to forgetting about weights in M , and therefore M can be understood as the Kripke-style structure K M , and RB±ATL + ({1}, 1) model-checking reduces to CTL + model-checking. Similarly, the strategy modality ∅ b behaves as the universal path quantifier A in weight-free transition systems, and therefore the model-checking problem reduces again to CTL + model-checking. Given S 1 ⊆ S, we write V S1 M (resp. K S1 M ) to denote the restriction of V M (resp. K M ) to the locations/states in S 1 only.

Model-checking problem for RB±ATL + ({1}, 1): algorithm

To solve MC(RB±ATL + ({1}, 1)), there is an essential case to consider, namely how to verify whether (M, s) |= {1} b Ψ (this is the key case that needs to be solved in a satisfactory way, complexity-wise). With a single agent in M , this amounts to checking the existence of a computation λ starting from s, with initial budget b ∈ N, satisfying Ψ. This is the place where the problem GREACH(1-VASS) introduced in Section 3.3 helps. The conditions on Ψ in Lemma 5 below are relaxed at a later stage. Lemma 5. Let Ψ be a Boolean formula built over path formulae of the form X p or p U q, where p, q are propositional variables. Let M be an RB-CGS, s ∈ S and b ∈ N. The problem of checking (M, s) |= {1} b Ψ (in RB±ATL + ({1}, 1)) is in np.

Proof. We recall that verifying (M, s) |= {1} b Ψ with a single agent in M amounts to check the existence of an infinite computation λ starting from s, with initial budget b ∈ N, satisfying Ψ. Without loss of generality, one can assume that Ψ is a Boolean formula in negation normal form (NNF) built over atomic formulae of the form X p or p U q. Satisfaction of Ψ on λ amounts to guess which atomic formulae in Ψ hold, and then to check that the guess is correct. The verification step is done in ptime, so that the whole step of model-checking {1} b Ψ can be done in np.

Since ¬(p U q) is logically equivalent to G ¬q ∨ (¬q U(¬p ∧ ¬q)), ¬ X p is logically equivalent to X ¬p, and X and G distributes over ∧, the formula Ψ can be assumed to be a positive Boolean formula built over atomic formulae of the form X C, G C or C U C where C and C are conjunctions of literals. Guessing which atomic formulae in Ψ hold to evaluate Ψ to true, amounts to guess a conjunction of the form

X C 0 ∧ G C 0 ∧ (C 1 U C 1 ) ∧ • • • ∧ (C n U C n ), (5)
for some n ∈ N, where the C i 's and C i 's are conjunctions of literals (empty conjunctions are equivalent to ). Below, we treat only the cases with C 0 and C 0 distinct from and n > 0, but the other cases admit a simpler treatment (omitted herein). Of course, the satisfaction of the atomic path formulae from the above conjunction (modulo the logical equivalences cited above) would make Ψ true propositionally (see Section 3.3 for a detailed description of the conditions whereby the conjunction enforces the truth of Ψ, see also Definition 9). Existence of an infinite computation λ starting from s, with initial budget b ∈ N, satisfying conjunction ( 5) is equivalent to the existence of an infinite run q 0 , x 0 -→ q 1 , x 1 -→ q 2 , x 2 • • • in the 1-VASS V M satisfying the following conditions:

1. q 0 , x 0 = s, b .

{q

i | i ∈ N} ⊆ {s ∈ S | (M, s) |= C 0 } def = S 1 . Hence, we can consider V S1 M instead of V M .
3. (M, q 1 ) |= C 0 . As there is only a linear amount of configurations obtained from q 0 , x 0 in one step, we can easily get rid of the constraint on q 1 , x 1 by exploring all possibilities (and this does not cause any exponential blow-up). Let

I 0 = {i ∈ [1, n] | (M, q 0 ) |= C i } and I 1 = {i ∈ [1, n] | (M, q 1 ) |= C i and (M, q 0 ) |= C i }.
4. There are a partition {Y 1 , . . . , Y α } of [1, n] \ (I 0 ∪ I 1 ) and a strict linear ordering 0 < i 1 < . . . < i α such that for all j ∈ [1, α], we have (M,

q ij ) |= k∈Yj C k and {q β | β < i j } ⊆ {s | (M, s) |= k∈Yj C k }.
In a nutshell, the satisfaction of ( . . , Y α and by the positions i 1 , . . . , i α . This is a standard type of reasoning when CTL + is involved, see e.g., [START_REF] Demri | Temporal Logics in Computer Science[END_REF].

C 1 U C 1 ) ∧ • • • ∧ (C n U C n ) requires
Consequently, after guessing which atomic formulae hold in the path formula Ψ, the next configuration q 1 , x 1 , the partition Y 1 , . . . , Y α (with linearly ordered sets), the sequence of states q i1 , . . . , q iα , we have then to solve an instance of GREACH(1-VASS) for the 1-VASS V S1 M and initial configuration q 1 , x 1 . We write X j to denote the set {s | (M, s) |= k∈Yj C k }. Without any loss of generality, we can assume that q 1 , q i1 , . . . , q iα are all pairwise distinct. For instance, if q i k = q i l , then we can simply merge Y k with Y l . So we have to solve an instance of GREACH(1-VASS) of the form V S1 M , q 1 , x 1 and X 1 , q i1 , . . . , X α , q iα , which can be done in ptime by Theorem 10. The guess and check steps can be therefore performed in np as all the witnesses are of polynomial size in the size of the inputs, and all the checking steps can be done in polynomial time in full generality.

Hence, the whole model-checking algorithm for RB±ATL + ({1}, 1) can be shown in ∆ P 2 as it uses a polynomial amount of instances of the problem in Lemma 5. Each instance can be solved in np, since GREACH(1-VASS) is in ptime (Theorem 10).

Theorem 11. MC(RB±ATL + ({1}, 1)) is ∆ P 2 -complete.

Proof. As regards the lower bound, it follows from the ∆ P 2 -hardness of model-checking CTL + [START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF]. As for the upper bound, let M = {1}, 1, S, Act, act, wf, δ, L be an RB-CGS, and φ a formula in RB±ATL + ({1}, 1). Let us present Algorithm 1 that computes the finite set {s ∈ S | (M, s) |= φ}, where we assume that b ∈ N and Ψ is a Boolean formula in NNF built over path formulae of the form X φ or φ U φ , for state formulae φ, φ . Moreover, let us assume that the maximal state formulae occurring in Ψ are φ 1 , . . . , φ N and the model-checking algorithm has already determined that they hold true exactly on the states in sets S 1 , . . . , S N , respectively. Let Ψ be the formula obtained from Ψ by replacing each φ i by a fresh propositional variable p i , and M be the RB-CGS obtained from M by modifying the labelling function as follows: L (p i ) def = S i . We have the following equivalences: By structural induction, one can show that (M, s) |= φ iff s ∈ MC(M, φ).

1. (M, s) |= ∅ b Ψ iff (K M , s) |= AΨ in CTL + , 2. (M, s) |= {1} ω Ψ iff (K M , s) |= EΨ in CTL + .
As far as computational complexity is concerned, MC(M, φ) is computed with a recursion depth linear in the size of φ and a polynomial number of np calls. More precisely, for each occurrence of a subformula ψ of φ, MC(M, ψ) can be computed only once, which guarantees the overall number of calls of the form MC(M, ψ): it is sufficient to take advantage of dynamic programming and to work with a table to remember the values MC(M, ψ) already computed. For the sake of clarity such a mechanism is omitted in the present algorithm. Intuitively, we would handle an array T , where T [ψ] takes either the value ⊥ (undefined) or a subset of S. Initially, all the values of T are undefined. Whenever MC(M, ψ) is invoked in the algorithm above, we operate a change of the following form in the code: we first check whether T [ψ] is defined. It is only in the case T [ψ] is undefined that a recursive call MC(M, ψ) is performed. This technique is standard and herein we use it so that for each subformula ψ, MC(M, ψ) is actually 28

Algorithm 1 -RB±ATL + ({1}, 1) Model-checking -

1: procedure MC(M, φ) 2:
case φ of ¬ψ: return S\ MC(M, ψ)

5:

φ 1 ∧ φ 2 : return MC(M, φ 1 )∩ MC(M, φ 2 )
6:

∅ b Ψ/ ∅ ω Ψ: return {s | (K M , s) |= AΨ in CTL + } 7:
{1} end case 10: end procedure called only once. We recall that ∆ P 2 , a.k.a., ptime np , is precisely the class of problems that can be solved in polynomial time with an oracle in np. We also take advantage of the fact that the model-checking problem for CTL + is in ∆ P 2 (see, e.g., [START_REF] Demri | Temporal Logics in Computer Science[END_REF]). The decision procedure for solving the model-checking problem for RB±ATL + ({1}, 1) invokes the subroutine for solving the model-checking problem for CTL + with one counter, that be run optimally thanks to Lemma 5. The existence of a polynomial-time reduction between MC(RB±ATL + ({1}, 1)) and the model-checking problem for CTL + is guaranteed, as both problems are ∆ P 2 -complete. The question about the encoding of MC(RB±ATL + ({1}, 1)) into plain CTL + is certainly interesting and solving conditions (A) and (B) in Lemma 4 actually amounts to detect graph-theoretical properties on the 1-VASS, so a direct encoding is feasible, but it is not further investigated here.

Model-checking problem for RB±ATL + (r)

In [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], the 2exptime upper bound for model-checking RB±ATL is obtained with a decision procedure calling subroutines to solve the nontermination and the control-state reachability problems for AVASS on instances of the form A M,A,s , where M is an RB-CGS, A is a coalition, and s is a state in M , as described in Section 4.2.1 below. On the other hand, to obtain the 2exptime upper bound for model-checking RB±ATL * , also in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], the decision procedure calls a subroutine for solving the parity game problem for AVASS (see Section 4.2.1) but, in the worst-case, on systems with a doubly-exponential number of locations in the size of the input formula. Indeed, synchronised products are considered between deterministic parity automata (on ω-words) and AVASS of the form A M,A,s . This is due to the fact that given an LTL formula, an equivalent deterministic parity automaton might have a doubly-exponential number of states in the size of the input LTL formula (see, e.g., [START_REF] Vardi | Reasoning about infinite computations[END_REF][START_REF] Schewe | Tighter bounds for the determinisation of Büchi automata[END_REF]). Hence, even when the number of resources r is fixed (which is an assumption made in this section), solving MC(RB±ATL + (r)) by using the method in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], would lead to a 2exptime upper bound.

In this section, we explain how to gain one exponential by providing a decision procedure that solves MC(RB±ATL + (r)) in exponential time, when r is fixed (this is known to be optimal as soon as r ≥ 4). Such an improvement can be explained by the fact that reasoning about LTL formulae of temporal depth one is usually simpler than for arbitrary LTL formulae (see, e.g., [START_REF] Demri | The complexity of propositional linear temporal logics in simple cases[END_REF]Section 7.3]). More precisely, we are able to de-sign some ad-hoc verification method using alternating VASS without going through a translation from LTL formulae to deterministic parity automata. Apart from our new exptime bound, this section can be viewed as providing an alternative decision procedure for solving MC(RB±ATL + ) without going through the determinisation of Büchi automata, or as generalising the reduction used to decide RB±ATL [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], but at the cost of building AVASS with an exponential number of locations (which is strictly more expensive than for RB±ATL, but strictly less than for RB±ATL * ). As CTL + is exponentially more succinct than CTL [START_REF] Wilke | CTL + is exponentially more succinct than CTL[END_REF], which entails that some ATL + (resp. RB±ATL + (Ag, r)) formulae can be exponentially more succinct than ATL (resp. RB±ATL(Ag, r)) formulae, this extra cost for solving MC(RB±ATL + (r)) is most likely the best we can hope for.

Correspondence between RB-CGS and AVASS

In this section, we recall the notion of alternating vector addition systems with states (AVASS), as well as relevant related decision problems. Roughly speaking, AVASS can be viewed as VASS in which fork rules are also allowed, but such branching in computations has no effect on the counters. As shown in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], AVASS are operational models closely related to the model-checking problem for RB±ATL-like logics. First, we need to introduce some preliminaries.

A binary tree T , which may contain nodes with a single child, is a non-empty subset of {1, 2} * such that, for all n ∈ {1, 2} * and i ∈ {1, 2}, n

• i ∈ T implies n ∈ T and, n • 2 ∈ T implies n • 1 ∈ T .
Trees of arbitrary finite arity are defined accordingly (details are omitted herein).

Definition 12 (AVASS [21]). An alternating VASS is a tuple

A = Q, r, R 1 , R 2 such that Q is a finite set of locations; r ≥ 0 is the number of resources; R 1 is a finite subset of Q × Z r × Q ( update rules); and R 2 is a (finite) subset of Q × Q × Q ( fork rules).
Standard VASS [START_REF] Karp | Parallel program schemata[END_REF] are AVASS with no fork rules (i.e., R 2 = ∅). A derivation skeleton in A is a labelling D : T → (R 1 ∪ R 2 ∪ {⊥}) such that T is a binary tree, and if n has one child (resp. has two children, is a leaf) in T , then

D(n) ∈ R 1 (resp. D(n) ∈ R 2 , D(n) =⊥). A derivation in A based on D is a labelling D : T → Q × Z r such that:
• if n has one child n in T , D(n) = q, u, q and D(n) = q, v for some v, then D(n ) = q , v + u ;

• if n has two children n and n in T , D(n) = q, q 1 , q 2 and D(n) = q, v for some v, then D(n ) = q 1 , v and D(n ) = q 2 , v .

So, the fork rules do not update the value of resources. Hence, there is an asymmetry between update rules and fork rules. Differently from branching VASS (see, e.g., [START_REF] Verma | Goubault-Larrecq, Karp-Miller Trees for a Branching Extension of VASS[END_REF][START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF][START_REF] Göller | A polynomial-time algorithm for reachability in branching VASS in dimension one[END_REF][START_REF] Figueira | Polynomial-space completeness of reachability for succinct branching VASS in dimension one[END_REF][START_REF] Mazowiecki | Reachability for Bounded Branching VASS[END_REF]), fork rules have no effect on counter values. A derivation D is admissible (or a proof ) whenever only natural numbers occur in it. By way of example, a proof can be found below (with the root at the bottom) assuming that

R 1 = {q 1 -2,3 ---→ q 0 , q 2 4,4 --→ q 3 } and R 2 = {q 0 - → q 1 , q 2 }.
q 3 , 9, 9 q 2 , 5, 5 . . . . q 1 , 3, 8 q 2 , 3, 8 q 0 , 3, 8 q 1 , 5, 5 q 0 , 5, 5 q 1 , 7, 2

Hereafter, we consider the following decision problems pertaining to AVASS.

Control-state reachability: given an AVASS A and control states q 0 and q f , is there a finite proof with root labelled by q 0 , 0 and each leaf belonging to {q f } × N r ?

Nontermination: given an AVASS A and a control state q 0 , is there a proof whose root is labelled by q 0 , 0 and all the maximal branches are infinite?

Parity game problem: given an AVASS A, a state q 0 ∈ Q, b ∈ N r , and a colouring col : Q → [0, p -1] for some number p ≥ 1, is there a proof with root labelled by q 0 , b , all the maximal branches being infinite, and the maximal colour occurring infinitely often along each maximal branch being even?

These problems are known to be 2exptime-complete [START_REF] Courtois | Alternating vector addition systems with states[END_REF][START_REF] Jurdziński | Fixed-dimensional energy games are in pseudo-polynomial time[END_REF][START_REF] Colcombet | Perfect half space games[END_REF]. Decidability of control-state reachability and nontermination problems were first established in [START_REF] Raskin | Games for counting abstractions[END_REF] by using monotonicity of the games. The 2exptime upper bound is preserved if we assume that the root is labelled by q 0 , b with b ∈ N r encoded in binary or if the set of fork rules R 2 is a finite subset of β≥2 Q β (by suitably adapting all the definitions, see e.g., [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Lemma 7]). Elements in Q β are said to be (β -1)-ary (β -1 is the number of branches in the forking).

By [START_REF] Colcombet | Perfect half space games[END_REF]Corollary 5.7] on the parity energy game problem with initial credit, and by [START_REF] Abdulla | Solving Parity Games on Integer Vectors[END_REF]Lemma 4] relating the parity game problem for AVASS and the parity energy game problem, the former can be solved in time

(|Q| × ||R 1 ||) 2 O(r×log(r+p)) + O(r × log|| b||),
where

|| b|| def = max{| b[i]| : i ∈ [1, r]} and ||R 1 || def = max{|| u|| : q u - → q ∈ R 1 }.
When r and p are bounded, the problem is therefore in exptime. Indeed, the expression 2 O(r×log(r+p)) and r are bounded, whereas ||R 1 || is at most exponential in the size of the input (integers are encoded in binary). Now, we briefly recall the correspondence established in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF] between strategies in RB±ATL-like logics and proofs in AVASS. Since we use this correspondence in the paper, we explain it in detail for the reader's benefit. Below, we consider AVASS with fork rules in β≥2 Q β (arbitrary arity), and where proofs are trees with nodes labelled by elements in Q × N r . Let M be a finite RB-CGS, A ⊆ Ag be a coalition, and s be one of its states. We construct the AVASS A M,A,s such that the set of computations in M starting in s and respecting a strategy F A corresponds to a derivation skeleton whose root is labelled by an update rule with first state s . Hence, we leverage on the fact that a b-strategy generates a set of maximal computations that can be arranged as a finitely-branching tree with infinite branches only, and such an infinite tree can be viewed precisely as an infinite proof on A M,A,s .

Given M = Ag, r, S, Act, act, wf, δ, L and a distinguished state s ∈ S, the AVASS A M,A,s def = Q, r, R 1 , R 2 is built as follows:

Q def = {s } ∪ { s, f | s ∈ S, f ∈ D A (s)} ∪ { g, s | s , s ∈ S, g ∈ D Ag (s ), δ(s , g) = s }.
Every location in Q is attached to a state in S and contains a finite piece of information: in s, f , f is a joint action available to A implementing its strategy whereas in g, s , we remember the global joint action to reach s .

• The set R 1 of update rules contains the following elements.

s , wf A (s , f ), s , f , for all f ∈ D A (s ). Indeed, the locations in Q attached to s have a special treatment.

g, s , wf A (s, f ), s, f , for all g, s ∈ Q and f ∈ D A (s).

• The set R 2 of fork rules contains the following elements.

-

For s, f ∈ Q, let { g 1 , s 1 , . . . , g α , s α } = { g, s ∈ S | s = δ(s, g), g ∈ D Ag (s), f g}.
This set is non-empty because the protocol function always returns a non-empty set of actions. We recall that a protocol function in an RB-CGS is a map of the form act : S × Ag → (℘(Act) \ ∅).

We add the α-ary fork rule s , f , g 1 , s 1 , . . . , g α , s α to R 2 . The joint actions available for the opponent coalition (Ag \A) determine which locations g 1 , s 1 , . . . , g α , s α can be reached. It is the proponent restriction condition that guarantees that using fork rules in this place (i.e., without updating the counter values) is correct. We recall that the proponent restriction condition enforces that the resource availability depends only on the agents in proponent coalitions.

Given an infinite computation

λ = s 0 g1 - → s 1 g2 - → s 2 .
. . starting in s = s 0 , also respecting a strategy F A , we can associate it with an infinite sequence (which we call an extended computation)

ext(λ, A) def = s 0 u0 - → s 0 , f 0 - → g 0 , s 1 u1 - → s 1 , f 1 - → • • •
with s 0 = s , and for all n ≥ 0,

f n = F A (s 0 g1 - → s 1 . . . gn - → s n ) where f n is the restriction of g n to A and wf A (s n , f n ) = u n .
Hence, the way ext(λ, A) is designed from λ essentially depends on the weight of the actions fired by the agents in the coalition A. Typically, A = A may lead to ext(λ, A) different from ext(λ, A ) (but not necessarily).

Further, transitions in M can be viewed as triples s , g, s such that δ(s , g) = s , also written as s g -→ s . The finite set of such transitions is denoted by Σ M , which can be interpreted as a finite alphabet when M is finite. An infinite computation λ = s 0 g1 -→ s 1 g2 -→ s 2 . . . can then be represented as the ω-word (s 0

g1 - → s 1 ) • (s 1 g2 - → s 2 ) • (s 2 g3 - → s 3 ) • • • in Σ ω M .
Given an infinite branch of the proof in A M,A,s corresponding to the extended

computation s 0 u0 - → s 0 , f 0 - → g 1 , s 1 u1 - → s 1 , f 1 - → • • • , its Σ M -projection is defined as the sequence (s 0 g1 - → s 1 ) • (s 1 g2 - → s 2 ) •(s 2 g3 - → s 3 ) • • • Formal correspondences
between M and A M,A,s are below. It is worth noting that in the proofs of A M,A,s , along all branches, there is a strict alternation between update rules and fork rules.

Proposition 1. [12, Lemma 4] Let L ⊆ Σ ω M and b ∈ N r .
There is a b-strategy F A w.r.t. s in M such that the set Comp(s , F A ) of computations is included in L iff there is a proof in A M,A,s with root labelled by s , b , every maximal branch being infinite, and its Σ M -projection being in L.

By way of example, let S φ be the set of states in S satisfying the (state) formula φ (S is from some RB-CGS M ) and L φ be the restriction of Σ ω M to ω-words involving only states from S φ (i.e., s g -→ s is allowed with s, s ∈ S φ ). By Proposition 1, (M, s ) |= A b G φ iff there is a proof in A M,A,s restricted to locations involving only states in S φ whose root is labelled by s , b and every maximal branch is infinite. This property can actually be generalised to any language in Σ ω M defined from a language in S ω and this is used in the proof of forthcoming Lemma 7.

Carefully constructing AVASS

In this section, we explain how to handle the verification of (M, s ) |= A b Ψ, for A ⊆ Ag and b ∈ N r . As in Section 3, we assume w.l.o.g. that Ψ is a Boolean formula in NNF built over atomic formulae of the form X p or p U q, where p, q are propositional variables. These are the building blocks to handle the general case, that is considered at a later stage (see Theorem 13). To determine the satisfaction of (M, s ) |= A b Ψ, we construct an AVASS A = Q , r, R 1 , R 2 , a colouring col : Q → [0, 1] (defining a co-Büchi condition, as there are two colors and the smallest one is even), and q ∈ Q such that 1. (M, s ) |= A b Ψ iff there is a proof with root labelled by q , b such that all the maximal branches are infinite and the maximal (only) colour that appears infinitely often along each branch is 0.

2. |Q | is (only) exponential in |M | + |Ψ|. 3. ||R 1 || ≤ |Ag| × max({||wf (s, a, a)|| : s ∈ S, a ∈ Ag, a ∈ Act}).
In Section 4.2.1, we have shown how to define an AVASS A M,A,s = Q, r, R 1 , R 2 given M , A and s . The AVASS A is made of copies of A M,A,s so that the general behavior of A M,A,s is preserved, but we decorate the locations with a finite memory taking care of the satisfaction of the path formula Ψ.

Let us provide a few more definitions. Without loss of generality, we assume that Ψ is a positive Boolean combination of atomic path formulae of one of the following forms: G , 1 U 2 , U( 1 ∧ 2 ), X where the 's are literals. Notice that the transformation to obtain this shape can be performed in linear time (see Lemma 5).

Let s ∈ S be a state and Φ be a Boolean combination of atomic path formulae of the form above. We write s(Φ) to denote the Boolean combinations of atomic path formulae obtained from Φ according to the following clauses:

1. If G occurs in Φ and (M, s) |= , then replace every occurrence of G in Φ by ⊥. We write s[Φ] to denote the path formula defined as for s(Φ) except that only the first three clauses are considered (next-time atomic formulae remain untouched, if any). Intuitively, when Φ is a path formula to be satisfied on the extension of a current finite computation and s is visited next, the path formula s(Φ) is obtained from Φ by replacing the atomic path subformulae in Φ that are definitely true or false by or ⊥, respectively. The final value for s(Φ) is obtained by using simplification rules to eliminate or propagate or ⊥, if possible (e.g., ⊥ ∨φ is reduced to φ). Hence, s(Φ) may take the values ⊥ or (not strictly speaking path formulae, but we assume so below). The same simplifications are used for s[Φ]. For technical reasons, we have also introduced the path formula s[Φ] that is computed without taking into account the next-time subformulae. This is helpful, when a path formula Φ is updated at the first position of a computation. Indeed, suppose that (M, λ) |= X with λ[0] = s. Obviously, (M, λ ≥1 ) |= and λ [START_REF] Alur | Alternating-time temporal logic[END_REF] satisfies the literal . In particular, if Φ contains X and (M, λ) |= Φ, then we may wish to replace X by in Φ but this can be done only after visiting λ [START_REF] Alur | Alternating-time temporal logic[END_REF], whence the slight difference between the definitions of s(Φ) and s[Φ]. We write S(Ψ) to denote the set of path formulae obtained from Ψ by successive applications (possibly zero) of s(•) and s[•] for some s ∈ S, i.e.,

S(Ψ)

def = {s 1 (s 2 (• • • s n [Ψ] • • • )) | s 1 , . . . , s n ∈ S, n ≥ 0}.
Observe that only the first application s n [Ψ] uses the transformation of the form s[•] and therefore ignores the X-formulae for the reasons just explained above. Here are its main properties. Lemma 6. Let Ψ be a path formula as above, M be an RB-CGS, and λ be one of its computations.

(correctness.1) (M, λ) |= Ψ iff (M, λ) |= s[Ψ] for λ[0] = s. (correctness.2) If Ψ has no next-time atomic formulae, then (M, λ) |= s(Ψ) iff (M, λ ≥1 ) |= s(Ψ) for λ[0] = s. (correctness.3) (M, λ) |= s[Ψ] iff (M, λ ≥1 ) |= s (s[Ψ]) for λ[0] = s and λ[1] = s . (small size) Ψ ∈ S(Ψ) and |S(Ψ)| is in O(3 |Ψ| ).
(stabilisation) There is i ≥ 0 such that for all j ≥ i, we have λ

[j](• • • (λ[0][Ψ]) • • • ) = λ[i](• • • (λ[0][Ψ]) • • • ).
As a consequence of Lemma 6, for all i ≥ 0, we have (M, λ)

|= Ψ iff (M, λ ≥i ) |= λ[i](• • • (λ[0][Ψ]) • • • )
. By Lemma 6(stabilisation), there exists a "limit" path formula Φ λ,Ψ equal to some path formula of the form λ

[I](• • • (λ[0][Ψ]) • • • ) for some I ≥ 1, such
that the satisfaction of a subset {G 1 , . . . , G q } of always formulae from Φ λ,Ψ makes the path formula propositionally true, assuming that (M, λ) |= Ψ holds true. In particular, this means that (M, λ) |= G 1 ∧• • •∧G q . Without loss of generality, we can also asssume no position after I witnesses the satisfaction of an until formula from Φ (since there are a finite amount of positive occurrences of until formulae in Φ).

Proof. (correctness.1)

• If G occurs in Ψ and (M, s) |= , then (M, λ) |= G . Consequently, (M, λ) |= Ψ iff (M, λ) |= Ψ[G ←⊥]. • Similarly, if 1 U 2 occurs in Ψ and (M, s) |= 2 , then (M, λ) |= 1 U 2 . Conse- quently, (M, λ) |= Ψ iff (M, λ) |= Ψ[ 1 U 2 ← ].
As in the definition, taking care of formulae U( 1 ∧ 2 ) is similar.

• If 1 U 2 occurs in Ψ and (M, s) |= 1 ∨ 2 , then (M, λ) |= 1 U 2 . Consequently, (M, λ) |= Ψ iff (M, λ) |= Ψ[ 1 U 2 ←⊥].
So let Φ be the path formula obtained from Ψ by applications of the above-mentioned substitutions, after applying the simplifications related to ⊥ and . Note that the order in which the substitutions are applied is irrelevant as well as how the simplications are performed. The path formula Φ is actually equal to s[Ψ]. From the above properties, we conclude (M, λ) |= Ψ iff (M, λ) |= Φ.

(correctness.2) The proof is similar to the proof for (correctness.1) by observing that if the truth status of an until formula (resp. the falsity of an always formula) could not be determined at state s and Ψ has no next-time atomic formulae, then (M, λ) |= Ψ iff (M, λ ≥1 ) |= Ψ.

(correctness.3) Suppose that X occurs in Ψ.

• If (M, s ) |= , then (M, λ) |= s[Ψ] iff (M, λ) |= (s[Ψ])[X ← ]. • If (M, s ) |= , then (M, λ) |= s[Ψ] iff (M, λ) |= (s[Ψ])[X ←⊥].
So let Φ be the path formula obtained from Ψ by applications of the above-mentioned substitutions, after applying the simplifications related to ⊥ and . Again, note that the order in which the substitutions are applied is irrelevant as well as how the simplifications are performed thanks to confluence. Indeed, when Φ (resp. Φ ) can be obtained from Φ by applying either a transformation from clauses (1)-( 4) in the definition of s(•) or a simplication, then there is Ψ C that can be obtained from Φ (resp. Φ ) in at most one step, whence the confluence property. From the above properties, we have (M, λ)

|= Ψ iff (M, λ) |= Φ.
As Φ has no next-time atomic formulae, by (correctness.2), we have (M, λ)

|= Φ iff (M, λ ≥1 ) |= Φ. By (correctness.1), we have (M, λ ≥1 ) |= Φ iff (M, λ ≥1 ) |= s (Φ) (s (Φ) = s [Φ] because Φ has no next-time X) and one can check that s (Φ) is logically equivalent to s (s[Ψ]).
Proof. The proof combines advantageously the properties of A M,A,s [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF] and the ones for A related to the satisfaction of path formulae.

Let us start by performing the complexity analysis before providing the correctness arguments.

As |Q| is in O(|M | 2 ), we have |Q | is in O(3 |Ψ| × |M | 2 ), see Lemma 6(small size). The value ||R 1 || is bounded by |Ag| × max({||wf (s, a, a)|| : s ∈ S, a ∈ Ag, a ∈ Act}), which is bounded by |M |2 |M | (
as a direct consequence of the construction of A M,A,s ). By using the expression

(|Q| × ||R 1 ||) 2 O(r×log(r+p))
+ O(r × log|| b||)

for the parity game problem for AVASS (see Section 4.2.1), when r is fixed and p = 2, (M, s

) |= A b Ψ can be checked in time exponential in |M | + | A b Ψ|. Let b ∈ N r . We write A M,A,s = Q, r, R 1 , R 2
to denote the AVASS defined in Section 4.2.1 given M , A and s . Similarly, we write A = Q , r, R 1 , R 2 to denote the AVASS defined from A M,A,s and Ψ as shown above. The locations in Q have one of the following forms:

Φ, s , Φ, s, f , Φ, g, s ,
where Φ is a path formula obtained from Ψ by replacing some atomic path formulae by either or ⊥, whereas s , s, f and g, s are locations from Q. By construction of A , removing from a proof in A the value Φ (projection on the second component of the locations), leads to a proof in A M,A,s . (⇒) First, suppose that (M, s ) |= A b Ψ. Without loss of generality, we assume that Ψ is a positive Boolean combination of atomic path formulae of one of the following forms: G , 1 U 2 , U( 1 ∧ 2 ), X where the 's are literals. By definition of the satisfaction relation, there is a b-strategy F A with respect to s such that for all λ ∈ Comp(s , F A ), we have (M, λ) |= Ψ. As done in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Section 4], the computations in Comp(s , F A ) can be organised as an infinite tree corresponding to a derivation skeleton for A M,A,s . Let us recall the definition of such a tree T F A equipped with a labelling function L : T F A → S and with a partial map R : T F A × T F A → ( s ∈S D Ag (s )). We reproduce below some material from [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Section 4] to have a self-contained formalisation. Below, we use some notations a bit different from those in the previous sections.

• L(ε) def = s where ε is the root of T F A .

• For all finite words w = k

1 • • • k β in T F A such that L(w) is already defined, we add to T F A the values k 1 • • • k β • 1, . . . , k 1 • • • k β • α such that -F A (L(ε) R(ε,k1) ----→ L(k 1 ) R(k1,k1k2) ------→ L(k 1 k 2 ) • • • R(k1•••k β-1 ,k1•••k β ) ------------→ L(w)) = f -{ g 1 , s 1 , . . . , g α , s α } = { g, s ∈ D Ag (s ) × S | s = δ(s , g), g ∈ D Ag (s ), f g} with s = L(w). -For all j ∈ [1, α], L(w • j) def = s j and R(w, w • j) def = g j .
The tree T F A is defined by saturation of the above rules, and the maps L and R are defined accordingly. A maximal branch w of T F A , R, L is understood as an element of (N \ {0}) ω , such that any (strict) finite prefix of w belongs to T F A . The label of w, written lab(w), is defined as follows:

L(ε) R(ε,k1) ----→ L(k 1 ) R(k1,k1k2) ------→ L(k 1 k 2 ) • • • R(k1•••k β-1 ,k1•••k β ) ------------→ L(k 1 • • • k β ) • • • where w = k 1 k 2 k 3 • • • .
By construction, lab(w) is a maximal computation (respecting the strategy F A ). The following properties are shown in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Section 4] and simply state that T F A , R, L contains all the computations from s that respect the strategy F A .

1. Completeness. For every maximal computation λ starting at s and respecting F A , there is a maximal branch w in T F A , R, L such that λ = lab(w).

2. Soundness. For every maximal branch w in T F A , R, L , there is a maximal computation λ starting at s and respecting F A such that lab(w) = λ.

Let TF A be the tree obtained from

T F A such that k 1 • • • k β in T F A implies 1•k 1 • • • 1•k β in TF A .
The essential step now is to build a derivation skeleton D : TF A → (R 1 ∪ R 2 ) as follows, where all the maximal branches of T F A are infinite.

• D(ε) = s 0 , wf A (s 0 , F A (s 0 )), s 0 , F A (s 0 ) with s 0 = s .

• D(1) = s 0 , F A (s 0 ) , g 1 , s 1 , . . . , g α , s α , where 1, . . . , α ∈ T F A (but α+1 ∈ T F A ), and for all j ∈ [1, α], L(j) = s j and R(ε, j) = g j . By construction of A M,A,s , the rule D( 1) is the unique fork rule starting from s 0 , F A (s 0 ) .

• Let n = 1k 1 1 • • • 1k β .
By construction we can assume that we already have that

D(1k 1 1 • • • k β-1 1) = s , f , g 1 , s 1 , . . . , g α , s α . Let g be equal to R(k 1 • • • k β , k 1 • • • k β • 1)
and f be the restriction of g to A (so f g ). Then,

D(n) = g k β , s k β , wf A (s k β , f ), s k β , f . • Let n = 1k 1 1 • • • 1k β 1 with k 1 , . . . , k β ≥ 1 be such that D(1k 1 1 • • • k β ) = g, s , wf A (s , f ), s , f ∈ R 1 .
Then, D(n) = s , f , g 1 , s 1 , . . . , g α , s α where

k 1 • • • k β 1, . . . , k 1 • • • k β α ∈ T F A (but k 1 • • • k β (α + 1) ∈ T F A )
, and for all j ∈ [1, α],

-L(k 1 • • • k β • j) = s j with β ≥ 1; -R(k 1 • • • k β , k 1 • • • k β j) = g j with β ≥ 1 and 1 ≤ k β ≤ α.
By construction of A M,A,s , D(n) is the unique fork rule starting from s , f .

Given an infinite branch w of D (resp. w of the derivation D based on D), say w = 1k 1 1k 2 1k 3 • • • ∈ N ω , we define the extended computation ext(w, A) as follows. Suppose that the label of such a branch is characterised by the values below. Any prefix of the form 1k 1 1 • • • k β is associated with an update rule whereas any prefix of the form 1k 1 1 • • • k β 1 is associated with a fork rule (not necessarily binary). Intuitively, we specify for each position on the branch which rule is applied next.

D(ε) = s 0 , u 0 , s 0 , f 0 D(1) = s 0 , f 0 , g 1 1 , s 1 1 , . . . , g 1 α1 , s 1 α1 . . . D(1k 1 1 • • • k i ) = g i ki , s i ki , u i ki , s i ki , f i . D(1k 1 1 • • • k i 1) = s i ki , f i , g i+1 1 , s i+1 1 , . . . , g i+1 αi+1 , s i+1 αi+1 . . . Then, ext(w, A) def = s0 u 0 -→ s0, f0 - → g 1 k 1 , s 1 k 1 u 1 -→ s 1 k 1 , f1 - → g 2 k 2 , s 2 k 2 u 2 -→ s 2 k 2 , f2 -→ g 3 k 3 , s 3 k 3 • • •
In [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Lemma 3], the following properties are established.

( †) Completeness. For every maximal computation λ starting at s and respecting F A , there is a maximal branch w in D such that ext(λ, A) = ext(w, A). Note that ext(λ, A) is defined earlier (see Section 4.2.1).

( ‡) Soundness. For every maximal branch w in D, there is a maximal computation λ starting at s and respecting F A such that ext(w, A) = ext(λ, A).

In order to define a proof D in A whose root is labelled by q , b such that all the maximal branches are infinite and the maximal colour that appears infinitely often is 0, it suffices to start from the proof D and to decorate with path formulae Φ ∈ S(Ψ) each node of D (already labelled by a location q). Given Φ ∈ S(Ψ) and a computation λ, by Lemma 6(correction.2) we have (M, λ) |= Φ implies (M, λ ≥1 ) |= s(Φ) when s = λ[0] and Φ has no next-time atomic formulae. Consequently, for each computation λ, we can define an ω-sequence Φ 0 , Φ 1 , . . . ∈ S(Ψ) ω such that for all i ≥ 0,

Φ i = λ[i](• • • (λ[0][Ψ]) • • • ). Moreover, there is I λ ≥ 0 such that Φ I λ , Φ I λ +1 , . . . ∈ {Φ I λ } ω because of Lemma 6(stabilisation). Let w be a maximal branch in D such that ext(w, A) = s 0 u0 - → s 0 , f 0 - → g 1 k1 , s 1 k1 u1 - → s 1 k1 , f 1 - → g 2 k2 , s 2 k2 u2 - → s 2 k2 , f 2 - → g 3 k3 , s 3 k3 • • •
. By ( ‡) above, there is a maximal computation λ starting at s and respecting F A such that ext(w, A) = ext(λ, A). Let Φ 0 , Φ 1 , . . . ∈ S(Ψ) ω be the ω-sequence defined from λ (since it satisfies Ψ, a property inherited from F A ). Let w be the corresponding maximal branch in D where the decoration is performed as follows (overloaded notation):

ext(w, A) = Φ 0 , s 0 u0 - → Φ 0 , s 0 , f 0 - → Φ 1 , g 1 k1 , s 1 k1 u1 - → Φ 1 , s 1 k1 , f 1 - → Φ 2 , g 2 k2 , s 2 k2 u2 - → Φ 2 , s 2 k2 , f 2 - → • • •
Note that for all i ≥ 0, the path formula Φ i appears in two consecutive locations (and this can happen many times if Φ i = Φ j for some j > i). One can check that the colour zero occurs infinitely often along w because Φ i stabilises to a value (say Φ I λ ) such that all the always formulae hold true and make Φ I λ true propositionally. Actually, this is a consequence of (M, λ) |= Ψ and the way the path formulae Φ i 's are computed (see Lemma 6).

(⇐) Reciprocally, assume that there is a proof D whose root is labelled by q , b such that all the maximal branches are infinite and the maximal colour that appears infinitely often is 0. We recall that Σ M is the finite alphabet made of triples s , g, s such that δ(s , g) = s in M . Let L Ψ be the subset of Σ ω M made of ω-sequences (LTL models) satisfying the path formula Ψ. By the bookkeeping of path formulae in S(Ψ), one can establish that the Σ M -projection of every maximal branch belongs to L Ψ . Indeed, suppose that on the branch the projection of S(Ψ) is the ω-sequence Ψ 0 , Ψ 1 , . . .. We have Ψ 0 = s[Ψ] where s is s and there is t ≥ 1 such that for all t ≥ t, we have Ψ t = Ψ t .

Finally, from the coloring map, we know that the satisfaction of always formulae of the form G in Ψ t makes it propositionally true. Moreover, all the underlying visited states satisfy .

By Proposition 1, there is a b-strategy F A w.r.t. s in M such that the set of computations Comp(s , F A ) is included in L Ψ . Consequently, there is a b-strategy F A w.r.t. s in M such that for all λ ∈ Comp(s , F A ), we have (M, λ) |= Ψ. That is, (M, s ) |= A b Ψ.

The model-checking algorithm

We immediately prove the main result of the section.

Theorem 13. For all r ≥ 1, MC(RB±ATL + (r)) is in exptime.

Proof. The proof of Theorem 13 makes use of a labelling algorithm, very similarly to the one in the proof of Theorem 11. However, to decide whether (M, s ) |= A b Ψ, for b ∈ (N ∪ {ω}) r , we first perform a reduction of the dimension by identifying the component in b equal to ω. Then, we take advantage of Lemma 7 in order to check an instance of the corresponding parity game problem for AVASS, which can be done in exponential time. As the number of such requests is only polynomial in the size of the input formula, the whole algorithm runs in exponential time.

The general structure of the proof follows faithfully the (standard) structure of the proof for Theorem 11. Let M = Ag, r, S, Act, act, wf, δ, L be an RB-CGS, and φ be a formula in RB±ATL + (Ag, r). Let us present Algorithm 2, an exponential-time labelling algorithm that computes the finite set {s ∈ S | (M, s) |= φ}.

The algorithm works on the structure of formula φ. The cases for atomic formulae and Boolean connectives are immediate. Then, we consider in detail the case of strategic formulae A b Ψ. Without loss of generality, we assume that Ψ is a Boolean formula in NNF built over atomic path formulae of the form X φ or φ U φ , where φ, φ are state formulae. Let us assume that the maximal state formulae occurring in Ψ are φ 1 , . . . , φ N and the model-checking algorithm has already determined that they hold true exactly on the states in S 1 , . . . , S N , respectively. Let Ψ be the formula obtained from Ψ by replacing each φ i by a fresh atom p i , and M be the RB-CGS obtained from M by modifying the labelling function as in the proof of

A = Q , r, R 1 , R 2 , col : Q → [0, 1]
, and a distinguished location q ∈ Q as explained in Section 4.2.2, but built on M \I , Ψ and s instead. By Lemma 7, (M, s ) |= A b Ψ iff there is a proof whose root is q , b \ I such that all the maximal branches are infinite and the maximal colour that appears infinitely often is 0.

Furthermore, note that we have the following equivalence: (M, s ) |= ∅ b Ψ iff (K M , s ) |= AΨ in CTL + . It is worth noting that strictly speaking, the distinction between ∅ b and A b in Algorithm 2 is not needed because the model-checking instance with CTL + can be formulated as an instance of the parity game problem for AVASS. However, it allows us to pinpoint when a call to a subroutine about AVASS is really needed and when a routine about CTL + suffices. end case 9: end procedure By structural induction, one can show that (M, s) |= φ iff s ∈ MC(M, φ) (as in the proof of Theorem 11). As far as computational complexity is concerned, MC(M, φ) is computed with a recursion depth linear in the size of φ and a polynomial amount of exptime requests. The exptime upper bound is due to Lemma 7 and the complexity analysis following the statement of Lemma 7. Note also that for each occurrence of a subformula ψ of φ, MC(M, ψ) can be computed only once, which guarantees the overall number of calls of the form MC(M, ψ): again, it is sufficient to take advantage of dynamic programming and to work with a table to remember the values MC(M, ψ) already computed (omitted in the present algorithm and already explained earlier). We also take advantage of the fact that the model-checking problem for CTL + is in ∆ P 2 ⊆ exptime.

Because of the results in [START_REF] Courtois | Alternating vector addition systems with states[END_REF][START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], we obtain immediately the following corollary.

Corollary 1. Let r ≥ 4 and |Ag| ≥ 2. Then, MC(RB±ATL + (Ag, r)) is exptimecomplete

The exptime lower bound follows from [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Corollary 1]. Specifically, in the proof of [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]Theorem 3] (by reduction from the control-state reachability for AVASS [START_REF] Courtois | Alternating vector addition systems with states[END_REF]) RB-CGS can be restricted to two agents. The exptime upper bound is from Theorem 13. In the case of one resource, we obtain the following bounds. Theorem 14. For r ∈ {1, 2, 3}, MC(RB±ATL + (r)) is pspace-hard and in exptime.

The pspace lower bound follows from the pspace-hardness of MC(ATL + ) [START_REF] Bulling | Verifying agents with memory is harder than it seemed[END_REF].

Discussion. Though establishing an exptime upper bound for MC(RB±ATL + (1)) reveals a substantial improvement in complexity compared to the 2exptime-completeness of MC(RB±ATL * ) [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], the exact complexity remains open and seems quite challenging. It is still unclear to us whether the developments in [START_REF] Bulling | Verifying agents with memory is harder than it seemed[END_REF]Section 3.2] or in [START_REF] Goranko | Game-theoretic semantics for ATL + with applications to model checking[END_REF] about MC(ATL + ) could be adapted to obtain an optimal upper bound.

As far as the complexity of MC(RB±ATL + (1)) is concerned, it is natural to wonder whether the model-checking problem for Parity-Energy ATL, also called pe-ATL in [START_REF] Della Monica | Parity-energy ATL for qualitative and quantitative reasoning in MAS[END_REF] when the energy bound is bounded below and unbounded above can be used to analyse the complexity of MC(RB±ATL + (1)). MC(pe-ATL) is in ∆ P 2 [START_REF] Della Monica | Parity-energy ATL for qualitative and quantitative reasoning in MAS[END_REF] and it seems hopeless to take advantage of this bound1 to solve efficiently MC(RB±ATL + (1)) since MC(ATL + ) is already pspace-hard [START_REF] Bulling | Verifying agents with memory is harder than it seemed[END_REF]. A notable difference between RB±ATL + (1) and pe-ATL, is that the parity condition in pe-ATL is actually a global fairness condition for all the computations of the CGS.

Further Results: Applications and Extensions

In this section, we leverage on the results from the previous sections to derive interesting consequences for syntactic fragments of our languages (typically by bounding the number of linear-time temporal operators), as well as for logics that happen to be closely related to RB±ATL, RB±ATL + , and RB±ATL * .

Restricting the linear-time temporal operators

In this section, we introduce fragments of RB±ATL + obtained by restricting the set of path formulae by allowing only a finite amount of patterns for each fragment. This is a standard approach in the literature about temporal logics, as it allows us to restrict ourselves to a bounded number of temporal patterns supposedly useful in practice, in order to obtain more tractability results [START_REF] Demri | Temporal Logics in Computer Science[END_REF]. For instance, RB±ATL can be understood as the fragment of RB±ATL + in which the only temporal patterns are X p, p 1 U p 2 and G p. For each fragment (defined below), we establish that its model-checking problem restricted to a single agent and a single resource can be solved in ptime by building upon our algorithm to solve RB±ATL + ({1}, 1).

We recall that the path formulae for RB±ATL + (Ag, r) are obtained from the following grammar: Ψ ::= ¬Ψ | Ψ ∧ Ψ | X φ | φ U φ. Given a finite set O = {⊕ 1 , . . . , ⊕ n } of patterns understood as built-in linear-time temporal operators, we associate to each pattern ⊕ i an arity a i ≥ 1 and an LTL formula Ψ i (p 1 , . . . , p ai ) of temporal depth one (its definition that unambiguously provides a semantics to the operator ⊕ i ). Hence, the formula Ψ i (p 1 , . . . , p ai ) is an LTL formula built from the grammar below, where p, q ∈ AP:

Ψ ::= p | ¬Ψ | Ψ ∧ Ψ | p U q | X p,
We write RB±ATL + O to denote the fragment of RB±ATL + in which path formulae are defined from the grammar below:

Ψ ::= ⊕ 1 (φ 1 , . . . , φ a1 ) | . . . | ⊕ n (φ 1 , . . . , φ an ),
where the φ i 's are state formulae and O = {⊕ 1 , . . . , ⊕ n }.

Let t be the map that transforms RB±ATL + O formulae into RB±ATL + formulae using the definitions for the linear-time temporal operators in O. Namely, t is the identity for propositional variables and it is homomorphic for Boolean connectives. Finally, for all To this end, let us first establish a few properties about RB±ATL + O ({1}, 1). For all i ∈ [1, n], the LTL formula Ψ i (p 1 , . . . , p ai ) is a constant of the logic RB±ATL + O ({1}, 1). Further, Ψ i (p 1 , . . . , p ai ) can be put in NNF in linear-time in the size of Ψ i (p 1 , . . . , p ai ); and since ¬ X p is logically equivalent to X ¬p and ¬(p U p ) is logically equivalent to G ¬p ∨(¬p U(¬p∧¬p )), Ψ i (p 1 , . . . , p ai ) is logically equivalent to a path formula Ψ i (p 1 , . . . , p ai ) in NNF such that the negation ¬ occurs only in front of propositional variables, and the atomic formulae have one of the forms X C, G C, and C U C , with C, C being conjunctions of literals. In particular, Ψ i (p 1 , . . . , p ai ) can be computed in linear-time in the size of Ψ i (p 1 , . . . , p ai ), also by using the fact that X and G distributes over ∧. As in the proof of Lemma 5, guessing which atomic formulae in Ψ i hold to evaluate Ψ i to true, amounts to guess a conjunction of the form

⊕ i ∈ O, we have t(⊕ i (φ 1 , . . . , φ ai )) def = Ψ i (t(
X C 0 ∧ G C 0 ∧ (C 1 U C 1 ) ∧ • • • ∧ (C m U C m ),
for some m ∈ N, where the C i 's and C j 's are arbitrary conjunctions of literals (empty conjunctions are equivalent to ). Each conjunction above can be understood as a propositional valuation on the path formula Ψ i (p 1 , . . . , p ai ), and because Ψ i (p 1 , . . . , p ai ) is fixed, the number of relevant conjunctions that need to be considered is exponential in the size of Ψ i but, more importantly, it is a constant for the logic RB±ATL + O ({1}, 1). Hence, as explained in the proof of Lemma 5, checking whether (M, s) |= {1} b ⊕ i (φ 1 , . . . , φ ai ) holds amounts to invoke a constant number of instances of GREACH(1-VASS). This constant number depends on the number of valuations/conjunctions satisfying Ψ i (p 1 , . . . , p ai ) and on the constant number of guesses (see again the proof of Lemma 5) to construct the instances of GREACH(1-VASS). Hence, in the labelling algorithm from the proof of Theorem 11, the case for formulae of the form {1} b ⊕ i (φ 1 , . . . , φ ai ) requires polynomial time only (assuming that O is fixed), which allows us to get an overall complexity in ptime.

As a corollary, we obtain the main result established in [START_REF] Belardinelli | Resource-bounded ATL: the quest for tractable fragments[END_REF].

Corollary 2. Model-checking RB±ATL({1}, 1) is in ptime.

Obviously, if O is expressive enough for RB±ATL + O to embed CTL, both problems MC(RB±ATL + O ({1}, 1)) and MC(RB±ATL({1}, 1)) are ptime-complete since ptimehardness is inherited from the model-checking problem for CTL [START_REF] Schnoebelen | The complexity of temporal logic model checking[END_REF]. Note also that ptime fragments of ATL + have been investigated in [START_REF] Goranko | Game-theoretic semantics for ATL+ with applications to model checking[END_REF].

Model-checking RB±ATL({1}, 1) is in ptime: a refined algorithm

In Section 5.1, we showed that model-checking RB±ATL({1}, 1) is in ptime using instances of the decision problem GREACH(1-VASS). Below, we provide a different polynomial-time algorithm for solving MC(RB±ATL({1}, 1)) in which we only use instances of CREACH(1-VASS) and NONTER(1-VASS) (instead of the more general decision problem GREACH(1-VASS), which is not necessary for RB±ATL({1}, 1)). The interest of this different proof derives from the particular version of the problem MC(RB±ATL({1}, 1)) we consider in this section, which differs in two points from the problem analysed in Section 5.1. The first point concerns the use of the linear-time temporal operator release R instead of the always operator G, which provides more generality in the syntax. The second point provides some restriction as we assume that in the input RB-CGS, there is some idle action idle that can be triggered from any state and for any agent and such that its cost is zero. The latter hypothesis has been assumed in [START_REF] Belardinelli | Resource-bounded ATL: the quest for tractable fragments[END_REF], following developments in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], and it happens to be essential to use instances of CREACH(1-VASS). The algorithm presented below appears in [START_REF] Belardinelli | Resource-bounded ATL: the quest for tractable fragments[END_REF] and compared to the algorithm underlying the proof of Corollary 2, it is designed to be implemented more efficiently. Hereafter, for every b ∈ N ∪ {ω}, we write b φ instead of {1} b φ.

As done in Section 4, given an RB-CGS M = {1}, S, Act, 1, act, wf, δ, L with a single agent and a single resource, the corresponding 1-VASS V M = S, 1, R V is such that q u -→ q ∈ R V iff there is some action a ∈ act(q, 1) such that δ(q, a) = q and wf (q, 1, a) = u. Similarly, we write K M = S, R, L K to denote the Kripke structure such that qRq iff there is some action a ∈ act(q, 1) such that δ(q, a) = q and L K (q) = {q} (by a slight abuse of notations, we assume that AP = Q). Note that, thanks to the idle action, K M is now a total Kripke structure, i.e., every world has at least one successor.

We now investigate the relationship between computations in M and runs in V M and in K M , respectively. Below, given a b-consistent computation q 0 a0 -→ q 1 a1 -→ q 2 • • • , the sequence of associated resource values is denoted by (v i ) i∈N . We recall that v 0 = b and v i+1 = v i + wf (q i , 1, a i ) for all i ≥ 0. Lemma 8. Let M be an RB-CGS with a single agent and a single resource.

(I) Let q 0 a0 - → q 1 a1 - → q 2 • • • be a b-consistent computation associated to the family (v i ) i∈N of resource values. If b ∈ N, then q 0 , v 0 -→ q 1 , v 1 -→ q 2 , v 2 • • • is an infinite run in V M ; otherwise (i.e., b = ω) q 0 - → q 1 - → q 2 • • • is an infinite path in K M .
Lemma 10. Let M be an RB-CGS for RB±ATL({1}, 1), S 1 , S 2 ⊆ S with s ∈ S, and b ∈ N.

(I) There is a b-consistent computation starting at s in M such that its projection on S is in S * 1 • S 2 • S ω (understood as an ω-regular expression) iff for some s ∈ S 2 , (V S1∪S2 M , s, b , s ) is a positive instance of CREACH(1-VASS).

(II) There is an ω-consistent computation starting at s in M such that its projection on

S is in S * 1 • S 2 • S ω iff in CTL, we have (K M , s) |= E( s ∈S1 s ) U( s ∈S2 s ). Proof. (I) ⇒ Suppose that λ = q 0 a0 - → q 1 a1 - → q 2 • • • is a b-consistent computation starting at s in M such that its projection on S is in S * 1 •S 2 •S ω . By Lemma 8.(I), q 0 , v 0 - → q 1 , v 1 - → q 2 , v 2 • • • is an infinite run in V M for v 0 = b, whose projection is in S * 1 • S 2 • S ω and q n ∈ S 2 . Then, clearly (V S1∪S2 M , s, b , q n )
is a positive instance of CREACH(1-VASS). For the ⇐-direction the proof is similar, while using Lemma 8.(II) and the idle action that allows us to extend a finite trace to an infinite one.

(II) ⇒ Suppose that λ = q 0 a0 -→ q 1 a1 -→ q 2 • • • is an ω-consistent computation starting in s = q 0 such that its projection on S is in S * 1 • S 2 • S ω . By Lemma 8.(I), q 0 -→ q 1 -→ q 2 • • • is an infinite path in K M . Hence, the CTL formula E( s ∈S1 s ) U( s ∈S2 s ) is true at s in K M . For the ⇐-direction the proof is similar, while using Lemma 8.(III). This is again a consequence of Lemma 8 but here, we have to use the fact that the distinguished action idle is enabled in any state (which is handy to extend to infinity a finite witness run). Finally, we consider the linear-time temporal operator R. (II) There is an ω-consistent computation starting at s in M such that its projection on S is in S ω 2 ∪ (S 2 \ S 1 ) * • (S 1 ∩ S 2 ) • S ω iff in CTL, we have

(K M , s) |= (E G s ∈S2 s ) ∨ E( s ∈(S2\S1) s ) U( s ∈S1∩S2
s ).

CTL with the release operator R is known to also admit a ptime model-checking problem (see, e.g., [START_REF] Demri | Temporal Logics in Computer Science[END_REF]Chapter 7]). The CTL formula in Lemma 11(II) can be equivalently replaced by E(

s ∈S1 s ) R( s ∈S2
s ).

In Algorithm 3 below, we shall use the release operator R in CTL in order to simplify the involved formulae. end case 20: end procedure • act(q, 1) = {(q , u, q ) ∈ R | q = q };

• for every (q, u, q ) ∈ act(q, 1), wf (q, 1, (q, u, q )) = u;

• for every (q, u, q ) ∈ act(q, 1), δ(q, (q, u, q )) = q .

Notice that, by the assumption of seriality in Definition 17, for every q ∈ Q, act(q, 1) = ∅, as required by Definition 3 of RB-CGS.

We now state the following auxiliary lemma, whose proof follows immediately by the definitions of A M and M A above. -→ s 2 • • • , with associated resource values ( v i ) i∈N , such that s 0 = s and for every i ≥ 0, ρ i = (s i , v i ) and v i+1 = v i + wf (s i , 1, a i ). It is not difficult to check that ρ = ρ λ .

The proof for item (2) is similar. By using Lemma 12 we can finally prove that RB±ATL * ({1}, r) and RBTL * are closely related semantically.

Theorem 19.

1. For every state formula φ and path formula Ψ in RBTL * , and model A with state q ∈ Q and run ρ,

(A, q) |= φ iff (M A , q) |= τ (φ) (A, ρ) |= Ψ iff (M A , λ ρ ) |= τ (Ψ)
where λ ρ is obtained from ρ as in Lemma 12.(2a). where ρ λ is obtained from λ as in Lemma 12.(1a).

Proof. Both items can be proved by mutual induction on the structure of formulae. The base cases for propositional variables and the inductive cases for Boolean and temporal operators are immediate. Item (1), case for φ = b Ψ. ⇒ Suppose that (A, q) |= φ, that is, for some run ρ from (q, b), (A, ρ) |= Ψ. By Lemma 12.(2a), in M A we can construct a b-consistent computation λ ρ from q such that (M A , λ ρ ) |= τ (Ψ) by the induction hypothesis. This means that (M A , q) |= {1} b τ (Ψ) = τ ( b Ψ) = τ (φ). ⇐ If (M A , q) |= {1} b τ (Ψ) = τ (φ), then for some b-consistent computation λ, (M A , λ) |= τ (Ψ). By Lemma 12.(2b), λ = λ ρ for some run ρ from (q, b) in A, and by induction hypothesis we obtain (A, ρ) |= Ψ, that is, (A, q) |= φ. As a consequence of Theorem 19, RBTL * and the restriction of RB±ATL * to a single agent are essentially the same logic in the sense that their translations according to τ, τ are semantically faithful when single-agent RB-CGS are understood as RBTL * models (i.e., a VASS with a valuation). A similar result holds for RBTL (resp. RBTL + ) and single-agent RB±ATL (resp. RB±ATL + ), as τ, τ preserves these fragments. Based on the correspondences established in Theorem 19 and the fact that translations τ, τ are polynomial, we derive the complexity results for the model-checking problem in Fig. 6. Notice that, for all numbers of resources, we have tight complexity bounds. Moreover, for the case of a single resource, the model-checking problem is no harder than for the corresponding fragment of CTL * . Thus, we conclude that reasoning about a single resource in CTL * and fragments comes at no extra computational cost.

Conclusions and Future Work

In this work, we have pushed further our understanding of the relationship between reasoning about resources in ATL-logics and decision problems for vector addition systems with states (VASS) or variants. This allowed us to establish new complexity results about model-checking problems for ATL-logics with resources and to identify several fragments with low complexity. More precisely, we proved that the model-checking problem for RB±ATL + ({1}, 1) is in ∆ P 2 (Theorem 11) by essentially introducing the generalised reachability problem for 1-VASS, and showing it to be in ptime (Theorem 10). Hence, MC(RB±ATL + ({1}, 1)) is no more complex than MC(CTL + ), despite the greater expressive power due to the presence of one resource. Additionally, we have established that the model-checking problem for RB±ATL({1}, 1) is ptime-complete and actually this holds for any fragment of RB±ATL + ({1}, 1) with a fixed finite set of linear-time temporal operators (see Section 5.1). For r ≥ 1, we proved MC(RB±ATL + (r)) to be in exptime, with an identical upper bound for its subproblem MC(RB±ATL(r)). To show this, we presented a reduction to the parity game problem for AVASS that is optimal complexity-wise, so that we avoid the doubly-exponential blow-up observed when defining the reduction from MC(RB±ATL * ) in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]. When r ≥ 4, we obtain exptime-completeness (Corollary 1).

Our main contributions are directed towards reducing the complexity gaps for many meaningful fragments of RB±ATL * and identifying fragments with a tractable modelchecking problem. Apart from the application to practical case studies that would take advantage of our identified tractable fragments and associated algorithms, here are research directions for future work.

• What is the precise complexity of MC(RB±ATL + (Ag, 1)) with arbitrary finite sets Ag of agents? Currently, this problem is known to be in exptime for |Ag| ≥ 2 and pspace-hard from MC(ATL + ) [START_REF] Bulling | Verifying agents with memory is harder than it seemed[END_REF]). However, it is an open problem whether there is a decision procedure running in polynomial space. To this end, refined analyses from [START_REF] Chatterjee | Energy parity games[END_REF][START_REF] Malvone | Concurrent multi-player parity games[END_REF][START_REF] Colcombet | Perfect half space games[END_REF] might help.

• It is well-known that CTL and CTL + are equally expressive [START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF], and this result extends to ATL and ATL + [START_REF] Bulling | Verifying agents with memory is harder than it seemed[END_REF]. In both cases, the characterisation of the complexity for the respective model-checking problem differs. It is an open problem whether RB±ATL(Ag, r) and RB±ATL + (Ag, r), for |Ag| ≥ 2 and r ≥ 1, are equally expressive.

• Another challenging issue consists in characterising the complexity of the problem MC(RB±ATL(Ag, 1)) for arbitrary finite sets of agents (currently known to be in pspace for |Ag| ≥ 2 [START_REF] Alechina | Model-checking for resource-bounded ATL with production and consumption of resources[END_REF] and ptime-hard from MC(CTL) [START_REF] Schnoebelen | The complexity of temporal logic model checking[END_REF]).

  b and ∅ b , as well as duals [[Ag b ]] and [[∅ b ]], for b ∈ (N ∪ {ω}) r . By Definition 5, the meaning of these operators is as follows: (M, s) |= ∅ b Ψ iff for every computation λ from s, (M, λ) |= Ψ (M, s) |= [[∅ b ]]Ψ iff for some computation λ from s, (M, λ) |= Ψ (M, s) |= Ag b Ψ iff for some b-consistent computation λ from s, (M, λ) |= Ψ (M, s) |= [[Ag b ]]Ψ iff for every b-consistent computation λ from s, (M, λ) |= Ψ Notice that the semantics of operators ∅ b and [[∅

  b

switch : - 1 switch : - 1 Figure 1 :

 111 Figure 1: the resource-bounded CGS in Example 1.

Figure 5 :

 5 Figure 5: Witness runs and path from Lemma 1(3)

Definition 9 .

 9 Let Ψ be a positive Boolean combination of atomic path formulae of the form C U C , X C and G C, where C and C are conjunctions of literals and X be a finite set of atomic formulae of the form C U C , X C or G C. We define the satisfaction relation X |= Ψ based on the standard clauses below (which can be read as the conjunction of the atomic path formulae from X makes Ψ true propositionnally):

(

  I) If (A) holds, then the instance is positive. (II) If (B) holds, then the instance is positive. (III) If the instance is positive, then either (A) or (B) holds.

  n witness positions, non necessarily pairwise different, whence the partition {Y 1 , . . . , Y α }. The satisfaction of the C k 's (first arguments of the U-formulae) is constrained by the implicit ordering Y 1 , .

3 .

 3 Concerning the case (M, s) |= {1} b Ψ for b ∈ N, we have (M, s) |= {1} b Ψ iff (M , s) |= {1} b Ψ , which can be checked in np by Lemma 5.

  return {s ∈ S | s ∈ L(p)} 4:

8 :

 8 ω Ψ: return {s | (K M , s) |= EΨ in CTL + } {1} b Ψ: return {s | (M , s) |= {1} b Ψ with the algorithm in the proof of Lemma 5 } 9:

2 .

 2 If 1 U 2 occurs in Φ and (M, s) |= 2 (resp. (M, s) |= 2 ∨ 1 ) , then replace every occurrence of 1 U 2 in Φ by (resp. by ⊥).

3 .

 3 The clause for handling U( 1 ∧ 2 ) is similar to (2). 4. If X occurs in Φ and (M, s) |= (resp. (M, s) |= ), then replace every occurrence of X in Ψ by (resp. by ⊥).

  Theorem 11: L (p i ) def = S i . Concerning the case (M, s ) |= A b Ψ, for A = ∅, we have (M, s ) |= A b Ψ iff (M , s ) |= A b Ψ . Let I ⊆ [1, r] be the set of components such that b(i) = ω for all i ∈ I. We have (M, s ) |= A b Ψ iff (M \I , s ) |= A b\I Ψ where M \I (resp. b \ I)is obtained from M (resp. b) by removing the components in I. In Algorithm 2, we define

Algorithm 2 - 6 :

 26 RB±ATL + (Ag, r) model checking -1: procedure MC(M, φ) return {s ∈ S | s ∈ L(p)} 4: ¬ψ: return S\ MC(M, ψ) 5: φ 1 ∧ φ 2 : return MC(M, φ 1 )∩ MC(M, φ 2 ) ∅ b Ψ: return {s | K M , s |= AΨ in CTL + } 7:A b Ψ: return {s ∈ S | A , col , q , b \I is a positive instance of the parity game problem for AVASS } 8:

Lemma 11 .

 11 Let M be an RB-CGS for RB±ATL({1}, 1), S 1 , S 2 ⊆ S with s ∈ S, and b ∈ N.(I) There is a b-consistent computation starting at s in M such that its projection on S is inS ω 2 ∪ (S 2 \ S 1 ) * • (S 1 ∩ S 2 ) • S ω iff either (V S2 M , s, b ) is a positive instance of NONTER(1-VASS) or for some s ∈ S 1 ∩ S 2 , (V S2 M , s, b , s ) is a positive instance of CREACH(1-VASS).

1 : 2 :φ of 3 :b ψ 1 U ψ 2 :ω ψ 1 U ψ 2 :∅ ω ψ 1 U ψ 2 :∅ b ψ 1 U ψ 2 :b ψ 1 R ψ 2 :

 1231212121212 procedure GMC(M, φ) case p: return {s ∈ S | s ∈ L(p)} 4: ¬ψ: return S \ GM C(M, ψ) 5:ψ 1 ∧ ψ 2 : return GM C(M, ψ 1 ) ∩ GM C(M, ψ 2 ) 6: b X ψ: return {s | ∃ a ∈ act(s, 1), 0 ≤ b+wf (s, 1, a), δ(s, a) ∈ GM C(M, ψ)} 7: ω X ψ: return {s | ∃ a ∈ act(s, 1), δ(s, a) ∈ GM C(M, ψ)} 8: ∅ ω X ψ: return {s | ∀ a ∈ act(s, 1), δ(s, a) ∈ GM C(M, ψ)} 9: ∅ b X ψ: return {s | ∀ a ∈ act(s, 1), δ(s, a) ∈ GM C(M, ψ)} 10: S 1 := GM C(M, ψ 1 ); S 2 := GM C(M, ψ 2 ); return {s ∈ S | ∃ s ∈ S 2 s.t. (V S1∪S2 M , s, b , s ) is a positive 11: inst. of CREACH(1-VASS) } 12: S 1 := GM C(M, ψ 1 ); S 2 := GM C(M, ψ 2 ); return {s ∈ S | K M , s |= E( s ∈S1 s ) U( s ∈S2 s )}13: S 1 := GM C(M, ψ 1 ); S 2 := GM C(M, ψ 2 ); return {s ∈ S | K M , s |= A( s ∈S1 s ) U( s ∈S2 s )} 14: S 1 := GM C(M, ψ 1 ); S 2 := GM C(M, ψ 2 ); return {s ∈ S | K M , s |= A( s ∈S1 s ) U( s ∈S2 s )} 15: S 1 := GM C(M, ψ 1 ); S 2 := GM C(M, ψ 2 );return {s ∈ S | (V S2 M , s, b ) is a positive inst. of NONTER(1-VASS) } ∪{s ∈ S | ∃ s ∈ S 1 ∩ S 2 s.t. (V S2 M , s, b , s ) is a positive inst. of CREACH(1-VASS) } 16: ω ψ 1 R ψ 2 : S 1 := GM C(M, ψ 1 ); S 2 := GM C(M, ψ 2 ); return {s ∈ S | K M , s |= E( s ∈S1 s ) R( s ∈S2 s )} 17: ∅ ω ψ 1 R ψ 2 : S 1 := GM C(M, ψ 1 ); S 2 := GM C(M, ψ 2 ); return {s ∈ S | K M , s |= A( s ∈S1 s ) R( s ∈S2 s )}18: ∅ b ψ 1 R ψ 2 : S 1 := GM C(M, ψ 1 ); S 2 := GM C(M, ψ 2 ); return {s ∈ S | K M , s |= A( s ∈S1 s ) R( s ∈S2 s )} 19:

Lemma 12 . 1 . 2 .s 2

 12122 Given a single-agent RB-CGS M , state s ∈ S, and budget b ∈ (N ∪ {ω}) r , (a) for every b-consistent computation λ starting at s in M , in A M there exists a run ρ λ from (s, b) such that for every i ≥ 0, (λ i , v i ) → (λ i+1 , v i+1 ) with v i+1 = v i + wf (λ i , 1, a i ) and λ i ai -→ λ i+1 . (b) for every run ρ from (s, b) in A M , ρ = ρ λ for some b-consistent computation λ starting at s in M . Given a model A for RBTL * , state q ∈ Q, and budget b ∈ (N ∪ {ω}) r , (a) for every run ρ from (q, b) in A, in M A there exists a b-consistent computation λ ρ such that for every i ≥ 0, λ ρ [i] (ρi, u,ρi+1) -------→ λ ρ [i + 1] with (ρ i , v i ) → (ρ i+1 , v i+1 ) and v i+1 = u + v i .(b) for every b-consistent computation λ starting at q in M A , λ = λ ρ for some run ρ starting at (q, b) in A.Proof. (sketch) 1a) Let λ be a b-consistent computation from s ∈ S, say λ = s 0 • • • with the associated resource values ( v i ) i∈N . We recall that v 0 = b and v i+1 = v i + wf (s i , 1, a i ) for all i ≥ 0. Let us consider the sequence (s0 , v 0 ) -→ • • • -→ (s i , v i ) • • • . By definition of A M , for all i ≥ 0, we have (s i , v i ) ti -→ (s i+1 , v i+1 ) in A M with t i = s i wf (si,1,ai) ------→ s i+1 . Consequently, ρ is a run in A M fromthe configuration (s, b) as s = s 0 and b = v 0 . 1b) Consider a run ρ from (s, b) in A M , and the b-consistent computation λ = s 0

2 .

 2 For every state formula φ and path formula Ψ in RB±ATL * , and single-agent RB-CGS M with state s ∈ S and computation λ,(M, s) |= φ iff (A M , s) |= τ (φ ) (M, λ) |= Ψ iff (A M , ρ λ ) |= τ (Ψ )

Item ( 2 )

 2 , case for φ = {1} b Ψ . ⇒ Suppose that (M, s) |= φ , that is, for some b-consistent computation λ from s, (M, λ) |= Ψ . ByLemma 12.(1a), inA M we can construct a run ρ λ from (s, b) such that (A M , ρ λ ) |= τ (Ψ ) by induction hypothesis. Hence, (A M , s) |= b τ (Ψ ) = τ (φ ). ⇐ Suppose that (A M , s) |= τ (φ ) = b τ (Ψ ).That is, for some run ρ from (s, b), (A M , ρ) |= τ (Ψ ). By Lemma 12.(1b) we have that ρ = ρ λ for some b-consistent computation λ such that (M, λ) |= Ψ by induction hypothesis. Hence, (M, s) |= φ .Case for φ = ∅ b Ψ . ⇒ Suppose that (A M , s) |= τ (φ ) = [ ω]τ (Ψ ). That is, for some run ρ from (s, ω), (A M , ρ) |= τ (Ψ ). By Lemma 12.(1b) we have that ρ = ρ λ for some ω-consistent computation λ from s such that (M, λ) |= Ψ by induction hypothesis. Hence, (M, s) |= φ . ⇐ Suppose that (M, s) |= φ , that is, for some computation λ from s, (M, λ) |= Ψ . By Lemma 12.(1a), in A M there exists a run ρ λ from (s, ω) such that (A M , ρ λ ) |= τ (Ψ ) by induction hypothesis. Hence, (A M , s) |= [ ω]τ (Ψ ) = τ (φ ).

  while a state is labelled with charge i if drone d i has charged as previous action (we can keep track of this information with an extra bit of memory in the system state).

  Figure 3: The complexity of model-checking RB±ATL + (Ag, r). Results proved in this paper are in boldface.

		12, Th. 2 and 3]	expspace-c. [12, Th. 4]
	≥ 4 3	in exptime (Th. 13) exptime-h. [12, Th. 2 and 3]	pspace-c [12, Cor. 2] [27]
	2	in exptime (Th. 13)
	1	pspace-h. (from ATL + [27])	in ∆ P 2 (Th. 11) 2 -h. (from CTL + [30]) ∆ P

r\|Ag| ∞ ≥ 2 1 ∞ in 2exptime [12, Th. 7] expspace-c. [12, Th. 8] ≥ 1 2exptime-h. (from ATL * ) in pspace ([12, Cor. 2] & Th. 19) pspace-h. (from CTL * ) Figure 4: The complexity of model-checking RB±ATL * (Ag, r). Results proved in this paper are in boldface.

  φ 1 ), . . . , t(φ ai )). The satisfaction relation |= for RB±ATL + O is essentially defined as for RB±ATL + except for formulae of the form ⊕ i (φ 1 , . . . , φ ai ). More precisely, (M, s) |= φ in RB±ATL + {⊕ 1 , ⊕ 2 , ⊕ 3 } of patterns, with a 1 = 1 and a 2 = a 3 = 2. We define Ψ 1 (p 1 ) ¬(p 1 U p 2 ). The definitions related to ⊕ 1 and ⊕ 2 are well-motivated to capture the formulae of the form A b X φ and A b φ 1 U φ 2 from RB±ATL, respectively. However, the pattern ⊕ 3 is instrumental to capture formulae of the form A b G φ. Indeed, in LTL, G p is logically equivalent to ¬( U ¬p) and therefore A b G p from RB±ATL is logically equivalent to A b ⊕ 3 ( , ¬p) in RB±ATL + O . It is even immediate to add the release operator R, not necessarily native to RB±ATL, as A b φ 1 R φ 2 is captured by A b ⊕ 3 (¬φ 1 , ¬φ 2 ) in RB±ATL + O (recall that state formulae are closed under negation, unlike path formulae in RB±ATL + O ). The main result of interest herein about RB±ATL + O is stated below (with associated arities and definitions). Observe that RB±ATL is equal to RB±ATL + O for some O. Theorem 15. Let O = {⊕ 1 , . . . , ⊕ n } be a finite fixed set of patterns. The modelchecking problem for RB±ATL +

	O	def ⇔ (M, s) |= t(φ) in
	RB±ATL + .
	Let us explain how RB±ATL can be viewed as a syntactic fragment of RB±ATL +	O
	for some finite set O =

def = X p 1 , Ψ 2 (p 1 , p 2 ) def = p 1 U p 2 and Ψ 3 (p 1 , p 2 ) def = O ({1}, 1) is in ptime.

Proof. Let O = {⊕ 1 , . . . , ⊕ n } be a fixed finite set of patterns (with associated definitions Ψ 1 , . . . , Ψ n and the corresponding map t parameterised by O). The ptime upper bound is obtained by running exactly the algorithm described in the proof of Theorem 11 and by taking advantage of the fact that O is fixed in RB±ATL + O ({1}, 1) so that the modelchecking algorithm runs in ptime.

  (from CTL) ∆ P 2 -h. (from CTL + [30]) pspace-h. (from CTL * ) Figure 6: The complexity of model-checking RBTL, RBTL + , and RBTL * .

	r	RBTL	RBTL +	RBTL *
	∞		expspace-c. [12, Th. 4]
	≥ 4		in pspace [12, Cor. 2]
	3		pspace-h. [29] [27]
	2
	1	in ptime (Cor. 2) ptime-h.	in ∆ P 2 (Th. 11)	in pspace ([12, Cor. 2])

We thank Dario Della Monica for checking that the np upper bound stated in [69, Theorem 5.1] is actually an ∆ P

upper bound in view of the algorithm developped in [69, Section 4].

Acknowledgment. We would like to deeply thank the anonymous referees for all their suggestions that helped us a lot improve the quality of this document. We would like also to thank Michael Blondin (University of Sherbrooke) for pointing us to [31] and for insightful feedback, as well as the anonymous referees at AAMAS'19 and ECAI'20 for their suggestions and comments that helped us improve the conference papers [39] and [40]. Francesco Belardinelli acknowledges the support of the ANR JCJC Project SVeDaS (ANR-16-CE40-0021) and Stéphane Demri acknowledges the support of the Centre National de la Recherche Scientifique (C.N.R.S.).

(small size) By definition, Ψ ∈ S(Ψ), as Ψ can be viewed as obtained from Ψ with no application of s(•) or s [•]. Each original subformula of Ψ evolves in Φ ∈ S(Ψ) in three possible ways: [START_REF] Alur | Alternating-time temporal logic[END_REF] it remains as it is; [START_REF] Alur | MOCHA user manual[END_REF] it is substituted by ⊥; or (3) it is substituted by (actually simplifications are also performed when ⊥ ∨ . . . or ∧ . . . occur), whence |S(Ψ)| is in O(3 |Ψ| ). (stabilisation) As the size of s(Ψ) is at most the size of Ψ, for any sequence s 1 , s 2 , . . ., the size of

stabilises from some position i. As any transformation strictly decreases the number of literals, we get the stabilisation of the path formula.

Let us explain how Q is defined and used. By definition, Q is equal to S(Ψ) × Q so that each Φ ∈ S(Ψ) has its own copy of A M,A,s . A location Φ, q is intended to follow the rules of A M,A,s to satisfy the path formula Φ. In order to update Φ, when the proof visits a next location q attached to the state s ∈ S, the next location in Q becomes s (Φ), q . The (initial) location q is defined as the pair s [Ψ], s , where s [Ψ] is built from the first three clauses only for defining s(•) (i.e., the atomic path formulae of the form X are exceptionally ignored to start with), which is safe by Lemma 6(correctness.1). Let us explain now how to define the update and fork rules when the locations in S(Ψ) × Q are involved (Φ ∈ S(Ψ)).

For every Φ ∈ S(Ψ), the update rules (related to the actions of coalition A) do not modify the first argument Φ as no next location is reached yet.

Note that we move from Φ to s i (Φ) in order to simplify Φ based on literals holding at s i . We perform such an update for all the branches. Consequently, a proof involving locations in S(Ψ)×Q leads to a proof in A M,A,s when the first component Φ in Φ, q is ignored. For all Φ, q in Q , we have col ( Φ, q ) def = 0 if {G 1 , . . . , G n } |= PROP Φ, where G 1 , . . . , G n are the G-formulae in Φ and |= PROP is the propositional entailment (which can be checked in logspace [START_REF] Lynch | Log Space recognition and translation of parenthesis languages[END_REF]). Otherwise, col ( Φ, q ) def = 1. So for acceptance, we want to use locations Φ, q with colour zero to be the only ones to occur infinitely often (and actually to stabilise on such a path formula Φ). In particular, by definition, col ( ⊥, q ) def = 1 and col ( , q ) def = 0. The rationale for the definition of col is simply that an infinite branch of a derivation in A , at some point Φ stabilises and all the states in S attached to the locations on that branch satisfy all the G-formulae in Φ (otherwise some of them would be replaced by ⊥). The colour zero is attached only to locations in Q for which the satisfaction of all the G-formulae entails the satisfaction of the final path formula Φ, see also the paragraph after the presentation of Lemma 6. Correctness of the construction is stated below. Lemma 7. Let b ∈ N r . Then, (M, s ) |= A b Ψ iff there is a proof in A whose root is labelled by q , b and all the maximal branches are infinite and the maximal colour that appears infinitely often is 0. Moreover, (M, s

Then, by definition of V M , we have that q i u -→ q i+1 . Moreover, the resource availability v i+1 = v i + u is greater than zero, as the computation is b-consistent, and therefore

this means that in M there is some action a i ∈ act(q i , 1) such that δ(q i , a i ) = q i+1 and wf

Then, by reasoning similarly to point (II) we can show that q 0

Lemma 8 is instrumental to the three following lemmas that are at the heart of the model-checking algorithm for RB±ATL({1}, 1). As earlier in the paper, given S 1 ⊆ S, we write V S1 M (resp. K S1 M ) to denote the restriction of V M (resp. K M ) to the states in S 1 only.

Lemma 9. Let M be an RB-CGS for RB±ATL({1}, 1), S 1 ⊆ S with s ∈ S 1 , and b ∈ N.

(I) There is a b-consistent computation starting at s in M that visits only states in

VASS). (II)

There is an ω-consistent computation starting in s in M that visits only states in

) is a positive instance of NONTER(1-VASS). For the ⇐-direction the proof is similar, while using Lemma 8.(II).

(II) ⇒ Suppose that λ = q 0 a0 -→ q 1 a1 -→ q 2 • • • is an ω-consistent computation starting in s = q 0 that visits only states in S 1 . By Lemma 8.(I), q 0 -→ q 1 -→ q 2 • • • is an infinite path in K M . Hence, the CTL formula E G( s ∈S1 s ) is true at s in K M . For the ⇐-direction the proof is similar, while using Lemma 8.(III).

Hence, Lemma 9 is a consequence of Lemma 8, which will be generalised in Lemma 11. Let us focus now on the until operator U.

Proof. (I) ⇒ If there is a b-consistent computation λ starting in s that only visits states in S 2 , then by Lemma 9.(I), (V S2 M , s, b ) is a positive instance of NONTER(1-VASS). On the other hand, if the projection of λ on S belongs to (S 2 \ S 1 ) * • (S 1 ∩ S 2 ) • S ω , then by Lemma 10(I), for some s ∈ S 1 ∩ S 2 , (V

For the ⇐-direction the proof is similar. In particular, if (V S2 M , s, b , s ) is a positive instance of CREACH(1-VASS) for some s ∈ S 1 ∩ S 2 , then by Lemma 10.(I), there is a b-consistent computation λ starting at s in M such that its projection on S is in

) is a positive instance of NONTER(1-VASS), by Lemma 9(I), there is a b-consistent computation λ starting at s in M such that its projection on S is in S ω 2 . (II) The result follows similarly by item (II) in Lemma 9 and 10. Let M = {1}, S, Act, 1, act, wf, δ, L be a resource-bounded CGS, and φ be a formula in RB±ATL({1}, 1). Let us present below Algorithm 3 that is a polynomial-time algorithm that computes the finite set GM C(M, φ) (by default, b ∈ N).

By induction, it can be shown that (M, s) |= φ iff s ∈ GM C(M, φ). Lemma 10 and Lemma 11 are used to prove the soundness of the subroutines for U and R, with b ∈ N∪{ω}, respectively. When the strategy modality is ∅ b , it behaves as the standard path quantifier A in CTL * , which is reflected in Algorithm 3. As far as computational complexity is concerned, GM C(M, φ) is computed with a recursion depth linear in the size of φ and the control-state reachability and nontermination problems can be solved in polynomial time by Theorem 7 and 8. More precisely, for each occurrence of a subformula ψ of φ, GM C(M, ψ) can be computed only once, which guarantees the overall number of calls of the form GM C(M, ψ) to be at most polynomial: it is sufficient to take advantage of dynamic programming and to work with a table to remember the values GM C(M, ψ) already computed (omitted in the present algorithm, see also the proof of Theorem 11). It is also worth observing that the instances we consider are polynomial in the sizes of M and φ. Finally, we take advantage of the fact that the model-checking problem for CTL including R remains in ptime (see, e.g., [START_REF] Demri | Temporal Logics in Computer Science[END_REF]Chapter 7]).

Consequently, reasoning about a single resource in CTL comes at no extra computational cost. Hence, in principle we can verify specification such as formula (1) in Example 2 efficiently.

Comparison with RBTL and RBTL *

In this section we discuss the resource-bounded temporal logic RBTL * , which extends CTL * by adding resources [START_REF] Bulling | On the (Un-)Decidability of Model-Checking Resource-Bounded Agents[END_REF][START_REF] Bulling | Expressing properties of resource-bounded systems: The logics RBTL * and RBTL[END_REF]. In particular, we show that this logic is essentially the same as single-agent RB±ATL * . While such a result is not surprising, apparently it has so far been overlooked in the literature. Indeed, in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], complexity results are given independently for both RBTL * and single-agent RB±ATL * , even though the two logics will be proved to be translatable one into the other. Such an equivalence allows us to apply results for single-agent RB±ATL to RBTL as well. We first introduce the syntax and semantics of RBTL * as given in [START_REF] Bulling | Expressing properties of resource-bounded systems: The logics RBTL * and RBTL[END_REF].

Definition 16. Given r ≥ 1, the state formulae φ and path formulae Ψ in RBTL * are built according to the following BNF grammar:

where p ∈ AP and b ∈ (N ∪ {ω}) r .

Formulae in RBTL * are understood as the state formulae.

The fragment RBTL of RBTL * is obtained by restricting path formulae just like in the case of RB±ATL:

The fragment RBTL + is defined from RBTL * as RB±ATL + is defined from RB±ATL * in Section 2. In [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF] the interpretation of RBTL * is given on a particular class of models, based on vector addition systems with states.

Definition 17 (Model). A model for RBTL * is a tuple A = Q, r, R, L such that (i) Q, r, R is a serial VASS, i.e., for every q ∈ Q, there exist q ∈ Q and u ∈ Z r such that (q, u, q ) ∈ R; and (ii) L : AP → P(Q) is a labelling function.

The assumption of seriality on models appeared originally in [START_REF] Bulling | Expressing properties of resource-bounded systems: The logics RBTL * and RBTL[END_REF], but it is omitted, for example, in [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF]. Here we assume seriality to facilitate the comparison with RB±ATL * , whose models are also serial by definition.

In a model A, a pseudo-run ρ is an infinite sequence (q 0 , v 0 ) → (q 1 , v 1 ) → . . . such that for all i ≥ 0, there exists (q, u, q ) ∈ R such that q i = q, q i+1 = q , and v i+1 = u + v i (with n + ω = ω). A pseudo-run ρ is a run iff for all i ≥ 0, v i ∈ (N ∪ {ω}) r . This is consistent with the notions used so far.

Definition 18 (Satisfaction relation).

The satisfaction relation |= in model A, for state q ∈ Q, run ρ, p ∈ AP, state formula φ, and path formula Ψ is defined as follows (clauses for Boolean connectives are immediate and thus omitted):

for some i ≥ 0, (A, ρ ≥i ) |= Ψ , and for all 0 ≤ j < i, (A, ρ ≥j ) |= Ψ The model-checking problem for RBTL * takes as inputs a model A, a location q and an RBTL * state formula φ, and asks whether (A, q) |= φ holds. A similar definition can be provided for all relevant fragments of RBTL * .

We now prove that the logics RBTL * and RB±ATL * ({1}, r) are semantically equivalent, in the sense that truth-preserving translations exist between models and formulae. First, consider the translation maps τ and τ between RBTL * and RB±ATL * ({1}, r) such that τ, τ are the identity on AP , they are homomorphic for Boolean and temporal oper- Further, given an RB-CGS M = {1}, AP, S, Act, r, act, wf, δ, L with a single agent 1, define the associated model A M = V M , L for RBTL * such that V M is the VASS associated to M , as defined in Section 4. Symmetrically, given a model A = Q, r, R, L , define the associated single-agent RB-CGS M A = {1}, r, Q, R, act, wf, δ, L (the set of actions is equal to the set of transitions R) such that for every q ∈ Q,