Patricia Bouyer
email: patricia.bouyer@lsv.fr.

Uli Fahrenberg
email: uli.fahrenberg@irisa.fr.

Kim G Larsen

Nicolas Markey
email: nicolas.markey@lsv.fr.

Joël Ouaknine
email: joel.ouaknine@cs.ox.ac.uk.

James Worrell
email: james.worrell@cs.ox.ac.uk.

Model Checking Real-Time Systems

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

Introduction

Timed automata were introduced by Rajeev Alur and David Dill in the early 1990s [START_REF] Alur | A theory of timed automata[END_REF] as finite-state automata equipped with real-valued variables for measuring time between transitions in the automaton. These variables all evolve at the same rate; they can be reset along some transitions, and used as guards along other transitions or invariants to be preserved while letting time elapse in locations of the automaton. Timed automata have proven very convenient for modeling and reasoning about real-time systems: they combine a powerful formalism with advanced expressiveness and efficient algorithmic and tool support, and have become a model of choice in the framework of verification of embedded systems. The timedautomata formalism is now routinely applied to the analysis of real-time control programs [START_REF] Dierks | PLC-automata: a new class of implementable real-time automata[END_REF]127] and timing analysis of software and asynchronous circuits [START_REF] Bozga | Verification of asynchronous circuits using timed automata[END_REF]146,150]. Similarly, numerous real-time communication protocols have been analysed using timed automata technology, often with inconsistencies being revealed [START_REF] Havelund | Formal modelling and analysis of an audio/video protocol: An industrial case study using Uppaal[END_REF]144]. During the last few years, timedautomata-based schedulability and response-time analysis of multitasking applications running under real-time operating systems have received substantial research effort [START_REF] Brekling | Models and formal verification of multiprocessor system-on-chips[END_REF][START_REF] David | Schedulability of Herschel-Planck revisited using statistical model checking[END_REF][START_REF] David | Model-based design for embedded systems[END_REF]109,156]. Also, for optimal planning and scheduling, (priced) timed automata technology has been shown to provide competitive and complementary performances with respect to classical approaches [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF][START_REF] Abdeddaïm | Job-shop scheduling using timed automata[END_REF][START_REF] Behrmann | Efficient guiding towards cost-optimality in Uppaal[END_REF][START_REF] Dierks | Finding optimal plans for domains with continuous effects with UPPAAL Cora[END_REF][START_REF] Hendriks | Model checker aided design of a controller for a wafer scanner[END_REF]108,119]. Finally, controller synthesis from timed games has been applied to a number of industrial case studies [START_REF] Altisen | A framework for scheduler synthesis[END_REF][START_REF] Cassez | Automatic synthesis of robust and optimal controllers -an industrial case study[END_REF]110].

The handiness of this formalism is exemplified in Fig. 1, modeling a (simplified) computer mouse: this automaton receives press events, corresponding to an action of the user on the button of the mouse. When two such events are close enough (less than 300 milliseconds apart), this is translated into a double click event.

Because clock variables are real-valued, timed automata are in fact infinitestate models, where a configuration is given by a location of the automaton and a valuation of the clocks. Timed automata have two kinds of transitions: action transitions correspond to firing a transition of the automaton, and delay transitions correspond to letting time elapse in the current location of the automaton. Section 2 provides the definitions of this framework. The main technical ingredient for dealing with this infinity of states is the region abstraction, as we explain in Sect. 3. Roughly, two clock valuations are called region equivalent whenever they satisfy the exact same set of constraints of the form x -y c, where the difference of two clocks x and y is compared to some integer c (no greater than some constant M ). This abstraction can be used to develop various algorithms, in particular for deciding bisimilarity (Sect. 4) or model checking some quantitative extensions of the classical temporal logics CTL and LTL (Sect. 6). We also show that some problems are undecidable, most notably language containment (Sect. 5) and model checking the full quantitative extension of LTL. On the practical side, regions are in some sense too fine-grained, and another abstraction, called zones, is preferred for implementation purposes. Roughly, zones provide a way of grouping many regions together, which is often relevant in practical situations. We explain in Sect. 7 how properties of timed automata can be verified in practice.

Finally, we conclude this chapter with two powerful extensions of timed automata: first, weighted timed automata allow for modeling quantitative constraints beyond time; since resource (e.g., energy) consumption is usually tightly bound to time elapsing, timed automata provide a convenient framework for modeling such quantitative aspects of systems. Unlike hybrid systems (see Chap. 28hybrid), weighted timed automata still enjoy some nice decidability properties (in restricted settings though), as we explain in Sect. 8. Then in Sect. 9 we present timed games, which are very powerful and convenient for dealing with the controller synthesis problem (see Chap. 25gamesynth) in a timed framework. Timed games also provide an interesting way of modeling uncertainty in real-time systems, assuming worst-case resolution of the uncertainty while still trying to benefit from non-worst-case situations.

Timed Automata

In this chapter, we consider as time domain the set R ≥0 of non-negative reals. While discrete time might look reasonable for representing digital systems, it assumes synchronous interactions between the systems. We refer to [START_REF] Alur | Real-time logics: Complexity and expressiveness[END_REF][START_REF] Asarin | On discretization of delays in timed automata and digital circuits[END_REF][START_REF] Janusz | Advances in asynchronous circuit theory part II: Bounded inertial delay models, MOS circuits, design techniques[END_REF]102] for more discussions on this point.

Let Σ be a finite set of actions. A time sequence is a finite or infinite non-decreasing sequence of non-negative reals. A timed word is a finite or infinite sequence of pairs (a 1 , t 1 ) . . . (a p , t p ) . . . such that a i ∈ Σ for every i, and (t i ) i≥1 is a time sequence. An infinite timed word is converging if its time sequence is bounded above (or, equivalently, converges).

We consider a finite set C of variables, called clocks. A (clock) valuation over C is a mapping v : C → R ≥0 which assigns to each clock a real value.

The set of all clock valuations over C is denoted R C ≥0 , and 0 C denotes the valuation assigning 0 to every clock x ∈ C.

Let v ∈ R C
≥0 be a valuation and t ∈ R ≥0 ; the valuation v + t is defined by (v + t)(x) = v(x) + t for every x ∈ C. For a subset r of C, we denote by v[r] the valuation obtained from v by resetting clocks in r; formally, for every x ∈ r, v[r](x) = 0 and for every x ∈ C \ r, v[r](x) = v(x).

The set Φ(C) of clock constraints over C is defined by the grammar

Φ(C) ϕ ::= x k | ϕ 1 ∧ ϕ 2 (x ∈ C, k ∈ Z and ∈ {<, ≤, =, ≥, >}).
We will sometimes make use of diagonal clock constraints, which additionally allow constraints of the form x -y k. We write Φ d (C) for the extension of Φ(C) with diagonal constraints. If v ∈ R C ≥0 is a clock valuation, we write v |= ϕ when v satisfies the clock constraint ϕ, and we say that v satisfies x k whenever v(x) k (similarly, v satisfies x -y k when v(x) -v(y) k).

If ϕ is a clock constraint, we write ϕ C for the set of clock valuations

{v ∈ R C ≥0 | v |= ϕ}.
Definition 1 ( [START_REF] Alur | A theory of timed automata[END_REF]). A timed automaton is a tuple (L, 0 , C, Σ, I, E) consisting of a finite set L of locations with initial location 0 ∈ L, a finite set C of clocks, an invariant1 mapping I : L → Φ(C), a finite alphabet Σ and a set E ⊆ L × Φ(C) × Σ × 2 C × L of edges. We shall write ϕ,a,r ---→ for an edge ( , ϕ, a, r, ) ∈ E; formula ϕ is the guard of the transition (and has to be satisfied when the transition is taken), and r is the set of clocks that are set to zero after taking that transition.

Later for defining languages accepted by timed automata we may add final or repeated (Büchi) locations, and for defining logical satisfaction relations we may add atomic proposition labeling to timed automata. However for readability reasons we omit them here.

Resource R j available j in use j (x j ≤ 1) acquire?

x j := 0

x j > 0 release! Process P i idle i (y i ≤ 2) attempting i (y i ≤ 2)
working i start! y i > 1, y i := 0 acquire! abort! y i = 2, y i := 0 release? y i := 0 Fig. 2 Model of a process that acquires and releases two resources. Here and in the rest of this chapter, transitions are decorated with their associated guards (e.g., x j > 0), letters of the alphabet (e.g., release!), and resets (written e.g., as x j := 0); invariants (if any) are written in brackets below their corresponding locations Example 1. Figure 2 shows timed automata models for processes and resources. Processes can use resources, but mutual exclusion is expected. The model for process P i is given in the upper part of the figure, whereas the model for resource R j is given in the lower part of the figure. Starting in the idle location, the process should start within one to two time units requesting a resource. After two time units it must abort its request, unless before two time units it acquires the resource and goes to the working location. The resource is released when the process is done working with it.

Our model for a resource has two locations, and when the resource is available, it can be acquired and should be released within one time unit.

The operational semantics of a timed automaton A = (L, 0 , C, Σ, I, E) is the (infinite-state) timed transition system A = (S, s 0 , R ≥0 × Σ, T ) given as follows:

S = ( , v) ∈ L × R C ≥0 v |= I( ) s 0 = ( 0 , 0 C ) T = ( , v) d,a --→ ( , v ) ∀d ∈ [0, d] : v + d |= I( ),
and

∃ ϕ,a,r ---→ ∈ E : v + d |= ϕ, and v = (v + d)[r]
In words, one can jump from one state ( , v) to another one ( , v ) by selecting a delay to be elapsed in (provided that the invariant of location is fulfilled in the meantime) and an edge of the automaton, which is taken after the delay, provided that its guard is satisfied at that time. In this semantics, a transition combines both a delay and (followed by) the application of an edge of the automaton. A slightly different semantics is sometimes used, which distinguishes pure-delay transitions (denoted

d -→, for d ∈ R ≥0 ) and pure-action transitions (denoted a -→ with a ∈ Σ). A (finite or infinite) run of a timed automaton A is a (finite or infinite) path ρ = ( 0 , v 0 ) d1,a1 ---→ ( 1 , v 1 ) d2,a2 ---→ • • • in the transition system A , which starts with v 0 = 0 C . Given a run ρ = ( 0 , v 0 ) d1,a1 ---→ ( 1 , v 1 ) d2,a2
---→ ( 2 , v 2 ) . . . , we say that it reads the timed word w = (a 1 , t 1 )(a 2 , t 2 ) . . . where for every i, t i = j≤i d j . A run is time-divergent if its time sequence (t i ) i diverges. A timed automaton is non-Zeno if any finite run can be extended into a time-divergent run.

