Uli Fahrenberg

Kim G Larsen

Axel Legay

Claus Thrane

Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems

Keywords: Timed automaton, region, zone, reachability, bisimilarity, priced timed automaton, weighted timed automaton, optimal reachability, optimal infinite run, conditional optimality, timed game, winning strategy

. The paper gives comprehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on associated decision problems related to model checking, equivalence checking, optimal scheduling, the existence of winning strategies, and then statistical model checking.

Introduction

The model of timed automata, introduced by Alur and Dill [START_REF] Alur | Automata for modeling real-time systems[END_REF][START_REF] Alur | A theory of timed automata[END_REF], has by now established itself as a classical formalism for describing the behaviour of real-time systems. A number of important algorithmic problems has been shown decidable for it, including reachability, model checking and several behavioural equivalences and preorders.

By now, real-time model checking tools such as Uppaal [START_REF] Behrmann | A tutorial on Uppaal[END_REF][START_REF] Kim | Uppaal in a nutshell[END_REF] and Kronos [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF] are based on the timed automata formalism and on the substantial body of research on this model that has been targeted towards transforming the early results into practically efficient algorithms -e.g. [START_REF] Behrmann | Uppaal implementation secrets[END_REF][START_REF] Behrmann | Lower and upper bounds in zone based abstractions of timed automata[END_REF][START_REF] Behrmann | Distributing timed model checking -how the search order matters[END_REF][START_REF] Behrmann | To store or not to store[END_REF] -and data structures -e.g. [START_REF] Behrmann | Efficient timed reachability analysis using clock difference diagrams[END_REF][START_REF] Kim | Efficient verification of real-time systems: compact data structure and state-space reduction[END_REF][START_REF] Kim | Clock difference diagrams[END_REF].

The maturity of a tool like Uppaal is witnessed by the numerous applications -e.g. [START_REF] D'argenio | The bounded retransmission protocol must be on time! In Ed Brinksma[END_REF][START_REF] Juhan | Memory arbiter synthesis and verification for a radar memory interface card[END_REF][START_REF] Hendriks | Model checking the time to reach agreement[END_REF][START_REF] Jensen | Scaling up Uppaal automatic verification of real-time systems using compositionality and abstraction[END_REF][START_REF] Lamport | Real-time model checking is really simple[END_REF][START_REF] Kim | Testing real-time embedded software using Uppaal-TRON: an industrial case study[END_REF][START_REF] Kim | Computer Aided Verification, 3rd International Workshop, CAV '91[END_REF][START_REF] Lindahl | Formal design and analysis of a gear controller[END_REF] -to the verification of industrial case-studies spanning real-time controllers and real-time communication protocols. More recently, model-checking tools in general and Uppaal in particular have been ap-plied to solve realistic scheduling problems by a reformulation as reachability problems -e.g. [START_REF] Abdeddaïm | Task graph scheduling using timed automata[END_REF][START_REF] Fehnker | Scheduling a steel plant with timed automata[END_REF][START_REF] Hune | Guided synthesis of control programs using Uppaal[END_REF][START_REF] Maler | Timed automata as an underlying model for planning and scheduling[END_REF].

Aiming at providing methods for performance analysis, a recent extension of timed automata is that of priced or 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], which makes it possible to formulate and solve optimal scheduling problems. Surprisingly, a number of properties have been shown to be decidable for this formalism [START_REF] Alur | Optimal paths in weighted timed automata[END_REF][START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF][START_REF] Bouyer | Staying alive as cheaply as possible[END_REF][START_REF] Fahrenberg | Discount-optimal infinite runs in priced timed automata[END_REF][START_REF] Kim | Optimal conditional reachability for multipriced timed automata[END_REF]. The recently developed Uppaal-Cora tool provides an efficient tool for solving cost-optimal reachability problems [START_REF] Kim | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF] and has been applied successfully to a number of optimal scheduling problems, e.g. [START_REF] Behrmann | Production scheduling by reachability analysis -a case study[END_REF][START_REF] Behrmann | Optimal scheduling using priced timed automata[END_REF][START_REF] Michael | Semantics and verification of a language for modelling hardware architectures[END_REF].

Most recently, substantial efforts have been made on the automatic synthesis of (correct-by-construction) controllers from timed games for given control objectives. From early decidability results [START_REF] Asarin | Symbolic controller synthesis for discrete and timed systems[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems (an extended abstract)[END_REF] the effort has lead to efficient on-thefly algorithms [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF][START_REF] Tripakis | On-the-fly controller synthesis for discrete and densetime systems[END_REF] with the newest of the Uppaal toolset, Uppaal-Tiga [START_REF] Behrmann | Uppaal-Tiga: Time for playing games![END_REF], Uppaal-SMC [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF][START_REF] David | Time for statistical model checking of real-time systems[END_REF], providing an efficient tool implementation with industrial applications emerging, e.g. [START_REF] Jakob Jessen | Guided controller synthesis for climate controller using Uppaal-Tiga[END_REF].

This survey paper aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the land and language of timed automata. The article gives comprehensive definitions of timed automata, weighted timed automata, and timed games and highlights a number of results on associated decision problems related to model checking, equivalence checking, optimal scheduling, the existence of winning strategies, and statistical model checking. The intention is that the paper should provide an easy-to-access collection of important results and overview of the field to anyone interested.

The authors would like to thank the students of the Marktoberdorf and Quantitative Model Checking PhD schools for their useful comments and help in weeding out a number of errors in the first two editions of this survey [START_REF] Fahrenberg | Verification, performance analysis and controller synthesis for real-time systems[END_REF][START_REF] Fahrenberg | Model-based verification and analysis for real-time systems[END_REF], as well as an anonymous reviewer who provided many useful remarks for the invited paper [START_REF] Fahrenberg | Verification, performance analysis and controller synthesis for real-time systems[END_REF] at FSEN 2009.

Timed automata

In this section we review the notion of timed automata introduced by Alur and Dill [START_REF] Alur | Automata for modeling real-time systems[END_REF][START_REF] Alur | A theory of timed automata[END_REF] as a formalism for describing the behaviour of real-time systems. We review the syntax and semantics and highlight the, by now classical, region construction underlying the decidability of several associated problems.

Here we illustrate how regions are applied in showing decidability of reachability and timed and untimed (bi)similarity. However, the notion of region does not provide the means for efficient tool implementations. The verification engine of Uppaal instead applies so-called zones, which are convex unions of regions. We give a brief account of zones as well as their efficient representation and manipulation using difference-bound matrices. x := 0 press?

Syntax and semantics

x ≤ 3

x := 0 press?

x > 3

x := 0

x = 100

x := 0 press?

x := 0

x = 100 x := 0 Figure 1.: A light switch modelled as a timed automaton.

ϕ ::= x ⊲⊳ k | ϕ 1 ∧ ϕ 2 (x ∈ C, k ∈ ), ⊲⊳ ∈ {≤, <, ≥, >}).
The set Φ + (C) of extended clock constraints ϕ is defined by the grammar

ϕ ::= x ⊲⊳ k | x -y ⊲⊳ k | ϕ 1 ∧ ϕ 2 (x, y ∈ C, k ∈ ), ⊲⊳ ∈ {≤, <, ≥, >}).
Remark 2.2. The clock constraints in Φ(C) above are also called diagonal-free clock constraints, and the additional ones in Φ + (C) are called diagonal. We restrict ourselves to diagonal-free clock constraints here; see Remark 2.44 for one reason. For additional modelling power, timed automata with diagonal constraints can be used, as it is shown in [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF] that any such automaton can be converted to a diagonal-free one; however the conversion may lead to an exponential blow-up. Definition 2.3. A timed automaton is a tuple (L, ℓ 0 , F, C, Σ, I, E) consisting of a finite set L of locations, an initial location ℓ 0 ∈ L, a set F ⊆ L of final locations, a finite set C of clocks, a finite set Σ of actions, a location invariants mapping I : L → Φ(C), and a set

E ⊆ L × Φ(C) × Σ × 2 C × L of edges.
Here 2 C denotes the set of subsets (i.e. the power set) of C. We shall write ℓ ϕ,a,r ---→ ℓ ′ for an edge (ℓ, ϕ, a, r, ℓ ′ ) ∈ E. In figures, resets are written as assignment to zero, e.g. x := 0.

Example 2.1. Figure 1 provides a timed automaton model of an intelligent light switch. Starting in the "Off" state, a press of the button turns the light on, and it remains in this state for 100 time units (i.e. until clock x = 100), at which time the light turns off again. During this time, an additional press resets the clock x and prolongs the time in the state by 100 time units. Pressing the button twice, with at most three time units between the presses, triggers a special bright light.

ϕ 1 ∧ ϕ 2 = ϕ 1 ∩ ϕ 2 .
We shall write v |= ϕ instead of v ∈ ϕ .

Definition 2.6. The semantics of a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E) is the transition system A = (S, s 0 , Σ ∪ | ≥0 , T = T s ∪ T d ) given as follows:

S = (ℓ, v) ∈ L × | C ≥0 v |= I(ℓ) s 0 = (ℓ 0 , v 0 ) T s = (ℓ, v) a -→ (ℓ ′ , v ′ ) ∃ℓ ϕ,a,r ---→ ℓ ′ ∈ E : v |= ϕ, v ′ = v[r] T d = (ℓ, v) d -→ (ℓ, v + d) ∀d ′ ∈ [0, d] : v + d ′ |= I(ℓ)
Remark 2.7. The transition system A from above is an example of what is known as a timed transition system, i.e. a transition system where the label set includes | ≥0 as a subset and which satisfies certain additivity and time determinacy properties. We refer to [START_REF] Aceto | Reactive Systems: Modeling, Specification and Verification[END_REF] for a more in-depth treatment. Also note that the semantics A contains no information about final states (derived from the final locations in F ); this is mostly for notational convenience.

Definition 2.8. A (finite) run of a timed automaton

A = (L, ℓ 0 , F, C, Σ, I, E) is a finite path ρ = (ℓ 0 , v 0 ) → • • • → (ℓ k , v k ) in A . It is said to be accepting if ℓ k ∈ F . ℓ 0 ℓ 1 a y ≤ 2 y := 0 b x ≤ 2 x := 0 c x ≥ 4 ∧ y ≤ 2

Reachability

We are concerned with the following problem: Given a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E), is any of the locations in F reachable? We shall later define the timed language generated by a timed automaton and see that this reachability problem is equivalent to emptiness checking: Is the timed language generated by A non-empty?

Example 2.2 (cf. [START_REF] Aceto | Reactive Systems: Modeling, Specification and Verification[END_REF]Ex. 11.7]). Figure 2 shows a timed automaton A with two clocks and a final location ℓ 1 . To ask whether ℓ 1 is reachable amounts for this automaton to the question whether there is a finite sequence of a-and b-transitions from ℓ 0 which brings clock values into accordance with the guard x ≥ 4 ∧ y ≤ 2 on the edge leading to ℓ 1 .

