Uli Fahrenberg
email: ulrich.fahrenberg@irisa.fr

Claus Thrane

Kim G Larsen

Distances for Weighted Transition Systems: Games and Properties

We develop a general framework for reasoning about distances between transition systems with quantitative information. Taking as starting point an arbitrary distance on system traces, we show how this leads to natural definitions of a linear and a branching distance on states of such a transition system. We show that our framework generalizes and unifies a large variety of previously considered system distances, and we develop some general properties of our distances. We also show that if the trace distance admits a recursive characterization, then the corresponding branching distance can be obtained as a least fixed point to a similar recursive characterization. The central tool in our work is a theory of infinite path-building games with quantitative objectives.

Introduction

In verification of concurrent and reactive systems, one generally seeks to assert properties of systems expressed in terms of sets of traces (or languages) or in terms of computation trees. The language point of view leads to what is generally called linear semantics, whereas the tree point of view leads to branching semantics. These semantics are the extreme points in a spectrum containing a number of other useful notions; see [START_REF] Van Glabbeek | The Linear Time -Branching Time Spectrum I[END_REF] for an overview.

As emphasized in [START_REF] Henzinger | The Embedded Systems Design Challenge[END_REF], working with applications in complex reactive systems or in embedded systems means that classical notions of linear and branching equivalence (or inclusion) of processes often need to be extended to accommodate quantitative information. This can be in relation to real-time behavior, resource usage, or can be probabilistic or stochastic information. In such a quantitative setting, equivalences and inclusions are replaced by symmetric or asymmetric distances between systems.

This approach of quantitative analysis has been taken in numerous papers by multiple authors, both in the real-time (or hybrid), in the probabilistic, and in general quantitative settings, see [2, 3, 8-12, 15, 19, 21, 22, 27] for a (non-exhaustive) choice of references. Indeed, the quantitative approach is also useful in settings without quantitative information in the models, e.g. in [START_REF] Černý | Simulation Distances[END_REF] various distances related to implementation correctness of discrete systems are considered.

The above-mentioned dichotomy between languages and trees persists in the quantitative setting, where one hence encounters both notions of linear and of branching distances. To the best of our knowledge, the treatment of those distances, and of the relations between them, has so far been somewhat ad hoc. Indeed, the general approach appears to be to introduce some particular distances which are relevant for a particular application and then show some useful properties; in this paper, we try to unify and generalize some of these approaches.

The present paper is in a sense a follow-up to previous papers [START_REF] Fahrenberg | A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF] by the same authors. In those papers, we introduce and investigate three different linear and branching distances. A paper similar in spirit to these is [START_REF] Luca De Alfaro | Linear and Branching System Metrics[END_REF], which analyses properties of what we later will call the point-wise distance for weighted Kripke structures. The starting point for the present paper is then the observation of similarities between the constructions for different types of distances, which we here generalize to encompass all of them and to construct a coherent framework.

In this paper, we take the view that in practical applications, say in reactive systems, the system distance which measures adherence to the property which we want to verify, will be specific to the concrete domain of the application. Hence in a general framework like the one proposed here, its description must be given as an input. A method to obtain the actual system distances, for some desired level of interaction, is then prescribed by the framework.

In this paper we assume that this system distance input is given as a distance on traces: Given two sequences of executions, one needs only to define what it means for these sequences to be closely related to each other. We show that such a trace distance always gives rise to natural notions both of linear and of branching distance.

