Relaxed Clock Difference Diagrams for
Timed Automata Model Checking
Esteban Pavese and Fernando Schapachnik
Departamento de Computación, FCEyN,
Universidad de Buenos Aires, Buenos Aires, Argentina ⋆
{epavese,fschapac}@dc.uba.ar
Abstract. Clock Difference Diagrams (CDDs), a BDD-like data struc-
ture for model checking of timed automata, were presented in 1999. After
the original article the work on them seems to have stopped, although
there are still important open questions.
The proposed algorithm relied on the traditionally used data structure
(DBMs) for most operations. CDDs definition required that repeated
subtrees were aliased, but no clear algorithm was presented for producing
such compact representation, which seems costly to achieve. Also, since
then, case studies have increased in size.
In this article we revisit CDDs by introducing RCDDs, a variation that
does not require maximum aliasing. We present the complete set of op-
erations required to perform forward reachability analysis with no need
for DBMs. By employing a fully RCDD-based algorithm our experiments
show a consistent reduction of time requirements in case studies from the
current literature, sometimes up to more than 40%.
1 Introduction and Previous Work
In current days timed systems are both pervasive and critical, ranging from
embedded and PDAs to plant and flight controllers. Their complexity is ever
increasing so automated ways of verifying them make sense. Automated methods,
however, are known to suffer from scalability problems: their time and memory
requirements grow exponentially as systems increase in size. This is why any
technique that can palliate such problems is useful.
We focus on exploration of timed automata [1] –an extension of finite au-
tomata with the possibility to model dense time– by on-the-fly forward reacha-
bility analysis [2]. Well-known tools in this area, such as Kronos [3] and UP-
PAAL [4], represent sets of clock valuations by means of a data structure called
Difference Bound Matrices (DBMs for short) [5]. DBMs are (n + 1) × (n + 1)
matrices, where n is the number of clocks in the system, counting 0 as a spe-
cial clock. Each cell represents the upper bound on the difference between the
corresponding clocks. Although Sect. 2 presents these concepts in more detail,
a brief description is required: said data structure provides support for a graph
⋆ Partially supported by UBACyT 2004 X020, PICT 32440 and 11738.

reachability-like algorithm (depicted in Fig. 1) which saves the encountered sym-
bolic states in a set called Visited .
For both warranting termination and avoiding duplicated exploration, timed
automata reachability requires knowing if a newly discovered symbolic state is
already covered by the existing ones. This is inefficient when working with DBMs,
because they can only represent convex clock valuations. The traditional solution
is to employ sets of DBMs, but it is usually very hard to detect superpositions
there, leading to repetitions of calculations and other drawbacks.
There have been many attempts to overcome this problem by using BDD-like
data structures [6], which are often used in untimed systems. See, for example,
Asarin et al. [7] and Strehl et al. [8] among others. The one with the most
potential, however, was a 1999 article by Behrmann et al. In [9] they presented
Clock Difference Diagrams (CDDs for short). Their work used DBMs for most
of the operations and CDDs for the Visited set, obtaining memory savings at
the cost of extra time.
We consider that CDDs needed to be revisited because:
– Besides their use as a representation for the Visited set, a complete reacha-
bility algorithm that did not rely on DBMs was yet to be provided.
– Being a tree-like data structure, they could have repeated subtrees. CDDs
then require that repeated subtrees were replaced by aliasing in a maximal
way (referred to as “maximal sharing” in the original article). Because detect-
ing repeated subtrees can be expensive we believe the topic required further
analysis (we elaborate on this on Sect. 3.5).
– The original case studies used only systems with a maximum of 5 clocks.
Complexity being O(n!2nCn), where n is number of clocks and C is the
largest constant appearing in the inequalities [10], it is dominated by the
number of clocks.
In this work, we present a data structure called Relaxed CDD (RCDD for
short) in which we implement all the operations required for the above men-
tioned reachability algorithm. RCDDs are similar to CDDs, but do not require
maximum sharing of subtrees. They achieve the reduction of verification times
at the expense of storing some extra constraints (compared to the traditional
encoding of DBMs). Their usage is explored in two ways: as a representation for
both convex and non-convex sets of clock valuations, the former as a complete
replacement for DBMs. We present correctness proofs (up to article length re-
strictions) and run case studies from the current literature obtaining speedups
of up to 40% with moderate increase of memory consumption.
CRDs, short for Clock Restriction Diagrams, should also be mentioned. They
were introduced by Wang in [11] and are similar to CDDs, but use open intervals.
As will be shown in Sect. 3.3, RCDDs allow to avoid many calls to a cubic
function, which is key to the time savings. These calls would not be avoided if
closed intervals were not present.
The rest of the article is structured as follows: next section introduces the
formalism of timed automata and provides the necessary background. RCDDs