An immediate obstacle to reachability checking is the infinity of the state space of A. In general, the transition system A has uncountably many states, hence straight-forward reachability algorithms do not work for us.

Notation 2.9. The derived transition relations in a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E) are defined as follows: For (ℓ, v), (ℓ ′ , v ′ ) states in A , we say that

• (ℓ, v) δ -→ (ℓ ′ , v ′ ) if (ℓ, v) d -→ (ℓ ′ , v ′ ) in A for some d > 0, • (ℓ, v) α -→ (ℓ ′ , v ′ ) if (ℓ, v) a -→ (ℓ ′ , v ′ ) in A
for some a ∈ Σ, and

• (ℓ, v) (ℓ ′ , v ′ ) if (ℓ, v) ( δ -→ ∪ α -→) * (ℓ ′ , v ′ ).
Definition 2.10. The set of reachable locations in a timed automaton

A = (L, ℓ 0 , F, C, Σ, I, E) is Reach(A) = ℓ ∈ L ∃v : C → | ≥0 : (ℓ 0 , v 0 ) (ℓ, v) .
Hence we can now state the reachability problem as follows:

Problem 2.1 (Reachability). Given a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E), is Reach(A) ∩ F = ∅ ? Definition 2.11. Let A = (L, ℓ 0 , F, C, Σ, I, E) be a timed automaton. A relation R ⊆ L × | C ≥0 × L × | C ≥0 is a time-abstracted simulation provided that for all (ℓ 1 , v 1 ) R (ℓ 2 , v 2 ), • for all (ℓ 1 , v 1 ) δ -→ (ℓ ′ 1 , v ′ 1 ) there exists some (ℓ ′ 2 , v ′ 2 ) such that (ℓ ′ 1 , v ′ 1 ) R (ℓ ′ 2 , v ′ 2 ) and (ℓ 2 , v 2 ) δ -→ (ℓ ′ 2 , v ′ 2 )
, and

• for all a ∈ Σ and (ℓ 1 , v 1 ) a -→ (ℓ ′ 1 , v ′ 1 ), there exists some (ℓ ′ 2 , v ′ 2 ) such that (ℓ ′ 1 , v ′ 1 ) R (ℓ ′ 2 , v ′ 2 ) and (ℓ 2 , v 2 ) a -→ (ℓ ′ 2 , v ′ 2 ). R is said to be F -sensitive if additionally, (ℓ 1 , v 1 ) R (ℓ 2 , v 2 ) implies that ℓ 1 ∈ F if and only if ℓ 2 ∈ F . A time-
abstracted bisimulation is a time-abstracted simulation which is also symmetric; we write (ℓ 1 , v 1 ) ≈ (ℓ 2 , v 2 ) whenever (ℓ 1 , v 1 ) R (ℓ 2 , v 2 ) for a time-abstracted bisimulation R.

Note that ≈ is itself a time-abstracted bisimulation, which is easily shown to be an equivalence relation and hence symmetric, reflexive and transitive. Observe also that a time-abstracted (bi)simulation on A is the same as a standard (bi)simulation on the transition system derived from A with transitions δ -→ and a -→. Likewise, the quotient introduced below is just the standard bisimulation quotient of this derived transition system. Definition 2.12. Let A = (L, ℓ 0 , F, C, Σ, I, E) be a timed automaton and R ⊆

L × | C ≥0 × L × | C
≥0 a time-abstracted bisimulation which is also an equivalence.

The

quotient of A = (S, s 0 , Σ ∪ | ≥0 , T ) with respect to R is the transition system A R = (S R , s 0 R , Σ ∪ {δ}, T R ) given by S R = S/R, s 0 R = [s 0 ] R ,

and with transitions

• π δ -→ π ′ whenever (ℓ, v) δ -→ (ℓ ′ , v ′ ) for some (ℓ, v) ∈ π, (ℓ ′ , v ′ ) ∈ π ′ , and • π a -→ π ′ whenever (ℓ, v) a -→ (ℓ ′ , v ′ ) for some (ℓ, v) ∈ π, (ℓ ′ , v ′ ) ∈ π ′ .
The following proposition expresses that F -sensitive quotients are sound and complete with respect to reachability.

Proposition 2.13 ([5]). Let

A = (L, ℓ 0 , F, C, Σ, I, E) be a timed automaton, R ⊆ L × | C ≥0 × L × | C
≥0 an F -sensitive time-abstracted bisimulation and ℓ ∈ F . Then ℓ ∈ Reach(A) if and only if there is a reachable state π in A R and v :

C → | ≥0 such that (ℓ, v) ∈ π.
Example 2.2 (continued). We shall now try to construct, in a naïve way, a timeabstracted bisimulation R for the timed automaton A from Figure 2 which is as coarse as possible. Note first that we cannot have (ℓ

0 , v) R (ℓ 1 , v ′ ) for any v, v ′ : C → | ≥0 because ℓ 1 ∈ F and ℓ 0 / ∈ F .
On the other hand it is easy to see that we can let (ℓ 1 , v) R (ℓ 1 , v ′ ) for all v, v ′ : C → | ≥0 , which leaves us with constructing R on the states involving ℓ 0 . We handle switch transitions α -→ first: If v, v ′ : C → | ≥0 are such that v(y) ≤ 2 and v ′ (y) > 2, the state (ℓ 0 , v) has an a-transition available while the state (ℓ 0 , v ′ ) has not, hence these cannot be related in R. Similarly we have to distinguish states (ℓ 0 , v) from states (ℓ 0 , v ′ ) where v(x) ≤ 2 and v ′ (x) > 2 because of b-transitions, and states (ℓ 0 , v) from states (ℓ 0 , v ′ ) where v(x) < 4 and v ′ (x) ≥ 4 because of c-transitions. Altogether this gives the five classes depicted to the left of Figure 3, where the shading indicates to which class the boundary belongs, and we have written the set of available actions in the classes. When also taking delay transitions δ -→ into account, one has to partition the state space further: From a valuation v in the class marked {a, b} in the left of the figure, a valuation in the class marked {a} can only be reached by a delay transition if v(y) < v(x); likewise, from the {a} class, the {a, c} class can only be reached if v(y) ≤ v(x) -2. Hence these two classes need to be partitioned as shown to the right of Figure 3.

It can easily be shown that no further partitioning is needed, thus we have defined the coarsest time-abstracted bisimulation relation for A, altogether with eight equivalence classes.

Regions

Motivated by the construction in the example above, we now introduce a timeabstracted bisimulation with a finite quotient. To ensure finiteness, we need the maximal constants to which respective clocks are compared in the invariants and guards of a given timed automaton. These may be defined as follows.

Definition 2.14. For a finite set C of clocks, the maximal constant mapping c max : C → ) Φ(C) is defined inductively as follows:

c max (x)(y ⊲⊳ k) = k if y = x 0 if y = x c max (x)(ϕ 1 ∧ ϕ 2 ) = max c(x)(ϕ 1 ), c(x)(ϕ 2 )
For a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E), the maximal constant mapping

is c A : C → ) defined by c A (x) = max c max (x)(I(ℓ)), c max (x)(ϕ) ℓ ∈ L, ℓ ϕ,a,r ---→ ℓ ′ ∈ E .
C → | ≥0 are said to be region equivalent, denoted v ∼ = v ′ , if • ⌊v(x)⌋ = ⌊v ′ (x)⌋ or v(x), v ′ (x) > c A (x)
, for all x ∈ C, and • v(x) = 0 iff v ′ (x) = 0, for all x ∈ C, and

• v(x) ≤ v(y) iff v ′ (x) ≤ v ′ (y) for all x, y ∈ C.
Proposition 2.17 ([5]). For a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E), the equivalence relation ∼ = defined on states of A by

(ℓ, v) ∼ = (ℓ ′ , v ′ ) if ℓ = ℓ ′ and v ∼ = v ′ is an F -sensitive time-abstracted bisimulation. The quotient A ∼ = is finite.
The equivalence classes of valuations of A with respect to ∼ = are called regions, and the quotient A ∼ = is called the region automaton associated with A.

Proposition 2.18 ([9]). The number of regions for a timed automaton A with a set C of n clocks is bounded above by Propositions 2.13 and 2.17 together now give the decidability part of the theorem below; for PSPACE-completeness see [START_REF] Alur | Model-checking for real-time systems[END_REF][START_REF] Courcoubetis | Minimum and maximum delay problems in real-time systems[END_REF].

n! • 2 n • x∈C (2c A (x) + 2).
Theorem 2.19. The reachability problem for timed automata is PSPACE-complete.

Behavioural refinement relations

We have already introduced time-abstracted simulations and bisimulations in Definition 2.11. As a corollary of Proposition 2.17, these are decidable:

Theorem 2.20. Time-abstracted simulation and bisimulation are decidable for timed automata.

Proof: 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.

The following provides a time-sensitive variant of (bi)simulation.

Definition 2.21. Let A = (L, ℓ 0 , F, C, Σ, I, E) be a timed automaton. A relation

R ⊆ L × | C ≥0 × L × | C ≥0 is a timed simulation provided that for all (ℓ 1 , v 1 ) R (ℓ 2 , v 2 ), • for all (ℓ 1 , v 1 ) d -→ (ℓ ′ 1 , v ′ 1 ), d ∈ | ≥0 , there exists some (ℓ ′ 2 , v ′ 2 ) such that (ℓ ′ 1 , v ′ 1 ) R (ℓ ′ 2 , v ′ 2 ) and (ℓ 2 , v 2 ) d -→ (ℓ ′ 2 , v ′ 2 )
, and

• for all (ℓ 1 , v 1 ) a -→ (ℓ ′ 1 , v ′ 1 ), a ∈ Σ, there exists some (ℓ ′ 2 , v ′ 2 ) such that (ℓ ′ 1 , v ′ 1 ) R (ℓ ′ 2 , v ′ 2 ) and (ℓ 2 , v 2 ) 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, which is easily shown to be an equivalence relation and hence transitive, reflexive and symmetric.

Definition 2.22. Two timed automata

A = (L A , ℓ A 0 , F A , C A , Σ A , I A , E A ) and B = (L B , ℓ B 0 , F B , C B , Σ B , I B , E B ) are said to be timed bisimilar, denoted A ∼ B, if (ℓ A 0 , v 0 ) ∼ (ℓ B 0 , v 0 ) in the disjoint-union transition system A ⊔ B .
Timed simulation of timed automata can be analogously defined. The following decidability result was established for parallel timed processes in [START_REF] Čerāns | Decidability of bisimulation equivalences for parallel timer processes[END_REF]; below we give a version of the proof which has been adapted for timed automata.

