Frédéric Herbreteau

B Srivathsan

Igor Walukiewicz

Better Abstractions for Timed Automata $

Keywords: Timed automata, reachability problem, non-convex abstractions

We study the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstractions preserve underlying simulation relations on the state space of the automaton. For both effectiveness and efficiency reasons, they are parameterized by the maximal lower and upper bounds (LU -bounds) occurring in the guards of the automaton.

One such abstraction is the a LU abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets, it has not been used in implementations. Firstly, we prove that a LU abstraction is the coarsest abstraction with respect to LU -bounds that is sound and complete for reachability. Secondly, we provide an efficient technique to use the a LU abstraction to solve the reachability problem.

Introduction

Timed automata are finite automata extended with clocks whose values can be compared with constants and set to zero. The clocks measure delays between different steps of execution of the automaton. The reachability problem for timed automata asks if there exists a path from its initial state to a given target state. This problem cannot be solved by a simple state exploration since clocks are real-valued variables. The standard solution to this problem involves computing the zone graph of the automaton which in principle could be infinite. In order to make it finite, zones are approximated using an abstraction operator. Till recently it has been generally assumed that for reasons of efficiency an abstraction of a zone should always be a zone. Here we avoid this assumption.

We first show that a LU abstraction defined by Behrmann et al. [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] is the coarsest sound and complete abstraction. We then present a method of constructing the abstracted zone graph using the a LU abstraction. Even though this abstraction can yield non-convex sets, we show that our method is at least as efficient as any other currently known method based on abstractions.

The reachability problem is a basic problem in verification. It is historically the first problem that has been considered for timed-automata, and it is still a lively subject of research [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF][START_REF] Wang | Efficient verification of timed automata with bdd-like data structures[END_REF][START_REF] Morbé | Fully symbolic model checking for timed automata[END_REF][START_REF] Herbreteau | Using non-convex approximations for efficient analysis of timed automata[END_REF]. Apart from being interesting by itself, the advances on this problem may give new methods for verification of more complicated models, like priced timed-automata [START_REF] Bouyer | Quantitative analysis of real-time systems using priced timed automata[END_REF], or probabilistic timed automata [START_REF] Gregersen | Formal design of reliable real time systems[END_REF][START_REF] Bouyer | From Qualitative to Quantitative Analysis of Timed Systems[END_REF][START_REF] Kwiatkowska | Automatic verification of real-time systems with discrete probability distributions[END_REF].

All approaches to solving the reachability problem for timed automata should ensure termination. To tackle this, most of them use abstractions to group together bisimilar valuations of clock variables, that is, valuations not distinguishable by the automaton as far as reachability to the final state is concerned. The first solution has been based on regions, which are certain equivalence classes of clock valuations [START_REF] Alur | A theory of timed automata[END_REF]. Their definition is parameterized by a threshold up to which the clock values should be considered. A great improvement in efficiency has been obtained by adopting zones instead of regions. These are sets of valuations defined by conjunctions of differences between pairs of clocks. They can be efficiently implemented using difference bound matrices (DBMs) [START_REF] Berthomieu | An enumerative approach for analyzing time petri nets[END_REF][START_REF] David | Timing assumptions and verification of finite-state concurrent systems[END_REF]. A challenge with zone based approach is that they are not totally compatible with regions, and moreover a forward exploration algorithm can produce infinitely many zones. The union of regions intersecting a zone is a natural candidate for a finitary abstraction. Indeed this abstraction would make the forward exploration algorithm terminate. However such an union of regions is not necessarily a zone and so it is not clear how to represent it. For this reason a number of abstraction operators have been proposed that give an approximation of the union of regions intersecting a zone. A coarser approximation would make the abstracted zone graph smaller. So potentially it would give a more efficient algorithm.

An important observation made in [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] is that if reachability is concerned then we can consider simulation instead of bisimulation. Indeed, it is safe to add configurations that can be simulated by those that we have already reached. Simulation relations in question depend on the given automaton, and it is Exptime-hard to calculate the biggest one [START_REF] Laroussinie | The state explosion problem from trace to bisimulation equivalence[END_REF]. A pragmatic approach is to abstract some part of the structure of the automaton and define a simulation based on this information. The most relevant information is the set of bounds with which clocks are compared to in the guards of the automaton. Since lower and upper bounds are considered separately, they are called LU -bounds. In [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] the authors define an abstraction based on simulation with respect to LUbounds; it is denoted a LU . Theoretically a LU is very attractive: it has clear semantics and, as we show here, it is always a union of regions. The problem is that a LU abstraction of a zone is seldom a convex set, so one cannot represent the result as a zone.

In this paper we give another very good reason to consider a LU abstraction. We show that it is actually the coarsest abstraction that is sound and complete with respect to reachability for all automata with the same LU -bounds. In other words, it means that in order to get coarser (that is better) abstractions one would need to look at some other structural properties of automata than just LU -bounds. Our main technical result is an effective algorithm for dealing with a LU abstraction. It allows to manipulate this abstraction as efficiently as purely zone based ones. We propose a forward exploration algorithm working with zones that constructs the a LU abstraction of the transition graph of the automaton. This algorithm uses standard operations on zones, plus a new test of inclusion of a zone in the a LU abstraction of another zone. The test is quadratic in the number of clocks and not more complex than that for just testing an inclusion between two zones. Since a LU abstraction is the coarsest sound and complete abstraction, it can potentially give smallest abstract systems.

Related Work

Forward analysis is the main approach for the reachability testing of realtime systems. The use of zone-based abstractions for termination has been introduced in [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF]. In recent years, coarser abstractions have been introduced to improve efficiency of the analysis [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]. An approximation method based on LUbounds, called Extra + LU , is used in the current implementation of UPPAAL [START_REF] Behrmann | UPPAAL 4.0[END_REF]. In [START_REF] Herbreteau | Using non-convex approximations for efficient analysis of timed automata[END_REF] it has been shown that it is possible to efficiently use the region closure of Extra + LU , denoted Closure + LU . This has been the first efficient use of a nonconvex abstraction. In comparison, a LU approximation has a well-motivated semantics, it is also region closed, coarser than Closure + LU and the resulting inclusion test is even simpler than that of Closure + LU . A comparison of these abstractions is depicted in Fig. 1.

Let us mention that abstractions are not needed in backward exploration of timed systems. Nevertheless, any feasible backward analysis approach needs to simplify constraints. For example [START_REF] Morbé | Fully symbolic model checking for timed automata[END_REF] does not use approximations and relies on an SMT solver instead. Clearly this approach is very difficult to compare with the forward analysis approach we study here.

Another related approach to verification of timed automata is to build a quotient graph of the semantic graph of the automaton with respect to some bisimulation relation [START_REF] Tripakis | Analysis of timed systems using timeabstracting bisimulations[END_REF][START_REF] Alur | Minimization of timed transition systems[END_REF][START_REF] Yannakakis | An efficient algorithm for minimizing real-time transition systems[END_REF]. For reachability properties, this approach is not a priori competitive with respect to using the simulation-based abstraction a LU . It is more adapted to checking branching time properties.

Organization of the Paper

The paper is organized as follows.

Section 2 presents the preliminary definitions. It introduces the notion of sound and complete abstractions parameterized by LU-bounds. It also explains how these abstractions could be used to solve the reachability problem.

Section 3 proposes abs LU abstraction, and proves that it is the coarsest sound and complete abstraction for all automata with given LU -bounds.

Section 4 shows that the a LU abstraction actually coincides with this coarsest abstraction abs LU .

Section 5 presents an efficient inclusion test for a LU abstraction, which allows for its use in implementations.

A preliminary version of this paper appeared in the conference on Logic in Computer Science [START_REF] Frédéric Herbreteau | Better abstractions for timed automata[END_REF]. This version includes all missing proofs and gives a more elaborate discussion about the inclusion test (Section 5).

Preliminaries

After recalling some preliminary notions, we introduce a concept of abstraction as a means to reduce the reachability problem for timed-systems to the one for finite systems. We then observe that simulation relation is a convenient way of obtaining abstractions with good properties.

Timed automata and the reachability problem

Let X be a set of clocks, i.e., variables that range over R ≥0 , the set of nonnegative real numbers. A clock constraint is a conjunction of constraints x#c for x ∈ X, # ∈ {<, ≤, =, ≥, >} and c ∈ N, e.g. (x ≤ 3 ∧ y > 0). Let Φ(X) denote the set of clock constraints over clock variables X. A clock valuation over X is a function v : X → R ≥0 . We denote by R X ≥0 the set of clock valuations over X, and by 0 the valuation that associates 0 to every clock in X. We write v φ when v satisfies φ ∈ Φ(X), i.e. when every constraint in φ holds after replacing every x by v(x). For δ ∈ R ≥0 , let v + δ be the valuation that associates v(x) + δ to every clock x. For R ⊆ X, let [R]v be the valuation that sets x to 0 if x ∈ R, and that sets x to v(x) otherwise.

A Timed Automaton (TA) is a tuple A = (Q, q 0 , X, T, Acc) where Q is a finite set of states, q 0 ∈ Q is the initial state, X is a finite set of clocks, Acc ⊆ Q is a set of accepting states, and T ⊆ Q × Φ(X) × 2 X × Q is a finite set of transitions (q, g, R, q ) where g is a guard, and R is the set of clocks that are reset on the transition.

The semantics of A is a transition system of its configurations. A configuration of A is a pair (q, v) ∈ Q × R X ≥0 and (q 0 , 0) is the initial configuration. We have two kinds of transitions: Delay: (q, v) → δ (q, v + δ) for some δ ∈ R ≥0 ; Action: (q, v) → t (q , v ) for some transition t = (q, g, R, q ) ∈ T such that v g and v = [R]v.

We will denote by S A the transition system describing the semantics of a timed automaton A. In this paper we are interested in the reachability problem: does there exist a configuration (q, v) with accepting state q ∈ Acc that is reachable from (q 0 , 0) by some finite sequence of delay and action transitions?

The class of TA we consider is usually known as diagonal-free TA since clock comparisons like x -y ≤ 1 are disallowed. Notice that if we are interested in state reachability, considering timed automata without state invariants does not entail any loss of generality as the invariants can be added to the guards. For state reachability, we can also consider automata without transition labels.

Abstractions

Since the transition system determined by the automaton is infinite, we usually try to find a finite approximation of it by grouping valuations together. In consequence we work with configurations consisting of a state and a set of valuations. For every transition t, we have a transition:

(q, W ) ⇒ t (q , W ) where W = {v : ∃v ∈ W, ∃δ ∈ R ≥0 s.t. v → t → δ v }
We will write ⇒ without superscript to denote the union of all ⇒ t relations. The transition relation defined above considers each valuation v ∈ W that can take the transition t, obtains the valuation after the transition, and then collects the time-successors from this obtained valuation. Therefore the symbolic transition ⇒ always yields sets closed under time-successors.