are detailed in Sect. 3. Experimentation is presented in Sect. 4. Finally, Sect. 5
rounds up the article with our conclusions and future road map.
2 Background
Timed automata [1] are a widely used formalism to model and analyze timed
systems. They are supported by several tools such as Kronos [3] or UPPAAL [4].
Their semantics are based on labeled state-transition systems and time-divergent
runs over them. Here we present their basic notions and refer the reader to [1,
3] for a complete formal presentation.
Definition 1 (Timed automaton). A timed automaton (TA for short) is a
tuple A = 〈L,X,Σ,E, I, l0〉, where L is a finite set of locations, X is a finite
set of clocks (non-negative real variables), Σ is a set of labels, E is a finite set
of edges, I : L tot→ ΨX is a total function associating to each location a clock
constraint called the location’s invariant, and l0 ∈ L is the initial location. Each
edge in E is a tuple 〈l, a, ψ, α, l′〉, where l ∈ L is the source location, l′ ∈ L is
the target location, a ∈ Σ is the label, ψ ∈ ΨX is the guard, α ⊆ X is the set of
clocks reset at the edge. The set of clock constraints ΨX for a set of clocks X is
defined according to the following grammar: ΨX ∋ ψ ::= x ∼ d|x− y ≺ c|ψ ∧ ψ,
where x, y ∈ X,∼∈ {<,≤,=, >,≥},≺∈ {<,≤}, d ∈ IN and c ∈ Z. Invariants
must be past-closed [12].
Usually, a TA A has an associated mapping Pr : L 7→ 2Props which assigns to
each location a subset of propositional variables from the set Props.
The parallel composition A1 ‖ A2 of TAs A1 and A2 is defined using a label-
synchronized product of automata [1, 3]. At any time, the state of the system
is determined by the location and the values of clocks, which must satisfy the
location invariant. The system can evolve in two different ways: either an enabled
transition is taken, changing the location and resetting some clocks while the
others keep their values unaltered (a discrete step), or it may let some amount of
time pass (a timed step). In the last case the system remains in the same location
and all clocks increase according to the elapsed time, while still satisfying the
location invariant.
Definition 2 (Clock valuations). A valuation is a total function from the
clock set X into IR+ (i.e., the reading of each clock in a particular moment).
The valuation set over X, VX is defined as {v : X tot→ IR+}. For each v ∈ VX and
δ ∈ IR+, v+ δ stands for the valuation defined as (∀x ∈ X)(v+ δ)(x) = v(x)+ δ.
To deal with infinite state manipulation, convex sets of clock valuations are
symbolically represented as conjunctions of inequalities in ΨX (e.g., 1 ≤ x ≤
5 ∧ x − y > 8). Each of these conjunctions represents a convex set of points,
and is referred to as a zone. A data structure called Difference Bound Matrices
(DBM) [5] is typically used to manipulate such kind of information. Non-convex
sets are represented as unions of convex sets, and are usually called regions.

1: function ForwardReach(Property φ)
2: Visited ← ∅
3: Pending ← {(l0, z0)}
4: while Pending 6= ∅ do
5: (l, z)← next(Pending)
6: Add((l, z),Visited)
7: if (l, z) |= φ then return YES
8: end if
9: Zl ←
S
(l,z′)∈(Visited∪Pending) z
′
10: for (l′, z′) ∈ suc⊲(l, z) do
11: if z′ * Zl then
12: Add((l′, z′),Pending)
13: end if
14: end for
15: end while
16: return NO
17: end function
Fig. 1. Forward reachability algorithm.
During the reachability algorithm (see Fig. 1), symbolic states are represented
by a pair (l, z) where l is a location and z a timed zone. Given a symbolic state,
the successor set is computed by the suc⊲ operator, which is defined as follows:
suc⊲(l, z) = {(l′, z′)/ 〈l, a, ψ, α, l′〉 ∈ E ∧ z′ = sucτ (resetα(z ∩ ψ)) ∩ I(l′)}
Where resetα means putting the clocks in α to zero and sucτ (ψ) means
replacing the constraints of the form x ≺ c by x < ∞ while leaving the rest
untouched.
Not every constraint needs to be present for all the operations. Actually, a
reduced version of the constraint systems can be used most of the time, thus
saving memory [13]. In practice, most tools use a variation of DBMs, called
Minimal Constraint Representation DBMs which employs that idea. As these
DBMs are sparse, they are not stored like proper matrices, but as a linked list
of constraints, in order to save space.
3 RCDDs
In this section, after presenting the basic definitions of our data structure,
Sect. 3.2 covers the algorithms and their correctness. Special focus is done in
Sect. 3.3 on how to avoid some costly operations in RCDDs, which is key to
their performance. Some methods to reduce the traditional memory overhead
of tree-like structures (especially in the case of zones) are shown in Sect. 3.4.
Finally, Sect. 3.5 contains a discussion on non-convex set representation.