To relate linear and branching distances, we introduce a general notion of simulation game with quantitative objectives. The idea of using games for linear and branching equivalences is not new [START_REF] Stirling | Modal and Temporal Logics for Processes[END_REF] and has been used in a quantitative setting e.g. in [START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Desharnais | Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games[END_REF], but here we explore this idea in its full generality.

One interesting result which we can show in our general framework is that for all interesting trace distances, the corresponding linear and branching distance are topologically inequivalent. From an application point of view this means that corresponding linear and branching distances (essentially) always measure very different things and that results about one of them cannot generally be transferred to the other. This result -and indeed also its proof -is a generalization of the well-known fact that language inclusion does not imply simulation to a quantitative setting.

We also show that for the common special case that the trace distance has a recursive characterization, the associated branching distance can be obtained as a least fixed point to a similar recursive characterization. This is again a generalization of some standard facts about simulation, but shows that for a large class of branching distances, characterizations as least fixed points are available. Definition 2. A ❑-weighted transition system (WTS) is a pair A = (S, T ) of sets S, T with T ⊆ S × ❑×S.

We use the familiar notation s x -→ s ′ to indicate that (s, x, s ′ ) ∈ T . Note that S and T may indeed be infinite, also infinite branching. For simplicity's sake we shall follow the common assumption that all our WTS are non-blocking, i.e. that for any state s ∈ S there is a transition s

x - → s ′ in T . A path from s 0 ∈ S in a WTS (S, T ) is an infinite sequence s j x j -→ s j+1 ∞ j=0 of transitions in T .
The set of such is denoted Pa(s 0 ). We will in some places also need finite paths, i.e. finite sequences s j

x j -→ s j+1 n j=0 of transitions; the set of finite paths from s 0 is denoted fPa(s 0 ). For a finite path π as above, we let len(π) = n denote its length and last(π) = s n+1 its last state. We write π j = s j for the ( j + 1)th state and tr(π) j for the ( j + 1)th weight in a finite or infinite path.

A path π = s j x j -→ s j+1 ∞ j=0
gives rise to a trace tr(π) = x j ∞ j=0 . The set of (infinite) traces from s 0 ∈ S is denoted Tr(s 0 ) = tr(π) π ∈ Pa(s 0 ) .

Interlude: Hemimetrics

Before we proceed, we recall some of the notions regarding asymmetric metrics which we will be using. First, a hemimetric on a set X is a function d : X × X → [0, ∞] which satisfies d(x, x) = 0 for all x ∈ X and the triangle inequality d(x, y) + d(y, z) ≥ d(x, z) for all x, y, z ∈ X.

We will have reason to consider two different notions of equivalence of hemimetrics. Two hemimetrics d 1 , d 2 on X are said to be Lipschitz equivalent if there are constants m, M ∈ | such that

m d 1 (x, y) ≤ d 2 (x, y) ≤ M d 1 (x, y)
for all x, y ∈ X. Lipschitz equivalent hemimetrics are hence dependent on each other; intuitively, a property using one hemimetric can always be approximated using the other. Another, weaker, notion of equivalence of hemimetrics is the following: Two hemimetrics d 1 , d 2 on X are said to be topologically equivalent if the topologies on X generated by the open balls B i (x; r) = {y ∈ X | d i (x, y) < r}, for i = 1, 2, x ∈ X, and r > 0, coincide. Topological equivalence hence preserves topological notions such as convergence of sequences: If a sequence (x j ) of points in X converges in one hemimetric, then it also converges in the other.

It is a standard fact that Lipschitz equivalence implies topological equivalence. From an application point-of-view, topological equivalence is interesting for showing negative results; proving that two hemimetrics are not topologically equivalent can be comparatively easy, and implies that intuitively, the two hemimetrics measure very different properties.

Examples of Trace Distances

The framework we are proposing in this article takes as starting point a trace distance defined on executions of a weighted automaton, i.e. a hemimetric d T : ❑ ω × ❑ ω → [0, ∞]. In this section we introduce a number of different such trace distances, to show that the framework is applicable to a variety of interesting examples.

Discrete trace distances. The discrete trace distance on ❑ ω is defined by d T (σ , τ) = 0 if σ = τ and d T (σ , τ) = ∞ otherwise. Hence only equality or inequality of traces is measured; we shall see below that this distance exactly recovers the usual Boolean framework of trace inclusion and simulation.

If ❑ comes equipped with a preorder ⊑ ⊆ ❑×❑ indicating that a label x ∈ ❑ may be replaced by any y ∈ ❑ with x ⊑ y, as e.g. in [START_REF] Thomsen | An Extended Bisimulation Induced by a Preorder on Actions[END_REF], then we may refine the above distance by instead letting d T (σ , τ) = 0 if σ j ⊑ τ j for all j and d T (σ , τ) = ∞ otherwise. We will see later that using this trace distance, we exactly recover the extended simulation of [START_REF] Thomsen | An Extended Bisimulation Induced by a Preorder on Actions[END_REF]; note that something similar is done in [START_REF] Karla Alves De Medeiros | Quantifying process equivalence based on observed behavior[END_REF].

Hamming distance. If one defines a metric d on ❑ by d(x, y) = 0 if x = y and d(x, y) = 1 otherwise, then the sum ∑ j d(σ j , τ j ) for any pair of finite traces σ , τ of equal length is precisely the well-known Hamming distance [START_REF] Hamming | Error Detecting and Error Correcting Codes[END_REF]. For infinite traces, some technique can be used for providing finite values for infinite sums; two such techniques are to use limit average or discounting. We can hence define the limit-average Hamming distance by d T (σ , τ) = lim inf j→∞ 1 j ∑ j d(σ j , τ j ), and for a fixed discounting factor 0 ≤ λ < 1, the discounted Hamming distance by d T (σ , τ) = ∑ j λ j d(σ j , τ j ).

Note that this approach can easily be generalized to other (hemi)metrics d on ❑; indeed the discrete trace distances from above can be recovered using d(x, y) = 0 if x ⊑ y and d(x, y) = ∞ otherwise.

Labeled weighted transition systems. A common example of weighted systems [START_REF] Bouyer | Infinite Runs in Weighted Timed Automata with Energy Constraints[END_REF][START_REF] Franck Van Breugel | A Behavioural Pseudometric for Metric Labelled Transition Systems[END_REF][START_REF] Černý | Simulation Distances[END_REF][START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF] has ❑ = Σ × | where Σ is a discrete set of labels. Hence x = (x ℓ , x w ) ∈ ❑ has x ℓ ∈ Σ as discrete component and x w ∈ | as real weight. A useful trace distance for this type of systems is the point-wise distance, see [START_REF] Luca De Alfaro | Linear and Branching System Metrics[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF], given by d T (σ , τ) = sup j |σ w jτ w j | if σ ℓ j = τ ℓ j for all j and d T (σ , τ) = ∞ otherwise. This measures the biggest individual difference between σ and τ.

Another interesting trace distance in this setting is the accumulated distance [START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF], where individual differences in weights are added up. Again one can use limit average or discounting for infinite sums; limit-average accumulating distance is defined by

d T (σ , τ) =    lim inf j→∞ 1 j ∑ j |σ w j -τ w j | if σ ℓ j = τ ℓ j for all j ∞ otherwise
and discounted accumulating distance, for a fixed λ < 1, by

d T (σ , τ) = ∑ j λ j |σ w j -τ w j | if σ ℓ j = τ ℓ j for all j ∞ otherwise
This is indeed a generalization of the Hamming distance above, setting d (x, w),

(y, v) = |w -v| if x = y and d (x, w), (y, v) = ∞ otherwise.
Also of interest is the maximum-lead distance from [START_REF] Henzinger | Quantifying Similarities Between Timed Systems[END_REF], where the individual weights are added up and one is concerned with the maximal difference between the accumulated weights. The definition is

d T (σ , τ) = sup j ∑ j i=0 σ w i -∑ j i=0 τ w i if σ ℓ j = τ ℓ j for all j ∞ otherwise

Simulation Games

In this central section we introduce the game which we will use to define both the linear and the branching distances. We shall use some standard terminology and constructions from game theory here; for a good introduction to the subject see e.g. [START_REF] Ferguson | Game Theory[END_REF].

Let A = (S, T ) be a weighted transition system with s,t ∈ S and d T :

❑ ω × ❑ ω → [0, ∞] a trace distance.
Using A as a game graph, the simulation game played on A from (s,t) is an infinite turnbased two-player game, where we denote the strategy space of Player i by Θ i and the utility function of Player 1 by u :

Θ 1 × Θ 2 → [0, ∞].
As usual u determines the pay-off of Player 1; we will not use pay-offs for Player 2 here. The game moves along transitions in A while building a pair of paths extending from s and t, according to the strategies of the players. In the terminology of [START_REF] Hans | Complexity of Path-Forming Games[END_REF][START_REF] Aviezri | [END_REF] we are playing a partisan path-forming game.

A configuration of the game is a pair of finite paths (π 1 , π 2 ) ∈ fPa(s) × fPa(t) (i.e. the history) which are consecutively updated by the players as the game progresses. The players must play according to a strategy of the following types:

• Θ 1 = T fPa(s)×fPa(t) , the set of mappings from pairs of finite paths to transitions, with the additional requirement that for all

θ 1 ∈ Θ 1 and (π 1 , π 2 ) ∈ fPa(s) × fPa(t), θ 1 (π 1 , π 2 ) = (last(π 1 ), x, s ′ ) for some x ∈ ❑, s ′ ∈ S.
This is the set of Player-1 strategies which observe the complete configuration.

• Similarly, Θ 2 = T fPa(s)×fPa(t) with the additional requirement that for all θ 2 ∈ Θ 2 and (π

1 , π 2 ) ∈ fPa(s) × fPa(t), θ 2 (π 1 , π 2 ) = (last(π 2 ), y,t ′ ) for some y ∈ ❑, t ′ ∈ S.
• Θ1 = T fPa(s) , the set of blind Player-1 strategies which cannot observe the moves of Player 2.

(Blind Player-2 strategies can be defined similarly, but we will not need those here.) It is convenient to identify Θ1 with the subset of Θ 1 of all strategies θ 1 which satisfy

θ 1 (π 1 , π 2 ) = θ 1 (π 1 , π ′ 2 ) for all π 1 ∈ fPa(s), π 2 , π ′ 2 ∈ fPa(t).
• In the proof of Proposition 4 we will also need Player-2 strategies with additional memory. Such a strategy is a mapping fPa(s) × fPa(t) × M → T × M, where M is a set used as memory.

Given a game with configuration (π 1 , π 2 ), a round is played, according to a strategy profile (i.e. a pair of strategies) (θ 1 , θ 2 ) ∈ Θ 1 × Θ 2 , by first updating π 1 according to θ 1 and then updating the resulting configuration according to θ 2 . Hence we define

Round (θ 1 ,θ 2 ) (π 1 , π 2 ) = π 1 • θ 1 (π 1 , π 2 ), π 2 • θ 2 (π 1 • θ 1 (π 1 , π 2 ), π 2 )
where • denotes sequence concatenation.

A strategy profile

(θ 1 , θ 2 ) ∈ Θ 1 × Θ 2 inductively determines an infinite sequence (π j 1 , π j 2 ) ∞ j=0 of configurations given by (π 0 1 , π 0 2 ) = (s,t) and (π j 1 , π j 2 ) = Round (θ 1 ,θ 2 ) (π j-1 1 , π j-1 2 ) for j ≥ 1.
The paths in this sequence satisfy π j i ⊑ π j+1 i , where ⊑ denotes prefix ordering, hence the limits

π 1 (θ 1 , θ 2 ) = lim j→∞ π j 1 ∈ Pa(s), π 2 (θ 1 , θ 2 ) = lim j→∞ π j 2 ∈ Pa(t)
exist (as infinite paths). We define the utility function

u as u(θ 1 , θ 2 ) = d T tr(π 1 (θ 1 , θ 2 )), tr(π 2 (θ 1 , θ 2 ))
This determines the pay-off to Player 1 when the game is played according to strategies θ 1 , θ 2 . Note again that the utility function for Player 2 is left undefined; especially we make no claim as to the game being zero-sum.

The value of game on A from (s,t) is defined to be the optimal Player-1 pay-off

v(s,t) = sup θ 1 ∈Θ 1 inf θ 2 ∈Θ 2 u(θ 1 , θ 2 )
Observe that the game is asymmetric; in general, v(s,t) = v(t, s).

A strategy θ1 for Player 1 is said to be optimal if it realizes the supremum above, i.e. whenever inf

θ 2 ∈Θ 2 u( θ1 , θ 2 ) = sup θ 1 ∈Θ 1 inf θ 2 ∈Θ 2 u(θ 1 , θ 2 ). The strategy is called ε-optimal for some ε > 0 provided that inf θ 2 ∈Θ 2 u( θ1 , θ 2 ) ≥ sup θ 1 ∈Θ 1 inf θ 2 ∈Θ 2 u(θ 1 , θ 2 ) -ε.
Note that ε-optimal strategies always exist for any ε > 0, whereas optimal strategies may not.

We also recall that the game is said to be determined if the sup and inf above can be interchanged, i.e. if v(s,t) = inf θ 2 ∈Θ 2 sup θ 1 ∈Θ 1 u(θ 1 , θ 2 ). Intuitively, the game is determined if there also exist ε-optimal Player-2 strategies for any ε > 0 which realize the value of the game (up to ε) independent of the strategy Player 1 might choose.

The 1-blind value of the game is defined to be ṽ(s,t) = sup

θ 1 ∈ Θ1 inf θ 2 ∈Θ 2 u(θ 1 , θ 2 )

Example: Discrete Trace Distance

It may be instructive to apply the above simulation game in the context of the discrete trace distance

d T (σ , τ) = 0 if σ = τ, d T (σ , τ) = ∞ otherwise, from Section 2.2.
In this case, the game has value v(s,t) = 0 if and only if, for every θ 1 ∈ Θ 1 there exist a θ 2 ∈ Θ 2 which in each round i ≥ 0 of the game, in configuration

(π i 1 , π i 2 ), maps θ 2 (π i 1 , π i 2 ) = (last(π i 2 ), x,t i+1 ) whenever θ 1 (π i 1 , π i 2 ) = (last(π i 1 ), x, s i+1 ). Otherwise, v(s,t) = ∞.
Hence we have v(s,t) = 0 if t simulates s in the sense of [START_REF] Milner | Communication and Concurrency[END_REF], and v(s,t) = ∞ otherwise. In other words, for discrete trace distance the game reduces to the standard simulation game of [START_REF] Stirling | Modal and Temporal Logics for Processes[END_REF].

Likewise, the blind value ṽ(s,t) = 0 if and only if every θ 1 ∈ Θ1 and corresponding path π 1 has a match θ 2 ∈ Θ 2 where configuration (

π i 1 , π i 2 ), of round i ≥ 0 facilitates θ 2 (π i 1 , π i 2 ) = (last(π i 2 ), x,t i+1 ) whenever θ 1 (π i 1 , π i 2 ) = (last(π i 1 ), x, s i+1
). Hence ṽ(s,t) = 0 if Tr(s) ⊆ Tr(t); we recover standard trace inclusion.

Linear and Branching Distance

We can now use the game introduced in Section 2.3 to define linear and branching distance: Definition 3. Let A = (S, T ) be a WTS and s,t ∈ S.

• The linear distance from s to t is the 1-blind value d L (s,t) = ṽ(s,t).

• The branching distance from s to t is the value d B (s,t) = v(s,t).

We proceed to show that the distances so defined are hemimetrics on S, cf. the proof of Theorem 1 in [START_REF] Černý | Simulation Distances[END_REF]. For linear distance, this also follows from Theorem 6 below, and we only include the proof for reasons of exposition. For branching distance, we have to assume in the proof below that the simulation game is determined; currently we do not know whether this assumption can be lifted. Proposition 4. Linear distance d L is a hemimetric on S, and if the simulation game is determined, so is d B .

Proof. Non-negativity of d L and d B follow directly from the non-negativity of d T . To prove that d L (s, s) = d B (s, s) = 0 for all s ∈ S, given any strategy θ 1 ∈ Θ 1 , we construct a Player-2 strategy θ 2 ∈ Θ 2 that mimics θ 1 and attains the game value of 0, as follows: It can be seen easily that the paths constructed by both players are the same, i.e. u(π 1 , π 2 ) = d T (τ, τ) for some τ ∈ Pa(s 0 ). Therefore,

θ 2 (π ′ , π) = θ 1 (π, π) if π ′ = π • θ 1 (π, π) (last(π), y, s ′ ) for some (last(π), y, s ′ ) ∈ T otherwise
u(π 1 , π 2 ) = 0 as d T is a hemimetric, whence d L (s, s) = d B (s, s) = 0.
We are left with showing that d L and d B obey the triangle inequality. For linear distance, let s 1 , s 2 , s 3 ∈ S and write Θ i, j k ( Θi, j k ) for the set of (blind) Player-k strategies in the simulation game computing d L (s i , s j ), for i, j ∈ {1, 2, 3} and k ∈ {1, 2}. Let ε > 0. It might be beneficial to look at Figure 1 to see the "chase of strategies" we will be conducting.

Choose a blind Player-1 strategy θ 1,3 1 ∈ Θ1,3 1 . Blind strategies correspond to choosing a path, so let π 1 ∈ Pa(s 1 ) be the path chosen by θ 1, 3 1 . This path in turn corresponds to a blind Player-1 strategy

θ 1,2 1 ∈ Θ1,2 1 . Let θ 1,2 2 ∈ Θ 1,2 2 be a Player-2 strategy for which u(θ 1,2 1 , θ 1,2 2 ) < d L (s 1 , s 2 ) + ε 2 . Write π 2 ∈ Pa(s 2
) for the path constructed by the strategy profile (θ 1,2 1 , θ 1,2 2 ), and let θ 2,3 1 ∈ Θ2,3 1 be a blind Player-1 strategy which constructs π 2 .

Let θ 2,3 2 ∈ Θ 2,3 2 ensure u(θ 2,3 1 , θ 2,3 2 ) < d L (s 2 , s 3 ) + ε 2 . Write π 3 ∈ Pa(s 3 ) for the path constructed by the strategy profile (θ 2, 3 1 , θ 2,3 2 ), and let θ 1,3 2 ∈ Θ 1,3 2 be a strategy which constructs π 3 . For the strategy profile (θ 1, 3 1 , θ 1,3 2 ) in G 1,3 , the paths constructed are π 1 ∈ Pa(s 1 ) and π 3 ∈ Pa(s 3 ). Hence we have inf

θ 2 ∈Θ 1,3 2 u(θ 1,3 1 , θ 2 ) ≤ u(θ 1,3 1 , θ 1,3 2 ) = d T (π 1 , π 3 ) ≤ d T (π 1 , π 2 ) + d T (π 2 , π 3 ) = u(θ 1,2 1 , θ 1,2 2 ) + u(θ 2,3 1 , θ 2,3 2 ) ≤ d L (s 1 , s 2 ) + d L (s 2 , s 3 ) + ε (1)
As θ 1,3 1 ∈ Θ1,3 1 was chosen arbitrarily, we have sup

θ 1 ∈ Θ1,3 1 inf θ 2 ∈Θ 1,3 2 u(θ 1 , θ 2 ) ≤ d L (s 1 , s 2 ) + d L (s 2 , s 3 ) + ε
and as also ε was chosen arbitrarily,

d L (s 1 , s 3 ) ≤ d L (s 1 , s 2 ) + d L (s 2 , s 3 ).
For branching distance, we cannot construct the paths in a one-shot manner as above, as the transitions chosen by Player 1 may depend on the history of the play. Let again ε > 0; assuming that the simulation game is determined, we can choose Player-2 strategies

θ 1,2 2 ∈ Θ 1,2 2 , θ 2,3 2 ∈ Θ 2,3 2 for which sup θ 1 ∈Θ 1,2 1 u(θ 1 , θ 1,2 2 ) < d B (s 1 , s 2 ) + ε 2 and sup θ 1 ∈Θ 2,3 1 u(θ 1 , θ 2,3 2 ) < d B (s 2 , s 3 ) + ε 2 .
Intuitively, we will use these strategies to allow Player 2 to find replying moves to Player-1 moves in the game computing d B (s 1 , s 2 ) by using the reply given by θ 2, 3 2 to the reply given by θ 1,2 2 . Hence we still follow the proof strategy depicted in Figure 1, but now for individual moves.

The strategy θ 1,3 2 uses a finite path m = π 2 ∈ fPa(s 2 ) as memory and is defined by

θ 1,3 2 (π 1 , π 3 )(π 2 ) = θ 2,3 2 π 2 • θ 1,2 2 (π 1 , π 2 ), π 3 with memory update m(π 1 , π 3 )(π 2 ) = π 2 • θ 1,2 2 (π 1 , π 2 ).
The initial memory for θ 1,3 2 is set to be the empty path, hence as the game progresses, a path π 2 ∈ Pa(s 2 ) is constructed. Now choose some θ 1,3 1 ∈ Θ 1,3 1 , and let π 1 ∈ Pa(s 1 ) and π 3 ∈ Pa(s 3 ) be the paths constructed by the strategy profile (θ 1, 3 1 , θ 1,3 2 ). If π 2 ∈ Pa(s 2 ) is the corresponding memory path, then the pair (π 1 , π 2 ) is constructed by the strategy profile (θ 1, 3 1 , θ 1,2 2 ) and the pair (π 2 , π 3 ) by the profile (θ 1,2 2 , θ 2,3 2 ). Hence we can use the exact same reasoning as in [START_REF] Aceto | 2-Nested Simulation Is Not Finitely Equationally Axiomatizable[END_REF] to conclude that inf

θ 2 ∈Θ 1,3 2 u(θ 1,3 1 , θ 2 ) ≤ d B (s 1 , s 2 ) + d B (s 2 , s 3 ) + ε and hence d B (s 1 , s 3 ) ≤ d B (s 1 , s 2 ) + d B (s 2 , s 3 ).

Properties

The following general result confirms that, regardless of the trace distance chosen, the linear distance is always bounded above by the branching distance. In the context of the discrete trace distance from Section 2.2, this specializes to the well-known fact that simulation implies language inclusion.

Theorem 5. For any s,t ∈ S, we have d L (s,t) ≤ d B (s,t).

Proof. Any Player-1 strategy in Θ1 is also in Θ 1 , hence sup

θ 1 ∈ Θ1 inf θ 2 ∈Θ 2 u(θ 1 , θ 2 ) ≤ sup θ 1 ∈Θ 1 inf θ 2 ∈Θ 2 u(θ 1 , θ 2 )
The game definition of linear distance yields the following explicit formula. Note the resemblance of this to the well-known Hausdorff construction for lifting a metric on a set to its set of subsets. Theorem 6. For all s,t ∈ S we have

d L (s,t) = sup σ ∈Tr(s) inf τ∈Tr(t) d T (σ , τ)
Proof. The definition of ṽ(s,t) immediately entails the fact that for any π 1 ∈ Pa(s) there exists π 2 ∈ Pa(t) such that d T (tr(π 1 ), tr(π 2 )) ≤ ṽ(s,t). It remains to show that ṽ(s,t) ≤ sup σ ∈Tr(s) inf τ∈Tr(t) d T (σ , τ). By blindness, any θ 1 ∈ Θ1 produces a unique path π 1 ∈ Pa(s) independent of the opponent strategy θ 2 ∈ Θ 2 . Hence we need only consider strategies θ 2 which define a single path π 2 from t, and the result follows.

We finish this section by exposing two properties regarding equivalence of the introduced hemimetrics. Transferring (in)equivalence of distances from one setting to another is an important subject, and we hope to show other results of the below kind, especially relating trace distance to branching distance, in future work. s Proof. This follows immediately from Theorem 6 and Theorem 3.87 in [START_REF] Charalambos | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF]. Note that the theorem in [START_REF] Charalambos | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF] actually is stronger; it is enough to assume d 1 T and d 2 T to be uniformly equivalent.

