<figure><img src="image_1.png" /></figure>

HAL
open science

# Difference Bound Constraint Abstraction for Timed Automata Reachability Checking

Weifeng Wang, Li Jiao

► To cite this version:

Weifeng Wang, Li Jiao. Difference Bound Constraint Abstraction for Timed Automata Reachability Checking. 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.146-160, 10.1007/978-3-319-19195-9_10 hal-01767323

HAL Id: hal-01767323

https://inria.hal.science/hal-01767323

Submitted on 16 Apr 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Difference Bound Constraint Abstraction for Timed Automata Reachability Checking

Weifeng Wang<fnref n="1" />,<fnref n="2" /> and Li Jiao<fnref n="1" />

**Abstract.** We consider the reachability problem for timed automata. One of the most well-known solutions for this problem is the zone-based search method. Max bound abstraction and LU-bound abstraction on zones have been proposed to reduce the state space for zone based search. These abstractions use bounds collected from the timed automata structure to compute an abstract state space. In this paper we propose a difference bound constraint abstraction for zones. In this abstraction, sets of difference bound constraints collected from the symbolic run are used to compute the abstract states. Based on this new abstraction scheme, we propose an algorithm for the reachability checking of timed automata. Experiment results are reported on several timed automata benchmarks.

## 1 Introduction

Model checking of timed automata has been studied for a long time since it was proposed [2]. One of the most interesting properties to be verified for timed automata is the reachability property. In this paper, we will focus on the reachability problem of timed automata.

It is known that the reachability problem for timed automata is PSPACE-complete [3]. Initially region-based method [2] was used to discretize the state space, and convert the timed automata model to finite automata. However, the resulting finite automata are so large that it is not practical to perform model checking on them. BDD-based [4, 8] and SAT-based [17] symbolic model checking can be used to fight the state explosion.

Zone-based method is an important approach to the reachability problem of timed automata. In zone-based method, a group of difference bound inequalities is used to symbolically represent a convex set of clock valuations (which is called a "zone"), and exhaustive search is performed on the symbolic state space [7]. Abstraction techniques for zones are used to reduce the symbolic state space, and ensure the reduced symbolic state space to be finite. In max-bound abstraction (a.k.a. k-approximation), the maximum constants appearing in the guards of the timed automata are collected, and used to compute abstractions for zones. LU-abstraction [6] improves by classifying the constants into two categories: those appearing in lower bound guards and those appearing in upper bound guards.

<footnote n="1">¹ State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
{wangwf,ljiao}@ios.ac.cn</footnote>

<footnote n="2">² University of Chinese Academy of Sciences, Beijing 100049, China</footnote>
Behrmann et al. [5] used static analysis on the structure of timed automata to obtain smaller bounds, which lead to coarser abstractions. Herbreteau et al [12] proposed to calculate the bounds on-the-fly, and used a non-convex abstraction based on LU-bounds. All the above mentioned techniques are based on bounds that are collected from the timed automata, which just capture limited amount of information about the system.

In this paper, we explore the possibility to use difference bound constraints as abstractions for zones. In our abstraction scheme, a set of difference bound constraints is used as the abstraction of the zone. In fact, the conjunction of these difference bound constraints is a zone that is larger than the original zone. This abstraction is, to some extent, similar to the predicate abstraction in the program verification field.

A lazy search algorithm similar to that in [13] is used to gradually refine the abstraction. Each node is a tuple (l, Z, C), where (l, Z) is the symbolic state, and C is a set of difference bound constraints, which serves as the abstraction. Initially, the difference bound constraint set of each node is ∅, which means there is no difference bound constraint in the abstraction, i.e., the abstracted zone is the set of all clock valuations. If a transition t is disabled from a node (l, Z, C), we extract a set of difference bound constraints $C_t$ from Z such that $Post_t(\llbracket C_t \rrbracket) = \emptyset$, $C_t$ is sufficient to prove that the transition t from the configuration (l, Z) is disabled. The difference bound constraints in $C_t$ are added to C, after which the change in C is propagated backward according to certain rules. The addition of difference bound constraints into the abstraction is in fact a refinement operation.

The key problem here is how to compute and propagate the set of difference bound constraints. We propose a method to propagate difference bound constraints, which makes use of structural information of the timed automata to identify “important” difference bound constraints in the zones from those that are “irrelevant”.

Unfortunately, the lazy search algorithm using only difference bound constraint abstraction does not necessarily terminate. The LU-abstraction $Extra_{LU}^+$ [6] is used in our algorithm to ensure termination. The resulting algorithm can be seen as a state space reduction using difference bound constraint abstraction on top of $Extra_{LU}^+$-based symbolic search.

We performed experiments to compare our method with zone-based search and the lazy abstraction method proposed in [13]. Results show that in general our method behaves similarly to that in [13], while in some cases our method can achieve better reduction of the state spaces.

**Related work.** Abstraction refinement techniques [9] have attracted much attention in recent years. This kind of techniques check the property of the system by iteratively checking and refining abstract models which tend to be smaller than the original model. Efforts have been devoted on adapting abstraction refinement techniques for the verification of timed automata [16, 10].

Lazy abstraction [11] is an important abstraction refinement technique. In the lazy abstraction procedure, an abstract reachability tree is built on-the-fly, a-
long with the refinement procedure, and predicate formulas are used to represent
the abstract symbolic states. Difference bound constraint abstraction is similar
to predicate abstraction, and the constraint propagation resembles interpolation
[15]. In our method, abstractions only take the form of conjunctions of differ-
ence bound constraints, which is more efficient than general-purpose first order
formulas. Herbreteau et al. [13] proposed a lazy search scheme to dynamically
compute the LU-bounds during state space exploration, which results in smaller
LU-bounds and coarser abstractions. We use a similar lazy search scheme.

**Organization of the paper.** In Section 2 we have a simple review of basic concepts related to timed automata. We present the difference bound constraint abstraction, and the model checking algorithm based on this abstraction in Section 3. An example is given in Section 4 to illustrate how our method achieves state space reduction. Experiment results are reported in Section 5, and conclusions are given in Section 6.

2 Preliminaries

**2.1 Timed Automata and the Reachability Property**

