Elena Ivanova
email: elena.ivanova@l2s.centralesupelec.fr

Antoine Girard
email: antoine.girard@l2s.centralesupelec.fr

Lazy Symbolic Controller for Continuous-Time Systems Based on Safe Set Boundary Exploration

Keywords: Safety specifications, Lazy controller synthesis, Symbolic control

In this paper, we present an abstraction-based approach to robust safety controller synthesis for continuous-time nonlinear systems. To reduce the computational complexity associated with symbolic control approaches, we develop a lazy controller synthesis algorithm, which iteratively explores states on the boundary of controllable domain while avoiding exploration of internal states, supposing that they are safely controllable a priory. A closedloop safety controller for the original problem is then defined as follows: we use the abstract controller to push the system from a boundary state back towards the interior, while for inner states, any admissible input is valid. We then compare the proposed approach with the classical safety synthesis algorithm and illustrate the advantages, in terms of run-time and memory efficiency, on an adaptive cruise control problem.

INTRODUCTION

Abstraction-based synthesis approaches attracted a lot of attention from the research community in the last decade. These methods consist in creating a finite-state abstraction (or a symbolic model) for a continuous or a hybrid system and refining the controller synthesized for the abstraction to a controller for the original system [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF]; [START_REF] Belta | Formal Methods for Discrete-Time Dynamical Systems[END_REF]). The replacement of a dynamical system by its abstraction allows us to leverage discrete controller synthesis techniques [START_REF] Cormen | Introduction to Algorithms[END_REF]) to deal with non-linear effects, state-input constraints, and a broad class of specifications, given, for instance, by automata or a temporal logic formula. In this paper, we focus on a safety specification, aiming to keep the system's trajectories within a given safe set. This specification often appears in real-world problems, e.g. temperature regulation in smart-buildings [START_REF] Meyer | Compositional abstraction and safety synthesis using overlapping symbolic models[END_REF], [START_REF] Thavlov | A heat dynamic model for intelligent heating of buildings[END_REF]), blood glucose rate control for diabetic patients [START_REF] Kushner | Models, devices, properties, and verification of artificial pancreas systems[END_REF]), adaptive cruise control [START_REF] Darbha | String stability of interconnected systems: An application to platooning in automated highway systems[END_REF]), [START_REF] Nilsson | Correct-by-Construction Adaptive Cruise Control: Two Approaches[END_REF]), satellite station keeping [START_REF] Weiss | Station keeping and momentum management of low-thrust satellites using mpc[END_REF]).

The symbolic model is usually represented as a finite transition system with a set of states obtained due to a finite partitioning of the original state space. As an abstract set of inputs, one commonly chose a finite number of admissible for the original plant control actions. Then, if a robust reachable tube computed for initial state A and a control action C intersect at the moment τ (a timesampling parameter) with an abstract state B, a state A links with a state B by a transition associated to an input C. If the exact reachable set cannot be found it is replaced by an over-approximation [START_REF] Girard | Reachability of uncertain linear systems using zonotopes. Hybrid Systems: Computation and Control[END_REF], [START_REF] Kurzhanski | Dynamics and Control of Trajectory Tubes[END_REF], [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF], [START_REF] Moor | Abstraction based supervisory controller synthesis for high order monotone continuous systems[END_REF], [START_REF] Meyer | TIRA: Toolbox for interval reachability analysis[END_REF]).

Intuitively, the more accurate abstractions with finer discretization parameters better mimic the original system's behavior, increasing the chance of successful controller synthesis. However, their construction is a more demanding process. Moreover, the computational complexity of the discrete controller synthesis algorithms typically depends on symbolic models' size. Finally, while all these computations are typically handled off-line, a controller obtained via abstraction-based techniques using symbolic models with a large number of states would require a considerable amount of memory for its real-time implementation.

To mitigate these intensive computational requirements, several lazy controller synthesis algorithms were recently introduced. In such approaches, the transitions are explored as needed and computed on the fly during a controller synthesis. In [START_REF] Gol | Languageguided controller synthesis for linear systems[END_REF]; [START_REF] Nilson | Augmented finite transition systems as abstractions for control synthesis[END_REF]; [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]; [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF]; [START_REF] Ivanova | Lazy safety controller synthesis with multi-scale adaptive-sampling abstractions of nonlinear systems[END_REF]) the authors proposed to start with rough abstractions and then iteratively refine them if necessary. In [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]; [START_REF] Ivanova | Lazy safety controller synthesis with multi-scale adaptive-sampling abstractions of nonlinear systems[END_REF]) the controller is synthesized only for reachable from the initial set states. The other authors use structural properties of the dynamics such as monotonicity [START_REF] Coogan | Efficient finite abstraction of mixed monotone systems[END_REF]; [START_REF] Saoud | Efficient synthesis for monotone transition systems and directed safety specifications[END_REF]) or incremental stability [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]) to ease these computations.

In this paper, we first introduce a novel lazy synthesis algorithm for a finite transition system with a safety specification, which avoids exploring a priori controllable states. Then, relying on ideas of adaptive time-sampling techniques [START_REF] Ivanova | Lazy safety controller synthesis with multi-scale adaptive-sampling abstractions of nonlinear systems[END_REF]), we construct an abstraction where only transitions between neighboring states are allowed. We then iteratively explore only boundary states of the controlled area since if all boundary states are controllable, then all internal states are also controllable. We also extend this idea towards a more general case, since no matter which time-sampling approach was used, as soon as a safely controllable boundary is found, the abstract controller can be refined to a safe controller for the original continuous-time system: for the internal states, any admissible input is applicable, while for boundary states we use the abstract controller to push the system back towards the interior. In spirit, this idea is close to Nagumo theorem result [START_REF] Blanchini | Set invariance in control[END_REF]) and extremal aiming principle [START_REF] Subbotin | Generalized Solutions of First Order PDEs: The Dynamical Optimization Perspective[END_REF]), but we benefit from abstraction based approaches to tackle the complex dynamic of the original system. This paper is organized as follows. In Section 2, we present a lazy safety controller synthesis algorithm for finite transition systems. Section 3 provides an abstraction-based approach for a safety controller synthesis for a continuoustime system with bounded disturbance and input-state constraints. The practical implementation of the algorithm and controller refinement are discussed. In Section 4, we consider an illustrative example to show the benefits of the approach.

TRANSITION SYSTEM

Safety Controllers for Finite Transition Systems

Definition 1. A finite transition system is a tuple Σ = (Q, U, F ), consisting of a finite set of states Q, a finite set of inputs U , and a transition relation

F ⊆ Q × U × Q.
For every transition (q, u, q ) ∈ F the state q is named u-predecessor of q and similarly the state q is named u-successor of q. Let F (q, u) denotes the set of all usuccessors of a state q. If there is q ∈ Q, u ∈ U such that | F (q, u) | > 1, then the transition system is called nondeterministic, otherwise it is deterministic. Since F (q, u) may be empty let us introduce a set Enab F (q) = {u ∈ U | F (q, u) = ∅} of all enabled inputs at a state q ∈ Q. We also introduce F (q, U ) = ∪ u∈U F (q, u). Definition 2. A controller for a transition system Σ = (Q, U, F ) is a map C: Q → 2 U , such that C(q) ⊆ Enab F (q) for every q ∈ Q.

We also use notation Dom(C) = {q ∈ Q | C(q) = ∅} for a domain of controller C. If Dom(C) = ∅ the controller is called trivial, otherwise non-trivial. Definition 3. A safety controller for a transition system Σ = (Q, U, F ) and a safe set Q S ⊆ Q is a controller C such that the following two properties hold (1) Dom(C) ⊆ Q S ;

(2) for all q ∈ Dom(C) and for all u ∈ C(q) the inclusion F (q, u) ⊆ Dom(C) is satisfied. Lemma 4. For a given transition system Σ = (Q, U, F ) and a safety specification Q S ⊆ Q, there exists a unique anda function (2) for all q ∈ Dom(C) the inclusion C(q) ⊆ C(q) is satisfied.

Algorithm 1: Classical Safety Controller Synthesis Input: Σ = (Q, U, F ) and a safe set Q S Output: Maximal Safety Controller C 1 begin 2 for q ∈ Q do 3 C(q) = {u ∈ Enab F (q) | F (q, u) ⊂ Q S }; 4 repeat 5 Q C := Dom(C); 6 for q ∈ Q C do 7 C(q) := {u ∈ C(q) | F (q, u) ⊆ Q C }; 8 until fixed point for map C is reached ; 9 return C; Algorithm 2: Lazy Controller Synthesis Input: Σ = (Q, U, F ), a safe set Q S ,
I: Q × 2 Q → {T rue, F alse} Output: A controller C 1 begin 2 for q ∈ Q do 3 C(q) = {u ∈ Enab F (q) | F (q, u) ⊂ Q S }; 4 repeat 5 Q C := Dom(C); 6 for {q ∈ Q C | I(q, Q C ) is False} do 7 C(q) := {u ∈ C(q) | F (q, u) ⊆ Q C };
The maximal safety controller C is the best possible safety controller in the sense that any other controller solving the same safety problem would be more restrictive.