σ 0 = τ 0 τ 1 σ 1 σ 2 τ 2 t σ 0 τ 0 τ 1 σ 1 σ 2 τ 2
The next theorem shows that if a trace distance can be used for measuring trace differences beyond the first symbol (which will be the case except for some especially trivial trace distances), then the corresponding linear and branching distances are topologically inequivalent. The proof is an easy adaption of the standard argument for the fact that language inclusion does not imply simulation.

Definition 8. A trace distance d T : ❑ ω × ❑ ω is said to be one-step indiscriminate if σ 0 = τ 0 implies d T (σ , τ) = 0 for all σ , τ ∈ ❑ ω .
Proposition 9. If d T is not one-step indiscriminate, then there exists a weighted transition system A on which the corresponding distances d L and d B are topologically inequivalent.

Proof. Let σ , τ ∈ ❑ ω such that σ 0 = τ 0 , d T (σ , τ) > 0, and d T (τ, σ ) > 0. A is depicted in Figure 2.

We have Tr(s) = Tr(t), hence d L (s,t) = 0. On the other hand, d B (s,t) = min d T (σ , τ), d T (τ, σ ) > 0. As two equivalent hemimetrics have value 0 at the same set of pairs of points, this finishes the proof. Also note that if σ and τ are cyclic, the construction can be adapted to yield a finite WTS A.