The initial configuration of the automaton is (q 0 , 0). Starting from the initial valuation 0 the set of valuations reachable by a time elapse at the initial state are given by {0 + δ | δ ∈ R ≥0 }. Call this W 0 .

From (q 0 , W 0 ) as the initial node, computing the symbolic transition relation ⇒ leads to different nodes (q, W ) wherein the sets W are closed under timesuccessors. Although the transition relation ⇒ talks about sets of valuations and not valuations themselves, it could still be potentially infinite. A further grouping of valuations is necessary to get finiteness.

An abstraction operation [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF] is a convenient way of expressing a grouping of valuations. It is a function a :

P(R |X| ≥0 ) → P(R |X| ≥0
) such that W ⊆ a(W ) and a(a(W )) = a(W ). An abstraction operator defines an abstract semantics:

(q, W ) ⇒ a (q , a(W ))
where a(W ) = W and (q, W ) ⇒ (q , W ).

If a has a finite range then this abstraction is said to be finite. We write ⇒ * a for the transitive closure of ⇒, similarly we write ⇒ * and → * respectively for the transitive closure of ⇒ and → (where → denotes the union of → t and → δ ).

Of course we want this abstraction to reflect some properties of the original system. In order to preserve reachability properties we can require the following two properties (recall that 0 ∈ W 0 ): Soundness: if (q 0 , a(W 0 )) ⇒ * a (q, W ) then there is a v ∈ W such that (q 0 , 0) → * (q, v). Completeness: if (q 0 , 0) → * (q, v) then there is a W such that v ∈ W and (q 0 , a(W 0 )) ⇒ * a (q, W ). It can be easily verified that if an abstraction satisfies W ⊆ a(W ) then the abstracted system is complete. However soundness is more delicate to obtain.

Naturally, it is important to be able to efficiently compute the abstract transition system. A standard way to do this is to use zones. A zone is a set of valuations defined by a conjunction of two kinds of constraints: comparison of differences between two clocks with an integer like x -y#c, or comparison of a single clock with an integer like x#c, where # ∈ {<, ≤, =, ≥, >} and c ∈ N. For instance (x -y ≥ 1) ∧ (y < 2) is a zone. Zones can be efficiently represented using difference bound matrices (DBMs) [START_REF] Berthomieu | An enumerative approach for analyzing time petri nets[END_REF][START_REF] David | Timing assumptions and verification of finite-state concurrent systems[END_REF]. This suggests that one should consider abstractions that give zones. As zones are convex, abstractions that range over zones are called convex abstractions. This is an important restriction as abstractions based on regions are usually not convex [START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF].

We propose a way to use non-convex abstractions and zone representations at the same time. We will only consider sets W of the form a(Z) and represent them simply by Z. This way we can represent states of an abstract transition system efficiently: we need just to store a zone. In order for this to work we need to be able to compute the transition relation ⇒ a on this representation. We also need to know when two zone representations stand for the same node in the abstract system. This is summarized in the following two requirements: Transition compatibility: for every transition (q, a(Z)) ⇒ a (q , W ) and the matching transition (q, Z) ⇒ (q , Z ) we have W = a(Z ). Efficient inclusion test: for every two zones Z, Z , the test Z ⊆ a(Z) is efficient. Ideally, it has the same complexity O(|X| 2 ) as the inclusion Z ⊆ Z.

The first condition is quite easy to satisfy: We will show quickly below that every abstraction relation coming from time-abstract simulation [START_REF] Tasiran | Verifying abstractions of timed systems[END_REF] is transition compatible. The second condition is the main topic of the paper.

Definition 1 (Time-abstract simulation) A (state based) time-abstract simulation between two states of a transition system S A is a relation (q, v) t.a. (q , v ) such that:

• q = q ,
• if (q, v) → δ (q, v + δ) → t (q 1 , v 1 ), then there exists a δ ∈ R ≥0 such that (q, v ) → δ (q, v + δ ) → t (q 1 , v 1 ) satisfying (q 1 , v 1 ) t.a. (q 1 , v 1 ).

For two valuations v, v , we say that v t.a. v if for every state q of the automaton, we have (q, v) t.a. (q , v ). An abstraction a t.a. based on a simulation t.a. can be defined as follows:

Definition 2 (Abstraction based on simulation) Given a set W , we define a t.a. (W ) = {v | ∃v ∈ W. v t.a. v }.

Definition 3 (Timed-elapsed zone) A zone Z is said to be time-elapsed if it is closed under time-successors: that is

Z = {v + δ | v ∈ Z, δ ∈ R ≥0 }.
We had previously noted that all nodes (q, W ) reachable through ⇒ * from the initial node (q 0 , W 0 ) are all time elapsed. We can now show that transition relations coming from abstractions based on time-abstract simulations satisfy the transition compatibility condition.

Lemma 4 Let a t.a. be an abstraction based on a time-abstract simulation relation and let Z be a time-elapsed zone. For every transition (q, a t.a. (Z)) ⇒ a t.a. (q , W ) and the matching transition (q, Z) ⇒ (q , Z ), we have W = a t.a. (Z ).

Proof

Let t be the transition corresponding to ⇒ a t.a. and ⇒. We first prove that W ⊆ a t.a. (Z ). Let v ∈ W . We will show that there exists a valuation in Z that simulates v with respect to t.a. . By the definition of the abstract symbolic transition (q, a t.a. (Z)) ⇒ a t.a. (q , W ), there is a valuation v 1 ∈ a t.a. (Z) and a time elapse δ 1 ∈ R ≥0 such that:

(q, v 1 ) → t → δ1 (q , v 1 ) and v t.a. v 1 Firstly consider the intermediate configuration obtained after the → t transition from (q, v 1 ). Call it (q , v 1 ). We know that v 1 ∈ W . This valuation v 1 can elapse a time δ 1 and become v 1 . Given that t.a. is a time-abstract simulation, this intermediate valuation v 1 can simulate v too: (q, v 1 ) → t (q , v 1 ) and v t.a. v 1

Recall that v 1 ∈ a t.a. (Z). Therefore, there exists a valuation v 2 ∈ Z such that v 1 t.a. v 2 . As (q, v 1 ) can take the transition → t , by definition of time-abstract simulation, there exists a time elapse δ 2 such that (q, v 2 ) can take the transition after the time elapse δ 2 :

(q, v 2 ) → δ2 → t (q , v 2 ) and v 1 t.a. v 2 (2)
From ( 1) and (2), we see that v t.a. v 2 . Note that as Z is a time-elapsed zone and since v 2 ∈ Z, we also have v 2 + δ 2 ∈ Z and this in turn implies that v 2 ∈ Z . This shows that v ∈ a t.a. (Z ) and hence W ⊆ a t.a. (Z ).

We will now show the converse: a t.a. (Z ) ⊆ W . Let v ∈ a t.a. (Z ). Then, there exists v 1 ∈ Z and a δ 1 ∈ R ≥0 such that (q, v 1 ) → t → δ1 (q , v 1 ) and v t.a. v 1 . By the property of an abstraction operator, we will have v 1 ∈ a t.a. (Z) too. Now, directly by the definition of (q, a t.a. (Z)) ⇒ a t.a. (q , W ), we get that v ∈ W and hence a t.a. (Z ) ⊆ W . This paper is essentially about how to satisfy the "efficient inclusion test" condition and get as good abstraction as possible at the same time. In this context, let us highlight an important remark that describes when an abstraction is better than another.

Remark 5 If a and b are two abstractions such that for every set of valuations W , we have a(W ) ⊆ b(W ), we prefer to use b since the graph induced by it is a priori smaller than the one induced by a (sic [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]). In such a case, the abstraction b is said to be coarser than abstraction a.

Bounds as parameters for abstraction

Remark 5 suggests to make use of the coarsest possible abstraction. For a given automaton it can be computed if two configurations are in a simulation relation. It should be noted though that computing the biggest simulation relation is Exptime-hard [START_REF] Laroussinie | The state explosion problem from trace to bisimulation equivalence[END_REF]. Since the reachability problem can be solved in Pspace, this suggests that it may not be reasonable to try to solve it using the abstraction based on the biggest simulation.

We can get simulation relations that are computationally easier if we consider only a part of the structure of the automaton. The simplest is to take a simulation based on the maximal constant that appears in guards. More refined is to take the maximum separately over constants from lower bound constraints, that is in guards of the form x > c or x ≥ c, and those from upper bound constraints, that is in guards x < c or x ≤ c. If one moreover does this for every clock x separately, one gets for each clock two integers L x and U x . The abstraction that is currently most used is a refinement of this method by calculating L x and U x for every state of the automaton separately [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF]. For simplicity of notation we will not consider this optimization but it can be incorporated with no real difficulty in everything that follows. We summarize this presentation in the following definition.

Definition 6 (LU-bounds)

The L bound for an automaton A is the function assigning to every clock a maximal constant that appears in a lower bound guard for x in A. Similarly U but for upper bound guards. An LU-guard is a guard where lower bound guards use only constants bounded by L and upper bound guards use only constants bounded by U . An LU-automaton is an automaton using only LU-guards.

In the rest of the paper, we try to find good abstractions parameterized by LU-bounds that also have an efficient inclusion test. Section 3 defines an abstraction abs LU and proves that this is the optimal sound and complete abstraction that is based on LU-bounds. Section 4 then shows that the a LU abstraction is the same as abs LU when zones closed under time successors are considered. We then give an efficient test Z ⊆ a LU (Z ) in Section 5, which enables the use of a LU in implementations.

The coarsest LU abstraction

We call an abstraction that is based on LU bounds an LU abstraction. A natural question is to know what is the coarsest LU-abstraction sound and complete for reachability testing. Given L and U bounds, we know that the automata under consideration have guards only of the following form (with ∈ {<, ≤} and ∈ {>, ≥}) :

x 0, x 1 , . . . , x L x x 0, x 1 , . . . , x U x
However, we do not know the shape of the automata, in particular, the order in which the above guards appear in the paths of the automata. An abstraction a is sound if for every possible path using the above guards that a valuation v ∈ a(W ) can execute, there is a representative v ∈ W that can execute the same path. If this rule is not followed, there is one possible automaton with guards respecting the given LU-bounds for which this abstraction is not sound. Hence our question can be reworded as follows:

Given L and U bounds, what is the coarsest abstraction that is sound and complete for all LU-automata?

We answer this question in four steps:

Step 1. We define a generic simulation relation LU (Definition 7) which is a union over all time-abstract simulation relations on LU-automata.

Roughly the simulation relation says that v LU v if all paths, using LUguards, executed by v can be executed by v . We define an abstraction abs LU that is based on LU-simulation (Definition 8). The definition of LU-simulation is difficult to work with as it talks about infinite sequences of transitions.