Controller Synthesis

There is a well-known fixed-point algorithm converging to the maximal safety controller C for a given Q S [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF]). However, the classical synthesis procedure (see Algorithm 1) is a very computationally-demanding process. So, to tackle real-world problems, where the huge transition systems should be explored, we have to develop more efficient controller synthesis techniques.

One way to reduce the computational burden is to use lazy synthesis algorithms [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF], [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF][START_REF] Saoud | Efficient synthesis for monotone transition systems and directed safety specifications[END_REF], Ivanova and Girard (2020)), aiming to provide safety controllers, while avoiding non-essential computations. In this paper, we introduce a lazy Algorithm 2, which, in general case, does not return a safety controller. However if the information function I : Q × 2 Q → {T rue, F alse} distinguish a priori controllable on the current iteration states from those which should be explored, then Algorithm 2 synthesise the maximal safety controller.

Theorem 5. Let C 1 and C 2 be controllers computed by the Algorithm 1 and Algorithm 2 correspondingly. Then

(1) in general case for all q ∈ Q, C 1 (q) ⊆ C 2 (q).

(2) if at every iteration of the loop 4-8 of the Algorithm 2, for all q ∈ Q C such that

I(q, Q C ) is T rue the inclusion F (q, u) ⊆ Q C is satisfied for all u ∈ U, then C 1 coincides with C 2 .
The proof of this result can be found in the Appendix.

ABSTRACTION BASED CONTROLLER SYNTHESIS

Problem Statement

A control system Σ = (T, R nx , U, W, f ) consists of a time domain T = [0, +∞), a state space R nx , a compact set U ⊂ R nu , a compact set W ⊂ R nw , and a non-linear function f : R nx × U × W → R nx , such that for any control u(•) ∈ L ∞ (T, U ), any disturbance w(•) ∈ L ∞ (T, W ) and any initial condition x(0) ∈ R nx there exists a unique solution x f (t | x(0), u(•), w(•)), t ∈ T of the following differential equation ẋ(t) = f (x(t), u(t), w(t))
(1) in the sense of Caratheodory. The notation L ∞ (T, S) is used for the space of functions s(•), measurable on T, such that s(t) ∈ S, t ∈ T almost everywhere.

In this paper, we look for admissible safety controllers, which keep all trajectories of the closed-loop system inside a safety set Y . Here the controller is said to be admissible if it is robust against any measurable bounded disturbance w(•) ∈ L ∞ (T, W ) and a solution of the closed-loop system exists.

To synthesize a desirable controller, we use an abstractionbased approach. For the original system, we create a finitestate abstraction (also known as a symbolic model) in such a manner that a controller synthesized for the abstraction can be refined to a controller for Σ = (T, R nx , U, W, f ).

Symbolic Model with Adaptive Time Sampling

This section we construct a finite transition system Σ A = (Q A , U A , F A ), which mimics the dynamic of the original plant Σ = (T, R nx , U, W, f ).

First, we introduce a finite partitioning Q S = {q 1 , . . . , q n } on an internal approximation S of the safety set Y such that S = ∪ n i=1 q i , q i ∩ q j = ∅ for all i = j and define Q A , as follows Q A = Q S ∪ {q us }, where q us = R nx \ S is an unsafe state. Let us remark that, depending on the context, a symbol q represents an abstract state or a subset of the space R nx , corresponding to this abstract state. We will use this duality in notation through the paper for the union of discrete states as well.

Let us formally define a neighborhood of a state q ∈ Q A , as follows,

N A (q) = {q ∈ Q A \ {q} | cl(q) ∩ q = ∅ or q ∩ cl(q ) = ∅}.
Here cl(q) is a closure of a set q ⊂ R nx .

Then for every q ∈ Q S we consider a finite set U S (q) = {u 1 , . . . , u m } ⊆ U and define for every u ∈ U S (q) a set of all reachable set

Reach(t | q, u(•)) = {x ∈ R nx | ∃ x(0) ∈ q and ∃ w(•) ∈ L ∞ ([0, t], W ) such that x f (t | x(0), u(•), w(•))
= x} corresponding to an initial set q, a constant control function u * : [0, t] → u and all admissible disturbances w(•). Since exact computation of reachable set is rarely possible its over-approximation Reach(t | q, u) is usually used to build symbolic models. Several methods exist for computing such over-approximations [START_REF] Girard | Reachability of uncertain linear systems using zonotopes. Hybrid Systems: Computation and Control[END_REF], [START_REF] Kurzhanski | Dynamics and Control of Trajectory Tubes[END_REF], [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF], [START_REF] Moor | Abstraction based supervisory controller synthesis for high order monotone continuous systems[END_REF], [START_REF] Meyer | TIRA: Toolbox for interval reachability analysis[END_REF]), and it is always a question of compromise between their precision and a simplicity of implementation.

Choosing U A = ∪ q∈Q S U S (q) as an input set for our abstraction we then say that for every q ∈ Q A , u ∈ U A transition (q, u, q ) ∈ F A if and only if q ∈ Q S , u ∈ U S (q), q ∈ Q A , the intersection q ∩ Reach(τ A q,u | q, u) = ∅, and for all t ∈ [0, τ A q,u ] the condition of a collision avoidance Reach(t | q, u) ∩ (R nx \ Y ) = ∅ is satisfied. Here, we use the adaptive time-sampling and a transition duration defined as τ A q,u = min(τ, τ q,u -ε), where τ is a given parameter which determine the maximal evolution time, while τ q,u is a moment of time

τ q,u = inf t∈[0,+∞) Reach(t | q, u) ⊆ N A (q)
when the over-approximation of reachable set leaves the neighborhood of N A (q). We chose ε < τ q,u arbitrary small to stop evolution just before leaving, while τ should be big enough since it serves only to manage situations when a solution stuck within the box. Let us remark that relation

N A ⊆ Q A × Q A is
symmetric, i.e. for any q, q ∈ Q A we have (q, q ) ∈ N A if and only if (q , q) ∈ N A . Theorem 6. Let for all q ∈ Q C the information function

I A (q, Q C ) = T rue if N A (q) ⊆ Q C F alse if N A (q) ⊆ Q C (2)
Then the controller C 2 given by the Algorithm 2 is the maximal safety controller for transition system Σ A = (Q A , U A , F A ) and a safe set

Q S = Q A \ {q us }.
Proof. Indeed, F A (q, U A ) ⊆ N A (q) for any q ∈ Q C . Consequently, at every iteration of the loop 4-8 of the Algorithm 2, for all q ∈ Q C such that

I A (q, Q C ) is T rue the inclusion F A (q, U A ) ⊆ Q C is satisfied. Hence, from Theorem 5, C 2 is the maximal safety controller. 2
Let us remark that while using lazy synthesis algorithm it reasonable compute the abstraction on the fly. Indeed, at every iteration of Algorithm 2 only boundary states are explored, so there is no need to pre-compute the symbolic model for the internal states.

Arbitrary Time Sampling

In the last section, we have shown that a symbolic model for the original problem can be constructed in a particular way allowing us to compute the maximal safety controller with efficient Algorithm 2 instead of the classical approach. However, with the transition relation defined in section 3.2, we lost flexibility in scaling time sampling parameters independently from space sampling parameters. In this section, we consider a more general case.

Let us define a transition relation F * A ⊆ Q A ×U A ×Q A such that for every q ∈ Q A , u ∈ U A a transition (q, u, q ) ∈ F * A if and only if q ∈ Q S , u ∈ U S (q), q ∈ Q A , the intersection q ∩ Reach(τ * q,u | q, u) = ∅, and for all t ∈ [0, τ * q,u ) the following Reach(t | q, u) ∩ (X \ S) = ∅ is satisfied. Here we assume only that sampling parameter τ * q,u > 0 and it is determined for any given q ∈ Q A , u ∈ U A . Such a definition doesn't put any requirements on a choice of time-sampling parameters and allows us to handle fixed [START_REF] Nilson | Augmented finite transition systems as abstractions for control synthesis[END_REF]), multi-scale [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF]; [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF] or adaptive time-samplings [START_REF] Ivanova | Lazy safety controller synthesis with multi-scale adaptive-sampling abstractions of nonlinear systems[END_REF]) in a unified way. The sampling procedure described in previous section is also obviously incorporated.

It is clear that if we synthesize a controller C 2 for the abstraction Σ * A (Q A , U A , F * A ), the safety set Q S and the information function I A (q, Q C ) with the Algorithm 2 there is no guarantee that C 2 is a safety controller. However, in the next section, we show that C 2 still can be refined towards a continuous time controller, which solves the original safety problem.

Controller Refinement

Let C 2 be a controller given by the Algorithm 2 for transition system Σ * A = (Q A , U A , F * A ) and a safe set