Theorem 2.23. Timed similarity and bisimilarity are decidable for timed automata.

Before the proof, we need a few auxiliary definitions and lemmas. The first is a product of timed transition systems which synchronizes on time, but not on actions: Definition 2.24. The independent product of the timed transition systems

A = (S A , s A 0 , Σ A ∪ | ≥0 , T A ), B = (S B , s B 0 , Σ B ∪ | ≥0 , T B ) associated with timed automata A, B is A × B = (S, s 0 , Σ A ∪ Σ B ∪ | ≥0 , T ) given by S = S A × S B s 0 = (s A 0 , s B 0 ) T = (p, q) a -→ (p ′ , q) a ∈ Σ, p a -→ p ′ ∈ T A ∪ (p, q) b - → (p, q ′ ) b ∈ Σ, q b - → q ′ ∈ T B ∪ (p, q) d -→ (p ′ , q ′ ) d ∈ | ≥0 , p d -→ p ′ ∈ T A , q d -→ q ′ ∈ T B
We need to extend region equivalence ∼ = to the independent product. Below, ⊕ denotes vector concatenation (direct sum); note that (p 1 , q 1 ) ∼ = (p 2 , q 2 ) is not the same as p 1 ∼ = p 2 and q 1 ∼ = q 2 , as fractional orderings x A ⊲⊳ x B , for x A ∈ C A , x B ∈ C B , have to be accounted for in the former, but not in the latter. Hence (p 1 , q 1 ) ∼ = (p 2 , q 2 ) implies p 1 ∼ = p 2 and q 1 ∼ = q 2 , but not vice-versa. Definition 2.25. For states p i = (ℓ pi , v pi ) in A and

q i = (ℓ qi , v qi ) in B for i = 1, 2, we say that (p 1 , q 1 ) ∼ = (p 2 , q 2 ) iff ℓ p1 = ℓ p2 ∧ ℓ q1 = ℓ q2 and v p1 ⊕ v q1 ∼ = v p2 ⊕ v q2 .
Note that the number of states in A × B ∼ = is finite, with an upper bound given by Proposition 2.18. Next we define transitions in

A × B ∼ = : Notation 2.26. Regions in A × B ∼ = will be denoted X, X ′ . The equivalence class of a pair (p, q) ∈ A × B is denoted [p, q]. Definition 2.27. For X, X ′ ∈ A × B ∼ = we say that • X a -→ ℓ X ′ for a ∈ Σ if for all (p, q) ∈ X there exists (p ′ , q) ∈ X ′ such that (p, q) a -→ (p ′ , q) in A × B , • X b - → r X ′ for b ∈ Σ if for all (p, q) ∈ X there exists (p, q ′ ) ∈ X ′ such that (p, q) b - → (p, q ′ ) in A × B , and • X δ -→ X ′ if for all (p, q) ∈ X there exists d ∈ | ≥0 and (p ′ , q ′ ) ∈ X ′ such that (p, q) d -→ (p ′ , q ′ ). Definition 2.28. A subset B ⊆ A × B ∼ = is a symbolic bisimulation provided that for all X ∈ B, • whenever X a -→ ℓ X ′ for some X ′ ∈ A × B ∼ = , then X ′ a -→ r X ′′ for some X ′′ ∈ B, • whenever X a -→ r X ′ for some X ′ ∈ A × B ∼ = , then X ′ a -→ ℓ X ′′ for some X ′′ ∈ B, and • whenever X δ -→ X ′ for some X ′ ∈ A × B ∼ = , then X ′ ∈ B.
Note that it is decidable whether A × B ∼ = admits a symbolic bisimulation. The following proposition finishes the proof of Theorem 2.23.

Proposition 2.29. The quotient A × B ∼ = admits a symbolic bisimulation if and only if A ∼ B.

Proof (cf. [START_REF] Čerāns | Decidability of bisimulation equivalences for parallel timer processes[END_REF]): For a given symbolic bisimulation

B ⊆ A × B ∼ = , the set R B = (p, q) [p, q] ∈ B ⊆ A × B is a timed bisimulation. For the other direction, one can construct a symbolic bisimulation from a timed bisimulation R ⊆ A × B by B R = [p, q] (p, q) ∈ R .

Language inclusion and equivalence

Similarly to the untimed setting, there is also a notion of language inclusion and equivalence for timed automata. We need to introduce the notion of timed trace first. Note that we restrict to finite timed traces here; similar results are available for infinite traces in timed automata with Büchi or Muller acceptance conditions, see [START_REF] Alur | A theory of timed automata[END_REF]. Definition 2.30. A timed trace over a finite set of actions Σ is a finite sequence ((t 1 , a 1 ), (t 2 , a 2 ), . . . , (t k , a k )), where a i ∈ Σ and t i ∈ | ≥0 for i = 1, . . . , k, and

t i < t i+1 for i = 1, . . . , k -1.
The set of all timed traces over Σ is denoted T Σ * . In a pair (t i , a i ), the number t i is called the time stamp of the action a i , i.e. the time at which event a i occurs.

Remark 2.31. Timed traces as defined above are also known as strongly monotonic timed traces, because of the assumption that no consecutive events occur at the same time. Weakly monotonic timed traces, i.e. with requirement t i ≤ t i+1 instead of t i < t i+1 , have also been considered, and there are some subtle differences between the two; see [START_REF] Ouaknine | Universality and language inclusion for open and closed timed automata[END_REF] for an important example. It is clear that L(A) = ∅ if and only if none of the locations in F is reachable, hence Theorem 2.19 provides us with the decidability result in the following theorem. Undecidability of universality was established in [START_REF] Alur | A theory of timed automata[END_REF]; we give an account of the proof below.

Definition 2.32. A timed trace ((t 1 , a 1 ), . . . , (t k , a k )) is accepted by a timed au- tomaton A = (L, ℓ 0 , F, C, Σ, I, E) if there is an accepting run (ℓ 0 , v 0 ) t1 -→ (ℓ 0 , v 0 + t 1 ) a1 -→ (ℓ 1 , v 1 ) t2-t1 ---→ • • • • • • a k-1 ---→ (ℓ k-1 , v k-1 ) t k -t k-1 -----→ (ℓ k-1 , v k-1 + t k -t k-1 ) a k -→ (ℓ k , v k ) in A. The timed language of A is L(A) = {τ ∈ T Σ * | τ accepted by A}.
Theorem 2.33. For a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E), deciding whether

L(A) = ∅ is PSPACE-complete. It is undecidable whether L(A) = T Σ * .
Proof: We show that the universality problem for a timed automata is undecidable by reduction from the Σ 1 1 -hard problem of deciding whether a given 2-counter machine M has a recurring computation.

Let the timed language L u be the set of timed traces encoding recurring computations of M . Observe that L u = ∅ if and only if M does not have such a computation. We then construct a timed automaton A u which accepts the complement of L u , i.e. L(A u ) = T Σ * \ L u . Hence the language of A u is universal if and only if M does not have a recurring computation.

Recall that a 2-counter, or Minsky, machine M is a finite sequence of labeled instructions {I 0 , • • • , I n } and counters x 1 and x 2 , with I i for 0 ≤ i ≤ n -1 on the form

I i : x c := x c + 1; goto I j or I i : if x c = 0 then goto I j else x c = x c -1; goto I k for c ∈ 1, 2
, with a special I n : Halt instruction which stops the computation.

The language L u is designed such that each I i and the counters x 1 and x 2 are represented by actions in Σ. A correctly encoded computation is represented by a timed trace where "instruction actions" occur at discrete intervals, while the state (values of x 1 and x 2 ) is encoded by occurrences of "counter actions" in-between instruction actions (e.g. if x i = 5 after instruction I j , then action x i occurs 5 times within the succeeding interval of length 1).

When counters are incremented (or decremented), one more (or less) such action occurs through the next interval, and increments and decrements are always from the right. Additionally we require corresponding counter actions to occur exactly with a time difference of 1, such that if x i occurs with time stamp a then also x i occurs with time stamp a + 1, unless x i is the rightmost x i action and I i at time stamp ⌊a⌋ is a decrement of x i . Figure 5 shows a increment of x 1 (from 4 to 5) using actions 1 and 2. We obtain A u as a disjunction of timed automata A 1 , . . . , A k where each A i violates some property of a (correctly encoded) timed trace in L u , either by accepting traces of incorrect format or inaccurate encodings of instructions.

Consider the instruction: (p): x 1 := x 1 +1 goto (q), incrementing x 1 and jumping to q. A correct encoding would be similar to the one depicted in Figure 5 where all 1's and 2's are matched one time unit later, but with an additional 1 action occurring. In order to accept all traces except this encoding we must consider all possible violations, i.e.

• not incrementing the counter (no change),

• decrementing the counter, • incrementing the counter more than once, • jumping to the wrong instruction, or • incrementing the wrong counter, and construct a timed automaton having exactly such traces.

Figure 6 shows the timed automaton accepting traces in which instruction p yields no change of x 1 .

Turning our attention to timed trace inclusion and equivalence, we note the following.

Proposition 2.34. Let A and B be timed automata. If A is timed simulated by B, then L(A) ⊆ L(B). If A and B are timed bisimilar, then L(A) = L(B).

By a standard argument, Theorem 2.33 implies undecidability of timed trace inclusion and equivalence, a result first shown in [START_REF] Alur | Automata for modeling real-time systems[END_REF].

Theorem 2.35. Timed trace inclusion and equivalence are undecidable for timed automata.

There is also a notion of untimed traces for timed automata.

Definition 2.36. The untiming of a set of timed traces L ⊆ T Σ * over a finite set of actions Σ is the set

U L = w = (a 1 , . . . , a k ) ∈ Σ * ∃t 1 , . . . , t k ∈ | ≥0 : ((t 1 , a 1 ), . . . , (t k , a k )) ∈ L .
Hence we have a notion of the set U L(A) of untimed language of a timed automaton A. One can also define an untime operation U for timed automata, forgetting about the timing information of a timed automaton and thus converting it to a finite automaton; note however that U L(A) L(U A) in general.

Lemma 2.37 ([9]). For A a timed automaton, U L(A) = L( A ∼ = ) provided that δ-transitions in A ∼ = are taken as silent.

As a corollary, sets of untimed traces accepted by timed automata are regular : Theorem 2.38 ([9]). For a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E), the set U L(A) ⊆ Σ * is regular. Accordingly, whether U L(A) = ∅ is decidable, and so is whether U L(A) = Σ * . Also untimed trace inclusion and equivalence are decidable.

Zones and difference-bound matrices

As shown in the above sections, regions provide a finite and elegant abstraction of the infinite state space of timed automata, enabling us to prove decidability of reachability, timed and untimed bisimilarity, untimed language equivalence and language emptiness.