A set of clock variables $X$ is a set of non-negative real-valued variables. A clock constraint is a conjunction of constraints of the form $x \sim c$, where $x, y \in X$, $c \in \mathbb{N}$, and $\sim \in \{<, \leq, >, \geq\}$. A difference bound constraint on $X$ is a constraint of the form $x-y \prec c$, where $x, y \in X \cup \{0\}$, $c \in \mathbb{N}$, and $\prec \in \{<, \leq\}$. Obviously a clock constraint can be re-written as conjunctions of difference bound constraints. A clock valuation is a function $\nu : X \mapsto \mathbb{R}_{\ge 0}$, which assigns to each clock variable a nonnegative real value. We denote $\mathbf{0}$ the special clock valuation that assigns $0$ to every clock variable. For a formula $\varphi$ on $X$, we write $\nu \models \varphi$, if $\varphi$ is satisfied by the valuation $\nu$. Furthermore, we denote by $[[\varphi]]$ the set of all clock valuations satisfying $\varphi$, i.e., $[[\varphi]] = \{\nu|\nu \models \varphi\}$.

**Definition 1 (Timed Automata).** A timed automaton is a tuple $\langle L, l_{init}, X, T \rangle$, where $L$ is a finite set of locations, $l_{init}$ is the initial location, $X$ is a finite set of clocks, and $T$ is a finite set of transitions of the form $l \xrightarrow{a,g,r} l'$, where $a$ is an action label, $g$ is a clock constraint, which we call guard, and $r \subseteq X$ is the set of clocks to be reset.

For a transition $t = l \xrightarrow{a,g,r} l' \in T$, we use t.a., t.g., t.r to denote the corre-
sponding action, guard, and set of clocks to be reset.

**Definition 2 (Semantics of Timed Automata).** A configuration of a timed automaton $\mathcal{A} = \langle L, l_{init}, X, T \rangle$ is a pair $(l, \nu)$ where $l \in L$ is a location, and $\nu$ is a clock valuation. The initial configuration is $(l_{init}, \mathbf{0})$. There are two kinds of transitions

- **Action.** For each pair of states $(l, \nu)$ and $(l', \nu')$, $(l, \nu) \to_t (l', \nu')$ iff there is a transition $t = l \xrightarrow{a,g,r} l' \in T$, and

• $\nu \models g$, and
• $\nu'(x) = \nu(x)$ for each $x \notin r$, and

• $\nu'(x) = 0$ for each $x \in r$.

- **Delay.** For each pair of configurations $(l, \nu)$ and $(l', \nu')$, and an arbitrary $\delta \in \mathbb{R}_{\ge 0}$, $(l, \nu) \to_{\delta} (l', \nu')$, iff $l = l'$ and $\nu'(x) = \nu(x) + \delta$ for each clock $x \in X$.

A run of a timed automaton is a (possibly infinite) sequence of configurations $\rho = (l_0, \nu_0)(l_1, \nu_1)\cdots$, where $(l_0, \nu_0) = (l_{init}, \mathbf{0})$, and for each $i \ge 0$, either $(l_i, \nu_i) \to_t (l_{i+1}, \nu_{i+1})$ for some $t \in T$, or $(l_i, \nu_i) \to_{\delta} (l_{i+1}, \nu_{i+1})$ for some $\delta \in \mathbb{R}_{\ge 0}$.

The definition of timed automata is always extended to networks of timed automata, which is a parallel composition of timed automata. The parallel composition can be obtained by the product of these components. Usually this product is not computed directly, but on-the fly during the verification. In this paper we will describe our method based on timed automata, while it could be naturally extended on networks of timed automata.

In this paper we will consider the *reachability* problem. Basically, a location of a timed automaton is reachable iff there is a run of the timed automaton that reaches the location.

**Definition 3 (Reachability).** A location $l_{acc}$ of a timed automaton $\mathcal{A}$ is reachable iff there is a finite run $\rho = (l_0, \nu_0)(l_1, \nu_1)\cdots (l_k, \nu_k)$, where $l_k = l_{acc}$.

## 2.2 Zone Based Symbolic Semantics

The symbolic semantics of timed automata has been proposed to fight state explosion. Basically, the idea is to represent a set of clock valuations using clock constraints. Zones are used in timed automata model checking to symbolically represent the sets of clock valuations. A *zone* is a convex set of clock valuations that can be represented by a set of difference bound constraints.

For a zone Z and a clock constraint g, we define $Z \wedge g$ as $\{\nu|\nu \in Z \wedge \nu \models g\}$, $Z[r := 0]$ as $\{\nu|\exists \nu' \in Z \cdot \forall x \in r(\nu(x) = 0) \wedge \forall x \notin r(\nu(x) = \nu'(x))\}$, and $Z \uparrow$ as $\{\nu|\exists \nu' \in Z, \delta \in \mathbb{R}_{\ge 0} \cdot \nu = \nu' + \delta\}$. Zones are closed under these operations [7].

**Definition 4 (Symbolic Semantics of Timed Automata).** The symbolic semantics of a timed automaton $\mathcal{A} = (L, l_{init}, X, T)$ is a labeled transition system $(S, \Rightarrow, s_0)$. Each state $s \in S$ is a symbolic configuration $(l, Z)$, where $l$ is a location, and $Z$ is a zone. The initial state is $s_0 = (l_{init}, [0 \le x_1 = x_2 = \cdots = x_n])$. For each pair of states $s = (l, Z)$ and $s' = (l', Z')$, $s \Rightarrow_t s'$ iff there exists a transition $t = l \xrightarrow{a,g,r} l' \in T$ such that $Z' = (Z \wedge g)[r := 0] \uparrow$. A symbolic run is a sequence $(l_0, Z_0)(l_1, Z_1)\cdots$, where $(l_0, Z_0) = (l_{init}, [0 \le x_1 = x_2 = \cdots = x_n])$, and for each $i \ge 0$, $(l_i, Z_i) \Rightarrow_t (l_{i+1}, Z_{i+1})$ for some $t \in T$.

In addition, we define the *Post* operator $Post_t(Z) \stackrel{\text{def}}{=} (Z \wedge t.g)[t.r := 0] \uparrow$. A transition $t = l \xrightarrow{a,g,r} l'$ is *disabled* at $(l, Z)$, if $Post_t(Z) = \emptyset$.
Symbolic semantics is sound and complete with respect to the reachability property [7]. A given location $l_{acc}$ is reachable iff there is a symbolic run ending with a configuration $(l_{acc}, Z)$ where $Z \neq \emptyset$.

Zones can be represented as Difference Bound Matrices (DBMs), and efficient algorithms for manipulating DBMs have already been proposed [7]. The DBM representation of a zone on the clock set $X$ is a $(|X| + 1) \times (|X| + 1)$ matrix, each element of which is a tuple $(<, c)$, where $< \in \{<, \leq\}$ and $c \in \mathbb{N}$. In a DBM $D$, $D_{0x} = (<, c)$ means $0 - x < c$, i.e. $x > -c$, $D_{x0} = (<, c)$ means $x - 0 < c$, i.e. $x < c$, for $x, y \neq 0$, $D_{ij} = (<, c)$ represents the constraint $x_i - x_j < c$. Two different DBMs might correspond to the same zone. In order to tackle this problem, the canonical forms of DBMs can be computed by the Floyd-Warshall algorithm [7].