Example 2. The process R 1 given in Fig. 2 has a single clock x 1 , and has as set of states S = {available 1 } × R ≥0 ∪ {in use 1 } × [0, 1] where we identify valuations (for the single clock x 1 ) with the value of x 1 . We give below a possible run for the resource R 1 :

(available 1 , 0)

5.4,acquire? --------→ (in use 1 , 0) 0.8,release! -------→ (available 1 , 0.8) 1.4,acquire? --------→ (in use 1 , 0) → . . .
In location in use, the invariant is satisfied in this run because the value of x 1 never exceeds 0.8 (hence satisfies the constraint x 1 ≤ 1).

We now define the parallel composition of timed automata, which allows us to define systems in a compositional way [START_REF] Arnold | The metric space of infinite trees. algebraic and topological properties[END_REF]107]. Let (A i ) 1≤i≤n be n timed automata, where

A i = (L i , i 0 , C i , Σ i , I i , E i ).
Assume that all Σ i 's are disjoint, and all C i 's are disjoint. If Σ is a new alphabet, given a (partial) synchronization function f :

n i=1 (Σ i ∪ {-}) → Σ, the synchronized product (or parallel composition) (A 1 A 2 • • • A n ) f is the timed automaton A = (L, 0 , C, Σ, I, E) where L = L 1 ו • •×L n , 0 = ( 1 0 , . . . , n 0 ), C = C 1 ∪• • •∪C n , I(( 1 , . . . , n )) = n i=1 I i ( i ) for every ( 1 , . . . , n ) ∈ L 1 × • • • × L n , and the set E is composed of the transitions ( 1 , . . . , n ) ϕ,a,r ---→ ( 1 , . . . , n ) whenever 1. there exists (α 1 , . . . , α n ) ∈ n i=1 (Σ i ∪ {-}) such that f (α 1 , . . . , α n ) = a; 2. if α i = -, then i = i ; 3. if α i = -, then there is a transition i ϕi,αi,ri -----→ i in E i 4. ϕ = {ϕ i | α i = -} and r = {r i | α i = -} Example 3.
We build on the system given in Fig. 2. The process and the resources are not expected to run independently, but they are part of a global system where the process should synchronize with the resources. Hence for this system we have a natural synchronization function f defined by Table 1.

P 1 P 2 R 1 start! - - → start 1 - start! - → start 2 abort! - - → abort 1 - abort! - → abort 2 acquire! - acquire? → acquire 1 - acquire! acquire? → acquire 2 release? - release! → release 1 - release? release! → release 2
Table 1 The synchronization function f

The global system (P 1 P 2 R 1 ) f (more precisely the part which is reachable from the initial state) is depicted in Fig. 3. This automaton is rather complex, and the component-based definition as (P 1 P 2 R 1 ) f is much easier to understand. Furthermore this allows addition of other processes and other resources to the system without any effort.

Checking Reachability

In this section we are interested in the most basic problem regarding timed automata, namely reachability. This problem asks, given a timed automaton A, whether a distinguished set of locations F of A is reachable or not.

Fig. 3 The global system (P 1 P 2 R 1 ) f , where "i j " (resp. "a j ", "w j ") stands for location "idle j " (resp. "attempting j ", "working j ") in P j , and "a 1 " (resp. "u 1 ") stands for location "available 1 " (resp. "in use 1 ") in R 1

Region Equivalence

For the rest of this section we fix a timed automaton A = (L, 0 , C, Σ, I, E) and a set of target locations F . For every clock x ∈ C we let M x be the maximal constant clock x is compared to in A.

Two valuations v, v : C → R ≥0 are said to be region equivalent w.r.t.

maximal constants M = (M x ) x∈C , denoted v ∼ =M v , if 2 • for all x ∈ C, v(x) = v (x) or v(x), v (x) > M x , and • for all x ∈ C with v(x) ≤ M x , v(x) = 0 iff v (x) = 0, and • for all x, y ∈ C with v(x) ≤ M x and v(y) ≤ M y , v(x) ≤ v(y) iff v (x) ≤ v (y) .
The equivalence classes of valuations with respect to ∼ =M are called regions (with maximal constants M ). The number of regions is finite and is bounded above by n! • 2 n • x∈C (2M x + 2). Region equivalence of valuations is extended to states of A by declaring that ( , v) ∼ =M ( , v ) whenever = and v ∼ =M v . We write [ , v]∼ =M for the equivalence class of ( , v).

Region equivalence enjoys nice properties, the most important of which is that it is a time-abstracted bisimulation in the following sense:

Definition 2. A relation R on the states of A is a time-abstracted bisimulation if ( 1 , v 1 )R( 2 , v 2 ) and ( 1 , v 1 ) d1,a ---→ ( 1 , v 1 ) for some d 1 ∈ R ≥0 and a ∈ Σ imply ( 2 , v 2 ) d2,a ---→ ( 2 , v 2 ) for some d 2 ∈ R ≥0 , with ( 1 , v 1 )R( 2 , v 2 ) and vice versa.
In other words, from two equivalent states, the automaton can take the same transitions, except that the values of the delays might have to be changed. This fundamental property has important consequences, like the construction of an interesting finite abstraction for A. Definition 3. The region automaton R∼ =M (A) = (S, s 0 , Σ, T ) associated with A has as set of states the quotient

S = L × R C ≥0 / ∼ =M , as initial state s 0 = [ 0 , 0 C ]∼ =M , and as transitions all the [ , v]∼ =M a -→ [ , v ]∼ =M for which ( , v) d,a --→ ( , v ) for some d ∈ R ≥0 . The target set of R∼ =M (A) is defined as S F = {[ , v]∼ =M | ∈ F }. y 1 0 x 1 1 1 2
Fig. 4 Clock regions for the system (P 1 R 1 ) f 1

The region automaton R∼ =M (A) is a finite automaton whose size is exponential compared with the size of A. It can be used to check, e.g., reachability properties (or equivalently language emptiness):

Proposition 1. The set of locations F is reachable in A from 0 iff S F is reachable in R∼ =M (A) from s 0 .
The region automaton has exponentially larger size, but checking a reachability property can be done on the fly, hence this can be done in polynomial space. One of the most fundamental theorems in the model checking of timed automata can be stated as follows.

Theorem 1 ( [START_REF] Alur | A theory of timed automata[END_REF]). The reachability problem in timed automata is PSPACEcomplete.

Example 4. Restricting our running example to process P 1 and resource R 1 (we assume f 1 is the synchronization function f restricted to those two processes), the global system has two clocks, x 1 and y 1 . The set of regions is then depicted in Fig. 4. There are 28 regions. The (reachable part of the) corresponding region automaton is depicted in Fig. 5. In this drawing we omit indices over names of locations since they should all be 1; also, the thick "release" transition at the top corresponds to a set of transitions from all the states on the right to all the states on the left.

Some Extensions of Timed Automata

Timed automata are the most basic model for representing systems with (quantitative) real-time constraints. It is natural to extend the model with features that help in modeling real systems. However decidability of the reachability problem remains the fundamental property one wants to preserve. In this subsection we mention several variants and extensions of timed automata that have been proposed in the literature.

Timed automata as defined in this chapter are the so-called diagonalfree timed automata since only constraints of the form x k are used. Timed automata with diagonal constraints (of the form x -y k) were also originally defined in the seminal paper [START_REF] Alur | A theory of timed automata[END_REF]. They can be analyzed using a slight refinement of the region automaton, but with no extra complexity. Furthermore, diagonal constraints can be removed from the model, at the expense of a (possibly exponential) blowup in the number of locations of the model [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF].

Another useful extension of timed automata is obtained by allowing edges to set clocks to arbitrary positive integers (x := k) instead of only 0, or even to synchronize clock values (x := y). In [START_REF] Bouyer | Updatable timed automata[END_REF] it is shown that any such updatable timed automaton can be converted to a usual one, hence this class is no more expressive than timed automata. If one also considers other updates however, like x := x + 1 or x :> k (which non-deterministically sets x to some value larger than k), the situation is much more complex [START_REF] Bouyer | Updatable timed automata[END_REF] and decidability of reachability is no longer preserved.

One can also extend the timed-automata formalism by allowing richer clock constraints, such as, e.g., x + y ≤ 5 or 2x -3y > 1. Most such attempted extensions however lead to undecidability of the reachability problem, see for instance [START_REF] Bérard | Timed automata and additive clock constraints[END_REF].

One can extend timed automata with urgency requirements [START_REF] Bornot | Modeling urgency in timed systems[END_REF]. For instance, some locations might be labelled as urgent, which indicates that no time can be spent in this location, it has to be left immediately when entered: an urgent location can easily be converted into a usual one by introducing an extra clock x which is reset in any edge to and has invariant x = 0 in , hence location-urgency does not add expressiveness to the class of timed automata. Some synchronization could be also labelled as urgent: in that case, the corresponding action should be done as soon as it is enabled. In our modeling of Example 1 the synchronization "acquire!/acquire?" could be made urgent since it is natural that a process acquires the resource as soon as it is available.

Another extension of timed automata we should mention is the stopwatch automata of [100]. Here timed automata are extended by allowing clocks to be stopped during a delay. Even though reachability is also undecidable for this extension and it has been shown to have the same expressive power as hybrid automata [START_REF] Cassez | The impressive power of stopwatches[END_REF], stopwatch automata have found some applications, e.g., in scheduling [START_REF] Abdeddaïm | Preemptive job-shop scheduling using stopwatch automata[END_REF]141] and permit efficient over-approximate analysis [START_REF] Cassez | The impressive power of stopwatches[END_REF]. Further extensions of the dynamics of timed automata lead to rectangular automata [100] and eventually to general hybrid automata [START_REF] Alur | Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems[END_REF][START_REF] Henzinger | The theory of hybrid automata[END_REF].

Finally, another interesting direction in which timed automata have been extended consists in adding parameters. Parameters can be used in lieu of numerical constants in the timed automaton, with the aim of deciding the existence of (and computing) values for the parameters for which a given property holds true. The use of parameters simplifies the modeling phase, but unfortunately the existence of valid parameters turns out to be undecidable in general [START_REF] Alur | Parametric real-time reasoning[END_REF]. Several decidable classes have been identified, including oneclock parametric timed automata [START_REF] Alur | Parametric real-time reasoning[END_REF]129] and L/U automata, where each parameter can be used either in lower-bound constraints or in upper-bound constraints [106].

(Bi)simulation Checking

(Bi)simulations for Timed Automata

As detailed in Sect. 2, the operational semantics of timed automata is given in terms of timed transition systems, which in fact can be viewed as standard labelled transition systems, with labels (d, a) comprising a delay and a letter. Hence any behavioral equivalence and preorder defined on labelled transition systems may be interpreted over timed automata. In particular the classical notions of simulation and bisimulation [130,138] give rise to the following notion of timed (bi)simulation:

Definition 4. Let A = (L, 0 , C, Σ, I, E) be a timed automaton. A relation R ⊆ L × R C ≥0 × L × R C ≥0 is a timed simulation provided that for all ( 1 , v 1 ) R ( 2 , v 2 ), for all ( 1 , v 1 ) d,a --→ ( 1 , v 1 ) with d ∈ R ≥0 and a ∈ Σ, there exists some ( 2 , v 2 ) such that ( 1 , v 1 ) R ( 2 , v 2 ) and ( 2 , v 2 ) d,a --→ ( 2 , v 2 ).
A timed bisimulation is a timed simulation which is also symmetric, and two states ( 1 , v 1 ), ( 2 , v 2 ) ∈ A are said to be timed bisimilar, written (

1 , v 1 ) ∼ ( 2 , v 2 ), if there exists a timed bisimulation R for which ( 1 , v 1 ) R ( 2 , v 2 ).
Note that ∼ is itself a timed bisimulation on A (indeed the greatest such), which is easily shown to be an equivalence relation and hence transitive, reflexive, and symmetric. Also-as usual-timed bisimilarity may be lifted to an equivalence between two timed automata A and B by relating their initial states. Consider the four automata A, X, U and D in Fig. 6 (identifying the automata with the names of their initial locations). Here (U, v) and (D, v) are timed bisimilar as any transition (U, v)

d,a --→ (V, v ) may be matched by either (D, v) a -→ (G, v ) or (D, v) a -→ (E, v
) depending on whether v(y) > 2 or not after delay d. In fact, it may easily be seen that U and D are the only locations of Fig. 6 that are timed bisimilar (when coupled with the same valuation of y). E.g., A and X are not timed bisimilar since the transition (X, 0)

1.5,a ---→ (Y, 1.5) cannot be matched by (A, 0) by a transition with exactly the same duration. Instead A and X are related by the weaker notion of time-abstracted bisimulation, which does not require equality of the delays (see Definition 2). It may be seen that A and X are both time-abstracted simulated by U and D but not time-abstracted bisimilar to U and D. Also, U and D are time-abstracted bisimilar, which follows from the following easy fact:

Theorem 2. Any two automata being timed bisimilar are also time-abstracted bisimilar.

Checking (Bi)simulations

As we now explain, timed and time-abstracted (bi)similarity are decidable for timed automata.

Theorem 3. Time-abstracted similarity and bisimilarity are decidable for timed automata.

For proving this result, one only needs to see that time-abstracted (bi)simulation in the timed automaton is the same as ordinary (bi)simulation in the associated region automaton; indeed, any state in A is untimed bisimilar to its image in A ∼ = . The result follows by finiteness of the region automaton.

For timed bisimilarity, decidability-as we shall see in Sect. 9-is obtained by playing a game on a product construction, yielding an exponential-time algorithm for checking timed bisimilarity.

Theorem 4 ([73]

). Timed similarity and bisimilarity are decidable for timed automata.

5 Language-Theoretic Properties

Language of a Timed Automaton

This section introduces the notion of (timed) language associated with timed automata, and focusses on basic decision problems such as language emptiness and inclusion, as well as standard Boolean operations on languages.

Properties of languages associated with various computational models are a classical object of study in computer science; moreover, many model-checking, refinement, and verification problems can often be stated in terms of languages, notably by translating them into language emptiness or language inclusion problems.

In this section we consider timed automata augmented with sets of accepting locations. Given a timed automaton A = (L, 0 , C, Σ, I, E, F ), where F ⊆ L is the set of accepting locations, a finite run

ρ = ( 0 , v 0 ) d1,a1 -→ ( 1 , v 1 ) d2,a2 -→ . . . dn,an -→ ( n , v n ) of A is accepting if n ∈ F .
The language L(A) of A consists of all finite timed words over alphabet Σ * generated by accepting runs of A.

The language of infinite words accepted by a timed automaton is defined analogously; the relevant acceptance condition is that the underlying infinite run visits locations in F infinitely often. We write L ω (A) to denote the set of infinite timed words accepted by A.

Timed Automata with ε-Transitions

Silent transitions are transitions of the form (q, g, ε, r, q ), where ε is the empty word. In other terms, they are transitions carrying no letter. Silent transitions offer a convenient way of modeling, e.g., internal actions. In the setting of finite-state automata, it is well known that such transitions can be removed, by merging them with the possible subsequent actions.

x = 2 ε x := 0 x = 0 Σ Fig. 7 A timed automaton with εtransitions

The question whether the above result extends to the timed setting was settled in [START_REF] Bérard | Timed automata with nonobservable actions: Expressive power and refinement[END_REF], with a negative answer: to see this, simply consider the automaton in Fig. 7; its language L(A) contains precisely those timed words in which all timestamps are even integer numbers. Towards a contradiction, assume that there exists a timed automaton B, without ε-transitions, such that L(A) = L(B); write m for the maximal integer constant appearing in the timing constraints of B. Then the one-letter word (σ, 2m) is accepted by B, since it is accepted by A. Since B has no silent transition, it must have a σ-transition from an initial state to an accepting one. The guard on this transition can only involve constants less than or equal to m, so that B must accept (σ, k) for all k > m, which is a contradiction.

Theorem 5 ([42]

). Silent transitions strictly increase the expressive power of timed automata.

It can be proved that in the case when ε-transitions do not reset any clock, they do not add expressiveness. Finally, let us mention that the question whether a timed automaton with silent transitions is equivalent (i.e., accepts the same language) to some timed automaton without such transitions is undecidable [START_REF] Bouyer | Undecidability results for timed automata with silent transitions[END_REF].

In the sequel, we consider timed automata without ε-transitions.

Clock Constraints as Acceptance Conditions

Clock constraints can be used to enable or disable certain conditions along the runs of a timed automaton. As such, they can be used to define acceptance conditions, when added on top of a finite-state automaton.

In this setting, we consider the untimed language of timed automata: given a timed automaton A, its untimed language (of infinite words) is the set L u containing exactly those words (a i ) i∈N for which there is a diverging realvalued sequence (d i ) i∈N such that the timed word (a i , d i ) i∈N ∈ L ω (A). Notice that thanks to the time-abstracted bisimulation between a timed automaton and its region automaton, the untimed language of a timed automaton is easily seen to be ω-regular.

c x = y ∧ f < 1; a x = y ∧ f < 1; b x = y ∧ f = 1; a y := 0 x = y ∧ f = 1; b x := 0 x > y ∧ f > 1; a y > x ∧ f > 1; b Fig. 8
Automaton accepting words with finitely many a's or finitely many b's

Conversely, any ω-regular language is the untimed language of a timed automaton: as an example, consider the language of infinite words over {a, b, c} that have finitely many a's or finitely many b's. The untimed language of the automaton depicted in Fig. 8 precisely corresponds to that language: indeed, the a-and b-transitions on the left can only be taken finitely many times, since we require time divergence. Hence one of the a-and the b-transitions at the bottom has to be taken. But after this time, only the corresponding transition on the right is allowed (together with the c-transition, which is always allowed). This construction can be generalized, so that: Theorem 6 ([101]). Given an ω-regular language L, there exists a (onelocation) timed automaton A such that L u (A) = L.

The number of clocks and locations can be shown to define strict hierarchies of (untimed) ω-regular languages.

More generally, given a finite-state automaton A and an ω-regular language L, one can equip A with clocks and clock constraints in such a way that the untimed language of the resulting timed automaton is the intersection of the language of A with L [101].

Intersection, Union, and Complement

A (finite or infinite) language is said to be timed regular if it is accepted by some timed automaton. Timed regular languages (both finite and infinite) are effectively closed under intersection and union. They are however not closed under complement. We reproduce in Fig. 9 an example (taken from [START_REF] Alur | A theory of timed automata[END_REF]) of a timed automaton A, equipped with a single clock, that cannot be complemented: there does not exist a timed automaton A such that L ω (A ) is the set of all timed words not accepted by A. The complement of L ω (A) contains

A : a a a a x := 0 a x = 1
Fig. 9 A non-complementable timed automaton all timed traces in which no pair of a's is separated by exactly one time unit. Intuitively, since there is no bound on the number of a's that can occur in any unit-duration time interval, any timed automaton capturing the complement of L ω (A) would require an unbounded number of clocks to keep track of the times of all the a's within the past one time unit. A formal proof that A cannot be complemented is given in [105].

Under some restrictions, timed automata can be made determinizable (hence also complementable). Most notably, event-clock automata [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF] enjoy this property. In such timed automata, each letter a of the alphabet is associated with two clocks x a and y a (and any clock is associated with some letter that way): clock x a (called the event-recording clock of a) is used to measure the delay elapsed since the last reset of event a (and is initially set to some special value +∞), while y a (the event-predicting clock of a) is used to constrain the delay until the next occurrence of a. One can easily show that event-clock automata can be represented as classical timed automata, though several clocks might be needed to encode each event-recording clock. It must be remarked that, at any time during a run of an event-clock automaton on some timed word w, the valuation of the clocks does not depend on the run, but only on w. As a consequence, the classical subset construction for determinising finite-state automata can be adapted to handle event-clock automata, which thus form an (effectively) determinizable and complementable class of timed automata.

Language Emptiness, Inclusion

It follows immediately from Theorem 1 that the language-emptiness problem for timed automata is PSPACE-complete [START_REF] Alur | A theory of timed automata[END_REF]. Unfortunately the languageuniversality, language-inclusion and language-equivalence problems for timed automata are all undecidable. By contrast, recall from Theorem 4 that the related branching-time counterparts to language inclusion and equivalence, namely similarity and bisimilarity, are both decidable on timed automata.

Theorem 7 ([13]

). The language-inclusion problem for timed automata is undecidable, both over finite and infinite words.

The proof of Theorem 7 is by reduction from the Halting Problem for Turing machines. This reduction involves encoding the valid halting computations of a given Turing machine M as a timed language whose complement is recognized by a timed automaton A M which can be effectively computed from M . Intuitively, discrete computation steps of M are simulated over unit-duration time intervals, with timed events used to encode the tape's contents. The integrity of the tape in a valid encoding of a computation is maintained by requiring that any given timed event be preceded and followed at a distance of exactly one time unit by the same timed event, and vice-versa (unless the corresponding character is to be modified by M in the computation step). Figure 11 illustrates this encoding. Note that the density of time enables one to accommodate arbitrarily large tape contents. The key idea is that while no timed automaton can in general accurately capture the encodings of valid computations of a Turing machine, A M can be engineered to recognise precisely all the invalid computations of M ; indeed, a computation is invalid if it fails one of finitely many rules, the most interesting of which is to adequately preserve the tape's contents. The latter is easily detected, either by a timed automaton witnessing a timed event with no predecessor one time unit earlier (corresponding to an insertion error on the tape), or conversely by a timed automaton witnessing a timed event with no successor one time unit later (corresponding to a deletion error on the tape). Other rule failures can likewise be detected by small timed automata. Automaton A M is obtained as the disjunction of those finitely many timed automata. The upshot is that M fails to have a valid halting computation iff A M accepts every single timed trace. This shows that universality, and a fortiori language inclusion, are indeed undecidable for timed automata.