Recursively Defined Distances

The game definition of branching distance in Definition 3 gives a useful framework, but it is not very operational. In this section we show that if the given trace distance has a recursive characterization, then the corresponding branching distance can be obtained as the least fixed point of a similar recursive formula.

We give the fixed-point theorem first and show in Section 3.1 below that the theorem covers all examples of distances introduced earlier.

Theorem 10. Let L be a complete lattice and f

: ❑ ω × ❑ ω → L, g : L → [0, ∞], F : ❑×❑×L → L such that d T = g • f , g is monotone, F(x, y, •) : L → L is monotone for all x, y ∈ ❑, and f (σ , τ) = F σ 0 , τ 0 , f (σ 1 , τ 1 ) (2)
Distances for Weighted Transition Systems for all σ , τ ∈ ❑ ω . Define I : L S×S → L S×S by

I(h)(s,t) = sup s x - →s ′ inf t y - →t ′ F x, y, h(s ′ ,t ′ )
Then I has a least fixed point h * : S × S → L, and d B = g • h * . Let us give some intuition about the theorem before we prove it. Note first the composition d T = g • f , where f maps pairs of traces to the lattice L which will act as memory in the applications below. Equation (2) then expresses that F acts as a distance iterator function which, within the lattice domain, computes the trace distance by looking at the first elements in the traces and then iterating over the rest of the trace. Under the premises of the theorem then, branching distance is the projection by g of the least fixed of a similar recursive function involving F. Proof. It is not difficult to show that I indeed has a least fixed point: The lattice L S×S with partial order defined point-wise by h 1 ≤ h 2 iff h 1 (s,t) ≤ h 2 (s,t) for all s,t ∈ S is complete, and I is monotone because of the monotonicity condition on F, hence Tarski's Fixed-point Theorem can be applied.