Unfortunately, the number of states obtained from the region partitioning is extremely large. In particular, by Proposition 2.18 the number of regions is exponential in the number of clocks as well as in the maximal constants of the timed automaton. Efforts have been made in developing 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][START_REF] Kim | Clock difference diagrams[END_REF], using the notion of zones from Definition 2.5 on page 4 as a coarser and more compact representation of the state space.

An extended clock constraint over a finite set C may be represented using a directed weighted graph, where the nodes correspond to the elements of C together with an extra "zero" node x 0 , and an edge x i k -→ x j corresponds to a constraint x ix j ≤ k (if there is more than one upper bound on x ix 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 ix 0 ≤ k. Lower bounds on x ix j are represented as (possibly negative) upper bounds on x jx i , and strict bounds x ix 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 has been introduced in [START_REF] David | Timing assumptions and verification of finite-state concurrent systems[END_REF].

Example 2.3. Figure 7 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.

Zone-based reachability analysis of a timed automaton A uses symbolic states of the type (ℓ, Z), where ℓ is a location of A and Z is a zone, instead of the region-based symbolic states of Proposition 2.17. Definition 2.39. For a finite set C, Z ⊆ | C ≥0 , and r ⊆ C, define Example 2.3 (continued). Figure 8 shows two canonical representations of the difference-bound matrix for the zone Z of Figure 7. The left part illustrates the shortest-path closure of Z; on the right is the shortest-path reduction [START_REF] Kim | Efficient verification of real-time systems: compact data structure and state-space reduction[END_REF] of Z, essentially obtained by removing redundant edges from the shortest-path closure. The latter is useful for checking zone inclusion, see below.

• the delay of Z by Z ↑ = {v + d | v ∈ Z, d ∈ | ≥0 } and • the reset of Z under r by Z[r] = {v[r] | v ∈ Z}. 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 1 x 2 x 3
The zone automaton associated with a timed automaton is similar to the region automaton of Proposition 2.17, but uses zones for symbolic states instead of regions: Definition 2.41. The zone automaton associated with a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E) is the transition system A Z = (S, s 0 , Σ ∪ {δ}, T ) given as follows:

S = (ℓ, Z) ℓ ∈ L, Z ⊆ | C ≥0 zone s 0 = ℓ 0 , v 0 T = (ℓ, Z) δ ℓ, Z ↑ ∧ I(ℓ) ∪ (ℓ, Z) a ℓ ′ , (Z ∧ ϕ)[r] ∧ I(ℓ ′ ) ℓ ϕ,a,r ---→ ℓ ′ ∈ E
The analogue of Proposition 2.13 for zone automata is as follows:

Proposition 2.42 ([95]). A state (ℓ, v) in a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E) is reachable if and only if there is a zone Z ⊆ | C ≥0 for which v ∈ Z and such that (ℓ, Z) is reachable in A Z .
The zone automaton associated with a given timed automaton is infinite and hence unsuitable for reachability analysis. Finiteness can be enforced by employ-

x 0 x 1 x 2 x 3 3 7 5 3 2 4 -4 -2 -1 -2 2 1 x 0 x 1 x 2 x 3
: C → | ≥0 | ∃v ′ ∈ Z : v ∼ = v ′ }
The normalized zone automaton is defined in analogy to the zone automaton from above, and Proposition 2.42 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.

Remark 2.44. For timed automata on extended clock constraints, i.e. with diagonal constraints permitted, it can be shown [START_REF] Bengtsson | On clock difference constraints and termination in reacha-bility 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 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 reacha-bility analysis of timed automata[END_REF].

In addition to the efficient computation of symbolic successor states according to the relation, termination of reachability analysis requires that we can efficiently recognize whether the search algorithm has encountered a given symbolic state. Here it is crucial that there is an efficient way of deciding inclusion Z 1 ⊆ Z 2 between zones. Both the shortest-path-closure canonical form as well as the more space-economical shortest-path-reduced canonical form [START_REF] Kim | Efficient verification of real-time systems: compact data structure and state-space reduction[END_REF], cf. Example 2.3, allow for efficient inclusion checking.

In analogy to difference-bound matrices and overcoming some of their problems, the data structure called clock difference diagram has been proposed [START_REF] Kim | Clock difference diagrams[END_REF]. However, the design of efficient algorithms for delay and reset operations over that data structure is a challenging open problem; generally, the design of efficient data structures for computations with (unions of) zones is a field of active research, see [START_REF] Xavier Allamigeon | Inferring min and max invariants using max-plus polyhedra[END_REF][START_REF] Asarin | Data-structures for the verification of timed automata[END_REF][START_REF] Jesper | Difference decision diagrams[END_REF] for some examples.

Weighted timed automata

The notion of weighted -or priced -timed automata was introduced independently, at the very same conference, by Behrmann et.al. [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] and Alur et.al. [START_REF] Alur | Optimal paths in weighted timed automata[END_REF].

In these models both edges and locations can be decorated with weights, or prices, giving the cost of taking an action transition or the cost per time unit of delaying in a given location. The total cost of a trace is then simply the accumulated (or total) weight of its discrete and delay transitions. As a first result, the above two papers independently, and with quite different methods, showed that the problem of cost-optimal reachability is computable for weighted timed automata with non-negative weights. Later, optimal reachability for timed automata with several weight functions was considered in [START_REF] Kim | Optimal reachability for multi-priced timed automata[END_REF] as well as optimal infinite runs in [START_REF] Bouyer | Staying alive as cheaply as possible[END_REF][START_REF] Fahrenberg | Discount-optimal infinite runs in priced timed automata[END_REF].

w (ℓ, v) d -→ (ℓ, v + d) = d R(ℓ) w (ℓ, v) a -→ (ℓ ′ , v ′ ) = P ℓ ϕ,a,r ---→ ℓ ′ with v |= ϕ, v ′ = v[r]
We shall denote weighted edges and transitions by symbols e -→ w to illustrate an edge or a transition labeled e with weight w.

Optimal reachability

The objective of optimal reachability analysis is to find runs to a final location with the lowest total weight as defined below.

Example 3.1. Figure 9 shows a simple weighted timed automaton with final location ℓ 3 . Below we give a few examples of accepting runs, where we identify valuations v : {x, y} → | ≥0 with their values (v(x), v(y)). The total weights of the runs given here are 17 and 11; actually the second run is optimal in the sense of Problem 3.1 below:

(ℓ 1 , 0, 0) 3 -→ 12 (ℓ 1 , 3, 3) a -→ 1 (ℓ 2 , 0, 3) c -→ 4 (ℓ 3 , 0, 3) (ℓ 1 , 0, 0) a -→ 1 (ℓ 2 , 0, 0) 3 -→ 6 (ℓ 2 , 3, 3) b -→ 0 (ℓ 2 , 0, 3) c -→ 4 (ℓ 3 , 0, 3) Definition 3.2. The total weight of a finite run ρ = s 0 --→ w1 s 1 --→ w2 • • • --→ w k s k in a weighted transition system is w(ρ) = k i=1 w k .
We are now in a position to state the problem with which we are concerned here: We want to find accepting runs with minimum total weight in a weighted timed automaton A. However due to the possible use of strict clock constraints on edges and in locations of A, the minimum total weight might not be realizable, i.e. there might be no run which achieves it. For this reason, one also needs to consider (infinite) sets of runs and the infimum of their members' total weights: Problem 3.1 (Optimal reachability). Given a weighted timed automaton A, compute W = inf w(ρ) ρ accepting run in A and a set P of accepting runs for which inf ρ∈P w(ρ) = W .

The key ingredient in the proof of the following theorem is the introduction of weighted regions in [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF]. A weighted region is a region as of Definition 2.16 enriched with an affine cost function describing in a finite manner the cost of reaching any point within it. This notion allows one to define the weighted region automaton associated with a weighted timed automaton, and one can then show that optimal reachability can be computed in the weighted region automaton. PSPACE-hardness in the below theorem follows from PSPACE-hardness of reachability for timed automata.

Theorem 3.3 ([21]

). The optimal reachability problem for weighted timed automata with non-negative weights is PSPACE-complete.

Similar to the notion of regions for timed automata, the number of weighted regions is exponential in the number of clocks as well as in the maximal constants of the timed automaton. Hence a notion of weighted zone -a zone extended with an affine cost function -was introduced [START_REF] Kim | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF] together with an efficient, symbolic A * -algorithm for searching for cost-optimal tracing using branch-and-bound techniques. In particular, efficient means of generalizing the notion of symbolic successor to incorporate the affine cost functions were given.

During the symbolic exploration, several small linear-programming problems in terms of determining the minimal value of the cost function over the given zone have to be dealt with. Given that the constraints of these problems are simple difference constraints, it turns out that substantial gain in performance may be achieved by solving the dual problem of minimum-cost flow [START_REF] Illum Rasmussen | Resource-optimal scheduling using priced timed automata[END_REF]. The newly emerged branch Uppaal-Cora provides an efficient tool for cost-optimal reachability analysis, applying the above data structures and algorithms and allowing the user to guide and heuristically prune the search.

R = (1, 4) x ≤ 2 ℓ 1 R = (2, 1)
x ≤ 3

Multi-weighted timed automata

The below formalism of doubly weighted timed automata is a generalization of weighted timed automata useful for modeling systems with several different resources.

Definition 3.4. A doubly weighted timed automaton is a tuple

A = (L, ℓ 0 , F, C, Σ, I, E, R, P )
where (L, ℓ 0 , F, C, Σ, I, E) is a timed automaton, R : L → ) 2 a location weightrate mapping, and P : E → ) 2 an edge weight mapping.

The semantics of a doubly weighted timed automaton is a doubly weighted transition system defined similarly to Definition 3.1, and the total weight of finite runs is defined accordingly as a pair; we shall refer to the total weights as w 1 and w 2 respectively. These definitions have natural generalizations to multi-weighted timed automata with more than two weight coordinates.

The objective of conditional reachability analysis is to find runs to a final location with the lowest total weight in the first weight coordinate while satisfying a constraint on the other weight coordinate.

Example 3.2. Figure 10 depicts a simple doubly weighted timed automaton with final location ℓ 3 . Under the constraint w 2 ≤ 3, the optimal run of the automaton can be seen to be (ℓ 1 , 0, 0)

1/3 ---→ ( 1 3 , 4 3 ) (ℓ 1 , 1/3, 1/3) a -→ (ℓ 2 , 1/3, 0) 5/3 ----→ ( 10 3 , 5 3 ) (ℓ 2 , 2, 5/3) b - → (ℓ 3 , 2, 0)
with total weight 11 3 , 3 .