Q S = Q A \ {q us }, while the I A (q, Q C ) is defined as in (2).
For every q ∈ Q A \ Dom(C 2 ), we define C dur 2 (q) = ∅, while if q ∈ Dom(C 2 ) and u ∈ C 2 (q), then the pair (u, τ * u,q ) ∈ C dur 2 (q). Hence, the controller C dur 2 store not only safe inputs, but a real duration of safe transitions.

Let us now define a set of border points

Q B = cl ({x ∈ R nx | ∃ q ∈ Dom(C 2 ) such that x ∈ q and N A (q) ⊆ Dom(C 2 )})
and a set of all internal points

Q I = Dom(C 2 ) \ Q B correspondingly.
We then define a quantizer, associating every border point x ∈ Q B with a unique state of transition system

Q x (x) = {q ∈ Dom(C 2 ) | x ∈ cl(q)}.
Now we are ready to introduce a controller refinement procedure for Σ = (T, R nx , U, W, f ). Let us consider the control input given for all t ∈ [t k , t k+1 ) by

u(t) ∈ U if m k = 0 u(t) = u k , if m k = 1 (3)
where

m k = 0, if x(t k ) ∈ Q I m k = 1, if x(t k ) ∈ Q B (4) (u k , τ k ) ∈ C dur 2 (Q x (x(t k ))), if m k = 1
(5) and the sequence of instants (t k ) is given by t 0 = 0 and

t k+1 = inf{t > t k |Q x (x(t)) ∈ Q B } if m k = 0 t k+1 = t k + τ k if m k = 1 (6)
Theorem 7. All trajectories of closed-loop system (1)-( 6) starting from a Dom(C 2 ) at t = 0 stays within a safe set S for all t ∈ T .

Proof. For any initial condition x(0) ∈ Dom(C 2 ) and any disturbance w(•) ∈ L ∞ (T, W ) the closed-loop trajectory ẋ(t) = f (x(t), u(t), w(t)), t ∈ T can not leave the Dom(C 2 ) without passing through the set Q B , and for every state in Q B there is a controller which brings us back The Zeno behaviour is impossible since being in mode 0 at t = s ∈ T we can either stay in mode 0 for all t ∈ [s, +∞) or switch to mode 1. If we have switched to mode 1 we spent there at least τ k seconds before switching back to mode 0. 2

Let us remark that while we stay inside the set Q I in the mode 0 we can apply any admissible closed-loop control: e.g.

u(t) = v(t, x) We say that a closed-loop control v(t, x) is admissible if the solution of ẋ(t) = f (x(t), v(t, x), w(t)), t ∈ T exists and v(t, x) ∈ U for all t ∈ T and x ∈ R nx .

EXAMPLE

As an illustrative example, let us consider the adaptive cruise control problem for two vehicles moving along a straight line [START_REF] Darbha | String stability of interconnected systems: An application to platooning in automated highway systems[END_REF], [START_REF] Nilsson | Correct-by-Construction Adaptive Cruise Control: Two Approaches[END_REF]). Each vehicle is modeled as a point mass m with velocity changing according to the law

vi = α(F i , v i ) = (F i -(f 0 + f 1 v i + f 2 v 2 i )
)/m, i = 1, 2. In equation above, F i represents a net action of braking and engine torque applied to the wheels, while the second term (f 1 + f 2 v i + f 3 v 2 i ) describes aerodynamic and rolling resistance effects. The net force F i is viewed as a control input for the following vehicle and as a disturbance for the lead one. It is assumed that F i ∈ [a, b], where a = -0.3mg, b = 0.2mg, g is a gravitational constant. Such bounds are consistent with non-emergency braking and acceleration.

First, we do a feedback linearization of the model by introducing F i,lin = α(F i , v i ). Let us assume that the first car doesn't violate speed restrictions

v 1 ∈ [0, v max ]. Since for any v 2 ∈ [0, v max ], zero belongs to [α(a, v 2 ), α(b, v 2 )]
we can always choose a suitable control law to do the same for the second car. Then, we chose a feedback stabilizer as a control law F 2,lin = u 1 + u 2 (v 1 -v 2 ) + u 3 e 1,2 . Here u 1 ∈ R, u 2 , u 3 ≥ 0.

The deviation e 1,2 from the desirable distance between the cars changes according to the following equation ė1,2 = (v 1 -v 2 ) -ḋdes , where d des = hv 2 + r, h > 0. Hence, the constant time headway spacing policy is considered (see Fig. 2 for an illustration).

Finally, the system dynamic is described as follows

v1 = β(F 1,lin , v 1 ) v2 = β(u 1 + u 2 (v 1 -v 2 ) + u 3 e 1,2 , v 2 ) ė12 = v 1 -v 2 -h v2 (7)
where

β(z, v) =    z, if v ∈ (0, v max ) max(z, 0), if v = 0 min(z, 0), if v = v max
Varying the new control parameters u 1 , u 2 , u 3 we want to keep the error e 1,2 in a range [-hv 2 -r, e max 1,2 ], while ensuring that

u 1 +u 2 (v 1 -v 2 )+u 3 e 1,2 ∈ [α(a, v 2 ), α(b, v 2 )].
To construct a symbolic model we introduce on a set

X = [0, v max ] × [0, v max ] × [-hv max -r, e max
1,2 ] a uniform Cartesian partition. Number of intervals in every direction is described by a given parameter n p

x . Intervals on the border are flat, while internal intervals whether semi-closed from the right side or open if they are next to the right border. For example, in first direction we have {0}, (0, η], (η, 2η], . . . , (v max -η, v max ), {v max }, where η = v max /n p x (1). For every state belonging to a safe set Y , we chose n p u different admissible inputs u = [u 1 , u 2 , u 3 ], ensuring that F 2,lin ∈ [α(a, v 2 ), α(b, v 2 )], and apply them τ, τ /2, τ /4 or τ /8 seconds. While computing the symbolic model we use interval over-approximations instead reachable sets. Since the system ( 7) is a mixed-monotone every over-approximation can be easily obtained by solving 6 differential equations [START_REF] Meyer | TIRA: Toolbox for interval reachability analysis[END_REF]).

Setting n p

x = [41, 41, 41], n p u = 18, τ = 1 we use the Algorithm 1 and Algorithm 2 to compute a controllers C 1 and C 2 for the abstraction. In our particular example, we got that the controllable domains Dom(C 1 ) and Dom(C 2 ) coincide. So, both of them are represented on Fig. 3(right), while Fig. 3(left) illustrate the safe specification in the abstract domain. However, our approach, with run-time equals to 70.3 min, is 2.58 times faster than the classical one since it explores 19574 less states. In the Fig. 4, a closed-loop trajectory simulated 500s for a given disturbance is also shown.

CONCLUSION

In this paper, we introduce a novel lazy synthesis algorithm for a finite transition system with a safety specification. The main idea is to iteratively explore only the boundary states of the controllable domain, supposing that internal states are safely controllable a priory. The [20,15,5] worst-case complexity of the proposed algorithm coincides with the complexity of the classical brute-force exploration [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF]), but, our approach is more efficient in practice. Indeed, if a controllable domain for the abstract controller is non-empty then we have a computational gain since we don't explore internal states. Moreover, realtime implementation of a closed-loop controller for the original continuous system is more memory efficient since the information for the internal states is not stored.

APPENDIX

Proof of Theorem 5

Proof. 1) The statement can be proven by induction. Let C i 1 , C i 2 be controllers before i iteration of the loops 4-8 of the Algorithm 1 and Algorithm 2 correspondingly. For all q ∈ Q from lines 2-3 we have C 0 1 (q) = Enab F (q) = C 0 2 (q). Let us show that if C i 1 (q) ⊆ C i 2 (q), q ∈ Q then C i+1 1 (q) ⊆ C i+1 2 (q), q ∈ Q. For any q ∈ Q, the following two cases are possible

• C i 1 (q) = ∅. Then, q / ∈ Q i+1 C1
= Dom(C i 1 ) and C i+1 1 (q) = C i 1 (q) = ∅ ⊆ C i+1 2 (q).

• C i 1 (q) = ∅. Since C i 1 (q) ⊆ C i 2 (q) we have C i 2 (q) = ∅. Then q ∈ Q i+1 C1 = Dom(C i 1 ) and from line 7 it follows C i+1 1 (q) := {u ∈ C i 1 (q) | F (q, u) ⊆ Q i+1 C1 }. (8) and, as a consequence, C i 1 (q) ⊇ C i+1 1 (q). Moreover, if I(q, Q i+1 C2 ) is T rue, then C i+1 2 (q) = C i 2 (q) and we get C i+1 2 (q) ⊇ C i+1 1 (q) since C i 2 (q) ⊇ C i 1 (q). If I(q, Q i+1 C2 ) is F alse then from line 7 of the Algorithm 2 it follows C i+1 2 (q) := {u ∈ C i 2 (q) | F (q, u) ⊆ Q i+1 C2 }. (9) Combining ( 8) and ( 9) with the fact that C i 1 (q) ⊆ C i 2 (q) and Q i+1 C1 = Dom(C i 1 ) ⊆ Dom(C i 2 ) = Q i+1 C2 we finally obtain C i+1 1 (q) ⊆ C i+1 2 (q). 2) Again C 0 1 (q) = Enab F (q) = C 0 2 (q). Supposing that C i 1 (q) = C i 2 (q) for all q ∈ Q let us show that C i+1 1 (q) = C i+1 2 (q) for all q ∈ Q. Since from the previous item C i+1 1 (q) ⊆ C i+1 2 (q), it is enough to prove that C i+1 1 (q) ⊇ C i+1 2 (q). Indeed,