Step 2. The next aim is to characterize this LU-simulation using a finite sequence of transitions (Definition 11). We want to come up with a sequence of LU-guards seq(v) executed by a valuation v for which we can say v LU v iff v executes this characteristic sequence seq(v). To achieve this, we go through an intermediate definition of what we call LU-regions (Definition 9). We define this sequence in Definition 11.

Step 3. Steps 1 and 2 have defined the necessary notions. We now observe that the following are equivalent (Proposition 12, Corollary 13):

• v LU v ,
• v can execute seq(v).

Step 4. The previous step gives a finite characterization of the generic LUsimulation LU . We use this to prove that every sound abstraction should be contained in abs LU , in other words abs LU is the coarsest abstraction sound and complete for all LU-automata (Theorem 14).

Section 3.1 handles Step 1; Section 3.2 defines the LU-regions as mentioned in Step 2; Sections 3.3 and 3.4 handle Steps 3 and 4 respectively.

LU-simulation

Using LU-bounds we define a simulation relation on valuations without referring to any particular automaton; or to put it differently, by considering all LU-automata at the same time.

Definition 7 (LU-simulation) Let L, U be two functions giving an integer bound for every clock. The LU-simulation relation between valuations is the biggest relation LU such that if v LU v then for every LU-guard g, and set of clocks R ⊆ X we have

• if v g,R -→ v 1 for some v 1 then v g,R -→ v 1 for v 1 such that v 1 LU v 1 . where v g,R -→ v 1 means that for some δ ∈ R ≥0 we have v + δ g and v 1 = [R](v + δ).
Note that in the above definition, the time elapse δ required for v to satisfy the guard g could be different from the time elapse δ required for v to satisfy the guard g. It is immediate that LU is the biggest relation that is a time-abstract simulation for all automata with given LU bounds. We define abstraction operator abs LU to be the abstraction based on this LU-simulation.

Definition 8 (Abstraction based on LU-simulation) For a zone Z we define:

abs LU (Z) = {v | ∃v ∈ Z. v LU v }.
The definition of LU-simulation is sometimes difficult to work with since it talks about infinite sequences of actions. We will present a useful characterization implying that actually we need to consider only very particular sequences of transitions that are of length bounded by the number of clocks (Corollary 13). Essentially, we are interested in the following question: given a valuation v, when does a valuation v LU -simulate it, that is, when is v LU v . We start with a preparatory definition of what we call LU -regions.

LU-regions

We introduce the notion of LU-regions. The classical notion of regions [START_REF] Alur | A theory of timed automata[END_REF] depends on the maximum bounds function M . Given only the maximum bounds M , we know that there could be guards x c and x c for c ∈ {0, . . . , M x } in the automaton. Let us call them the M-guards. However, with the LU-bounds, there is more information and consequently fewer guards: x c for c ∈ {0, . . . , U x }, and x c for c ∈ {0, . . . , L x }. Note that for each x, we have

M x = max(L x , U x ).
Let us denote the region of a valuation v by [v] M . A valuation v belongs to the region [v] M if two properties are satisfied:

Invariance by guards: v satisfies all M -guards that v satisfies, Invariance by time-elapse: for every time elapse

δ ∈ R ≥0 , there is a δ ∈ R ≥0 such that v + δ ∈ [v + δ] M .
We would like to define a notion of LU-regions in the same spirit, now with the additional information on the guards. For this discussion let us fix some L and U functions.

Definition 9 (LU-region) For a valuation v we define its LU-region, denoted v LU , to be the set of valuations v such that:

• v satisfies all LU -guards that v satisfies.

• For every pair of clocks x, y with v

(x) = v (x) , v(y) = v (y) , v(x) ≤ U x and v(y) ≤ L y we have: -if 0 < {v(x)} < {v(y)} then {v (x)} < {v (y)}. -if 0 < {v(x)} = {v(y)} then {v (x)} ≤ {v (y)}.
The first invariance with respect to guards has been directly incorporated in the first condition of the definition. The second condition in the definition of LU-regions has been added in order to obtain the invariance by time-elapse property mentioned. Note that it is possible to have v ∈ v LU but v / ∈ v LU . The following lemma will now show that with the two conditions specified in the definition, one can achieve the invariance with respect to time-elapse.

Lemma 10 Let v, v be valuations such that v ∈ v LU . For all δ ∈ R ≥0 , there exists a δ ∈ R ≥0 such that v + δ ∈ v + δ LU .

Proof

We are given valuations v and v such that v ∈ v LU . Therefore, v satisfies all the LU-guards that v satisfies, and the property given by second condition of Definition 9 is true for the ordering of fractional parts. Let us call it the order property. Additionally, we are given a time elapse δ ∈ R ≥0 from the valuation v. We need to construct a value δ ∈ R ≥0 such that v + δ ∈ v + δ LU . Assume δ < 1. Without loss of generality, we can assume that δ < 1. If δ ≥ 1, then we can put δ = δ and consider the valuations v + δ and v + δ . As we are not altering the fractional parts in these valuations, the order property is true for v + δ and v + δ . It is also easy to see that as v satisfies all LU-guards that v does, the valuation v + δ satisfies all LU-guards that v + δ does. This gives us v + δ ∈ v + δ LU and we need to consider the time elapse {δ} from v + δ . Therefore, in the rest of the proof, without loss of generality, we can assume that δ < 1.

Assume v(z) = v (z) for all clocks z. Suppose for a clock z, we have v(z) < v (z) . Then, as v satisfies all guards which v does, it should be the case that U z < v(z) . All guards having constants in between v(z) and v (z) would be lower bound guards. So, irrespective of what we choose for δ , the value v (z) + δ will satisfy all the LU-guards with respect to z that v(z) + δ satisfies. Also, z does not concern the order property at all. Similarly, if v (z) < v(z) , as v satisfies all LU-guards that v satisfies, it should be the case that L z < v (z) < v(z) . In both the cases, we can safely ignore the clock z.

Assume v(z) ≤ max(L z , U z ) for all clocks z. For a clock z such that v(z) is greater than both L z and U z , we know that v (z) should be greater than L z in order to satisfy the same LU-guards. Hence any amount of time elapse would maintain this property and additionally such clocks do not concern order property. Hence, we assume without loss of generality that all clocks are less than at least one of the bounds.

Constructing δ . We now have v and v such that for all clocks z, the integral parts match, that is

v(z) = v (z) and v(z) ≤ max(L z , U z ). Moreover, the time elapse δ < 1. Let 0 ≤ λ 1 < λ 2 < • • • < λ k < 1 be the fractional parts of clocks in v. Let us denote by X i the set of clocks z that have {v(z)} = λ i . Similarly, let 0 ≤ λ 1 < λ 2 < • • • < λ k < 1 denote
the fractional parts in v and we define the set X i to be the set of clocks z such that {v (z)} = λ i . This is pictorially illustrated below.

0 X1 X2 . . . X k 1 In v 0 X 1 X 2 . . . X k 1 In v
After a time elapse δ from v, some of the clocks cross the next integer, whereas some of them do not. Let us say that clocks in X j ∪ • • • ∪ X k have crossed the integer. Now the fractional parts of these clocks would be smaller than those of

X 1 ∪ • • • ∪ X j-1 as shown below: 0 Xj . . . X k X1 . . . Xj-1 1 In v + δ
We need to choose a value δ so that for all clocks y ∈ X j ∪ • • • ∪ X k such that (v + δ)(y) ≤ L y , the time elapse δ takes v to the next integer. Correspondingly for all the clocks x ∈ X 1 ∪ • • • ∪ X j-1 such that (v + δ)(x) ≤ U x , the time elapse δ still keeps v within the same integer. Clearly we need this property to be satisfied so that v + δ satisfies the same LU-guards as v + δ. To this regard, we define the following two values:

l = min{ {v (y)} | (v + δ)(y) ≤ L y and y ∈ X j ∪ • • • ∪ X k } u = max{ {v (x)} | (v + δ)(x) ≤ U x and x ∈ X 1 ∪ • • • ∪ X j-1 }
Firstly note that u < l. If not, there exist clocks y and x such that v(y) ≤ L y and v(x) ≤ U x , for which the order property is not true, thus giving a contradiction. Let δ be a value between u and l. Set δ = 1-δ. By construction, v + δ satisfies the same LU-guards as v + δ.

We will now see that this choice of δ also satisfies order property for v + δ and v + δ. Due to δ some clocks in v would have crossed the next integer. Let us say that clocks in X j ∪ • • • ∪ X k have crossed and the others stay within the same integer. We pictorially depict the scenario with the two valuations v + δ and v + δ below.

0 Xj . . . X k X1 . . . Xj-1 1 In v + δ 0 X j . . . X k X 1 . . . X j -1 1 In v + δ
Pick two clocks x, y such that:

(v + δ)(x) = (v + δ )(x) and (v + δ)(y) = (v + δ )(y) (3)
(v + δ)(x) ≤ U x and (v + δ)(y) ≤ L y {(v + δ)(x)} < {(v + δ)(y)}
Consider the case when both x, y ∈ X 1 ∪ • • • ∪ X j-1 . As they have not crossed integer in v, they should not have crossed integer in v too because of (3). Therefore both x, y ∈ X 1 ∪ • • • ∪ X j -1 . We know from order property that {v (x)} < {v (y)}. Clearly the time elapse of δ has not changed this ordering for these clocks and hence {(v +δ )(x)} < {(v +δ )(y)}. We can prove similarly when both x, y ∈

X j ∪ • • • ∪ X k .
Let us now consider the case when y ∈

X 1 ∪ • • • ∪ X j-1 and x ∈ X j ∪ • • • ∪ X k . As x has crossed integer in v, it should have crossed integer in v too by the hypothesis (3). Therefore x ∈ X j ∪ • • • ∪ X k . Again by hypothesis (3) the clock y should not have crossed integer and hence y ∈ X 1 ∪ • • • ∪ X j -1 . Hence we get that {(v + δ )(x)} < {(v + δ )(y)}.
This way we have proved the order property for v + δ and v + δ for the case of the strict inequality. The case of the equality can be handled in a similar way.

Finite paths characterizing LU-simulation

The previous section took a digression to define the notion of LU-regions. Now, we are in a position to answer the question: given two valuations v, v , when is v LU v . This section is devoted to show the link between this question and the definition of LU-regions. For valuations v, v , we will show that v LU v if and only if v can elapse some amount of time and fall into the LU-region of v (Proposition 12). Before that, we will define a sequence of guards that succinctly describes the LU-region v LU . Definition 11 (LU-sequence) For a valuation v, let g int be the conjunction of all LU guards that v satisfies. For every pair of clocks x, y such that v(x) ≤ U x , v(y) ≤ L y , consider guards:

• if 0 < {v(x)} < {v(y)} then we take a guard g xy ≡ (x < v(x) + 1) ∧ (y > v(y) + 1). • if 0 < {v(x)} = {v(y)} then we take a guard g xy ≡ (x ≤ v(x) + 1) ∧ (y ≥ v(y) + 1).
For every y with v(y) ≤ L y put g y = {g xy : v(x) ≤ U x }. Consider all the clocks y with v(y) ≤ L y and suppose that y 1 , . . . , y k is the ordering of these clocks with respect to the value of their fractional parts: 0 ≤ {v(y

1 )} ≤ • • • ≤ {v(y k )}. The LU-sequence seq(v) is defined to be the sequence of transitions gint -→ gy k -→ . . .
v LU v iff there is δ ∈ R ≥0 with v + δ ∈ v LU .
Proof First let us take v and consider its LU-sequence seq(v). The sequence seq(v) can be performed from v (the symbol τ denotes a time elapse):

v gint --→ v τ -→ v + δ k gy k --→ v + δ k τ -→ v + δ k-1 gy k-1 ----→ . . . . . . τ -→ v + δ 1 gy 1 --→ v + δ 1
when choosing δ i = (1 -{v(y i )}) or δ i = (1 -{v(y i )}) + ε for some sufficiently small ε > 0; depending on whether we test for non-strict or strict inequality in g yi . Delay δ i makes the value of y i integer or just above integer. If v LU v , then there exists a δ such that v + δ can do the sequence of transitions given by seq(v). The guard g int ensures that v + δ satisfies the same LU -guards as v. Note that in particular, this entails that for every pair of clocks x, y such that v(x) ≤ U x , v(y) ≤ L y and {v(x)} > 0, we have:

• (v + δ )(x) < v(x) + 1, and
• (v + δ )(y) ≥ v(y) .
Following transition g int , valuation v +δ can satisfy guards g y k to g y1 by letting some time elapse:

v + δ gint --→ v + δ τ -→ v + δ k gy k --→ v + δ k τ -→ v + δ k-1 gy k-1 ----→ . . . . . . τ -→ v + δ 1 gy 1 --→ v + δ 1
Consider the clock y i . If the integral part (v + δ )(y i ) is strictly greater than v(y i ) , time elapse is not necessary to cross the guard g yi . On the other hand, if (v + δ )(y i ) = v(y i ) , then for the guard g yi to be crossed, δ i should be sufficiently large to make the value of (v + δ i )(y i ) integer or just above integer. But at the same time, the guard g xyi is satisfied, which entails that for all x such that v(x) ≤ U x , v(x) = (v + δ )(x) , we get:

• if 0 < {v(x)} < {v(y i )}, then {(v + δ )(x)} < {(v + δ )(y i )} and • if 0 < {v(x)} = {v(y i )}, then {(v + δ )(x)} ≤ {(v + δ )(y i )}
Therefore, from the definition of LU -regions, we get that v + δ ∈ v LU . This shows left to right implication.

For the right to left implication we show that the relation S = {(v, v ) : v ∈ v LU } is an LU-simulation relation. For this we take any (v, v ) ∈ S, any LU guard g, and any reset R such that v

g,R -→ v 1 . We show that v g,R -→ v 1 for some v 1 with (v 1 , v 1 ) ∈ S.
The only non-trivial part in this is to show that if v + δ g for some δ, then there exists a δ such that (v + δ, v + δ ) ∈ S and v + δ g. But this is exactly given by Lemma 10.

In particular the proof shows the following.

Corollary 13 For two valuations v, v : v LU v iff v can execute the sequence seq(v).

Proof of optimality

We are now ready to show that abs LU (Z) (Definition 8), the abstraction based on LU simulation, is the coarsest sound and complete abstraction that uses solely the LU information.

Theorem 14

The abs LU abstraction is the coarsest abstraction that is sound and complete for all LU-automata. It is also finite.

Proof

Suppose that we have some other abstraction a that is not included in abs LU on at least one LU -automaton. This means that there is some LU automaton A 1 and its reachable configuration (q 1 , Z) such that a (Z) \ abs LU (Z) is not empty. We suppose that a is complete and show that it is not sound.

Take v ∈ a (Z) \ abs LU (Z). Consider the test sequence seq(v) as in Corollary 13. From this corollary we know that it is possible to execute this sequence from v but it is not possible to do it from any valuation in Z since otherwise we would get v ∈ abs LU (Z).

As illustrated in Fig 2 we add to A 1 a new sequence of transitions constructed from the sequence seq(v). We start this sequence from q 1 , and let q f be the final state of this new sequence. The modified automaton A 1 started in the initial configuration arrives with (q 1 , Z) in q 1 and then it can try to execute the q 0 . . . sequence we have added. From what we have observed above, it will not manage to reach q f . On the other hand from (q 1 , v) it will manage to complete the sequence. But then by completeness of the abstraction (q 1 , a (Z))

• . . . • . . . • q 1 . . . Automaton A 1 • • • q f g int g y k g y1 seq(v)
seq(v)
-→ (q f , W ) for a nonempty W . So a is not a sound abstraction.

That abs LU is finite is easy to see. The set abs LU (Z) is a union of classical regions. Recall that we denote by M the bound function that assigns to each clock x, the maximum of L x and U x . Let v be a valuation in Z.

If v ∈ [v] M
then it is easy to see that v ∈ v LU and by definition v ∈ abs LU (Z).

The a LU abstraction

Since abs LU is the coarsest abstraction, we would like to use it in a reachability algorithm. The definition of abs LU , or even the characterization referring to LU-regions, are still too complicated to work with. It turns out though that there is a close link to an existing abstraction.

The a LU abstraction proposed by Behrmann et al. in [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] has a much simpler definition. Quite surprisingly, in the context of reachability analysis the two abstractions coincide (Theorem 19). The a LU abstraction is based on a simulation relation LU .

Definition 15 (LU-preorder [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]) Let L, U : X → N ∪ {-∞} be two bound functions. For a pair of valuations we set v LU v if for every clock x:

• if v (x) < v(x) then v (x) > L x , and • if v (x) > v(x) then v(x) > U x .
It has been shown in [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] that LU is a simulation relation. The a LU abstraction is based on this relation.

Definition 16 (a LU -abstraction [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]) Given L and U bound functions, for a set of valuations W we define: Our goal is to show that when we consider zones closed under time-successors, a LU and abs LU coincide. To prove this, we would first show that there is a very close connection between valuations in v LU and valuations that simulate v with respect to LU . The following lemma says that if v ∈ v LU then by slightly adjusting the fractional parts of v we can get a valuation v 1 such that v LU v 1 . We start with a preliminary definition.

a LU (W ) = {v | ∃v ∈ W. v LU v }.
Definition 17 A valuation v 1 is said to be in the neighborhood of v, written v 1 ∈ nbd(v) if for all clocks x, y:

• v(x) = v 1 (x) ,
• {v(x)} = 0 iff {v 1 (x)} = 0,

• {v(x)} {v(y)} implies {v 1 (x)} {v 1 (y)} where is either < or =.

Notice that the neighborhood of v is the same as the region of v with respect to the classical region definition with maximal bound being ∞.

We give a brief intuition before proving the following lemma which gives the relation between LU-regions and LU simulation. Consider a valuation v shown in Figure 4. Its LU-region v LU is given by the shaded portion. Pick a valuation v that belongs to v LU and let us see if it satisfies v LU v .

As we can see in Figure 4, the value of v (x) > v(x) and additionally v (x) ≤ U x . This shows that v LU v due to its x-coordinate. However, by slightly adjusting the fractional parts: that is, reducing {v (y)} to move it down a bit and then reducing {v (x)} to make v (x) equal to v(x) leads us to a valuation v 1 which is in the neighborhood of v but now v LU v 1 . The adjustment is depicted in Figure 4. Essentially, the following lemma claims that the LU-region v LU can be obtained as the downward closure of LU over the set nbd(v), in other words, a LU (nbd(v)). Lemma 18 (Adjustment) Let v be a valuation and let v ∈ v LU . Then, there exists a

v 1 ∈ nbd(v ) such that v LU v 1 . Proof Let v ∈ v LU . The goal is to construct a valuation v 1 ∈ nbd(v ) that satisfies v LU v 1 .
To be in the neighborhood, the valuation v 1 should have the same integral parts as that of v and should agree on the ordering of fractional parts. So for all x, we put v 1 (x) = v (x) . It remains to choose the fractional parts for v 1 . But before, we will first see that there are clocks for which irrespective of what the fractional part is, the two conditions in Definition 15 would be true. Consider a clock x that has v (x) < v(x) . Since v satisfies all LU-guards as v, we should have v (x) > L x . The first condition of LU for x becomes true and the second condition is vacuously true. Similarly, when v (x) > v(x) , we should have v(x) > U x and the second condition of LU becomes true and the first condition is vacuously true. Therefore, clocks x that do not have the same integral part in v and v satisfy the LU condition directly thanks to the different integral parts. Whatever the fractional parts of v 1 are, the LU condition for these clocks would still be true.

Let us therefore now consider only the clocks that have the same integral parts: v (x) = v(x) . If this integer is strictly greater than both L x and U x , the two conditions of LU would clearly be satisfied, again irrespective of the fractional parts. So we consider only the clocks x that have the same integral part in both v and v and additionally either v(x) ≤ U x or v(x) ≤ L x .

We prune further from among these clocks. Suppose there is such a clock that has {v (x)} = 0. To be in the neighborhood, we need to set {v 1 (x)} = 0. If {v(x)} is 0 too, we are done as the LU condition becomes vacuously true.

Otherwise, we would have v (x) = v 1 (x) < v(x). But recall that v ∈ v LU and so it satisfies the same LU-guards as v does. This entails that v 1 (x) > L x and we get the first condition of LU to be true. Once again, the other condition is trivial. So we eliminate clocks that have zero fractional parts in v . A similar argument can be used to eliminate clocks that have zero fractional parts in v.

So finally, we end up with the set of clocks x that have:

• v (x) = v(x) ,
• {v (x)} > 0 and {v(x)} > 0,

• v(x) < max(U x , L x ).
Call this set X f . The task is to select non-zero fractional values {v 1 (x)} for all clocks x in X f so that they match with the order in v . This is the main challenge and this is where we would be using the second property in the definition of v ∈ v LU , which we restate here:

∀x, y ∈ X f such that v(x) ≤ U x and v(y) ≤ L y (4) 0 < {v(x)} < {v(y)} ⇒ {v (x)} < {v (y)} 0 < {v(x)} = {v(y)} ⇒ {v (x)} ≤ {v (y)} Let 0 < λ 1 < λ 2 < • • • < λ n < 1 be
the fractional values taken by clocks of X f in v , that is, for every clock x ∈ X f , the fractional value {v (x)} = λ i for some i ∈ {1, . . . , n}. Let X i be the set of clocks x ∈ X f that have the fractional value as λ i :

X i = {x ∈ X f | {v (x)} = λ i } for i ∈ {1, . . . , n}.
In order to match with the ordering of v , one can see that for all clocks x i in some X i , the value of {v 1 (x i )} should be the same, and if x j ∈ X j with i = j, then we need to choose {v 1 (x i )} and {v 1 (x j )} depending on the order between λ i and λ j .