The precise formulation of the conditional optimal reachability problem is as follows, where we again need to refer to (possibly infinite) sets of runs: Problem 3.2 (Conditional optimal reachability). Given a doubly weighted timed automaton A and M ∈ ), compute W = inf w 1 (ρ) ρ accepting run in A, w 2 (ρ) ≤ M } and a set P of accepting runs such that w 2 (ρ) ≤ M for all ρ ∈ P and inf ρ∈P w(ρ) = W . Theorem 3.5 ([76, 77]). The conditional optimal reachability problem is computable for doubly weighted timed automata with non-negative weights and without weights on edges. The proof of the above theorem rests on a direct generalization of weighted to doubly-weighted zones. An extension can be found in [START_REF] Kim | Optimal reachability for multi-priced timed automata[END_REF], where it is shown that also the Pareto frontier, i.e. the set of cost vectors which cannot be improved in any cost variable, can be computed.

Optimal infinite runs

In this section we shall be concerned with computing optimal infinite runs in (doubly) weighted timed automata. We shall treat both the limit ratio viewpoint discussed in [START_REF] Bouyer | Staying alive as cheaply as possible[END_REF] and the discounting approach of [START_REF] Fahrenberg | Discount-optimal infinite runs in priced timed automata[END_REF][START_REF] Fahrenberg | Discounting in time[END_REF].

Example 3.3. Figure 11 shows a simple production system modelled as a weighted timed automaton. The system has three modes of production, High, Medium, and Low. The weights model the cost of production, so that the High production mode has a low cost, which is preferable to the high cost of the Low production mode. After operating in a High or Medium production mode for three time units, production automatically degrades (action d) to a lower mode. When in Medium or Low production mode, the system can be attended to (action a), which advances it to a higher mode.

The objective of optimal-ratio analysis is to find an infinite run in a doubly weighted timed automaton which minimizes the ratio between the two total weights. This will be formalized below. Definition 3.6. The total ratio of a finite run ρ = s 0 w1

--→ z1 s 1 w2 --→ z2 • • • w k --→ z k s k in a doubly weighted transition system is Γ(ρ) = k i=1 w k k i=1 z k .

The total ratio of an infinite run

ρ = s 0 w1 --→ z1 s 1 w2 --→ z2 • • • is Γ(ρ) = lim inf k→∞ Γ(s 0 → • • • → s k ).
A special case of optimal-ratio analysis is given by weight-per-time models, where the interest is in minimizing total weight per accumulated time. The example provided in this section is a case of this. In the setting of optimal-ratio analysis, these can be modelled as doubly weighted timed automata with R 2 (ℓ) = 1 and P 2 (e) = 0 for all locations ℓ and edges e.

Example 3.3 (continued). In the timed automaton of Figure 11, the following cyclic behaviour provides an infinite run ρ:

(H, 0, 0) 3 -→ (H, 3, 3) d -→ (M, 0, 3) 3 -→ (M, 3, 6) d -→ (L, 3, 6) 1 -→ (L, 4, 7) a -→ (M, 0, 0) 3 -→ (M, 3, 3) a -→ (H, 0, 0) - → • • •
Taking the weight-per-time viewpoint, the total ratio of ρ is Γ(ρ) = 4.8.

Problem 3.3 (Minimum infinite ratio).

Given a doubly weighted timed automaton A, compute W = inf Γ(ρ) ρ infinite run in A and a set P of infinite runs for which inf ρ∈P Γ(ρ) = W .

The main tool in the proof of the following theorem is the introduction of the corner-point abstraction of a timed automaton in [START_REF] Bouyer | Staying alive as cheaply as possible[END_REF]. This is a finite refinement of the region automaton of Definition 2.16 in which one also keeps track of the corner points of regions. One can then show that any infinite run with minimum ratio must pass through corner points of regions, hence these can be found in the corner-point abstraction by an algorithm first proposed in [START_REF] Karp | A characterization of the minimum cycle mean in a digraph[END_REF].

The technical condition in the theorem that the second weight coordinate be strongly diverging means that any infinite run ρ in the closure of the timed automaton in question satisfies w 2 (ρ) = ∞, see [START_REF] Bouyer | Staying alive as cheaply as possible[END_REF] for details. Theorem 3.7 ( [START_REF] Bouyer | Staying alive as cheaply as possible[END_REF]). The minimum infinite ratio problem is computable for doubly weighted timed automata with non-negative and strongly diverging second weight coordinate.

For discount-optimal analysis, the objective is to find an infinite run in a weighted timed automaton which minimizes the discounted total weight as defined below. The point of discounting is that the weight of actions is discounted with time, so that the impact of an event decreases, the further in the future it takes place.

