BRICS RS-02-35 P. Bouyer: Timed Automata May Cause Some Troubles BRICS

Basic Research in Computer Science

Timed Automata May Cause Some Troubles

Patricia Bouyer BRICS Report Series RS-02-35 ISSN 0909-0878 August 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Patricia Bouyer.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/35/

Timed Automata May Cause Some Troubles

Patricia Bouyer^{∗}

LSV – CNRS UMR 8643 & ENS de Cachan  BRICS^{†}– Aalborg University
61, Av. du Président Wilson  Fredrik Bajers Vej 7E
94235 Cachan Cedex – France  9220 Aalborg Ø – Denmark

                   e-mail: bouyer@cs.auc.dk

Abstract

Timed automata are a widely studied model. Its decidability has been proved using the so-called region automaton construction. This construction provides a correct abstraction for the behaviours of timed automata, but it does not support a natural implementation and, in practice, algorithms based on the notion of zones are implemented using adapted data structures like DBMs. When we focus on forward analysis algorithms, the exact computation of all the successors of the initial configurations does not always terminate. Thus, some abstractions are often used to ensure termination, among which, a widening operator on zones.

In this paper, we study in details this widening operator and the forward analysis algorithm that uses it. This algorithm is most used and implemented in tools like Kronos and Uppaal. One of our main results is that it is hopeless to find a forward analysis algorithm, that uses such a widening operator, and which is correct. This goes really against what one could think. We then study in details this algorithm in the more general framework of updatable timed automata, a model which has been introduced as a natural syntactic extension of classical timed automata. We describe subclasses of this model for which a correct widening operator can be found.

1 Introduction

Real-Time Systems. Since their introduction by Alur and Dill in [AD90, AD94], timed automata are one of the most studied models for real-time systems. Numerous works have been devoted to the “theoretical” comprehension of timed automata: determinization [AFH94], minimization [ACD^{+}92], power of clocks [ACH94, HKWT95], power of ε-transitions [BDGP98], extensions of the model [DZ98, HRS98, CG00, BFH^{+}01], logical characterizations [Wil94, HRS98],… have in particular been investigated. Practical aspects of the model have also been studied and several model-checkers are now available (HyTech^{1} [HHWT97], Kronos^{2} [DOTY96], Uppaal^{3} [LPY97]). Timed automata afford to modelize many real-time systems and the existing model-checkers have allowed to verify a lot of industrial case studies (see the web pages of the tools or, for example, [HSLL97, TY98]).

∗This work has been partly supported by the french project RNRT “Calife”.

†Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

Implementation of Timed Automata. The decidability of the timed automata model has been proved by Alur and Dill in [AD90, AD94]. It is based on the construction of the so-called region automaton: it abstracts finitely and in a correct way the behaviours of timed automata. However, in practice, such a construction is not implemented, because it does not support a natural implementation, but algorithms glancing on-the-fly through the automaton are preferred. These algorithms are based on the notion of zones and can be efficiently implemented using data structures like DBMs [Dil89] and CDDs [BLP^{+}99]. Among these algorithms are the forward analysis algorithms that compute all the reachable configurations. However, the exact forward computation does not always terminate. Abstractions have been proposed to avoid this termination problems (see for example [DT98]) and they are implemented in tools like Kronos and Uppaal.

Our contributions. In this paper, we study in details one of the abstractions proposed in [DT98]. It consists in a widening operator that is applied to zones to enforce the termination of the forward searching in the timed automaton. The most important result is that, against what one can think, there is no way to find a correct forward analysis algorithm for timed automata that uses this widening operator. We then consider the more general framework of updatable timed automata, as defined in [BDFP00a]. This model is a syntactic extension of the classical timed automata coming from a model built for a communication protocol in [BF99] and its decidability has been precisely settled in [BDFP00a]. We then describe several subclasses of this model for which we can find a correct widening operator and thus a correct forward analysis algorithm. These subclasses contain in particular all the timed automata that do not use comparisons between clocks. From this study, it appears that problems in the correctness of the widening operator come only from the nature of the constraints which are used in the automata, but not from the syntactic macros that have been added in the updatable timed automata model.

1http://www-cad.eecs.berkeley.edu:80/˜ tah/HyTech/

2http://www-verimag.imag.fr/TEMPORISE/kronos/

3http://www.uppaal.com/

Outline of the paper. The structure of the paper is the following: we first recall some background on the implementation of timed automata and we describe the forward analysis algorithm that uses the widening operator we will study (section 2) ; we then discuss the correctness of this algorithm and get that, even if surprising, the algorithm is not correct in general (section 3) ; we then present the updatable timed automata framework (section 4) and we study very precisely the correctness of the widening operator (section 5) ; we also propose an implementation of the algorithm for the subclasses of updatable timed automata for which a correct widening operator can be found (section 5) ; we discuss some other methods for all the automata for which we can not propose a correct widening operator ; we finally conclude with some remarks (section 6).

Some technical proofs of this paper are presented in Appendix (page 42).

2 Implementation of Timed Automata, State of the Art

In this section, we present the basic notions for timed automata [AD90, AD94], and we focus on implementation issues for this model. In particular, we present an algorithm which is implemented in some tools.

2.1 Preliminaries

If Z is any set, let Z^{∗} be the set of finite sequences of elements in Z. We consider as time domain 𝕋 the set ℚ^{+} of non-negative rationals or the set ℝ^{+} of non-negative reals and Σ as a finite set of actions. A time sequence over 𝕋 is a finite non decreasing sequence τ = (t_{i})_{1≤i≤p} ∈ 𝕋^{∗}. A timed word ω = (a_{i}, t_{i})_{1≤i≤p} is an element of (Σ × 𝕋)^{∗}, also written as a pair ω = (σ, τ), where σ = (a_{i})_{1≤i≤p} is a word in Σ^{∗} and τ = (t_{i})_{1≤i≤p} a time sequence in 𝕋^{∗} of same length.

2.1.1 Clock Valuations.

We consider a finite set X of variables, called clocks. A clock valuation over X is a mapping v : X → 𝕋 that assigns to each clock a time value. The set of all clock valuations over X is denoted 𝕋^{X}. Let t ∈ 𝕋, the valuation v + t is defined by (v + t)(x) = v(x) + t, ∀x ∈ X. We also use the notation (α_{i})_{1≤i≤n} for the valuation v such that v(x_{i}) = α_{i}. For a subset C of X, we denote by [C ← 0]v the valuation such that for each x ∈ C, ([C ← 0]v)(x) = 0 and for each x ∈ X \ C, ([C ← 0]v)(x) = v(x).

2.1.2 Clock Constraints.

Given a set of clocks X, we introduce two sets of clock constraints over X. The most general one, denoted by C(X), is defined by the following grammar:

φ ::= x ∼ c | x − y ∼ c | φ ∧ φ | true
where x, y ∈ X, c ∈ ℚ, ∼ ∈ {<, ≤, =, ≥, >}

We also use the proper subset of diagonal-free constraints where the comparison between two clocks is not allowed. This set is denoted by C_{df}(X) and is defined by the grammar:

φ ::= x ∼ c | φ ∧ φ | true,
where x ∈ X, c ∈ ℚ and ∼ ∈ {<, ≤, =, ≥, >}

We write v ⊧ φ when the clock valuation v satisfies the clock constraint φ.

A k-bounded clock constraint is a clock constraint that involves only constants between −k and +k.

2.1.3 Timed Automata.

A timed automaton over 𝕋 is a tuple A = (Σ, Q, T, I, F, X), where Σ is a finite alphabet of actions, Q is a finite set of states, X is a finite set of clocks, T ⊆ Q × [C(X) × Σ × 2^{X}] × Q is a finite set of transitions, I ⊆ Q is the subset of initial states and F ⊆ Q is the subset of final states. A path in A is a finite sequence of consecutive transitions:

P = q_{0} ⟶^{φ_{1},a_{1},C_{1}} q_{1} … q_{p−1} ⟶^{φ_{p},a_{p},C_{p}} q_{p}

where (q_{i−1}, φ_{i}, a_{i}, C_{i}, q_{i}) ∈ T for each 1 ≤ i ≤ p.

The path is said to be accepting if it starts in an initial state (q_{0} ∈ I) and ends in a final state (q_{p} ∈ F). A run of the automaton through the path P is a sequence of the form:

⟨q_{0}, v_{0}⟩ ⟶_{t_{1}}^{φ_{1},a_{1},C_{1}} ⟨q_{1}, v_{1}⟩ … ⟶_{t_{p}}^{φ_{p},a_{p},C_{p}} ⟨q_{p}, v_{p}⟩

where τ = (t_{i})_{1≤i≤p} is a time sequence and (v_{i})_{1≤i≤p} are clock valuations defined by:

\{ \begin{matrix}v_{0}(x) = 0, ∀x ∈ X \\ v_{i−1} + (t_{i} − t_{i−1}) ⊧ φ_{i} \\ v_{i} = [C_{i} ← 0] (v_{i−1} + (t_{i} − t_{i−1})) \end{matrix}

The label of the run is the timed word w = (a_{1}, t_{1}) … (a_{p}, t_{p}). If the path P is accepting then the timed word w is said to be accepted by the timed automaton. The set of all timed words accepted by A is denoted by L(A).

2.2 Practical Issues

For verification purposes, a fundamental question about timed automata is to decide whether the accepted language is empty. This problem is called the emptiness problem. A class of timed automata is said decidable if the emptiness problem is decidable for this class. Note that this problem is equivalent to the reachability problem which tests whether a state can be reached in a timed automaton.

Alur and Dill proved in [AD90, AD94] that the emptiness problem is decidable for timed automata. The proof of this result is based on a “region automaton construction”. In practice, this construction is not implemented because it does not support a natural implementation and it suffers from an enormous combinatorics explosion. The idea of the region automaton is to construct a finite simulation graph for the automaton based on an equivalence relation (of finite index) defined on the clock valuations. Some works have been done to reduce the size of this simulation graph by enlarging the equivalence relation, see for example [ACD^{+}92, YL97, TY01]. However, in practice, such graphs are not constructed and on-the-fly zone algorithms glancing symbolically through the graph are implemented. One of the advantages of these algorithms is that they can easily be implemented using the Difference Bounded Matrices data structure (DBM for short), initially proposed by [Dil89]. For example, forward analysis algorithms (that is algorithms computing step-by-step the successors of the initial configurations) [Alu99] are implemented in tools like Uppaal [BL96, LPY97] or Kronos [BTY97, Daw97, Yov98]. The forward analysis algorithm computing the exact set of successors does not always terminate; in [MP99], subclasses of classical timed automata, for which termination is guaranteed, are proposed, but these classes are a bit restrictive. Different kinds of abstractions [DT98] are thus proposed to enforce the termination, among which a widening operator on zones.

The aim of this paper is to study in details the widening operator proposed in [DT98] and implemented in tools like Kronos and Uppaal. We will thus now present the widening operator defined in [DT98] and describe the forward analysis algorithm which uses this operator. This algorithm is implemented in some tools for the verification of classical timed automata. We also explain how this algorithm is implemented using the DBM data structure. Note that this data structure, apart from being adapted to the implementation of algorithms for timed automata, is very interesting in that it will be useful to prove properties of timed automata.

2.3 A Forward Analysis Algorithm for Timed Automata

2.3.1 Zones.

A zone is a subset of 𝕋^{n} defined by a general clock constraint. Let k be a constant. A k-bounded zone is a zone defined by a k-bounded clock constraint. Let Z be a zone. The set of k-bounded zones containing Z is finite and not empty (𝕋^{n} is a k-bounded zone and contains Z), the intersection of these kbounded zones is a k-bounded zone containing Z, and is thus the smallest one having this property. It is called the k-approximation of Z and is denoted Approx_{k}(Z).

Example 1 Consider the zone Z drawn with on the figure beside: Z is defined by the clock constraint

1 < x < 4 ∧ 2 < y < 4 ∧ x − y < 1.

Taking k = 2, the k-approximation of Z is drawn adding the part ; it is defined by the clock constraint

1 < x ∧ 2 < y ∧ x − y < 1.

0 1 2  4 x 124y

2.3.2 The Algorithm.

Let A be a classical timed automaton. If e = (q ⟶^{g,a,C:=0} q′) is a transition of A and if Z is a zone, then Post(Z, e) denotes the set [C ← 0](g ∩ \overrightarrow{Z}) where \overrightarrow{Z} represents the future of Z and is defined by

\overrightarrow{Z} = \{v + t | v ∈ Z and t ≥ 0\}

Post(Z, e) is the set of valuations which can be reached by waiting in the current state, q, and then taking the transition e. We associate with A the largest constant, k, appearing in A (i.e. the largest constant c such that there is a constraint x ∼ c for some clock x or x − y ∼ c for some clocks x and y). A maximal constant can be computed for each clock x (in a similar way), but for our purpose, it does not change anything, the presentation would just be a bit more complicated.

One of the forward analysis algorithms for classical timed automata uses the k-approximation (cf section 2.3.1) as a widening operator. It is presented as Algorithm 1 (q_{0} is the initial location of the automaton whereas Z_{0} represents the initial zone, it is often the valuation where all the clocks are set to zero).

Algorithm 1 Algorithm using k-Approximations for Classical Timed Automata # TA-Algorithm (A:TA) { # Define k as the maximal constant appearing in A; # Visited := ∅; (* Visited stores the visited states *) # Waiting := {(q_{0},Approx_{k}(Z_{0}))}; # Repeat # Get and Remove (q,Z) from Waiting; # If q is final # then {Return “Yes”;} # else {If there is no (q,Z’) ∈ Visited such that Z ⊆ Z’ # then {Visited := Visited ∪ {(q,Z)}; # Successor := {(q’,Approx_{k}(Post(Z,e))) | # e transition from q to q’}; # Waiting := Waiting ∪ Successor;}} # Until (Waiting = ∅); # Return “No”; }

We first point out that this algorithm terminates because there are finitely many k-bounded zones and thus finitely many k-approximations of zones that can be computed for each control state of the automaton. This algorithm computes step-by-step an overapproximation of the set of reachable states and tests whether this approximation intersects the set of final states. Thus, if the answer of the algorithm is “No”, it is sure that no final state can be reached. However, if the answer is “Yes”, it can a priori be the case that the overapproximation intersects the set of final states whereas the exact set of reachable states does not intersect this set. We will discuss in details the correctness of Algorithm 1 in Section 3.

2.4 The Implementation: the DBM Data Structure

In order to implement Algorithm 1, an adapted data structure is needed to represent the zones and this data structure must allow to test for inclusion of zones and to compute easily the different operations used in the algorithm, that is the intersection of two zones, the future of a zone, the image of a zone by a reset and the k-approximation of a zone. Tools like Uppaal or Kronos use the data structure proposed by Dill in [Dil89], the DBM data structure. A detailed presentation of this data structure can be found in [CGP99] and in [Ben02]. However, we will recall some basic properties of it because it will be the core tool in the rest of the paper.

A difference bounded matrice (say DBM for short) for n clocks is an (n + 1)- square matrice of pairs

(m; ≺) ∈ 𝕍 = (ℤ × {<, ≤}) ∪ {(∞; <)}.

A DBM M = (m_{i,j}, ≺_{i,j})_{i,j=1...n} defines the following subset of 𝕋^{n} (the clock x_{0} is supposed to be always equal to zero, i.e. for each valuation v, v(x_{0}) = 0):

{v : {x_{1}, …, x_{n}} ⟶ 𝕋 | ∀ 0 ≤ i, j ≤ n, v(x_{i}) − v(x_{j}) ≺_{i,j} m_{i,j}}

where γ < ∞ means that γ is some real (there is no bound on it). This subset of 𝕋^{n} is a zone and will be denoted, in what follows, by ⟦M⟧. Each DBM on n clocks represents a zone of 𝕋^{n}. Note that several DBMs can define the same zone.

Example 2 The zone defined by the equations x_{1} > 3 ∧ x_{2} ≤ 5 ∧ x_{1} − x_{2} < 4 can be represented by the two DBMs

( \begin{matrix}(0; ≤) & (−3; <) & (∞; <) \\ (∞; <) & (0; ≤) & (4; <) \\ (5; ≤) & (∞; <) & (0; ≤) \end{matrix} ) and ( \begin{matrix}(∞; <) & (−3; <) & (∞; <) \\ (∞; ≤) & (∞; <) & (4; <) \\ (5; ≤) & (∞; <) & (0; ≤) \end{matrix} )

Thus the DBMs are not a canonical representation of zones. Moreover, it isn’t possible to test syntactically whether ⟦M_{1}⟧ = ⟦M_{2}⟧. A normal form has thus been defined for representing zones. Its computation uses the Floyd algorithm and some syntactic rewritings (see [Dil89, CGP99] for a description of this procedure). In what follows, we denote by ϕ(M) the normal form of M. Before stating some very important properties of the normal form, we define a total order on 𝕍 in the following way: if (m; ≺), (m′; ≺′) ∈ 𝕍, then

(m; ≺) ≤ (m′; ≺′) ⟺ \{ \begin{matrix}m < m′ \\ or \\ m = m′ and either ≺ = ≺′ or ≺′ = ≤ . \end{matrix}

Of course, for each m ∈ ℤ, it holds that m < ∞. We define >, ≥ and < in a natural way. These orders are extended to the DBMs in the following way: let M = (m_{i,j}; ≺_{i,j})_{i,j=0...n} and M′ = (m′_{i,j}; ≺′_{i,j})_{i,j=0...n} be two DBMs, then

M ≤ M′ ⟺ for every i, j = 0 … n, (m_{i,j}; ≺_{i,j}) ≤ (m′_{i,j}; ≺′_{i,j}).

We can now state some (very useful) properties of normal forms. If M and M′ are DBMs, then:

{(i) ⟦M⟧ = ⟦ϕ(M)⟧ and ϕ(M) ≤ M, \atop (ii) ⟦M⟧ ⊆ ⟦M′⟧ ⟺ ϕ(M) ≤ M′ ⟺ ϕ(M) ≤ ϕ(M′).}

The last point expresses the fact that the test for inclusion of zones can be checked syntactically on the normal forms of the DBMs (representing the zones). Normal forms of DBMs can be characterized in a natural way. If M = (m_{i,j}; ≺_{i,j})_{i,j=0...n} is a DBM such that ⟦M⟧ ≠ ∅, then the two following properties are equivalent:

(i) M is in normal form,

(ii) for every i, j = 0 … n, for every real −m_{j,i} ≺_{j,i} r ≺_{i,j} m_{i,j}, there exists a valuation v ∈ ⟦M⟧ such that v(x_{j}) − v(x_{i}) = r (still assuming that v(x_{0}) = 0).

This property expresses the fact that if a DBM is in normal form, then no constraint of this DBM can be tightened using the Floyd algorithm.

The emptiness can be checked on the DBMs, even if they are not in normal form. For this, we define an addition on the set 𝕍:

(m; ≺) + (m′; ≺′) = (m′′; ≺′′)

where m′′ = m+m′ and ≺′′ is ≤ if both ≺ and ≺′ are ≤ and ≺′′ is < otherwise. Now, if M = ((m_{i,j}; ≺_{i,j})_{i,j}) is a DBM, ⟦M⟧ = ∅ if and only if there exists a negative cycle in M, which means that there exists a sequence of distinct indices (i_{1}, i_{2}, …, i_{l−1}, i_{l} = i_{1}) such that

(m_{i_{1},i_{2}}; ≺_{i_{1},i_{2}}) + (m_{i_{2},i_{3}}; ≺_{i_{2},i_{3}}) + ⋯ + (m_{i_{l−1},i_{l}}; ≺_{i_{l−1},i_{l}}) < (0; ≤)

This condition will be used a lot in the remainder of the paper.

2.4.1 Computation of Some Operations on DBMs.

As we argued at the beginning of the section, the data structure used to represent zones must also be appropriate to compute the four operations on zones that are used by Algorithm 1, namely future, intersection, image by resets and k-approximation. These operations on DBMs are described nicely in [CGP99] and [Ben02], here we recall them quickly.

Intersection. Assume that M = (m_{i,j}; ≺_{i,j})_{i,j=1...n} and M′ = (m′_{i,j}; ≺′_{i,j} )_{i,j=1...n} are two DBMs. Then, defining M′′ = (m′′_{i,j}; ≺′′_{i,j})_{i,j=1...n} by

(m′′_{i,j}; ≺′′_{i,j}) = min((m_{i,j}; ≺_{i,j}), (m′_{i,j}; ≺′_{i,j})) for all indices i, j = 1 … n.

We get that ⟦M′′⟧ = ⟦M⟧ ∩ ⟦M′⟧. Note that it can be the case that M′′ is not in normal form, even if M and M′ are in normal form.

Future. Assume that M = (m_{i,j}; ≺_{i,j})_{i,j=1...n} is a DBM in normal form. We define the DBM \overrightarrow{M} = (m′_{i,j}; ≺′_{i,j})_{i,j=1...n} by:

\{ \begin{matrix}(m′_{i,j}; ≺′_{i,j}) = (m_{i,j}; ≺_{i,j}) if j ≠ 0 \\ (m′_{i,0}; ≺′_{i,0}) = (∞; <) \end{matrix} .

We get that ⟦\overrightarrow{M}⟧ = \overrightarrow{⟦M⟧} and that the DBM \overrightarrow{M} is in normal form.

Image by resets. Assume that M = (m_{i,j}; ≺_{i,j})_{i,j=1...n} is a DBM in normal form. We define the DBM M_{x_{k}:=0} = (m′_{i,j}; ≺′_{i,j})_{i,j=1...n} by:

\{ \begin{matrix}(m′_{i,j}; ≺′_{i,j}) = (m_{i,j}; ≺_{i,j}) & if i, j ≠ k \\ (m′_{k,k}; ≺′_{k,k}) = (m′_{k,0}; ≺′_{k,0}) = (m′_{0,k}; ≺′_{0,k}) = (0; ≤) \\ (m′_{i,k}; ≺′_{i,k}) = (m_{i,0}; ≺_{i,0}) & if i ≠ k \\ (m′_{k,i}; ≺′_{k,i}) = (m_{0,i}; ≺_{0,i}) & if i ≠ k \end{matrix}

We get that ⟦M_{x_{k}:=0}⟧ = [x_{k} ← 0]⟦M⟧ and that the DBM M_{x_{k}:=0} is in normal form.

k-approximation. Assume that M = (m_{i,j}; ≺_{i,j})_{i,j=1...n} is a DBM in normal form. We define the DBM M_{k} = (m′_{i,j}; ≺′_{i,j})_{i,j=1...n} by:

\{ \begin{matrix}(m′_{i,j}; ≺′_{i,j}) = (m_{i,j}; ≺_{i,j}) & if − k ≤ m_{i,j} ≤ k \\ (m′_{i,j}; ≺′_{i,j}) = (∞; <) & if m_{i,j} > k \\ (m′_{i,j}; ≺′_{i,j}) = (−k; <) & if m_{i,j} < −k \end{matrix}

We get that ⟦M_{k}⟧ = Approx_{k}(⟦M⟧), but M_{k} is not in normal form.

Combining all these constructions, if e is a transition of the form q ⟶^{g,a,C:=0} q′ and if M is a DBM representing a zone Z, using what precedes, it is easy to compute a DBM which represents the zone Approx_{k}([C ← 0](g ∩ \overrightarrow{Z})) = Approx_{k}(Post(Z, e)). This DBM may not be in normal form. The DBM data structure can thus be used to compute all the operations needed by Algorithm 1.

3 Correctness Problems

As argued in Section 2.3.2, Algorithm 1 raises a correctness problem. Indeed, it computes an overapproximation of the set of reachable states which can a priori be strictly larger than the set of reachable states. This algorithm is much implemented and used, nevertheless, we did not find any complete proof of its correctness in the literature. There exist of course several papers claiming that they present such proofs but these proofs are incomplete and even sometimes incorrect:

• In the PhD. Thesis [Tri98], the implementation of the c-closure presented page 127 (of [Tri98]) corresponds to our Approx_{c} approximation. Thus, their Yes/No Algorithm should correspond to Algorithm 1. However, the definition of the c-closure given page 21 does not correspond to the implementation. For example, consider the following graph where c is 2:

zone Z

c-closure of Z what the implementation

really computes

The proof of correctness of the Yes/No Reachability Algorithm (Lemma 5.9 page 58) is done using the c-closure which is defined and not the one which is implemented. Thus, the correctness of the implemented algorithm is not complete in this paper.

• In the PhD. Thesis [WT94], if Z is a zone then round(Z) corresponds to our Approx_{k} overapproximation. The theorem which aims at proving that Algorithm 1 is correct is Theorem 4.8 on page 90. The proof is done in the following way: considering a zone Z, it is decomposed into finitely many subzones that are assumed to be included in regions, then the computation of the round operator is done first for the subzones (this step is easy); round(Z) is obtained by computing the union of the round of these subzones. But round is not compatible with union, for example have a look at the following zone:

zone Z

round applied to the subzones of Z

round(Z)

Besides, this proof only aimed at proving the correctness of Algorithm 1 when we restrict to diagonal-free timed automata.

A surprising observation...

In trying to write a complete proof for the correctness of Algorithm 1, we have had some troubles, and studying precisely what were the problems we were confronted to, we have been forced to face the facts that Algorithm 1 can not be correct! Consider for example the automaton Cex depicted on figure 1.

iq x_{3} ≤ 3 \{x_{3}, x_{1}\} := 0 x_{2} = 3 x_{2} := 0 x_{1} = 2, x_{1} := 0 x_{2} = 2, x_{2} := 0 \begin{matrix}x_{1} = 2, \\ x_{1} := 0 \end{matrix} x_{2} = 2 x_{2} := 0 x_{1} = 3 x_{1} := 0 x_{2} > x_{1} + 2 x_{4} < x_{3} + 2 Error  The loop

Figure 1: A surprising counter-example, Cex

It is just a matter of computing successors of zones to get that the zones we can reach in state q, when we start with the valuation where all the clocks are set to zero in state i, are

\{ \begin{matrix}x_{3} ≥ 2α + 5 \\ x_{2} ≥ 1 \\ x_{4} ≥ 2α + 6 \\ 1 ≤ x_{2} − x_{1} ≤ 3 \\ x_{3} − x_{1} = 2α + 5 \\ 2α + 6 ≤ x_{4} − x_{1} ≤ 2α + 8 \\ 2α + 2 ≤ x_{3} − x_{2} ≤ 2α + 4 \\ x_{4} − x_{2} = 2α + 5 \\ 1 ≤ x_{4} − x_{3} ≤ 3 \end{matrix}

where α is the number of loops which are taken (we call Z_{α} this zone). This kind of zones is depicted on figure 3. We can then notice that, for every α, if we impose the condition x_{4} − x_{3} < 2 in Z_{α}, then x_{2} − x_{1} < 2 because

x_{2} − x_{1} = (x_{2} − x_{4}) + (x_{4} − x_{3}) + (x_{3} − x_{1})
< (−2α − 5) + 2 + (2α + 5)
< 2

Thus, the state “Error” of Cex is not reachable. However, if we fix a maximal constant M and if we use the widening operator using this constant M (that

x_{1} x_{2}  x_{3} x_{4} [1; 3]  [1; 3] [2α + 5] [2α + 5] [2α + 2; 2α + 4] [2α + 6; 2α + 8]

Figure 2: The zone Z_{α}

is if we use the operator Approx_{M}), then for a number of loops α sufficiently large (that is such that 2α + 5 > M), the constraint (x_{3} − x_{1} ≤ 2α + 5) will be erased when we will apply the widening operator and thus Algorithm 1 will conclude that the state “Error” is reachable. Thus, we conclude that for the automaton Cex, there exists no widening operator which is correct with respect to reachability. From this counter-example, we get that the widening operator is not correct with respect to reachability and this was a big surprise! More precisely, we can state the following result:

Theorem 1 There is no way to have a correct forward analysis algorithm for timed automata that uses a widening operator on zones.

The aim of the rest of this paper is to study more precisely where appear the problems and to bring out subclasses for which we can find a correct widening operator. We decided to do this study in the more general framework of updatable timed automata, as defined in [BDFP00a].

4 The Updatable Timed Automata Framework

Updatable timed automata are a syntactic extension of timed automata that has been introduced in [BDFP00a]. We will now present the model, the basic results and propose a first algorithm which is correct for all the updatable timed automata that are decidable.

4.1 Definitions

4.1.1 Updates.

An update is a function from 𝕋^{X} to P(𝕋^{X}) which assigns to each valuation a set of valuations. In this work, updates are restricted according to the following definitions.

A simple update over a clock z has one of the two following forms:

up ::= z :∼ c | z :∼ y + c
where c ∈ ℚ, y ∈ X and ∼ ∈ {<, ≤, =, ≥, >}

Let v be a valuation and up be a simple update over z. A valuation v′ is in up(v) if v′(y) = v(y) for any clock y ≠ z and if v′(z) verifies (∼ ∈ {<, ≤, =, ≠, ≥, >}):

\{ \begin{matrix}v′(z) ∼ c and v′(z) ≥ 0 & if up = z :∼ c \\ v′(z) ∼ v(y) + d and v′(z) ≥ 0 & if up = z :∼ y + d \end{matrix}

In what follows, an update over a set of clocks X is a collection up = (up_{i})_{1≤i≤k}, where each up_{i} is a simple update over some clock x_{i} ∈ X (note that it could happen that x_{i} = x_{j} for some i ≠ j). Let v, v′ ∈ 𝕋^{n} be two clock valuations, v′ ∈ up(v) if and only if, for all i, the clock valuation v_{i} defined by

\{ \begin{matrix}v_{i}(x_{i}) & = & v′(x_{i}) \\ v_{i}(y) & = & v(y) for any y ≠ x_{i} \end{matrix}

is in up_{i}(v). The set of updates over the set of clocks X is denoted by U(X).

Example 3 For the update up = (x :> y, x :< 7), a valuation v′ is in up(v) if the value v′(x) verifies: v′(x) > v(y) ∧ v′(x) < 7. Note that up(v) may be empty. For instance, the update (x :< 1, x :> 1) leads to the empty set.

An update is a reset whenever it is a collection of simple updates of the form x := 0. The set of resets is denoted by U_{0}(X). For a subset C of X, if up is the reset ⋀_{x∈C} x := 0 (we write C := 0), for each valuation v, the valuation up(v) is also denoted by [C ← 0]v.

4.1.2 Updatable Timed Automata.

An updatable timed automaton over 𝕋 is a 6-tuple A = (Σ, Q, T, I, F, X), where Σ is a finite alphabet of actions, Q is a finite set of states, X is a finite set of clocks, T ⊆ Q × [C(X) × Σ × U(X)] × Q is a finite set of transitions, I ⊆ Q is the subset of initial states and F ⊆ Q is the subset of final states. A path in A is a finite sequence of consecutive transitions:

P = q_{0} ⟶^{φ_{1},a_{1},up_{1}} q_{1} … q_{p−1} ⟶^{φ_{p},a_{p},up_{p}} q_{p}

where (q_{i−1}, φ_{i}, a_{i}, up_{i}, q_{i}) ∈ T for each 1 ≤ i ≤ p.

The path is said to be accepting if it starts in an initial state (q_{0} ∈ I) and ends in a final state (q_{p} ∈ F). A run of the automaton through the path P is a sequence of the form:

⟨q_{0}, v_{0}⟩ ⟶_{t_{1}}^{φ_{1},a_{1},up_{1}} ⟨q_{1}, v_{1}⟩ … ⟶_{t_{p}}^{φ_{p},a_{p},up_{p}} ⟨q_{p}, v_{p}⟩

where τ = (t_{i})_{1≤i≤p} is a time sequence and (v_{i})_{1≤i≤p} are clock valuations defined by:

\{ \begin{matrix}v_{0}(x) = 0, ∀x ∈ X \\ v_{i−1} + (t_{i} − t_{i−1}) ⊧ φ_{i} \\ v_{i} ∈ up_{i} (v_{i−1} + (t_{i} − t_{i−1})) \end{matrix}

The label of the run is the timed word w = (a_{1}, t_{1}) … (a_{p}, t_{p}). If the path P is accepting then the timed word w is said to be accepted by the timed automaton. The set of all timed words accepted by A is denoted by L(A).

Example 4 Consider a system that handles data which come from an external environment. The time needed to deal the data depends on its (bounded) size. Updatable timed automata provide an elegant and concise way to model such a system. Indeed, it is sufficient to store the size in a variable taking nondeterministically a value less than 3 (assuming that the maximum size for the data is 3).

p  q 0 ≤ size− init < 1, Handling NewData, size :< 3 ∧ init := 0 1 ≤ size− init < 2, Handling 2 ≤ size− init < 3, Handling

Let C ⊆ C(X) be a set of clock constraints and U ⊆ U(X) be a set of updates, the class Aut(C, U) is the set of all updatable timed automata whose transitions only use clock constraints of C and updates of U only. The usual class of timed automata, defined in [AD90, AD94], is the family Aut(C_{df}(X), U_{0}(X)). However, what we now usually call the family of classical timed automata, as presented in section 2.1.3, is the family Aut(C(X), U_{0}(X)).

4.1.3 Known Results about the Emptiness Problem.

We characterized the decidable subclasses of updatable timed automata in [BDFP00a]. The following tabular summarizes roughly the results:

U_{0}(X) ∪ { … }  Diagonal-free clock constraints  General clock constraints
x := c, x := y  Pspace-complete
x := x + 1  Pspace-complete
x := y + c  Undecidable
x := x − 1  Undecidable

x := y − c

x :< c

Pspace-complete

Pspace-complete

x :> c Undecidable

x :∼ y + c y + c <: x :< y + d

y + c <: x :< z + d  Undecidable

with ∼ ∈ {≤, <, >, ≥} and c, d ∈ ℚ^{+}.

The table reads as follows: the class of updatable timed automata that only use diagonal-free clock constraints but that also use decrementation updates (i.e. updates of the form x := x − 1) is undecidable whereas the class of updatable timed automata that use general clock constraints and updates of the form x :< c is decidable using a Pspace algorithm.

The proof of these decidability results is based on the generalization of the construction of the region automaton for classical timed automata (as presented in [AD90, AD94]). For the following of the paper, we will need more precise decidability results, we present them now.

4.2 Regions and Precise Results about Decidability [BDFP00a]

4.2.1 Regions.

The definition of regions we use in this paper is the one presented in [BDFP00a]. It is a bit different from the initial definition of Alur and Dill [AD90, AD94]. We will see the difference in Example 5. Let X be a set of clocks, n = |X| and

α = ((max_{x})_{x∈X}; (max_{x,y})_{x,y∈X}) ∈ ℕ^{n} × (ℤ × ℤ)^{n^{2}}

be a tuple such that for every x, y ∈ X, \{ \begin{matrix}− max_{y,x} ≤ max_{x,y} \\ max_{x,y} ≤ max_{x} \end{matrix} .

The tuple α defines a set of regions R_{α}: a region R of R_{α} is defined by a tuple

((I_{x})_{x∈X}; (J_{x,y})_{x≠y∈X}; ≺)

where:

• I_{x} is one of the following intervals:

] − ∞; −max_{x}[ ; ]max_{x}; +∞[ ;
]c; c + 1[ where − max_{x} ≤ c < max_{x}
or {c} where − max_{x} ≤ c ≤ max_{x}

• J_{x,y} is one of the following intervals:

] − ∞; −max_{y,x}[ ; ]max_{x,y}; +∞[ ;
]c; c + 1[ where − max_{y,x} ≤ c < max_{x,y}
or {c} where − max_{y,x} ≤ c ≤ max_{x,y}

• ≺ is a total preorder defined on the set

{x | ∃ c ∈ [− max_{x}; max_{x}[ such that I_{x} =]c; c + 1[}.

A valuation v is in the region R if:^{4}

v(x) ∈ I_{x}  for each x ∈ X
I_{x} =]max_{x}; +∞[ or I_{y} =]max_{y}; +∞[ ⟹ v(x) − v(y) ∈ J_{x,y} for every x ≠ y ∈ X
x ≺ y ⟹ frac(v(x)) ≤ frac(v(y))  for every x, y ∈ X.

Note that for a valuation v, there is a unique region in R_{α} containing v; it is denoted by [v]_{α}.

Example 5 We define the tuple

α = ((max_{x}, max_{y}), (max_{x,y}, max_{y,x})) as

max_{x} = 3, max_{y} = 2, max_{x,y} = 2, max_{y,x} = 0

The set of regions R_{α} is represented on the figure beside. The region drawn with is represented by the intervals

\{ \begin{matrix}I_{x} =]2, 3[ \\ I_{y} =]2, +∞[ \end{matrix} and \{ \begin{matrix}I_{x,y} =]0, 1[ \\ I_{y,x} =] − 1, 0[ \end{matrix}

The region drawn with is represented by the following intervals and preorder:

\{ \begin{matrix}I_{x} =]1, 2[ \\ I_{y} =]1, 0[ \end{matrix} and ≺ is defined byy ≺ x

0 1 2 3  x 12y

4frac(γ) denotes the fractional part of γ

The difference with traditional sets of regions [AD90, AD94] is that we allow some diagonal constraints in the non-bounded regions.

We can note that every convex union of regions of R_{α} is a zone. The set of such convex unions of regions of R_{α} is denoted by Z_{α}. If Z is a zone, we define Approx_{α}(Z) the smallest zone of Z_{α} that contains Z (this zone is welldefined because there are finitely many zones in Z_{α}, thus it can be argued as in section 2.3.1 for the k-approximation that this smallest zone exists). We say that Approx_{α}(Z) is the α-overapproximation of Z. We can note that the k-overapproximation of a zone defined in Section 2.3.1 corresponds to the α-overapproximation when α = ((k, …, k), (k, …, k)).

A set of regions α = ((max_{x}))_{x∈X}; (max_{x,y})_{x,y∈X}) is called diagonal-free if for all clocks x, y ∈ X, max_{x,y} = −∞. In this case we simply write α = (max_{x})_{x∈X}.

Example 6 We define α as the (diagonal-free) tuple (max_{x}, max_{y}) defined by:

max_{x} = 3, max_{y} = 2

The set of regions R_{α} is represented on the figure

beside. 0 1 2 3  x 12y

4.2.2 Precise Decidability Results.

In Section 4.1.3, we presented roughly the decidability results we obtained in [BDFP00a]. We will now make these results more precise. We distinguish two different cases, the updatable timed automata with diagonal-free clock constraints and the updatable timed automata with general clock constraints.

Diagonal-free updatable timed automata. Let C ⊆ C_{df}(X) be a set of diagonal-

free clock constraints and let U ⊆ U(X) be a set of updates such that

up = ⋀_{x∈X} up_{x} ∈ U ⟺ for each x, up_{x} ∈ {det_{x}, inf_{x}, sup_{x}, int_{x}} where:

det_{x} ::= x := c | x := z + d with c ∈ ℕ, d ∈ ℤ and z ∈ X inf_{x} ::= x :◁ c | x :< z + d | inf_{x} ∧ inf_{x}

with ◁∈ {<, ≤}, c ∈ ℕ, d ∈ ℤ and z ∈ X

sup_{x} ::= x :▷ c | x :> z + d | sup_{x} ∧ sup_{x}

with ▷∈ {>, ≥}, c ∈ ℕ, d ∈ ℤ and z ∈ X

int_{x} ::= x :∈ (c; d) | x :∈ (c; z + d) | x :∈ (z + c; d) | x :∈ (z + c; z + d) where ( and ) are either [ or ], z is a clock and c, d are in ℤ.

If the system of linear Diophantine inequations over the variables (max_{x})_{x∈X}

{c ≤ max_{x} | x ∼ c ∈ C or x :∼ c ∈ U}

∪ {max_{z} ≤ max_{y} + c | z :∼ y + c ∈ U} (1)

has a solution, then the class Aut(C, U) is decidable. Moreover, if α = (max_{x})_{x∈X} is a solution of this system, then we can test for emptiness of any updatable timed automaton from Aut(C, U) using the region automaton based on the diagonal-free set of regions R_{α}. Of course, this condition is not necessary, it can be the case that this system does not have a solution, but that its emptyness can however be decided, for example when clocks are bounded, but updates which are used lead to systems which dont’t have any solution.

Remark 1 The system of equations (1) has been set in order for a solution α to define a set of regions R_{α} such that the region automaton using R_{α} as set of regions is bisimilar to the original updatable timed automaton. All the conditions described by (1) aim at ensuring this property. See [BDFP00a] for detailed explanations on how these conditions ensure the bisimulation property.

General updatable timed automata. Let C ⊆ C(X) be a finite set of clock constraints and U ⊆ U(X) be a finite set of updates such that

up = ⋀_{x∈X} up_{x} ∈ U ⟺ ∀x ∈ X, up_{x} ∈ \begin{matrix}\{x := c, x :< c, x :≤ c | c ∈ ℕ\} \\ ∪ \{x := y | y ∈ X\}. \end{matrix}

Then the class Aut(C, U) is decidable. Moreover, if the tuple α = ((max_{x})_{x∈X}; (max_{x,y})_{x,y∈X}) is a solution of the following linear Diophantine inequation system:

{c ≤ max_{x} | x ∼ c ∈ C} ∪ {c ≤ max_{x,y} | x − y ∼ c ∈ C} ∪ {c ≤ max_{x}, max_{z} ≥ c + max_{z,x} | x :< c or x :≤ c or x := c ∈ U, and z ∈ X} ∪ {max_{x} ≤ max_{y}, max_{z,y} ≥ max_{z,x}, max_{x,z} ≤ max_{x,y} | x := y ∈ U and z ∈ X}

(2)

then we can test for emptiness of every updatable timed automaton from Aut(C, U) using the region automaton based on the set of regions R_{α}.

Remark 2 Considering a classical timed automaton A and defining the constant k as the largest constant appearing in A, the set of regions α = ((k, …, k), (k, …, k)) is a solution to the system which is associated to A as above.

Remark 3 In both cases (diagonal-free and general frameworks), the set of solutions of the linear system corresponding to an updatable timed automaton might have several solutions. However, if there is a solution, then there is a unique minimal solution (for the natural order on the tuples): indeed, all the inequations are of one of the forms

X ≥ c, X − Y ≥ c

where X and Y are variables and c is a constant. Thus, if we denote by (X_{i})_{i=1...n} all the variables involved in the system, it can be represented by a DBM M and the unique minimal solution is the offset-point of the zone represented by M, that is the point with minimal coordinates belonging to the zone represented by M.

Example 7 Consider the following updatable timed automaton:

a, y := 0 b, y := 1 x − y < 1, c

The system of inequations associated with this automaton is the following:

max_{y} ≥ 0
max_{x} ≥ 0 + max_{x,y}
max_{y} ≥ 1
max_{x} ≥ 1 + max_{x,y}
max_{x,y} ≥ 1

The minimal solution α of this system is:

\{ \begin{matrix}max_{x} = 2 \\ max_{y} = 1 \\ max_{x,y} = 1 \end{matrix}

The set of regions defined by these constants is thus presented with plain lines on the figure beside.

1 2  x 1y0

In what follows we will only consider decidable updatable timed automata, that is updatable timed automata that belong to some decidable class Aut(C, U). We will associate with each decidable updatable timed automaton a set of regions, R_{α} as described above, where α is the minimal solution of the previous system (the smallest is the solution, the smallest is the number of regions of R_{α} and the more abstract is the region automaton).

4.3 A First Correct Algorithm for Decidable Updatable Timed Automata

For each zone Z, for each tuple α, we define the closure by regions from R_{α} of Z by

Closure_{α}(Z) = ⋃ {R ∈ R_{α} | R ∩ Z ≠ ∅}.

We say that Closure_{α}(Z) is the α-closure of Z. First note that Closure_{α}(Z) can be different from Approx_{α}(Z): Approx_{α}(Z) is convex whereas Closure_{α}(Z) can be non-convex. Example 8 Let us consider the set of regions defined as on the picture beside. If we consider the zone Z drawn using

then the closure by region Closure_{α}(Z) is drawn adding the part : it is thus non convex. The α-approximation Approx_{α}(Z) is obtained by adding the part in .

The first algorithm is presented as Algorithm 2.

Algorithm 2 A First Algorithm for Decidable Updatable Timed Automata # First UTA-Algorithm (A:UTA) { # Compute α using U and C; # Visited := ∅; (* Visited stores the visited states *) # Waiting := {(q_{0},Closure_{α}(Z_{0}))}; # Repeat # Get and Remove (q,Z) from Waiting; # If q is final # then {Return “Yes”;} # else {If there is no (q,Z’) ∈ Visited such that Z ⊆ Z’ # then {Visited := Visited ∪ {(q,Z)}; # Successor := {(q’,Closure_{α}(Post(Z,e))) | # e transition from q to q’}; # Waiting := Waiting ∪ Successor;}} # Until (Waiting = ∅); # Return “No”; }

This algorithm of course terminates (if α is fixed, when Z varies, there are finitely many different Closure_{α}(Z)). We will prove the correctness of this algorithm.

Let U be a set of updates and C a set of clock constraints. Let α be the tuple defining the set of regions R_{α} as in Section 4.2. It implies in particular (see [BDFP00a]) that for each clock constraint g ∈ C, for each update up ∈ U, for each region R ∈ R_{α}, for each valuation v ∈ R:

\{ \begin{matrix}R ⊆ g or R ⊆ ¬g \\ up(v) ∩ R ≠ ∅ ⟹ ∀v′ ∈ [v]_{α}, up(v′) ∩ R ≠ ∅ \end{matrix}  (3)

This ensures that the emptiness problem is decidable for the class Aut(C, U) (see [BDFP00a]).

Proposition 1 The “First UTA-Algorithm” tests for emptiness of every decidable updatable timed automaton.

The proof of this proposition is proved using several intermediary results. We first claim that:

Lemma 1 The two following conditions hold:

\{ \begin{matrix}Closure_{α}(g) = g & for each clock constraintg in C \\ up(Closure_{α}(Z)) ⊆ Closure_{α}(up(Z)) & for each zoneZ and for each updateup in U \end{matrix}

(4)

See the proof in Appendix.

We also claim that:

Lemma 2 For each zone Z, \overrightarrow{Closure_{α}(Z)} ⊆ Closure_{α}(\overrightarrow{Z}) and for each clock constraint g such that Closure_{α}(g) = g, g ∩ Closure_{α}(Z) ⊆ Closure_{α}(g ∩ Z).

See the proof in Appendix.

Using these two lemmas, we are now ready to prove the proposition. Using the conditions (4), if e = (q, g, a, up, q′) is a transition, we compute:

Post(Closure_{α}(Z), e) = up(g ∩ \overrightarrow{Closure_{α}(Z)})
⊆ up(g ∩ Closure_{α}(\overrightarrow{Z})) from Lemma 2
⊆ up(Closure_{α}(g ∩ \overrightarrow{Z})) from Lemma 2
⊆ Closure_{α}(up(g ∩ \overrightarrow{Z})) from condition (4)
⊆ Closure_{α}(Post(Z, e))

In particular, whenever Post(Z, e) is empty, Post(Closure_{α}(Z), e) is empty (because Closure_{α}(Z) is empty if and only if Z is empty).

In fact, the “First UTA-Algorithm” computes for some consecutive transitions (e_{i})_{i=1...p}, the zone

Closure_{α}(Post(Closure_{α}(Post(Closure_{α}(Post(…, e_{p−2})), e_{p−1})), e_{p})).

Using iteratively the above relation and the fact that Closure_{α} is involutive, we get that:

Closure_{α}(Post(Closure_{α}(Post(…, e_{p−1})), e_{p})) ⊆ Closure_{α}(Post(Post(…, e_{p−1}), e_{p}))

Thus, we get, if R(⟨q_{0}, Z_{0}⟩) and MUA(⟨q_{0}, Z_{0}⟩) denote respectively the exact set of reachable states and the set of states computed by the “First UTA-Algorithm”,

R(⟨q_{0}, Z_{0}⟩) ⊆ MUA(⟨q_{0}, Z_{0}⟩) ⊆ Closure_{α}(R(⟨q_{0}, Z_{0}⟩))

Thus, MUA(⟨q_{0}, Z_{0}⟩) = ∅ ⟺ R(⟨q_{0}, Z_{0}⟩) = ∅, and this concludes the proof of the theorem. □

Hence, for each decidable updatable timed automaton A, we can test for emptiness of L(A) using Algorithm 2. However, this algorithm can not be implemented easily, but its correctness is fundamental for proving the correctness of other algorithms.

5 Where We Focus on Correctness

We will now extend Algorithm 1 to (decidable) updatable timed automata and study precisely the correctness of this algorithm. We know that a correct widening operator can not be found for every automaton, but we will enlighten what are exactly the problems and bring out subclasses for which such an algorithm can be used.

5.1 The Natural Extension of Algorithm 1 for Decidable Updatable Timed Automata

In this section, we present a forward analysis algorithm for updatable timed automata. This algorithm is parameterized by a function f, which associates to each automaton a set of regions. From this set of regions will depend the widening operator which is used in the algorithm. Of course, we will focus on the class of decidable updatable timed automata, and we want to bring out subclasses of this model for which we can find a function f which leads to a correct algorithm. Our algorithm is then described by Algorithm 3.

Algorithm 3 Algorithm for Updatable Timed Automata # UTA-Algorithm [f] (A:UTA) { # Define β as f(A); # Visited := ∅; (* Visited stores the visited states *) # Waiting := {(q_{0},Approx_{β}(Z_{0}))}; # Repeat # Get and Remove (q,Z) from Waiting; # If q is final # then {Return “Yes”;} # else {If there is no (q,Z’) ∈ Visited such that Z ⊆ Z’ # then {Visited := Visited ∪ {(q,Z)}; # Successor := {(q’,Approx_{β}(Post(Z,e))) | # e transition from q to q’}; # Waiting := Waiting ∪ Successor;}} # Until (Waiting = ∅); # Return “No”; }

Considering classical timed automata and defining the function f as the one which associates to every classical timed automaton A the tuple ((k, …, k), (k, …, k)) where k is the maximum constant appearing in A, Algorithm 3 parametrized by f corresponds to Algorithm 1. As Algorithm 1, Algorithm 3 terminates because there are finitely many overapproximations of zones that can be associated with each control state. From the counterexample of section 3, we know that it is hopeless to find a parameter function f such that for every decidable updatable timed automaton, Algorithm 3 is correct, but our aim is to distinguish classes together with appropriate parameters such that it is the case.

We will first study in details the (partial) correctness of Algorithm 3, and we will then present how the DBM data structure can be used in order to implement Algorithm 3 when this last one is correct.

5.2 Partial Correctness

As we have seen in section 3, Algorithm 3 is not correct in general. However, we will propose some subclasses for which it is correct. We will write the proofs very carefully and with details because, as it will appear, some properties of zones and DBMs are not intuitive at all, and, in the past, mistakes have been done (see section 3), maybe because of this bad intuition we have about zones. We will thus explain where the problems exactly come from.

As we proved that Algorithm 2 is correct with respect to reachability, to prove that Algorithm 3 (parameterized by a function f) is correct for a subclass of timed automata, it is sufficient to prove the following: given a timed automaton A of this class, α associated to A as in section 4.2 and β = f(A), then for every “computed zone”^{5},

Z  ⊆ Approx_{β}(Z) ⊆ Closure_{α}(Z)
↑  ↑  ↑
Exact set  Algorithm 3  Algorithm 2

(5)

because, if it is the case, it means that the approximation Approx_{β} used in Algorithm 3 is coarser than the closure by region Closure_{α} used in Algorithm 2. Thus, as Algorithm 2 is correct with respect to reachability, Algorithm 3 will also be correct for the corresponding class of automata.

5.2.1 Diagonal-Free Updatable Timed Automata.

Let A be a diagonal-free decidable updatable timed automaton. As described in Section 4.2, we associate with A a diagonal-free set of regions R_{α} where α = (max_{x})_{x∈X}. We then define a second set of regions, R_{β} where β is the tuple ((Max_{x})_{x∈X}; (Max_{x,y})_{x,y∈X}) with Max_{x,y} = Max_{x} = max_{x} for every clocks x, y ∈ X.

Example 9 The sets of regions R_{α} and R_{β} can be both represented (in a two-dimensional timespace) as on the figure beside, where α is drawn with solid lines whereas the refinement β also uses dashed lines (R_{β} refines R_{α}).

0 1 2 3  x 12y

If α and β are defined as above, we have the following property:

Proposition 2 For each zone Z, the following holds:

Z ⊆ Approx_{β}(Z) ⊆ Closure_{α}(Z).

Proof It is equivalent to prove that for every zone Z, for every region R of R_{α},

R ∩ Z = ∅ ⟹ R ∩ Approx_{β}(Z) = ∅

Let R = ((I_{x_{i}})_{x_{i}∈X}; ≺) be a region of R_{α} and let M_{R} = ((r_{i,j}; ≺_{i,j})_{i,j=0...n}) be the DBM representing R such that:

5We will make the notion of “computed zone” more precise after.

(r_{i,0}; ≺_{i,0}) = \{ \begin{matrix}(c + 1; <) & if I_{x_{i}} =]c; c + 1[ \\ (c; ≤) & if I_{x_{i}} = \{c\} \\ (+∞; <) & if I_{x_{i}} =]max_{x_{i}}; +∞[ \end{matrix}

(r_{0,i}; ≺_{0,i}) = \{ \begin{matrix}(−c; <) & if I_{x_{i}} =]c; c + 1[ \\ (−c; ≤) & if I_{x_{i}} = \{c\} \\ (−max_{x_{i}}; <) & if I_{x_{i}} =]max_{x_{i}}; +∞[ \end{matrix}

(r_{i,j}; ≺_{i,j}) = \{ \begin{matrix}(c − d + 1; <) & if I_{x_{i}} =]c; c + 1[, I_{x_{j}} =]d; d + 1[ \\ & and x_{j} ≺ x_{i}, x_{i} ⊀ x_{j} \\ (c − d; <) & if I_{x_{i}} =]c; c + 1[, I_{x_{j}} =]d; d + 1[ \\ & and x_{i} ≺ x_{j}, x_{j} ⊀ x_{i} \\ (c − d; ≤) & if I_{x_{i}} =]c; c + 1[, I_{x_{j}} =]d; d + 1[ \\ & and x_{i} ≺ x_{j}, x_{j} ≺ x_{i} \\ (+∞; <) & in all other cases \end{matrix}

Note that the diagonal-free hypothesis on R_{α} has the important consequence that if (r_{i,0}; ≺_{i,0}) = (+∞; <), then for every j ≠ 0, (r_{i,j}; ≺_{i,j}) = (r_{j,i}; ≺_{j,i}) = (+∞; <). That’s this property which will be the central point of the proof.

Let Z be a zone and M = ((m_{i,j}; <_{i,j})_{i,j}) a DBM in normal form that represents Z. Assume that Z ∩ R = ∅. It means that there exists a sequence of distinct indices (i_{1}, i_{2}, …, i_{l} = i_{1}) such that

α_{i_{1},i_{2}} + α_{i_{2},i_{3}} + ⋯ + α_{i_{l−1},i_{l}} < (0; ≤)  (6)

where α_{i_{j},i_{k}} = min((m_{i_{j},i_{k}}; <_{i_{j},i_{k}}); (r_{i_{j},i_{k}}; ≺_{i_{j},i_{k}})). As M is in normal form, we can assume that two successive α_{h,ℓ} does not come from M, otherwise, we can simplify the sum (6). Note that if (m_{i_{j},i_{k}}; <_{i_{j},i_{k}}) < (r_{i_{j},i_{k}}; ≺_{i_{j},i_{k}}) and if I_{x_{i}} and I_{x_{j}} are both bounded, then we can distinguish two cases:

• \underline{First case:} (r_{i_{j},i_{k}}; ≺_{i_{j},i_{k}}) = (r_{i_{j},i_{k}}; ≤) = (−r_{i_{k},i_{j}}; ≤) = (−r_{i_{k},i_{j}}; ≺_{i_{k},i_{j}}).

In this case, (m_{i_{j},i_{k}}; <_{i_{j},i_{k}}) < (−r_{i_{k},i_{j}}; ≺_{i_{k},i_{j}}), thus

(m_{i_{j},i_{k}}; <_{i_{j},i_{k}}) + (r_{i_{k},i_{j}}; ≺_{i_{k},i_{j}}) < (0; ≤)

Thus, Z ⊆ (x_{i_{j}} −x_{i_{k}} < −r_{i_{k},i_{j}}) and R∩(x_{i_{j}} −x_{i_{k}} < −r_{i_{k},i_{j}}) ≠ ∅. Thus, we get that Approx_{β}(Z) ⊆ (x_{i_{j}} − x_{i_{k}} < −r_{i_{k},i_{j}}) and then that Approx_{β}(Z) ∩ R = ∅. Note that, obviously, the zone defined by (x_{i_{j}} − x_{i_{k}} < −r_{i_{k},i_{j}}) is β-bounded because R_{β} refines R_{α}.

• \underline{Second case:} (r_{i_{j},i_{k}}; ≺_{i_{j},i_{k}}) = (c; <) and (r_{i_{k},i_{j}}; ≺_{i_{k},i_{j}}) = (−c + 1; <).

In this case, (m_{i_{j},i_{k}}; <_{i_{j},i_{k}}) ≤ (c − 1; <). Thus, as previously, we obtain that Approx_{β}(Z) ∩ R = ∅.

Let us assume now that we are not in one of the two previous cases. Thus, if (m_{i_{j},i_{j+1}}; <_{i_{j},i_{j+1}}) < (r_{i_{j},i_{j+1}}; ≺_{i_{j},i_{j+1}}), it means that either I_{x_{i_{j}}} = ] max_{x_{i_{j}}}; +∞[ or I_{x_{i_{j+1}}} =] max_{x_{i_{j+1}}} ; +∞[. If I_{x_{i_{j}}} =] max_{x_{i_{j}}}; +∞[, from the construction of M_{R}, we get that i_{j−1} = 0, because if i_{j−1} ≠ 0, then (r_{i_{j−1},i_{j}}; ≺_{i_{j−1},i_{j}}) = (+∞; <). If I_{x_{i_{j+1}}} =] max_{x_{i_{j+1}}} ; +∞[, we get that it is not possible, because every coefficient r_{i_{j+1},∗} is infinite. After this analysis, we get that in the sum (6), we can not have two coefficients coming from M. Thus, as R is not empty, we have exactly one coefficient coming from M in the sum (6). Collecting all these informations, we get that there exists a sequence of indices (k_{1}, …, k_{p}) such that

(r_{0,k_{1}}; ≺_{0,k_{1}}) + (m_{k_{1},k_{2}}; <_{k_{1},k_{2}}) + (r_{k_{2},k_{3}}; ≺_{k_{2},k_{3}}) + ⋯ + (r_{k_{p},0}; ≺_{k_{p},0}) < (0; ≤)

Now, by computing the normal form of M_{R}, the only coefficients of M_{R} that can be tightened are the (r_{x,y}; ≺_{x,y}) where r_{x,0} is bounded. Thus, we can simplify the previous sum and get that

(r_{0,k_{1}}; ≺_{0,k_{1}}) + (m_{k_{1},k_{2}}; <_{k_{1},k_{2}}) + (r_{k_{2},0}; ≺_{k_{2},0}) < (0; ≤)

Setting (c; ≺) = (r_{k_{2},0}; ≺_{k_{2},0}) + (r_{0,k_{1}}; ≺_{0,k_{1}}), we get that

\{ \begin{matrix}Z ⊆ (x_{k_{1}} − x_{k_{2}} ≺ −c) \\ R ∩ (x_{k_{1}} − x_{k_{2}} ≺ −c) = ∅ \end{matrix}

Thus, as

−Max_{x_{k_{1}},x_{k_{2}}} = −max_{x_{k_{1}}} ≤ c ≤ max_{x_{k_{2}}} = Max_{x_{k_{2}},x_{k_{1}}}

the zone (x_{k_{1}} − x_{k_{2}} ≺ −c) is β-bounded. As previously, we conclude that Approx_{β}(Z) ⊆ (x_{k_{1}} − x_{k_{2}} ≺ −c) and thus that R ∩ Approx_{β}(Z) = ∅. □

Remark 4 We can note that if we consider Approx_{α} instead of Approx_{β}, the previous property does not hold anymore. See for example the figure below.

zone Z

Approx^{β}(Z) \ Z

Approx^{α}(Z) \ Approx^{β}(Z)

Using what we said before, we get the following theorem:

Theorem 2 Algorithm 3 is correct (with respect to reachability) for decidable diagonal-free updatable timed automata (taking as parameter the function defined just before the previous proof).

This theorem, even if it is not as general as we could expect, is already interesting because in many practical cases, the automata built for real systems are diagonal-free (see as examples [HSLL97] or [BBP02]).

5.2.2 General Updatable Timed Automata.

From the counter-example of section 3, it is hopeless to prove the correctness of Algorithm 3 in the general case. However, we will bring out a subclass of the general updatable timed automata for which we can find a parameter function f such that Algorithm 3 is correct. So, let us take a decidable updatable timed automaton A and let us consider the set of regions R_{α} defined as in section 4.2 where α = ((max_{x})_{x∈X}; (max_{x,y})_{x,y∈X}). The parameter function f associates with A the tuple β = ((Max_{x})_{x∈X}; (Max_{x,y})_{x,y∈X}) where Max_{x} = Max_{x,y} = ∑_{z∈X} max_{z} for every clocks x, y ∈ X. Roughly, the constant ∑_{z∈X} max_{z} is the maximum constant that can appear in a DBM in normal form that represents a region of R_{α}.

Theorem 3 Algorithm 3 is correct (with respect to reachability) for decidable general updatable timed automata that use less than three clocks (the parameter is the one defined just above).

This theorem is not in contradiction with what we announced in section 3. Indeed, the counter-example of figure 1 uses four clocks. The limit between correctness and non-correctness locates thus precisely between three and four clocks. Proof The property (5) is equivalent to proving that for every region R of R_{α}, for every “computed” zone Z, if R ∩ Z = ∅ then R ∩ Approx_{β}(Z) = ∅. Let A be a decidable general updatable timed automaton with less than three clocks, as defined in section 4.2. We will prove that, for each “computed” zone Z, the following holds: for each region R of R_{α}, whenever

R ∩ Z = ∅

implies that there exists a β-bounded zone V such that

\{ \begin{matrix}Z ⊆ V \\ R ∩ V = ∅ \end{matrix}  (7)

This property will imply what we want because Approx_{β}(Z) is the smallest β-bounded zone that contains the zone Z. Assume that a zone Z verifies the condition (7) and suppose we are given a clock constraint g and an update up of the automaton A. We will prove that up(g ∩ \overrightarrow{Z}) also verifies the condition (7). Having proved that, we will deduce that if Z is one of the zones which are computed by the algorithm and if R is any region of R_{α}, if Z ∩ R = ∅, then Approx_{β}(Z) ∩ R = ∅ because Approx_{β}(Z) is the smallest β-bounded zone containing Z.

Computing the future. Assume that R ∩ \overrightarrow{Z} = ∅. It means that \overleftarrow{R} ∩ Z = ∅ where \overleftarrow{R} is the past of R, that is \overleftarrow{R} = \{v | ∃t. v + t ∈ R\}. Moreover, using the bisimulation property of the set of regions R_{α} (see remark 1, page 19), \overleftarrow{R} is a union of regions ⋃_{i} R_{i}. For each i, we can find a β-bounded zone V_{i} such that

\{ \begin{matrix}Z ⊆ V_{i} \\ R_{i} ∩ V_{i} = ∅ \end{matrix}

We then define V = ⋂_{i} V_{i}. It verifies that

\{ \begin{matrix}Z ⊆ V \\ \overleftarrow{R} ∩ V = ∅ \end{matrix}

Let us prove that we can eliminate all the constraints of V which are of the form “x bounded by c”. Let M_{R} = ((r_{i,j}); ≺_{i,j})_{i,j}) be a DBM for \overleftarrow{R} such that for each i, (m_{0,i}; ≺_{0,i}) is (0; ≤) (see [Ben02], part A). Moreover, assume that V can be rewritten as a DBM ((v_{i,j}; <_{i,j})_{i,j}). As \overleftarrow{R} ∩ V = ∅, if we assume that a constraint “x bounded by c” is needed in V, it means that there exists (i_{1}, i_{2}, …, i_{p} = 0, i_{p+1}, … i_{l} = i_{1}) such that

α_{i_{1},i_{2}} + ⋯ + α_{i_{p−2},i_{p−1}} + (v_{i_{p−1},0}; <_{i_{p−1},0}) + α_{0,i_{p+1}} + ⋯ + α_{i_{l−1},i_{l}} < (0; ≤) (8)

where α_{k,h} = min((r_{k,h}; ≺_{k,h}); (v_{k,h}; <_{k,h})). In particular,

α_{0,i_{p+1}} = min((r_{0,i_{p+1}}; ≺_{0,i_{p+1}}); (v_{0,i_{p+1}}; <_{0,i_{p+1}})) = (v_{0,i_{p+1}}; <_{0,i_{p+1}})

because (r_{0,i_{p+1}}; ≺_{0,i_{p+1}}) = (0; ≤). Thus, the sum (v_{i_{p−1},0}; <_{i_{p−1},0} ) + (v_{0,i_{p+1}}; <_{0,i_{p+1}}) in (8) can be safely replaced by a constraint (v′_{i_{p−1},i_{p+1}}; <′_{i_{p−1},i_{p+1}}) = (v_{i_{p−1},0}; <_{i_{p−1},0}) + (v_{0,i_{p+1}}; <_{0,i_{p+1}}). We thus define the zone

V′ = ⋀{x_{i} − x_{j} <_{i,j} v_{i,j} ∈ V | j ≠ 0} ∧ (x_{i_{p−1}} − x_{i_{p+1}} <′_{i_{p−1},i_{p+1}} v′_{i_{p−1},i_{p+1}})

which is a β-bounded zone. We get thus that

\{ \begin{matrix}\overrightarrow{Z} ⊆ V′ \\ R ∩ V′ = ∅ \end{matrix}

Intersection with a clock constraint. Assume that g is a clock constraint and that R ∩ (g ∩ Z) = ∅. We distinguish two cases: \underline{First case:} R ∩ g = ∅, by definition of the regions, there exists a constraint x − y ≺ c (constraint “defining α”) such that g ⊆ (x − y ≺ c) and R ∩ (x − y ≺ c) = ∅. Thus, we get that g ∩ Z ⊆ (x − y ≺ c) and R ∩ (x − y ≺ c) = ∅. Note that as x − y = c is a constraint defining the set of region R_{α}, (x − y ≺ c) is a β-bounded zone. \underline{Second case:} R ⊆ g. It thus means that R ∩ Z = ∅, and we can use the induction hypothesis to prove that there exists a β-bounded zone V such that Z ⊆ V and R ∩ V = ∅. In particular, Z ∩ g ⊆ V and R ∩ V = ∅.

Computing the image by an update. Let up be an update such as the ones of Section 4.2 (general case). It can be written as

up = ⋀_{x∈Y} (x := y_{x}) ∧ ⋀_{x∈X\Y} (x :∼ c_{x}).

Then the image of a zone by up can be computed by first applying the update ⋀_{x∈Y} (x := y_{x}) (which is equivalent to the update ⋀_{x∈Y} (x := y_{x}) ∧ ⋀_{x∈X\Y} (x := x)) and then applying successively each update x :∼ c_{x} (for x ∈ X \ Y).

First assume that up is ⋀_{x∈X}(x := y_{x}) and that R ∩ up(Z) = ∅. First of all, if y_{x_{1}} = y_{x_{2}}, then up(Z) is included in the zone (x_{1} = x_{2}). If for one of such pairs, R ∩ (x_{1} = x_{2}) = ∅, then up(Z) ⊆ (x_{1} = x_{2}) and (x_{1} = x_{2}) is β-bounded. We thus assume that it is not the case. Thus, the set E = {R_{i} ∈ R_{α} | up(R_{i}) ⊆ R} is not empty and we have moreover that {v | up(v) ∈ R} = ⋃_{R_{i}∈E} R_{i} (because of the bisimulation property of the set of regions R_{α}, see remark 1 page 19). For each i, R_{i} ∩ Z = ∅, thus there exists a β-bounded zone V_{i} such that Z ⊆ V_{i} and V_{i} ∩ R_{i} = ∅. We distinguish two cases (we have only three clocks, say {x_{1}, x_{2}, x_{3}}):

• \underline{First case:} X = \{y_{x_{1}}, y_{x_{2}}, y_{x_{3}}\}. We define

V = ⋀_{i}{x_{i} − x_{j} ≺ m | y_{x_{i}} − y_{x_{j}} ≺ m ∈ V_{i}}

We have that up(Z) ⊆ V and that R ∩ V = ∅, because if v ∈ R ∩ V, then we can define safely v′ such that v′(y_{x_{i}}) = v(x_{i}) for each i = 1, 2, 3 and v′ will be in ⋂_{i} V_{i}, which is not possible because v = up(v′) and thus v′ would be in one of the R_{i}’s.

• \underline{Second case:} Y = \{y_{x_{1}}, y_{x_{2}}, y_{x_{3}}\} ≠ X. We define R′ = R∩⋂_{y_{x_{i}}=y_{x_{j}}} (x_{i} = x_{j}). We have thus that Z ∩ R′ = ∅. The zones Z and R′ can now be considered as one or two-dimensional zones (depending on the cardinality of Y). For concluding, we will apply the following (obvious) claim to the zones Z and R′: Claim Let Z_{1} and Z_{2} be one or two-dimensional zones such that Z_{1} ∩ Z_{2} = ∅. Assume that M_{1} = ((m_{i,j}; ≺_{i,j})) is a DBM in normal form defining Z_{1}, then there exists i and j such that Z_{2} ⊆ ¬(x_{i} − x_{j} ≺_{i,j} m_{i,j}). Note that one of the indices i or j may be 0. There exists thus a constraint x_{i} −x_{j} ≺ c that is a constraint defining the normal form of R′ and such that Z ⊆ ¬(x_{i} − x_{j} ≺ c). Of course, from the definition of β, we get that the zone (x_{i} − x_{j} ≺ c) is β-bounded, and defining

V = ¬(x_{i} − x_{j} ≺ c) ∧ ⋀_{y_{x_{k}} =y_{x_{l}}}(x_{k} = x_{l})

we get that up(Z) ⊆ V and R ∩ V = ∅.

Assume that up is x_{k} :≺ c and that

R ∩ up(Z) = ∅

We have that up(Z) is included in x_{k} ≺ c, thus, if R is not included in x_{k} ≺ c, we have finished because (x_{k} ≺ c) is a β-bounded zone. Assume now that R ⊆ (x_{k} ≺ c). We define Free_{x_{k}}(R) as the set {v | ∃v′ ∈ R s.t. ∀x ∈ X \ {x_{k}}, v(x) = v′(x)}. In the same way, we define Free_{x_{k}}(Z). By construction of the set of regions R_{α} (because of the bisimulation property...), Free_{x_{k}}(R) is a union of regions and for each v in Free_{x_{k}}(R), there exists v′ ∈ up(v) ∩ R. Thus, it is easy to see that Free_{x_{k}}(R) ∩ Free_{x_{k}}(Z) = ∅. As we only have 3 clocks, Free_{x_{k}}(Z) and Free_{x_{k}}(R) can be considered as two-dimensional zones. Applying the previous claim, there exists a constraint x_{i} − x_{j} ≺ c that does not involve the clock x_{k}, which is a constraint of the normal form of Free_{x_{k}}(R) and such that Free_{x_{k}}(Z) ⊆ ¬(x_{i}−x_{j} ≺ c). The constraint ¬(x_{i}−x_{j} ≺ c) is of course a β-bounded zone (because of the definition of β), up(Z) ⊆ ¬(x_{i} − x_{j} ≺ c) and R ∩ ¬(x_{i} − x_{j} ≺ c) = ∅.

The proof is now finished: we have proved that if Z verifies the property (7), then up(\overrightarrow{Z} ∩ g) verifies also (7). Applying the widening operator Approx_{β} at each step of the computation is thus correct: if R is a region and Z a computed zone, R ∩ Z = ∅ implies that R ∩ Approx_{β}(Z) = ∅. □

Remark 5 In the previous proof, the hypothesis on the small number of clocks is used. Indeed, updating a clock is “equivalent” to projecting on a smaller dimension, and when we only have three clocks, the projection is one or twodimensional and has thus nice properties. An error which maybe explains the numerous mistakes done in the literature is that zones in big dimensions are not similar to what we can “see” in two dimensions, thus it is not correct to project and to visualize what happens in two dimensions. In the previous proof, for the reset, if we want to be general and to reason with n clocks, we get the following: applying the induction hypothesis to the projection of Z and any region “belonging” to Free_{x_{k}}(R) will allow to get a β-bounded zone V which “separates” them (in the sense that Z ⊆ V and Free_{x_{k}}(R) ∩ V = ∅). However, we have no argument to say that this β-bounded zone does not use the clock x_{k}. Thus, from V, it is not possible to compute a β-bounded zone that “separates” up(Z) and R. That’s the reason why the theorem 3 is not true in general.

5.3 Implementation of the Algorithm

From what precedes, we have that, even if it is not correct in general, Algorithm 3 can however be used safely for some subclasses of systems. We will thus show that the DBM data structure is appropriate to implement Algorithm 3: we will show how to compute the new operations on zones appearing in Algorithm 3 using the DBMs. New operations are of two types: image by updates and widening operator Approx_{β}.

Image by updates. Let up be an update and M be a DBM (in normal form). The DBM M represents a clock constraint φ over the set of clocks X. From up, we construct a clock constraint φ_{up} over the set of clocks X ∪ X′ (where X′ is a disjoint copy of X) by induction on up in the following manner:

\{ \begin{matrix}φ_{x:∼c} = x′ ∼ c \\ φ_{x:∼y+c} = x′ ∼ y + c \\ φ_{up_{1}∧up_{2}} = φ_{up_{1}} ∧ φ_{up_{2}}. \end{matrix}

We now define the formula φ′_{up} = φ ∧ φ_{up}. This formula represents the update up in the sense that if V is a valuation for the clocks X ∪ X′, then

V ⊧ φ′_{up} ⟺ V_{|X} ⊧ φ and V_{|X′} ∈ up(V_{|X}).

We assume that up = ⋀_{i=1}^{n} up_{i} where up_{i} updates the clock x_{i}. We define N = (η_{i,j})_{i,j=0...2n} as the DBM of size 2n + 1 (over the set of clocks X ∪ X′) as follows:

• for i, j = 0 … n, η_{i,j} = (m_{i,j}; ≺_{i,j}),

• for each update up_{i} (1 ≤ i ≤ n), we distinguish the different possible values of up_{i}:

if up_{i} is:  then we set:
x_{i} := c  η_{i+n,0} = (c, ≤) and η_{0,i+n} = (−c; ≤)
x_{i} := x_{j} + c  η_{i+n,j} = (c; ≤) and η_{j,i+n} = (−c; ≤)
x_{i} :≺ c with ≺∈ {<; ≤}  η_{i+n,0} = (c; ≺) and η_{0,i+n} = (0; ≤)
x_{i} :≻ c with ≻∈ {>; ≥}  η_{0,i+n} = (−c; ≺)

(where ≺ is < if ≻ is > and ≺ is ≤ if ≻ is ≥)

x_{i} :≺ x_{j} + c with ≺∈ {<; ≤} η_{i+n,j} = (c; ≺) and η_{j,i+n} = (∞; <)
x_{i} :≻ x_{j} + c with ≻∈ {>; ≥}  η_{j,i+n} = (−c; ≺)

(where ≺ is < if ≻ is > and ≺ is ≤ if ≻ is ≥)

If up_{i} is a conjunction of simple updates, we take the smallest constraints,

• for every i, j = 0 … 2n + 1, if η_{i,j} has not been initialized yet , we set η_{i,j} = (+∞; <).

By construction, the DBM N represents the clock constraint φ′_{up} (indices 1 ≤ i ≤ n correspond to the set of clocks X whereas indices n + 1 ≤ i ≤ 2n + 1 correspond to the set of clocks X′):

⟦N⟧ = {V valuation over X ∪ X′ | V ⊧ φ′_{up}}.

We define (ϕ(N))_{|X′} as the square submatrice of size n + 1 of N where we erase everything about the set of clocks X. It can be represented by the picture beside (the white part correspond to the clocks from X). Then we get that:

⟦(ϕ(N))_{|X′}⟧ = up(⟦M⟧).

( ∗ ∗ … ∗ ∗ … ∗ ; ∗ ∗ … ∗ ∗ … ∗ ; ⋮ ; ∗ ∗ … ∗ ∗ … ∗ ; ∗ ∗ … ∗ ∗ … ∗ ; ⋮ ; ∗ ∗ … ∗ ∗ … ∗ )

If we want to compute the image by the update up of a zone Z represented by a DBM M (in normal form), we first compute the DBM N, then its normal form and finally we erase some coefficients and the result of this algorithm gives a DBM (in normal form) that represents up(Z).

β-overapproximation. Let β = ((max_{x})_{x∈X}; (max_{x,y})_{x,y∈X}) defining a set of regions. All the β which are used in one of the correct algorithms described before verifies in addition that for every x, y ∈ X, max_{x,y} = max_{x}, We assume X = {x_{1}, …, x_{n}}. A DBM M = (m_{i,j}; ≺_{i,j})_{i,j} is said β-bounded if:

0 ≤ m_{i,0} ≤ max_{x_{i}} or m_{i,0} = ∞  for every 1 ≤ i ≤ n
−max_{x_{i}} ≤ m_{0,i} ≤ 0  for every 1 ≤ i ≤ n
−max_{x_{j},x_{i}} ≤ m_{i,j} ≤ max_{x_{i},x_{j}} or m_{i,j} = ∞ for every 1 ≤ i, j ≤ n

Lemma 3 Let Z be a zone. Then

Z ∈ Z_{β} ⟺ there exists a β-bounded DBMM_{β} such thatZ = ⟦M_{β}⟧.

See the proof in Appendix.

We consider the following algorithm (we assume M = (m_{i,j}; ≺_{i,j}) and M′ = (m′_{i,j}; ≺′_{i,j})):

# β-Overapproximation Algorithm (M:n-dimensional DBM) # M’ = ϕ(M); (* Normal Form of M *) # for i = 1 to n do # for j = 1 to n do # if (m’_{i,j};≺_{i,j})>(max_{x_{i},x_{j}};≤) then (m’_{i,j};≺_{i,j}) becomes (+∞;<); # if (m’_{i,j};≺_{i,j})<(-max_{x_{j},x_{i}};<) then # (m’_{i,j};≺_{i,j}) becomes (-max_{x_{j},x_{i}};<); # endfor; # if (m’_{i,0};≺_{i,0})>(max_{x_{i}};≤) then (m’_{i,0};≺_{i,0}) becomes (+∞;<); # if (m’_{0,i};≺_{0,i})<(-max_{x_{i}};<) then (m’_{0,i};≺_{0,i}) becomes (-max_{x_{i}},<); # endfor; # Return M’;

If M is a DBM, applying this algorithm to M, we obtain a DBM that we denote by ϕ_{β}(M). We can note that ϕ_{β}(M) is a β-bounded DBM and thus that ⟦ϕ_{β}(M)⟧ is in Z_{β}.

Property 1 If M is a DBM, then it holds that ⟦ϕ_{β}(M)⟧ = Approx_{β}(⟦M⟧).

See the proof in Appendix.

The “β-Overapproximation Algorithm” applied to M computes thus a DBM that represents the β-overapproximation of ⟦M⟧. This DBM might not be in normal form. The complexity of the computation of such a βoverapproximation is not high (it is in O(n^{3}) if n is the number of clocks).

Combining the constructions of section 2.4.1 with what precedes, we get that if e = q ⟶^{g,a,up} q′ is a transition and if M is a DBM representing the zone Z, we can compute a DBM M′ which represents the zone Approx_{β}(up(g ∩ \overrightarrow{Z})) = Approx_{β}(Post(Z, e)) but which might not be in normal form. Normal forms are computed before performing all the operations on DBMs, apart from the intersection for which it is not required, and apart from when we just performed either an image by update or a future operation (after such operations, DBMs are automatically in normal form). Thus, each operation in Algorithm 3 can be computed using the DBM data structure, which is thus appropriate to the implementation of this algorithm. Moreover, the complexity of each step of the algorithm is, as for classical timed automata, polynomial in the number of clocks.

5.4 Discussion

The automata for which we have troubles with the widening operator have diagonal clock constraints (and more than four clocks). We will propose two methods for alleviating this problem. Of course, these solutions will a priori not be as efficient as Algorithm 3.

5.4.1 First Proposition with a Preprocessing Step for Some Timed Automata.

This method does concern the decidable updatable timed automata with general clock constraints and deterministic updates: we allow updates of the form x := y and x := c where x and y are clocks and c is a constant. We know that every (classical) timed automaton with general clock constraints can be transformed into a (classical) diagonal-free timed automaton [BDGP98]. In the same way, every updatable timed automaton that uses only updates of the form x := y and x := c can be transformed into a diagonal-free updatable timed automaton that uses also updates of the form x := y and x := c. This transformation can not be done if we use non-deterministic updates. As we know, this transformation suffers from a combinatorics explosion. However, if the number of diagonal constraints used in the automaton is small, the size of the automaton obtained after this preprocessing step will not be too big. Thus, Algorithm 3 can then be applied to the resulting diagonal-free automaton.

5.4.2 Second Proposition.

The last method we propose can be used for every decidable updatable timed automaton. In practice, it may be expensive, in memory as well as in time.

Let A be an updatable timed automaton. We associate with A the set of regions R_{α} as in section 4.2. We assume that α = ((max_{x})_{x∈X}; (max_{x,y})_{x,y∈X}) and we define the tuple β = ((Max_{x})_{x∈X}; (Max_{x,y})_{x,y∈X}) such that Max_{x} = Max_{x,y} = max_{x} for every x, y ∈ X.

Let R be a region of R_{α} and Z be a zone. We assume that M = ((m_{i,j}; ≺_{i,j} )_{i,j}) is a DBM in normal form for Z and M_{R} = ((r_{i,j}; <_{i,j})_{i,j}) is a DBM that represents R (computed directly from its definition using intervals, like in section 4.2.1, without tightening any constraint). Assume now that Z ∩R = ∅. It means that there exists a sequence of distincts indices (i_{1}, …, i_{l} = i_{1}) such that

α_{i_{1},i_{2}} + ⋯ + α_{i_{l−1},i_{l}} < (0; ≤)  (9)

where α_{h,ℓ} = min((r_{h,ℓ}; ≺_{h,ℓ}); (m_{h,ℓ}; <_{h,ℓ})) and two consecutives α_{h,ℓ} do not belong to M (this is posssible as M is in normal form).

The idea will be then to ensure that there is just one of the coefficient α_{i_{j},i_{j+1}} which comes from the DBM M_{R}. It will be the case whenever we have that, for every pair (i, j) where i.j ≠ 0, there exists an interval I_{i,j} ∈ I_{i,j} where

I_{i,j} = {] − ∞; −max_{x_{j}}[,]max_{x_{i}}; +∞[} ∪ {[c] | −max_{x_{j}} ≤ c ≤ max_{x_{i}}}
∪ {]c; c + 1[ | −max_{x_{j}} ≤ c < max_{x_{i}}}

such that Z ⊆ I_{i,j}. In that case, for every pair (i, j) such that i.j ≠ 0, (m_{i,j}; ≺_{i,j} ) ≤ (r_{i,j}; <_{i,j}). Thus inequality (9) can be transformed into:

α_{i,0} + α_{0,j} + (m_{j,i}; ≺_{j,i}) < (0; ≤)

We can distinguish three cases:

1. α_{i,0} = (m_{i,0}; ≺_{i,0}) and α_{0,j} = (r_{0,j}; <_{0,j}).

In this case, we get that (r_{0,j}; <_{0,j}) + (m_{j,0}; ≺_{j,0}) < (0; ≤). Thus, Z ⊆ ¬(−x_{j} <_{0,j} r_{0,j}) and R ⊆ (−x_{j} <_{0,j} r_{0,j})

2. α_{i,0} = (r_{i,0}; <_{i,0}) and α_{0,j} = (m_{0,j}; ≺_{0,j}).

In this case, we get that (r_{i,0}; <_{i,0}) + (m_{0,i}; ≺_{0,i}) < (0; ≤). Thus, Z ⊆ ¬(x_{i} <_{i,0} r_{i,0}) and R ⊆ (x_{i} <_{i,0} r_{i,0}).

3. α_{i,0} = (r_{i,0}; <_{i,0}) and α_{0,j} = (r_{0,j}; <_{0,j}).

In this case, we get that (r_{i,0}; <_{i,0}) + (r_{0,j}; <_{0,j}) + (m_{j,i}; ≺_{j,i}) < (0; ≤). Thus, Z ⊆ ¬(x_{i} − x_{j} <′ c) and R ⊆ (x_{i} − x_{j} <′ c) where (c; <′) = (r_{i,0}; <_{i,0}) + (r_{0,j}; <_{0,j})

In all the cases, there exists a β-bounded zone V such that

\{ \begin{matrix}Z ⊆ V \\ R ∩ V = ∅ \end{matrix}

The solution we propose is thus to decompose a “computed zone” in the following way:

Z = ⨆ {Z ∩ ⋂_{i,j} I_{i,j} | I_{i,j} ∈ I_{i,j}}

and to compute the image by Approx_{β} of each such sub-zone of Z. Note that an idea of splitting zones was already presented in [Bou00, Ben02], but it was a bit different, and, here, it appears as some kind of “necessary” condition for having a correct algorithm.

A work direction is now to look for more efficient algorithms that test for emptiness timed automata with diagonal clock constraints. Maybe backward analysis algorithms would be more appropriate to this model...

6 Conclusion

In this paper, we studied the widening operator proposed in [DT98] to overcome the non-termination problem of the forward analysis algorithm for timed automata. This operator is very nice in that it can be very easily computed using the standard DBM data structure. However, we have proved in this paper that it is hopeless to look for a correct forward analysis algorithm that uses such an operator: there exist timed automata for which no widening operator is correct. This result is very surprising because several (attempts of) correctness proofs can be found in the literature and the algorithm is implemented and used in model-checking tools like Kronos and Uppaal.

Having stated this result, we took the more general setting of updatable timed automata and brought out subclasses of this model for which we can propose a correct widening operator. Among these subclasses, we can find all the decidable diagonal-free updatable timed automata, and in particular all the classical timed automata which do not use diagonal clock constraints. This class of timed automata is sufficiently large, and that’s maybe the reason why the bug has not been detected before. For the timed automata for which no correct widening operator can be used, other methods are proposed.

This work is also the link that was missing between the theoretical work we did on this updatable timed automata model in [BDFP00a, BDFP00b] (namely decidability and expressiveness) and a tool that would deal with updatable timed automata. If we restrict to diagonal-free systems, updates can be safely added without more difficulty than implementing the image by updates of zones. Considering general updatable timed automata, some problems appear when we want to implement them. However, the problems come from the use of diagonal clock constraints and not from the updates which are used.

Acknowledgments: I would like to thank François Laroussinie for interesting discussions on DBMs, Antoine Petit and Béatrice Bérard for their careful reading of some drafts of this paper and Kim G. Larsen, Emmanuel Fleury and Gerd Behrmann for discussions on the subject during our so-called “Uppaal meetings”. I also want to thank Sergio Yovine as well as anonymous referees for helpful comments about this work.

References

[ACD^{+}92] Rajeev Alur, Costas Courcoubetis, David Dill, Nicolas Halbwachs, and Howard Wong-Toi. Minimization of timed transition systems. In Proc. 3rd International Conference on Concurrency Theory (CON-CUR’92), volume 630 of Lecture Notes in Computer Science, pages 340–354. Springer, 1992.

[ACH94] Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger. The observational power of clocks. In Proc. 5th International Conference on Concurrency Theory (CONCUR’94), volume 836 of Lecture Notes in Computer Science, pages 162–177. Springer, 1994.

[AD90] Rajeev Alur and David Dill. Automata for modeling real-time systems. In Proc. 17th International Colloquium on Automata, Languages and Programming (ICALP’90), volume 443 of Lecture Notes in Computer Science, pages 322–335. Springer, 1990.

[AD94] Rajeev Alur and David Dill. A theory of timed automata. Theoretical Computer Science (TCS), 126(2):183–235, 1994.

[AFH94] Rajeev Alur, Limor Fix, and Thomas A. Henzinger. A determinizable class of timed automata. In Proc. 6th International Conference on Computer Aided Verification (CAV’94), volume 818 of Lecture Notes in Computer Science, pages 1–13. Springer, 1994.

[Alu99] Rajeev Alur. Timed automata. In Proc. 11th International Conference on Computer Aided Verification (CAV’99), volume 1633 of Lecture Notes in Computer Science, pages 8–22. Springer, 1999. Invited talk.

[BBP02] Béatrice Bérard, Patricia Bouyer, and Antoine Petit. Analysing the PGM protocol with uppaal. In Proc. 2nd Workshop on Real-Time Tools (RT-TOOLS’02), 2002. Proc. published as Technical Report 2002-025, Uppsala University, Sweden.

[BDFP00a] Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. Are timed automata updatable? In Proc. 12th International Conference on Computer Aided Verification (CAV’2000), volume 1855 of Lecture Notes in Computer Science, pages 464–479. Springer, 2000.

[BDFP00b] Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. Expressiveness of updatable timed automata. In Proc. 25th International Symposium on Mathematical Foundations of Computer Science (MFCS’2000), volume 1893 of Lecture Notes in Computer Science, pages 232–242. Springer, 2000.

[BDGP98] Béatrice Bérard, Volker Diekert, Paul Gastin, and Antoine Petit. Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae, 36(2–3):145–182, 1998.

[Ben02] Johan Bengtsson. Clocks, DBMs ans States in Timed Systems. PhD thesis, Uppsala University, Uppsala, Sweden, 2002.

[BF99] Béatrice Bérard and Laurent Fribourg. Automated verification of a parametric real-time program: the ABR conformance protocol. In Proc. 11th International Conference on Computer Aided Verification (CAV’99), volume 1633 of Lecture Notes in Computer Science, pages 96–107. Springer, 1999.

[BFH^{+}01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. Minimumcost reachability for priced timed automata. In Proc. 4th International Workshop on Hybrid Systems: Computation and Control (HSCC’01), volume 2034 of Lecture Notes in Computer Science, pages 147–161. Springer, 2001.

[BL96] Johan Bengtsson and Fredrik Larsson. Uppaal, a tool for automatic verification of real-time systems. Master’s thesis, Department of Computer Science, Uppsala University, Sweden, 1996.

[BLP^{+}99] Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. Efficient timed reachability analysis using clock difference diagrams. In Proc. 11th International Conference on Computer Aided Verification (CAV’99), volume 1633 of Lecture Notes in Computer Science, pages 341–353. Springer, 1999.

[Bou00] Patricia Bouyer. A new algorithm to decide emptiness of updatable timed automata. Research Report LSV–00–9, Laboratoire Spécification et Vérification, ENS de Cachan, France, 2000.

[BTY97] Ahmed Bouajjani, Stavros Tripakis, and Sergio Yovine. On-the-fly symbolic model-checking for real-time systems. In Proc. 18th IEEE Real-Time Systems Symposium (RTSS’97), pages 25–35. IEEE Computer Society Press, 1997.

[CG00] Christian Choffrut and Massimiliano Goldwurm. Timed automata with periodic clock constraints. Journal of Automata, Languages and Combinatorics (JALC), 5(4):371–404, 2000.

[CGP99] Edmund Clarke, Orna Grumberg, and Doron Peled. Model-Checking. The MIT Press, Cambridge, Massachusetts, 1999.

[Daw97] Conrado Daws. Analyse par simulation symbolique des systèmes temporisés avec kronos. Research report, Verimag, 1997.

[Dil89] David Dill. Timing assumptions and verification of finite-state concurrent systems. In Proc. of the Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197–212. Springer, 1989.

[DOTY96] Conrado Daws, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. The tool kronos. In Proc. Hybrid Systems III: Verification and Control (1995), volume 1066 of Lecture Notes in Computer Science, pages 208–219. Springer, 1996.

[DT98] Conrado Daws and Stavros Tripakis. Model-checking of real-time reachability properties using abstractions. In Proc. 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), volume 1384 of Lecture Notes in Computer Science, pages 313–329. Springer, 1998.

[DZ98] François Demichelis and Wieslaw Zielonka. Controlled timed automata. In Proc. 9th International Conference on Concurrency Theory (CONCUR’98), volume 1466 of Lecture Notes in Computer Science, pages 455–469. Springer, 1998.

[HHWT97] Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: A model-checker for hybrid systems. Journal on Software Tools for Technology Transfer (STTT), 1(1–2):110–122, 1997.

[HKWT95] Thomas A. Henzinger, Peter W. Kopke, and Howard Wong-Toi. The expressive power of clocks. In Proc. 22nd International Colloquium on Automata, Languages and Programming (ICALP’95), volume 944 of Lecture Notes in Computer Science, pages 417–428. Springer, 1995.

[HRS98] Thomas A. Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. The regular real-time languages. In Proc. 25th International Colloquium on Automata, Languages and Programming (ICALP’98), volume 1443 of Lecture Notes in Computer Science, pages 580–591. Springer, 1998.

[HSLL97] Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund. Formal modeling and analysis of an audio/video protocol: An industrial case study using uppaal. In Proc. 18th IEEE Real-Time Systems Symposium (RTSS’97), pages 2–13. IEEE Computer Society Press, 1997.

[LPY97] Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. Journal of Software Tools for Technology Transfer (STTT), 1(1–2):134–152, 1997.

[MP99] Supratik Mukhopadhyay and Andreas Podelski. Beyond region graphs: Symbolic forward analysis of timed automata. In Proc. 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS’99), volume 1738 of Lecture Notes in Computer Science, pages 232–244. Springer, 1999.

[Tri98] Stavros Tripakis. L’analyse formelle des systèmes temporisés en pratique. PhD thesis, Université Joseph Fourier, Grenoble, France, 1998.

[TY98] Stavros Tripakis and Sergio Yovine. Verification of the fast reservation protocol with delayed transmission using the tool kronos. In Proc. 4th IEEE Real-Time Technology and Applications Symposium (RTAS’98), pages 165–170. IEEE Computer Society Press, 1998.

[TY01] Stavros Tripakis and Sergio Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25–68, 2001.

[Wil94] Thomas Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In Proc. 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’94), volume 863 of Lecture Notes in Computer Science, pages 694–715. Springer, 1994.

[WT94] Howard Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Stanford University, USA, 1994.

[YL97] Mihalis Yannakakis and David Lee. An efficient algorithm for minimizing real-time transition systems. Formal Methods in System Design, 11(2):113–136, 1997.

[Yov98] Sergio Yovine. Model-checking timed automata. In School on Embedded Systems, volume 1494 of Lecture Notes in Computer Science, pages 114–152. Springer, 1998.

[figure]

Appendix: Technical Proofs of this Paper

4.3 A First Correct Algorithm for Decidable Updatable Timed Automata

Lemma 1 The two following conditions hold:

\{ \begin{matrix}Closure_{α}(g) = g & for each clock constraintg in C \\ up(Closure_{α}(Z)) ⊆ Closure_{α}(up(Z)) & for each zoneZ and for each updateup in U \end{matrix}

(4)

Proof Let g be in C. Then Closure_{α}(g) = ⋃{R ∈ R_{α} | R ∩ g ≠ ∅} = g because for each region R ∈ R_{α}, if R ∩ g ≠ ∅ then R ⊆ g. We will now prove the second condition, namely that for each zone Z, for each update up ∈ U,

up(Closure_{α}(Z)) ⊆ Closure_{α}(up(Z))  (5)

Let us take a zone Z. We can write Z as ⋃_{f} Z_{i} where there exists regions R_{i} such that Z_{i} = Z ∩ R_{i} and Z_{i} is not empty. If we prove condition (5) for each zone Z_{i}, then condition (5) will also hold for Z:

up(Closure_{α}(Z)) = up(Closure_{α}(∪_{f}Z_{i}))
= up(∪_{f}Closure_{α}(Z_{i}))
= ∪_{f}up(Closure_{α}(Z_{i}))
⊆ ∪_{f}Closure_{α}(up(Z_{i})) if condition (5) holds for each Z_{i}
⊆ Closure_{α}(∪_{f}up(Z_{i}))
⊆ Closure_{α}(up(∪_{f}Z_{i}))
⊆ Closure_{α}(up(Z))

Thus, we just have to prove the condition (5) for zones included in a region (defined by α). Let Z be a zone included in a region. We want to prove that

up(Closure_{α}(Z)) ⊆ Closure_{α}(up(Z))

Thus, let us assume that there exists a valuation v′ ∈ up(Closure_{α}(Z)) \ Closure_{α}(up(Z)). There exists v ∈ Closure_{α}(Z) such that v′ ∈ up(v). Thus, we obtain that up(v) ∩ [v′]_{α} ≠ ∅. Let v_{0} be in Z, then [v]_{α} = [v_{0}]_{α} and thus, by hypothesis, up(v_{0}) ∩ [v′]_{α} ≠ ∅ and thus [v′]_{α} ⊆ Closure_{α}(up(Z)). This is a contradiction to the fact that v′ ∉ Closure_{α}(up(Z)). □

Lemma 2 For each zone Z, \overrightarrow{Closure_{α}(Z)} ⊆ Closure_{α}(\overrightarrow{Z}) and for each clock constraint g such that Closure_{α}(g) = g, g ∩ Closure_{α}(Z) ⊆ Closure_{α}(g ∩ Z).

Proof Let us take v_{0} ∈ \overrightarrow{Closure_{α}(Z)}. There exists some v_{1} ∈ Closure_{α}(Z) and some t ≥ 0 such that v_{0} = v_{1} + t. By definition of Closure_{α}, there exists some v_{2} ∈ Z such that [v_{1}]_{α} = [v_{2}]_{α}. Thus, [v_{0}]_{α} is a time successor of [v_{2}]_{α}: there exists v_{3} ∈ [v_{0}]_{α} and t′ ≥ 0 such that v_{3} = v_{2} + t′. Thus, v_{3} ∈ \overrightarrow{Z} and it follows that v_{0} ∈ Closure_{α}(\overrightarrow{Z}) because [v_{3}]_{α} = [v_{0}]_{α}. Thus, we get the property we wanted.

The second property holds because of the relation Closure_{α}(g) = g: let us take some v_{0} ∈ g ∩ Closure_{α}(Z). We have that [v_{0}]_{α} ⊆ g and that there exists v_{1} ∈ [v_{0}]_{α} ∩ Z. We obtain that v_{1} ∈ g ∩ Z and thus that v_{0} ∈ Closure_{α}(g ∩ Z). □

5.3 Implementation of the Algorithm

Lemma 3 Let Z be a zone. Then

Z ∈ Z_{β} ⟺ there exists a β-bounded DBMM_{β} such thatZ = ⟦M_{β}⟧.

Proof If M_{β} is a β-bounded DBM, then ⟦M_{β}⟧ is in Z_{β}. A region R ∈ R_{β} is β-bounded. Assume Z is the convex union of two zones Z_{1} and Z_{2} which belong to Z_{β} and such that there exists two β-bounded DBMs M_{Z_{1}} and M_{Z_{2}} such that Z_{1} = ⟦M_{Z_{1}}⟧ and Z_{2} = ⟦M_{Z_{2}}⟧. We assume that for l = 1, 2, M_{Z_{l}} = (m_{i,j}^{(l)}; ≺_{i,j}^{(l)})_{i,j=1...n} and we construct M = (m_{i,j}; ≺_{i,j})_{i,j=1...n} such that:

(m_{i,j}; ≺_{i,j}) = max((m_{i,j}^{(1)}; ≺_{i,j}^{(1)}), (m_{i,j}^{(2)}; ≺_{i,j}^{(2)})).

We first note that M is a β-bounded DBM. We want to prove that ⟦M⟧ = Z. We note first that for l = 1, 2, M_{Z_{l}} ≤ M, thus Z_{l} ⊆ ⟦M⟧ and this implies that Z ⊆ ⟦M⟧. Let r be a real such that −m_{j,i} ≺_{j,i} r ≺_{i,j} m_{i,j}. There exists k such that (m_{i,j}; ≺_{i,j}) = (m_{i,j}^{(k)}; ≺_{i,j}^{(k)}). We have that (m_{j,i}^{(k)}; ≺_{j,i}^{(k)}) ≤ (m_{j,i}; ≺_{j,i}), thus

−m_{j,i}^{(k)} ≺_{j,i}^{(k)} r ≺_{i,j}^{(k)} m_{i,j}^{(k)}. This implies that there exists a valuation v ∈ Z_{k} such that v(i) − v(j) = r. As a consequence, we can not tighten any constant in M. Thus, Z = ⟦M⟧. This concludes the proof. □

Property 1 If M is a DBM, then it holds that ⟦ϕ_{β}(M)⟧ = Approx_{β}(⟦M⟧).

Proof Let M be a DBM in normal form. We get immediately that Approx_{β}(⟦M⟧) ⊆ ⟦ϕ_{β}(M)⟧ because Approx_{β}(⟦M⟧) is the smallest zone from Z_{β} that contains ⟦M⟧ and ⟦ϕ_{β}(M)⟧ is such a zone. There exists a β-bounded DBM M_{β} such that Approx_{β}(⟦M⟧) = ⟦M_{β}⟧. We get that M ≤ M_{β}. Assume that M = (m_{i,j}; ≺_{i,j})_{i,j=1...n} and that M_{β} = (m_{i,j}^{(β)}; ≺_{i,j}^{(β)} )_{i,j=1...n}. We will prove, coefficient by coefficient, that ϕ_{β}(M) ≤ M_{β}. As a first example, assume that (m_{i,0}; ≺_{i,0}) > (max_{i}; ≤) and that (m_{i,j}; ≺_{i,j}) > (max_{i,j}; ≤), then M ≤ M_{β} implies that (m_{i,j}^{(β)}; ≺_{i,j}^{(β)}) = (∞; <). As an other example, assume that (m_{i,0}; ≺_{i,0}) > (max_{i}; ≤) and that (m_{i,j}; ≺_{i,j} ) < (− max_{j,i}; <), then M ≤ M_{β} implies that (m_{i,j}^{(β)}; ≺_{i,j}^{(β)}) ≥ (− max_{j,i}; <). We don’t write the many other cases, but, in this way, we prove that ϕ_{β}(M) ≤ M_{β}, which implies that ⟦ϕ_{β}(M)⟧ ⊆ Approx_{β}(⟦M⟧). This concludes the proof. □

Recent BRICS Report Series Publications

RS-02-35 Patricia Bouyer. Timed Automata May Cause Some Troubles. August 2002. 44 pp.

RS-02-34 Morten Rhiger. A Foundation for Embedded Languages. August 2002. 29 pp.

RS-02-33 Vincent Balat and Olivier Danvy. Memoization in Type-Directed Partial Evaluation. July 2002. 18 pp. To appear in Batory and Consel, editors, ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering, GPCE ’02 Proceedings, LNCS, 2002.

RS-02-32 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. On Obtaining Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation. July 2002. 43 pp. To appear in Chin, editor, ACM SIGPLAN ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ASIA-PEPM ’02 Proceedings, 2002.

RS-02-31 Ulrich Kohlenbach and Paulo B. Oliva. Proof Mining: A Systematic Way of Analysing Proofs in Mathematics. June 2002. 47 pp.

RS-02-30 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. June 2002.

RS-02-29 Christian N. S. Pedersen and Tejs Scharling. Comparative Methods for Gene Structure Prediction in Homologous Sequences. June 2002. 20 pp.

RS-02-28 Ulrich Kohlenbach and Laurenţiu Leuştean. Mann Iterates of Directionally Nonexpansive Mappings in Hyperbolic Spaces. June 2002. 33 pp.

RS-02-27 Anna Östlin and Rasmus Pagh. Simulating Uniform Hashing in Constant Time and Optimal Space. 2002. 11 pp.

RS-02-26 Margarita Korovina. Fixed Points on Abstract Structures without the Equality Test. June 2002.

RS-02-25 Hans Hüttel. Deciding Framed Bisimilarity. May 2002. 20 pp.

RS-02-24 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Static Analysis for Dynamic XML. May 2002. 13 pp.