Therefore, we need to pick n values 0 < σ 1 < σ 2 < • • • < σ n < 1 and assign for all x i ∈ X i , the fractional part {v 1 (x i )} = σ i . We show that it can be done by an induction involving n steps.

After the k th step of the induction we assume the following hypothesis:

• we have picked values 0 < σ n-k+1 < σ n-k+2 < • • • < σ n < 1, • for all clocks x ∈ X n-k+1 ∪X n-k+2 • • •∪X n , the LU condition is satisfied, • for all clocks y ∈ X 1 ∪ X 2 • • • ∪ X n-k , we have v(y) ≤ L y ⇒ {v(y)} < σ n-k+1 (5)
Let us now perform the k + 1 th step and show that the induction hypothesis is true for k + 1. The task is to pick σ n-k . We first define two values 0 < l < 1 and 0 < u < 1 as follows:

l = max {v(z)} | z ∈ X n-k and v(z) ≤ L z u = min { {v(z)} | z ∈ X n-k and v(z) ≤ U z } ∪ σ n-k+1
We claim that l ≤ u. Firstly, l < σ n-k+1 from the third part of the induction hypothesis. So if u is σ n-k+1 we are done. If not, suppose l > u, this means that there are clocks x, y ∈ X n-k with v(x) ≤ U x and v(y) ≤ L y such that {v(x)} < {v(y)}. From Equation 4, this would imply that {v (x)} < {v (y)}. But this leads to a contradiction since we know they both equal λ n-k in v .

This leaves us with two cases, either l = u or l < u. When l = u, we pick σ n-k = l = u. Firstly, from the third part of the hypothesis, we should have l < σ n-k+1 and so σ n-k < σ n-k+1 . Secondly for all z ∈ X n-k , if v 1 (z) < v(z), then z should not contribute to l and so v(z) > L z , which is equivalent to saying, v 1 (z) > L z . Similarly, if v 1 (z) > v(z), then z should not contribute to u and so v(z) > U z , thus satisfying the LU condition for z. Finally, we should show the third hypothesis. Consider a clock y ∈

X 1 ∪ • • • ∪ X n-k-1 with v(y) < L y . If {v(y)} ≥ σ n-k , it
would mean that {v(y)} ≥ u and from Equation 4gives a contradiction. So the three requirements of the induction assumption are satisfied after this step in this case. 4, we should have {v(y)} < u. Take the maximum of {v(y)} over all such clocks:

Now suppose l < u. Consider a clock y ∈ X 1 ∪ • • • ∪ X n-k-1 such that v(y) < L y . From Equation
λ = max{{v(y)} | y ∈ X 1 ∪ • • • ∪ X n-k-1 and v(y) < L y }
Choose σ n-k in the interval (λ, u). We can see that all the three assumptions of the induction hold after this step.

We can now prove the main result of this section. Recall Definition 3 of time-elapsed zones.

Theorem 19 If Z is time-elapsed then abs LU (Z) = a LU (Z) Proof Suppose v ∈ a LU (Z).
There exists a v ∈ Z such that v LU v . It can be easily verified that LU is a LU -simulation relation. Since LU is the biggest LU-simulation, we get that v LU v . Hence v ∈ abs LU (Z).

Suppose v ∈ abs LU (Z). There exists v ∈ Z such that v LU v . From Proposition 12, this implies that there exists a δ such that v + δ ∈ v LU . As Z is time-elapsed, we get v + δ ∈ Z. Moreover, from Lemma 18, we know that there is a valuation v 1 ∈ nbd(v + δ ) such that v LU v 1 . Every valuation in the neighborhood of v + δ satisfies the same constraints of the form y -x c with respect to all clocks x, y and hence v 1 belongs to Z too. Therefore, we have a valuation v 1 ∈ Z such that v LU v 1 and hence v ∈ a LU (Z).

Using a LU to solve the reachability problem

A forward exploration algorithm for solving the reachability problem constructs the reachability tree starting from the initial node (q 0 , Z 0 ) (cf. Figure 5), with

Z 0 = {0 + δ | δ ∈ R ≥0 }.
The successor with respect to ⇒ can be computed in time O(|X| 2 ) where X is the number of clocks [START_REF] Zhao | A quadratic-time dbmbased successor algorithm for checking timed automata[END_REF]. By definition ⇒ computes a time-elapsed zone. Therefore, all nodes that are explored by the algorithm have time-elapsed zones.

Before continuing exploration from a node (q, Z), the algorithm first checks if q is accepting. If not, the algorithm checks if for some visited node (q, Z ), we have Z ⊆ a LU (Z ). If this is the case, (q, Z) need not be explored. Otherwise, the successors of (q, Z) are computed as stated above. This way we ensure termination of the algorithm since a LU is a finite abstraction [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF].

Since the reachability algorithm refers to only time-elapsed zones, Theorems 14 and 19 show that a LU is the coarsest sound and complete abstraction provided the only thing we know about the structure of the automaton are its L and U bounds. Recall that coarser abstractions make abstract graph smaller, so the exploration algorithm can finish faster.

In Definition 6, we introduced LU -bounds that associate an L bound and a U bound to every clock in an automaton A. Those bounds are the same in every state of the automaton. Instead, state-of-the-art algorithms calculate LU -bounds for each state of the automaton separately [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF], or even on-the-fly during exploration [START_REF] Herbreteau | Using non-convex approximations for efficient analysis of timed automata[END_REF][START_REF] Frédéric Herbreteau | Lazy abstractions for timed automata[END_REF]. The maximality argument in favor of a LU is of course true also in this case.

The last missing piece is an efficient inclusion test Z ⊆ a LU (Z ). This is the main technical contribution of this paper.

An O(|X|

2 ) algorithm for Z ⊆ a LU (Z )
In this section, we present an efficient algorithm for the inclusion test Z ⊆ a LU (Z ) (Theorem 32). In the algorithm for the reachability problem as ex-plained in Section 4.2, each time a new node (q, Z) is seen, it is checked if there exists an already visited node (q, Z ) such that Z ⊆ a LU (Z ). This means that a lot of such inclusion tests need to be performed during the course of the algorithm. Hence it is essential to have a low complexity for this inclusion procedure. We are aiming at quadratic complexity as this is the complexity incurred in the existing algorithms for inclusions of the form Z ⊆ Z used in the standard reachability algorithm. It is well known that all the other operations needed for forward exploration, can be done in at most quadratic time [START_REF] Zhao | A quadratic-time dbmbased successor algorithm for checking timed automata[END_REF].

We will now characterize when Z ⊆ a LU (Z ) holds. The main steps are outlined below.

Step 1. As a first step, we reduce the inclusion problem to a problem of intersection in Section 5.1. The question Z ⊆ a LU (Z ) boils down to asking if there exists a valuation v ∈ Z such that its LU-region v LU does not intersect Z (Proposition 21).

Step 2. As a next step, we consider the intersection v LU ∩ Z . We aim to show that this intersection can be decided by looking at projections on every pair of clocks (Proposition 28). This is the most difficult step in the way to the inclusion test and spans three sections. We first describe a convenient graph representation of zones in Section 5.2. We call this the distance graph and will use it to represent Z . Subsequently, in Section 5.3, we see how we can represent LU-regions as distance graphs. This gives a distance graph representation for v LU . Finally, in Section 5.4, we analyze the graph representations of v LU and Z to see when the intersection v LU ∩ Z is empty. We show that for this it is enough to look at two clocks at a time.

Step 3. The previous step gives the condition for v LU ∩ Z to be empty. We now look at the zone Z to find out quickly the valuation v ∈ Z that can potentially satisfy this condition (Proposition 31).

Step 4. We substitute the valuation obtained from Step 3 to the condition of Step 2 to give the efficient test for inclusion (Theorem 32). Both steps 3 and 4 appear in Section 5.5.

Notation. For notational convenience, we denote v(x) by v x for a valuation v and clock x.

Reducing inclusion to intersection

The aim of this chapter is to reduce the question of inclusion to a question of intersection. The adjustment lemma (Lemma 18) shows a close connection between LU -regions and LU -simulation in one direction: that is, if v ∈ v LU then we can find a valuation v 1 in the neighborhood of v such that v LU v 1 . We show below a connection in the other direction too.

Lemma 20 Let v, v be valuations. If v LU v , then v ∈ v LU .
Proof It is not difficult to see from the definition of LU (Definition 15) that both v and v satisfy the same LU-guards. It remains to show the second property for v to be in v LU .

Let x, y be clocks such that v x = v x , v y = v y , and v x ≤ U x , v y ≤ L y . Suppose {v x } {v y }, for being either < or =. As v LU v , if v x > v x , we need v x > U x which is not true. Hence we can conclude that v x ≤ v x . Similarly, for y, one can conclude that v y ≥ v y . As the integer parts are the same in v and v , we get {v x } < {v y } or {v x } ≤ {v y } depending on whether is < or =.

The above along with the adjustment lemma help us to reduce the question of inclusion as a question of intersection.

Proposition 21 Let Z, Z be zones. Then, Z ⊆ a LU (Z ) iff there exists a valuation v ∈ Z such that v LU ∩ Z is empty.

Proof

Consider the left-to-right direction. Suppose Z ⊆ a LU (Z ). Then there exists a valuation v ∈ Z such that for every valuation v ∈ Z we have v LU v . Pick an arbitrary v ∈ Z . In particular, every valuation

v 1 ∈ nbd(v ) satisfies v LU v 1 .
From the Adjustment lemma 18, we get that v ∈ v LU . Since v is arbitrary, we get that v LU ∩ Z is empty. Now for the right-to-left direction. Suppose v LU ∩ Z is empty. Then by Lemma 20, we get that v LU v for every valuation v ∈ Z . This shows that Z ⊆ a LU (Z ).

Distance graphs

Thanks to Proposition 21, we know that to solve Z ⊆ a LU (Z ), we need to check if there exists a valuation v ∈ Z such that its LU-region v LU does not intersect with the zone Z . The focus now is to study this intersection.

We will begin with a convenient representation of zones that we use to solve this intersection question. The standard way to represent a zone is using a DBM. An equivalent representation is in terms of graphs [START_REF] Shostak | Deciding linear inequalities by computing loop residues[END_REF] which we call here distance graphs.

Definition 22 (Distance graph)

A distance graph G has clocks as vertices, with an additional special vertex x 0 representing constant 0. Between every two vertices there is an edge with a weight of the form ( , c) where c ∈ Z and ∈ {≤, <} or ( , c) = (<, ∞). An edge x c -→ y represents a constraint y -x c: or in words, the distance from x to y is bounded by c. We let [[G]] be the set of valuations of clock variables satisfying all the constraints given by the edges of G with the restriction that the value of x 0 is 0. We also say that the y -