In the definition below, ε is the empty run, and (ℓ, v) → ρ denotes the concatenation of the transition (ℓ, v) → with the run ρ. Definition 3.8. The discounted total weight of finite runs in a weighted timed automaton under discounting factor λ ∈ [0, 1[ is given inductively as follows:

w λ (ε) = 0 w λ (ℓ, v) a -→ P ρ = P + w λ (ρ) w λ (ℓ, v) d -→ ρ = R(ℓ) d 0 λ τ dτ + λ d w λ (ρ)
The discounted total weight of an infinite run ρ = (ℓ 0 , v 0 )

d1 -→ (ℓ 0 , v 0 + d 1 ) a1 -→ P1 (ℓ 1 , v 1 ) - → • • • is w λ (ρ) = lim k→∞ w λ (ℓ 0 , v 0 ) - → • • • a k --→ P k (ℓ k , v k )
provided that the limit exists.

Example 3.3 (continued). The discounted total weight of the infinite run ρ in the timed automaton of Figure 11 satisfies the following equality, where

I t = t 0 λ τ dτ = -1 ln λ (1 -λ t ): w λ (ρ) = 2I 3 + λ 3 (5I 3 + λ 3 (9I 1 + λ(1 + 5I 3 + λ 3 (2 + w λ (ρ)))))
With a discounting factor of λ = .9 for example, the discounted total weight of ρ would hence be w λ (ρ) ≈ 40.5.

Problem 3.4 (Minimum discounted weight). Given a weighted timed automaton

A and λ ∈ [0, 1[, compute W = inf w λ (ρ) ρ infinite run in A and a set P of infinite runs for which inf ρ∈P w λ (ρ) = W .

The proof of the following theorem rests again on the corner-point abstraction, and on a result in [START_REF] Andersson | Improved combinatorial algorithms for discounted payoff games[END_REF]. The technical condition that the timed automaton be time-divergent is analogous to the condition on the second weight coordinate in Theorem 3.7. Theorem 3.9 ( [START_REF] Fahrenberg | Discount-optimal infinite runs in priced timed automata[END_REF]). The minimum discounted weight problem is computable for time-divergent weighted timed automata with non-negative weights and rational λ.

Timed games

Recently, substantial effort has been made towards the synthesis of winning strategies for timed games with respect to safety and reachability control objectives. From known region-based 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][START_REF] Tripakis | On-the-fly controller synthesis for discrete and densetime systems[END_REF] and implemented in the newest branch Uppaal-Tiga.

For timed games, as for untimed ones, transitions are either controllable or uncontrollable (i.e. under the control of an environment), and the problem is to synthesize a strategy for when to take which (enabled) controllable transitions in order that a given objective is guaranteed regardless of the behaviour of the environment.

Definition 4.1. A timed game is a tuple (L, ℓ 0 , F, C, Σ c , Σ u , I, E) with Σ c ∩Σ u = ∅ and for which the tuple (L, ℓ 0 , F, C, Σ = Σ c ∪ Σ u , I, E) is a timed automaton.
Edges with actions in Σ c are said to be controllable, those with actions in Σ u are uncontrollable. We need the notion of strategy; essentially, a strategy provides instructions for which controllable edge to take, or whether to wait, in a given state:

1 ℓ 2 ℓ 3 ℓ 4 ℓ 5 ℓ 6 x > 1 u 1 x ≤ 1 c 1 x < 1 x := 0 u 2 x < 1 u 3 x ≥ 2 c 2 c 3 x ≤ 1 c 4
Definition 4.2. A strategy for a timed game A = (L, ℓ 0 , F, C, Σ c , Σ u , I, E) is a mapping σ from finite runs of A to Σ c ∪ {δ}, where δ / ∈ Σ, such that for any run ρ = (ℓ 0 , v 0 ) → • • • → (ℓ k , v k ), • if σ(ρ) = δ, then (ℓ, v) d -→ (ℓ, v + d) in A for some d > 0, and • if σ(ρ) = a, then (ℓ, v) a -→ (ℓ ′ , v ′ ) in A .
A strategy σ is said to be memoryless if σ(ρ) only depends on the last state of ρ, i.e. if ρ 1 = (ℓ 0 , v 0 )

d1 -→ (ℓ 0 , v 0 + d 1 ) → • • • → (ℓ k , v k ), ρ 2 = (ℓ 0 , v 0 ) d ′ 1 -→ (ℓ 0 , v 0 + d ′ 1 ) → • • • → (ℓ k , v k ) imply σ(ρ 1 ) = σ(ρ 2 ).
An outcome of a strategy is any run which adheres to its instructions in the obvious manner: I,E) is said to be an outcome of a strategy σ provided that

Definition 4.3. A run (ℓ 0 , v 0 ) d1 -→ (ℓ 0 , v 0 + d 1 ) → • • • → (ℓ k , v k ) in a timed game A = (L, ℓ 0 , F, C, Σ c , Σ u ,
• for all (ℓ i , v i ) d -→ (ℓ i , v i + d) and for all d ′ < d, we have σ (ℓ 0 , v 0 ) → • • • → (ℓ i , v i + d ′ ) = δ, and • for all (ℓ i , v i + d) a -→ (ℓ i+1 , v i+1 ) for which a ∈ Σ c , we have σ (ℓ 0 , v 0 ) → • • • → (ℓ i , v ′ i ) = a.
An outcome is said to be maximal if

ℓ k ∈ F , or if (ℓ k , v k ) a -→ (ℓ k+1 , v k+1 ) implies a ∈ Σ u .
Hence an outcome is maximal if it stops in a final state, 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 state may "get stuck" in a non-final state. The aim of reachability games is to find strategies all of whose maximal outcomes end in a final state; the aim of safety games is to find strategies all of whose (not necessarily maximal) outcomes avoid final states: Definition 4.4. 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.

Example 4.1 (continued).

The following memoryless strategy is winning for the reachability game on the timed game from Figure 12:

σ(ℓ 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 x(x) = 1
Problem 4.1 (Reachability and safety games). Given a timed game A, does there exist a winning strategy for the reachability game on A? Does there exist a winning strategy for the safety game on A?

An important ingredient in the proof of the following theorem is the fact that for reachability as well as safety games, it is sufficient to consider memoryless strategies. 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. Theorem 4.5 ([13, 82]). The reachability and safety games are decidable for timed games.

In [START_REF] Cassez | Timed control with observation based and stuttering invariant strategies[END_REF] the on-the-fly algorithm applied in Uppaal-Tiga has been extended to timed games under partial observability.

The field of timed games is a very active research area. Research has 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 with 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. Lately [START_REF] Bouyer | Almost optimal strategies in one clock priced timed games[END_REF] proves 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 3EXPTIME.

We conclude this section by reestablishing the connection between the notion of games and bisimulation [START_REF] Stirling | Modal and temporal logics for processes[END_REF] in the presence of time: Proposition 4.6. Timed bisimilarity polynomial-time reduces to timed safety games.

Observe that this provides an alternative proof of the decidability of timed bisimilarity in Theorem 2.23 on page 10.

p p 1 p 2 ϕ 1 r 1 a ϕ 2 r 2 a q q 1 ϕ r a p, q p 1 , q p, q 1 ⊥ p 2 , q p 1 , q 1 p 2 , q 1 z = 0 z = 0 z = 0 ϕ r a ′ ϕ 1 r1 a ′ ϕ 2 r2 a ′ φ1 r 1 a φ2 r 2 a φ r a φ r a Φ ∧ z = 0, a, ∅ Φ = ¬(ϕ 1 ∧ ϕ 2 ) ∧ z = 0 a, ∅ Φ ∧ z = 0, a, ∅
A i = (L i , ℓ i 0 , F, C i , Σ, I i , E i ), for i ∈ {1, 2}, with C 1 ∩ C 2 = ∅, we consider the timed game with locations L = {⊥} ∪ (L 1 × L 2 ) ∪ (L 1 × L 2 × Σ × {1, 2}), where F = {⊥} is a designated final location. We set C = C 1 ∪ C 2 ∪ {z}, where z / ∈ C 1 ∪ C 2 is a fresh clock, Σ c = Σ ∪ {⊥} and Σ u = {a ′ | a ∈ Σ}, and E is defined by (p, q) ϕ,a ′ ,r ----→ (p ′ , q, a) 1 ∈ E if p ϕ,a,r ---→ p ′ ∈ E 1 , (p, q) ϕ,a ′ ,r ----→ (p, q ′ , a) 2 ∈ E if q ϕ,a,r ---→ q ′ ∈ E 2 , (p ′ , q, a) 1 φ,a,r ---→ (p ′ , q ′ ) ∈ E if q ϕ,a,r ---→ q ′ ∈ E 2 , (p, q ′ , a) 2 φ,a,r ---→ (p ′ , q ′ ) ∈ E if p ϕ,a,r ---→ p ′ ∈ E 1 , and (p, q, a) i Φ∧z=0,⊥,∅ -------→ ⊥ for all i ∈ {1, 2}.
Here we denote r = r ∪ {z} and φ = ϕ ∧ z = 0, and Φ = j ¬ϕ j when q ϕj ,a,r ----→ q ′ and i = 1 and symmetrically for i = 2. Location invariants are defined by I(p, q) = I 1 (p) ∧ I 2 (q) for (p, q) ∈ L 1 × L 2 and I(p, q, a) i = (z = 0) for all (p, q, a) i ∈ L 1 × L 2 × Σ × {1, 2}. See Figure 13 for a simple example of this construction.

It remains to be seen that A 1 and A 2 are timed bisimilar if and only if a strategy σ exists for which any outcome ρ = (ℓ 0 , v 0 )

d1 -→ (ℓ 0 , v 0 + d 1 ) → • • • → (ℓ k , v k ) satisfies ℓ k = ⊥ (i.e.

it avoids the final location ⊥).

Assume A 1 and A 2 are timed bisimilar, then we can prove something stronger than the above, namely that any strategy will avoid ⊥.

Indeed, if (ℓ 0 , v 0 ) d1 -→ (ℓ 0 , v 0 + d 1 ) → • • • → (ℓ k , v k
) is a run in the timed game, and the transition

(ℓ k-2 , v k-2 ) a -→ (ℓ k-1 , v k-1 ) exists due to the first component (p k-2 , v k-2 ) of (ℓ k-2 , v k-2 ), then the corresponding a -→ transition in A 1 has a matching a -→ transition in A 2 . Hence the state (ℓ k-1 , v k-1
) has an enabled a-labeled edge, which by definition of Φ implies that the edge to ⊥ is disabled, thus ℓ k = ⊥. A symmetric argument applies in the other case. Now assume σ is a strategy which ensures avoidance of ⊥, then we shall show that any (ℓ j , v) = ((p j , q j ), v) for j ≥ 0, (i.e. of type S 1 × S 2 ) occurring in an outcome of σ satisfies (p j , v) ∼ (q j , v). Assume to the contrary that (p j , v)

a -→ (p ′ j , v ′ ) ∈ A 1 and (q j , v) a -→ (q ′ j , v ′′ ) ∈ A 2
for some a ∈ Σ, then we may extend the run to (ℓ j , v) by (ℓ j , v)

a -→ (ℓ j+1 , v ′ ) ⊥ -→ ⊥, moreover σ((ℓ 0 , v 0 ) → • • • → (ℓ j+1 , v ′ )) = ⊥
is the only choice for σ as by construction neither δ (due to the invariant z = 0) nor any b = a is available.

Statistical Model Checking for Networks of Price Timed Automata

A weak point of model checking is undoubtly the state-space explosion, i.e. the exponential growth in the analysis effort measured in the number of modelcomponents. Another limitation of real-time model checking is that it merely provides -admittedly most important -hard quantitative guarantees, e.g. the worst case response time of a recurrent task under a certain scheduling principle, the worst case execution time of a piece of code running on a particular execution platform, or the worst case time before consensus is reached by a real-time network protocol. In addition to these hard guarantees, it would be desirable in several situations to obtain refined performance information concerning likely or expected behaviors in terms of timing and resource consumption. In particular, this would allow to distinguish and select between systems that perform identically from a worst-case perspective.

In a series of recent works [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF], we proposed a stochastic semantics for Priced Timed Automata (PTA), whose clocks can evolve with different rates, while2 being used with no restrictions in guards and invariants. Networks of PTAs (NPTA) are created by composing PTAs via input and output actions. More precisely, we define a natural stochastic semantics for networks of NPTAs based on races between components being composed. We shall observe that such race can generate arbitrarily complex stochastic behaviors from simple assumptions on individual components. We shall see that our semantics cannot be emulated by applying the existing stochastic semantic of [START_REF] Baier | Probabilistic and topological semantics for timed automata[END_REF][START_REF] Bertrand | Quantitative model-checking of one-clock timed automata under probabilistic semantics[END_REF] to the product of components. Other related work includes the very rich framework of stochastic timed systems of MoDeST [START_REF] Bohnenkamp | Modest: A compositional modeling formalism for real-time and stochastic systems[END_REF]. Here, however, general hybrid variables are not considered and parallel composition does not yield fully stochastic models. For the notion of probabilistic hybrid systems considered in [START_REF] Teige | Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems[END_REF] the choice of time is resolved nondeterministically rather than stochastically as in our case. Moreover, based on the stochastic semantics, we are able to express refined performance properties, e.g. in terms of probabilistic guarantees of time-and cost-bounded properties 3 .

To allow for the efficient analysis of probabilistic performance properties we propose to work with Statistical Model Checking (SMC) [START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF][START_REF] Håkan | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], an approach that has been proposed as an alternative to avoid an exhaustive exploration of the state-space of the model. The core idea of SMC is to monitor some simulations of the system, and then use results from the statistic area (including sequential hypothesis testing or Monte Carlo simulation) in order to decide whether the system satisfies the property with some degree of confidence.

In this section, we first give insights on the model and on the stochastic semantic, then on the use of statistical model checking. Finally, we conclude with a brief discussion and some applications;

Networks of Stochastic Automata

Networks of Price Timed Automata We consider the analysis of Priced Timed Automata (PTAs) that are timed automata whose clocks can evolve with different rates in different locations. In fact, the expressive power (up to timed bisimilarity) of NPTA equals that of general linear hybrid automata (LHA) [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF], rendering most problems -including that of reachability -undecidable. We also assume PTAs are input-enabled, deterministic (with a probability measure defined on the sets of successors), and non-zeno. PTAs communicate via broadcast channels and shared variables to generate Networks of Price Timed Automata (NPTA).

Fig. 14 provides an NPTA with three components A, B, and T as specified using the Uppaal GUI. One can easily see that the composite system (A|B|T ) has the transition sequence:

(A0, Bo, T0), [x = 0, y = 0, C = 0] 1 -→ a! -→ (A1, B0, T1), [x = 1, y = 1, C = 4] 1 -→ b! -→ (A1, B1, T2), [x = 2, y = 2, C = 6] ,
demonstrating that the final location T 3 of T is reachable. In fact, location T 3 is reachable within cost 0 to 6 and within total time 0 and 2 in (A|B|T ) depending on when (and in which order) A and B choose to perform the output actions a! and b!. Assuming that the choice of these time-delays is governed by probability distributions, a measure on sets of runs of NPTAs is induced, according to which quantitative properties such as "the probability of T 3 being reached within a total cost-bound of 4.3" become well-defined.

Probabilistic Semantics of NPTA Components In our early works [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF], we provide a natural stochastic semantics, where PTA components associate probability distributions to both the time-delays spent in a given state as well as to the transition between states. In Uppaal-SMC uniform distributions are applied for bounded delays and exponential distributions for the case where a component can remain indefinitely in a state. In a network of PTAs the components repeatedly race against each other, i.e. they independently and stochastically decide on their own how much to delay before outputting, with the "winner" being the component that chooses the minimum delay. For instance, in the NPTA of Fig. 14,A wins the initial race over B with probability 0.75.

In contrast to the probabilistic semantics of timed automata in [START_REF] Baier | Probabilistic and topological semantics for timed automata[END_REF][START_REF] Bertrand | Quantitative model-checking of one-clock timed automata under probabilistic semantics[END_REF] our semantics deals with networks and thus with races between components. Let A j = (L j , X j , Σ, E j , R j , I j ) (j = 1 . . . n) be a collection of composable NPTAs. Under the assumption of input-enabledness, disjointness of clock sets and output actions, states of the the composite NPTA A = (A 1 | . . . | A n ) may be seen as tuples s = (s 1 , . . . , s n ) where s j is a state of A j , i.e. of the form (ℓ, ν) where ℓ ∈ L j and ν ∈ R X j ≥0 . Our probabilistic semantics is based on the principle of independency between components. Repeatedly each component decides on its own -based on a given delay density function and output probability function -how much to delay before outputting and what output to broadcast at that moment. Obviously, in such a race between components the outcome will be determined by the component that has chosen to output after the minimum delay: the output is broadcast and all other components may consequently change state.

Let us first consider a component A j and let St j denote the corresponding set of states. For each state s = (ℓ, ν) of A j we shall provide probability distributions for both delays and outputs. In this presentation, we restrict to uniform and universal distributions, but arbitrary distributions can be considered.

The delay density function µ s over delays in R ≥0 will be either a uniform or an exponential distribution depending on the invariant of ℓ. Denote by E ℓ the disjunction of guards g such that (ℓ, g, o, -, -) ∈ E j for some output o. Otherwise -that is I j (ℓ) does not put an upper bound on the possible delays out of s -the delay density function µ s is an exponential distribution with a rate P (ℓ), where P : L j → R ≥0 is an additional distribution rate component added to the NPTA A j . For every state s = (ℓ, ν), the output probability function γ s over Σ j o is the uniform distribution over the set {o : (ℓ, g, o, -, -) ∈ E j ∧ ν |= g} whenever this set is non-empty 4 . We denote by s o the state after the output of o. Similarly, for every state s and any input action ι, we denote by s ι the state after having received the input ι.

Probabilistic Semantics of Networks of NPTA We shall now see that while the stochastic semantics of each PTA is rather simple (but quite realistic), arbitrarily complex stochastic behavior can be obtained by their composition.

Reconsider the closed network

A = (A 1 | . . . | A n ) with a state space St = St 1 × • • • × St n .
For s = (s 1 , . . . , s n ) ∈ St and a 1 a 2 . . . a k ∈ Σ * we denote by π(s, a 1 a 2 . . . a k ) the set of all maximal runs from s with a prefix t 1 a 1 t 2 a 2 . . . t k a k for some t 1 , . . . , t n ∈ R ≥0 , that is runs where the i'th action a i has been outputted by the component A c(ai) . We now inductively define the following measure for such sets of runs:

P A π(s, a1 . . . an) = t≥0 µs c (t) • j =c τ >t µs j (τ )dτ • γ sc t (a1) • P A π(s t ) a 1 , a2 . . . an) dt
where c = c(a 1 ), and as base case we take P A (π(s), ε) = 1.

This definition requires a few words of explanation: at the outermost level we integrate over all possible initial delays t. For a given delay t, the outputting component c = c(a 1 ) will choose to make the broadcast at time t with the stated density. Independently, the other components will choose to a delay amount, which -in order for c to be the winner -must be larger than t; hence the product of the probabilities that they each make such a choice. Having decided for making the broadcast at time t, the probability of actually outputting a 1 is included. Finally, in the global state resulting from all components having delayed t timeunits and changed state according to the broadcasted action a 1 the probability of runs according to the remaining actions a 2 . . . a n is taken into account.

The Hammer Game To illustrate the stochastic semantics further consider the network of two priced timed automata in Fig. 16 modeling a competition between the two players Axel and Alex both having to hammer three nails down. As can be seen by the representing Work-locations the time (-interval) and rate of energy-consumption required for hammering a nail depends on the player and the nail-number. As expected Axel is initially quite fast and uses a lot of energy but becomes slow towards the last nail, somewhat in contrast to Alex. To make it an interesting competition, there is only one hammer illustrated by repeated competitions between the two players in the Ready-locations, where the slowest player has to wait in the Idle-location until the faster player has finished hammering the next nail. Interestingly, despite the somewhat different strategy applied, the best-and worst-case completion times are identical for Axel and Alex: 59 seconds and 150 seconds. So, there is no difference between the two players and their strategy, or is there?

Assume now that a third person wants to bet on who is the more likely winner -Axel or Alex -given a refined semantics, where the time-delay before performing an output is chosen stochastically (e.g. by drawing from a uniform distribution) and independently by each player (component).

Under such a refined semantics there is a significant difference between the two players (Axel and Alex) in the Hammer Game. In Fig. 17a) the probability distributions for either of the two players winning before a certain time is given. Though it is clear that Axel has a higher probability of winning than Alex (59% versus 41%) given unbounded time, declaring the competition a draw if it has not finished before 50 seconds actually makes Alex the more likely winner. Similarly, Fig. 17b) illustrates the probability of either of the two players winning given an upper bound on energy. With an unlimited amount of energy, clearly Axel is the most likely winner, whereas limiting the consumption of energy to maximum 52 "energy-units" gives Alex an advantage.