To show that d B = g • h * , we pull back d B along g: With the notation for the simulation game from Section 2.3, define f B (s,t) = sup

θ 1 ∈Θ 1 inf θ 2 ∈Θ 2 f tr(π 1 (θ 1 , θ 2 )), tr(π 2 (θ 1 , θ 2 ))
We have d B = g • f B by monotonicity of g, so it will suffice to show that f B = h * . Let us first prove that f B is a fixed point for I: Let s,t ∈ S, then

I( f B )(s,t) = sup s x - →s ′ inf t y - →t ′ F x, y, f B (s ′ ,t ′ ) = sup s x - →s ′ inf t y - →t ′ F x, y, sup θ ′ 1 ∈Θ ′ 1 inf θ ′ 2 ∈Θ ′ 2 f (tr(π 1 (θ ′ 1 , θ ′ 2 )), tr(π 2 (θ ′ 1 , θ ′ 2 ))) = sup s x - →s ′ inf t y - →t ′ sup θ ′ 1 ∈Θ ′ 1 inf θ ′ 2 ∈Θ ′ 2 F x, y, f (tr(π 1 (θ ′ 1 , θ ′ 2 )), tr(π 2 (θ ′ 1 , θ ′ 2 )))
(the last step by the monotonicity assumption on F; note that in the second sup-inf pair, strategies from s ′ and t ′ are considered). By the recursion formula (2) for F, we end up with