The zone-based semantics described in the above is not necessarily finite. Max-bound abstraction and LU-bound abstraction are proposed to reduce the state space to finite, and the former can be seen as a special case of the latter. Basically, these abstraction techniques remove from the zone those constraints that exceed certain bounds, resulting in an abstracted zone that is larger than the original one. Coarser abstractions lead to smaller symbolic state space. As far as we know, $Extra_{LU}^{+}$ [6] is the coarsest convex-preserving abstraction based on LU-bounds.

An LU-bound is a pair of functions $LU$, where $L: X \to \mathbb{N} \cup \{-\infty\}$ is called a lower bound function and $U: X \to \mathbb{N} \cup \{-\infty\}$ an upper bound function.

**Definition 5 (LU-extrapolation [6]).** Let $Z$ be a zone whose canonical DBM is $\langle c_{i,j}, <_{i,j} \rangle_{i,j=0,1,...,|X|}$. Given an LU-bound $LU$, the LU-extrapolation $Extra_{LU}^{+}(Z)$ of $Z$ is a zone $Z'$ which can be represented by a DBM $\langle c'_{i,j}, <'_{i,j} \rangle_{i,j=0,1,...,|X|}$, where

$$ \langle c'_{i,j}, <'_{i,j} \rangle = \begin{cases} \infty & \text{if } c_{i,j} > L(x_i) \\ \infty & \text{if } -c_{0,i} > L(x_i) \\ \infty & \text{if } -c_{0,j} > U(x_j), i \neq 0 \\ (-U(x_j), <) & \text{if } -c_{0,j} > U(x_j), i = 0 \\ (c_{i,j}, <_{i,j}) & \text{otherwise} \end{cases} $$

We denote by $\Rightarrow^E$ the symbolic semantics of timed automata augmented with $Extra_{LU}^{+}$: for two symbolic configurations $(l, Z)$ and $(l', Z')$, $(l, Z) \Rightarrow^E (l', Z')$ iff there is a zone $Z''$ such that $(l, Z) \Rightarrow (l', Z'')$ and $Z' = Extra_{LU}^{+}(Z'')$. We can choose the LU-bound $L(x)$ and $U(x)$ as follows: for each clock $x$, $L(x)(U(x))$ is the largest constant $c$ such that $x > c(x < c)$ or $x \ge c(x \le c)$ appears in the guard of some transition. Intuitively, $L(x)(U(x))$ collects the maximum constant appearing in the lower-bound (upper-bound) guard of $x$. It can be proved that $\Rightarrow^E$ preserves reachability [6].
# 3 Difference Bound Constraint Abstraction Based Reachability Checking

## 3.1 Difference Bound Constraint Abstraction and Adaptive Simulation Graph

For a zone Z and a difference bound constraint c we denote $Z \models c$ as $\forall \nu \in Z \cdot \nu \models c$. For a set C of difference bound constraints we denote $[[C]]$ to be the set of valuations that satisfy all the constraints in C, i.e., $[[C]] = \{\nu | \forall c \in C \cdot \nu \models c\}$. Intuitively, a set C of difference bound constraints is interpreted as a conjunction of the constraints from C. In fact, $[[C]]$ is also a zone, although it will not be stored as a canonical DBM in our algorithm. In the sequel, we might mix the use of set-theoretic notations (e.g. intersection) and logic notations (e.g. conjunction) on zones and constraints.

**Definition 6 (Difference Bound Constraint Abstraction).** A difference bound constraint abstraction C for a zone Z is a set of difference bound constraints such that $Z \subseteq [[C]]$.

This definition resembles the concept of predicate abstraction in program verification. Each difference bound constraint in C can be seen as a predicate. In our algorithm, only those difference bound constraints that are useful for the reachability problem are kept, while the irrelevant constraints are ignored. The difference bound constraint abstraction of a zone is still a zone, but we store it as a set of constraints rather than a canonical DBM. Based on this abstraction, we define an Adaptive Simulation Graph (ASG) similar to that in [13].

**Definition 7 (Adaptive Simulation Graph).** Given a timed automaton $\mathcal{A}$, the adaptive simulation graph ASG$_\mathcal{A}$ of $\mathcal{A}$ is a graph with nodes of the form $(l, Z, C)$, where $l$ is a location, $Z$ is a zone, and $C$ is a set of difference bound constraints such that $Z \subseteq [[C]]$. A node could be marked tentative (which roughly means it is covered by another node). Three constraints should be satisfied:

**G1** For the initial state $l_0$ and initial zone $Z_0$, there is a node $(l_0, Z_0, C_0)$ in the graph for some $C_0$.

**G2** If a node $(l, Z, C)$ is not tentative, then for every transition $(l, Z) \Rightarrow_t (l', Z')$ s.t. $Z' \neq \emptyset$, there is a successor $(l', Z', C')$ for this node.