Verifying Queries using Statistical Model Checking

Following [START_REF] Panangaden | Labelled Markov Processes[END_REF], the measure P A may be extended in a standard and unique way to the σ-algebra generated by the sets of runs (so-called cylinders) π(s, a 1 a 2 . . . a n ).

As we shall see this will allow us to give proper semantics to a range of probabilistic time-and cost-constrained temporal properties. Let A be a NPTA. Then we consider the following non-nested PWCTL properties: Then:

A |= P ♦ C≤c ϕ ∼ p iff P A * σ∈Σ * π(s 0 , σo ϕ ) ∼ p
which is well-defined since the σ-algebra on which P A * is defined is closed under countable unions and finite intersections. To complete the semantics, we note that P( C≤c ϕ) ∼ p is equivalent to (1p) ∼ P(♦ C≤c ¬ϕ). 5Compared with previous stochastic semantics of timed automata (see e.g., [START_REF] Baier | Probabilistic and topological semantics for timed automata[END_REF][START_REF] Bertrand | Quantitative model-checking of one-clock timed automata under probabilistic semantics[END_REF]), we emphasize the novelty of the semantics of NPTA in terms of RACES between components, truthfully reflecting their independencies. In particular our stochastic semantics of a network (A 1 |..|A n ) is significantly different from that obtained by applying the stochastic semantics of [START_REF] Baier | Probabilistic and topological semantics for timed automata[END_REF][START_REF] Bertrand | Quantitative model-checking of one-clock timed automata under probabilistic semantics[END_REF] to a product construction A 1 A 2 . . . A n , as information about independencies are lost. So though (A 1 |..|A n ) and A 1 A 2 . . . A n are timed bisimilar they are in general not probabistic timed bisimilar, and hence distinguishable by PWCTL. The situation is illustrated with the following example. The problem of checking P M (ψ) ≥ p (p ∈ [0, 1]) for a PWCTL property ψ is unfortunately undecidable in general 6 . Our solution is to approximate the answer using simulation-based algorithms known under the name of statistical model checking algorithms. We briefly recap statistical algorithms permitting to answer the following three types of questions:

1. Hypothesis Testing: Is the probability P M (ψ) for a given NPTA M greater or equal to a certain threshold p ∈ [0, 1] ? 2. Probability evaluation: What is the probability P M (ψ) for a given NPTA M ? 3. Probability comparison: Is the probability P M (ψ 1 ) greater than the probability P M (ψ 2 ]?

From a conceptual point of view solving the above questions using SMC is simple. First, each run of the system is encoded as a Bernoulli random variable that is true if the run satisfies the property and false otherwise. Then a statistical algorithm groups the observations to answer the three questions. For the qualitative questions (1 and 3), we shall use sequential hypothesis testing, while for the quantitative question (2) we will use an estimation algorithm that resemble the classical Monte Carlo simulation. The two solutions are detailed hereafter.

Hypothesis Testing This approach reduces the qualitative question to testing the hypothesis H : p = P M (ψ) ≥ θ against K : p < θ. To bound the probability of making errors, we use strength parameters α and β and we test the hypothesis H 0 : p ≥ p 0 and H 1 : p ≤ p 1 with p 0 = θ + δ 0 and p 1 = θδ 1 . The interval p 0p 1 defines an indifference region, and p 0 and p 1 are used as thresholds in the algorithm. The parameter α is the probability of accepting H 0 when H 1 holds (false positives) and the parameter β is the probability of accepting H 1 when H 0 holds (false negatives). The above test can be solved by using Wald's sequential hypothesis testing [START_REF] Wald | Sequential Analysis[END_REF]. This test computes a proportion r among those runs that satisfy the property. With probability 1, the value of the proportion will eventually cross log(β/(1-α) or log((1-β)/α) and one of the two hypothesis will be selected.

Probability Estimation This algorithm [START_REF] Hérault | Ap-proximate probabilistic model checking[END_REF] computes the number of runs needed in order to produce an approximation interval [pε, p + ε] for p = P r(ψ) with a confidence 1α. The values of ε and α are chosen by the user and the number of runs relies on the Chernoff-Hoeffding bound.

Probability Comparison

This algorithm, which is detailed in [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF], exploits an extended Wald testing.

UPPAAL-SMC

We have implemented the above model and algorithms in a statistical extension of UPPAAL called Uppaal-SMC. In addition to the features exposed above, the tool also proposes a friendly-user interface to plot results of estimating distributions as well as a distributed engine to exploit computer grids. Details on Uppaal-SMC can be found in [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF][START_REF] David | Time for statistical model checking of real-time systems[END_REF]. As an illustration, here is how we translate the SMC queries from previous section in Uppaal-SMC.

• Hypothesis testing: Pr[bound](ϕ)>=p 0 , where bound defines how to bound the runs. The three ways to bound them are 1) implicitly by time by specifying <=M (where M is a positive integer), 2) explicitly by cost with x<=M where x is a specific clock, or 3) by number of discrete steps with #<=M . In the case of hypothesis testing p 0 is the probability to test for. The formula ϕ is either <> q or [] q where q is a state predicate.

Some Illustrations

We briefly survey some recent results obtained via Uppaal-SMC.

Robot Control

In [START_REF] Bulychev | Monitor-based statistical model checking for weighted metric temporal logic[END_REF] we considered a case -explored in [START_REF] Barbot | Efficient CTMC model checking of linear real-time objectives[END_REF] -of a robot moving on a two-dimensional grid. We are interested in the probability that the robot reaches its goal location without staying on consecutive fire fields for more than one time unit and on consecutive ice fields for more than two time units. We applied Uppaal-SMC to compute the probability of the robot reaching this, without staying more than x time units in some fixed position.

Bluetooth [START_REF] Mcdermott-Wells | What is bluetooth? Potentials[END_REF] is a wireless telecommunication protocol using frequency-hopping to cope with interference between the devices in the wireless network. In paper [START_REF] David | Time for statistical model checking of real-time systems[END_REF] we adopted the model from [START_REF] Duflot | A formal analysis of bluetooth device discovery[END_REF], annotated the model to record the power utilization and evaluated the probability distributions of likely response times and energy consumption.

Lightweight Medium Access Protocol (LMAC) [START_REF] Lodewijk | A lightweight medium access protocol (LMAC) for wireless sensor networks: Reducing preamble transmissions and transceiver state switches[END_REF] LMAC is a communication scheduling protocol based on time slot distribution for nodes sharing the same medium. The protocol is designed having wireless sensor networks in mind: it is simple enough to fit on a modest hardware and at the same time robust against topology reconfiguration, minimizing collisions and power consumption. In [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF] we showed how collisions can be analyzed and power consumption estimated using statistical model checking techniques.