Q i+1 C1 = Dom(C i 1 ) = Dom(C i 2 ) = Q i+1 C1 .
Let us, for simplicity, introduce a notation

Q i+1 C = Q i+1 C1 = Q i+1
C2 . For all q ∈ Q three cases are possible

• if q / ∈ Q i+1 C then C i+1 1 (q) = C i 1 (q) = C i 2 (q) = C i+1 2 (q). • if q ∈ Q i+1 C and I(q, Q i+1 C ) is T rue then C i+1 2 (q) = C i 2 (q) and C i+1 1 (q) := {u ∈ C i 1 (q) | F (q, u) ⊆ Q i+1 C }. For all q ∈ Q i+1 C such that I(q, Q i+1 C ) is T rue the inclusion F (q, u) ⊆ Q i+1 C
is satisfied, consequently, C i+1 (q) = C i (q). Hence, C i+1 2 (q) = C i+1 1 (q), since

C i 2 (q) = C i 1 (q). • if q ∈ Q i+1 C and I(q, Q i+1 C
) is F alse then C i+1 2 (q) := {u ∈ C i 2 (q) | F (q, u) ⊆ Q i+1 C } and C i+1 1 (q) := {u ∈ C i 1 (q) | F (q, u) ⊆ Q i+1 C }. Remembering that C i 2 (q) = C i 1 (q) we get C i+1 2 (q) = C i+1 1 (q). 2

8

  until fixed point on map C is reached ; 9 return C; maximal safety controller C such that for any safety controller C the following hold (1) Dom(C) ⊆ Dom( C);

Fig. 1 .

 1 Fig. 1. A piece of a closed-loop trajectory. Mode 0: a normal line; mode 1: a dashed line. to the Dom(C 2 ) ⊆ S ⊆ Y (see line 7 of the Algorithm 2).The Zeno behaviour is impossible since being in mode 0 at t = s ∈ T we can either stay in mode 0 for all t ∈ [s, +∞) or switch to mode 1. If we have switched to mode 1 we spent there at least τ k seconds before switching back to mode 0. 2

Fig. 2 .

 2 Fig. 2. An illustration for an adaptive cruise control problem.

Fig. 3 .Fig. 4 .

 34 Fig. 3. Left: a safe set. Right: a controllable set.

Table 1 .

 1 Vehicle and safety parameters

	Parameter	Value	Unit	Parameter	Value	Unit
	m	1370	Kg	v max	25	m/s
	f 0	51.0709	N	h	2	s
	f 1	0.3494	N s/m	r	2.5	m
	f 2	0.4161	N s 2 /m 2	e max 1,2	55	m

This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 725144).


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

Stéphane Demri
email: demri@lsv.fr

Resource-bounded ATL: the Quest for Tractable Fragments

Keywords:

Resource-aware logics to represent strategic abilities in multi-agent systems are notoriously hard to handle as they combine strategic reasoning with reasoning about resources. In this work, we begin by providing a general overview of the model-checking results currently available for the Resource-bounded Alternating-time Temporal Logic RB±ATL. This allows us to identify several open problems in the literature, as well as to establish relationships with RBTL-like logics, when RB±ATL is restricted to a single agent. Then, we tackle one such open problem that we deem highly significant: we show that model checking RB±ATL is ptime-complete when restricted to a single agent and a single resource. To do so, we make a valuable detour on vector addition systems with states, by proving new complexity results for their state-reachability and nontermination problems, when restricted to a single counter. Thus, reasoning about resources comes at no computational extra cost in the single-resource, single-agent case.

INTRODUCTION

In recent years, logic-based languages for specifying the strategic behaviours of agents in multi-agent systems have been the object of increasing interest. A wealth of logics for strategies have been proposed in the literature, including Alternating-time Temporal Logic [START_REF] Alur | Alternating-Time Temporal Logic[END_REF], possibly 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 game structures and multi-agent systems [START_REF] Alur | jMocha: A model checking tool that exploits design structure[END_REF][START_REF] Cermák | MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications[END_REF][START_REF] Kacprzak | VerICS 2007 -a Model Checker for Knowledge and Real-Time[END_REF][START_REF] Lomuscio | MCMAS: A Model Checker for the Verification of Multi-Agent Systems[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 multi-agent systems of interest, it is key to account for the resources actions might consume or produce. These considerations have prompted recently investigations in resource-aware logics for strategies. Obviously, there is a long tradition in resource-aware logics that dates back at least to substructural and linear logics (see e.g. [START_REF] Pym | Possible worlds and resources: the semantics of BI[END_REF]). More specifically, in this paper we follow the line of Resource-bounded Alternating-time Temporal Logics [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF][START_REF] Alechina | On the Boundary of (Un)decidability: Decidable Model-Checking for a Fragment of Resource Agent Logic[END_REF][START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF][START_REF] Alechina | Resource Logics with a Diminishing Resource[END_REF][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], which are characterised by two main features: firstly, actions in concurrent game structures are endowed with (positive/negative) costs; and secondly, the standard strategy operators of Alternating-time Temporal Logic (ATL) are indexed by tuples of natural numbers, intuitively representing the resource budget available to agents in the coalition. This account has proved successful in the modelling and verification of a number of multiagent scenarios, where reasoning about resources is critical [START_REF] Alechina | The virtues of idleness: A decidable fragment of resource agent logic[END_REF].

Our motivation for the present contribution is threefold. First of all, in the literature there are several gaps in the results available for the decidability and complexity of the related model checking problem. For instance, if we assume two resources and two agents in our multi-agent system, then model checking is known to be pspacehard and in exptime, but no tight complexity result is available. Our long-term aim is to fill all such gaps eventually. Further, while completing this picture, it is of interest to identify model checking instances that are tractable. Although the notion of tractable 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 model) falls certainly within the description. Finally, complexity results for Resource-bounded ATL appear disseminated in a number of references, and 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) are key in this respect [START_REF] Karp | Parallel program schemata[END_REF].

Our contribution in this paper is also threefold. Firstly, we give an overview of the complexity results currently available for both RB±ATL and RB±ATL * , the two most significant flavours of Resourcebounded ATL. This allows us to point out that, while for RB±ATL * we have tight complexity results for any number of resources and agents, in RB±ATL there are still several open problems, whose solution is not apparent. Secondly, we extend current model checking results for RB±ATL to a more expressive language including the release operator R too. Thirdly, we prove that model checking RB±ATL is ptime-complete, when we reason about a single resource and a single agent. Since we show that this setting is tantamount to the Computation Tree Logic CTL with a single resource, our result means that we can reason about resources in CTL at no extra computational cost. Most interestingly, to prove this main contribution we establish new complexity results for the state-reachability and nontermination problems in VASS with a single counter. The latter can be seen as self-standing contributions in formal methods.

Structure of the paper. In Sect. 2, we present background notions on resource-bounded concurrent game structures and ATLlike logics. In Sect. 2.3, we show that the resource-bounded logics RBTL * and RB±ATL * restricted to a single agent have the same expressive power. In Sect. 3, we prove the main theoretical contributions of the paper. Specifically, in Sect. 3.1 we review the state of the art on model checking RB±ATL. Then, in Sect. 3.2 we show that the state-reachability and nontermination problems for VASS with a single counter are decidable in ptime. Finally, in Sect. 3.3 we leverage on our new results for 1-VASS to prove that model checking RB±ATL with a single agent and a single resource is ptime-complete. Sect. 4 concludes the paper, discusses the complexity of RB±ATL * fragments, and evokes directions for future work.

PRELIMINARIES

Below, we introduce preliminary notions on models for resourcebounded logics, as well as the logical languages themselves. Our presentation follows closely [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF]. In the rest of the paper, N (resp. Z) is the set of natural numbers (resp. integers) and [m,m ′ ] with m,m ′ ∈ Z is the set {j ∈ Z | m ≤ j ≤ m ′ }. For a finite or infinite sequence u ∈ X ω ∪X * of elements in some set X , we write u i for the (i +1)-th element of u, i.e., u = u 0 u 1 . . .. For i ≥ 0, u ≤i is the prefix of u of length i + 1, i.e., u ≤i = u 0 u 1 . . . u i and u ≥i is the suffix of u defined as u ≥i = u i u i+1 . . .. The length of a finite or infinite sequence u ∈ X ω ∪ X * is denoted as |u|, where |u| = ω for u ∈ X ω .

Resource-bounded CGS