I( f B )(s,t) = sup s x - →s ′ inf t y - →t ′ sup θ ′ 1 ∈Θ ′ 1 inf θ ′ 2 ∈Θ ′ 2 f (x • tr(π 1 (θ ′ 1 , θ ′ 2 )), y • tr(π 2 (θ ′ 1 , θ ′ 2 )))
Now because of independence of choices, we can rewrite this to

I( f B )(s,t) = sup s x - →s ′ sup θ ′ 1 ∈Θ ′ 1 inf t y - →t ′ inf θ ′ 2 ∈Θ ′ 2 f (x • tr(π 1 (θ ′ 1 , θ ′ 2 )), y • tr(π 2 (θ ′ 1 , θ ′ 2 )))
and collapsing the sup-sup and inf-inf into one sup and inf, respectively, conclude

I( f B ) = f B .
To show that f B is the least fixed point for I, let h : S × S → L such that I( h) = h; we want to prove f B ≤ h. Note first that for all s,t ∈ S and all s x -→ s ′ , there is t y -→ t ′ such that F(x, y, h(s ′ ,t ′ )) ≤ I( h)(s,t). Now fix s,t ∈ S and let θ 1 ∈ Θ 1 ; we will be done once we can construct a Player-2 strategy θ 2 ∈ Θ 2 for which f (tr(π 1 (θ 1 , θ 2 )), tr(π 2 (θ 1 , θ 2 ))) ≤ h(s,t).

We have to define θ 2 for configurations (π ′ 1 , π 2 ) ∈ fPa(s) × fPa(t) in which π ′ 1 = π 1 • (s j , x, s j+1 ) and len(π 1 ) = len(π 2 ). Write last(π 2 ) = t j ; by the note above, we can choose a transition t j y -→ t j+1 for which F(x, y, h(s ′ ,t ′ )) ≤ I( h)(s,t), so we let θ 2 (π ′ 1 , π 2 ) = (t j , y,t j+1 ). The so-defined strategy has f (tr(π

1 (θ 1 , θ 2 )), tr(π 2 (θ 1 , θ 2 ))) ≤ sup s x - →s ′ inf t y - →t ′ F(x, y, h(s ′ ,t ′ )) = h(s,t)

Applications

We reconsider here the example trace distances from Section 2.2 and exhibit the corresponding linear and branching distances.

Discrete trace distances. For the discrete trace distance on ❑ ω given by d T (σ , τ) = 0 if σ = τ and d T (σ , τ) = ∞ otherwise, we saw already in Section 2.4 that we recover ordinary trace inclusion and simulation. For linear distance, we can also use Theorem 6 to show that d L (s,t) = 0 if Tr(s) ⊆ Tr(t) and d L (s,t) = ∞ otherwise.

For the branching distance, we can now also apply Theorem 10 with L = [0, ∞], g the identity mapping, and F(x, y, z) = z if x = y, F(x, y, z) = ∞ otherwise. Then the branching distance is the least fixed point of the equations d B (s,t) = sup s [START_REF] Milner | Communication and Concurrency[END_REF], and d B (s,t) = ∞ otherwise.

x - →s ′ inf t x - →t ′ d B (s ′ ,t ′ ), hence d B (s,t) = 0 if t simulates s in the stan- dard sense
For the refined discrete trace distance d T (σ , τ) = 0 if σ j ⊑ τ j for all j, d T (σ , τ) = ∞ otherwise, we analogously get d L (s,t) = 0 if all σ ∈ Tr(s) can be refined by a τ ∈ Tr(t) (i.e. σ j ⊑ τ j for all j) and d L (s,t) = ∞ otherwise. Also, d B (s,t) = 0 if there is a relation R ⊆ S × S for which (s,t) ∈ R and whenever (s ′ ,t ′ ) ∈ R and s ′ x -→ s ′′ , then also t ′ y -→ t ′′ with x ⊑ y and (s ′′ ,t ′′ ) ∈ R (the extended simulation of [START_REF] Thomsen | An Extended Bisimulation Induced by a Preorder on Actions[END_REF]), and d B (s,t) = ∞ otherwise.

Hamming distance. For Hamming distance induced by the metric d(x, y) = 0 if x = y and d(x, y) = 1 otherwise on ❑, linear distance is given by d L (s,t) ≤ k if and only if any trace σ ∈ Tr(s) can be matched by a trace τ ∈ Tr(t) with Hamming distance at most k, both for the limit-average and the discounting interpretation. The branching distance associated with the discounting version is precisely the (discounted) correctness distance of [START_REF] Černý | Simulation Distances[END_REF]: d B (s,t) measures "how often [the system starting in s 2 ] can be forced to cheat", i.e. to take a transition different from the one the system starting in s 1 takes.