3.1 Data Structure Definition
Definition 3 (RCDD). Given a set X of clock variables, X ′ = X ∪ {0}, an
RCDD is defined by a tuple k = [diff (k), Ints(k), S(k)], where:
1. diff (k) ∈ (X × X ′) ∪ {TRUE ,FALSE} is the clock difference represented
by this node. These clock differences are extended with values TRUE and
FALSE . We call nodes that hold the latter terminal.
2. Ints(k) is a list of outgoing edges. Each edge is labeled with an integral inter-
val. Ints(k)n denotes the nth list’s interval, and |Ints(k)| denotes the list’s
size.
3. S(k) is a list of successor nodes. S(k)n and |S(k)| are defined in a similar
way as previously. For each 1 ≤ n ≤ |S(k)|, S(k)n yields the node reached
by traversing the edge Ints(k)n.
An RCDD k such that diff (k) is TRUE (or FALSE ) will usually be referred
as just TRUE (or FALSE ) for short. Similarly, given an interval I we will write
S(k, I) to denote the node obtained by traversing the edge labeled I from k.
Formally, S(k, I) = k′ ⇔ ∃i, 1 ≤ i ≤ |Ints(k)| such that Ints(k)i = I ∧ S(k)i =
k′.
Since RCDDs are hierarchical in nature, an order on clock differences is
needed, which can be defined as an extension of an order on clock variables.
Definition 4 (Total order on clock differences). Given a total order < on
clock variables, the total order on clock differences, also noted <, is defined as
its pairwise extension.
This total order allows us to state the structure’s invariant, as follows:
Definition 5 (Structure invariant). The following constraints are imposed
on every node k of an RCDD:
– Whenever diff (k) is TRUE or FALSE , the lists Ints(k) and S(k) must be
empty.
– In the other case, no element of S(k) may be FALSE .
– Given a total order on clock differences <, it must hold that for any k′ in
S(k), either diff (k) < diff (k′) or k′ is TRUE .
– Since edges are labeled by intervals, the existence of both differences xi − xj
and xj − xi for any pair of clocks xi, xj is redundant. Therefore, if diff (k)
is of the form xj − xi it must hold that xi < xj.
– Every pair of intervals in diff (k) must be disjoint. Moreover, diff (k) must
be sorted; we say that for any two intervals I and J , I < J ⇔ ∀i, j such
that i ∈ I and j ∈ J , it holds that i < j.
It is worth noting that, unlike CDDs, RCDDs do not require sharing of
repeated subtrees (more on that on Sect. 3.4). On the following, we will elaborate
on the structure’s semantics. For this purpose, we’ll need to define a mapping
between temporal constraints in ΨX and RCDDs.

Definition 6 (Mapping of temporal constraints to RCDDs, r;RCDD).
∀ψ1, ψ2 ∈ ΨX , x, y ∈ X,x < y, c ∈ IN, we define the mapping r ; RCDD as
follows:
r;RCDD(True) = [TRUE , λ, λ] (1)
r;RCDD(False) = [FALSE , λ, λ] (2)
r;RCDD(c < x) = [x− 0, «(c,∞)», «r;RCDD(True)»] (3)
r;RCDD(x < c) = [x− 0, «[ 0, c)», «r;RCDD(True)»] (4)
r;RCDD(x− y < c) = [x− y, «(−∞, c)», «r;RCDD(True)»] (5)
r;RCDD(ψ1 ∧ ψ2) = Intersection(r;RCDD(ψ1), r;RCDD(ψ2)) (6)
Mapping definitions 3, 4 and 5 have also a corresponding one for ≤ with the
interval closed to the right.
We will now aim to define the semantics of the structure.
Definition 7 (RCDD satisfiability). The satisfiability of an RCDD k by a
clock valuation v ∈ VX (noted v |= k) is defined inductively as follows, ∀x, y ∈
X :
v |= [TRUE , λ, λ] ∧ v |6= [FALSE , λ, λ] (7)
v |= [x− y, Ints, S] ≡
|Ints|
∨
i=1
{ ( v(x)− v(y) ∈ Intsi ) ∧ v |= Si } (8)
That is, a valuation v satisfies a node of an RCDD that contains the clocks x
and y if and only if the difference among x’s and y’s value in v is included in
some of the node’s outgoing edges and v also satisfies the corresponding subtree.
It is worth emphasizing that given the intervals’ disjunction, the satisfied
path (if any) is unique, easing the algorithms.
Theorem 1. The mapping r;RCDD previously defined is correct with respect
to satisfiability, that is, ∀ψ ∈ ΨX , v ∈ VX , v |= ψ ⇔ v |= r;RCDD(ψ).
3.2 Algorithms
In this section, we present in Figs. 3(a) to 4(b) the conceptual, recursive al-
gorithms for all operations needed for reachability verification with RCDDs
(except for inclusion, which is presented in its iterative version in Fig. 2). In
these algorithms, the restriction forbidding the existence of FALSE nodes has
been relaxed, in order to keep the presentation simple. We also elaborate on the
strategies used to develop efficient, iterative algorithms, where the restrictions
are enforced in full. Finally we present the iterative algorithm for zone inclusion
checking, being a critical operation in the verification, along with a proof of its
correctness.
In the algorithms, RCDDs that represent zones will be noted as RCDDz.