**G3** If a node $(l, Z, C)$ is tentative, there is a non-tentative node $(l, Z', C')$ covering it, i.e., $Z \subseteq [[C]] \subseteq [[C']]$.

In addition, two invariants are required.

**I1** If a transition $t$ is disabled from $(l, Z)$, and $(l, Z, C)$ is a non-tentative node, then $t$ should also be disabled from $(l, [[C]])$.

**I2** For every edge $(l, Z, C) \Rightarrow_t (l', Z', C')$ in the ASG: $Post_t( [[C]] ) \subseteq [[C']]$.

For a node $v = (l, Z, C)$, we use $v.l$, $v.Z$, and $v.C$ to denote the three components. We say that a node $(l, Z, C)$ is covered by a node $(l, Z', C')$, if $Z \subseteq [[C']]$.

The following theorem states that, the adaptive simulation graph preserves reachability of the corresponding timed automaton.
**Theorem 1.** A location $l_{acc}$ in the timed automaton $\mathcal{A}$ is reachable, iff there is a node $(l_{acc}, Z, C)$ such that $Z \neq \emptyset$ in $\mathcal{ASG}_\mathcal{A}$.

The right-to-left direction of this theorem is obviously true: by the definition of ASG, each path in $\mathcal{ASG}_\mathcal{A}$ corresponds to a symbolic run in $\mathcal{A}$. In order to prove the other direction of Theorem 1, we prove a slightly stronger lemma.

**Lemma 1.** If there is a symbolic run $(l_0, Z_0) \cdots (l, Z)$ in $\mathcal{A}$ with $Z \neq \emptyset$, then there must be a non-tentative node $(l, Z_1, C_1)$ in $\mathcal{ASG}_\mathcal{A}$ such that $Z \subseteq [C_1]$.

*Proof.* We prove this lemma by induction on the length of the run. For the 0-length run and $(l_0, Z_0)$, the lemma is trivially true. Assume the lemma is true for a run $(l_0, Z_0) \cdots (l, Z)$, now we prove that the lemma holds for every successor $(l', Z')$ of $(l, Z)$ with $(l, Z) \Rightarrow_t (l', Z')$ and $Z' \neq \emptyset$.

We need to prove that there is a node in $\mathcal{ASG}_\mathcal{A}$ corresponding to $(l', Z')$ as described in the lemma. By induction hypothesis, there is a non-tentative node $v$ such that $Z \subseteq [v.C]$. We now assert that $Post_t(v.Z) \neq \emptyset$. Because, otherwise, by **I1** of Definition 7 we will have $Post_t([v.C]) = \emptyset$, and consequently $Post_t(Z) \subseteq Post_t([v.C]) = \emptyset$, which contradicts the assumption $Z' \neq \emptyset$. From **G2** we know that there is a successor $v'$ of $v$ such that $(v.l, v.Z) \Rightarrow_t (v'.l, v'.Z)$. By **I2** we have $Post_t([v.C]) \subseteq [v'.C']$, so $Z' = Post_t(Z) \subseteq Post_t([v.C]) \subseteq [v'.C]$, If $v'$ is non-tentative, then it is a node that we want to find, and the lemma is proved. Otherwise, there is a non-tentative node $v''$ covering $v'$. From **G3** we know that $[v'.C] \subseteq [v''.C]$, so $Z' \subseteq [v''.C]$, and $v''$ is the qualifying node.

According to Theorem 1, the reachability problem could be solved by exploring the ASG. The algorithm for constructing the ASG will be described in the next subsection.

## 3.2 The ASG-constructing Algorithm

The algorithm for constructing the ASG is shown in Algorithm 1. The main procedure repeatedly calls `EXPLORE` to explore the nodes until an accepting node is found (lines 10-11), or the worklist is empty (line 8).

The function `EXPLORE` proceeds as follows. For a node $v$ to be explored, first it checks whether $v$ is an accepting node. If so, the algorithm exits with the result "reachable", otherwise it checks whether there is a non-tentative node $v''$ covering $v$. If so, $v$ is marked tentative with respect to $v''$ (line 13), and the set of difference bound constraints of $v''$ is copied to $v$ to maintain **G3** of Definition 7 (line 14). There is no need to generate successor nodes for a tentative node. Otherwise, the difference bound constraint set of $v$ is computed using the transitions disabled at $v$ to maintain **I1** (line 17), after which successor nodes of $v$ are generated (maintaining **G2**) and put into the worklist for exploration (lines 19-21).

Whenever the difference bound constraint set of a node $v'$ is changed, PROP-AGATE will be called (lines 15, 18, 38) to propagate the newly-added constraints
<table><caption>**Algorithm 1** The ASG-constructing algorithm</caption><tr><td>1:</td><td>function MAIN</td><td>20:</td><td>create the successor v' =</td></tr><tr><td>2:</td><td>let v<sub>root</sub> = (l<sub>0</sub>, Z<sub>0</sub>, Ø)</td><td></td><td>(l', Z', Ø) of v</td></tr><tr><td>3:</td><td>add v<sub>root</sub> to the worklist</td><td>21:</td><td>add v' to worklist</td></tr><tr><td>4:</td><td>while worklist not empty do</td><td>22:</td><td>function RESOLVE</td></tr><tr><td>5:</td><td>remove v from the worklist</td><td>23:</td><td>for all v tentative w.r.t. v' do</td></tr><tr><td>6:</td><td>EXPLORE(v)</td><td>24:</td><td>if v.Z &sub; [[v'.C]] then</td></tr><tr><td>7:</td><td>RESOLVE</td><td>25:</td><td>mark v non-tentative</td></tr><tr><td>8:</td><td>return "not reachable"</td><td>26:</td><td>set v.C &larr; Ø</td></tr><tr><td>9:</td><td>function EXPLORE(v)</td><td>27:</td><td>add v to worklist</td></tr><tr><td>10:</td><td>if v.l is accepting then</td><td>28:</td><td>function PROPAGATE(v', C')</td></tr><tr><td>11:</td><td>exit "reachable"</td><td>29:</td><td>let v = parent(v')</td></tr><tr><td>12:</td><td>else if &exist; v'' non-tentative s.t. v.l =</td><td>30:</td><td>C &larr; BACKPROP(v, v', C')</td></tr><tr><td></td><td>v'', q &and; v.Z &sub; [[v''.C]] then</td><td>31:</td><td>C<sub>1</sub> &larr; UPDATE(v, C)</td></tr><tr><td>13:</td><td>mark v tentative w.r.t. v''</td><td>32:</td><td>if C<sub>1</sub> &ne; Ø then</td></tr><tr><td>14:</td><td>v.C &larr; v''.C</td><td>33:</td><td>for all v<sub>t</sub> tentative w.r.t. v do</td></tr><tr><td>15:</td><td>PROPAGATE(v, v.C)</td><td>34:</td><td>if v<sub>t</sub>.Z &sub; [[v.C]] then</td></tr><tr><td>16:</td><td>else</td><td>35:</td><td>C<sub>t</sub> &larr; UPDATE(v<sub>t</sub>, C<sub>1</sub>)</td></tr><tr><td>17:</td><td>v.C &larr; DISABLED(v.l, v.Z)</td><td>36:</td><td>PROPAGATE(v<sub>t</sub>, C<sub>t</sub>)</td></tr><tr><td>18:</td><td>PROPAGATE(v, v.C)</td><td>37:</td><td>if v &ne; v<sub>root</sub> then</td></tr><tr><td>19:</td><td>for all (l', Z') s.t. (v.l, v.Z) &rarr;</td><td>38:</td><td>PROPAGATE(v, C<sub>1</sub>)</td></tr><tr><td></td><td>(l', Z') and Z' &ne; Ø do</td><td></td><td></td></tr></table>

backward to its parent $v$ (to maintain **I2**) (lines 29-31), and further to the nodes tentative with respect to $v$ (to maintain **G3**) (line 36). If a tentative node $v_t$ is no longer covered by $v$, the function RESOLVE will eventually be called (line 7) to mark it non-tentative, remove all constraints from its difference bound constraint set, and put it into the worklist for exploration (lines 25-27).

For each node $v$, the difference bound constraint abstraction $v.C$ is stored as a set of difference bound constraints, rather than a canonical DBM. Checking whether $Z &sub; [[C]]$ for a zone $Z$ and a difference bound constraint set $C$ can be accomplished by checking whether $Z &supseteq; c$ for all $c &in; C$. When adding constraints to a difference bound constraint abstraction, only the strongest constraints are kept, which is handled by the function UPDATE, whose code is omitted here.

### 3.3 Computing the Difference Bound Constraint Sets

The algorithm for building the ASG relies on two functions DISABLED, and BACKPROP to extract the “important” difference bound constraints from zones. In this subsection we describe an implementation of the two functions. Before doing that we introduce the arithmetic on $\{<, \leq\} \times \mathbb{N}$. For two arbitrary pairs $(<1, c_1)$, $(<2, c_2) \in \{<, \leq\} \times (\mathbb{N} \cup \{+\infty\})$, $(<1, c_1) + (<2, c_2) = (<3, c_3)$, where $c_3 = c_1 + c_2$, and $<3 = <$ iff $<1 = <$ or $<2 = <$. The order “<” is defined as: $(<1, c_1) < (<2, c_2)$ iff $c_1 < c_2$ or $c_1 = c_2 \land <1 = < \land <2 = \leq$.
**DISABLED** In order to maintain the invariant **I1**, the result *C* computed by DISABLED(*l*, *Z*) should satisfy: i) *Z* ⊆ [[*C*]], and ii) *Post*<sub>*t*</sub>([[*C*]]) = ∅ for each *t* disabled at (*l*, *Z*).