x-constraint of [[G]] is c if the weight of the x - → y edge in G is c.
For readability, we will often write 0 instead of x 0 . Figure 6 illustrates a zone with its constraints and the corresponding distance graph.

An arithmetic over the weights ( , c) can be defined as follows [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF]. Equality

( 1 , c 1 ) = ( 2 , c 2 ) if c 1 = c 2 and 1 = 2 . Addition ( 1 , c 1 ) + ( 2 , c 2 ) = ( , c 1 + c 2 ) where =< iff either 1 or 2 is <. Minus -( , c) = ( , -c).
Order ( 1 , c 1 ) < ( 2 , c 2 ) if either c 1 < c 2 or (c 1 = c 2 and 1 =< and 2 =≤).

This arithmetic lets us talk about the weight of a path as a weight of the sum of its edges.

A cycle in a distance graph G is said to be negative if the sum of the weights of its edges is at most (<, 0); otherwise the cycle is positive. The following proposition is folklore.

Proposition 23 A distance graph G has only positive cycles iff [[G]] = ∅.

A distance graph is in canonical form if the weight of the edge from x to y is the lower bound of the weights of paths from x to y. Given a distance graph, its canonical form can be computed by using an all-pairs shortest paths algorithm like Floyd-Warshall's [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF] in time O(|X| 3 ) where |X| is the number of clocks. Note that the number of vertices in the distance graph is |X| + 1. For computing the successors of a node in the zone graph, the most complex operation is the computation of Z ∧ g which involves a canonicalization operation. However, since g has diagonal free constraints, the canonicalization procedure involved to compute Z ∧ g is easier and costs only O(|X| 2 ) [START_REF] Zhao | A quadratic-time dbmbased successor algorithm for checking timed automata[END_REF].

Recall that we have reduced the problem Z ⊆ a LU (Z ) to checking if there exists v such that v LU ∩ Z is empty. For this, we need to know when the intersection of an LU-region and a zone is empty. In the next section we will see that an LU-region is a zone and can be represented using a distance graph. Therefore, it boils down to asking given two distance graphs G 1 and

G 2 when is [[G 1 ]] ∩ [[G 2 ]] empty.
For two distance graphs G 1 , G 2 which are not necessarily in canonical form, we denote by min(G 1 , G 2 ) the distance graph where each edge has the weight equal to the minimum of the corresponding weights in G 1 and G 2 . Even though this graph may be not in canonical form, it should be clear that it represents intersection of the two arguments, that is,

[[min(G 1 , G 2 )]] = [[G 1 ]] ∩ [[G 2 ]
]; in other words, the valuations satisfying the constraints given by min(G 1 , G 2 ) are exactly those satisfying all the constraints from G 1 as well as from G 2 .

Proposition 23 tells us that the intersection

[[G 1 ]] ∩ [[G 2 ]
] is empty iff the distance graph min(G 1 , G 2 ) has a negative cycle.

LU-regions as distance graphs

Our aim is to check when the intersection of v LU and Z is empty. We saw in the previous subsection that zones can be conveniently and canonically represented by distance graphs. Here, we will see how we can canonically represent an LU -region of a valuation as a distance graph.

We will first recall a constructive definition of Alur-Dill regions.

Definition 24 (Regions: constructive definition) A region with respect to bound function M is the set of valuations specified as follows:

1. for each clock x ∈ X, one constraint from the set:

{x = c | c = 0, . . . , M x } ∪ {c -1 < x < c | c = 1, . . . , M x } ∪ {x > M x } 2.
for each pair of clocks x, y having interval constraints: c -1 < x < c and d -1 < y < d, it is specified if {x} is less than, equal to or greater than {y}.

The distance graph representing a region can be constructed using the above constructive definition of a region. For a valuation v, let G M v denote the canonical distance graph representing the region [v] M . We are now interested in getting the LU-region of v, that is, v LU as a distance graph. For convenience, we will recall below the definition of LU-regions.

Definition 9. (LU-region)

For a valuation v we define its LU-region, denoted v LU , to be the set of valuations v such that:

• v satisfies the same LU -guards as v.

• For every pair of clocks x, y with v(x) = v (x) , v(y) = v (y) , v(x) ≤ U x and v(y) ≤ L y we have: For a valuation v, we need to collect all valuations v satisfying the above two conditions to get v LU . We begin with a motivating example in Figure 7. In the (a) part of the figure, we consider a valuation v such that v x > U x . The shaded portion in Figure 7 (a) shows the region [v] M and the finite valued x -y and x -0 constraints bounding this region (c.f. Definition 22 for definition of x -y-constraints and Figure 6 for an illustration). The LU-region v LU is shown in Figure 7 (b). Observe that it matches with the definition given above. But more importantly, note that it can be seen as a transformation of [v] M by moving its x -y and x -0 constraints to infinity and keeping the rest same.

-if 0 < {v(x)} < {v(y)} then {v (x)} < {v (y)}. -if 0 < {v(x)} = {v(y)} then {v (x)} ≤ {v (y)}. Ux x y 0 v [v] M (a) Ux x y 0 v v LU (b) Ly x y 0 v [v] M (c) Ly x y 0 v v LU (d)
We now consider a valuation v with v y > L y in Figure 7 (c). Once again, the shaded portion shows the region [v] M and the relevant boundary constraints. We depict the LU-region v LU in Figure 7 (d) matching the definition given above. Note that it can be seen as a transformation of [v] M by moving the x -y constraint to infinity and the 0-y constraint up to L y . However, when we move x -y to infinity, the graph that we get would no longer be canonical. We could then consider the canonicalization of the transformed graph.

( yx , c yx ) =          (<, ∞) if v x > U x (<, ∞) if v y > L y and x = 0 (<, -L y )
if v y > L y and x = 0 ( yx , c yx ) otherwise Then, the distance graph G LU v is defined to be the canonical form of G .

The following lemma confirms that the distance graph defined above indeed represents v LU .

Lemma 26 Let v be a valuation. Let G LU v be the graph obtained by Definition 25. Then the sets v LU and [[G LU v ]] are equal.

Proof Let v ∈ v LU . We will now show that v ∈ [[G LU v ]]. First observe that [[G LU v ]] = [[G ]]
where G is the graph as in Definition 25. Therefore it is sufficient to show that v satisfies the constraints given by G . From the definition, it is clear that an edge y -→ x is finite valued in G only if v x ≤ U x . Additionally when v y ≤ L y , the value of the edge y -→ x is the same as that in G M v . Otherwise if v y > L y , the only finite value is (<, -L y ) for the edge y -→ x 0 . Since v ∈ v LU , it satisfies all the LU -guards that v satisfies. If y is a clock such that v y > L y then v y > L y too. So v satisfies constraints of the form y <-Ly ----→ x 0 . It now remains to look at edges y d --→ x with v y ≤ L y , v x ≤ U x and the weight ( , d) coming from G M v . Let v x and v y be denoted as c x and c y respectively. As v satisfies the same LU -guards as v, we have:

v x < c x + 1 v y ≥ c y (6)
Therefore v x -v y < c x + 1 -c y . Since G M v represents the region containing v, by definition of regions, the constant in the weight ( , d) is either c x -c y + 1 or c x -c y . If it is the former, then clearly, v also satisfies x -y d. We need to consider the latter case, that is, d is c x -c y . Thanks to (6) above, if either v x < c x or v y ≥ c y + 1, we are done. We are left with considering the case when v x = c x and v y = c y . We have:

v x -v y c x -c y ⇒ {v x } -{v y } 0 ⇒ {v x } -{v y } 0 (as v ∈ v LU ) ⇒ v x + {v x } -( v y + {v y }) c x -c y ⇒ v x -v y d This proves that if v ∈ v LU ,
G M v . Since v ∈ [[G ]]
, it is clear that v satisfies the same LU -guards as v. We now consider the order property for LU -regions. From Definition 9, the order property only need to be considered when v x = v x and v y = v y . Let us denote c x = v x = v x and c y = v y = v y By definition of G , the edge y -→ x in G has the same weight as that in G M v . Let the edge weight y -→ x be ( , d). We have:

v x -v y d ⇒ {v x } -{v y } d -(c x -c y )
If {v x } < {v y } then either d -(c x -c y ) < 0 or if it is 0 then is the strict inequality. As this edge remains in G , the valuation v satisfies v x -v y d. Moreover, since the integral parts of v match, we get {v x } -{v y } d -(c x -c y ). By the aforementioned property, we get {v x } < {v y }. A similar argument follows for the case when {v x } = {v y }.

Before we use the distance graph G LU v for further analysis, recall that we first defined a graph G in Definition 25 and then obtained G LU v by canonicalizing it. We will now observe some properties of G LU v that are either retained from G or obtained thanks to canonicalization. These observations would be important in the next section when we do the analysis on the distance graph representing LU-region v LU and zone Z .

Lemma 27 Let v be a valuation. Let G M v , G LU v
be the canonical distance graphs of [v] M and v LU respectively. For variables x, y, if the edge y -→ x has a finite value in G LU v , then:

1. v x ≤ U x , 2. if v y ≤ L y , the value of y - → x in G LU v and G M v are equal, 3. if v y > L y , the value of y - → x in G LU v equals the value of the path y - → x 0 - → x in G LU v .

Proof

The graph G LU v is the canonical form of the graph G defined in Definition 25.

By definition, if v x > U x , all incoming edges to x in G have weight (<, ∞). So, the shortest path in this graph G from a variable y to a variable x such that v x > U x is (<, ∞). Therefore, if in the canonical form G LU v , the edge y -→ x is finite valued, we should have v x ≤ U x . This gives the first part of the lemma.

Consider the second part of the lemma. We know that v y ≤ L y and from the first part of the lemma, we know that v x ≤ U x . The weight of y -→ x in G is the same as that of G M v according to Definition 25. Note that the finite values in the graph G are either the same as that of G M v or of the form (<, -L z ) for some edges z -→ 0. In the latter case, we also know by definition that v z > L z . Therefore the value (<, -L z ) is greater than the corresponding value in G M v . As G M v is canonical, the shortest path from y to x in G cannot reduce from its value in G M v and hence equals just the edge value y -→ x. This gives the second part of the lemma.

Finally consider the third part. Assume v y > L y . From Part 1, we know that v x ≤ U x . By Definition 25, the weight of y -→ x equals (<, ∞) if x is not x 0 . The only finite valued outgoing edge from y is y -→ x 0 . Therefore, we can infer two things: the shortest path from y to x 0 is given by the edge y -→ x 0 ; and the shortest path from y to x should contain this edge y -→ x 0 . Secondly, note that variable x 0 has v x0 ≤ L x0 (v x0 = 0 = L x0 ). By definition, the value of x 0 -→ x in G is given by the corresponding value in G M v and by Part 2, we know that this value stays in G LU v , that is, the shortest path from x 0 to x in G is given by the direct edge. Summing up, the shortest path from y to x in G is given by y -→ x 0 -→ x, where both y -→ x 0 and x 0 -→ x are values coming from G LU v .