Theorem 7 places a serious limitation on the algorithmic analysis of timed automata since many verification questions naturally reduce to checking language inclusion. In spite of this hindrance there has been a great deal of research on various aspects of timed language inclusion, including [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF]102,134] among many others. Here we describe several approaches, involving syntactic and semantic restrictions on timed automata, to obtaining positive decidability results for language inclusion.

Let us first notice that the classical approach to deciding language inclusion is by testing emptiness of the intersection of the first language with the complement of the second one. Thus whether L ω (A) ⊆ L ω (B) is decidable as soon as B can be complemented. For instance: Theorem 8 ( [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF]). Given timed automata A and B, the language-inclusion problem

L ω (A) ⊆ L ω (B) is decidable if B is an event-clock automaton.
Using more elaborate techniques (based on well-quasi-orderings and Higman's Lemma), we can prove: Theorem 9 ([124, 134, 135]). Given timed automata A and B, the finiteword language-inclusion problem L(A) ⊆ L(B) is decidable and non-primitive recursive provided B has at most one clock.

In the case of infinite words, the language-inclusion problem L ω (A) ⊆ L ω (B) is undecidable even when B has only one clock. The proof of undecidability is by reduction from the boundedness problem for lossy channel machines [START_REF] Parosh | Decidability and complexity results for timed automata via channel machines[END_REF].

A natural semantic restriction on timed automata to recover decidability of language inclusion involves adopting a discrete-time model. Given a timed language L, let Z(L) denote the set of timed words (a 1 , t 1 ) . . . (a p , t p ) such that each timestamp t i lies in Z. Given timed automata A and B, the discrete-time language-inclusion problem is to decide whether Z(L(A)) ⊆ Z(L(B)). This problem is EXPSPACE-complete: the exponential blow-up over the complexity of the language-inclusion problem for classical non-deterministic finite automata arises from the succinct binary representation of clock values in timed automata. Hardness in EXPSPACE is proven in [START_REF] Baier | When are timed automata determinizable?[END_REF].

Using a technique called digitization [102] the discrete behaviors of timed automata can be used to infer conclusions about their dense-time behavior. For example: Theorem 10 ([102]). Let A be a closed timed automaton (i.e., having only non-strict inequalities as clock constraints) and B an open timed automaton (i.e., having only strict inequalities). Then L(A) ⊆ L(B) if and only if

Z(L(A)) ⊆ Z(L(B)).
To apply Theorem 10 one can imagine over-approximating a real-time model by a closed timed automaton and under-approximating a specification by an open timed automaton.

Rather than restricting the precision of the semantics we can instead consider a time-bounded semantics in which we consider only finite timed words of total duration at most N . Note that due to the density of time there is no bound on the number of events that can be performed in a fixed time period. In this case, for the whole class of timed automata, we have: Theorem 11 ([133]). Over bounded time (i.e., considering only finite timed words of total duration at most N , for some fixed time bound N ), the languageinclusion problem is 2-EXPSPACE-complete.

Theorem 11 was proven as a corollary of the decidability of satisfiability of monadic second-order logic over structures of the form (I, <, +1), with I a bounded interval of reals and +1 denoting the plus-one relation: +1(x, y) iff y = x + 1.

Notwithstanding the positive decidability results Theorem 9 and Theorem 11, neither one-clock timed automata nor automata over bounded time are closed under complement. (The counterexample in Sect. 5.4 can still be used in both cases.) To remedy this deficiency, the strictly more powerful model of alternating timed automata has been introduced [124, 135]. Alternating timed automata are a common generalization of timed automata and alternating finite automata; they are closed under all Boolean operations, but language inclusion remains decidable for alternating timed automata with one clock or over bounded time. Unlike in the untimed setting, alternating timed automata are strictly more expressive than purely non-deterministic timed automata. This extra expressiveness is crucially utilised in [135] where it is shown how to translate formulas of Metric Temporal Logic (see Sect. 6) into equivalent one-clock alternating timed automata.

Timed Temporal Logics

The whole theory of temporal-logic model checking has been extended to the setting of timed automata, in order to express and check richer properties beyond emptiness/reachability. We present the most significant results below.

Linear-Time Temporal Logics

The most natural way of extending LTL (see Chap. 2temp) with quantitative requirements is by decorating modalities with timing constraints. We present the resulting logic, called Metric Temporal Logic (MTL), below. Another extension consists in using clocks in formulas, with a way of resetting them when some property is fulfilled and checking their values at a later moment. The resulting logic is called Timed Propositional Temporal Logic (TPTL). Due to lack of space, we don't detail the latter logic, and rather refer to [START_REF] Alur | Real-time logics: Complexity and expressiveness[END_REF][START_REF] Alur | A really temporal logic[END_REF][START_REF] Bouyer | On the expressiveness of TPTL and MTL[END_REF] for more details about TPTL.

Given a set P of atomic propositions, the formulas of MTL are built from P using Boolean connectives and time-constrained versions of the until operator U as follows:

ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | ϕ U I ϕ ,
where I ⊆ (0, ∞) is an interval of reals with endpoints in N ∪ {∞}. We sometimes abbreviate U (0,∞) to U , calling this the unconstrained until operator.

Further connectives can be defined following standard conventions. In addition to propositions (true) and ⊥ (false) and disjunction ∨, we have the constrained eventually operator ♦ I ϕ ≡ U I ϕ, and the constrained always operator I ϕ ≡ ¬♦ I ¬ϕ.

Sometimes MTL is presented with past connectives (e.g., constrained versions of the "since" connective from LTL) as well as future connectives [START_REF] Alur | Real-time logics: Complexity and expressiveness[END_REF]. However we do not consider past connectives in this chapter.

Next we describe two commonly adopted semantics for MTL.

Continuous Semantics.

Given a set of propositions P , a signal is a function f : R ≥0 → 2 P mapping t ∈ R ≥0 to the set f (t) of propositions holding at time t. We say that f has finite variability if its set of discontinuities has no accumulation points (in other words, on any finite interval the value of f can only change a finite number of times). In this chapter, we require that all signals be finitely variable. Given an MTL formula ϕ over the set of propositional variables P , the satisfaction relation f |= ϕ is defined inductively, with the classical rules for atomic propositions and Boolean operators, and with the following rule for the "until" modality, where f t denotes the signal f t (s) = f (t + s):

f |= ϕ 1 U I ϕ 2 iff for some t ∈ I, f t |= ϕ 2 and f u |= ϕ 1 for all u ∈ (0, t).

Pointwise Semantics.

In the pointwise semantics MTL formulas are interpreted over timed words. Given a (finite or infinite) timed word w = (a 1 , t 1 ), . . . , (a n , t n ) over alphabet 2 P and an MTL formula ϕ, the satisfaction relation w, i |= ϕ (read "w satisfies ϕ at position i") is defined inductively, with the classical rules for Boolean operators, and with the following rule for the "until" modality:

w, i |= ϕ 1 U I ϕ 2 iff there exists j such that i < j < |w|, w, j |= ϕ 2 , t j -t i ∈ I, and w, k |= ϕ 1 for all k with i < k < j.

The pointwise semantics is less natural if one thinks of temporal logics as encoding fragments of monadic logic over the reals. On the other hand it seems more suitable when considering MTL formulas as specifications on timed automata. In this vein, when adopting the pointwise semantics it is natural to think of atomic propositions in MTL as referring to events (corresponding to location changes) rather than to locations themselves.

Consider our example of Fig. 2. Using LTL, we can express the property that Process P i will try to get the resource infinitely many times, by writing ♦ start!. With MTL, we can be more precise and write ♦ ≤4 start!, stating that whatever the current state, within four time units Process P 1 will start trying to acquire the resource. MTL can also be used to express bounded-time response properties, such as (start! ⇒ ♦ ≤10 acquire!).

Verification of Linear-Time Temporal Logics

Model checking timed automata can be carried out under either pointwise or continuous semantics. For the latter, it is necessary to alter our definitions to associate a language of signals with a timed automaton rather than a language of timed words. In turn, this requires a notion of timed automata in which locations are labelled by atomic propositions. A full development of this semantics can be found, e.g., in [START_REF] Alur | The benefits of relaxing punctuality[END_REF].

Theorem 12 ([13]). Model checking and satisfiability for LTL, over both the pointwise and continuous semantics, are PSPACE-complete.

The PSPACE upper bound in Theorem 12 can be established in the same manner as in the untimed case, by translating the negated formula to a Büchi automaton, and performing an on-the-fly reachability check on the product of this automaton with the region graph of the model.

Theorem 13 ([135-137]). Model checking and satisfiability for MTL in the pointwise semantics over finite words are decidable but non-primitive recursive. Over infinite words, both problems are undecidable.

As explained in Sect. 5.5, the decidability results are essentially obtained by translating MTL formulas into one-clock alternating timed automata, and rephrasing the model-checking or satisfiability problems as instances of language emptiness in one-clock alternating timed automata.

The undecidability result proceeds by reduction from the recurrent reachability problem for channel machines with insertion errors: the infinite runs of such a machine can be encoded as timed words, which in turn are easily characterized by an MTL formula [136].

Theorem 14 ([14]). Model checking and satisfiability for MTL in the continuous semantics (over both finite and infinite signals) are undecidable.

The extra expressiveness of the continuous semantics enables a more direct proof of undecidability than in Theorem 13. In this case, one can directly encode the computations of a Turing machine as timed signals, which again can be captured by an MTL formula, following a scheme similar to that of Theorem 7.

A key ingredient of the undecidability proof of Theorem 14, as well as the non-primitive recursive complexity in Theorem 13, is the ability of MTL to express punctuality, i.e., the requirement that two events be separated by an exact duration. A fragment of MTL that syntactically disallows punctuality, known as Metric Interval Temporal Logic (MITL), was proposed by Alur et al. in [START_REF] Alur | The benefits of relaxing punctuality[END_REF]. In MITL, one requires that all instances of the interval I appearing in uses of the constrained until operator U I be non-singular. The main result of [START_REF] Alur | The benefits of relaxing punctuality[END_REF] is as follows:

Theorem 15 ( [START_REF] Alur | The benefits of relaxing punctuality[END_REF]). For both the pointwise and continuous semantics, model checking and satisfiability for MITL are EXPSPACE-complete, over both finite and infinite behaviors.

This theorem was obtained by translating MITL formulas into equivalent timed automata of potentially exponential size. In contrast, it is easy to write an MTL formula that has no equivalent timed automaton: for example, the formula ¬♦ (a ∧ ♦ =1 a) captures the complement of the language of automaton A in Fig. 9.

Another decidable fragment of MTL can be obtained by adapting the idea of event clocks to temporal logics [140]: here, timing constraints can only refer to the next (or previous) occurrence of an event. Hence ECTL (standing for Event-Clock Temporal Logic) extends LTL with I ϕ and I ϕ. For instance, that there are two consecutive a's separated by one time unit is written in ECTL as ♦ (a ∧ =1 a).

Theorem 16 ([140]

). Satisfiability and model checking are PSPACE-complete for ECTL, in either the pointwise or continuous semantics.

Not surprisingly, deciding ECTL is achieved by a translation to event-clock automata (see Sect. 5.4). However, event-clock automata are not powerful enough to precisely capture ECTL, and require the use of timed Hintikka sequences. Intuitively, given a formula ϕ in ECTL, a timed Hintikka sequence is a timed word on sets of subformulas of ϕ, required to satisfy local consistency conditions. Compare to a timed word, a timed Hintikka sequence contains more information about the truth value of the subformulas of ϕ, which will help the event-clock automaton decide whether the underlying timed word is to be accepted. We refer to [140] for more details, and to [104] for an extension of event-clock automata that encompasses ECTL.

Rather than imposing syntactical restrictions, an alternative approach to recovering decidability is to consider a time-bounded semantics, i.e., in which either timed words or signals are observed over a fixed, bounded time interval: Theorem 17 ([133]). Model checking and satisfiability for MTL over bounded time, in either the pointwise or continuous semantics, are EXPSPACEcomplete.

The main technique used in the proof of Theorem 17 is an exponential transformation from MTL formulas, given a fixed time bound, into equisatisfiable LTL formulas.

Branching-Time Temporal Logics

Given a set P of atomic propositions, TCTL * formulas are state-formulas obtained as formulas ϕ s from the following grammar:

ϕ s ::= p | ¬ ϕ s | ϕ s ∧ ϕ s | Eϕ p | Aϕ p ϕ p ::= ϕ s | ¬ ϕ p | ϕ p ∧ ϕ p | ϕ p U I ϕ p
Compared to CTL * , TCTL * has a time-constrained until, requiring as for MTL that the right-hand side formula should be fulfilled within that time. The same shorthands as for MTL can be defined, such as ♦ I ϕ or I ϕ.

As for the linear-time temporal logics, the semantics of TCTL * comes in (at least) two flavours: continuous and pointwise. The continuous semantics is defined on dense trees, which naturally extend classical discrete trees to the continuous setting [START_REF] Alur | Techniques for Automatic Verification of Real-Time Systems[END_REF][START_REF] Faella | Dense real-time games[END_REF] and represent the set of signals of timed automata; this semantics extends the continuous-time semantics of MTL with path quantifiers.

The pointwise semantics is defined over discrete (but infinite-branching) trees, which can be used to represent the timed words generated by timed automata. This corresponds to evaluating TCTL * formulas over the operational semantics of timed automata, as defined in Sect. 2.

Finally, as for the untimed case, the fragment of TCTL * where each temporal modality is under the immediate scope of a path quantifier is of particular interest, and will be called TCTL.

Before turning to the algorithmic part, let us show how TCTL can be used to express desirable properties of the timed system modeled in Fig. 2. Mutual exclusion (in a setting with two processes P 1 and P 2 and one resource R 1 ) is expressed as ¬ E♦ (working 1 ∧ working 2 ): two processes will never be working (i.e., using the resource) at the same time. We can also express timing requirements, such as the fact that Process P i will never be working continuously for more than one time unit: A ( A♦ ≤1 ¬ working i ).

Verification of Branching-Time Temporal Logics

Since TCTL * embeds MTL, there is no hope that its model checking and satisfiability will be decidable. On the lower side, CTL model checking is clearly decidable over timed automata: CTL is invariant under bisimulation, so that any property to be checked on a timed automaton can equivalently be checked on its corresponding finite-state region automaton.

Concerning TCTL, model checking can be shown to be decidable. Actually, this can easily be shown on the explicit-clock version of TCTL (using formula clocks), which strictly subsumes TCTL. For this logic, the important property is that any two region-equivalent states satisfy the same formulas: this can be proven by induction on the structure of the formula. Consider for instance the formula ζ = Eϕ U I ψ, assuming that ϕ and ψ are compatible with region (i.e., if they hold true in some state, then they also hold true in any regionequivalent state). Given a timed automaton A, consider the automaton A t obtained by adding an extra clock t to A, which does not modify its behavior. Then if ( , v) |= ζ in A, then ( , v t ) |= Eϕ U (ψ ∧ t ∈ I) where v t extends v by mapping clock t to zero and "t ∈ I" (which is not a TCTL formula but whose meaning is rather clear) is also compatible with regions. In the end, the set of states in A t where formula Eϕ U (ψ ∧ t ∈ I) is a union of regions, so that it is also the case for the set of states of A where ζ holds.

Using this result, TCTL model checking can be achieved by labeling states of the region automaton with the subformulas they satisfy. This applies for both semantics, with slight differences. It should be noticed that this extends to the explicit-clock version of TCTL, and even to the fragment of explicit-clock TCTL * where formula-clocks are only reset at the level of path quantifiers [START_REF] Brihaye | Timed concurrent game structures[END_REF].

While labeling the region automaton requires exponential space, the algorithm can be implemented in a space-efficient manner so as to only use polynomial space. Reachability being already PSPACE-hard, we get the following theorem: Theorem 18 ( [START_REF] Alur | Model-checking in dense realtime[END_REF]). TCTL model checking is PSPACE-complete. TCTL (as well as CTL) suffers from not being able to express useful properties, in particular fairness (see Chap. 2temp on temporal logics). One way to solve this problem is by decorating path quantifiers with fairness requirements [START_REF] Alur | Techniques for Automatic Verification of Real-Time Systems[END_REF]152]. One can then apply classical algorithms for CTL with fairness [START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF] or adapt fixpoint characterizations. Another approach is to consider TCTL defined with formula clocks as sketched above, and to have it include CTL * . The resulting logic is very expressive while still enjoying a PSPACE model-checking algorithm [START_REF] Brihaye | Timed concurrent game structures[END_REF].