Theorem 2. The algorithms presented in Figs. 3(a) to 4(b) are correct. That
is, the only valuations that satisfy the resulting RCDDs are the ones that are
compatible to the application of the respective operation in the input constraint
system.
Proof. Proofs omitted due to lack of space. The interested reader can find them
in [14].
Iterative versions of the algorithms are stack-based. The stack’s size is fixed
during the verification process, thus reducing memory operations on it (the max-
imum stack size is roughly n2/2+n where n is the number of clocks in the system,
though it will rarely reach that size). Also, only intervals taking part on non-
FALSE paths are stored and evaluated, effectively reducing memory and time
consumption. Fig. 2 shows the algorithm used to decide whether a zone is in-
cluded in a given region or not. The stack used in this case holds information
about both RCDDs, marking intervals as they are traversed. The algorithm re-
quires the RCDD representing the zone to be in canonical form, which is much
like the canonical form for DBMs; this is not needed for the RCDD representing
the region.
Theorem 3. The algorithm of zone inclusion checking (Fig. 2) is correct.
Proof. First of all, the algorithm termination is guaranteed since on each step
smaller RCDDs are pushed onto the stack (or else they’re pushed with more
marks on its intervals). This ensures that eventually the stack will empty. We
need to prove then that the result is correct, that is, it holds that ∀ψ1, ψ2 ∈
ΨX , Included?(Canonical(r;RCDD(ψ1)), r;RCDD(ψ2)) ⇔ ψ1 ⊆ ψ2. The
canonical form for an RCDD representing a zone is similar to that of a DBM.
We’ll prove each implication.
=⇒ ) Assuming the algorithm returns True, we prove that the RCDD represent-
ing a zone has its only path included (possibly split up) in those in the RCDD
passed as a region. We’ll analyze each case as we pop from the stack, beginning
with the initial state of the stack, which has only [z, r].
– if r is either TRUE or FALSE , the inclusion verification is trivial.
– if diff (top.r) < diff (top.z), since top.z is in canonical form this means the
difference in r is restricted to some values, whereas z does not restrict it
at all. This would make the algorithm return False, which goes against our
assumption.
– if diff (r) > diff (z), then the difference in z is not directly restricted in r
(it may be, as deduced from other restrictions; however, we may ignore this
condition until we find the conflicting differences). In this case we push the
successor node for z.
– finally, if diff (r) = diff (z) we only need to check that the interval leading
out of z is spanned by those leading out of r. If that is not the case, then
valuations exist that satisfy z but not r, which would have resulted in a
False output. In order to check this, we push into the stack each successor
of r that comes from an interval which spans over the one of z.