5.4.

When does an LU -region intersect a zone.

We are now in a position to characterize the intersection v LU ∩ Z . Let G LU v as defined in the previous section be the canonical distance graph of v LU and let G Z be the canonical distance graph of Z . By Proposition 23, the intersection v LU ∩ Z is empty iff min(G LU v , G Z ) has a negative cycle. We will now state a necessary and sufficient condition for the distance graph min(G LU v , G Z ) to have a negative cycle. We denote by Z xy the weight of the edge x -→ y in G Z . Similarly we denote v LU xy for the weight of x -→ y in G LU v . When a variable x represents the special clock x 0 , we define v LU 0x and v LU x0 to be (≤, 0). Since by convention x 0 is always 0, this is consistent. We also denote

[v] M
xy for the weight of x -→ y in G M v with the same convention when x = x 0 . The next proposition is the most important observation used in getting the final inclusion test.

Proposition 28 Let v be a valuation and Z a zone. The intersection v LU ∩Z is empty iff there exist two variables x, y such that v x ≤ U x and Z xy + v LU yx < (≤, 0). To prove the above proposition, we need a small but a crucial observation that exploits the special structure of regions. A variable x is said to be bounded 2. Suppose v y1 > L y1 . Consider again the two edges y 1 -→ x 1 and y 2 -→ x 2 of (8) and now suppose that v y1 > L y1 . By Part 3 of Lemma 27, the edge y 1 -→ x 1 can be replaced by:

y 1 - → x 0 - → x 1 of G LU v
If there is another variable in N that is greater than its L bound, then the vertex x 0 would occur twice in the negative cycle. From this negative cycle, we can obtain a smaller negative cycle containing only one occurrence of x 0 . Hence, without loss of generality, we can assume that x 0 occurs only once in N . In particular, this gives us that:

v y2 ≤ L y2
Note that the special variable x 0 has v x0 ≤ L x0 as its value is always supposed to be 0 and L x0 is defined to be 0. Now consider the two edges:

x 0 - → x 1 and y 2 - → x 2
This corresponds to Case 1 as v x0 ≤ L x0 and v y2 ≤ L y2 . As we have seen, these two edges can be eliminated to give a smaller negative cycle containing either x 0 -→ x 2 or y 2 -→ x 1 , with the respective value coming from G LU v . If it is the latter edge y 2 -→ x 1 , the smaller negative cycle does not contain y 1 and hence all variables are bounded by L. By Case 1, it can be reduced to a cycle as required by the proposition.

Let us now consider the former edge x 0 -→ x 2 . We have the cycle:

y 1 - → x 0 - → x 2 - → . . . - → y 1
All the variables other than y 1 in the path x 0 -→ . . . -→ y 1 are bounded by their L bound. We can therefore assume that all edges in x 2 -→ . . . -→ y 1 come from G Z , because if not, we can apply the argument of Case 1 to further reduce the cycle. As G Z and G LU v are canonical, this cycle reduces to y 1 -→ x 2 -→ y 1 with y 1 -→ x 2 coming from G LU v and x 2 -→ y 1 coming from Z . This again conforms to the form of the cycle required by [START_REF] Berthomieu | An enumerative approach for analyzing time petri nets[END_REF].

Final steps

Proposition 28 gives a useful characterization of when v LU ∩ Z is empty. To lift this characterization to Z ⊆ a LU (Z ) and Proposition 21, we need to find the least value of v LU yx from among the valuations v ∈ Z and see if this satisfies the condition given in Proposition 28.

For the moment, assume that L = U so that the LU-regions coincide with the classic regions. Consider a zone Z lying within the M bounds, as shown in Figure 9. The values of [v] M yx for different valuations in the zone are shown. The value decreases as we move towards the "left boundary". In the figure, since the y -x constraint of Z is given by y -x ≤ -1, there exists a valuation v 4 on the "boundary" and hence the least value of [v] M yx among all v ∈ Z would

[ v 1 ] M y x = 4 [ v 2 ] M y x = 3 [ v 3 ] M y x = 2 [ v 4 ] M y x = 1 y - x ≤ - 1 Figure 9: Value of [v] M
yx decreases as we move left be given by [v 4 ] M yx which is (≤, 1). If the y -x constraint of Z was y -x < -1 with a strict inequality, then the least value of [v] M yx from v ∈ Z is no longer (≤, 1) as there is no valuation attaining this value. In this case, the least value of [v] M yx would be (<, 2), given by the open region containing v 5 with constraints y -x < -1 and x -y < 2.

Due to this asymmetry, we need to define the following notion to handle weights in a convenient way. For a weight ( , c) we define -( , c) as ( , -c) and a ceiling function • as follows.

Definition 30 For a real c, let c denote the smallest integer that is greater than or equal to c. We define the ceiling function ( , c) for a weight ( , c) depending on whether equals ≤ or <, as follows:

(≤, c) = (≤, c) if c is an integer (<, c ) otherwise (<, c) = (<, c + 1) if c is an integer (<, c ) otherwise
The following proposition is one of the two cores for the proof of the main theorem. It gives the least value of v LU yx from among the valuations v present in a zone Z.

Proposition 31 Let Z be a non-empty zone, and let x, y be two clocks. The least value of v LU yx among the valuations v ∈ Z such that v x ≤ U x is given by:

(<, ∞) if Z x0 < (≤, -U x ) max{ -Z xy , -Z x0 -(<, L y )} otherwise

Proof

Let G be the canonical distance graph representing the zone Z. We denote the weight of an edge i -

→ j in G by ( ij , c ij ). Recall that this means Z ij = ( ij , c ij ).
We are interested in computing the smallest value of the x -y constraint defining an LU -region intersecting Z. Additionally we want to restrict to LUregions in which all its valuations satisfy x ≤ U x , that is, we need to find:

β := min{ v LU yx | v ∈ Z and v x ≤ U x } Clearly, if v x > U x for all valuations v ∈ Z, then β is (<, ∞). When Z x0 < (≤, -U x ), it means that all valuations v ∈ Z satisfy 0 -v x x0 c x0 and c x0 ≤ -U x . Moreover x0 is the strict inequality if c x0 = -U x . In consequence, all valuations v ∈ Z satisfy v x > U x when Z x0 < (≤, -U x ). Whence β = (<, ∞).
This corresponds to the first case in the statement of the lemma. Let now restrict to the case when Z x0 ≥ (≤, -U x ). By definition of regions (cf. Definition 24) and Lemma 27, we have for a valuation v: v LU yx = (≤, v x -v y ) if v x ≤ U x and v y ≤ L y (<, -L y ) + (≤, v x ) if v x ≤ U x and v y > L y [START_REF] Bouyer | From Qualitative to Quantitative Analysis of Timed Systems[END_REF] Let G be the graph in which the edge 0 -→ x has weight min{(≤, U x ), ( 0x , c 0x )} and the rest of the edges are the same as that of G. This graph G represents the valuations of Z that have v x ≤ U x : [[G ]] = {v ∈ Z | v x ≤ U x }. We show that this set is not empty. For this we check that G does not have negative cycles. Since G does not have negative cycles, every negative cycle in G should include the newly modified edge 0 -→ x. Note that the shortest path value from x to 0 does not change due to this modified edge. So the only possible negative cycle in G is 0 -→ x -→ 0. But then we are considering the case when Z x0 ≥ (≤, -U x ), and so Z x0 + (≤, U x ) ≥ (≤, 0). Hence this cycle cannot be negative either. In consequence all the cycles in G are positive and [[G ]] is not empty.