By Definition 4 we know that $Post_t(Z) = \emptyset$ iff $Z \wedge t.g = \emptyset$. Thus the problem is reduced to: given a zone $Z$, and a formula $\varphi$ which is conjunctions of difference bound constraints, such that $Z \wedge \varphi = \emptyset$, find a set $C$ of difference bound constraints such that $Z \subseteq [C]$ and $[C] \wedge \varphi = \emptyset$. Since $Z \wedge \varphi = \emptyset$, there must be a sequence of difference bound constraints $x_0 - x_1 <_{0} c_0, x_1 - x_2 <_{1} c_1, \dots, x_{m-1} - x_m <_{m-1} c_{m-1}, x_m - x_0 <_{m} c_m$ such that

- C1 Each of them appears either in $\varphi$, or in the canonical DBM of $Z$.

- C2 $x_i \neq x_j$ for $i, j \in \{0, 1, \dots, m\}$ and $i \neq j$

- C3 $(<_0, c_0) + \dots + (<_m, c_m) < (<, 0)$, i.e., this sequence of difference bound constraints forms a contradiction.

We take $C$ to be $\{c = x_i - x_{(i+1) \bmod (m+1)} <_i c_i | c$ is from $Z\}$. Obviously, the $C$ obtained above satisfies i) and ii).

As shown in [7], a conjunction of difference bound constraints can be seen
as a directed weighted graph, where each clock variable corresponds to a node,
and each constraint corresponds to a weighted edge, whose weight is a pair in
$\{<, \leq\} \times (\mathbb{N} \cup \{+\infty\})$. Figure 1 illustrates the directed weighted graph for the
zone $x \geq 0 \wedge y - x = 10$. There is a contradiction in the conjunction iff there is
a negative cycle in the graph, i.e., the sum of weights in the cycle is less than
($\leq, 0$).

<figure><img src="image_3.png" /><figcaption>Fig. 1: Directed weighted graph of zone $x \ge 0 \wedge y - x = 10$</figcaption></figure>

The difference bound constraints in *C* correspond to the edges in the graph of *Z* that form a negative cycle with the edges from the graph of *ϕ*. So the problem is reduced to finding a negative cycle in the merged graph of *Z* and *ϕ*, and picking the edges in the cycle that belong to *Z*. This task is accomplished by the function FINDCONTRA in Algorithm 2, where Floyd-Warshall algorithm is used to find a negative cycle. Function DISABLED in Algorithm 2 calls FINDCONTRA for every disabled transition, and collects all the constraints obtained.