1: function Included? (z: RCDDz, r: RCDD)→ ret: boolean
2: ret← True
3: Stack(RCDD, RCDD) stack
4: Push (stack, [z, r])
5: while ¬ Empty(stack) ∧ ret do
6: top← Pop (stack)
7: if top.r = FALSE then ret← (top.z = FALSE)
8: else if top.r = TRUE then ret← True
9: else
10: if diff (top.r) < diff (top.z) then ret← False
11: else if diff (top.z) < diff (top.r) then
12: I ← Ints(top.z)1
13: Push (stack, [S(top.z, I), top.r])
14: else
15: I ← Ints(top.z)1
16: if ¬ IsSpanned? (I, top.r) then ret← False
17: else
18: J ← first unmarked interval in top.r
19: if there is no such J then continue
20: elseMark (top.r, J)
21: end if
22: if I ∩ J 6= ∅ then
23: Push (stack, [top.z, top.r])
24: Push (stack, [S(top.z, I), S(top.r, J)])
25: elsePush (stack, [top.z, top.r])
26: end if
27: end if
28: end if
29: end if
30: end while
31: return ret
32: end function
Fig. 2. RCDD inclusion checking iterative algorithm.
Since all options which would allow valuations satisfying z and not r are
filtered out by the assumption of a True output, we only need to prove the other
implication.
⇐=) We prove this implication by means of its counterpart. We’ll prove that
∀ψ1, ψ2 ∈ ΨX ,¬Included?(Canonical(r; RCDD(ψ1)), r; RCDD(ψ2)) =⇒
ψ1 * ψ2, that is, there exists a valuation v that satisfies ψ1 but not ψ2. Since
the ret variable is set to True at the beginning, it will suffice to analyze the
situations where it is set to False:
– it may be that top.r = FALSE and top.z 6= FALSE . In that case any valua-
tion v is such that it doesn’t satisfy FALSE .
– it may also be that diff (top.r) < diff (top.z). In that case, any valuation
will satisfy diff (top.r) in top.z: its absence means the lack of restriction. We

may choose any valuation v such that v(diff (top.r)) is not in any of top.r’s
intervals (there exist infinitely many of such valuations).
– lastly, it may be that diff (top.r) = diff (top.z) and that the interval leading
out of top.z is not spanned by those in top.r. In this case, we just need to
take a valuation v such that v(diff (top.r)) is indeed within the subinterval
not spanned.
Since we find a valuation v for every case where the result is set to False, the
theorem is proven.
3.3 Early Cut
The inclusion algorithm features early cuts in cases where it can be easily de-
duced that there is no inclusion. This is not news, as its DBM counterpart does
the same. What’s novel, is the use of an early cut in the intersection algorithm.
At the end of the intersection it is necessary to determine if the result is
empty or not, and this requires obtaining the structure’s canonical form. This
operation is very expensive: its runtime is O(n3), n being the number of clocks
in the system.
Because both upper and lower explicit bounds are present for each clock
in RCDDs, it can be determined early in the process whether the resulting
intersection will be empty or not. For instance, if 2 < x ∧ x < 3 ∧ y < 7 is to be
intersected with 0 < x∧x < 2∧y < 3, in RCDDs the upper and lower bound on
clock x are close to each other in the representation, and thus operated at the
same time, so only by performing the simple intersection operation, which means
taking the stricter constraint for each bound, it can be deduced 2 < x ∧ x < 2.
Knowing that, the costly canonical form function has no need to be called.
The actual implementation of this early cut would be, in the iterative version
of Algorithm 4(a), to return FALSE as an else to the if in line 12.
These savings in the number of times that the canonical form operation is
called are key in reducing the verification time.
It should be noted that the same optimizations could in principle be applied
to raw DBMs. However, they are incompatible with the minimal constraint rep-
resentation. Having the intervals, RCDDs achieve not to store the complete
matrix, but at the same time allowing for this important saving in computation.
3.4 Representing Zones
RCDDs are basically trees. Tree-like structures can have a large representation
overhead if they are not treated carefully.
Proposition 1. Each RCDD node (k) can be represented in a fixed number of
bits. As the number of clocks is fixed it is easy to compute how many bits are
needed to represent two clocks.

1: function Union (rA, rB : RCDD)→
r′ : RCDD
2: if rA = FALSE return RCDDB
3: else if rA = TRUE return TRUE
4: else if diff (rA) < diff (rB)
5: for all I ∈ Ints(rA)
6: Add_RCDD(r′, I,
Union(S(rA, I), rB))
7: end for
8: else if diff (rA) > diff (rB)
9: . . . follows as previous case.
10: else
11: for all I ∈ Ints(rA), J ∈ Ints(rB)
12: if ¬Empty(I ∩ J)
13: Add_RCDD(r′, I ∩ J,
Union(S(rA, I), S(rB , J)))
14: end if
15: end for
16: end if
17: return r′
18: end function
1: function Reset (C : Set(clock), z :
RCDDz)→ z′ : RCDDz
2: if z = FALSE ∨ z = TRUE return z
3: end if
4: I ← Ints(z)1
5: RCDDz z′′ ← Reset(C, S(z, I))
6: if diff (z) = x− 0 for some x ∈ C
7: diff (z′) ← diff (z)
8: AddInterval (z’, [ 0, 0 ], z′′)
9: else if diff (z) = x−y and (x ∈ C∨y ∈
C)
10: if y ∈ C
11: diff (z′) ← diff (z)
12: AddInterval (z’,
ClockInterval (x), z′′)
13: else
14: diff (z′) ← (−1)×diff (z)
15: AddInterval (z’,
ClockInterval (y), z′′)
16: end if
17: else
18: AddInterval (z’, I, z′′)
19: end if
20: return z’
21: end function
Fig. 3. RCDD union and reset recursive algorithms.
Proposition 2. Each RCDD edge (Ints(k)i) can also be represented by a fixed
number of bits. Each comparison requires an additional bit to indicate whether
the constraint is < or ≤. To calculate how many bits will be needed for the
constants, use the upper bound as defined in [15]. After that, a pointer to the
S(k)i node is needed. Pointers have a fixed length (given an architecture).
Zones have a very particular shape in RCDDs: each node has only one edge.
We can take advantage of that to produce a more compact representation. As
we only need to code for a list of nodes (pair of clocks) and intervals, there is no
need to specify pointers: each interval refers to the next node on the list.
From Props. 1 and 2 we know that each pair (node, interval) can be coded
in a fixed number of bits. So, we can calculate a priori how many intervals can
be packed in a machine word. If we also consider that the minimized version of
the constraint system usually requires O(n) clock constraints, we can allocate
continuous blocks of words so that most RCDDs will fit in just one of them. If
more than one block is needed, only then a pointer is required.
In this way memory is saved because in modern machines a pointer takes
a considerable number of bits –e.g. 32 or 64– which can instead probably code
many intervals.

