Martin De Wulf

Laurent Doyen

Nicolas Markey

Jean-François Raskin

Robust Safety of Timed Automata

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

1 Introduction Timed automata. Timed and hybrid systems are dynamical systems with both discrete and continuous components. A paradigmatic example of a hybrid system is a digital embedded control program for an analog plant environment, like a furnace or an airplane: the controller state moves discretely between control modes, and in each control mode, the plant state evolves continuously according to physical laws. Behaviors of controllers for physical systems are often subject to real-time constraints. A natural model for such controllers is the timed automaton model introduced by Alur and Dill [START_REF] Alur | A theory of timed automata[END_REF]. Timed automata extend finite state automata with continuous variables called clocks. Those clocks take their values in the nonnegative real numbers and count time; they can be reset and compared to other clocks or constants in guards labeling edges and invariants labeling states of the automaton. Several verification and control problems have been studied for timed automata, see for example [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems (an extended abstract)[END_REF][START_REF] Cassez | A comparison of control problems for timed and hybrid systems[END_REF], and verification tools have been developed, e.g. [BDL + 06].

When a high-level description of a controller has been proven correct it would be valuable to ensure that an implementation of that controller can be obtained in a systematic way in order to ensure the preservation of correctness. This is often called program refinement: given a high-level description P 1 of a program, refine that description into another description P 2 such that the "important" properties of P 1 are maintained. Usually, P 2 is obtained from P 1 by reducing non-determinism. To reason about the correctness of P 2 w.r.t. P 1 , we often use a notion of simulation [START_REF] Milner | A Calculus of Communicating Systems[END_REF] which is powerful enough to ensure conservation of LTL properties for example.

Unfortunately, for timed automata this is often not possible for several fundamental and/or technical reasons. First, the notion of time used in the traditional semantics of timed automata is continuous, defining perfect clocks with infinite precision, while implementations can only access time through digital and finitely precise clocks. Second, timed automata react instantaneously to events and timeouts while implementations can only react within a given, usually small but non-zero, reaction delay. Third, timed automata may describe control strategies that are unrealistic, such as Zeno-strategies or strategies that require the controller to act faster and faster [START_REF] Cassez | A comparison of control problems for timed and hybrid systems[END_REF]. For those reasons, a model of a digital controller that has been proven correct in the traditional semantics may not be implementable (at all) or it may not be possible to turn it systematically into an implementation that is still correct. correct w.r.t. this model.

Implementability of timed automata. To overcome those problems, [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF] proposed an alternative semantics for timed automata, which takes into account the digital and imprecise aspects of the hardware in which the automaton is being executed. The hardware is assumed to repeatedly execute the following procedure: it first reads the value of the global clock, then evaluates the guard of each transition, and executes one of the enabled transitions. This procedure is assumed to run in at most ∆ L time units. Moreover, the global (digital) clock is updated at least every ∆ P time units, and its value may drift by some value ε (i.e., the delay u between two updates of the clock is at most ∆ P , and the clock is incremented by some value c between u(1 -ε) and u(1 + ε)). The resulting set of executions is denoted by A Prg ∆ L ,∆ P ,ε and called the program semantics. The automaton A is said to be implementable w.r.t. a given property P iff there exists positive values for the parameters ∆ L , ∆ P and ε for which all the executions of A Prg ∆ L ,∆ P ,ε satisfy P. This model of an implementation platform is clearly implementable by an hardware with bounded imprecision, and the semantics of the implementation platform is kept deliberately simple: any platform that ensures the minimal performances that are imposed by the program semantics ensures compliance with the formal model (see [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF] for more discussion and details).

In [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF], a different semantics is also introduced for the purpose of verification. This new semantics is called the Almost-ASAP semantics and is obtained by enlarging the guards of A by a parameter ∆. allowing the clocks to drift by ε. The set of executions of A under this semantics is denoted by A AAsap ∆ . We say that A robustly satisfies a property P if there exists positive values for the parameter ∆ such that all the executions of A AAsap ∆ satisfy P. It is shown in [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF] that the Almost-ASAP semantics A AAsap ∆ over-approximates the program semantics A Prg ∆ L ,∆ P ,ε if ∆ > 3∆ L +4∆ P when ε = 0,1 and therefore a timed automaton is implementable w.r.t. a property P if it robustly satisfies P. In the rest of this paper, we denote by A ε ∆ the semantics of A enlarged (or perturbed) by ∆ and ε, i.e., whose guards are enlarged by ∆ and whose clocks may drift by at most ε.

The robust semantics considered here differs from the Almost-ASAP semantics. First, the Almost-ASAP semantics does not consider drifting clocks, but as we will see later, enlargements on guards only are sufficient in the sense that guard perturbations and drifts on clocks give rise to the same reachable states. Second, in the Almost-ASAP semantics, we make a distinction between the controller and the plant: only the controller is enlarged. Here we consider enlargements of all the transitions, even those that belong to the plant. So, clearly, the robust semantics that we consider here overapproximates the AASAP semantics, and robust correctness considered here implies implementability in the sense of [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF].

Robust verification of timed automata. In this paper, we consider the robust safety verification problem which asks, given a timed automaton A and a set of Bad states to avoid (i.e., a safety property), if there exist ∆, ε ∈ Q >0 such that Reach( A ε ∆ ) ∩ Bad = ∅. The main result of this paper is to show that the robust safety verification problem is decidable. 2 To show this, we make a strong link with the robust semantics defined in [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] Puri | Dynamical properties of timed automata[END_REF] where Puri presents an algorithm to compute the set ∩ ε>0 Reach( A ε 0 ). This is the set of states that can be reached when the clocks drift by an infinitesimal amount. We show that Puri's algorithm can be used to compute the following sets (which are therefore equal):

\ ε>0 Reach( A ε 0 ) = \ ∆>0 Reach( A 0 ∆ ) = \ ∆>0 \ ε>0 Reach( A ε ∆ )
The proof of this result follows the general ideas of Puri's proof and it is based on the structure of limit cycles of timed automata (a fundamental notion introduced by Puri) but we need new techniques to handle both the imprecisions on guards and the clock drifts. To establish the decidability of the robust safety verification problem, we show that

\ ∆>0 \ ε>0 Reach( A ε ∆ ) ∩ Bad = ∅ iff ∃∆ > 0, ε > 0. Reach( A ε ∆ ) ∩ Bad = ∅.
Hence, to solve the robust safety verification problem, it suffices to compute the set T ∆>0 T ε>0 Reach( A ε ∆ ) and check if it has an empty intersection with Bad. We give a detailed proof of all intermediate results, some of which are useful by themselves to develop the robust verification of timed automata for LTL and a fragment of MTL [START_REF] Bouyer | Robust model-checking of linear-time properties in timed automata[END_REF][START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF]. This paper is an extended and revised version of [START_REF] De Wulf | Robustness and implementability of timed automata[END_REF].

Related works. The problem of designing controllers for embedded systems is an extremely important subject and a very active area of research. This design problem has been addressed by a large number of researchers in computer science but also in other research communities like control theory. Researchers in control theory have studied the general problem of going from a continuous formulation of the control problem to a discrete solution which is implementable by digital devices. Here, we focus on the particular nice mathematical model of timed automata. Timed automata are important but by no means the only important mathematical model in the context of the modelbased design of embedded control systems (see for instance Matlab-Simulink models, dynamical systems of control theory, etc.) Timed automata are adequate for modeling a large variety of real-time constrained behaviors but they abstract away other properties of systems, like power-consumption, distribution, concurrency etc., properties that may be important for the correct physical realization of timed controllers. Our paper thus focuses on an important aspect related to the implementation of real-time behaviors but other important aspects must be tackled by other techniques and are treated elsewhere (and should not be ignored in practice). In the rest of this paragraph, we concentrate on other works that are related to the specific issue of the robustness of timed models and their realization by digital devices.

One of the first attempts to make mathematical models of timed systems implementable was done by Dierks for Programmable Logic Controllers (PLC) [START_REF] Dierks | Specification and Verification of Polling Real-Time Systems[END_REF][START_REF] Dierks | PLC-automata: a new class of implementable real-time automata[END_REF]. The language used to define the semantics of PLC-automata and to specify real-time constraints is the Duration Calculus [START_REF] Zhou Chaochen | A calculus of durations[END_REF], which is a dense time interval-based temporal logics that allows to fix the delays for the visibility of events, the computation times, the imprecision of the clocks, etc. That logic is very expressive, but its major drawback is to be undecidable [START_REF] Zhou Chaochen | Decidability and undecidability results for duration calculus[END_REF].

Other notions of robustness for timed systems have also been addressed in several works for timed automata [GHJ97, ALM05] and hybrid automata [Frä99, AB01, AT04], but none of these works make a link between robustness and implementability.

In [START_REF] Henzinger | From control models to real-time code using giotto[END_REF], Henzinger et al. introduce a programming model for real-time embedded controllers called Giotto. Giotto is an embedded software model that can be used to specify a solution to a given control problem independently of an execution platform but which is closer to executable code than a mathematical model. So, Giotto can be seen as an intermediary step between mathematical models like hybrid automata and real execution platforms.

In [AIK + 03], Alur et al. consider the more general problem of generating code from hybrid automata, but they only sketch a solution and state interesting research questions. In [AFM + 02, AFP + 03], Yi et al. present a tool called Times, which generates executable code from timed automaton models. However, they make the synchrony hypothesis and so they assume that the hardware on which the code is executed is infinitely fast and precise.

In [START_REF] Altisen | Implementation of timed automata: an issue of semantics or modeling?[END_REF], Altisen and Tripakis tackle the problem of the implementability of timed automata specifications by considering an alternative direction to ours. By contrast with our approach, they do consider the usual semantics of timed automata and propose to model the execution platform within this formal semantics. For instance, they show how drifting clocks or delays in synchronization can be modeled using parametrized widgets in the form of timed automata. The resulting model is a network of timed automata composed of the initial model of the controller and a bunch of timed automata that models the platform. On the one hand, this approach is general in the sense that different implementation platforms can be modeled accurately by timed au-tomata models. On the other hand, one drawback of their approach comes from the fact that models of specific platforms tend to be very large and may impair the automatic verification step because of the state explosion problem. Also, in early steps of the design of a timed controller, we may not know the exact platform that will be used to implement the control strategy but we may already be interested to verify the robustness of the control strategy with regard to timing imprecisions. The use of a robust semantics partially avoid those problems by leaving the details of the implementation unspecified: the proof of implementability makes reference to a naive implementation schema which imposes very few constraints on the platform that is chosen for the actual implementation and which is met by any reasonable implementation platform (see [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF] for more details). The price to pay in our setting is that we may be over-pessimistic and declare some control strategies not to be implementable while a precise modeling of the execution platform in the setting of Altisen and Tripakis might allow to establish implementability of the control strategy.

Finally, note that the algorithm presented in this paper to solve the robust safety verification problem is not usable in practice as it relies on the construction of the region automaton. Recent works have investigated the development of practical algorithms [START_REF] Daws | Symbolic robustness analysis of timed automata[END_REF][START_REF] Swaminathan | A symbolic decision procedure for robust safety of timed systems[END_REF] but, to the best of our knowledge, no efficient implementation has been released yet.

Timed models

This section is devoted to the definitions of timed automata and their perturbed semantics, and of several other important notions that will be used in this paper.

In the sequel, R 0 is the set of nonnegative reals, and N is the set of nonnegative integers.

Definition 1 A timed transition system (TTS for short) T is a tuple S, ι, Σ, → where S is a (possibly infinite) set of states, ι ∈ S is the initial state, Σ is a finite set of labels, and → ⊆ S × (Σ ∪ R 0 ) × S is the transition relation. We write q σ -→ q if (q, σ, q ) ∈ →.

A trajectory of a TTS T = S, ι, Σ, → is a finite sequence π = (s 0 , t 0 ) σ1 --→ (s 1 , t 1 ) . . .

σ k --→ (s k , t k ) such
that for all 0 i k, we have (s i , t i ) ∈ S × R 0 , and for all 0 i < k, we have s i σi -→ s i+1 , and either σ i ∈ Σ and t i+1 = t i , or σ i ∈ R 0 and

t i+1 = t i + σ i . Let π = (s 0 , t 0 ) σ1 --→ (s 1 , t 1 ) . . . σ k --→ (s k , t k
) be a trajectory. The i + 1-st state in π, written state i (π), is the state s i . We denote by first(π) = state 0 (π) and last(π) = state k (π) the initial and final states of π. We say that π is a trajectory from s 0 to s k , and we sometimes write π more briefly as s 0 σ1 --→ s 1 . . .

σ k --→ s k . The length of π, written |π|, is k, and its duration Duration(π) is t k -t 0 .
The sequence of states s 0 s 1 . . . s k is called a path in T , and the trace of π is the sequence trace(π) = λ 1 . . . λ k where for all 1 i k, λ i = σ i if σ i ∈ Σ, and

λ i = time if σ i ∈ R 0 (time is a special symbol not in Σ).
A trajectory is stutter-free iff its trace contains alternately a symbol in Σ and the symbol time, i.e., it does not contain two consecutive symbols in Σ or two consecutive time's.

A state s of T is reachable from a state s if there exists a trajectory π of T such that first(π) = s and last(π) = s . Given a set of states Q ⊆ S, we write Reach(T , Q) for the set of states that are reachable from some state in Q. We abusively write Reach(T ) for Reach(T , {ι}), the set of states that are reachable from the initial state of T .

Given a set Var = {x 1 , . . . , xn} of clocks, a clock valuation is a function v : Var → R 0 . In the sequel, we often identify a clock valuation with a point in R n 0 . Given two valuations v and v and two nonnegative reals t and λ, we write v + v for the valuation x → v(x) + v (x), v + t for the valuation x → v(x) + t and λv for x → λv(x). If R ⊆ Var, then v[R := 0] denotes the valuation v such that v (x) = 0 for all x ∈ R, and v (x) = v(x) for all x ∈ R.

A closed rectangular guard g over Var is a set of inequalities of the form a i x i b i , one for each x i , where a i , b i ∈ Q 0 ∪ {+∞} and a i b i . We write Rectc(Var) for the set of closed rectangular guards over Var. For ∆ 0, we define

g ∆ = {(x 1 , . . . , xn) | a i -∆ x i b i + ∆} ⊆ R n 0 .
When ∆ = 0, we write g instead of g 0 . We now define timed automata. Our definition is a slightly modified version of the classical timed automata proposed by [START_REF] Alur | A theory of timed automata[END_REF]. In particular, all clocks are assumed to be bounded by some constant M , and guards on edges are rectangular and closed. The first requirement is not restrictive (except w.r.t. the conciseness of the models [START_REF] Bouyer | On conciseness of extensions of timed automata[END_REF]), the second one is discussed below.

Definition 2 A (closed) timed automaton is a tuple A = Loc, Var, q 0 , Lab, Edg where -Loc is a finite set of locations representing the discrete states of A.

-Var = {x 1 , . . . , xn} is a finite set of real-valued variables.

q 0 = (l 0 , v 0 ), where l 0 ∈ Loc, is the initial location and v 0 is the initial clock valuation such that for any

x ∈ Var, v 0 (x) ∈ N ∧ v 0 (x) M . -Lab is a finite alphabet of labels. -Edg ⊆ Loc × Rectc(Var) × Lab × 2 Var × Loc is the set of transitions. A transition
(l, g, σ, R, l ) represents a jump from location l to location l with guard g, event σ and a subset R ⊆ Var of variables to be reset.

We now define a family of semantics for timed automata which is parametrized by ε ∈ R 0 (drift on clocks) and ∆ ∈ R 0 (imprecision on guards).

Definition 3 Given ε, ∆ ∈ R 0 , the perturbed semantics of a timed automaton A = Loc, Var, q 0 , Lab, Edg is the TTS A ε ∆ = S, ι, Σ, → where:

1. S = {(l, v) | l ∈ Loc ∧ v : Var → [0, M ]}; 2. ι = q 0 ; 3. Σ = Lab;
4. The transition relation → is defined by (a) For the discrete transitions: ((l, v), σ, (l , v )) ∈ → whenever there exists an edge

(l, g, σ, R, l ) ∈ Edg such that v ∈ g ∆ and v = v[R := 0]; (b) For the continuous (or timed) transitions: ((l, v), t, (l , v )) ∈ → whenever l = l and v (x i ) -v(x i ) ∈ [(1 -ε)t, (1 + ε)t] for i = 1 . . . n.
The traditional semantics of A is A 0 0 . When ε > 0 or ∆ > 0, we call A ε ∆ the perturbed semantics of A. In the sequel, we often write A , A ∆ , and A ε instead of respectively A 0 0 , A 0 ∆ , and A ε 0 .

Remark 1 Our definition of timed automata does not allow strict inequalities; This is not restrictive in the presence of guard enlargement. Indeed, consider a timed automaton A with (possibly open) rectangular guards and the closure automaton b A resulting from A by replacing all strict inequalities by non-strict ones. It appears obviously that

Reach( b A ε ∆ 2 ) ⊆ Reach( A ε ∆ ) and Reach( A ε ∆ ) ⊆ Reach( b A ε ∆ ),
and hence the robust safety verification problem for A and Bad ("Do there exist ∆, ε ∈ R >0 such that Reach( A ε ∆ ) ∩ Bad = ∅? ") is equivalent to the the robust safety verification problem for b A and Bad. Note that this only holds thanks to guard enlargement, and the situation is different when only clock drifts are allowed [START_REF] Dima | Dynamical properties of timed automata revisited[END_REF].

Remark 2 Notice that guard enlargement and clock drifts are monotone, in the sense that for any ∆ ∆ and ε ε , we have Reach( A ε ∆ ) ⊆ Reach( A ε ∆ ). Thanks to this observation, we can define the following sets:

R ε ∆→0 = \ ∆>0 Reach( A ε ∆ ) R ε→0 ∆ = \ ε>0 Reach( A ε ∆ )
These sets are central in the sequel: we prove that, under some minor restriction, the sets R 0 ∆→0 and R ε→0 0 are equal, and they also coincide with

T ∆>0 R ε→0 ∆ and T ε>0 R ε ∆→0 .
It follows from [START_REF] Puri | Dynamical properties of timed automata[END_REF] that those sets are computable; we will reprove this result in the sequel.

We now recall some additional classical notions related to timed automata. In the sequel, x denotes the integer part of x (the greatest integer k x), and x denotes its fractional part.

Definition 4 A clock region is an equivalence class of the relation ∼ defined over the clock valuations in Var → [0, M ]. We have v ∼ w iff the following three conditions hold:

-∀x ∈ Var. v(x) = w(x) ; -∀x ∈ Var. v(x) = 0 iff w(x) = 0. -∀x, y ∈ Var. v(x)
v(y) iff w(x) w(y) ;

We denote by (v) the clock region containing v, and by [r] the topological closure of a region r, which is then abusively called a closed clock region. The clock region (v) contains the valuations that agree with v on the integer part of the variables, and on the ordering of their fractional part and zero.

A clock region r is a time-successor of a clock region r if r = r and for some v ∈ r and t ∈ R >0 , we have v + t ∈ r .

Definition 5 Given the TTS A = S, s 0 , Σ, → A of a timed automaton A, we define the corresponding region graph

G = R A , → G of A: -R A = {(l, r) | ∃(l, v) ∈ S : r = (v)} is the set of regions; -→ G ⊆ R A × (Σ ∪ {time}) × R A where ((l, r), time, (l , r)) ∈ → G if and only if l = l
and r is a time-successor of r, and ((l, r), σ, (l , r))

∈ → G for σ ∈ Σ if and only if (l, v) σ -→ A (l , v ) for some v ∈ r and v ∈ r .
Notice that R A is finite (the total number W = |R A | of regions is exponential in the size of A) and a region (l , r ) is reachable in G from a region (l, r) if and only if (l , v ) is reachable in A from a state (l, v) for some v ∈ r, v ∈ r [START_REF] Alur | A theory of timed automata[END_REF].

In the rest of the paper, we often abusively use operators that apply to valuations v or clock regions r to pairs ( , v) and ( , r) where is a location. For example, we write ( , v) + ( , v ) to denote ( , v + v ) and λ( , v) to denote ( , λv), and similarly for distances, norms and neighbourhoods. We write ( , v) ∈ ( , r) instead of v ∈ r, [( , v)] instead of ( , [v]), etc.

Since guards are closed, the successors of a closed region by a discrete transition or by the passage of time is a union of closed regions. Since there are finitely many regions, the next lemma follows.

Lemma 6 Let A be a (closed) timed automaton. The set Reach( A ) is a closed set.

Given a path p = p 0 p 1 • • • p N in the region graph of a timed automaton A, and a trajectory π of A , we say that π follows p if for all i,

0 i N , state i (π) ∈ [p i ].
Note that, since we consider closed regions, a trajectory could follow several paths of the region graph.

Definition 7 A zone Z ⊆ R n 0 is a closed set defined by inequalities of the form

x i -x j m ij , α i x i β i
where 1 i, j n and m ij , α i , β i ∈ Z. A set of states is called a zone-set if it is a finite union of sets of the form {l} × Z where l is a location and Z is a zone.

Definition 8 A progress cycle in the region graph of a timed automaton is a cycle in which each clock of the automaton is reset at least once.

The correctness of our algorithm (Theorem 11 below) heavily relies on the fact that timed automata should not have weird behaviors, like cycles that do not let time elapse. However, apart from Theorems 11, 39 and 47, all our intermediate results hold in the general case. We thus formulate the following assumption, but we will always explicitly refer to it when it is needed.

Assumption 9 We only consider timed automata whose cycles in the region graph are all progress cycles.

This assumption was made by Puri in [START_REF] Puri | Dynamical properties of timed automata[END_REF]. It is weaker than the classical non-Zeno assumptions in the literature. For example in [START_REF] Asarin | Controller synthesis for timed automata[END_REF], the authors impose that "in every cycle in the transition graph of the automaton, there is at least one transition which resets a clock variable x i to zero, and at least one transition which can be taken only if x i 1". Other natural hypotheses would be to ask that every cycle in the region graph has a timed transition (labeled by time), or that every cycle in the region graph contains a time-elapsing region, that is, a region r such that ∃v ∈ r • ∃t > 0 : v + t ∈ r. Again, Assumption 9 is weaker. Example Consider the timed automaton Aα of Fig. 1(a) where α ∈ {2, 3}. The automaton has two clocks x and y. There is one initial location 1 with initial clock values x = 1 and y = 0. For locations 1 and 2 , the sets of reachable states in the classical semantics Aα with ε = ∆ = 0 are depicted in Fig. 1(b). The final states (or bad states) correspond to the location err with any clock valuation. For both α = 2 and α = 3, the timed automaton Aα does not reach the bad states. Consider the perturbed semantics Aα 0 ∆ for ε = 0 and ∆ > 0. In this semantics, guards are enlarged by ∆. The edge from 1 to 2 has the guard x 2+∆ and the edge from 2 to 1 has the guard y 2 -∆. From the initial state ( 1 , x = 1, y = 0), the transition to 2 can be taken after ∆ time units, reaching the states ( 2 , x = 0, y 1 + ∆). Similarly, the transition from 2 back to 1 is enabled ∆ time units earlier than before and the states ( 1 , x 1 -2∆, y = 0) are reachable. It is easy to show that after having taken k times the transitions of the cycle, the states ( 1 , x 1 -2k∆, y = 0) (provided x 0) and ( 2 , x = 0, y 1 + (2k -1)∆) (provided y 2) are reachable. Hence, for all ∆ > 0 the states ( 1 , x 0, y = 0) and ( 2 , x = 0, y 2) are reachable in Aα 0 ∆ and were not reachable in the classical semantics A 2 0 0 . Those states are represented in Fig. 1(c). The same situation occurs in the perturbed semantics Aα ε

0 for ∆ = 0 and ε > 0, that is, R ε→0 ∆ = R ε ∆→0 = Reach( Aα ).
This example shows that the classical semantics is not robust with respect to small perturbations in either the timing constraints or the clock rate. The effect of such perturbations, no matter how small they are, may lead to dramatically different behaviours of the system. In this case, the location err is reachable in the perturbed semantics A 2 0 ∆ for any ∆ > 0, but not in the classical semantics A 2 0 0 . We say that the safety property (to avoid the location err) is not robustly satisfied by A 2 . Such non-robust systems cannot have a correct implementation because their correctness relies on the mathematical idealization of the traditional semantics.

On the other hand, for α = 3 the safety property still holds in the limit of the perturbed semantics. As we will show, this implies that there exists a strictly positive value of ∆ for which the perturbed semantics Aα 0 ∆ is safe. In fact, any ∆ < 1 3 fits in our example.

The robust safety verification problem is decidable

The main result of this paper is a detailed proof that the robust safety verification problem is decidable, for both perturbed guards and drifting clocks (Theorem 11).

Definition 10 The robust safety verification problem asks, given a timed automaton A and a zone-set Bad, if there exist

∆, ε ∈ Q >0 such that Reach( A ε ∆ ) ∩ Bad = ∅.
Theorem 11 Under assumption 9, the robust safety verification problem is decidable.

The rest of the paper is devoted to the detailed proof of this result. The main argument is based on an algorithm presented by Puri in [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] Puri | Dynamical properties of timed automata[END_REF] to compute a robust semantics for timed automata, namely the set R ε→0 0 . Puri gives a proof of correctness of his algorithm, using innovative techniques for the analysis of cycles in timed automata. However, some of Puri's important results are proven in broad outline. For instance, Puri's claim that R ε→0

0 = R ε→0 ∆→0 where R ε→0 ∆→0 = T ∆>0 T ε>0 Reach( A ε ∆ ) is not really justified ([Pur98, Theorem 9.1]).
Moreover, several proofs of intermediate results that are used by Puri to establish the correctness of his algorithm are quickly sketched, giving a rough idea of the proof scheme. For some of them, we were not able to complete the proofs, in particular for [Pur98, Lemma 6.4] where the statement of the lemma itself is actually wrong.

Therefore, we give in the next sections a detailed proof of Theorem 11 and of the equality R ε→0 ∆→0 = R ε→0 0

. Moreover, we show that the same semantics is also obtained under guard perturbations only, i.e., R 0

∆→0 = R ε→0 ∆→0 = R ε→0 0 .
On the one hand, we exploit the new techniques introduced by Puri and we clarify and reprove some of his lemmas, and on the other hand, we also introduce new lemmas and proof techniques to bridge over some gaps of Puri's papers, and extend his results to the semantics with guard perturbations. We proceed with the following steps:

1. in Section 4, we recall classical results about regions and zones for timed automata.

We essentially follow the work of Puri; 2. in Section 5, we show that the robust safety verification problem reduces to the computation of the set

R ε→0 ∆→0 = T ∆>0 T ε>0 Reach( A ε ∆ ) (Theorem 15
). This has no counterpart in [START_REF] Puri | Dynamical properties of timed automata[END_REF]. 3. in Section 6, we show that Algorithm 1 below (due to Puri) computes R ε→0 ∆→0 = R 0 ∆→0 = R ε→0 0 : (a) in Section 6.1, we study the structure of the cycles of timed automata and of their region graph. This is important because cycles allow perturbations to accumulate (see the example of Section 2). The material in this section is essentially due to Puri, and the detailed proofs follow his ideas; (b) in Section 6.2, we show that Algorithm 1 is sound, i.e., the set J * it computes is contained in R 0 ∆→0 and in R ε→0 0 (Theorem 39). This part required 3 pages for R 0 ∆→0 and 5 pages for R ε→0 0 , to give a precise justification of the 5 lines in [Pur00, Lemma 7.11]; (c) in Section 6.3, we show that Algorithm 1 is complete, i.e., the set J * it computes contains R ε→0 ∆→0 (Theorem 46). Our approach to establish the key lemmas of [Pur00, Section 8.2] uses an original technique based on parametric DBMs, which allows to extend Puri's results to both guard perturbations and clock drifts; 4. in Section 7, we show that the safety verification problem is PSPACE-complete, as claimed by Puri.

Several results in this paper are highly technical, and all proofs are given in details. To help the reader, we give overviews of the main technical developments in the beginning of Sections 6, 6.2 and 6.3.

Properties of Regions and Zones

We review the important properties of the clock regions and zones of timed automata, for a heavy use in the sequel.

Clock regions. According to Definition 4, a clock region of a timed automaton contains a set of valuations that agree on the integral part of the clocks and on the ordering of their fractional parts. We make this characterization of clock regions more concrete with the following representation [START_REF] Puri | Dynamical properties of timed automata[END_REF].

Definition 12 Given a timed automaton A with n clocks (Var = {x 1 , . . . , xn}) and largest constant M , we represent a clock region of A by: 1. a tuple of (a 1 , . . . , an) of elements of {0, 1, ..., M, ⊥}; 2. and a tuple (X 0 , X 1 , . . . , X k ) of k + 1 (0 k n) sets of clocks that form a partition of the clocks that have a value less than M . Those sets are required to be non-empty, except X 0 . Formally, let

Var M = {x i ∈ Var | a i = ⊥}. We require that Var M = X 0 ∪ • • • ∪ X k , X i ∩ X j = ∅ if i = j and X i = ∅ for all 1 i k.
The clock region characterized by a tuple (a i ) 1 i n and (X i ) 0 i k is the set of all valuations v : Var → R 0 such that:

1. For all x i ∈ Var: v(x i ) > M iff a i = ⊥, and if a i = ⊥ then v(x i ) = a i ;
2. for all x, y ∈ Var M : v(x) < v(y) iff for some i < j, x ∈ X i and y ∈ X j ; 3. and for all x ∈ Var M : v(x) = 0 iff x ∈ X 0 .

A more classical way to represent clock regions is by the set of constraints it satisfies. Our representation of a clock region r is easily translated to a set of constraints that are satisfied by (and only by) valuations of r. A valuation v belongs to the clock region represented by (a i ) 1 i n and (X i ) 0 i k if and only if v satisfies the following constraints [START_REF] Alur | A theory of timed automata[END_REF]:

-x i > M for each x i such that a i = ⊥; -x i = a i for each x i ∈ X 0 ; -a i < x i < a i + 1 for each x i ∈ X l for some l > 0; -x i -a i < x j -a j for each x i , x j such that x i ∈ X l and x j ∈ Xm for some 0 < l < m; -x i -a i = x j -a j for each x i , x j ∈ X l for some l > 0.
Example. In a timed automaton with 5 clocks and largest constant M = 8, a clock region r represented by (1, 3, 5, ⊥, 2) and ({x 1 , x 3 }, {x 2 }, {x 5 }) satisfies the following constraints:

0 = x 1 -1 = x 3 -5 < x 2 -3 < x 5 -2 < 1 ∧ x 4 > 8.
The closure [r] of r then satisfies:

0 = x 1 -1 = x 3 -5 x 2 -3 x 5 -2 1 ∧ x 4 8.
Vertices of a clock region. For a set S ⊆ R n , let Conv(S) be the convex hull of S, i.e., the smallest convex set containing S. Since clock regions are bounded, they are convex polytopes, and can also be defined as the convex hull of a finite set of points:

Definition 13 Let r be a clock region of a timed automaton. The set of vertices of r is the smallest set of points S(r) such that [r] = Conv(S(r)).

Lemma 14 shows that the set S(r) is unique and the number of vertices is at most n + 1, where n is the number of clocks of the automaton.

Lemma 14

The vertices of a clock region r are the integer vectors of its closure:

S(r) = [r] ∩ N n . Proof. Let v ∈ [r].
Let the representation of r be given as (a i ) 1 i n and (X i ) 0 i k . Then, for all valuations w ∈ [r] we have:

∀0 i k. ∀x, y ∈ X i . w(x) = w(y) , ∀0 i < j k. ∀x ∈ X i , y ∈ X j . w(x) w(y) , ∀x ∈ X 0 . w(x) = 0,
Let v 0 be the valuation such that v 0 (x i ) = a i for each 0 i k. We have v 0 ∈ [r] and for all 0 < j k, the valuation v j defined by

v j (x) = v 0 (x) if x ∈ X i with i < j v j (x) = v 0 (x) + 1 if x ∈ X i with i j belongs to [r].
We now prove that those valuations generate the whole closed clock region [r]. Let w be a valuation in [r]. We define

w = (1 -w(x k ) ) • v 0 + ( w(x 1 ) -w(x 0 ) ) • v 1 + • • • + ( w(x k ) -w(x k-1 ) ) • v k
where each x i is a clock in the corresponding X i for 1 i k, and w(x 0 ) = 0 by convention. We claim that w = w. To show this, let y be a clock in some X j . Then

w (y) = (1 -w(x k ) ) • v 0 (y) + ( w(x 1 ) -w(x 0 ) ) • v 1 (y) + • • • + ( w(x k ) -w(x k-1 ) ) • v k (y) = (1 -w(x k ) ) • v 0 (y) + ( w(x 1 ) -w(x 0 ) ) • (v 0 (y) + 1) + • • • + ( w(x j ) -w(x j-1 ) ) • (v 0 (y) + 1)+ ( w(x j+1 ) -w(x j ) ) • (v 0 (y)) + • • • + ( w(x k ) -w(x k-1 ) ) • (v 0 (y)) = v 0 (y) + w(x j ) = w(y)
since y ∈ X j . Therefore [r] = Conv({v 0 , . . . , v k }). On the other hand, {v 0 , . . . , v k } is the smallest set generating [r], since there is no valuation v i that is a convex combination of the others. Lemma 14 entails that if a clock region r is a sub-region of a clock region r , then its set of vertices S(r) is the intersection of [r] and the set S(r ) of vertices of r .

Zones and DBMs. Related to the algorithmic analysis of timed automata, an efficient data structure has been introduced to represent zones: the difference bound matrices (DBM) [START_REF] Berthomieu | An enumerative approach for analyzing time Petri nets[END_REF][START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF]. We briefly introduce DBMs and show how the basic operations that are useful for reachability analysis are computed3 .

Let x 1 , . . . , xn be the clocks of a timed automaton. The idea of DBMs is to represent all constraints uniformly, by constraints of the form x i -x j a with a ∈ Z ∪ {+∞} and 0 i, j n where x 0 is the constant 0. For bounded zones, the range of a can be reduced to Z ∩ [-M, M ] where M is the largest constant of the timed automaton.

A DBM is a (n + 1) × (n + 1) matrix M = `mi,j ´0 i,j n where each m i,j is of the form (a i,j , ≺ i,j ) where ≺ i,j ∈ {<, } and a i,j ∈ Z is called a bound. In the sequel, we only consider DBMs that represent closed sets, that is, DBMs where ≺ i,j is always . The set of valuations represented by the DBM M = `mi,j ´0 i,j n is:

M = {(x 1 , . . . , xn) ∈ R n | ∀ 0 i, j n : x i -x j m ij ∧ x 0 = 0}.
A DBM is associated with a complete directed graph with nodes 0, 1, . . . , n and edges (i, j) labeled by m ij . In this graph, the length of a path is the sum of the labels of the edges in the path. It is easy to see that the length of a path from node i to node j is an upper bound of the difference x i -x j . The length of the shortest paths between nodes gives the tightest bounds on the variables and difference of variables. This allows to define a normal form for DBMs that corresponds to the shortest path closure of the associated directed graph. If the graph contains a cycle of negative length, the shortest path closure does not exist and the DBM represents the empty set as a constraint of the form x i -x i m with m < 0 is unsatisfiable. Hence, for nonempty DBMs in normal form, we have m i,i = 0 for all 0 i n.

Operations on sets represented by DBMs are executed by syntactic transformations on the DBM. Some of those operations require the normal form. We present the operations that will be useful in the sequel. Other operations like the difference of two DBMs and the inclusion test are definable (see e.g. [ACD + 92, Yov96, CGP99] for details).

-Intersection: given two DBMs M = `mi,j ´0 i,j n and M = `m i,j ´0 i,j n , let M be the DBM such that m i,j = min{m i,j , m i,j }. Then, we have M = M ∩ M . It is not required that M and M are in normal form. In any case the result is not necessarily in normal form.

-Time passing: given a DBM in normal form M = `mi,j ´0 i,j n , let M be the DBM `m i,j ´0 i,j n such that m i,0 = ∞ and m i,j = m i,j for all 0 i, j n with j = 0. This removes the upper bound on all the clocks. We have

M = {v + t | v ∈ M ∧ t ∈ R 0 } and M is in normal form.
-Reset: given a DBM in normal form M = `mi,j ´0 i,j n and a clock x, let M[x := 0] be the DBM `m i,j ´0 i,j n such that for all 0 i, j n with i = j:

m i,j = 8 > < > : m 0,j if x = x i m i,0 if x = x j m i,j otherwise
We have removed all the bounds involving x and set x to zero. We have

M[x := 0] = {v[x := 0] | v ∈ M }. We define similarly M[R := 0] for R ⊆ {x 1 , . . . , xn}.
The result is in normal form. -Emptiness test: given a DBM M = `mi,j ´0 i,j n , we have M = ∅ if and only if there is a cycle in the directed graph associated to M whose length is negative. The emptiness test is realized by the shortest path algorithm used to put DBMs in normal form.

Removing existential quantification

This first part of the proof of Theorem 11 consists in removing the existential quantification on ∆ and ε. Given a timed automaton A, we let R ε→0 ∆→0 = T ∆>0 T ε>0 Reach( A ε ∆ ). We then have the following result:

Theorem 15 For any timed automaton A, any zone-set Bad, the following equivalence holds:

R ε→0 ∆→0 ∩ Bad = ∅ iff ∃∆ > 0, ε > 0 : Reach( A ε ∆ ) ∩ Bad = ∅.
The proof of Theorem 15 is based on several intermediate lemmas. Lemma 16 corrects a wrong claim of Puri about a lower bound on the distance between two zones with empty intersection. This bound is claimed to be 1 2 in [Pur98, Lemma 6.4]. We show that 1 n is the tightest bound, where n is the number of clocks. We introduce the following classical distances over R n :

d∞(x, y) = x -y ∞ = max 1 i n (|x i -y i |) d 1 (x, y) = x -y 1 = X 1 i n (|x i -y i |).
Lemma 16 Let Z 1 , Z 2 ⊆ R n be two zones such that Z 1 ∩ Z 2 = ∅. For all x ∈ Z 1 and y ∈ Z 2 , we have d∞(x, y)

1 n . This bound is tight.

Proof. First, we show that 1 n is a lower bound. Clearly, for all v ∈ R n , v 1 n • v ∞. We prove that x -y 1 1, which entails the result.

We consider two zones given by two DBMs in normal form:

Z 1 ≡ `mi,j ´ and Z 2 ≡ `m i,j
´ . Since Z 1 ∩ Z 2 = ∅, there must exist a "negative cycle":

m ( ) i1,i2 + m ( ) i2,i3 + m ( ) i3,i4 + • • • + m ( ) ip,i1
-1

where each term m ( ) i,j of the sum can be taken either in the matrix of Z 1 or in the matrix of Z 2 . We may assume that at least one m ( ) i,j comes from Z 1 and one from Z 2 since otherwise Z 1 (or Z 2 ) would be empty and the result would hold vacuously.

Since for DBMs in normal form, we have m a,b + m b,c ma,c for all indices a, b, c, we can merge any two consecutive m i,j into one while keeping the inequality. The same holds for m i ,j , and we can thus assume that m i,j and m i ,j alternate in the sum above (starting with m i1,i2 , say).

Pick x ∈ Z 1 and y ∈ Z 2 . Then

(x i2 -x i1 ) + (y i3 -y i2 ) + (x i4 -x i3 ) + • • • + (y i1 -y ip ) -1.
Terms can be rearranged in this sum, yielding

(y i1 -x i1 ) -(y i2 -x i2 ) + (y i3 -x i3 ) -• • • -(y ip -x ip ) -1.
If i k = 0 for some k, then x i k -y i k = 0. Thus, we assume that 1 i k n. We take the absolute value, and apply the triangle inequality:

1 ˛(y i1 -x i1 ) -(y i2 -x i2 ) + (y i3 -x i3 ) -• • • -(y ip -x ip ) ˛ |(y i1 -x i1 )| + |(y i2 -x i2 )| + |(y i3 -x i3 )| + • • • + |(y ip -x ip )| x -y 1 .
Now, let us show that this bound is tight. Consider the zones Z 1 , Z 2 ⊆ R n defined by the following equations:

-If n is odd Z 1 ≡  x 1 = 1 x 2i -x 2i+1 = 0 1 i n-1 2 Z 2 ≡  x 2i-1 -x 2i = 0 1 i n-1 2 xn = 0 x1 x3 x2 -If n is even Z 1 ≡ 8 < : x 1 = 1 x 2i -x 2i+1 = 0 1 i n 2 -1 xn = 0 Z 2 ≡ ˘x2i-1 -x 2i = 0 1 i n 2 x1 x2
We have Z 1 ∩ Z 2 = ∅; indeed combining the equations of Z 1 and Z 2 yields x i = x j for all 0 i, j n, which leads to a contradiction since x 1 = 1 and xn = 0. On the other hand, let p = (1, n-2 n , n-2 n , n-4 n , n-4 n , . . . ) and q = ( n-1 n , n-1 n , n-3 n , n-3 n , n-5 n , . . . ) (take the first n coordinates). It is easy to check that p ∈ Z 1 and q ∈ Z 2 , while d∞(p, q) = max( 1 n , . . . ,

1 n ) = 1 n .
In order to prove Lemma 16 in presence of both kinds of perturbation, we have to extend the previous lemma to sequences of sets as follows:

Lemma 17 Let A δ be a collection of sets such that A δ1 ⊆ A δ2 if δ 1 δ 2 . Assume that Z = T δ>0 A δ is a nonempty zone-set. Also assume the existence of a zone-set Z such that ∃δ 0 > 0 • ∀δ ∈ (0, δ 0 ) • A δ ∩ Z = ∅. Then there exists δ 1 > 0 such that for all 0 < δ < δ 1 , we have d∞(A δ , Z ) 1 2n . Proof. We pick δ 0 > 0 such that ∀0 < δ < δ 0 • A δ ∩ Z = ∅, and δ 0 > 0 such that ∀x ∈ A δ 0 • ∃z ∈ Z : d∞(x, z) < 1 2n . ( 1
)
Such a δ 0 exists by definition of Z. Assume the lemma is wrong:

∀δ 1 > 0 • ∃0 < δ < δ 1 • ∃x ∈ A δ , y ∈ Z : d∞(x, y) < 1 2n .
Applying this result with δ 1 = min(δ 0 , δ 0 ), we pick a δ 1 > 0, and two points x ∈ A δ 1 and y ∈ Z such that d∞(x, y) < 1 2n . From (1), and since A δ 1 ⊆ A δ 0 , there exists z ∈ Z such that d∞(x, z) < 1 2n . Thus d∞(y, z) < 1 n , and with Lemma 16, Z ∩ Z = ∅. Then any A δ intersects Z , since it contains Z. This contradicts our hypotheses.

In the sequel, when a distance d or a norm • is used, we always refer to d∞ and • ∞.

The following two lemmas rely on the theory of real numbers and the basics of topology. Our main tool for proving Theorem 15 can then be stated as follows:

Lemma 20 Let A ∆ (∆ ∈ R >0 ) be a collection of closed sets such that A ∆1 ⊆ A ∆2 if ∆ 1 ∆ 2 . Assume that A = T ∆>0 A ∆ is nonempty. Let B be a bounded set. If d(A, B) > 0, then there exists ∆ > 0 such that A ∆ ∩ B = ∅. Define N∞(X, η) = {x ∈ R n | ∃x ∈ X : d∞(x, x )
η} and let N∞(x, η) = N∞({x}, η).

Proof. For a contradiction, assume that for all ∆ > 0, we have

A ∆ ∩ B = ∅. Let δ i = 1
i (for each i 1). Then, we have:

∀i 1 • ∃x i ∈ A δi ∩ B.
Since B is bounded, so is the set {x i | i 1}. By Bolzano-Weierstrass Theorem, there exists a point x such that:

∀ε > 0 • ∀i 1 • ∃j i : x j ∈ N∞(x, ε) ∩ A δj .
Let us show that x is in the closure of A δi for all i 1. Since A δj ⊆ A δi for all j i, we have:

∀i 1 • ∀ε > 0 • ∃j : x j ∈ N∞(x, ε) ∩ A δi ,
that is:

∀i 1 • ∀ε > 0 : N∞(x, ε) ∩ A δi = ∅.
Hence, for all i 1 the point x is in the closure of the closed set A δi , and thus x ∈ A δi .

Since, for all ∆ > 0 there exists i 1 such that δ i ∆ and thus A δi ⊆ A ∆ , we have ∀∆ ∈ R >0 : x ∈ A ∆ . This entails that x ∈ A. Now observe that:

∀i 1 : d∞({x}, B) d∞(x, x i ) + d∞({x i }, B).
Observe that d∞(x, x i ) can be made arbitrarily small for sufficiently large i, and that for all i 1, d∞({x i }, B) = 0 since x i ∈ B. Therefore, we get:

∀ε > 0 : d∞({x}, B) ε,
and d∞({x}, B) = 0, which is a contradiction.

We conclude this section by the proof of Theorem 15.

Proof of Theorem 15.

Let R ε→0 ∆ = T ε>0 Reach( A ε ∆ ), for any ∆ > 0. If R ε→0 ∆→0 ∩ Bad = ∅, since R ε→0
∆→0 and Bad are unions of sets of the form {l} × Z l where Z l is a zone 4 , Lemma 16 applies and we have d(R ε→0 ∆→0 , Bad) > 0. From Lemma 20, we obtain that there exists ∆ > 0 such that R ε→0 ∆ ∩ Bad = ∅. Clearly, R ε→0 ∆ satisfies the conditions of Lemma 17, hence the existence of some ∆ 1 such that ∀∆ ∈ (0, ∆ 1 ), we have d(R ε→0 ∆ , Bad) > 0. We pick such a ∆ 0 ∈ (0, ∆ 1 ). Applying Lemma 20 to R ε→0 ∆0 , we get the existence of ε 0 such that Reach( A ε0 ∆0 ) ∩ Bad = ∅. Conversely, if there exists ∆ > 0 and ε > 0 such that Reach(

A ε ∆ ) ∩ Bad = ∅, then trivially R ε→0 ∆→0 ∩ Bad = ∅.
It should be noted that a simpler proof could be achieved in the presence of only one perturbation (for guard enlargement only, such a proof can be found in [START_REF] De Wulf | Robustness and implementability of timed automata[END_REF]).

6 An algorithm for computing R 0 ∆→0 , R ε→0 0 and R ε→0

∆→0

In this section, we prove that R 0 ∆→0 = R ε→0 0 = R ε→0 ∆→0 , and that those sets are computed by Algorithm 1 (originally proposed in [START_REF] Puri | Dynamical properties of timed automata[END_REF] to compute R ε→0 0 ). The following example illustrates the algorithm, and informally justifies its correctness. The rest of this section is devoted to a formal proof of correctness.

Example. Consider the timed automaton Aα of Fig. 1(a) (the value of α does not matter here). The reachable states of Aα in locations 1 and 2 are depicted on Fig. 1(b) and are computed in J * by the algorithm at line 3. Then, in the while-loop, the algorithm adds to J * the progress cycles of the region graph of Aα that "touch" the set J * , and performs a reachability analysis from the new states in the classical semantics. In the example, the progress cycle ( 1 , R 1 ), ( 1 , R 2 ), ( 1 , R 3 ), ( 2 , R 4 ) shown Algorithm 1: Algorithm for computing the limit sets R ε→0 ∆→0 , R 0 ∆→0 and R ε→0 0 of a closed timed automaton A.

Data: A timed automaton A = Loc, Var, q 0 , Lab, Edg .

Result: The set J * , which we will prove equals R ε→0 ∆→0 , R 0 ∆→0 and R ε→0

1 2 2 3 3 1 R 1 R 2 R 3 2 R 4 Fig. 2 A progress cycle R 1 , R 2 , R 3 , R 4 in the region graph of Aα of Fig. 1(a).
in Fig. 2 is added, and the set J * computed by the algorithm is the set R 0 ∆→0 shown in Fig. 1(c).

Observe that the algorithm manipulates only closed regions. In particular, the set J * is closed by Lemma 6. The condition J * ∩ [p 0 ] = ∅ at line 4 implies that some points of J * belong to the frontier of p 0 . It is clear that in the perturbed semantics of timed automata, no matter the values of ε, ∆ > 0, some states of p 0 are reachable. Moreover, as we show in the sequel, every state of p 0 can actually be reached from every state of [p 0 ] (and thus from J * ∩ [p 0 ]), by repeating the cycle p = p 0 p 1 . . . p k sufficiently many times (the number of iterations increases as ε and ∆ tend to 0).

The main technique to prove that a state u ∈ [p 0 ] can reach a state v ∈ [p 0 ] in A 0 ∆ and in A 0 ε is the following. Assume that there is a trajectory in A 0 0 that starts and ends in u and follows the cycle p, called a limit cycle. We modify this trajectory using the perturbation ε or ∆ to reach a state u 1 in the neighborhood of u. This is done in Theorem 29 for A 0 ∆ and in Theorem 31 for A 0 ε . By repeating this, we construct u 2 , . . . u k = v such that u i is reachable from u i-1 in A 0 ∆ (Theorem 28) and in A 0 ε (Theorem 30). Unfortunately, we cannot assume in general that u ∈ [p 0 ] has a limit cycle in A 0 0 , even though p 0 has a cycle in the region graph of A [START_REF] Puri | Dynamical properties of timed automata[END_REF]. We are saved by Theorem 23 which shows that (i) from all states x ∈ [p 0 ], there is a trajectory in A 0 0 that reaches a state u ∈ [p 0 ] that has a limit cycle, and dually (ii) all states y ∈ [p 0 ] are reachable in A 0 0 from some state v ∈ [p 0 ] that has a limit cycle. Notice that Theorem 23 does not involve perturbations.

Limit cycles

Definition 21 (Limit Cycle) A limit cycle of a timed automaton A is a finite trajectory π of A that contains at least one discrete transition and such that last(π) = first(π).

As suggested in [START_REF] Puri | Dynamical properties of timed automata[END_REF], not all states of a progress cycle have a limit cycle.

Definition 22 Let p = p 0 p 1 . . . p N be a cycle in the region graph of a timed automaton A (i.e., p N = p 0 ). For Q 0 ⊆ [p 0 ], define the return map Rp(Q 0 ) as follows:

Rp(Q 0 ) = ( q ∈ [p 0 ]
˛there exists a trajectory π of A that follows p such that first(π) ∈ Q 0 and last(π) = q

) For i 2, define recursively R i p (Q 0 ) = Rp(R i-1 p (Q 0 )
) and let L i,p be the set of states that can return back to themselves after i cycles through p: L i,p = {q | q ∈ R i p ({q})}. We write Lp = ∪ i∈N>0 L i,p the set of states having a limit cycle.

The following key property of Lp is central to the proof of correctness of Algorithm 1. It states that Lp is both forward and backward reachable from all valuations in a cycle p.

Theorem 23 ([Pur98, Lemma 7.10]) Let p = p 0 . . . p N be a cycle in the region graph of a timed automaton. For all z ∈ [p 0 ], there exists z and z in Lp, and trajectories π and π in A , such that:

first(π) = z and last(π) = z and first(π ) = z and last(π ) = z.

The proof proposed by Puri is quite sketchy. We develop here a full proof of this result, following the same steps.

Lemma 24 ([Pur98, Lemma 7.1]) Let p = p 0 p 1 . . . p N be a path in the region graph of a timed automaton A, let π and π be two trajectories of A that follow p. Then for all λ ∈ [0, 1], there exists a trajectory π of A that follows p and such that first(π ) = λ.first(π) + (1 -λ).first(π ) and last(π ) = λ.last(π) + (1 -λ).last(π ).

Proof. Let π = (q 0 , t 0 ) σ 1 (q 1 , t 1 ) σ 2 • • • σ N (q N , t N ) and π = (q 0 , t 0 ) σ 1 • • • σ N (q N , t N ). Consider the sequence π = (q 0 , t 0 ) σ 1 (q 1 , t 1 ) σ 2 • • • σ N (q N , t N )
where for all 0 i N , q i = λ.q i + (1 -λ).q i and t

i = λ.t i + (1 -λ).t i and for all 1 i N , σ i = λ.σ i + (1 -λ).σ i if σ i ∈ R 0 and σ i = σ i otherwise.
It is easy to show that π is a trajectory in A since regions are convex sets.

Lemma 25 ([Pur98, Lemma 7.3]) Let p be a cycle in the region graph of a timed automaton. Then Lp is convex.

Proof. Let x, y ∈ Lp, and λ ∈ [0, 1]. There exists natural numbers k and l such that x ∈ L k,p and y ∈ L l,p . Then x, y ∈ L k.l,p , and according to Lemma 24, we have λ

.x + (1 -λ).y ∈ L k•l,p ⊆ Lp.
Definition 26 Let p = p 0 p 1 . . . p N be a cycle in the region graph of a timed automaton (i.e. p 0 = p N ). The orbit graph of p is the graph Θp = (V Θ , → Θ ) such that V Θ = S(p 0 ) is the set of vertices of p 0 and for all v, w ∈ V Θ , v → Θ w iff w ∈ Rp({v}). For m ∈ N and v ∈ V Θ , we define

Succ m (v) = {w ∈ V Θ | v → m Θ w} and Pred m (v) = {w ∈ V Θ | w → m Θ v}.
Given a vertex v ∈ V Θ , the set Rp({v}) is a closed region according to Lemma 6, and thus we have Rp({v}) = Conv({w ∈ V Θ | v → Θ w}) as a closed region contains all its vertices. More generally, we have

R k p ({v}) = Conv({w ∈ V Θ | v → k Θ w}) for all k 1.
Lemma 27 ([Pur98, Lemma 7.4]) Let p = p 0 . . . p k be a path in the region graph of a timed automaton A. For all vertices v ∈ S(p 0 ) of p 0 , there exists a vertex v ∈ S(p k ) of p k such that there exists a trajectory of A from v to v , and conversely, for all vertices v ∈ S(p k ) of p k , there exists a vertex v ∈ S(p 0 ) of p 0 such that there exists a trajectory of A from v to v . The same argument can be applied backwardly, since the predecessor of a subregion of p k is a closed subregion of p 0 .

Proof of Theorem 23. Let Θp = (V Θ , → Θ ) be the orbit graph of p. Let V = {v ∈ V Θ | ∃m ∈ N. v ∈ Succ m (v)}. Lemma 27 entails that every vertex in the orbit graph has an outgoing edge. Thus for all v ∈ V Θ , there exists an integer mv such that for any m mv, the intersection Succ m (v) ∩ V is non-empty, because V Θ is finite. Let M = max{mv | v ∈ V Θ } be the largest such mv. Then Succ M (v) ∩ V = ∅ for all v. A similar argument proves the existence of M such that Pred M (v) ∩ V = ∅ for all v.

Since z ∈ [p 0 ], we can write z = P i λ i v i , where λ i ∈ [0, 1], P i λ i = 1 and v i ∈ V Θ . For each v i , let w i be an element of Succ M (v i ) ∩ V . From Lemma 24, there is a path from z to z = P i λ i w i and z ∈ Conv(V ). By Lemma 25 we have Conv(V ) ⊆ L and thus z ∈ L.

Conversely, if x i is a vertex in Pred M (v i ) ∩ V , there is a path from z = P i λ i x i ∈ Conv(V ) ⊆ L to z.

Soundness of Algorithm 1: J

* ⊆ R 0 ∆→0 and J * ⊆ R ε→0 0
We show that the set J * computed by Algorithm 1 is reachable in the limit sets R 0 ∆→0 and R ε→0 0 . In particular, for all progress cycles that are added to J * by the algorithm, we show that every point of the cycle is reachable if either a drift on clocks or an enlargement of the guards is allowed, no matter how small it is.

The proof is based on Theorem 23 and on the fact that for all progress cycles p, the set Lp is a strongly connected component of both A 0 ∆ and A ε 0 for all ∆, ε > 0. Hence in Lp, every state is reachable from every state for the perturbed semantics, and thus similarly, in each region of the cycle p every state is reachable from every state by Theorem 23.

Apart from Theorem 39, all the results of this section apply to progress cycles but do not require Assumption 9.

Imprecise guards: J * ⊆ R 0 ∆→0 .

Theorem 28 Let A be a timed automaton, let p = p 0 p 1 • • • p N be a progress cycle of the region graph of A, and ∆ ∈ R >0 . For all states u, v ∈ Lp, there exists a trajectory

π of A 0 ∆ such that first(π) = u and last(π) = v.
This theorem results immediately from the following lemma.

Lemma 29 Let A be a timed automaton, let p = p 0 p 1 • • • p N be a progress cycle of the region graph of A. For all ∆ ∈ R >0 , for all state u ∈ Lp and for all neighbour state v ∈ [p 0 ] ∩ N∞(u, ∆ 2 ), there exists a trajectory π of A 0 ∆ such that first(π ) = u and last(π ) = v.

Proof. Let A = Loc, Var, q 0 , Lab, Edg . Since u ∈ Lp, there exists a trajectory π of A 0 0 that follows p a certain number of times and such that first(π) = last(π) = u. We slightly modify π to make it stutter-free (we insert a zero length timed transition between two consecutive discrete transitions, and we merge consecutive timed transitions). Assume that5 :

π = ( 0 , u 0 ) t0 -→ ( 0 , u 0 ) σ0 --→ R0 ( 1 , u 1 ) t1 -→ ( 1 , u 1 ) σ1 --→ R1 • • • • • • σm-2 ----→ Rm-2 ( m-1 , u m-1 ) tm-1 ----→ ( m-1 , u m-1 ) σm-1 ----→ Rm-1 ( m, um) tm --→ ( m, u m )
with u 0 = u m = u. Each t i ∈ R 0 and σ i ∈ Σ. We annotate π with sets of clocks R i ⊆ Var that are reset by discrete transitions σ i . Note that S i=m-1 i=0 R i = Var by Assumption 9.

Intuitively, we prove the lemma by modifying the length of the timed transitions of π so that the clocks are reset slightly earlier or later than in π. We obtain a trajectory of A 0 ∆ because the guards are enlarged and therefore they are enabled in the states of the new trajectory.

Let the representation of p 0 be given by (ax) x∈Var and (X i ) 0 i k . For all valuations w ∈ p 0 , we have:

for all x ∈ Var: w(x) = ax; for all x ∈ X 0 : w(x) = 0; for all i and for all x, y ∈ X i : w(x) = w(y) ; for all i < j and for all x ∈ X i , y ∈ X j : w(x) < w(y) ; By hypothesis, p is a progress cycle and each clock is reset at least once along π. For each clock x ∈ Var, let αx be the index of the last transition of π in which x is reset. Formally, we have:

x ∈ Rα x ∀i > αx : x ∈ R i (2)
Then, for each clock x ∈ Var, we have:

u 0 (x) = u m (x) = u(x) = m X i=αx+1 t i (3) Let v ∈ [p 0 ] ∩ N∞(u, ∆
2 ) and for each x ∈ Var let δx = v(x) -u(x). Clearly, we have |δx| for all x ∈ Var: 0 v(x) 1; for all x ∈ X 0 : v(x) = 0; for all i and for all x, y ∈ X i : v(x) = v(y) ; for all i < j and for all x ∈ X i , y ∈ X j : v(x) v(y) ;

This entails that:

for all i and for all x, y ∈ X i : δx = v(x) -u(x) = v(y) -u(y) = δy; for all x, y ∈ Var such that u(x) < u(y) (and hence αx > αy from Eq. ( 3)), we have v(x) v(y) and thus u(x) + δx u(y) + δy, that is:

δx -δy u(y) -u(x) = αx X i=αy+1 t i (4)
Let Γ = {αx | x ∈ Var} = {α 1 , . . . , α l } be the set of positions in π where a clock is reset for the last time. Assume without loss of generality that α 1 < α 2 < • • • < α l and that for all 1 i l, the clock x i ∈ Var is such that that αx i = α i . Consider the time stamps in π as the following block-sequence, and construct the sequence (t i ) 0 i m by adding a shift given as follows: ˆt0 . . . tα 1 ˜ˆt α1+1 . . . tα 2 ˜. . . ˆtαj-1+1 . . . tα j ˜. . . ˆtα l-1 +1 . . . tα l ˜ˆt α l +1 . . . tm +0 each t i is obtained from t i by distributing the shift of each block over the time stamps of the block. This can be done in such a way that each t i is nonnegative for all 0 i m since for all i α 1 we have t i = t i , for all 2 j l we have:

+δ 1 -δ 2 . . . +δ j-1 -δ j . . . +δ l-1 -δ l +δ l = ˆt 0 . . . t
αj X i=αj-1+1 t i = 0 @ αj X i=αj-1+1 t i 1 A + δ j-1 -δ j 0
(by Eq. ( 4))

and finally for all i α l + 1 we have:

m X i=α l +1 t i = m X i=α l +1 t i + δ l = u(x l ) + δ l = v(x l ) 0.
We now construct the trajectory π from π by replacing each t i by t i :

π = ( 0 , v 0 ) t 0 -→ ( 0 , v 0 ) σ0 --→ R0 ( 1 , v 1 ) t 1 -→ ( 1 , v 1 ) σ1 --→ R1 • • • • • • σm-2 ----→ Rm-2 ( m-1 , v m-1 ) t m-1 ----→ ( m-1 , v m-1 ) σm-1 ----→ Rm-1 ( m, vm) t m --→ ( m, v m )
where v 0 = u 0 = u, for all 0 i m :

v i = v i + t i and for all 1 i m : v i = v i-1 [R i-1 := 0]. We claim that π is a trajectory of A 0 ∆ .
To show this, we must verify that the guard (which is enlarged by ∆ in A 0 ∆ ) of each discrete transition σ i is satisfied by v i . Since π is a trajectory of A , we know that each u i satisfies the corresponding guard under the classical semantics. Therefore, it is sufficient to prove that the difference |u i (x) -v i (x)| is bounded by ∆ for all x ∈ Var. To do that, let j be the greatest index such that j i and u j (x) = v j (x) (such an index exists because u 0 = v 0 ). Clearly, the difference |u i (x) -v i (x)| is bounded by the sum of the shifts that we have introduced between index j and i. For uniformity, let the first shift be δ 0 -δ 1 with δ 0 = δ 1 and the last shift be δ l -δ l+1 with δ l+1 = 0. Notice that

|δ i | ∆ 2
holds for all i = 0, . . . , l + 1. If a block ˆtαp-1+1 . . . tα p ˜is such that j α p-1 + 1 and αp i, then the whole shift δ p-1 -δp counts in the sum. On the other hand, if i or j lies inside the block, then only a portion α(δ p-1 -δp) of the shift counts where α ∈ [0, 1]. Accordingly, the sum of the shifts can take one of the three forms (where α, β ∈ [0, 1]):

• s 1 = α(δp -δ p+1 ) (if i and j lie in the same block) • s 2 = α(δp -δ p+1 ) + β(δ p+1 -δ p+2 ) (if i and j lie in consecutive blocks) • s 3 = α(δp -δ p+1 ) + δ p+1 -δq + β(δq -δ q+1 ) (otherwise)
It is easy to show the following bounds:

• |s 1 | α • 2 • ∆ 2 ∆ • |s 2 | = |α(δp -δ p+2 ) + (β -α)(δ p+1 -δ p+2 )| α • ∆ + |β -α|∆ |s 2 | = |(α -β)(δp -δ p+1 ) + β(δp -δ p+2 )| |α -β|∆ + β • ∆ ) ⇒ |s 2 | ∆ • |s 3 | = |α(δp -δ q+1 ) + (1 -β)(δ p+1 -δq) + (β -α)(δ p+1 -δ q+1 )| |s 3 | = |(α -β)(δp -δq) + (1 -α)(δ p+1 -δq) + β(δp -δ q+1 )| ) ⇒ |s 3 | ∆ which shows that |u i (x) -v i (x)| ∆ for all x ∈ Var.
Finally, since the sets of clocks R i that are reset in π are the same as in π, Eq. (3) applies and we get for all x ∈ Var:

v m (x) = m X i=αx+1 t i = m X i=αx+1 t i + δx = u m (x) + δx = u(x) + δx Hence v m = v. It follows that first(π ) = u and last(π ) = v as required. Drifting clocks: J * ⊆ R ε→0 0 .
We prove a result similar to Theorem 28 for drifting clocks.

Theorem 30 (See also [START_REF] Puri | Dynamical properties of timed automata[END_REF]Lemma 7.11]) Let A be a timed automaton, let p = p 0 p 1 • • • p N be a progress cycle of the region graph of A, and ε ∈ R >0 . For all states u, v ∈ Lp, there exists a trajectory π of A ε 0 such that first(π) = u and last(π) = v.

The proof of Theorem 30 relies on the following lemma, implying that it is possible to go from a state x 0 = u ∈ Lp to a state x k = v ∈ Lp in A ε 0 by successively reaching x 1 , x 2 , . . . x k where x i+1 is at bounded distance from x i . The key is that the bound depends only on the extremal states u and v.

Lemma 31 Let A be a timed automaton and p = p 0 p 1 • • • p N be a progress cycle of the region graph of A. For all u, v ∈ Lp, for all ε ∈ R >0 , there exists δ > 0 such that for all x ∈ Conv({u, v}) and for all y ∈ Lp ∩ N∞(x, δ), there exists a trajectory π in A ε 0 such that first(π) = x and last(π) = y.

To prove Lemma 31, we apply a drift on a limit cycle trajectory starting in u. Since the effect of drifts is proportional to the duration of the trajectory, we need a bound on the minimal duration of such a trajectory, in order to guarantee a lower bound on the perturbation that we can enforce. This is done in Lemma 32. Then, to show that every state in N∞(x, η) is reachable from a state x, we need to establish the relationship between numbers δ and η in the following statement:

∀x ∈ [r ] ∩ N∞(x i+1 , δ) • ∃x ∈ [r] ∩ N∞(x i , η) : x τ -→ x in A ε 0 for some τ ∈ R 0 .
This statement can be used inductively to show that a neighborhood of x k = v (and thus v itself) can be reached from x 0 = u, as in Theorem 30. When ε = 0, we show in Lemma 33 that η = 2δ fits. To have a proof of Lemma 31, we would need that η = 0 while δ > 0. To obtain this, we use the drifts on clocks. The proof is quite involved because Lemma 33 tends to require a larger value of η to guarantee some δ, while the drifts help us to decrease η.

In the next lemma, we show that every limit-cycle trajectory of strictly positive duration can be extended to a limit-cycle trajectory of duration at least 1 2 without increasing the size of π more than twice. This last condition is important as otherwise, the lemma would be trivially true.

Lemma 32 Let A be a timed automaton, let p = p 0 p 1 p 2 . . . p N be a progress cycle in the region graph of A. If there exists a limit cycle π of A that follows p such that Duration(π) > 0, then there exists a limit cycle π of A with first(π ) = first(π) and such that |π | 2|π| and Duration(π ) 1/2.

Proof. The result is immediate if Duration(π) 1/2. Assume Duration(π) < 1/2, and let k = |π| and u = first(π) = last(π). Let π 2 be the trajectory obtained by repeating π twice. We have |π 2 | = 2k and first(π 2 ) = state k (π 2 ) = last(π 2 ) = u. Since all clocks are reset along π, their value remain strictly less than 1/2 in every state of π and π 2 . By the fact that Duration(π) > 0, there must be at least one timed transition in π with a strictly positive time stamp. Consider the first such transition in π 2 , and let increase its length by 1/2 time units, yielding a new trajectory π in which each clock remains below 1. Therefore, the same transitions as in π 2 can be taken as the guards satisfied by a state of π are also satisfied by the corresponding state in π . Observe that we keep in the second half of the trajectory π the same sequence of transitions as in π, and since all clocks are reset along π, we obtain last(π ) = u = first(π ), |π | = 2|π| and Duration(π ) 1/2. Lemma 33 Let A be a timed automaton, let r and r be two regions of A s.t. ( , r) time ---→ ( , r ) in the region graph of A. For all u ∈ r, v ∈ r and τ ∈ R >0 such that ( , u) τ -→ ( , v) in A 0 0 , and for all δ 0, for all y ∈ N∞(v, δ)∩[r ], there exists x ∈ N∞(u, 2δ)∩ [r] and τ ∈ R 0 such that ( , x) τ -→ ( , y) in A 0 0 .

Proof. Let n be the number of clocks of A. Reminiscent of the normal form DBM representation of regions, let α i , β i , m i,j ∈ Z and α i , β i , m i,j ∈ Z be the tightest constants such that for all valuations u, v, we have u ∈ [r] and v ∈ [r ] if and only if for all 1 i, j n:

u i -u j m i,j α i u i β i ( [r] ) v i -v j m i,j α i v i β i ([r ])
In particular, this entails that -m j,i u i -u j β i -α j and -m j,i v i -v j β i -α j for all 1 i, j n, and since the constants are tight:

-m j,i m i,j β i -α j -m j,i m i,j β i -α j (5) Now, let u ∈ r, v ∈ r and τ ∈ R >0 such that ( , u) τ -→ ( , v
) in A 0 0 , and let δ 0 and y ∈ N∞(v, δ) ∩ [r ]. Since r is a time successor of r and v = u + τ , we have for all 1 i, j n:

m i,j = m i,j v i -v j = u i -u j (6)
We define the valuation D = y -v. Since y ∈ N∞(v, δ), we have D ∞ δ and since y ∈ [r ], we have for all 1 i, j n:

(v i + D i ) -(v j + D j ) m i,j α i v i + D i β i (7)
Now let z = u + D. As shown on Fig. 3, we might have z ∈ [r]. Thus, we have to construct a neighbour x of z that belongs to [r] and such that x τ -→ y for some τ ∈ R 0 . By Eq. ( 6) and (7), we have for all 1 i, j n:

z i -z j = (u i + D i ) -(u j + D j ) = (v i + D i ) -(v j + D j ) m i,j (8)
1 First, assume that for some i 0 , we have α i0 = β i0 : This means that the interior of r is empty, as on Fig. 3(a). Let t = -D i0 . Notice that the value of t is independent of the choice of i 0 . Indeed, if for some j = i 0 we have α j = β j , then using Eq. ( 5) we get:

α i0 -β j -m j,i0 m i0,j β i0 -α j
and -m j,i0 = m i0,j since α i0 -β j = β i0 -α j . By Eq. ( 6), we have -m j,i0 = m i0,j and thus in the region [r ], we have v i0 -v j = -m j,i0 = m i0,j = y i0 -y j and thus D i0 = D j . Now, let x = z + t so that x i0 = u i0 . We show that x ∈ [r]. Clearly, by Eq. (8) we have:

x i -x j = z i -z j m i,j
And in particular, for all 1 j n : -m i0,j x j -x i0 m j,i0 . Since x i0 = u i0 = α i0 = β i0 and by Eq. ( 5) we have:

α j β i0 -m i0,j x j m j,i0 + α i0 β j Now, we have x -u ∞ = D + t ∞ 2 D ∞ 2δ and thus x ∈ N∞(u, 2δ) ∩ [r].
2 Second, assume that for all i, we have α i < β i : This means that the interior of r is not empty, as on Fig. 3(b). We define the following sets:

I ={i | α i > z i } I ={i | z i > β i }
-If I = ∅ and I = ∅, then z ∈ [r] by Eq. (8) and we take x = z. We have

x -u ∞ = z -u ∞ = D ∞ δ. -If I = ∅, then define t = max{α i -z i | i ∈ I}
and let i 0 be an index in I such that t = α i0 -z i0 . Clearly t > 0 and since t = α i0 -u i0 -D i0 and α i0 u i0 , we have t -D i0 . We take x = z + t so that x i0 = α i0 . We show that x ∈ [r]. Clearly, by Eq. (8) we have:

x i -x j = z i -z j m i,j
In particular, for all 1 i n we have x j -x i0 m j,i0 β j -α i0 by Eq. (5). Since x i0 = α i0 , this yields x j β j . Moreover, for all i ∈ I we have x i = z i +t α i by definition of t, and for all i ∈ I we have

x i = z i + t z i α i . Finally, we have x -u ∞ = D + t ∞ 2 D ∞ 2δ. -If I = ∅, then define t = min{β i -z i | i ∈ I } and let i 0 be an index in I such that t = β i0 -z i0 .
Clearly t < 0 and since t = β i0 -u i0 -D i0 and u i0 β i0 , we have t -D i0 . We take x = z + t so that x i0 = β i0 . We show that x ∈ [r]. Clearly, by Eq. (8) we have:

x i -x j = z i -z j m i,j
In particular, for all 1 j n we have x i0 -x j m i0,j β i0 -α j by Eq. (5). Since x i0 = β i0 , this yields x j α j . Moreover, for all i ∈ I we have x i = z i + t β i by definition of t, and for all i ∈ I we have

x i = z i + t z i β i . Finally, we have x -u ∞ = D + t ∞ 2 D ∞ 2δ.
In each case, we have x ∈ N∞(u, 2δ) ∩ [r] and ( , x) τ -→ ( , y) in A 0 0 for τ = τ -t (obviously we have τ 0 because r is a time successor of r).

Lemma 34 Let A be a timed automaton. Let ( , x) and ( , y) be two states of A , and τ ∈ R 0 such that ( , x)

τ -→ ( , y) in A . For all ε ∈ R >0 , for all x ∈ N∞(x, ετ ) : ( , x ) τ -→ ( , y) in A ε 0 .
Proof. The result is immediate if τ = 0. Otherwise, it suffices to set the rate of each clock c of A to 1 -(x (c) -x(c))/τ , which lies between 1 -ε and 1 + ε.

Lemma 35 Let A be a timed automaton, let r and r be two regions of A such that r→r in the region graph of A. For all u ∈ [r], v ∈ [r ] and ε ∈ R >0 :

if there is a timed transition u τ -→ v in A , then for all η ∈ R 0 , we have:

∀y ∈ N∞(v, η + ετ 2 + 3ε ) ∩ [r ] • ∃x ∈ N∞(u, η) ∩ [r] : x τ -→ y in A ε 0 ; -if there is an action transition u σ -→ v in A , then for all η ∈ R 0 , we have ∀y ∈ N∞(v, η) ∩ [r ] • ∃x ∈ N∞(u, η) ∩ [r] : x σ -→ y in A ε 0 .
Proof. We only prove the first part of the lemma, the second part being quite obvious.

We have v = u+τ . Let δ = (η+ετ )/(2+3ε) and let y ∈ N∞(v, δ)∩[r ]. From Lemma 33, there exists x ∈ N∞(u, 2δ) ∩ [r] such that x τ -→ y in A for some τ ∈ R 0 . So we have y = x + τ . Using the triangle inequalities, we have:

τ = y -x ∞ = (v -u) -[(x -u) + (v -y)] ∞ τ -3δ (9)
Consider the set S = N∞(x, ετ ) ∩ Conv({u, x}). Since d∞(u, x) 2δ, there exists x ∈ S such that:

( d∞(u, x ) = 0 if d∞(u, x) ετ (take x = u) d∞(u, x ) 2δ -ετ if d∞(u, x) > ετ Since [r] is convex and x, u ∈ [r], we have x ∈ [r], and since x τ -→ y in A , Lemma 34 entails that x τ -→ y in A ε 0 .
To complete the proof, we have to show that x ∈ N∞(u, η), that is d∞(u, x ) η. Starting from Eq. (9), we have:

ε(τ -τ ) 3εδ = (2 + 3ε)δ -2δ = η + ετ -2δ
and thus 2δ -ετ η which entails d∞(u, x ) η.

Lemma 36 Let A be a timed automaton, let ε ∈ R >0 and Kε = 1/(2 + 3ε). Let p = p 0 p 1 • • • p N be a path in the region graph of A. Let π be a trajectory of A that follows p and let u = first(π), v = last(π) and T = Duration(π). For all y ∈ N∞(v, K N ε εT ) ∩ [p N ], there exists a trajectory π in A ε 0 that follows p and such that first(π ) = u and last(π ) = y.

Proof. Let π = (q 0 , t 0 )σ 1 (q 1 , t 1 )σ 2 . . . σ N (q N , t N ) with t 0 = 0 and t N = T . Define ε i = K i ε εt i . We show that for all 0 i < N , for all y ∈ N∞(q i+1 , ε i+1 ) ∩ [r i+1 ], there exists x ∈ N∞(q i , ε i ) ∩ [r i ] such that there exists a transition from x to y in A ε 0 :

if q i σi+1 ---→ q i+1 is a discrete transition, then we have ε i+1 ε i because t i+1 = t i and Kε 1. The claims follows then directly from Lemma 35.

otherwise, we have a timed transition q i τ -→ q i+1 and t i+1 = t i + τ . By Lemma 35 with η = ε i , we have:

∀y ∈ N∞(q i+1 , Kε(ε i + ετ )) ∩ [r i+1 ] • ∃x ∈ N∞(q i , ε i ) ∩ [r i ] : x τ -→ y in A ε 0 .
Since Kε 1, we have:

Kε(ε i + ετ ) = K i+1 ε εt i + Kεετ K i+1 ε ε(t i + τ ) = K i+1 ε εt i+1 = ε i+1
Hence, N∞(q i+1 , ε i+1 ) ⊆ N∞(q i+1 , Kε(ε i + ετ )) and we have:

∀y ∈ N∞(q i+1 , ε i+1 ) ∩ [r i+1 ]. ∃x ∈ N∞(q i , ε i ) ∩ [r i ]. x τ -→ y in A ε 0 .
Applying this result for each 0 i < N , we obtain immediately that for all y ∈ N∞(q N , ε N ) ∩ [r N ], there exists x ∈ N∞(q 0 , ε 0 ) ∩ [r 0 ] such that there exists a trajectory π in A ε 0 that follows p with first(π ) = x and last(π ) = y. Finally, we have q N = last(π) and q 0 = first(π) so that x = u since ε 0 = 0 and N∞(q 0 , 0) = {q 0 }. Lemma 37 Let A be a timed automaton and p be a progress cycle of the region graph of A. For all u, v ∈ Lp, there exists an n ∈ N such that Conv({u, v}) ⊆ Ln,p.

Proof.

Let k and l be such that u ∈ L k,p and v ∈ L l,p . Take n = kl. The result follows from Lemma 24.

We proceed with the proofs of Lemma 31 and Theorem 30.

Proof of Lemma 31. If p is not a time-elapsing progress cycle, then Lp is a singleton that contains the valuation in which all clocks are equal to zero. In this case, the result is immediate.

Assume that p contains a time-elapsing region. For u, v ∈ Lp, let n ∈ N be given by Lemma 37. We are in the conditions of Lemma 32: for all x ∈ Conv({u, v}) there exists a limit cycle π on x with Duration(π) > 0 and |π| nW where W is the number of regions of A. Therefore, there exists a limit cycle π on x with Duration(π ) 1/2 and |π | 2nW . Let N = 2nW and take δ = 1 2 εK N ε . By Lemma 36, for all y ∈ N∞(x, δ) ∩ [p 0 ] there exists a trajectory π in A ε 0 such that first(π) = x and last(π) = y. Finally, the result follows from the fact that Lp ⊆ [p 0 ].

Proof of Theorem 30. For u, v ∈ Lp, let δ as given by Lemma 31 and let k = 1 δ . Consider the points x 0 = u, x k = v, and x i = u + iδ(v -u) for i = 1, . . . , k -1. It is easy to see that d∞(x i , x i+1 ) δ • d∞(u, v) δ (because the ∞-distance between two points of a region is at most 1). Thus from Lemma 31, for all 0 i k -1 there exists a trajectory from x i to x i+1 in A ε 0 , and thus a trajectory π such that first(π) = u and last(π) = v.

Soundness of Algorithm 1.

The second part of the next theorem corresponds to [Pur98, Theorem 7.3].

Theorem 38 Let A be a timed automaton. Let p = p 0 p 1 . . . p N be a progress cycle of the region graph of A. For all x, y ∈ [p 0 ], we have:

-For all ∆ ∈ R >0 , there exists a trajectory π in A 0 ∆ such that first(π) = x and last(π) = y; -For all ε ∈ R >0 , there exists a trajectory π in A ε 0 such that first(π ) = x and last(π ) = y.

Proof. From Theorem 23, there exist u, v ∈ Lp and two trajectories π 1 and π 3 of A such that first(π 1 ) = x and last(π 1 ) = u, and first(π 3 ) = v and last(π 3 ) = y. By Theorem 28, there exists a trajectory π 2 of A 0 ∆ such that first(π 2 ) = u and last(π 2 ) = v. We construct π by concatenating the three trajectories π 1 , π 2 and π 3 . The proof is similar for the second part of the theorem, based on Theorem 30.

As a consequence, we get the following extension of [Pur98, Theorem 5.1].

Theorem 39 Let A be a timed automaton satisfying Assumption 9. Let J * be the set computed by Algorithm 1. Then J * ⊆ R 0 ∆→0 and J * ⊆ R ε→0 0 .

Proof. For all ∆ > 0, if a set of regions J * is reachable in A 0 ∆ , then:

so is the set Reach(G, J * ) of regions reachable from J * in the region graph G of A; any cycle p is a progress cycle, so that Theorem 38 applies: if p 0 is a region in p such that [p 0 ] ∩ J * = ∅, then the set

J * ∪ [p 0 ] is reachable in A 0 ∆ .
Since J * is obtained by iterating the above two operations (lines 3, 5 and 6 of the algorithm) from the set of initial states [q 0 ], this ensures that J * ⊆ Reach( A 0 ∆ ). This holds for all ∆ > 0, and hence J * ⊆ R 0 ∆→0 . The proof for drifts on clocks is similar.

Completeness of Algorithm

1: R ε→0 ∆→0 ⊆ J *
To prove the completeness of Algorithm 1, we have to show that any state that is reachable in the semantics A ε ∆ no matter how small are ε and ∆, lies in the set J * computed by Algorithm 1. First, we show that if the number of transitions in trajectories is fixed, then there is a bound on the distance between a state reachable in A ε ∆ and the set of reachable states Reach( A ) in the classical semantics (Theorem 44). This bound vanishes when ε → 0 and ∆ → 0. This shows that a state x ∈ R ε→0 ∆→0 that is reachable in a fixed number of steps from the initial states in A ε ∆ for all ε, ∆ > 0 is at distance zero from the reachable states in the classical semantics. An argument related to topologically closed sets then shows that x ∈ Reach( A ). Second, to extend the result to the whole set R ε→0 ∆→0 , we roughly use the fact that longer trajectories necessarily contain a cycle that is added to J * by the algorithm. Therefore, only a bounded part of those trajectories can take the state far from J * . By a similar argument as above, this distance to J * is shown to vanish when ε → 0 and ∆ → 0 (Theorem 45). The proofs of the theorems are based on a detailed study of the reachability properties of the perturbed semantics, for which we need parametric DBM, an extension of DBM (that we have presented in Section 4).

A parametric DBM (PDBM) in R n is a matrix M = `mi,j ´0 i,j n where m i,j ∈ Z × N is called a parametric bound. In a PDBM, each m i,j is a couple (a, b) of integers with b 0. Given a number Ω ∈ R 0 , the value of m i,j is m Ω = a + bΩ. The set represented by M is:

M Ω = {(x 1 , . . . , xn) ∈ R n | ∀ 0 i, j n : x i -x j m ij Ω ∧ x 0 = 0}.
As usual, we often write M for M 0 . More general definitions of PDBM have been introduced in [AAB00, HRSV01], with implementations. Here, we use PDBM for purely theoretical purposes, so we keep the definition as simple as possible.

For a PDBM M = `mij ´0 i,j n with m ij = (a ij , b ij ), we define the width of M by w(M) = max{b ij | 0 i, j n}. Thus a DBM is a zero-width PDBM. Any closed rectangular guard g can be represented by a PDBM Mg with w(Mg) = 2 such that for all Ω ∈ R 0 we have Mg Ω = N∞( g , Ω). In particular, g = Mg .

Example Let g ≡ x = 4 ∧ 1 y 3. Then, 0 x y 0 0 @ (0, 0) (-4, 1) (-1, 1) (4, 1) (0, 0) (3, 2) (3, 1) (-1, 2) (0, 0)

1 A Mg = x y
When the reachable states in the perturbed semantics of a timed automaton A are computed parametrically using PDBM, it would be nice that the classical semantics M gives exactly the reachable states in A and that the perturbed semantics M Ω gives the reachable states in A ε ∆ . This can be obtained when ε = 0 by taking Ω = ∆. For the general case ε > 0, the set M Ω over-approximates the reachable states, provided ε is sufficiently small. We are more precise in Lemma 42 and Lemma 43.

In that context, the width of PDBM records the accumulation of the deviations allowed by the perturbed semantics. This is useful to bound the distance between states that are reachable in the perturbed semantics and states that are reachable in the classical semantics. The following lemma gives such a bound.

Lemma 40 (See also [START_REF] Puri | Dynamical properties of timed automata[END_REF]Lemma 7

.4]) Let M be a PDBM in R n and let Ω ∈ R 0 such that Ω • (2n + 1) • w(M) < 1. Let Z = M and Z = M Ω . For all x ∈ Z , there exists x ∈ Z such that x -x ∞ n • w(M) • Ω.
Proof. First, assume that x is a vertex of Z . Then x can be obtained by solving a system of n equations of the form x i -x j = m ij Ω , x i = m i0 Ω or x i = -m 0i Ω . Therefore, each x i is the sum or difference of at most n coefficients m ij Ω . Since the bounds m ij are entries of M, for all 1 i n, if x i = l i + k i Ω for some l i , k i ∈ Z, then |k i | n • w(M) and we take x i = l i . Then x -x ∞ n • w(M) • Ω and we claim that x ∈ Z. Let l 0 = k 0 = 0. Then, for all 0 i, j n we have (for m ij = (a ij , b ij )):

x i -x j = l i -l j + (k i -k j ) • Ω a ij + b ij Ω Hence, l i -l j a ij + (b ij -k i + k j ) • Ω
Since l i , l j and a ij are integers and

|(b ij -k i + k j ) • Ω| (2n + 1) • w(M) • Ω < 1, we have x i -x j = l i -l j a ij = m ij 0 . Therefore x ∈ Z.
Second, if x is not a vertex, then it can be written as x = P i λ i v i with λ i 0 and P i λ i = 1 and each v i is a vertex of Z . From the proof above, for each v i there exists

v i ∈ Z such that v i -v i ∞ n • w(M)
• Ω. We take x = P i λ i v i . Clearly x ∈ Z, and we have:

x -x ∞ = ' ' ' X i λ i (v i -v i ) ' ' ' ∞ X i λ i v i -v i ∞ X i λ i (n • w(M) • Ω) n • w(M) • Ω
Now, we show how to extend to PDBM the operations that we have presented in Section 4 for DBM. To do so, we have to define the minimum of two parametric bounds (for intersection of PDBM). We define a lexicographic order on parametric bounds: ) Ω . Thus if we take a sufficiently small Ω, the order is preserved at the semantic level. In the sequel, this will imply that provided Ω is below some threshold, the operations on PDBM can be performed independently of the value of Ω. The sum of two parametric bounds (a, b) and (a , b ) is (a + a , b + b ).

We review the important operations on PDBM:

-Intersection: the intersection of two PDBM M 1 and M 2 is the PDBM M whose entries are the minimum (according to the lexicographic order on parametric bounds) of the corresponding entries of M 1 and M 2 . Hence w(M) max{w(M 1 ), w(M 2 )}. -Time passing and reset: those operations only substitute entries of the matrix with other entries of the matrix and they preserve the normal form. Thus the width cannot increase. -Normalization: to obtain the normal form of a PDBM M in R n , each entry m ij is replaced by the length of the shortest path from node i to node j, which has at most n edges. Therefore, the width of the normal form is bounded by n • w(M). -Emptiness test: given a PDBM M, let M be its normal form. The emptiness test checks whether one of the diagonal entries is negative (a parametric bound m = (a, b) is negative iff m < (0, 0) iff a -1).

A summary of the above observations is given in Table 1. Their correctness is established in the following lemma.

Lemma 41 For all PDBM M, M in R n , we have: -M ∩ M Ω = M Ω ∩ M Ω for all 0 Ω 1/max{w(M), w(M )};

PDBM in R n Input in
-M Ω = M Ω for all Ω ∈ R 0 , if M is in normal form; -M[R := 0] Ω = M Ω [R := 0] for all Ω ∈ R 0 and all R ⊆ {x 1 , . . . , xn}, if M is in normal form; -if M is the normal form of M, then the DBM ` m ij Ω ´0 i,j n is the normal form of the DBM ` m ij Ω ´0 i,j n , for all 0 Ω 1/max{w(M), w(M )}; -M Ω = ∅ iff M 0 = ∅, for all 0 Ω 1/(n • w(M)).
Proof. The argument is similar for the five claims. We give the details for the last one. First, we have M 0 ⊆ M Ω for all Ω. Thus it suffices to show that M 0 = ∅ implies that M Ω = ∅ for all Ω < 1/(n • w(M)). If M 0 = ∅ then there exists a parametric bound m = (a, b) in the diagonal of the normal form PDBM M such that a -1. Since b n • w(M), we have m Ω = a + bΩ < 0 and therefore M Ω is empty.

Notations. Given a TTS T = S, ι, Σ, → , let U ⊆ S and σ ∈ Σ. We define the following operators:

post σ T (U ) = {s ∈ S | ∃s ∈ U. s σ -→ s } post time T (U ) = {s ∈ S | ∃s ∈ U. ∃t ∈ R 0 . s t -→ s }
We use the PDBM to characterize the relationship between the reachable states of the classical semantics A and those of the perturbed semantics A ε ∆ . By an abuse of notation, we omit the location in the argument of post(•), that is we use Z = M instead of Z = { } × M for ∈ Loc. Finally, we assume that the edges of timed automata are identified by their label. This is clearly not restrictive for reachability analysis.

In Lemma 42, the PDBM M contains the exact information about the timed successors of M in the classical semantics, and it is an over-approximation of the timed successors in the perturbed semantics. Lemma 43 is similar for discrete successors.

Lemma 42 Let A be a timed automaton with n clocks and largest constant M . Let M be a PDBM in R n in normal form. There exists a PDBM M in normal form such that:

-∀ Ω ∈ R 0 • ∀∆ ∈ R 0 • ∀ε Ω/(2(M + 1)) : post time A ε ∆ ( M Ω ) ⊆ M Ω ; -post time A 0 0 ( M 0 ) = M 0 ; -w(M ) = w(M) + 1.
Proof. Assume that Ω, ∆ ∈ R 0 and ε Ω/(2(M + 1)). First, observe that in the classical semantics A , the length of a timed transition is bounded by M . In the perturbed semantics A ε ∆ however, a timed transition may be longer than M because clocks can progress more slowly, namely at the rate 1 -ε. Therefore, the length of a timed transition is bounded by M/(1 -ε) and thus by M + 1 since ε 1/(M + 1). Second, we obtain M by constructing the time successor of M as described above (in the exact semantics), and then by replacing each bound (a, b) of the PDBM by (a, b+1), except on the diagonal. Clearly we have w(M ) = w(M) + 1 and M 0 = M 0 and thus post time A 0 0 ( M 0 ) = M 0 . On the other hand, if we have ( , x) t -→ ( , x ) in A ε ∆ and x i -x j m ij Ω , then:

x i -x j m ij Ω + 2εt m ij Ω + 2ε(M + 1) m ij Ω + Ω = m ij Ω Therefore post time A ε ∆ ( M Ω ) ⊆ M Ω .
Lemma 43 Let A be a timed automaton with n clocks and alphabet Lab. Let M be a PDBM in R n . For all σ ∈ Lab, there exists a PDBM M in normal form such that:

-∀ Ω 1/(max{2, w(M)}) • ∀∆ Ω • ∀ε ∈ R 0 : post σ A ε ∆ ( M Ω ) ⊆ M Ω ; -post σ A 0 0 ( M 0 ) = M 0 ; -w(M ) n • max{2, w(M)}.
Proof. Assume that Ω, ε ∈ R 0 and ∆ Ω. Let ( , , g, σ, R) be the edge of A associated with σ. Let Mg be the PDBM that represents the guard g (with w(Mg) = 2). To construct M , let M∩ be the PDBM M ∩ Mg put in normal form, and let

M = M∩[R := 0] which is in normal form. According to Table 1, we have w(M ) n • max{2, w(M)} and post σ A ε ∆ ( M Ω ) ⊆ post σ A ε Ω ( M Ω ) = M Ω (by Lemma 41)
For Ω = ∆ = ε = 0, the sets collapse and post σ

A 0 0 ( M 0 ) = M 0 .
With the previous two lemmas, we have characterized how much the set of reachable states can increase by taking one transition (either timed or discrete) in the perturbed semantics A ε ∆ instead of the classical semantics A 0 0 . That increase is measured in terms of the width of a PDBM. In the next theorem, we use an argument by induction to give a bound on the increase after a given number of transitions. However, this is not sufficient to prove the completeness of Algorithm 1. We need in addition to show that every trajectory π in A ε ∆ can be approached by a trajectory π in A 0 0 where each intermediate state in π is "close" to the corresponding state in π . To obtain this result, we introduce the notion of automaton refinement that roughly divides the guards into small pieces of size6 1/γ (with γ ∈ N) so that two valuations that satisfy the same guard are necessarily "close" to each other (by choosing γ sufficiently large). This is the core of Theorem 44.

Automaton refinement. Given a timed automaton A with n clocks and a positive integer γ, the γ-refinement of A is the timed automaton Aγ constructed from A as follows:

we first substitute each constant c appearing in the rectangular constraints (guards, invariants, initial and final conditions) of A with cγ we then replace each edge (l, l , g, σ, R) in the resulting automaton with the set of all edges (l, l , g , σ, R) where g ranges over the set of all unit constraints (i.e., conjunctions of constraints of the form x i = a or a x i a + 1) that imply g. Equalities of the form x i = a are used only if g implies x i = a.

Roughly, the γ-refinement of A is a scaling of the constants by a factor γ (and thus a scaling of the time), followed by a partitioning of the guards such that the distance between two valuations that satisfy the guard is at most 1 (instead of being a multiple of γ, as is the case after the first step).

The important property of such refinements is that for all ∆, ε ∈ R 0 , the two TTS A ε ∆ and Aγ ε γ∆ are bisimilar, witnessed by the bijection µγ : Q A → Q Aγ such that µγ ( , v) = ( , γv). We extend µγ to trajectories as expected (states are mapped according to µγ and the time stamps are multiplied by γ). Finally, for all v, v ∈ Q Aγ we have µ

-1 γ (v) -µ -1 γ (v ) ∞ = v -v ∞/γ
Example. For γ = 2, an edge ( , , g, σ, R) in A with g ≡ (x = 4) ∧ (1 y 3) is replaced in Aγ with the following four edges:

( , , {x = 8 ∧ 2 y 3}, σ, R) ( , , {x = 8 ∧ 4 y 5}, σ, R) ( , , {x = 8 ∧ 3 y 4}, σ, R) ( , , {x = 8 ∧ 5 y 6}, σ, R)
The next theorem extends and clarifies Theorem 8.2 in [START_REF] Puri | Dynamical properties of timed automata[END_REF].

Theorem 44 Let A be a timed automaton with n 1 clocks and largest constant M . For all distances 0 < α < 1, for any number of steps k ∈ N, there exist two numbers D, E ∈ R >0 such that for all ∆ ∈ [0, D], for all ε ∈ [0, E] and for all stutter-free trajectories π of A ε ∆ such that |π | = k, there exists a trajectory π of A such that: -first(π) ∈ [first(π )]; -trace(π) = trace(π ); π is "close" to π in the following sense:

∀ 0 i k, if state i (π) = ( i , v i ) and state i (π ) = ( i , v i ), then i = i and v i -v i ∞ < α.
Proof. Given 0 < α < 1 and k ∈ N, let γ = 2/α and:

D = α 4γ(n + 1) k+1 E = D 2(γM + 1) Let ∆ ∈ [0, D] and ε ∈ [0, E] and let Ω = γD. Let trace(π ) = σ 1 σ 2 . . . σ k . Let ρ = µγ (π ).
Then ρ is a trajectory of Aγ ε γ∆ . Let M 0 be a PDBM in normal form such that M 0 = [first(π )] and w(M 0 ) = 0 (in fact M 0 can be seen as a DBM). Observe that γ∆ Ω and ε Ω/(2(Mγ + 1)) where Mγ = γM is the largest constant of Aγ . Therefore, by Lemma 42 and 43, there exists PDBM M 1 , M 2 , . . . , M k in normal form such that, for all 1 i k and provided that Ω 1/(max{2, w(

M i )}), (a) post σi Aγ ε γ∆ ( M i-1 Ω ) ⊆ M i Ω ; (b) post σi Aγ ( M i-1 0 ) = M i 0 ; (c) w(M i ) max{w(M i-1 ) + 1, n • max{2, w(M i-1 )}.
Let us show that w(M i ) 2(n + 1) i . We proceed by induction. The claim holds for i = 1 since w(M 0 ) = 0. Assume that it holds up to some index i -1, with i 2. Then we have

w(M i ) max ˘w(M i-1 ) + 1, n • max{2, w(M i-1 )} ¯ max{1 + 2(n + 1) i-1 , 2n • (n + 1) i-1 } (by (c)) 2(n + 1) i-1 + 2n • (n + 1) i-1 2(n + 1) i
Notice that the condition Ω 1/(max{2, w(M i )}) is satisfied. For each 0 i k, let q i = state i (π ). By (a), we have µγ (q k ) ∈ M k Ω . Since α < 1, it is easy to see that:

Ω = α 4(n + 1) k+1 < 1 (2n + 1)w(M k )
and thus by Lemma 40, there exists q k ∈ M k such that:

µγ (q k ) -q k ∞ n • w(M k ) • Ω < 2(n + 1) k+1 • Ω α.
Using (b), we can construct in a backward fashion a trajectory ρ of Aγ such that:

-last(ρ) = q k ; -trace(ρ) = trace(π ); -first(ρ) ∈ M 0 = [q 0 ].
For each 0 i k, let q i = state i (ρ). For all i such that σ i = time, we have q i ∈ g i and µγ (q i ) ∈ N∞( g i , γ∆) where g i is the guard of the edge of Aγ associated to σ i that has been taken in ρ. Since the size of g i is at most 1, we have:

µγ (q i ) -q i ∞ 1 + γ∆ 1 + Ω (10)
Observe that the effect of discrete transitions is to reset some clocks and that does not increase the ∞-distance between two states: we also have µγ (q i ) -q i ∞ 1 + γ∆ for all i such that σ i-1 = time. Since π is stutter-free and trace(ρ) = trace(π ), Eq. (10) holds for all 0 i k. Now, let π = µ -1 γ (ρ) which is a trajectory of A since ρ is a trajectory of Aγ . Thus, we have for all 0 i k:

q i -µ -1 γ (q i ) ∞ 1 + Ω γ < 2 γ α
which entails that π is "close" to π as required.

The following theorem is the key of the proof of completeness. It shows that for all distances α > 0, we can choose sufficiently small values of ∆ and ε such that from J * the points that are reachable in A ε ∆ are at distance at most α from J * . By contrast with Theorem 44, we do not make the hypothesis that the length of the trajectories is bounded. This result is similar to Theorem 8.3 in [START_REF] Puri | Dynamical properties of timed automata[END_REF], but the constants are different because only drifting clocks were considered by Puri and the bound of Lemma 16 was wrong.

Theorem 45 Let A be a timed automaton with n 1 clocks and largest constant M that satisfies Assumption 9. For all distances α ∈ R >0 , there exist two numbers D, E ∈ R >0 such that for all ∆ ∈ [0, D], for all ε ∈ [0, E] and for all trajectories π of A ε ∆ such that first(π ) ∈ J * , we have d∞(last(π ), J * ) < α.

Proof. Without loss of generality, we may assume that α < 1 2n . Let W be the number of regions of A, let γ = 2/α and:

D = α 4γ(n + 1) 2W +1 E = D 2(γM + 1)
Let ∆ ∈ [0, D] and ε ∈ [0, E] and let π be a stutter-free trajectory of A ε ∆ such that first(π ) ∈ J * . Let m = |π | and for each 0 i m, let q i = state i (π ).

-If m 2W . By Theorem 44, there exists a trajectory π of A such that first(π) ∈

[first(π )] and for all 0 i m, q i -q i ∞ < α where q i = state i (π). Since q 0 ∈ [q 0 ] ⊆ J * , the state qm is reachable from J * and thus qm ∈ J * . Since qm -q m ∞ < α this yields d∞(last(π ), J * ) < α.

-If m > 2W . By induction, assume that d∞(q i , J * ) < α for all 0 i m -1. Consider the sub-trajectory of π from state q m-2W to q m , and according to Theorem 44, let π be a trajectory such that for all m -2W i m, it holds q i -q i ∞ < α, where q i = state i-(m-2W ) (π). Then for all i with m -2W i m -1, we have : d∞(q i , J * ) q i -q i ∞ + d∞(q i , J * ) 2α < 1 n , and by Lemma 16, this implies [q i ] ∩ J * = ∅ for all m -2W i m -1 (since J * is a zone-set). On the other hand, the trajectory π has the same trace as the sub-trajectory of π from q m-2W to q m and thus it is stutter-free and |π| = 2W . Therefore, π has 2W + 1 states and thus there exists two states q k and q k in π with k < k such that [q k ] = [q k ] and a discrete transition occurred along π between q k and q k in π, and thus there exists a path from [q k ] to itself in the region graph of A. Since [q k ] ∩ J * = ∅, we have [q k ] ⊆ J * by line 5 of Algorithm 1 and [q i ] ⊆ J * for all i k by line 6 of the algorithm. So we have qm ∈ J * and since qm -q m ∞ < α, this yields d∞(last(π ), J * ) < α.

Theorem 46 Let J * be the set computed by Algorithm 1. Then R ε→0 ∆→0 ⊆ J * .

Proof. For all y ∈ R ε→0 ∆→0 , for all ∆ > 0 and ε > 0 there exists a trajectory π of A ε ∆ such that first(π) ∈ J * (because J * contains the initial states) and last(π) = y. Therefore, by Theorem 45 for all α ∈ R >0 we have d∞(y, J * ) < α. This implies that d∞(y, J * ) = 0 and since J * is a closed set (a finite union of closed regions) we have y ∈ J * .

With Theorems 39 and 46 we have proven the following inclusions:

Complexity

The complexity issues have been studied in [START_REF] Puri | Dynamical properties of timed automata[END_REF]. We mention the main theorem and we give a detailed proof of the hardness result.

Theorem 48 ( [START_REF] Puri | Dynamical properties of timed automata[END_REF]) Given a timed automaton A = Loc, Var, q 0 , Lab, Edg satisfying Assumption 9 and a location ∈ Loc, deciding whether there exists a valuation v such that ( , v) ∈ R 0 ∆→0 (or equivalently ( , v) ∈ R ε→0 0 , or ( , v) ∈ R ε→0 ∆→0 ) is PSPACEcomplete.

The proof uses the following definition of Linear Bounded Turing Machines (LBTM). A LBTM is a non-deterministic Turing machine that can only use a number of tape cells equal to the length of its input.

Definition 49 (Linear Bounded Turing Machine) A LBTM M = (Q, Σ, q 0 , q f , E) consists of:

a finite set of control states Q, a finite alphabet Σ, an initial state q 0 ∈ Q, a final state q f ∈ Q, and a set of transitions E ⊆ Q × Σ × Σ × {left, right} × Q.

A configuration of M is a triple (q, w, i) ∈ Q × Σ * × N where q is a control location, w ∈ Σ * is the content of the tape, and i is the position of the tape head. A configuration (q , w , i ) is a successor of a configuration (q, w, i) iff there exists a transition (q, σ, σ , d, q ) ∈ E such that:

(1) w i = σ;

(2) w i = σ and w j = w j for all j = i;

(3) i = i -1 if d = left and i = i + 1 if d = right with 1 i |w|.

We assume that the condition 1 i |w| is realized using input delimiters. An execution of M on the input x ∈ Σ * is a sequence s 0 s 1 . . . sn of configurations starting with s 0 = (q 0 , x, 1) and such that s i+1 is a successor of s i for every 0 i < n. We say that M accepts x iff M has an execution on x finishing in sn = (q f , w, i) for some w ∈ Σ * and i ∈ N. The acceptance problem for LBTM asks, given a LBTM M and an input word x ∈ Σ * whether M accepts x.

Proof of Theorem 48. First, we prove PSPACE-membership. It is not possible to use Algorithm 1 because we should construct the region graph G, which may have a number of states exponential in the number of clocks of the timed automaton A.

However, we can check the reachability of a region r by guessing a path in the region graph from the initial regions to r in polynomial space. This is a fairly standard trick used for showing PSPACE-membership of the reachability problem for classical timed automata with an on-the-fly algorithm [START_REF] Alur | A theory of timed automata[END_REF]. The difficult point is that the successor of a given region r can be a neighbour region r such that [r] ∩ [r ] = ∅ provided r lies in a progress cycle S of G. As we have shown, the entire region r can be reached from r in A ∆ no matter how small ∆ is, by repeating the cycle S. Hence we can add S in one step in the set of reachable states. Such an acceleration has been proven correct (Theorem 39) and complete (Theorem 46). So, when guessing the successor of a region r, we must take into account the neighbour regions of r and decide whether they are in a progress cycle or not. This can be checked in PSPACE using the same procedure as for classical timed automata [START_REF] Alur | A theory of timed automata[END_REF]. A polynomially bounded part of the memory is reserved for executions of this procedure. Since the content of this part of the memory is not necessary for further computations, it can be reused by subsequent calls and PSPACE-membership follows.

We establish PSPACE-hardness using a reduction of the acceptance problem for LBTM The reduction is similar to [START_REF] Courcoubetis | Minimum and maximum delay problems in real-time systems[END_REF], where a configuration (q, w, i) of a LBTM is encoded by a location (q, i) (that records the control state q and the tape position i) and by the clocks y 1 , . . . , y |w| , one for each tape cell. We assume without loss of generality that Σ = {a, b}. A clock y i has the value y i = na if w i = a and y i = n b > na if w i = b. This encoding is not preserved by time passing. Thus we need to periodically refresh the values of the clocks. This is done in two phases: (I) resetting the clocks coding a 'b' (by checking y i = n b ), then letting n b -na time unit elapse, and (II) resetting the clock coding an 'a' (by checking y i = n b again) and finally letting na time unit elapse. During phase (I), the clock that encodes the tape cell pointed by the head, is updated according to the transitions of the LBTM.

We show how to adapt this reduction to the perturbed semantics of timed automata. Due to guards enlargements, equality cannot be tested precisely and the clocks can not store precise values na and n b . However, if ∆ is sufficiently small and na and n b are not too close, we can still distinguish clocks coding an 'a' and clocks coding a 'b'. The details of this proof follow.

Let M = (Q, Σ, q 0 , q f , δ) be a LBTM and x ∈ Σ * be an input word. Let n = |x|, na = 3 and n b = 6. We construct a timed automaton A(M, x) with n + 1 clocks and a location f such that M accepts x iff ( f , v) ∈ R 0 ∆→0 for some valuation v. Let A(M, x) = Loc, Var, q A 0 , Lab, Edg with: -Loc = {s 0 , s 1 , f } ∪ {(q, i, j, ϕ, d) | q ∈ Q ∧ 1 i n ∧ 1 j n + 1 ∧ ϕ ∈ {I, II} ∧ d ∈ {left, right}}; a location (q, i, j, ϕ, d) encodes the control state q, the tape position i, the number j of the next clock to be treated, the phase ϕ of the simulation, and the direction d of the next head movement; -Var = {y i | 1 i n} ∪ {z}; q A 0 = (s 0 , v 0 ) with v 0 (t) = 0 for all t ∈ Var; -Lab = {τ }; -The set Edg contains the following edges (we write g,R --→ when ( , , g, τ, R) ∈ Edg):

-Initialization:

• s 0 z=3,{yi|xi=a}∪{z} --------------→ s 1

• s 1 z=3,{z} ------→ (q 0 , 1, 1, I, left)

  Reach( Aα ) for timed automaton Aα. Aα 0 ∆ ) for timed automaton Aα.

Fig. 1

 1 Fig. 1 Differences between standard and perturbed semantics.

Lemma 18

 18 If d(A, B) > 0, then A ∩ B = ∅. Lemma 19 If A ⊆ B, then d(A, C) d(B, C) for all C.

0 begin1

 0 Construct the region graphG = (R A , → G ) of A ; Compute the set C(G) of simple cycles of G ; 2 J * ← Reach(G, [q 0 ]) ; 3 while for some p = p 0 p 1 . . . p k ∈ C(G), [p 0 ] ⊆ J * and J * ∩ [p 0 ] = ∅ do 4 J * ← J * ∪ [p 0 ] ; 5 J * ← Reach(G, J * ) ;

  Proof. Let v be a vertex of [p 0 ]. Then {v} is a subregion of [p -0], and the set of its successors in [p k ] is a closed subregion of [p k ]. According to Lemma 14, a subregion of [p k ] necessarily contains a vertex.

∆ 2 .

 2 Moreover since v ∈ [p 0 ], the closed version of the above inequalities defining p 0 are satisfied by v. Let v(x) = v(x) -ax, we have:

  The interior of [r] is not empty.

Fig. 3

 3 Fig. 3 Construction of a predecessor of y in the closed region [r].

  (a, b) (a , b ) if and only of either a < a , or a = a and b b . This (syntactical) definition is justified by the following observation: for all Ω such that bΩ 1, if (a, b) (a , b ) then (a, b) Ω (a , b

⊆

  All those sets are thus equal:Theorem 47 Under Assumption 9, we have R 0 ∆→0 = R ε→0 0 = R ε→0 ∆→0 , and those sets are computed by Algorithm 1.

Table 1

 1 Operations on PDBM (NF = normal form).

		NF	Output in NF	Width of the result
	Intersection M 1 ∩ M 2	No	No	max{w(M 1 ), w(M 2 )}
	Time passing M	Yes	Yes	w(M)
	Reset M[R := 0]	Yes	Yes	w(M)
	Normalization of M Emptiness test of M	No	Yes	n • w(M)

For ε > 0, a general constraint of the form ∆ > f (∆ L , ∆ P , ε) is also established in[START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF], where f is a simple function such that f (∆ L , ∆ P , ε) → 0 when ∆ L , ∆ P , ε → 0.

This holds under some assumption that is discussed in Section 2.

In Section 6.3, we study in more details a parametric extension of DBMs, which we use for proving completeness of our algorithm.

Assuming Algorithm 1 is correct, the set J * = R ε→0 ∆→0 it computes is a union of closed regions.

It is not restrictive to assume that π starts and ends with a timed transition as timed transitions of length zero are allowed.

The size of a set is the maximal distance (for d∞) between two points in the set.

This research was supported by the Belgian FNRS grant 2.4530.02 of the FRFC project "Centre Fédéré en Vérification", by the project "MoVES", an Interuniversity Attraction Poles Programme of the Belgian Federal Government, and by the French project DOTS (ANR-06-SETI-003).

-Refresh: for every (q, i, j, ϕ, d) ∈ Loc with j = i and j n,

• (q, i, j, ϕ, d) z 0 ∧ yj 4,∅ -----------→ (q, i, j + 1, ϕ, d)

• (q, i, j, ϕ, d) z 0 ∧ yj 5,{yj } -----------→ (q, i, j + 1, ϕ, d)

, right}, and for every transition (q, σ, σ , d , q ) ∈ E,

• If (σ, σ ) = (a, a) then (q, i, i, I, d)

------→ (q, i + 1, 1, I, right) -Termination: for every 1 i n, d ∈ {left, right},

After the initialization step, the automaton is in the location (q 0 , 1, 1, I, left) and we have the following relations between the tape content w and the clocks y 1 , . . . , yn when z = 0:

After executing one transition (q, σ, σ , d , q ) of M , let w be the new tape content (w differs from w by at most one symbol). If we simulate that transition by the refresh steps, the execution step, and the phase changes, it is easy to check that in location (q, i, 1, I, d), when z = 0 we have:

Note that two clocks coding the same symbol are not necessarily equal (however, their difference is bounded by ∆). The reader can check that after having executed a second transition of M , there is no accumulation of the imprecisions and the conditions (11) still hold. Hence, provided ∆ is sufficiently small (in fact ∆ < 1/2), the automaton A(M, x) will correctly distinguish clocks coding 'a' from clocks coding 'b' for any number of transitions, and thus simulate faithfully the execution of M on x.

It is now easy to see that the location f is reachable in R 0 ∆→0 iff f is reachable in A 0 0 iff M accepts x. This concludes the proof since our construction is polynomial in the size of M and x.