Resource-bounded CGS are concurrent game structures [START_REF] Alur | Alternating-Time Temporal Logic[END_REF] enriched with counters and a cost function that assigns a cost (either positive or negative) to every action, thus updating the values of the counters as the system executes. Hereafter we follow closely [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF] and assume a countably infinite set AP of propositional variables (or atoms).

Definition 2.1 (RB-CGS).

A resource-bounded concurrent game structure is a tuple M = ⟨Aд,S,Act,r ,act,cost,δ ,L⟩ such that:

• Aд is a finite, non-empty set of agents (by default Aд = [1,k] for some k ≥ 1); • S is a finite, non-empty set of states s,s ′ , . . . ; • Act is a finite, non-empty set of actions with a distinguished action idle; • r ≥ 1 is the number of resources;

• act : S × Aд → ℘(Act ) \ {∅} is the protocol function, such that for all s ∈ S and a ∈ Aд, idle ∈ act (s,a);

• cost : S × Aд × Act → Z r is the (partial) cost function; that is, cost (s,a, a)
is defined only when a ∈ act (s,a), and moreover, we assume that cost (s,a, idle) = ⃗ 0; • δ : S × (Aд → Act ) → S is the (partial) transition function such that δ is defined for state s and map f : Aд → Act only if for every agent a ∈ Aд, f (a) ∈ act (s,a);

• L : AP → ℘(S ) is the labelling function.
Intuitively, a resource-bounded CGS describes the interactions of a group Aд of agents, who are able to perform the actions in Act according to the protocol function act. The execution of a joint action entails a transition in the system, as specified by the function δ . Moreover, on each transition the values of the r resources are updated according to the cost of the joint action. The idle action is 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 | 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] or Section 3). An RB-CGS M is finite whenever L is restricted to a finite subset of AP. The size |M | of a finite 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.

Given a coalition A ⊆ Aд and 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 a state s ∈ S, the set of joint actions available to Aд is simply denoted as D(s), and the function δ is defined only for such joint actions. We write f ⊑ д if Dom( f ) ⊆ Dom(д), and for every agent a ∈ Dom( f ), д(a) = f (a). Given a joint action f ∈ D A (s), we write out (s, f ) to denote the set of immediate outcomes:

out (s, f ) def = {s ′ ∈ S | for some д ∈ D(s), f ⊑ д and s ′ = δ (s,д)}.
Further, given a joint action f ∈ D A (s) and a state s, the cost of a transition from s by f (w.r.t. coalition A) is defined as

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

f 0 --→ s 1 f 1 --→ s 2 . . . such that for all 0 ≤ i < |λ| -1 we have s i+1 = δ (s i , f i ).

The logics RB±ATL * and RB±ATL

To specify the strategic properties of agents in resource-bounded CGS, we present the logics RB±ATL * and its fragment RB±ATL, which are extensions of 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. Once more, in the presentation of RB±ATL * and RB±ATL we follow [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF]. Syntax. Given a finite set Aд of agents and a number r ≥ 1 of resources, we write RB±ATL * (Aд,r ) to denote the resource-bounded logic with agents from Aд and r resources, whose models are resource-bounded CGS with the same parameters. Definition 2.2 (RB±ATL * ). The state-formulas ϕ and path-formulas ψ in RB±ATL * (Aд,r ) are built according to the following BNF:

ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | ⟨⟨A ⃗ b ⟩⟩ψ ψ ::= ϕ | ¬ψ | ψ ∧ ψ | Xψ | ψ Uψ ,
where p ∈ AP, A ⊆ Aд, and ⃗ b ∈ (N ∪ {ω}) r . The formulas in RB±ATL * (Aд,r ) are understood as the state-formulas.

Clearly, RB±ATL * extends ATL * by indexing the strategic operator ⟨⟨A⟩⟩ with tuple ⃗ b, whose intuitive meaning is that the coalition A can achieve their goal by using at most ⃗ b resources. Alternatively, ⃗ b can be understood as the initial budget of the computations, which is the interpretation followed along the paper. Then, the value ω plays the role of an infinite supply of the resource.

The dual operator [[A

⃗ b ]] is introduced as [[A ⃗ b ]]ψ def = ¬⟨⟨A ⃗ b ⟩⟩¬ψ .
The linear-time operators X and U have their standard readings; while the propositional connectives ∨, →, and temporal operators release R, always G, and eventually F are introduced as usual. For instance, ϕ Rψ def = ¬(¬ϕ U ¬ψ ), and therefore ϕ Rψ shall be equivalent to Gψ ∨ (¬ϕ ∧ ψ ) U(ϕ ∧ ψ ).

We also consider the fragment RB±ATL(Aд,r ) of RB±ATL * (Aд,r ), where path formulas are restricted by ψ ::

= X ϕ | ϕ U ϕ | ϕ R ϕ.
Remark 1. Differently from [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF], we explicitly consider the release operator R in our definition of RB±ATL. Indeed, in [START_REF] Laroussinie | On the Expressiveness and Complexity of ATL[END_REF] it is proved that, differently from the case of the Computation Tree Logic CTL, it is not possible to express R in terms of X and U in ATL. This proof can be quite easily adapted to the case of RB±ATL by assigning cost 0 to all actions. Hence, we explicitly introduce the operator R. In Section 3.3, we will prove that this extra expressivity comes at no cost in terms of the complexity of the verification problem.

Semantics. We provide a formal interpretation of the languages RB±ATL * and RB±ATL by using resource-bounded CGS. Specifically, we need a formal notion of resource-bounded strategy for the interpretation of strategic operators ⟨⟨A ⃗ b ⟩⟩. To start with, a (memoryful) strategy F A for 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

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

Given a bound ⃗ b ∈ (N ∪ {ω}) r and a computation λ = s 0 f 0 --→ s 1 f 1 --→ s 2 . . . in Comp(s, F A ), let the resource availability ⃗ v i at step i < |λ| be defined as: ⃗ v 0 = ⃗ b and for all i < |λ| -1, ⃗ v i+1 = cost A (s i , f i ) + ⃗ v i (assuming n + ω = ω for every n ∈ Z). Then, λ is ⃗ b-consistent iff for all i < |λ|, ⃗ v i ∈ (N ∪ {ω}) r . 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. Since the resource availability depends only on the agents in A, in [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF] this is called the proponent restriction condition (see also [START_REF] Alechina | On the Boundary of (Un)decidability: Decidable Model-Checking for a Fragment of Resource Agent Logic[END_REF]). The set of all the ⃗ b-consistent (infinite) computations is denoted by

Comp(s, F A , ⃗ b). A ⃗ b-strategy F A with respect to s is a strategy such that Comp(s, F A ) = Comp(s, F A , ⃗ b).

Definition 2.3 (Satisfaction relation).

We define the satisfaction relation |= for a state s ∈ S, an infinite computation λ, p ∈ AP, a state-formula ϕ, and a path-formula ψ as follows (clauses for Boolean connectives are standard and thus omitted):

(M,s) |= p iff s ∈ L(p) (M,s) |= ⟨⟨A ⃗ b ⟩⟩ψ iff for some ⃗ b-strategy F A w.r.t. s, for all λ ∈ Comp(s, F A ), (M,λ) |= ψ (M,λ) |= ϕ iff (M,λ 0 ) |= ϕ (M,λ) |= Xψ iff (M,λ ≥1 ) |= ψ (M,λ) |= ψ Uψ ′ iff for some i ≥ 0, (M,λ ≥i ) |= ψ ′ ,
and for all 0 ≤ j < i, (M,λ ≥j ) |= ψ

Clearly, ATL * and ATL [START_REF] Alur | Alternating-Time Temporal Logic[END_REF] can be seen as fragments of RB±ATL * and RB±ATL respectively. In particular, the unindexed strategic operator ⟨⟨A⟩⟩ can be expressed as ⟨⟨A ⃗ ω ⟩⟩. In the sequel, we consider the following decision problem.

Definition 2.4 (Model Checking

). Let k,r ≥ 1, ϕ a formula in RB±ATL * ([1,k],r ) (resp. RB±ATL([1,k],r )), M be a finite RB-CGS for Aд = [1,
k] and r resources, and let s be a state in M. The model checking problem amounts to decide whether (M,s) |= ϕ.

We conclude this section with a remark on the case of a single agent, which will be prominent in what follows.

Remark 2. In the case of a single agent, that is, for Aд = {1}, in our languages we only have modalities ⟨⟨Aд

⃗ b ⟩⟩ and ⟨⟨∅ ⃗ b ⟩⟩, as well as duals [[Aд ⃗ b ]] and [[∅ ⃗ b ]], for ⃗ b ∈ (N ∪ {ω}) r .
By Definition 2.3, the meaning of these operators is as follows: One of our goals is to provide a framework for the complexity classification of (fragments of) RB±ATL(Aд,r ), as well as extensions such as RB±ATL * (Aд,r ). Mainly, we focus on bounding the number of agents or resources, proving novel results along the way.