1: function Intersection (rA, rB :
RCDD)→ r′ : RCDD
2: if rA = FALSE return FALSE
3: else if rA = TRUE return rB
4: else if diff (rA) < diff (rB)
5: for all I ∈ Ints(rA)
6: Add_RCDD(r′, I,
Intersection(S(rA, I), rB))
7: end for
8: else if diff (rA) > diff (rB)
9: . . . follows as previous case.
10: else
11: for all I ∈ Ints(rA), J ∈ Ints(rB)
12: if ¬Empty(I ∩ J)
13: Add_RCDD(r′, I ∩ J,
Intersection(S(rA, I),
S(rB , J)))
14: end if
15: end for
16: end if
17: return r′
18: end function
1: function TimeSucc (z: RCDDz)→
z′ : RCDDz
2: if z = FALSE ∨ z = TRUE return z
3: else if diff (z) = x− 0 for some x
4: I ← Ints(z)1
5: J ← 〈I.min,+∞〉
6: diff (z′) ← diff (z)
7: AddInterval (z’, J)
8: S(z’, J) ← TimeSucc(S(z, I))
9: else return z
10: end if
11: return z’
12: end function
Fig. 4. RCDD intersection and time successors recursive algorithms.
3.5 Representing Regions
Although the main motivation of CDDs was to obtain an appropriate data struc-
ture for non-convex sets, some problems require special attention. We find the
requirement for maximum sharing –present in CDDs and omitted in RCDDs–
problematic.
Indeed, the original approach to maximum sharing described in [9] was to
keep a CDD-node cache as a hash table and try to find an existing node there
when a new one was required. The operation was reputed as taking constant time.
However, for a node to be a suitable replacement of another, their successors
have to match. Unlike BDDs, which have fixed binary branching, each CDD
node can be branched in any number of (non-overlapping) intervals. The depth
is indeed bounded by the square of the number of clocks, as each node involves
two of them1. It can clearly be seen that it doesn’t seem likely to implement the
cache in constant time, so we take the term constant as meaning negligible, and
attribute that to the small sizes of the case studies originally used.
1 Note that this strategy differs from the reduce operation in OBDDs [16]. Reduce is
called once at the end of operations to recover the structure invariant that states
the nonexistence of repeated subgraphs. It works bottom up in linear time to merge
isomorphic substructures. Again, the time is linear because the branching is only
finite.