These positive results about model checking do not extend to satisfiability: Theorem 19 ( [START_REF] Alur | Model-checking in dense realtime[END_REF]). TCTL satisfiability is undecidable.

The proof follows the same ideas as for undecidability of MTL satisfiability, by associating universal path-quantifiers with each temporal modality. As for the linear-time case, it suffices to ban equality constraints to recover decidability [117,118]. This can be proved by lifting tree-automata techniques to the timed setting.

7 Symbolic Algorithms, Data Structures, Tools

Zones and Operations

As shown in the previous sections, the regions introduced in Sect. 3 provide a finite and elegant abstraction of the infinite state space of timed automata, enabling us to prove decidability of a wide range of problems, including (timed and untimed) bisimilarity, untimed language equivalence and language emptiness, as well as TCTL model checking.

Unfortunately, the number of states obtained from the region partitioning is extremely large. Indeed, it is exponential in the number of clocks as well as in (the binary representation of) the maximal constants of the timed automaton [START_REF] Alur | A theory of timed automata[END_REF]. Efforts have been made to develop more efficient representations of the state space [START_REF] Behrmann | Efficient timed reachability analysis using clock difference diagrams[END_REF][START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF]103,121], using the notion of zones introduced below as a coarser and more compact representation of the state space.

For a finite set C of clocks, a subset Z ⊆ R C ≥0 is called a zone if there exists ϕ ∈ Φ d (C) for which Z = ϕ C . For reachability analysis, we need the following operations on zones: for a zone Z ⊆ R C ≥0 and r ⊆ C, let us denote

• the delay of Z by Z ↑ = {v + d | v ∈ Z, d ∈ R ≥0 } and • the reset of Z under r by Z[r] = {v[r] | v ∈ Z}.
Lemma 1 ([103, 157]). Let Z, Z be zones over C and r ⊆ C. Then Z ↑ , Z[r], and Z ∩ Z are also zones over C. Definition 5. The zone automaton associated with a timed automaton A = (L, 0 , C, Σ, I, E) is the transition system A Z = (S, s 0 , Σ ∪ {δ}, T ) given as follows:

S = ( , Z) ∈ L, Z ⊆ R C ≥0 is a zone s 0 = 0 , v 0 T = ( , Z) δ , Z ↑ ∩ I( ) C ∪ ( , Z) a , (Z ∩ ϕ C )[r] ∩ I( ) C ϕ,a,r ---→ ∈ E
Analogously to Prop. 1, we have:

Proposition 2 ([157]). A location in a timed automaton A = (L, 0 , F, C, Σ, I, E) is reachable if and only if there is a zone Z ⊆ R C ≥0 for which ( , Z) is reachable in A Z .
A priori, however, the zone automaton defined above is infinite, hence another, finite, abstraction is needed. This is provided by normalization using region equivalence ∼ =M : for a maximal constant M , the normalization of a zone

Z ⊆ R C ≥0 is the set {v : C → R ≥0 | ∃v ∈ Z : v ∼ =M v }.
The normalization of a zone is not in general a zone, hence in practice other normalization operators are used (see Sect. 7.3). The normalized zone automaton is defined analogously to the zone automaton defined above, and in case the timed automaton to be verified does not contain diagonal clock constraints of the form x -y k, Prop. 2 also holds for the normalized zone automaton. Hence we can obtain a reachability algorithm by applying any search strategy (depth-first, breadth-first, or another) on the normalized zone automaton.

For timed automata that contain diagonal clock constraints x -y k, however, it can be shown [START_REF] Bengtsson | On clock difference constraints and termination in reachability analysis of timed automata[END_REF][START_REF] Bouyer | Untameable timed automata![END_REF] that normalization as defined above does not give rise to a sound and complete characterization of forward reachability. Instead, one can apply a refined normalization which depends on the difference constraints used in the timed automaton, see [START_REF] Bengtsson | On clock difference constraints and termination in reachability analysis of timed automata[END_REF].

Symbolic Datastructures