**BACKPROP** In order to maintain the invariant **I2**, the result *C* computed by BACKPROP(*v*, *v'*, *C*') (where (*v*.*l*, *v*.*Z*) ⇒<sub>*t*</sub> (*v'*.*l*, *v'*.*Z*)) should satisfy: i) *Post*<sub>*t*</sub>([[*C*]]) ⊆ [[*C*′]] and ii) *v*.*Z* ⊆ [[*C*]].
If there is a set $C_{c'}$ of difference bound constraints for each $c' \in C'$, such that $v.Z \subseteq [[C_{c'}]]$ and $Post_t( [[C_{c'}]] ) \models c'$, then we can choose $C$ as $\bigcup_{c' \in C'} C_{c'}$. One can easily check that such a $C$ satisfies the above two conditions. We only need to consider the propagation of each difference bound constraint in $C'$ one by one.

For simplicity, we break up each transition into three steps: guard, reset, and time delay, and explain the propagation for each step. The overall description of BACKPROP is shown in Algorithm 2.

We assume two zones $Z_1, Z_2$ and a difference bound constraint $c_2$ which corresponds to $Z_2$ (i.e. $Z_2 \models c_2$).

**Delay.** Now we have $Z_1 \uparrow= Z_2$, we want to find a $C_{c_2}$ such that $Z_1 \subseteq [[C_{c_2}]]$ and $[[C_{c_2}]] \uparrow \models c_2$. Observe that $c_2$ must be in one of the three cases: $x - 0 \prec c$, $0 - x \prec c$, and $x - y \prec c$, where $x, y \in X$ and $c \in \mathbb{N}$. Since $Z_1 \uparrow= Z_2$, $c_2$ can not be of the form $x - 0 \prec c$, and for the other two cases we have $Z_1 \models c_2$ and $[[\{c_2}\]] \uparrow \models c_2$. So we can just choose $C_{c_2}$ to be $\{c_2\}$. Intuitively, for time delay, we just copy $c_2$ from the successor to the predecessor.

**Reset.** For a set $r$ of clocks such that $Z_1[r] = Z_2$, we want to find a $C_{c_2}$ such that $Z_1 \subseteq [[C_{c_2}]]$ and $[[C_{c_2}]][r] \models c_2$. Let $c_2$ be $x - y \prec c$, where $x \in X \cup \{0\}$, $y \in X$ and $c \in \mathbb{N}$, we choose $C_{c_2}$ as $\{c_1\}$, where:

$$ c_1 = \begin{cases} x - y \prec c, & \text{if } x, y \notin r \\ 0 - y \prec c, & \text{if } x \in r, y \notin r \\ x - 0 \prec c, & \text{if } x \notin r, y \in r \\ 0 - 0 \prec c, & \text{if } x, y \in r \end{cases} \qquad (1) $$

The first and the last cases are trivial. Let's look at the second case. Since $x \in r$, according to the definition of reset operation, it must be the case that $Z_2 \models x = 0$. According to the assumption, $Z_2 \models c_2$. Note that $c_2$ is $x - y \prec c$. Combining the above two results we have $Z_2 \models 0 - y \prec c$. Since $y \notin r$, the value of $y$ has not changed during the reset operation, thus we have $Z_1 \models 0 - y \prec c$. Conversely, we can check that $[[\{0 - y \prec c\}][r] \models x - y \prec c$. Thus $\{c_1\}$ is a qualified candidate for $C_{c_2}$. It is similar for the third case.

Here we ignore the case when $c_2$ is $x - 0 \prec c$ because, according to the time delay operation (which always follows the reset operation in the timed automata run), this is impossible.

**Guard.** For a guard $g$ such that $Z_1 \wedge g = Z_2$, we want to find a $C_{c_2}$ such that $Z_1 \subseteq [[C_{c_2}]]$ and $[[C_{c_2}] \wedge g \models c_2$. Notice that $Z_1 \wedge g \models c_2$ iff $Z_1 \wedge (g \wedge \neg c_2) = \emptyset$, similarly, $[[C_{c_2}] \wedge g \models c_2$ iff $[[C_{c_2}] \wedge (g \wedge \neg c_2) = \emptyset$. Like $c_2$, its negation $\neg c_2$ is also a difference bound constraint, so $g \wedge \neg c_2$ is a conjunction of difference bound constraints, and we can use FINDCONTRA to compute the set $C_{c_2}$.
<table><caption>**Algorithm 2**</caption><tr><td>1: function FINDCONTRA(Z, φ)</td><td>8: C ← C ∪ FINDCONTRA(Z, t.g)</td></tr><tr><td>2: Find a negative cycle using Floyd-Warshall algorithm on the merged graph of Z and φ</td><td>9: return C</td></tr><tr><td>3: Take the sequence of constraints corresponding to the negative cycle in Z ∧ φ: c<sub>0</sub>, c<sub>1</sub>, . . . , c<sub>m-1</sub>.</td><td>10: function BACKPROP(v, v', C')</td></tr><tr><td>4: return {c<sub>i</sub> | c<sub>i</sub> is from Z}</td><td>11: Given v ⇒<sub>t</sub> v'</td></tr><tr><td>5: function DISABLED(l, Z)</td><td>12: C ← ∅</td></tr><tr><td>6: C ← ∅</td><td>13: for all c<sub>2</sub> ∈ C' do</td></tr><tr><td>7: for all t disabled at (l, Z) do</td><td>14: Compute c<sub>1</sub> according to (1)</td></tr><tr><td></td><td>15: C ← C ∪ FINDCONTRA(v.Z, g ∧ ¬c<sub>2</sub>)</td></tr><tr><td></td><td>16: return C</td></tr></table>

### 3.4 Termination of the ASG-constructing Algorithm

In order to ensure that the ASG-constructing algorithm terminates, we make slight modifications on Definition 7 and on Algorithm 1. The condition **G2** of Definition 7 is modified to:

**G2'** If a node $(l, Z, C)$ is not tentative, then for every transition $(l, Z) \Rightarrow^E_t (l', Z')$ s.t. $Z' \neq \emptyset$, there is a successor $(l', Z', C')$ for this node.

The symbolic transition relation $\Rightarrow$ is replaced with $\Rightarrow^E$, which means that the operator $Extra_{LU}^+$ is used when computing the successor nodes. Accordingly, in Line 19 of Algorithm 1, $(v.l, v.Z) \Rightarrow (v'.q, v'.Z)$ should be changed to $(v.l, v.Z) \Rightarrow^E (v'.q, v'.Z)$.

Now our algorithm can be seen as a further reduction made on top of $Extra_{LU}^+$-based search.

**Theorem 2.** For an arbitrary timed automaton $\mathcal{A}$, the modified version of Algorithm 1 as described above will terminate.

*Proof.* Assume, to the contrary, that the algorithm does not terminate. There must be an infinite sequence of explored nodes $v_1, v_2, \dots$ (listed in the order of exploration) such that $v_1.l = v_2.l = \dots$. Since the symbolic state space with $Extra_{LU}^+$ abstraction is finite, there must be two nodes $v_i, v_j$ (with $i < j$) in the sequence such that $v_i.Z = v_j.Z$. From Definition 6 we know that $v_j.Z = v_i.Z \subseteq [v_i.C]$, so $v_j$ will never be explored, which contradicts the assumption.

## 4 An Example

Here we illustrate how our method works on the example timed automaton $\mathcal{A}_1$ shown in Figure 2a, where $q_4$ is the accepting location. Following [5], instead of considering one global LU-bound, we associate a local LU-bound to each location using static guard analysis. The LU-bound at each location is given in Figure 2c.
<figure><img src="image_4.png" /><figcaption>Fig. 2: (2a): a timed automaton $\mathcal{A}_1$, (2b): the ASG of $\mathcal{A}_1$. Solid arrows represent the transition relation, while dotted arrows represent the cover relation. (2c): the LU-bounds of $\mathcal{A}_1$</figcaption></figure>

Using zone-based search, the following symbolic configurations will be generated: $(q_0, x = z \ge 0 \land y \le z)$, $(q_0, z = x + 1 \land y \le z \land x \ge 0)$, $(q_0, z = x + 2 \land y \le z \land x \ge 0)$, ..., $(q_0, z = x + 100 \land y \le z \land x \ge 0)$, ..., which is more than 100 nodes. When using our method, the resulting ASG has only 3 nodes, as shown in Figure 2b. In this example our method successfully ignores many of the constraints that are irrelevant to the reachability problem, achieving a huge reduction.

The algorithm in [13] can not avoid generating too many nodes either. The reason is that, LU-bound based abstractions can not find that the difference bound constraints on $z-x$ and $y-x$ are irrelevant. In our abstraction scheme, we consider more information than just LU-bounds, so our method can identify these constraints to be irrelevant.

# 5 Experiments

We have implemented UPPAAL's search algorithm, the algorithm in [13], and our algorithm. Similar to [14], an improvement is made on Algorithm 1 in the implementation: for each node $v$, if there is a node $v'$ such that $v.l = v'.l$ and $v.Z \subseteq v'.Z$, then $v$ will be deleted, parents of $v$ will be inherited by $v'$, and the difference bound constraints in $v'.C$ will be propagated to the parents of $v$, and nodes that are covered by $v$ (if there is any) will be marked non-tentative.

We performed experiments on several benchmarks. The results are shown in Table 1 and Table 2, which are the results for breadth-first search (bfs) and
depth-first search (dfs), respectively. $D''$ is from [13], Fischer comes from the demos in the UPPAAL tool. The other models are from [1]. In our experiment settings, no location is set to be accepting, thus forcing the algorithms to perform exhaustive state space exploration. The programs are run on a VMware virtual machine with Ubuntu 10.04 operating system, which is allocated 2GB of memory. The underlying PC has an Intel Core i7 CPU of 2.93GHz and 3GB of RAM.

<table><caption>Table 1: Experiment results of the three methods using bfs search. “Search-Extra<sub>LU</sub><sup>+</sup>” stands for Extra<sub>LU</sub><sup>+</sup>-based search similar to UPPAAL. “a<sub>≤LU</sub>, disabled” is the algorithm in [13]. “DBCA-Extra<sub>LU</sub><sup>+</sup>” is difference bound constraint abstraction combined with Extra<sub>LU</sub><sup>+</sup>. “tnds” is the total number of nodes generated, “fnds” is the number of nodes finally left, and “tm(s)” is the running time (in seconds). “to” stands for time-out(200s).</caption><thead><tr><th rowspan="2">Model</th><th colspan="3">Search-Extra<sub>LU</sub><sup>+</sup></th><th colspan="3">a<sub>≤LU</sub>, disabled</th><th colspan="3">DBCA-Extra<sub>LU</sub><sup>+</sup></th></tr><tr><th>tnds</th><th>fnds</th><th>tm(s)</th><th>tnds</th><th>fnds</th><th>tm(s)</th><th>tnds</th><th>fnds</th><th>tm(s)</th></tr></thead><tbody><tr><td>A<sub>1</sub></td><td>405</td><td>204</td><td>0.03</td><td>405</td><td>203</td><td>0.14</td><td>3</td><td>3</td><td>0.00</td></tr><tr><td>D''<sub>7</sub></td><td>12869</td><td>12869</td><td>6.77</td><td>113</td><td>113</td><td>0.00</td><td>113</td><td>113</td><td>0.01</td></tr><tr><td>D''<sub>8</sub></td><td>48619</td><td>48619</td><td>100.08</td><td>145</td><td>145</td><td>0.01</td><td>145</td><td>145</td><td>0.01</td></tr><tr><td>D''<sub>70</sub></td><td></td><td></td><td>to</td><td>9941</td><td>9941</td><td>4.35</td><td>9941</td><td>9941</td><td>90.19</td></tr><tr><td>CSMA/CD 9</td><td>99288</td><td>45836</td><td>3.13</td><td>78552</td><td>35084</td><td>7.33</td><td>78552</td><td>35084</td><td>4.38</td></tr><tr><td>CSMA/CD 10</td><td>258249</td><td>120845</td><td>8.44</td><td>200649</td><td>90125</td><td>12.15</td><td>200649</td><td>90125</td><td>14.91</td></tr><tr><td>CSMA/CD 11</td><td>656312</td><td>311310</td><td>25.30</td><td>501432</td><td>226830</td><td>65.16</td><td>501432</td><td>226830</td><td>38.27</td></tr><tr><td>CSMA/CD 12</td><td>1636261</td><td>786447</td><td>68.81</td><td>1230757</td><td>561167</td><td>118.12</td><td>1230757</td><td>561167</td><td>98.58</td></tr><tr><td>FDDI 12</td><td>52555</td><td>727</td><td>13.72</td><td>422</td><td>341</td><td>0.56</td><td>176</td><td>154</td><td>0.13</td></tr><tr><td>FDDI 30</td><td></td><td></td><td>to</td><td>2923</td><td>2227</td><td>26.84</td><td>464</td><td>406</td><td>2.29</td></tr><tr><td>Fischer 8</td><td>132593</td><td>25080</td><td>2.61</td><td>132593</td><td>25080</td><td>8.44</td><td>132593</td><td>25080</td><td>7.55</td></tr><tr><td>Fischer 9</td><td>487459</td><td>81035</td><td>11.24</td><td>487459</td><td>81035</td><td>30.82</td><td>487459</td><td>81035</td><td>22.35</td></tr><tr><td>Critical 4</td><td>434421</td><td>53937</td><td>6.83</td><td>499441</td><td>53697</td><td>31.58</td><td>548781</td><td>54180</td><td>23.59</td></tr><tr><td>Lynch 4</td><td>46432</td><td>12700</td><td>1.19</td><td>46432</td><td>12700</td><td>1.26</td><td>46432</td><td>12700</td><td>1.05</td></tr></tbody></table>

The results on the model $A_1$ show the advantage of our method over LU-bound based abstractions. This is the case when LU-bound information is not sufficient to identify irrelevant constraints. On the other models, our method behaves similarly as $a_{≤LU}, disabled$. This is quite reasonable, since we use the same lazy search framework.

In many cases $DBCA-Extra_{LU}^{+}$ generates less nodes, but costs more time than $Search-Extra_{LU}^{+}$. This is due to the overhead of the effort to maintain the invariants of ASGs. The situation is similar for $a_{≤LU}, disabled$. However, for some of the models we can see that the state space reduction of our method over $Search-Extra_{LU}^{+}$ is large enough to cover the overhead.
<table><caption>Table 2: Experiment results of the three methods using dfs search. All settings are the same as in Table 1, except that dfs search is performed here</caption><thead><tr><th rowspan="2">Model</th><th colspan="3">Search-Extra<sup>+</sup><sub>LU</sub></th><th colspan="3">a<sub>≤LU</sub>, disabled</th><th colspan="3">DBCA-Extra<sup>+</sup><sub>LU</sub></th></tr><tr><th>tnds</th><th>fnds</th><th>tm(s)</th><th>tnds</th><th>fnds</th><th>tm(s)</th><th>tnds</th><th>fnds</th><th>tm(s)</th></tr></thead><tbody><tr><td>A<sub>1</sub></td><td>405</td><td>204</td><td>0.02</td><td>405</td><td>203</td><td>0.23</td><td>3</td><td>3</td><td>0.00</td></tr><tr><td>D<sub>7</sub><sup>′′</sup></td><td>12869</td><td>12869</td><td>6.61</td><td>113</td><td>113</td><td>0.01</td><td>113</td><td>113</td><td>0.01</td></tr><tr><td>D<sub>8</sub><sup>′′</sup></td><td>48619</td><td>48619</td><td>110.15</td><td>145</td><td>145</td><td>0.01</td><td>145</td><td>145</td><td>0.01</td></tr><tr><td>D<sub>70</sub><sup>′′</sup></td><td></td><td></td><td>to</td><td>9941</td><td>9941</td><td>4.68</td><td>9941</td><td>9941</td><td>55.30</td></tr><tr><td>CSMA/CD 9</td><td>246072</td><td>45836</td><td>9.43</td><td>136813</td><td>36901</td><td>18.63</td><td>129718</td><td>35415</td><td>11.58</td></tr><tr><td>CSMA/CD 10</td><td>822699</td><td>120845</td><td>37.98</td><td>452788</td><td>98731</td><td>96.94</td><td>362407</td><td>90769</td><td>35.57</td></tr><tr><td>CSMA/CD 11</td><td>2758945</td><td>311310</td><td>150.23</td><td></td><td></td><td>to</td><td>997243</td><td>228054</td><td>120.85</td></tr><tr><td>FDDI 12</td><td>1016</td><td>727</td><td>0.27</td><td>96</td><td>96</td><td>0.02</td><td>96</td><td>96</td><td>0.03</td></tr><tr><td>FDDI 30</td><td>6308</td><td>4507</td><td>5.73</td><td>240</td><td>240</td><td>0.26</td><td>240</td><td>240</td><td>0.41</td></tr><tr><td>FDDI 50</td><td>17508</td><td>12507</td><td>53.21</td><td>400</td><td>400</td><td>0.72</td><td>400</td><td>400</td><td>1.35</td></tr><tr><td>Fischer 8</td><td>218017</td><td>25080</td><td>4.37</td><td>196738</td><td>25080</td><td>14.00</td><td>156634</td><td>25080</td><td>7.84</td></tr><tr><td>Fischer 9</td><td>1058685</td><td>81035</td><td>25.80</td><td>906766</td><td>81035</td><td>86.21</td><td>642739</td><td>81035</td><td>44.13</td></tr><tr><td>Critical 4</td><td>1067979</td><td>54469</td><td>15.19</td><td>1025269</td><td>53731</td><td>66.45</td><td>1009995</td><td>54488</td><td>38.25</td></tr><tr><td>Lynch 4</td><td>84421</td><td>12700</td><td>1.21</td><td>83171</td><td>12700</td><td>3.81</td><td>83967</td><td>12700</td><td>3.25</td></tr></tbody></table>

# 6 Conclusion

In this paper we proposed a difference bound constraint abstraction on zones for timed automata reachability checking. Difference bound constraint sets are used as abstractions in a lazy search algorithm, and Extra<sup>+</sup><sub>LU</sub> is used to ensure termination. Experiments show that in some of the cases the new abstraction scheme reduces the state spaces. A future work would be to perform experiments on other models to further investigate the performance.

Our abstraction is not necessarily coarser than [13], because non-convex abstractions [12] are used in [13], while difference bound constraint abstraction is in fact conjunctions of constraints, which is convex. However, our abstraction scheme makes it possible to make use of more information than just LU-bounds, achieving state space reduction in some cases.

The difference bound constraint abstraction is used in a forward lazy search scheme, and Extra<sup>+</sup><sub>LU</sub> is used to ensure termination. In fact, backward zone-based search is also possible [18], and does not need Max-bound abstraction or LU-abstraction to ensure termination. A possible future work is to explore the possibility to perform lazy search using difference bound constraint abstraction in a backward manner.

# Acknowledgements

We thank the anonymous reviewers for their helpful comments on the earlier version of this paper.
References

1. Benchmarks of Timed Automata. http://www.comp.nus.edu.sg/~pat/bddlib/timedexp.html

2. Alur, R., Dill, D.: Automata for modeling real-time systems. In: M. Paterson (ed.) ICALP 1990, LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)

3. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

4. Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data-structures for the verification of timed automata. In: O. Maler (ed.) HART 1997, LNCS, vol. 1201, pp. 346–360. Springer, Heidelberg (1997)

5. Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.: Static guard analysis in timed automata verification. In: H. Garavel, J. Hatcliff (eds.) TACAS 2003, LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003)

6. Behrmann, G., Bouyer, P., Larsen, K., Pelnek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: K. Jensen, A. Podelski (eds.) TACAS 2004, LNCS, vol. 2988, pp. 312–326. Springer, Heidelberg (2004)

7. Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: J. Desel, W. Reisig, G. Rozenberg (eds.) Lectures on Concurrency and Petri Nets, LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)

8. Beyer, D.: Improvements in bdd-based reachability analysis of timed automata. In: J. Oliveira, P. Zave (eds.) FME 2001, LNCS, vol. 2021, pp. 318–343. Springer, Heidelberg (2001)

9. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: E. Emerson, A. Sistla (eds.) CAV 2000, LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)

10. Dierks, H., Kupferschmid, S., Larsen, K.: Automatic abstraction refinement for timed automata. In: J.F. Raskin, P. Thiagarajan (eds.) FORMATS 2007, LNCS, vol. 4763, pp. 114–129. Springer, Heidelberg (2007)

11. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70. ACM (2002)

12. Herbreteau, F., Kini, D., Srivathsan, B., Walukiewicz, I.: Using non-convex approximations for efficient analysis of timed automata. In: FSTTCS 2011, pp. 78–89 (2011)

13. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: N. Sharygina, H. Veith (eds.) CAV 2013, LNCS, vol. 8044, pp. 990–1005. Springer, Heidelberg (2013)

14. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. CoRR abs/1301.3127 (2013)

15. McMillan, K.: Lazy abstraction with interpolants. In: T. Ball, R. Jones (eds.) CAV 2006, LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)

16. Sorea, M.: Lazy approximation for dense real-time systems. In: Y. Lakhnech, S. Yovine (eds.) FORMATS/FTRTFT 2004, LNCS, vol. 3253, pp. 363–378. Springer, Heidelberg (2004)

17. Wozna, B., Zbrzezny, A., Penczek, W.: Checking reachability properties for timed automata via sat. Fundam. Inf. 55(2), 223–241 (2003)

18. Yovine, S.: Model checking timed automata. In: G. Rozenberg, F. Vaandrager (eds.) Lectures on Embedded Systems, LNCS, vol. 1494, pp. 114–152. Springer, Heidelberg (1998)