Case studies have grown since the CDD article by Behrmann et al. Current
literature examples have at least an order of magnitude more states, and many
times the number of clocks (keep in mind that timed automata reachability is
exponential in the number of clocks).
Also, more operations output RCDDs –as opposed to only union in the CDD
article–, meaning that repeated subtrees need to be detected on a number of
different algorithms. Combined with the size of current models, we find that
repetition detection consumes unacceptable time in the techniques we proto-
typed.
Nevertheless, we still believe that sharing is the crucial point for the use of
CDD-like data structures as a representation for regions. Our tests confirm that
the number of inclusions and states is reduced using RCDDs as a representa-
tion for regions. However, memory requirements increase unacceptably without
sharing, and as already mentioned, the sharing detection problem seems still un-
solved for CDDs. We find that more research should be done in this area before
reaching to a sustainable conclusion.
4 Case Studies
To validate the data structure, we incorporated RCDDs into the model checker
Zeus2 [17] and ran a series of experiments against well known case studies from
the literature. Some case studies were also treated by ObsSlice [18], a safe
model reducer, and are primed on the tables.
Example Components Clocks Reachable states
MinePump 10 10 1172911
MinePump’ 10 10 131261
RCS5 8 8 271771
Conveyor6AB 11 12 1357200
Pipe6 14 14 80280
Pipe6 ’ 14 14 24375
Table 1. Examples sizes.
1. RCS5 , the Railroad Crossing System inspired in [19] with 5 trains.
2. Pipe6 , end-to-end signal propagation in a pipe-line of sporadic processes that
forward a signal emitted by a quasi periodic source, with 6 stages.
3. Conveyor6AB , Conveyor Belt [17] (with 6 stages and 2 objects).
4. MinePump, a design of a fault-detection mechanism for a distributed mine-
drainage controller. [20].
Table 1 summarizes the sizes of the examples used in this article. All the
experiments were run on an Intel Pentium IV 3.0 MHz machine with 2 GB of
RAM, running Linux 2.6.
2 Although Zeus is a distributed tool, a monoprocessor version was used for this
article.

Example RDBM RDBM #cf() RCDD RCDD ∆ #cf()
time mem. time mem.
(secs.) (KB) (×103) (secs.) (KB) (%)
RCS5 true 52.40 7320 273 56.49 (+7%) 9548 (+30%) -38
RCS5 false 1859.40 34348 3784 1575.20 (-15%) 38144 (+11%) -33
MinePump’ true 71.71 6924 405 40.76 (-43%) 8112 (+17%) -35
MinePump’ false 856.84 19488 1728 554.91 (-35%) 23856 (+22%) -33
MinePump true 5145.56 56644 5031 2977.80 (-42%) 72760 (+28%) -33
MinePump false 37768.39 152840 15583 22440.00 (-40%) 194104 (+27%) -32
Conveyor6AB true 2.35 3216 27 1.50 (-36%) 3372 (+4%) -34
Conveyor6AB false 16.93 7972 197 12.13 (-28%) 7840 (-1%) -32
Pipe6 ’ true 128.66 16988 673 120.34 (-6%) 24560 (+44%) -34
Pipe6 ’ false 58.87 13228 349 40.81 (-30%) 11772 (-11%) -39
Pipe6 true 4215.56 152416 10532 3366.45 (-20%) 200256 (+31%) -40
Pipe6 false 253.29 35268 1168 160.91 (-36%) 30368 (-13%) -42
Table 2. Results obtained with both implementations.
As can be seen in Table 2 in most of the case studies a time saving of around
40% is achieved, with the exception of a few cases that take little time and where
overhead probably dominates. The same table also shows that the time saved
is proportional to the number of avoided calls to the canonical form function
(recall Sect. 3.3). There is, however, a memory penalty of more or less the same
order of magnitude than the time saved. It is nevertheless interesting to note
that in cases like MinePump false, the time saved is more than 4 hours of almost
11 hours, at the price of less than 40 extra MB of RAM, a tradeoff that seems
more than acceptable.
For a number of technical and availability reasons we didn’t have a chance
to compare against other tools. However, as each tool contains heuristics and
improvements that might not be present in the others, cross tool comparisons
does not permit to assess the performance of the data structure by itself, which is
the objective of this paper. It should be noted, however, that the use of RCDDs
is orthogonal to most available techniques for the reduction of time and space
such as zone widening, abstractions, etc.
5 Conclusions and Future Work
In this article we revisited Clock Difference Diagrams, a data structure that
was born to represent non-convex sets of clock valuations for model checking
of timed automata. The original presentation left some questions open, namely
the provision of an algorithm that did not rely on DBMs, experimentation with
bigger case studies, and clarification of the repeated subtree detection algorithm.
While analyzing these questions we developed RCDDs, a variation of the
above mentioned CDDs. RCDDs differ from standard CDDs, mainly in that
they do not require maximum sharing. Although that is a desirable property,
repeated subtrees detection can be very costly. As all the algorithms needed for