A zone, given by a conjunction of elementary clock constraints, may be represented using a directed weighted graph, where the nodes correspond to the clocks in C together with an extra "zero" clock x 0 , and an edge x i k -→ x j corresponds to a constraint x i -x j ≤ k (if there is more than one upper bound on x i -x j , k is the minimum of all these constraints' right-hand sides). The extra clock x 0 is fixed at value 0, so that a constraint x i ≤ k can be represented as x i -x 0 ≤ k. Lower bounds on x i -x j are represented as (possibly negative) upper bounds on x j -x i , and strict bounds x i -x j < k are represented by adding a flag to the corresponding edge.

The weighted graph in turn may be represented by its adjacency matrix, which in this context is known as a difference-bound matrix or DBM. The above technique was introduced in [START_REF] David | Timing assumptions and verification of finite-state concurrent systems[END_REF] (the main ideas were already present in [START_REF] Berthomieu | An enumerative approach for analyzing time Petri nets[END_REF]). Figure 12 gives an illustration of an extended clock constraint together with its representation as a difference-bound matrix. Note that the clock constraint contains superfluous information.

Z =                    x 1 ≤ 3 x 1 -x 2 ≤ 10 x 1 -x 2 ≥ 4 x 1 -x 3 ≤ 2 x 3 -x 2 ≤ 2 x 3 ≥ -5 x 0 x 3 x 2 x 1 5 2 -4 10 2 3
Fig. 12 Graph representation of extended clock constraint On zones represented using DBMs, efficient (in time cubic in the number of clocks in C) algorithms are available for computing delays, resets and intersections. For reachability checking, other necessary operations inclusion checking whether Z ⊆ Z , and emptiness checking, Z = ∅; these can also be computed efficiently using DBMs.

For these computations, a canonical representation obtained as the shortestpath closure of the DBM graph is used. Another useful canonical form is the shortest-path reduction described in [120]. Whereas the shortest-path closure form gives all derived constraints, the shortest-path reduced form provides a memory-efficient representation, containing only a minimal set of constraints. Figure 13 shows the two canonical forms of the DBM of Fig. 12. Given the shortest-path closure of the DBM graph, the shortest-path reduced form is obtained by partitioning the set of clocks according to zero cycles in the DBM graph; in the DBM of Fig. 13, {x 1 , x 2 , x 3 } constitutes one such class, and {x 0 } is another one. The reduced form is now obtained by maintaining a minimal set of constraints for each class, essentially a simple cycle of the clocks of the class, and only keeping constraints between representatives of different classes, here x 1 and x 0 .

To combat state-space explosion in zone graphs, several optimizations are used. One such approach is to detect whether a state ( , Z) reached through the algorithm is contained in another state ( , Z ) which has already been explored. In this case, exploration of ( , Z) will be unnecessary.

Another such optimization is to work with unions of zones. If states ( , Z) and ( , Z ) are found to reachable during the analysis, then we know that altogether the state ( , Z ∪ Z ) is reachable. Unfortunately, unions of zones are not generally themselves zones, so cannot be efficiently represented using DBMs.

Shortest-path closure

x 0 x 3 x 2 x 1 5 1 2 -2 -4 4 3 3 7 -1 2 -2 Shortest-path reduction x 0 x 3 x 2 x 1 2 -4 3 3 2 Fig. 13 Canonical representations
For representing unions of zones, or federations as they are called in this context, a data structure inspired by decision diagrams called clock difference diagrams or CDDs is used [121]. However, no efficient algorithms are known to compute delays or resets of federations using CDDs, so in practice reachability analysis using CDDs is done by extracting the zones from the CDD and performing the operations on them one by one.

Other promising data structures in this context are numerical decision diagrams [START_REF] Asarin | Data-structures for the verification of timed automata[END_REF], difference decision diagrams [132], clock-restriction diagrams [154], max-plus polyhedra [START_REF] Xavier Allamigeon | Inferring min and max invariants using max-plus polyhedra[END_REF], constraint matrix diagrams [START_REF] Ehlers | Fully symbolic timed model checking using constraint matrix diagrams[END_REF], and time-darts [111]; generally, the design of efficient data structures for symbolic exploration of timed automata is a field of active research.

Practical Efficiency

Symbolic, zone-based exploration of the (reachable) state-space of timed automata using the DBM data structure is key to their analysis. However, a number of additional algorithmic techniques have been developed for gaining efficiency in practice. In the following we indicate a number of these.

As described in Sect. 7.1, normalization of zones with respect to the maximum constant M appearing in the given timed automata ensures finiteness of the zone graph and hence termination of algorithms searching the zone graph. Here, a practical problem is that the normalization of a zone is in general not a zone itself, but rather a finite union of such. However, given a representation of the zone as a shortest-path-closed DBM, a syntactic extrapolation operation that removes bounds that are larger than the maximum constant may be easily performed: any upper bound constraint of the form x i -x j < k where k > M is removed, and any lower bound of the form x i -x j > k where k < -M is replaced by x i -x j > -M . Clearly, under extrapolation, only a finite number of DBMs will be encountered, ensuring termination. Furthermore, the correctness is based on the fact that extrapolation of a zone (based on its DBM representation) is included in its normalization, as shown in [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF][START_REF] Bouyer | Untameable timed automata![END_REF].

Coarser, yet complete, notions of extrapolation have been obtained by performing the operation with respect to clock-and location-dependent maximum constants [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF] and further differentiating the maximum constant used in upper or lower bound comparisons [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF][START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]. In fact, this last extrapolation yields performance comparable to that of the overapproximate convex hull abstraction [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF].

Several of the algorithmic problems presented in this chapter-e.g., reachability, model checking, and equivalence checking, as well as notions of optimal reachability and controllability, which will be described in later sectionshave a fixed-point characterization. Though easy to implement, this leads to backwards iterative algorithms, requiring one to consider and classify states which are possibly not even reachable. Thus, for most problems, so-called on-the-fly algorithms have been devised, where the satisfaction of the given property by the initial state is attempted to be concluded in as local a fashion as possible, only exploring the state space when needed. For the analysis of timed-automata-based models, such on-the-fly algorithms have been proposed for instance for reachability [120, 157], liveness checking [147, 151], model checking with respect to TCTL [START_REF] Bouajjani | On-the-fly symbolic model checking for real-time systems[END_REF], time-abstract bisimulation checking [149], and controller synthesis for timed game automata [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF].

Despite the above efforts in applying aggressive (yet complete) abstractions, the analysis of timed-automata-based models suffers from the state-space explosion problem. Thus, complementary techniques have been proposed and implemented for reducing space consumption at the expense of time performance [START_REF] Behrmann | To store or not to store[END_REF]120]. Also, various AI-inspired techniques have been developed for efficient guidance of the symbolic exploration of timed automata towards specified error states [114][115][116]. Similarly, the technique of symmetry reduction has been developed and implemented for networks of timed automata with several symmetric components, potentially yielding an exponential gain in performance [START_REF] Hendriks | Adding symmetry reduction to Uppaal[END_REF]. Moreover, so-called time-convexity analysis provides significant performance improvement [153].

Finally, several attempts have been made to extend the technique of partialorder reduction to networks of timed automata. In contrast to the proved effect in the finite-state setting, early attempts [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF]131] did not show any improvement in performance compared with regular symbolic exploration. In fact, being a strong synchronizer in a timed-automata network, time reduces the number of independent transitions, which are key for partial-order reduction to have effect. In later work [START_REF] Ben Salah | On interleaving in timed automata[END_REF]125,126], it was found that the union of all zones reached by different interleavings of the same set of transitions is convex, providing the basis of substantial improvement.

Also, bounded model-checking techniques have been developed for timed automata using difference logics, though with a limited performance improvement [START_REF] Cotton | Some progress in satisfiability checking for difference logic[END_REF][START_REF] Cotton | Fast and flexible difference constraint propagation for DPLL(T)[END_REF].

Tools and Applications

Timed automata and their extensions have been applied to the modeling, analysis and optimization of numerous real-time applications. In this section we give a few examples, not aiming at being exhaustive but rather to illustrate the wide range of application domains.

A variety of mature tools are available which provide important computeraided support for applications. Well-known tools include UppAal [122], Kronos [158], RED [155] and HyTech [START_REF] Henzinger | A user guide to HyTech[END_REF]. A larger number of other tools related to the analysis of timed automata have emerged over the years including Else [159], Rabbit [START_REF] Beyer | Rabbit: A tool for BDD-based verification of real-time systems[END_REF], Verics [START_REF] Dembinski | Verics: A tool for verifying timed automata and estelle specifications[END_REF], and TAME [START_REF] Archer | Using TAME to prove invariants of automata models: Two case studies[END_REF] as well as tools for analyzing other timed formalisms based on translation to timed automata including Times [START_REF] Amnell | Times -a tool for modelling and implementation of embedded systems[END_REF] (task automata), Moby [145] (PLC programs), SART [START_REF] Bøgholm | Model-based schedulability analysis of safety critical hard real-time Java programs[END_REF] (Safety Critical Java), ART [START_REF] Michael | Semantics and verification of a language for modelling hardware architectures[END_REF] (task graphs), Romeo [START_REF] Gardey | Romeo: A tool for analyzing time Petri nets[END_REF] and TAPALL [START_REF] Byg | TAPAAL: Editor, simulator and verifier of timed-arc Petri nets[END_REF] (Time and Timed-arc Petri Nets), and VeSTA [112] (component integration checking).

The timed-automata formalism is now routinely applied to the modeling and analysis of real-time control programs, including a wide class of Programmable Logic Controller (PLC) control programs [START_REF] Dierks | PLC-automata: a new class of implementable real-time automata[END_REF]127] and timing analysis and code generation of vehicle control software [150]. The timed-automata approach has also demonstrated its viability in the timing analysis of certain classes of asynchronous circuits [START_REF] Bozga | Verification of asynchronous circuits using timed automata[END_REF].

Similarly, numerous real-time communication protocols have been analyzed using timed automata technology, often with inconsistencies being revealed: e.g., using real-time model checking, the cause of a ten-year-old bug in the IR-link protocol used by Bang & Olufsen was identified and corrected [START_REF] Havelund | Formal modelling and analysis of an audio/video protocol: An industrial case study using Uppaal[END_REF]. Most recently, real-time model checking has been applied to the clock synchronization algorithm currently used in a wireless sensor network that has been developed by the Dutch company CHESS [144]. Here it is shown that in certain cases a static, fully synchronized network may eventually become unsynchronized if the current algorithm is used, even in a setting with infinitesimal clock drifts.

During the last few years, timed automata modeling of multitasking applications running under real-time operating systems has received substantial research effort. Here the goals are multiple: to obtain less-pessimistic worst-case response time analysis compared with classical methods for single-processor systems [156]; to relax the constraints of period task arrival times of classical scheduling theory to task arrival patterns that can be described using timed automata [START_REF] Fersman | Schedulability analysis of fixed-priority systems using timed automata[END_REF]; to allow for schedulability analysis of tasks in terms of concurrent objects executing on multiprocessor or distributed platforms (e.g., MPSoC) [START_REF] Brekling | Models and formal verification of multiprocessor system-on-chips[END_REF][START_REF] David | Model-based design for embedded systems[END_REF]109].