Labeled weighted transition systems. For the trace distances on labeled weighted transition systems, let us for simplicity assume that |Σ| = 1, hence ❑ = |. For the point-wise trace distance d T (σ , τ) = sup j |σ jτ j | we can derive a recursive formula for the corresponding branching distance by applying Theorem 10 with L = [0, ∞], g the identity mapping, and F(x, y, z) = max |x -y|, z). Then d B is the least fixed point to the equations

d B (s,t) = sup s x - →s ′ inf t y - →t ′ max |x -y|, d B (s ′ ,t ′ )
For discounted accumulated trace distance d T (σ , τ) = ∑ j λ j |σ jτ j |, we can similarly let F(x, y, z) = |x -y| + λ z, then the corresponding branching distance is the least fixed point to the equations

d B (s,t) = sup s x - →s ′ inf t y - →t ′ |x -y| + λ d B (s ′ ,t ′ )
Note that these two branching distances are exactly the ones the authors define in [START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF].

For the maximum-lead distance d T (σ , τ) = sup j ∑ j i=0 σ i -∑ j i=0 τ i , we need to do more work. Intuitively, a recursive formulation needs to keep track of the accumulated delay, hence needs (infinite) memory. This can be accomplished by letting L = [0, ∞] [-∞,∞] ; the set of functions from leads to dis-tances. We can then define

f (σ , τ)(δ ) = max |δ |, ∞ sup j=0 |δ + j ∑ i=0 σ j - j ∑ i=0 τ j |
and g(h) = h(0). Now with F(x, y, h)(δ ) = max |δ + x -y|, h(δ + xy) , we indeed have that f (σ , τ) = F σ 0 , τ 0 , f (σ 1 , τ 1 ) , hence we can apply Theorem 10 to conclude that d B (s,t) = h * (s,t)(0), where h * is the least fixed point to the equations h(s,t)(δ ) = sup This is precisely the formulation of branching maximum-lead distance given in [START_REF] Henzinger | Quantifying Similarities Between Timed Systems[END_REF].

Conclusion and Future Work

We have shown that simulation games with quantitative objectives provide a general framework for studying linear and branching distances for quantitative systems. Specifically, that our framework covers and unifies a number of previously distinct approaches, and that certain common special cases lead to useful recursive characterizations of branching distance.

Already we have seen that one very general property, topological inequivalence of linear and branching distance, follows almost immediately from the game characterization. Also this general approach permits the conclusion that independent of the trace distance, the branching distance provides an upper bound on the linear distance, a property which is useful for applications such as analysis of real-time systems, where linear distances are known to be uncomputable [START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF].

It seems likely that by permitting a broader range of strategies, we may encompass more advanced levels of system interaction and observations, and hence capture quantitative extensions of other wellknown system relations such as 2-nested simulation [START_REF] Aceto | 2-Nested Simulation Is Not Finitely Equationally Axiomatizable[END_REF][START_REF] Friso Groote & Frits | Structured Operational Semantics and Bisimulation as a Congruence[END_REF] or bisimulation [START_REF] Milner | Communication and Concurrency[END_REF]. Thus, we expect our framework to be of great use for reasoning about, and applying quantitative verification.

The game perspective on linear and branching distances also suggests that several interesting results and properties of games with quantitative objectives are transferable to our setting. As an example, one may consider computability and complexity results: For a concrete setting such as finite weighted labeled automata, discounted or limit average accumulating distances can be computed using discounted and mean-payoff games, respectively. Hence the complexity of computing these branching distances is in NP ∩ coNP. Similarly, results concerning strategy iteration or value iteration for games with quantitative objectives may be transferred to the distance setting.

Figure 1 :

 1 Figure 1: Construction of strategies in the proof of Proposition 4

Proposition 7 (

 7 cf.[START_REF] Charalambos | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF] Thm. 3.87]). If trace distances d 1 T and d 2 T are Lipschitz equivalent, then the corresponding linear distances d 1 L and d 2 L are topologically equivalent.

Figure 2 :

 2 Figure 2: Weighted transition system for the proof of Proposition 9

  |δ + x -y|, h(s ′ ,t ′ )(δ + xy)

Acknowledgment

The authors acknowledge interesting and fruitful discussions on the topic of this work with Tom Henzinger, Pavol Černý and Arjun Radhakrishna of IST Austria.


Uli Fahrenberg

Kim G Larsen

Claus Thrane

Model-based Verification and Analysis for Real-Time Systems

Keywords: Timed automata, regions, zones, reachability, bisimilarity, priced and weighted timed automata, optimal reachability, optimal infinite runs, conditional optimality, timed games, winning strategies

. 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, and the existence of winning strategies.

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 applied 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], 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, and the existence of winning strategies. 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 edition of this survey [START_REF] Fahrenberg | Verification, performance analysis and controller synthesis 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.

Syntax and semantics

Definition 2.1. The set Φ(C) of clock constraints ϕ over a finite set (of clocks) C is defined by the grammar

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

ϕ ::= x k | x -y k | ϕ 1 ∧ ϕ 2
x ≤ 3

x := 0 press?

x > 3

x := 0

x = 100

x := 0 press?

x := 0

x = 100 x := 0 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.

(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 R C ≥0 . Definition 2.5. The zone of an extended clock constraint in Φ + (C) is a set of clock valuations C → R ≥0 given inductively by x k = {v : C → R ≥0 | v(x) k}, x -y k = {v : C → R ≥0 | v(x) -v(y) k}, and
ϕ 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 , Σ ∪ R ≥0 , T = T s ∪ T d ) given as follows: S = ( , v) ∈ L × R 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 R ≥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 .
S = {Off} × R ≥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":