Computing Nash Equilibrium in Wireless Ad Hoc Networks One of the important aspects in designing wireless ad-hoc networks is to make sure that a network is robust to the selfish behavior of its participants, i.e. that its configuration satisfies Nash equilibrium (NE). In [START_REF] Bulychev | Computing Nash equilibrium in wireless ad hoc networks: A simulation-based approach[END_REF] we proposed an SMC-based algorithm for computing NE for the case when network nodes are modeled by SPTA and an utility function of a single node is equal to a probability that the node will reach its goal.

Energy aware Buildings In [START_REF] David | Runtime verification of biological systems[END_REF], we considered energy aware buildings. We refer to a recently developed framework including components for layout of builidngs, availability of heaters, climate and user behavious allowing to evaluated different strategies for distributing heaters among rooms in terms of the resulting comfort and energy consumption. To indicate central parts of this framework and the clear advantages of modeling the evoluation of room temperatures with ODEs, we illustrated in [START_REF] David | Runtime verification of biological systems[END_REF] the framework with a small instance comprising two rooms with a single shared heater.

Systems Biology

In [START_REF] David | Statistical model checking for stochastic hybrid systems[END_REF][START_REF] David | Runtime verification of biological systems[END_REF], we extended our model in order to incorporate ODEs. We then showed how the combination of ODEs and SMC allows us to reason on biological oscillations -a problem that is beyond the scope of most existing formal verification techniques. We model a genetic circadian oscillator, which is used to distill the essence of several real circadian oscillators.

Duration Probabilistic Automata In [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF] we compared Uppaal-SMC to Prism [START_REF] Kwiatkowska | PRISM 2.0: A tool for probabilistic model checking[END_REF] in the context of Duration Probabilistic Automata (DPA) [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF]. A Duration Probabilistic Automaton (DPA) is a composition of Simple Duration Probabilistic Automata (SDPA). An SDPA is a linear sequence of tasks that must be performed in a sequential order. Each task is associated with a duration interval which gives the possible durations of the task. The actual duration of the tasks is given by a uniform choice from this interval. The comparison with Prism was made by randomly generating models with a specific number of SDPAs and a specific number of tasks per SDPA and translate these into Prism and Uppaal models. The queries to the models were What is the probability of all SDPAs ending within t time units (Estimation)and Is the probability that all SDPAs end within t time units greater than 40% (Hypothesis testing). The value of t is different for each model as it was computed by simulating the system 369 times and represent the value for which at least 60% of the runs finished all their tasks.

Definition 2 . 1 .

 21 The set Φ(C) of clock constraints ϕ over a finite set (of clocks) C is defined by the grammar Off Light x ≤ 100 Bright x ≤ 100 press?

Definition 2 . 4 .Definition 2 . 5 .

 2425 A clock valuation on a finite set C of clocks is a mapping v : C → | ≥0 . The initial valuation v 0 is given by v 0 (x) = 0 for all x ∈ C. For a valuation v, d ∈ | ≥0 , and r ⊆ C, the valuations v + d and v[r] are defined by(v + d)(x) = v(x) + d v[r](x) = 0 for x ∈ r, v(x) for x / ∈ r.Extending the notation for power set introduced above, we will in general write B A for the set of mappings from a set A to a set B. The set of clock valuations on C is thus | C ≥0 . The zone of an extended clock constraint in Φ + (C) is a set of clock valuations C → | ≥0 given inductively by x ⊲⊳ k = {v : C → | ≥0 | v(x) ⊲⊳ k}, xy ⊲⊳ k = {v : C → | ≥0 | v(x)v(y) ⊲⊳ k}, and

Figure 2 .

 2 Figure 2.: A timed automaton with two clocks.Example 2.1 (continued). The light switch model from figure 1 has as state set S = {Off} × | ≥0 ∪ {Light, Bright} × [0, 100]where we identify valuations with their values at x. A few example runs are given below; we abbreviate "press?" to "p":

2 yFigure 3 .

 23 Figure 3.: Time-abstracted bisimulation classes for the two-clock timed automaton from Example 2.2. Left: equivalence classes for switch transitions only; right: equivalence classes for switch and delay transitions.

Notation 2 . 15 .Definition 2 . 16 .

 215216 For d ∈ | ≥0 we write ⌊d⌋ and d for the integral, respectively fractional, part of d, so that d = ⌊d⌋ + d . For a timed automaton A = (L, ℓ 0 , F, C, Σ, I, E), valuations v, v ′ :

Example 2 . 2 (

 22 continued). The 69 regions of the timed automaton A from Figure2are depicted in Figure4.

4 x 2 yFigure 4 .

 424 Figure 4.: Clock regions for the timed automaton from Example 2.2.

Figure 5 .

 5 Figure 5.: Timed trace encoding a increment instruction I i+1 of a 2-counter machine.

ΣFigure 6 .

 6 Figure 6.: Timed automaton which violates the encoding of the increment instruction.

Figure 7 .

 7 Figure 7.: Graph representation of extended clock constraint. Lemma 2.40 ([62, 95]). If Z is a zone over C and r ⊆ C, then Z ↑ and Z[r] are also zones over C. Extended clock constraints representing Z ↑ and Z[r] may be computed efficiently (in time cubic in the number of clocks in C) by representing the zone Z in a canonical form obtained by computing the shortest-path closure of the directed graph representation of Z, see [72].

Figure 8 .

 8 Figure 8.: Canonical representations. Left: shortest-path closure; right: shortestpath reduction.

Figure 9 .

 9 Figure 9.: A weighted timed automaton with two clocks.

Definition 3 . 1 .

 31 A weighted timed automaton is a tuple A = (L, ℓ 0 , F, C, Σ, I, E, R, P ), where (L, ℓ 0 , F, C, Σ, I, E) is a timed automaton, R : L → ) a location weight-rate mapping, and P : E → ) an edge weight mapping.The semantics of A is the weighted transition system A = (S, s 0 , Σ ∪ | ≥0 , T, w), where (S, s 0 , Σ ∪ | ≥0 , T ) is the semantics of the underlying timed automaton (L, ℓ 0 , F, C, Σ, I, E), and the transition weights w : T → | are given as follows:

Figure 10 .

 10 Figure 10.: A doubly weighted timed automaton with two clocks.

1 Figure 11 .

 111 Figure 11.: A weighted timed automaton modelling a simple production system.

Example 4 . 1 .

 41

Figure 12

 12 provides a simple example of a timed game. Here, Σ c = {c 1 , c 2 , 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.

  ℓ

Figure 12 .

 12 Figure 12.: A timed game with one clock. Controllable edges (with actions from Σ c ) are solid, uncontrollable edges (with actions from Σ u ) are dashed.

Figure 13 .

 13 Figure 13.: A timed game constructed for bisimilarity checking of two simple timed automata Proof: Given timed automataA i = (L i , ℓ i 0 , F, C i , Σ, I i , E i ), for i ∈ {1, 2}, with C 1 ∩ C 2 = ∅, we consider the timed game with locations L = {⊥} ∪ (L 1 × L 2 ) ∪ (L 1 × L 2 × Σ × {1, 2}),where F = {⊥} is a designated final location. We set C = C 1 ∪ C 2 ∪ {z}, where z / ∈ C 1 ∪ C 2 is a fresh clock, Σ c = Σ ∪ {⊥} and Σ u = {a ′ | a ∈ Σ}, and E is defined by

Figure 14 .

 14 Figure 14.: An NPTA, (A|B|T ).

Figure 15 .

 15 Figure 15.: Cumulative probabilities for time and Cost-bounded reachability of T 3 .

  Denote by d(ℓ, ν) the infimum delay before enabling an output, i.e. d(ℓ, ν) = inf{d ∈ R ≥0 : ν + R j • d |= E ℓ }, and denote by D(ℓ, ν) the supremum delay, i.e. D(ℓ, ν) = sup{d ∈ R ≥0 : ν + R j • d |= I j (ℓ)}. If D(ℓ, ν) < ∞ then the delay density function µ s is a uniform distribution on [d(ℓ, ν), D(ℓ, ν)].

Figure 16 .: 3 -

 163 Figure 16.: 3-Nail Hammer Game between Axel and Alex.

Figure 17 .

 17 Figure 17.: Time-and Cost-dependent Probability of winning the Hammer Game

Figure 18 .

 18 Figure 18.: Cumulative probabilities for time and cost-bounded reachability of T 3 . ψ ::= P ♦ C≤c ϕ ∼ p | P C≤c ϕ ∼ pwhere C is an observer clock (of A), ϕ a state-property (wrt. A) , ∼∈ {<, ≤, = , ≥, >}, and p ∈ [0, 1]. This logic is a stochastic extension of the classical WCTL logic for non-stochastic systems, where the existential quantifier is replaced by a probability operator. For the semantics let A * be the modification of A, where the guard C ≤ c has been conjoined to the invariant of all locations and an edge (ℓ, ϕ, o ϕ , ∅, ℓ) has been added to all locations ℓ, where o ϕ is a new output action. Then:

Example 5 . 1 .

 51 Reconsider the Example of Fig. 14. Then it can be shown that (A|B|T ) |= P ♦ t≤2 T 3 = 0.75 and (A|B|T ) |= P ♦ C≤6 T 3 = 0.75, whereas (AB|T ) |= P ♦ t≤2 T 3 = 0.50 and (AB|T ) |= P ♦ C≤6 T 3 = 0.50. Fig. 18 gives a time-and cost-bounded reachability probabilities for (A|B|T ) and (AB|T ) for a range of bounds. Thus, though the two NPTAs satisfy the same WCTL properties, they are obviously quite different with respect to PWCTL. The NPTA B r of Fig. 14 is a variant of B, with the uniform delay distribution enforced by the invariant y ≤ 2 being replaced by an exponential distribution with rate 1 2 . Here (A|B r |T ) satisfies P ♦ t≤2 T 3 ≈ 0.41 and P ♦ C≤6 T 3 ≈ 0.49.

•

  Estimation: Pr[bound](ϕ) • Comparison: Pr[bound 1 ](ϕ 1 )>= Pr[bound 2 ](ϕ 2 ).

in contrast to the usual restriction of priced timed automata[START_REF] Alur | Optimal paths in weighted timed automata[END_REF]

We also note that the above (stochastic) interpretation of PWCTL is a conservative extension of the classical (non-stochastic) interpretation of WCTL, in the sense that A |= P ♦ C≤c ϕ > 0 implies An |= E♦ C≤c ϕ, where An refers to the standard non-stochastic semantics of A.