Just as symbolic reachability checking of finite-state models has led to very efficient planning and scheduling algorithms, reachability checking for (priced) timed automata has demonstrated competitive and complementary performance with respect to classical approaches such as MIPL on optimal scheduling problems involving real-time constraints, e.g., job-shop and task-graph scheduling [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF][START_REF] Behrmann | Efficient guiding towards cost-optimality in Uppaal[END_REF] and aircraft landing problems [119]. In fact a translation of the variant PDDL3 of PDDL (Planning Domain Definition Language) into priced timed automata has been made [START_REF] Dierks | Finding optimal plans for domains with continuous effects with UPPAAL Cora[END_REF] allowing optimal planning questions to be answered by cost-optimal reachability checking. Industrial applications include planning a wafer scanner from the semiconductor industry [START_REF] Hendriks | Model checker aided design of a controller for a wafer scanner[END_REF] and computation of optimal paper paths for printers [108].

Most recently, computation of winning strategies for timed games has been applied to controller synthesis for embedded systems, including synthesis of most general non-preemptive online schedulers for real-time systems with sporadic tasks [START_REF] Altisen | A framework for scheduler synthesis[END_REF], synthesis of climate control for pig shed provided by the company Skov [110], and automatic synthesis of robust and near-optimal controllers for industrial hydraulic pumps [START_REF] Cassez | Automatic synthesis of robust and optimal controllers -an industrial case study[END_REF].

Weighted Timed Automata

Time is not the only quantity one may want to measure when checking an embedded system: one may need to keep track of the battery charge or of the level of oil in a tank. Hybrid automata [START_REF] Henzinger | The theory of hybrid automata[END_REF]100] extend timed automata with extra variables that can help measure such quantities. Unfortunately, reachability is undecidable for these models, even with two-slope hybrid variables. Weighted timed automata [START_REF] Alur | Optimal paths in weighted timed automata[END_REF][START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] is an intermediary model, extending timed automata with hybrid observer variables: these variables cannot appear in the guards of the automaton, but they can be used, for example, for optimization purposes. The special case where the observer is a stopwatch (computing the accumulated delay in some locations) was already introduced and solved in [START_REF] Alur | Computing accumulated delays in real time systems[END_REF].

Formally, a weighted timed automaton is a pair (A, w) where A is a timed automaton and w labels the locations and edges of A with an integer (or a vector of integers for automata with multiple observer variables). For a transition t, w(t) is the value by which the value of the observer variable is increased, while for a location , w( ) is the rate by which the variable increases w.r.t. time (in other words, the observer variable p follows the differential equation dp/dt = w( )).

The semantics of a weighted timed automaton (A, w) is that of the underlying timed automaton A. Each run of A is decorated with the value of the observer variable. Figure 14 shows an example of a weighted timed automaton 3 , and a run of this automaton. This run reaches the rightmost location within 3 time units, and with a total weight of 19.7.

Cost-Optimal Schedules

Natural questions on this family of models include optimal reachability of a given location, or optimal mean-cost of infinite runs. Formally, the associated decision problems respectively ask whether the target location can be reached with total weight less than a given threshold, and whether there is an infinite run along which the average weight is less than the given bound. These problems turn out to be decidable. The main technique used in the algorithms is a refinement of the region equivalence of Sect. 3 called corner-point equivalence [START_REF] Bouyer | Staying alive as cheaply as possible[END_REF]. Intuitively, for these two optimization problems, optimal schedules will amount to staying as long as possible in interesting locations. Corner-point regions extend classical regions with an extra corner of this region, i.e., an integer valuation that belongs to the closure of the region. A corner-point (r, c) represents a clock valuation v that is close to the corner c but lies within the region r. The corner-point automaton is the weighted automaton C M = (S, s 0 , Σ, T ) where S ⊆ L × R × {0, ..., M } C is the set of states (writing R for the set of regions), with three kinds of transitions:

• action transitions: there is a transition from ( , R, c) to ( , R , c ) if there is a transition t = ( , ϕ, a, r,

) in A such that R ⊆ ϕ C , with R = R[r] and c = c[r].
The weight of this transition is w(t). • ε-delay transitions: these are transitions from ( , R, c) to ( , R , c), where R is the immediate time-successor of R sharing corner c. Such a transition corresponds to a very small delay, and its corresponding weight is set to zero. • 1-delay transitions: these are transitions from ( , R, c) to ( , R, c ), where c = c + 1. This corresponds to spending (almost) one time unit in re-gion ( , R). Notice that such a transition is only available if c and c + 1 are corners of R. The weight of this transition is w( ).

Figure 15 displays two sequences of delay transitions in the corner-point automaton; while both sequences depart from the same region and visit the same sequence of locations, the accumulated weight evolves very differently along the two sequences-which explains why we have to refine regions. The corner-point automaton enjoys the following properties: if there is a run from some location to some location with total weight m in a given weighted timed automaton, then there is a run from ( , 0, 0) to some ( , R, c) with total weight at most m in the corresponding corner-point automaton; in other words, running through corner-points is always better when trying to optimize the value of the total weight. Conversely, for any positive ε, if there is a run from ( , 0, 0) to some ( , R, c) with weight m in the corner-point automaton, then there is a run in the original weighted timed automaton from (with initial valuation 0) to , with total weight at most m + ε.

This statement can be extended in various ways, so as to handle optimization of the ratio between two variables along finite or infinite runs. In the end: Theorem 20 ( [START_REF] Bouyer | Staying alive as cheaply as possible[END_REF]). The optimal-reachability and the optimal-ratio problems are PSPACE-complete.

Other related problems have been considered in the literature, such as conditional optimal reachability on multi-weighted timed automata [123]. The aim in this setting is to minimize the value of one variable under some conditions on the other variables. We refer to [123], where the problem is shown to be decidable.

Weighted Temporal Logics

Unfortunately, the encouraging results above do not extend to richer properties that could be expressed in weighted extensions of classical temporal logics4 . While this is not surprising for linear-time temporal logics (as these logics are already mostly undecidable in the timed setting), this also holds for weighted extensions of CTL, be it with modalities decorated with weight constraints (writing E♦ ≤10 T to express that T can be reached within total cost less than 10), or with explicit constraints as atomic formulas (writing E♦ (T ∧ c ≤ 10) to express the same property) [START_REF] Bouyer | Improved undecidability results on weighted timed automata[END_REF][START_REF] Brihaye | Model-checking for weighted timed automata[END_REF]. Undecidability can be proved by encoding the halting problem for a two-counter machine, where each counter is encoded by a clock of the timed automaton. The central trick in the reduction is the ability to multiply the value of a clock by some constant (while preserving the value of the other clocks). This is achieved by the automaton depicted in Fig. 16, in which we enforce the condition that location T must be reachable from S with total cost exactly 1: indeed, the total cost accumulated from S to T is precisely 1 + 2x 0 -y 0 , where x 0 and y 0 are the values of clocks x and y in S. This provides us with a way of doubling the value of clock x, by letting clock y play the role of x afterwards. Using this module, it is easy to build a complete reduction involving four clocks, which can be further improved to only three clocks. Theorem 21 ([49, 63]). WCTL model checking is undecidable (on weighted timed automata with at least three clocks).

Notice that the standard restriction to non-punctual constraints in the logic does not help, as the above reduction can be carried out using only inequality constraints. One way of recovering decidability is to restrict to one-clock weighted timed automata. These automata enjoy several special properties which allow us to prove that refining regions to a small granularity (in O(C -h(ϕ) ) where C is the maximal rate in the automaton and h(ϕ) is the temporal height of the formula being checked) provides a correct finite-state abstraction on which ϕ can be checked. It follows:

Theorem 22 ( [START_REF] Bouyer | Model checking oneclock priced timed automata[END_REF]). WCTL model checking is PSPACE-complete on one-clock weighted timed automata.

Energy Constraints