(Off, 0) 150 --→ (Off, 150) p -→ (Light, 0) 100 --→ (Light, 100) - → (Off, 0) (Off, 0) p -→ (Light, 0) 10 -→ (Light, 10) p -→ (Light, 0) 100 --→ (Light, 100) - → (Off, 0) (Off, 0) p -→ (Light, 0) 1 -→ (Light, 1) p -→ (Bright, 0) 100 --→ (Bright, 100) - → (Off, 0) 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 → R ≥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 × R C ≥0 × L × R 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 × R C ≥0 × L × R C
≥0 a time-abstracted bisimulation which is also an equivalence.

The quotient of A = (S, s 0 , Σ ∪ R ≥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 ([4]). Let A = (L, 0 , F, C, Σ, I, E) be a timed automaton, R ⊆ 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.

L × R C ≥0 × L × R C ≥0 an F -
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 → Z Φ(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 → Z defined by c A (x) = max c max (x)(I( )), c max (x)(ϕ) ∈ L, ϕ,a,r ---→ ∈ E .
C → R ≥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 ([4]). 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 ([8]

). 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 × 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 -→ ( 1 , v 1 ), d ∈ R ≥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 ∪ R ≥0 , T A ), B = (S B , s B 0 , Σ B ∪ R ≥0 , T B ) associated with timed automata A, B is A × B = (S, s 0 , Σ A ∪ Σ B ∪ R ≥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 ∈ R ≥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 ∈ R ≥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. 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 ∈ R ≥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. Definition 2.32. A timed trace ((t 1 , a 1 ), . . . , (t k , a k )) is accepted by a timed automaton 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}.
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.

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 may 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 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. 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 ∈ R ≥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 ([8]). 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 ([8]). 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 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.

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 5
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 ⊆ R 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 ∈ R ≥0 } and • the reset of Z under r by Z[r] = {v[r] | v ∈ Z}.
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 ⊆ R 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 ([72]). 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 ⊆ R 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 employing normalization, using the fact that region equivalence ∼ = has finitely many equivalence classes: Definition 2.43. For a timed automaton A and a zone

Z ⊆ R C ≥0 , the normalization of Z is the set {v : C → R ≥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 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 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].

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]. I,E,R,P ),where (L,0 ,F,C,Σ,I,E) is a timed automaton, R : L → Z a location weight-rate mapping, and P : E → Z an edge weight mapping.

Definition 3.1. A weighted timed automaton is a tuple A = (L, 0 , F, C, Σ,
The semantics of A is the weighted transition system A = (S, s 0 , Σ ∪ R ≥0 , T, w), where (S, s 0 , Σ ∪ R ≥0 , T ) is the semantics of the underlying timed automaton (L, 0 , F, C, Σ, I, E), and the transition weights w : T → R are given as follows: We shall denote weighted edges and transitions by symbols e -→ w to illustrate an edge or a transition labeled e with weight w.

w ( , v) d -→ ( , v + d) = d R( ) w ( , v) a -→ ( , v ) = P ϕ,a,r ---→ with v |= ϕ, v = v[r] 1 R = 4 2 R = 2

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} → R ≥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 re-gion 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 ([18]). 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.

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 → Z 2 a location weightrate mapping, and P : E → Z 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

R = (1, 4) x ≤ 2 1 R = (2, 1)
x ≤ 3 ( 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 ∈ Z, 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 ([60, 61]). 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].

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.

--→ 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 λ. 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 Figure 12.
A timed game with one clock. Controllable edges (with actions from Σc) are solid, uncontrollable edges (with actions from Σu) are dashed.

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. Edges with actions in Σ c are said to be controllable, those with actions in Σ u are uncontrollable.

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

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

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 , I, E) is said to be an outcome of a strategy σ provided that • 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 ([12, 65]). 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 9.

Proof: Given timed automata A i = (L i , i 0 , F, C i , Σ, I i , E i ), for i ∈ {1, 2}, with ϕ,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}.

C 1 ∩ C 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 -→ 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 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.

  (x, y ∈ C, k ∈ Z, ∈ {≤, <, ≥, >}).

Figure 1 .

 1 Figure 1. A light switch modelled as a timed automaton.

Definition 2 . 4 .

 24 A clock valuation on a finite set C of clocks is a mapping v : C → R ≥0 . The initial valuation v 0 is given by v 0 (x) = 0 for all x ∈ C. For a valuation v, d ∈ R ≥0 , and r ⊆ C, the valuations v + d and v[r] are defined by

Example 2 . 1 (

 21 continued). The light switch model from figure 1 has as state set

Figure 2 .

 2 Figure 2. A timed automaton with two clocks.

2 4 x 2 yFigure 4 .

 24 Figure 4. Clock regions for the timed automaton from Example 2.2. Notation 2.15. For d ∈ R ≥0 we write d and d for the integral, respectively fractional, part of d, so that d = d + d . Definition 2.16. 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.

Proposition 2 . 29 .

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

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 .

 2 40 ([48, 72]). 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[START_REF] Kim | Efficient verification of real-time systems: compact data structure and state-space reduction[END_REF].

Figure 8 .

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

Figure 9 .

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

Figure 10 .

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

1 Figure 11 .Definition 3 . 6 .

 11136 Figure 11. A weighted timed automaton modelling a simple production system. Definition 3.6. The total ratio of a finite run ρ = s 0 w1

Definition 4 . 1 .

 41 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.

  we consider the timed game with locationsL = {⊥} ∪ (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)

ΦFigure 13 .

 13 Figure 13. A timed game constructed for bisimilarity checking of two simple timed automata

  sensitive time-abstracted bisimulation and ∈ F . Then ∈ Reach(A) if and only if there is a reachable state π in A R and v : C → R ≥0

	y		y
	{b}	∅
	2		2
	{a, b}	{a}	{a, c}
	2	4	x	2	4	x
	Figure 3. Time-abstracted bisimulation classes for the two-clock timed automaton from Exam-
	ple 2.2. Left: equivalence classes for switch transitions only; right: equivalence classes for switch
	and delay transitions.
	such that ( , v) ∈ π.
	Example 2.2 (continued). We shall now try to construct, in a naïve way, a time-
	abstracted 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 → R ≥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 → R ≥0 , which leaves us with
	constructing R on the states involving 0 . We handle switch transitions α -→ first: If v, v : C → R ≥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