(M,s) |= ⟨⟨∅ ⃗ b ⟩⟩ψ iff for every computations λ from s, (M,λ) |= ψ (M,s) |= [[∅ ⃗ b ]]ψ iff for some computation λ from s, (M,λ) |= ψ (M,s) |= ⟨⟨Aд ⃗ b ⟩⟩ψ iff for some ⃗ b-consistent computation λ from s, (M,λ) |= ψ (M,s) |= [[Aд ⃗ b ]]ψ iff for every ⃗ b-consistent computation λ from s, (M,λ) |= ψ

When RBTL * comes into play

Below, we present a resource-bounded temporal logic that extends CTL * by adding resources [START_REF] Bulling | Expressing Properties of Resource-Bounded Systems: The Logics RBTL * and RBTL[END_REF][START_REF] Bulling | On the (Un-)Decidability of Model-Checking Resource-Bounded Agents[END_REF]. Then, we show that this logic is essentially the same as single-agent RB±ATL * described in Example 2. While such a result is not surprising, apparently it has so far been overlooked in the literature 1 . 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 2.5. Given r ≥ 1, the state-formulas ϕ and path-formulas ψ in RBTL * are built according to the following BNF:

ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | ⟨ ⃗ b⟩ψ ψ ::= ϕ | ¬ψ | ψ ∧ ψ | Xψ | ψ Uψ ,
where p ∈ AP and ⃗ b ∈ (N ∪ {ω}) r . Formulas in RBTL * are all and only the state-formulas generated by the BNF.

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

ψ ::= X ϕ | ϕ U ϕ | ϕ R ϕ.
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 2.6 (Model). A model for RBTL * is a tuple A = ⟨Q,r ,R,L⟩ s.t. (i) (Q,r ,R
) is a vector addition system with states (VASS), that is,

(1) Q is a non-empty finite set of control states;

(2) r ≥ 1 is the number of counters;

(3) R is a finite subset of Q × Z r × Q; and (ii) L : AP → ℘(Q ) is a labelling function.
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 . A pseudo-run λ is a run iff for all i ≥ 0, ⃗ v i ∈ (N ∪ ω) r .
Definition 2.7 (Satisfaction relation). We define the satisfaction relation |= in model A, for state q ∈ Q, run λ, p ∈ AP, state-formula ϕ, and path-formula ψ as follows (clauses for Boolean connectives are immediate and thus omitted):

(A,q) |= p iff q ∈ L(p) (A,q) |= ⟨ ⃗ b⟩ψ iff for some run λ from (q, ⃗ b), (A,λ) |= ψ (A,λ) |= ϕ iff (A,λ 0 ) |= ϕ (A,λ) |= Xψ iff (A,λ ≥1 ) |= ψ (A,λ) |= ψ Uψ ′ iff for some i ≥ 0, (A,λ ≥i ) |= ψ ′ ,
and for all 0 ≤ j < i, (A,λ ≥j ) |= ψ

Next, we prove that the logics RBTL * and RB±ATL * ({1},r ) with a single agent are semantically equivalent, in the sense that truthpreserving translations exist between models and formulas. First, consider the translation map τ from RBTL * to RB±ATL * ({1},r ) such that τ is the identity on AP, it is homomorphic for Boolean and temporal operators, and τ (⟨ ⃗ b⟩ψ

) def = E ⃗ b τ (ψ ).
Actually, it can be shown that τ is a bijection between RBTL * and RB±ATL * ({1},r ). Not only that, but τ is a bijection between RBTL and RB±ATL({1},r ) as well. Further, given a resource-bounded CGS M = ⟨{1},AP,S,Act,r , act,cost,δ ,L⟩ with a single agent 1, define the associated model A M = ⟨S,r ,R,L⟩ for RBTL * such that • R is the set of tuples (q,⃗ u,q ′ ) such that δ (q, a) = q ′ for some action a ∈ act (q, 1) with cost (q, 1, a) = ⃗ u.

Symmetrically, given a model A = ⟨Q,r ,R,L⟩, define the associated single-agent, resource-bounded CGS M A = ⟨{1},Q,R,r ,act, cost,δ ,L⟩ such that for every q ∈ Q,

• act (q, 1) = {(q ′ ,⃗ u,q ′′ ) ∈ R | q = q ′ }; • for every (q,⃗ u,q ′ ) ∈ act (q, 1), cost (q, 1, (q,⃗ u,q ′ )) = ⃗ u; • for every (q,⃗ u,q ′ ) ∈ act (q, 1), δ (q, (q,⃗ u,q ′ )) = q ′ . We now state the following auxiliary lemma, whose proof follows immediately by the definitions of A M and M A above. Lemma 2.8.

(1) Given a single-agent, resource-bounded CGS M and state s ∈ S, for every ⃗ b-consistent computation λ 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 + ⃗ u for ⃗ u = cost (λ i , 1, a i ) and λ i a i --→ λ i+1 . ( 2
) Given a model A for RBTL * and state q ∈ Q, for every run λ from (s, ⃗ b), in M A there exists a ⃗ b-consistent computation λ ′ such that for every i ≥ 0, λ i

(λ i ,⃗ u,λ i +1 ) ---------→ λ i+1 for (λ i , ⃗ v i ) → (λ i+1 , ⃗ v i+1 ) and ⃗ v i+1 = ⃗ u + ⃗ v i .
By using Lemma 2.8 we can finally prove that RB±ATL * ({1},r ) and RBTL * are closely related semantically. Theorem 2.9. (1) For every ϕ in RBTL * and model A with state q ∈ Q, (A,q) |= ϕ iff (M A ,q) |= τ (ϕ). (2) For every ϕ ′ in RB±ATL * and single-agent, resource-bounded CGS M with state s ∈ S, (M,s) |= Consequently, RBTL * and the restriction of RB±ATL * to a single agent are essentially the same logic in the sense that their translations 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 and single-agent RB±ATL. This result is particularly relevant in the light of Section 3, where we dig deeper into the verification of single-agent, resource-bounded logics.

ϕ ′ iff (A M ,s) |= τ -1 (ϕ ′ ).
Example 2.10. We illustrate the formal machinery introduced so far, particularly the single-agent case, with a toy example. 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 requires one energy unit.

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

• act (s 1 ,rover ) = {move, switch, idle} and act (s 2 ,rover ) = {recharge, switch, idle}; • cost (s 1 ,rover , move) = cost (s 1 ,rover , switch) = cost (s 2 , rover , switch) = -1 and cost (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 = {movinд} and L(movinд) = {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 at most b energy units, such that it will eventually be moving". This specification can be expressed in RB±ATL as

[[{rover } ω ]] G(⟨⟨{rover } b ⟩⟩ F movinд) (1)
Next, we show that specifications such as [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF], concerning a single agent and a single resource, can be efficiently verified in ptime.

MODEL-CHECKING RB±ATL({1}, 1)

This section is devoted to the technical developments of our main theoretical results. Specifically, in Section 3.1 we review the known complexity results for model checking RB±ATL and its fragments. Then, in Section 3.2 we prove that the control-state reachability and nontermination problems for vector addition systems with states (VASS) with one counter are decidable in ptime. These results are then used in Section 3.3 to show that the model-checking problem for RB±ATL({1}, 1) is also in ptime. Thus, our contribution shows that reasoning about a single resource in RB±ATL with a single agent comes at no extra computational cost compared to CTL. in ptime (Th. 3.10) Table 1: the complexity of model checking RB±ATL(Aд,r ).

r \|Aд| ∞ 2 1 ∞ 2exptime-c. [

Model Checking Results for RB±ATL

In Table 1, we summarize the main complexity results available in the literature for RB±ATL(Aд,r ), depending on the number |Aд| of agents and the number r of resources. The result in boldface is original from this contribution. All the results hold in the presence of R instead of G, except the pspace upper bound from [START_REF] Alechina | Model-checking for Resource-Bounded ATL with production and consumption of resources[END_REF]Theo. 2].

For an unbounded number of resources and at least two agents, the model-checking problem is known to be 2exptime-complete. This result follows from Theorem 2 (membership) and Theorem 3 (hardness) in [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF]. When restricted to a single agent, the problem becomes expspace-complete [START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF]Th. 4].

For a fixed number of resources greater than four and at least two agents, the model-checking problem is again exptime-complete. The upper bound follows from [1, 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 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 than two, and two agents, the model-checking problem is in exptime [1, Cor. 1]. In the case of a single agent, the same problem is in pspace [1, Cor. 2]; whereas 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].

Finally, in the case of a single resource, the problem is known to be in pspace [6, Th. 2] (the result is established for a language with G and it is plausible to extend it to R). For the case of a single agent, model checking is in ptime, which is the main theoretical contribution of this section. It is therefore ptime-complete as model checking CTL is already ptime-hard (see, e.g., [START_REF] Demri | Temporal Logics in Computer Science[END_REF][START_REF] Ph | The complexity of temporal logic model checking[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 3.3, 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.

Decision problems for 1-VASS

In order to show that the model-checking problem for RB±ATL({1}, 1) is ptime-complete, 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. More precisely, we show that the control-state reachability and nontermination problems for 1-VASS are in ptime, whereas, for instance, 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]. Although control-state reachability is a subproblem of the covering problem, that has been quite studied (see, e.g., [START_REF] Faouzi 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]), to the best of our knowledge there is no result in the literature on the upper bound when restricted to a single counter. Hereafter, we provide 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] St | A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One[END_REF], the updates in the BVASS (extending VASS) are restricted to the set {-1, 0, +1} (see [START_REF] St | A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One[END_REF]Def. 1]). Therefore the upper bound in [START_REF] St | A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One[END_REF] does not extend to our present case where updates are arbibtrary 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].