Recently, weighted timed automata have been pushed one step closer to hybrid automata, with the introduction of energy constraints [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Chakrabarti | Resource interfaces[END_REF]. These constraints aim at modeling, for example, autonomous robots, which often must take care of their battery charge level, and ensure that they never run out of energy. This is modeled with weighted timed automata, with the constraint that the accumulated value of the variable must never drop below 0 (or any lower bound). The same problem can of course be considered with an additional upper-bound constraint. Notice that this is a departure from the motto that the cost variable is an observer. Figure 17 displays an example of a weighted timed automaton, together with the evolution of the variable along one particular run. This corresponds to a feasible (prefix of a) run, as the variable remains between the lower bound L and upper bound U . Only a few results have been obtained so far. Let us begin with the untimed case [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF]: for lower-bound constraints, the problem still amounts to optimizing the accumulated cost, with the extra energy constraint. In that setting, the Bellman-Ford algorithm can be used to compute the maximal accumulated cost that can be achieved from the initial state, with the extra energy constraint. This provides a polynomial-time algorithm for solving reachability under lower-bound constraints. In case we also have an upper-bound constraint, the problem can be solved in exponential time by augmenting the state space with the explicit value of the variable. In the timed setting, the only known positive results concern one-clock weighted timed automata under lowerbound constraints [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF]. The central technique is the computation of an optimal schedule through a finite linear automaton (i.e., visiting all its locations with a fixed, linear order), such as the one depicted in Fig. 18. Notice that along such runs, we allow lower-bound constraints (written ≥ b i ) on each transition. Along such a path, one can prove that the optimal policy is to spend no time in a location r i if

r i-1 r i p i-1 ≥ b i-1 r i+1 p i ≥ b i
• either r i-1 > r i (in which case it is more profitable to spend time in location r i-1 ); • or r i+1 ≥ r i and b i-1 + p i-1 ≥ b i (in which case it is possible to directly jump to the more profitable location r i+1 ).

If any of these conditions is fulfilled, location r i can be dropped, and replaced by a transition from r i-1 to r i+1 with weight p i-1 + p i+1 and cost-constraint

≥ max(b i-1 , b i -p i-1
). This provides us with a linear automaton along which the rates are increasing. The optimal policy along such a path can be proved to be to exit a location as soon as the cost constraint ≥ b i is fulfilled. This gives a way of computing the optimal achievable energy level at the end of the path as a function of the initial credit. This extends to one-clock automata by composing such functions. In the end:

Theorem 23 ( [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF]). Optimal reachability is decidable in one-clock weighted timed automata under lower-bound constraints.

Unfortunately, this algorithm does not extend to n-clock automata: indeed, one can easily come up with a small module to increase or decrease the value of the cost variable by the value of a clock (see Fig. 16), thus providing a way of checking linear constraints between several clocks. As a consequence: Theorem 24 ( [START_REF] Bouyer | Lower-bound constrained runs in weighted timed automata[END_REF]). Optimal reachability is undecidable in four-clock weighted timed automata under lower-bound constraints.

Weighted timed automata under energy constraints are a very recent and active topic with many open problems. Several directions are currently being explored, such as the extension to exponential variables, where the variable follows the differential equation dp/dt = w( ) • p, or the inclusion of imprecisions in clock values or variable growth.

Timed Games

Games provide a nice framework for modeling and reasoning about the interactions between various agents (a reactive system and its environment, several components, etc.). We refer to Chap. 25gamesynth for details about games and their use for synthesizing correct models.

We consider two-player timed games, in which transitions are partitioned into controllable and uncontrollable (i.e., under the control of an environment).

The problem is then to synthesize a strategy telling when to take which (enabled) controllable transitions in order that a given objective is guaranteed regardless of the behavior of the environment. Definition 6. A timed game is a tuple G = (L, 0 , C, Σ c , Σ u , I, E) with Σ c ∩ Σ u = ∅ for which the tuple A G = (L, 0 , C, Σ = Σ c ∪ Σ u , I, E) is a timed automaton. We require this automaton to be deterministic (so that from any state, an action in Σ corresponds to a unique transition). Edges with actions in Σ c are said to be controllable, those with actions in Σ u are uncontrollable.

We shall again assume a set F of accepting locations to be given for the rest of this section. A strategy in a timed game G provides instructions as to which controllable edge to take, or whether to wait, in a given state. Hence it is a mapping σ from finite runs of the underlying timed automaton A G to Σ c ∪ {δ}, where δ / ∈ Σ, such that for any run ρ

= ( 0 , v 0 ) → • • • → ( k , v k ), • if σ(ρ) = δ, then ( , v) d -→ ( , v + d
) is a transition in A G for some d > 0, and

• if σ(ρ) = a, then ( , v) a -→ ( , v ) is a transition in A G .
An outcome of a strategy is any run which adheres to its instructions. Such an outcome is said to be maximal if it stops in an accepting location, or if no controllable actions are available at its end. An underlying assumption is that uncontrollable actions cannot be forced, hence a maximal outcome which does not end in a final location may "get stuck" in a non-final location. The aim of reachability games is to find strategies all of whose maximal outcomes end in an accepting location; the aim of safety games is to find strategies all of whose (not necessarily maximal) outcomes avoid accepting locations: Definition 7. A strategy is said to be winning for the reachability game if any of its maximal outcomes is an accepting run. It is said to be winning for the safety game if none of its outcomes are accepting. x ≤ 1 c 1

x < 1 u 3 c 3

x > 1 u 1 x ≥ 2 c 2

x < 1, u 2 , x := 0

x ≤ 1, c 4 Fig. 19 A timed game with one clock. Controllable edges (with actions from Σc) are solid, uncontrollable edges (with actions from Σu) are dashed Example 5. Figure 19 provides a simple example of a timed game. Here, Σ c = {c 1 , c 2 , c 3 , c 4 } and Σ 2 = {u 1 , u 2 , u 3 }, and the controllable edges are drawn with solid lines, the uncontrollable ones with dashed lines. The following memoryless strategy is winning for the reachability game:

σ( 1 , v) = δ if v(x) = 1 c 1 if v(x) = 1 σ( 2 , v) = δ if v(x) < 2 c 2 if v(x) ≥ 2 σ( 3 , v) = δ if v(x) < 1 c 3 if v(x) ≥ 1 σ( 4 , v) = δ if v(x) = 1 c 4 if v(x) = 1
Theorem 25 ([25, 26, 65, 128]). The (time-optimal) reachability and safety games are decidable for timed games. They are EXPTIME-complete.

A key ingredient in the proof of the above theorem is the fact that for reachability as well as safety games, it is sufficient to consider memoryless strategies, which only observe the last configuration of a run. This is not the case for other, more subtle, control objectives (e.g., counting properties modulo some N ) as well as for the synthesis of winning strategies under partial observability. The other ingredient is the region abstraction: if there is a winning strategy, then there is one that only depends on the current region. This provides an exponential-time algorithm, which can be proved to be optimal.

A problem with the above approach is that the safety game can be won by preventing time from diverging. In order to rule out such behaviors, a solution was proposed in [START_REF] Luca De Alfaro | The element of surprise in timed games[END_REF]; it uses a more symmetric presentation of games, in which both players have a strategy which proposes at the same time the amount of time this player wants to delay, and the transition she wants to take afterwards. At each step, the player with the shortest delay is chosen and her choice is performed. With this definition, if time converges along an outcome, then the player(s) who have applied their choices infinitely many times must have proposed converging sequences of delays. By adding a fairness requirement to the winning condition, we can declare this kind of behavior losing. Deciding the existence of winning strategies for reachability and safety objectives remains EXPTIME-complete in this context.

The field of timed games is a very active research area. From the regionbased decidability results, efficient on-the-fly algorithms have been developed [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF]148] and implemented in UppAal. In [START_REF] Cassez | Timed control with observation based and stuttering invariant strategies[END_REF] these algorithms have been extended to timed games under partial observability. Research has also been conducted towards the synthesis of optimal winning strategies for reachability games on weighted timed games. In [START_REF] Alur | Optimal reachability for weighted timed games[END_REF][START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF] computability of optimal strategies is shown under a certain condition of strong cost non-Zenoness, requiring that the total weight diverges at a given minimum rate per time. Later undecidability results [START_REF] Bouyer | Improved undecidability results on weighted timed automata[END_REF][START_REF] Brihaye | On optimal timed strategies[END_REF] show that for weighted timed games with three or more clocks, this condition (or a similar one) is necessary. It is proved in [START_REF] Bouyer | Almost optimal strategies in one-clock priced timed automata[END_REF] that optimal reachability strategies are computable for one-clock weighted timed games, though there is an unsettled (large) gap between the known lower bound complexity P and an upper bound of 3-EXPTIME, which was recently lowered to EXPTIME [START_REF] Dueholm Hansen | A faster algorithm for solving one-clock priced timed games[END_REF]142].

We conclude this section by illustrating how timed games can be used to decide timed bisimilarity of two states of a timed automaton. This provides a simple proof of Theorem 4, which we explain on a small example: consider the states of Fig. 20. That two states (p, v) and (q, w) (where v and w are two valuations of the same set of clocks C) are timed bisimilar means that any transition from either state can be mimicked from the other one, ending up in states that are again bisimilar. We can see this as a game on the product of two copies of the automaton (see Fig. 21): from the joint state ((p, q), (v, w)), the first player chooses to apply one transition from one of the states (p, v) and (q, w), and the second player has to respond (immediately) with an appropriate move from the other state. The second player has a strategy to always avoid the Bad state if, and only if, the starting states are timed bisimilar. This provides an exponential-time algorithm for checking timed bisimilarity [START_REF] Alur | The observational power of clocks[END_REF].

10 Ongoing and Future Challenges

In this chapter, we have surveyed timed automata and the theoretical developments that have led to their being widely accepted as a model for modeling and reasoning about real-time systems. Many developments are still ongoing: we briefly list here some important topics which we think are among the important avenues to be explored during the coming years:

• Robustness (in the timed setting) and implementability [START_REF] De Wulf | Robust safety of timed automata[END_REF][START_REF] Gupta | Robust timed automata[END_REF]139,143] address the problem of reconciling the semantics of timed automata (with real-valued clocks) with the models they represent (which usually run at a finite frequency). • Statistical model checking consists in checking several runs of the model against a given property, and compute statistics to get an estimate of the correctness of the model. The approach has recently been studied and implemented in the setting of stochastic timed automata, where it provides interesting results, even for problems that are otherwise undecidable [START_REF] David | Time for statistical model checking of real-time systems[END_REF]. • Games on timed automata have received a lot of attention over the last ten years, as they are a convenient formalism for the automated synthesis of real-time systems. Recent extensions to non-zero-sum games [START_REF] Brenguier | Nash Equilibria in Concurrent Games -Application to Timed Games[END_REF]113],

where the players have their own objectives, open a rich and promising area of research for synthesizing complex systems.

Index

Fig. 1

 1 Fig. 1 A timed automaton

Fig. 5

 5 Fig. 5 Region automaton for (P 1 R 1 ) f 1

Fig. 6

 6 Fig. 6 Four timed automata A, X, U and D

Fig. 10

 10 Fig. 10 An event-clock automaton

Fig. 11

 11 Fig. 11 Encoding computations of Turing machines as timed words

Fig. 14

 14 Fig. 14 Example of a weighted timed automaton

Fig. 15

 15 Fig. 15 Two different runs in the corner-point abstraction

Fig. 16

 16 Fig. 16 Module for testing whether y = 2x

Fig. 17

 17 Fig. 17 A weighted timed automaton under energy constraints

  Fig. 17 A weighted timed automaton under energy constraints

Fig. 18 A

 18 Fig. 18 A linear weighted automaton

Fig. 20

 20 Fig. 20 Two states of a timed automaton

2 ∧Fig. 21

 221 Fig. 21 Timed bisimilarity as a timed game

The original definition of timed automata[START_REF] Alur | A theory of timed automata[END_REF] did not contain invariants in locations, but had Büchi conditions to enforce liveness. Invariants were added by[103]. Several other convenient extensions have been introduced since then, which we discuss in Sect. 3.2.

y 1 =2,abort 1 ,y 1 :=0 y 1 >1,start 1 ,y 1 :=0 y 1 =2,abort 1 ,y 1 :=0 acquire 1 , x 1 :=0 acquire 1 , x 1 :=0 x 1 ≤1,release 1 , y 1 :=0 x 1 ≤1, release 1 ,y 1 :=0 x 1 ≤1, release 2 , y 2 :=0 y 2 >1, start 2 , y 2 :=0 acquire 2 , x 1 :=0 acquire 2 , x 1 :=0 x 1 ≤1, release 1 , y 1 :=0 x 1 ≤1, release 1 , y 1 :=0x 1 ≤1,release 1 ,y 1 :=0 y 1 >1,start 1 ,y 1 :=0

For d ∈ R ≥0 we write d and d for the integral and fractional parts of d, i.e., d = d + d .

Notice that the labeling in the second location is a clock invariant (enforcing that no time will elapse in that location). The rate of p is not given in that location as no time will elapse anyway.

Even if we restrict to nonnegative weights, which is what we assume in this subsection on temporal logics.

Acknowledgement

We thank the reviewers for their numerous comments, remarks and additional references, which greatly helped us improve this chapter.