reachability analysis of timed automata have been presented and proven correct,
RCDDs can completely replace the traditional DBMs as a data structure for
timed model checking.
The original 1999 article that introduced CDDs, by Behrmann et al., showed
memory savings at the price of augmented times. Their case studies, although
representative at the time, are orders of magnitude smaller than the ones that
tools deal with today. With hundreds of thousands of states, and many operations
manipulating RCDDs, detecting repetitions becomes prohibitive. In fact, early
tests confirm that the number of inclusions and states is reduced using RCDDs
as a representation for non-convex sets, but, without sharing repeated subtrees,
memory requirements increase unacceptably. However, we were not able to come
up with a repetition detection technique that did not took also unacceptable
extra time. It is worth noting that the original presentation of CDDs did not
give details on how to achieve that. We still consider this an open question where
more research should be put.
Partial hashing of subtrees might be used to detect duplication. Another idea
is to store not the subtree, but the symbolic calculation from where it can be
reconstructed. An approach similar to OBDDs Reduce operation [16], where the
data structure is minimized after being constructed might make sense and needs
to be tried.
Case studies for RCDDs have shown a positive impact: times are reduced
with a mild memory overhead. The savings go up to 40%; in cases saving 4
hours out of 11, with an overhead of only 40 MB of RAM. This lets us conclude
that the structure seems suitable for a verification tool.
Future research agenda includes looking more closely into sharing for very
large data structures, as mentioned above. Also, as Zeus was born with the aim
of being a distributed tool, we would like to look into the possibility of having
multiple threads working with different branches of the tree in parallel.
References
1. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science
126(2) (1994) 183–235
2. Bouajjani, A., Tripakis, S., Yovine, S.: On-the-Fly Symbolic Model-Checking for
Real-Time Systems. In: 18th IEEE Real-Time Systems Symposium (RTSS ‘97),
San Francisco, USA, IEEE Computer Scienty Press (1997)
3. Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A
model-checking tool for real-time systems. In: Proc. of the 10th Intl. Conf. CAV ’98.
Volume 1427 of LNCS., Springer-Verlag (1998) 546–550
4. Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a
tool suite for automatic verification of real-time systems. In: Hybrid Systems,
Springer-Verlag (1995) 232–243
5. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems.
In: International Workshop of Automatic Verification Methods for Finite State
Systems. Volume 407 of LNCS., Grenoble, France, Springer-Verlag (1990) 197–212
6. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE
Transactions on Computers 35(8) (1986) 677–691

7. E. Asarin, M. Bozga, A. Kerbrat, O. Maler, M. Pnueli, A. Rasse: Data structures
for the verification of timed automata. In O. Maler, ed.: Hybrid and Real-Time
Systems. Volume 1201 of LNCS., Grenoble, France, Springer Verlag (1997) 346–360
8. K. Strehl, L. Thiele: Symbolic model checking using Interval Diagram techniques.
Technical report, Computer Engineering and Networks Lab (TIK), Swiss Federal
Institute of Technology (ETH) (1998)
9. Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reach-
ability analysis using Clock Difference Diagrams. In: Computer Aided Verification.
(1999) 341–353
10. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Infor-
mation and Computation 104(1) (1993) 2–34
11. Wang, F.: Efficient verification of timed automata with BDD-like data-structures.
In: VMCAI 2003: Proceedings of the 4th International Conference on Verification,
Model Checking, and Abstract Interpretation, London, UK, Springer-Verlag (2003)
189–205
12. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for
Real-Time Systems. Information and Computation 111(2) (1994) 193–244
13. Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Compact data structures and
state-space reduction for model-checking real-time systems. Real-Time Syst. 25(2-
3) (2003) 255–275
14. Pavese, E.: A new data structure based on BDDs for the model check-
ing of timed systems. Degree thesis, Departamento de Computación, Fac-
ultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires (2006)
(http://lafhis.dc.uba.ar/~epavese/tesis_pavese.ps.gz).
15. Behrmann, G., Bouyer, P., Larsen, K., Pelnek, R.: Lower and upper bounds in zone
based abstractions of timed automata. In: Proceedings of the 10th International
Conference on Tools and Algorithms for Construction and Analysis of Systems
(TACAS’04). Volume 2988 of LNCS., Springer Verlag (2004) 312–326
16. Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press. Cam-
bridge, Massachusetts (1999)
17. Braberman, V., Olivero, A., Schapachnik, F.: Issues in Distributed Model-Checking
of Timed Automata: building zeus. International Journal of Software Tools for
Technology Transfer 7 (2005) 4–18
18. Braberman, V., Garbervetsky, D., Olivero, A.: ObsSlice: A timed automata slicer
based on observers. In: Proc. of the 16th Intl. Conf. CAV ’04. LNCS, Springer
Verlag (2004)
19. Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: An implemen-
tation of three algorithms for timing verification based on automata emptiness. In:
Proceedings of the 13th IEEE Real-time Systems Symposium, Phoenix, Arizona
(1992) 157–166
20. Braberman, V.: Modeling and Checking Real-Time Systems Designs. Ph d. the-
sis, Departamento de Computación, Facultad de Ciencias Exactas y Naturales,
Universidad de Buenos Aires (2000)