We recall the notion of VASS as given in Definition 2.6, so a VASS is a structure V = (Q,r ,R), where R is a finite set of transitions. A configuration of a VASS V is defined as a pair (q, ⃗ x ) ∈ Q × N r (ω is discarded in this section). Given (q, ⃗ x ), (q ′ , ⃗

x ′ ) and a transition

t = q ⃗ u - → q ′ , we write (q, ⃗ x ) t - → (q ′ , ⃗ x ′ ) whenever ⃗ x ′ = ⃗ u + ⃗ x. Then, (q 0 , ⃗ x 0 ) is called the initial configuration.
An r -VASS is a VASS with r counters. We present two standard decision problems on VASS that play a crucial role in solving the model checking problem for RB±ATL(Aд, 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 )?

Other classical decision problems for VASS have been considered in the literature (see e.g. recent developments about the reachability problem in [START_REF] Czerwinski | The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract)[END_REF][START_REF] Schmitz | The complexity of reachability in vector addition systems[END_REF]), but in this paper we only need to tame the control-state reachability and nontermination problems for 1-VASS in order to solve the model-checking problem for RB±ATL({1}, 1). Definition 3.1 (Simple Run, Path, and Loop). A simple run ρ = (q 0 , ⃗ x 0 ), . . . , (q k , ⃗ x k ), k ≥ 0, is a finite run such that no control state appears twice. A simple path is a sequence of transitions t 1 . . . t k such that no control state occurs more than once. A simple loop is a sequence of 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.

In a 1-VASS, a simple loop is (strictly) positive if the cumulated effect is (strictly) 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. The following lemma provides 1-VASS with a characterisation of runs ending in a distinguished final state. Lemma 3.2. Let V be a 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 configuration (q f ,x f ) for some x f ≥ 0 iff (1) either q 0 = q f ; or (2) there is a simple path (q 0 ,x 0 ), . . . , (q k ,x k ) with q k = q f ; or (3) we have that

• there is a simple run (q 0 ,x 0 ), . . . , (q n ,x n ),

• there is a strictly positive simple loop t 1 . . . t β such that

(q n ,x n ) t 1 ...t β ----→ (q n ,x n + α ) is a run (α > 0),
• there is a simple path starting at q n and ending at q f . Witness runs and path for (V , (q0, 7),q f ): initial run: (q0, 7), (q2, 11), (q3, 4) "> 0 loop": (q3, 4), (q5, 1), (q4, 6), (q3, 5) As illustration, Figure 2 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 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 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 j -x i . Such a transformation can be performed as soon as the subruns correspond to the application of simple loops with negative effect. Without loss of generality, we can assume that ρ has no loop with strictly negative effect.

final path: q3 - → q5 - → 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 . Consequently,

• there is a simple run (q 0 ,x 0 ), . . . , (q I ,x I ); • 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 ));
• 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. So, there 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 3.2 can be turned into an algorithm running in polynomial time. Proof. Let V be a 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]. Let us compute the values maxval i q : • maxval 0 q 0 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 j q ′ + u ∈ N | j ≤ i, q u - → q ′ is a transition}).
The values maxval i q 's 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.

Further, note that condition (2) in Lemma 3.2 is equivalent to maxval |Q | q f -∞. Similarly, the three conditions in (3) from Lemma 3.2 are equivalent to: there are q ∈ Q and I < J ≤ |Q | such that

• maxval I q -∞.
• maxval I q < maxval J q and auxval 0 q < auxval J -I q , where the values auxval i q ′ 's (i ∈ [0, J -I ], q ′ ∈ Q) are defined as follows (similarly to what is done for the maxval j q ′ 's): -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 j q ′′ + u ∈ N | j ≤ i, q ′ u - → q ′′ is a transition}).
• There is a simple path starting at q and ending at q f . The first two points above can be checked in ptime, and the third one in nlogspace as it is an instance of the standard graph reachability problem GAP. So, CREACH(1-VASS) is in ptime. □ Note that the values auxval i q ′ 's in the proof of Theorem 3.3 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 )2 . Now, let us turn to the characterisation of runs and paths witnessing nontermination. Lemma 3.4. Let V be a 1-VASS and (q 0 ,x 0 ) an initial configuration. There is an infinite run starting at (q 0 ,x 0 ) iff

• there is a simple run (q 0 ,x 0 ), . . . , (q n ,x n ); and

• there is a positive simple loop t 1 . . . t k such that (q n ,x n )

t 1 ...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 configuration (q n ,x n ). Let us prove the other direction, similarly to what is done in the proof of Lemma 3.2. 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 strictly negative effect. 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 ≥ |Q | such that q J = q I = q (such an index J necessarily exists). Obviously, there is a positive 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 3.4 can be turned into an algorithm to check nontermination, running in polynomial time.

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