To find β, it is sufficient to consider only the valuations in [[G ]]. As seen from Equation 9, among the valuations in [[G ]], we need to differentiate between those with v y ≤ L y and the ones with v y > L y . We proceed as follows. We first compute min{ v 9, for every v ∈ [[G 1 ]], [v] yx is given by (≤, v x -v y ) . Let ( 1 , w 1 ) be the shortest path from x to y in the graph G 1 . Then, we have for all v ∈ [[G 1 ]], v y -v x 1 w 1 . If 1 is ≤, then the least value of [v] yx would be (≤, -w 1 ) and if 1 is <, one can see that the least value of [v] yx is (<, -w 1 + 1). This shows that β 1 = ( 1 , -w 1 ) . It now remains to calculate ( 1 , w 1 ).

Recall that G 1 has the same edges as in G except possibly different edges 0 -→ x and 0 -→ y. If the shortest path from x to y has changed in G 1 , then clearly it should be due to one of the above two edges. However note that the edge 0 -→ x cannot belong to the shortest path from x to y since it would contain a cycle x -→ . . . 0 -→ x -→ . . . y that can be removed to give shorter path. Therefore, only the edge 0 -→ y can potentially yield a shorter path: x -→ . . . -→ 0 -→ y. However, the shortest path from x to 0 in G 1 cannot change due to the added edges since that would form a cycle with 0 and we know that all cycles in G 1 are positive. Therefore the shortest path from x to 0 is the direct edge x -→ 0, and the shortest path from x to y is the minimum of the direct edge x -→ y and the path x -→ 0 -→ y. We get: ( 1 , w 1 ) = min{( xy , c xy ), ( x0 , c x0 ) + (≤, L y )} which equals min{Z xy , Z x0 + (≤, L y )}. Finally, from the argument in the above two paragraphs, we get: Again, if [[G 2 ]] is empty, we set β 2 to (<, ∞). Otherwise, from Equation 9, for each valuation v ∈ [[G 2 ]], the value of [v] yx is given by (<, v x -L y ). For the minimum value, we need the least value of v x from v ∈ [[G 2 ]]. Let ( 2 , w 2 ) be the shortest path from x to 0 in G 2 . Then, since -v x 2 w 2 , the least value of v x would be -w 2 if 2 is ≤ and equal to -w 2 if 2 =< and β 2 would respectively be (<, -w 2 -L y ) or (<, -w 2 + 1 -L y ). It now remains to calculate ( 2 , w 2 ).

β 1 =      (<, ∞) if [[G 1 ]] = ∅ -Z xy if [[G 1 ]] = ∅
Recall that G 2 is G with 0 -→ x and y -→ 0 modified. The shortest path from x to 0 cannot include the edge 0 -→ x since it would need to contain a cycle, for the same reasons as in the β 1 case. So we get ( 2 , w 2 ) = min{Z x0 , Z xy + (< , -L y )}. If Z x0 ≤ Z xy + (<, -L y ), then we take ( 2 , w 2 ) as Z x0 , otherwise we take it to be Z xy + (<, -L y ). So, we get β 2 as the following:

β 2 =      (<, ∞) if [[G 2 ]] = ∅ -Z xy + (<,

Conclusions

Traditional methods for timed automata reachability store abstractions of zones for termination. Therefore, only convex abstractions have been used in implementations. We have proposed to store zones and use abstractions indirectly by means of inclusion tests Z ⊆ a(Z ). This allows us to use non-convex abstractions while still working with zones. The coarser the abstraction a, the higher is the possibility of inclusion, and hence smaller would be the reachability tree that is explored. For this construction to work efficiently, one also needs an efficient inclusion test.

In this paper, we have given a complete solution to using the a LU abstraction for the reachability algorithm. Firstly, we have given an O(|X| 2 ) test for Z ⊆ a LU (Z ) inclusion. This is the cornerstone of our approach since this test is used in the inner loop of the algorithm. Our test has the same complexity as Z ⊆ Z test used in the traditional algorithm. We have also shown that the a LU abstraction is the coarsest abstraction that is sound and complete with respect to reachability for all automata with the same LU -bounds. The result showing that a LU abstraction is the coarsest possible is quite unexpected. It works thanks to the observation that when doing forward exploration it is enough to consider only time-elapsed zones. This result explains why after Extra + LU from [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] there have been no new abstraction operators [START_REF] Bouyer | From Qualitative to Quantitative Analysis of Timed Systems[END_REF]. Indeed it is not that easy to find a better zone inside a LU abstraction than that given by Extra + LU abstraction.

The maximality result for a LU shows that to improve reachability testing even further we will need to look at new structural properties of timed automata, or to consider more refined algorithms than forward exploration. A work in this direction is [START_REF] Frédéric Herbreteau | Lazy abstractions for timed automata[END_REF].

Figure 1 :

 1 Figure 1: A comparison of abstraction operators for zones.

Proposition 12

 12 For every two valuations v and v :

Figure 2 :

 2 Figure 2: Adding the sequence seq(v) to A 1 .

Figure 3 Figure 3 :

 33 Figure 3 gives an example of a zone Z and its abstraction a LU (Z). It can be seen that a LU (Z) is not a convex set.

Figure 4 :

 4 Figure 4: Intuition for the adjustment lemma.

Figure 5 :

 5 Figure 5: A reachability tree of zones computed by a forward exploration

Figure 6 :

 6 Figure 6: An arbitrary zone with its constraints and distance graph

Figure 7 :

 7 Figure 7: v LU can be thought of as a transformation of [v] M by altering select constraints. Pictures (a) and (b) handle the case when vx > Ux; pictures (c) and (d) handle the case when vy > Ly

Definition 25 (

 25 These examples lead us to the definition of the distance graph G LU v for v LU as a transformation of the distance graph G M v . Distance graph G LU v ) Let v be valuation. Given the distance graph of the region [v] M in canonical form G M v = ( xy , c xy ) x,y∈X , first define the distance graph G = ( xy , c xy ) x,y∈X as follows:

  then v satisfies the constraints of G and hence v ∈ [[G ]]. Now for the other direction, assume v ∈ [[G ]]. We will show that v ∈ v LU . Let x, y be clocks such that v x ≤ U x and v y ≤ L y . From the definition of [[G ]], edges of the form y -→ x 0 and x 0 -→ x are retained as in

  LU yx | v ∈ [[G ]] and v y ≤ L y }. Call this β 1 . Next, we compute min{[v] yx | v ∈ [[G ]] and v y > L y } and set this as β 2 . Our required value β would then equal min{β 1 , β 2 }.To compute β 1 , consider the following distance graph G 1 which is obtained from G by just changing the edge 0 -→ y to min{(≤, L y ), ( 0y , c 0y )} and keeping the remaining edges the same as in G . The set of valuations[[G 1 ]] equals {v ∈ [[G ]] | v y ≤ L y }. If [[G 1 ]] = ∅, we set β 1 to (<,∞) and proceed to calculate β 2 . If not, we see that from Equation

  and Z xy ≤ Z x0 + (≤, L y ) -Z x0 + (≤, -L y ) if [[G 1 ]] = ∅ and Z xy > Z x0 + (≤, L y ) (10) We now proceed to compute β 2 = min{[v] yx | v ∈ [[G ]] and v y > L y }. Let G 2 be the graph which is obtained from G by modifying the edge y -→ 0 to min{Z y0 , (<, -L y )} and keeping the rest of the edges the same as in G . Clearly [[G 2 ]] = min{v ∈ [[G ]] | v y > L y }.

  1) if [[G 2 ]] = ∅ and Z x0 ≥ Z xy + (<, -L y ) -Z x0 + (<, -L y ) if [[G 2 ]] = ∅ and Z x0 < Z xy + (<, -L y )[START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF]

$ This work has been supported by project AVeRTS -CEFIPRA -Indo-French Program in ICST -DST/CNRS rf. 218093. Author B. Srivathsan is partially funded by a grant from Infosys Foundation.

x y 0 Z A B Figure 8: A bounded region is either totally contained in a zone Z or totally disjoint from it. It can never intersect partially. For example, the bounded region B is totally inside Z, however the bounded region A is totally disjoint from Z.

in valuation v if v x ≤ max(L x , U x ). If x, y are bounded in v, then the projection of the region [v] M onto x, y has very specific boundaries. Call it a bounded region. The following lemma makes use of the fact that a bounded region is either fully contained in a zone or is totally disjoint from it, that is, there cannot be a partial intersection of the bounded region and zone, as illustrated in Figure 8.

In the second case, we have edges x <d --→ y and y We can now prove Proposition 28.

Proof of Proposition 28

The distance graph min(G LU v , G Z ) represents the set v LU ∩ Z . By Proposition 23, the intersection is empty iff min(G LU v , G Z ) has a negative cycle. If there exist variables x, y such that Z xy + v LU yx < (≤, 0), then there is a negative cycle x -→ y -→ x in min(G LU v , G Z ) and hence v LU ∩ Z is empty. This shows the right-to-left direction.

The left-to-right direction is less trivial. Assume that v LU ∩ Z is empty. Then, there is a negative cycle N in min(G LU v , G Z ). To prove the proposition, we aim to show the following.

Aim. We show that the negative cycle N of min(G LU v , G Z ) can be reduced to the form:

Firstly, since both G LU v and G Z are canonical, we can assume without loss of generality that no two consecutive edges in N come from the same graph.

Suppose there are two edges y 1 -→ x 1 and y 2 -→ x 2 in N with weights coming from G LU v :

Since they are part of a negative cycle, their edge weights should be a finite value and by Part 1 of Lemma 27, this means:

. By Part 2 of Lemma 27, the edge values y 1 -→ x 1 and y 2 -→ x 2 are the same as in G M v . Consider the edge:

Again, from the same lemma, this edge value comes from G M v too. If the value of this edge y 1 -→ x 2 is smaller than the value of the path

in N , then this path can be replaced by the single edge y 1 -→ x 2 to get a smaller negative cycle in min(G LU v , G Z ). However, if the value of the path y

, then by Lemma 29:

v and hence we get a smaller negative cycle. Therefore in this case, we can eliminate the two edges y 1 -→ x 1 and y 2 -→ x 2 to get a smaller negative cycle containing either y 1 -→ x 2 or y 2 -→ x 1 . If N does not contain a variable z such that v z > L z , this elimination can be repeatedly applied and N can be reduced to a negative cycle of the form y -→ x -→ y with v y ≤ L y , v x ≤ U x and the edge weights y -→ x coming from G LU v and x -→ y coming from G Z , exactly as required by [START_REF] Berthomieu | An enumerative approach for analyzing time petri nets[END_REF].

However, we would like to write β 2 in terms of the cases used for β 1 in Equation 10 so that we can write β, which equals min{β 1 , β 2 }, conveniently.

Let ψ 1 be the inequation: Z xy ≤ Z x0 + (≤, L y ). From Equation 10, note that β 1 has been classified according to ψ 1 and ¬ψ 1 when [[G 1 ]] is not empty. Similarly, let ψ 2 be the inequation: Z x0 ≥ Z xy + (<, -L y ). From Equation 11we see that β 2 has been classified in terms of ψ 2 and ¬ψ 2 when [[G 2 ]] is not empty. Notice the subtle difference between ψ 1 and ψ 2 in the weight component involving L y : in the former the inequality associated with L y is ≤ and in the latter it is <. This necessitates a bit more of analysis before we can write β 2 in terms of ψ 1 and ¬ψ 1 .

Suppose Although ¬ψ 2 does not hold now, we can safely take β 2 to be -Z x0 + (<, -L y ) as its value is in fact equal to -Z xy + (<, 1) in this case. Summarizing the above two paragraphs, we can rewrite β 2 as follows:

We are now in a position to determine β as min{β 1 , β 2 }. Recall that we are in the case where Z x0 ≤ (≤, -U x ) and we have established that

] by construction, both of them cannot be simultaneously empty. Hence from Equations 10 and 12, we get β, the min{β 1 , β 2 } as:

There remains one last reasoning. To prove the lemma, we need to show that β = max{ -Z xy , -Z x0 + (<, -L y )}. For this it is enough to show the following two implications:

We prove only the first implication. We have a simple method that tells us when an LU-region v LU does not intersect a zone Z (Proposition 28). We have also characterized the potential valuation v from Z that could satisfy the non-intersection condition with Z (Proposition 31). This gives the necessary tools to solve inclusion Z ⊆ a LU (Z ). The following theorem presents the efficient inclusion test.

Theorem 32 Let Z, Z be non-empty zones. Then, Z ⊆ a LU (Z ) iff there exist two variables x, y such that:

Proof From Proposition 21, we know that Z ⊆ a LU (Z ) iff there exists a valuation v ∈ Z such that v LU does not intersect Z .

From Proposition 28, we know that v LU ∩ Z is empty iff there exists a variable x such that v x ≤ U x and a variable y such that:

This is possible for variables x, y iff the least value of v LU yx from among the valuations in Z satisfies the inequation ( 14) with Z xy . This is where we use Proposition 31. According to this proposition, for ( 14) to be true for some valuation v ∈ Z, we would need Z x0 ≥ (≤, -U x ) and:

Consider the first inequality: Z xy + -Z xy < (≤, 0). Let Z xy be ( xy , c xy ). If xy is the weak inequality ≤, then -Z xy is (≤, -c xy ) and hence the condition becomes: Z xy + (≤, -c xy ) < (≤, 0). This is equivalent to saying Z xy < (≤, c xy ), that is, Z xy < Z xy . Now, if xy is the strict inequality <, then -Z xy becomes (<, -c xy + 1) and hence the condition becomes: Z xy + (< , -c xy + 1) < (≤, 0). This is equivalent to saying Z xy < (<, c xy ). In both cases, the first inequality of Equation ( 15) becomes Z xy < Z xy .

By a similar reasoning, the second inequality of Equation ( 15) can be seen to correspond to Z xy + (<, -L y ) < Z x0 . This proves the theorem.

The Z ⊆ a LU (Z ) test involves a comparison of corresponding edges in the distance graphs G Z and G Z , so it takes in the worst case a O(|X| 2 ) number of steps. Notice that in fact the test requires only two tests for every pair of clocks.