Proof. Let V be a 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, 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 3.3 as we consider runs of length exactly i. When there is no such run, by convention maxval i q = -∞. • maxval 0 q 0 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 's 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 3.4 is equivalent to: there are q ∈ Q and I < J ≤ |Q | such that maxval I q -∞ and maxval I q ≤ maxval J q and auxval 0 q ≤ auxval J -I q , where values auxval i q ′ 's (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. □

To conclude, by Theorem 3.3 and 3.5 both the state-reachability and nontermination problems for 1-VASS are decidable in ptime.

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

In this section we establish our main theoretical result, that is, the model-checking problem for RB±ATL({1}, 1) is ptime-complete (forthcoming Theorem 3.10) by leveraging on Theorem 3.3 and 3.5. Hereafter, for every b ∈ N ∪ {ω}, we write ⟨⟨b⟩⟩ϕ instead of ⟨⟨{1} b ⟩⟩ϕ. 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.

As done in Section 2.3, given a resource-bounded CGS M = ({1},S,Act, 1,act,cost,δ ,L) with a single agent and a single resource, let us 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 cost (q, 1, a) = u. Similarly, we write K M = (S,R,L K ) to denote the Kripke structure such that q R q ′ 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 a total Kripke structure, i.e., every world has at least one successor. We introduce Kripke structures as the modality ⟨⟨ω⟩⟩ amounts to forget about the costs in M, and therefore M can be understood as the Kripke structure K M , and model checking reduces to CTL model checking. Similarly, as remarked in Section 2.3, the strategy modality ⟨⟨∅ b ⟩⟩ behaves as the universal path quantifier A in cost-free transition systems.

We now investigate the relationship between computations in M and runs in V M and in K M , respectively (a variant of Lemma 2.8). Lemma 3.6. Let M be a RB-CGS with a single agent and a single resource.

(I) Let q 0 a 0 - → q 1 a 1 - → q 2 • • • be a b-consistent computation associated to the family of resource values (v i ) i ∈N . If b ∈ N, then (q 0 ,v 0 ) - → (q 1 ,v 1 ) - → (q 2 ,v 2 ) • • • is an infinite run in V M ; otherwise q 0 - → q 1 - → q 2 • • • is an infinite path in K M . (II) Let (q 0 ,v 0 ) - → (q 1 ,v 1 ) - → (q 2 ,v 2 ) • • • be an infinite run in V M .
Then, there is a v 0 -consistent computation q 0

a 0 - → q 1 a 1 - → q 2 • • • associated to the family of resource values (v i ) i ∈N . (III) Let q 0 - → q 1 - → q 2 • • • is an infinite path in K M . Then, there is an ω-consistent computation q 0 a 0 - → q 1 a 1 - → q 2 • • • in M.
The proof of Lemma 3.6 follows immediately by definition, and this result is instrumental to the three following lemmas that are at the heart of the model-checking algorithm for RB±ATL({1}, 1). Given S 1 ⊆ S, we write V S 1 M (resp. K S 1 M ) to denote the restriction of V M (resp. K M ) to the locations in S 1 only. Lemma 3.7. 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

S 1 iff (V S 1 M , (s,b)) is a positive instance of NONTER(1-VASS). (II) There is an ω-consistent computation starting in s in M that visits only states in S 1 iff (K M ,s) |= E G( s ′ ∈S 1 s ′ ) in CTL.
This is a consequence of Lemma 3.6 (which will be generalised in Lemma 3.9). Let us focus now on the until operator U. (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 ′ ∈S 1 s ′ ) U( s ′ ∈S 2 s ′ ).
This is again a consequence of Lemma 3.6 but here, we have to use the fact that the distinguished action idle is enabled in any state (which is handy to extend to the infinity a finite witness run). Finally, we consider the linear-time temporal operator R. Lemma 3.9. Let M be a 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 ω 2 ∪ ((S \ S 1 ) ∩ S 2 ) * • (S 1 ∩ S 2 ) • S ω iff either (V S 2 M , (s,b)) is a positive instance of NONTER(1-VASS) or for some s ′ ∈ S 1 ∩ S 2 , (V S 2 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 ω 2 ∪ ((S \ S 1 ) ∩ S 2 ) * • (S 1 ∩ S 2 ) • S ω iff in CTL, we have (K M ,s) |= (E G s ′ ∈S 2 s ′ ) ∨ E( s ′ ∈(S \S 1 )∩S 2 s ′ ) U( s ′ ∈S 1 ∩S 2 s ′ ).
By using Lemmas 3.7-3.9 we derive our main theoretical result. end case 16: end procedure By induction, one can show that (M,s) |= ϕ iff s ∈ GMC (M,ϕ). Lemmas 3.7-3.9 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, which is reflected in Algorithm 1. As far as computational complexity is concerned, GMC (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 3.3 and 3.5. More precisely, for each occurrence of a subformula ψ of ϕ, GMC (M,ψ ) can be computed only once, which guarantees the overall number of calls of the form GMC (M,ψ ): it is sufficient to take advantage of dynamic programming and to work with a table to remember the values GMC (M,ψ ) already computed (omitted in the present algorithm). It is also worth observing that the instances we consider are polynomial in the sizes of M and ϕ. Finally, we take 3 We omit the case for the operator G as G ϕ is logically equivalent to ⊥ R ϕ. Table 2: The complexity of model checking RB±ATL * (Aд,r ).

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 the Computation Tree Logic CTL comes at no extra computational cost. Hence, in principle we can verify specification such as formula (1) in Example 2.10 efficiently. Based on the correspondences established in Theorem 2.9, we immediately derive the following consequence.

Corollary 3.11. The model-checking problem for RBTL restricted to a single resource is ptime-complete.

  Notice that the semantics of operators ⟨⟨∅ ⃗ b ⟩⟩ and [[∅ ⃗ b ]] corresponds to the meaning of modalities A and E in CTL * ; whereas ⟨⟨Aд ⃗ b ⟩⟩ and [[Aд ⃗ b ]] can be used to introduce resource-bounded counterparts E ⃗ b and A ⃗ b of modalities E and A. In Section 2.3, we show that RB±ATL * for the single agent case is basically equivalent to a different resourcebounded logic RBTL * introduced in [14].

switch : - 1 switch : - 1 Figure 1 :

 111 Figure 1: the resource-bounded CGS in Example 2.10. Transitions with action idle are omitted.

Figure 2 :

 2 Figure 2: Witness runs and path from Lemma 3.2(3)

Theorem 3 . 3 .

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

Lemma 3 . 8 . 2 M,

 382 Let M be a 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 S 1 ∪S (s,b),s ′ ) is a positive instance of CREACH(1-VASS).

Theorem 3 . 10 . 8 : 9 : 1 U ψ 2 : 11 :⟨⟨b⟩⟩ψ 1 R ψ 2 : 2 M 2 M 14 :

 310891211122214 The model-checking problem for RB±ATL({1}, 1) is ptime-complete. ptime-hardness is inherited from the model-checking problem for CTL.Proof. Let M = ({1},S,Act, 1,act,cost,δ ,L) be a resource-bounded CGS, and ϕ be a formula in RB±ATL({1}, 1). Let us present Algorithm 1, a polynomial-time algorithm that computes the finite set {s ∈ S | (M,s) |= ϕ} (by default, b ∈ N)3 .Algorithm 1 -RB±ATL({1}, 1) model checking -1: procedure GMC(M, ϕ) return {s ∈ S | s ∈ L(p ) } 4: ¬ψ : return S \ G MC (M, ψ ) 5: ψ 1 ∧ ψ 2 : return G MC (M, ψ 1 ) ∩ G MC (M, ψ 2 ) 6: ⟨⟨b⟩⟩ X ψ : return {s | ∃ a ∈ act (s, 1), 0 ≤ b + cost (s, 1, a), δ (s, a) ∈ G MC (M, ψ ) } 7: ⟨⟨ω⟩⟩ X ψ : return {s | ∃ a ∈ act (s, 1), δ (s, a) ∈ G MC (M, ψ ) } ⟨⟨∅ b ⟩⟩ X ψ : return {s | ∀ a ∈ act (s, 1), δ (s, a) ∈ G MC (M, ψ ) } ⟨⟨b⟩⟩ψ S 1 := G MC (M, ψ 1 ); S 2 := G MC (M, ψ 2 ); return {s ∈ S | ∃ s ′ ∈ S 2 s.t. V S 1 ∪S 2 M , (s, b ), s ′ is a positive inst. of CREACH(1-VASS) } 10: ⟨⟨ω⟩⟩ψ 1 U ψ 2 : S 1 := G MC (M, ψ 1 ); S 2 := G MC (M, ψ 2 ); return {s ∈ S | K M , s |= E( s ′ ∈S 1 s ′ ) U( s ′ ∈S 2 s ′ ) } ⟨⟨∅ b ⟩⟩ψ 1 U ψ 2 : S 1 := G MC (M, ψ 1 ); S 2 := G MC (M, ψ 2 ); return {s ∈ S | K M , s |= A( s ′ ∈S 1 s ′ ) U( s ′ ∈S 2 s ′ ) }12: S 1 := G MC (M, ψ 1 ); S 2 := G MC (M, ψ 2 ); return {s ∈ S | V S , (s, b ) is a positive inst. of NONTER(1-VASS) } ∪{s ∈ S | ∃ s ′ ∈ S 1 ∩ S 2 s.t. V S , (s, b ), s ′ is a positive inst. of CREACH(1-VASS) } 13: ⟨⟨ω⟩⟩ψ 1 R ψ 2 : S 1 := G MC (M, ψ 1 ); S 2 := G MC (M, ψ 2 ); return {s ∈ S | K M , s |= E( s ′ ∈S 1 s ′ ) R( s ′ ∈S 2 s ′ ) } ⟨⟨∅ b ⟩⟩ψ 1 R ψ 2 : S 1 := G MC (M, ψ 1 ); S 2 := G MC (M, ψ 2 ); return {s ∈ S | K M , s |= A( s ′ ∈S 1 s ′ ) R( s ′ ∈S 2 s ′ ) } 15:

r \ |Aд | ∞ 2 1 ∞

 1 in 2exptime [1, Th. 7] expspace-c. [1, Th. 8] ≥ 1 2exptime-h. (from ATL * ) in pspace ([1, Cor. 2] & Th. 2.9) pspace-h. (from CTL * )

Proc. of the 18th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2019), N. Agmon, M. E. Taylor, E. Elkind, M. Veloso (eds.), May 13-17, 2019, Montreal, Canada. © 2019 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

Indeed, in[START_REF] Alechina | On the Complexity of Resource-Bounded Logics[END_REF], complexity results are given independently for both RBTL * and singleagent RB±ATL * , even though the two logics can be translated one into the other.

We remark that 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 should have been used.

Acknowledgment. We would like to thank Michael Blondin (University of Sherbrooke) for pointing us to [35] and for insightful feedback, as well as the anonymous referees for their suggestions and comments. F. Belardinelli acknowledges the support of the ANR JCJC Project SVeDaS (ANR-16-CE40-0021).

CONCLUDING REMARKS

We investigated the complexity of the model-checking problem for Resource-bounded Alternating-time Temporal Logics. In particular, we established that RBTL * and RB±ATL * ({1},r ) can be understood as slight variants of the same logic. More importantly, we provided a unified view of the model-checking problems for RB±ATL, then proved that model checking RB±ATL({1}, 1) is ptime-complete. To do so, we designed original algorithms to solve the control-state reachability and nontermination problems for 1-VASS. Hence, as far as worst-case complexity is concerned, the model-checking problems for CTL and RB±ATL({1}, 1) behave similarly.

The paper has not touched very much on the model-checking problem for RB±ATL * , for which the main results are summarised in Table 2. Unlike RB±ATL, tight complexity bounds are known for all variations on the number of agents and resources. For at least two agents, the model-checking problem is 2exptime-complete. The upper bound comes from [1, 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 pspace-complete: the lower bound follows immediately from the pspace-hardness of the model-checking problem for CTL * ; as for the upper bound, we derive it from the fact that model checking RBTL * is in pspace [1, Cor. 2] and Theorem 2.9.

As far as future work is concerned, we plan to implement the ptime algorithm for model checking RB±ATL({1}, 1), possibly taking advantage of the very recent results in [START_REF] Almagor | Coverability in 1-VASS with Disequality tests[END_REF], and to investigate the complexity of other meaningful fragments of RB±ATL(Aд,r ) for which tight bounds are unknown. The synthesis of parameters for the parameterised version of RB±ATL({1}, 1) (as well as for other fragments of RB±ATL * (Aд,r )) is also worth further investigation.