**Timed Automata: Semantics, Algorithms and Tools**

Johan Bengtsson and Wang Yi Uppsala University Email: {johanb,yi}@it.uu.se

**Abstract. This chapter is to provide a tutorial and pointers to results and related**
work on timed automata with a focus on semantical and algorithmic aspects of
verification tools. We present the concrete and abstract semantics of timed au-
tomata (based on transition rules, regions and zones), decision problems, and
algorithms for verification. A detailed description on DBM (Difference Bound
Matrices) is included, which is the central data structure behind several verifica-
tion tools for timed systems. As an example, we give a brief introduction to the
tool UPPAAL.

**1** **Introduction**

Timed automata is a theory for modeling and verification of real time systems. Exam-
ples of other formalisms with the same purpose, are timed Petri Nets, timed process
algebras, and real time logics [BD91,RR88,Yi91,NS94,AH94,Cha99]. Following the
work of Alur and Dill [AD90,AD94], several model checkers have been developed with
*timed automata being the core of their input languages e.g. [Yov97,LPY97]. It is fair*
to say that they have been the driving force for the application and development of the
theory. The goal of this chapter is to provide a tutorial on timed automata with a focus
on the semantics and algorithms based on which these tools are developed.

In the original theory of timed automata [AD90,AD94], a timed automaton is a finite- state Büchi automaton extended with a set of real-valued variables modeling clocks.

Constraints on the clock variables are used to restrict the behavior of an automaton, and
Büchi accepting conditions are used to enforce progress properties. A simplified ver-
*sion, namely Timed Safety Automata is introduced in [HNSY94] to specify progress*
properties using local invariant conditions. Due to its simplicity, Timed Safety Au-
*tomata has been adopted in several verification tools for timed automata e.g. U*PPAAL

[LPY97] and Kronos [Yov97]. In this presentation, we shall focus on Timed Safety Au-
*tomata, and following the literature, refer them as Timed Automata or simply automata*
when it is understood from the context.

The rest of the chapter is organized as follows: In the next section, we describe the syn- tax and operational semantics of timed automata. The section also addresses decision problems relevant to automatic verification. In the literature, the decidability and unde- cidability of such problems are often considered to be the fundamental properties of a computation model. Section 3 presents the abstract version of the operational semantics based on regions and zones. Section 4 describes the data structure DBM (Difference

Bound Matrices) for the efficient representation and manipulation of zones, and opera- tions on zones, needed for symbolic verification. Section 5 gives a brief introduction to the verification tool UPPAAL. Finally, as an appendix, we list the pseudo-code for the presented DBM algorithms.

**2** **Timed Automata**

A timed automaton is essentially a finite automaton (that is a graph containing a finite
set of nodes or locations and a finite set of labeled edges) extended with real-valued
variables. Such an automaton may be considered as an abstract model of a timed sys-
tem. The variables model the logical clocks in the system, that are initialized with zero
when the system is started, and then increase synchronously with the same rate. Clock
*constraints i.e. guards on edges are used to restrict the behavior of the automaton. A*
transition represented by an edge can be taken when the clocks values satisfy the guard
labeled on the edge. Clocks may be reset to zero when a transition is taken.

*The first example Fig. 1(a) is an example timed automaton. The timing behavior of*
the automaton is controlled by two clocks and^{}. The clock is used to control the
**self-loop in the location loop. The single transition of the loop may occur when** ^{}.
Clock^{}**controls the execution of the entire automaton. The automaton may leave start**
at any time point when^{}**is in the interval between 10 and 20; it can go from loop to**
**end when**^{}*is between 40 and 50, etc.*

**start**

**loop**

**end**
x:=0, y:=0
10<=y<=20
enter

40<=y<=50

y:=0 leave x==1

x:=0

work 10<=y<=20

y:=0

**start**
**y<=20**

**loop**
**y<=50**

**end**
**y<=20**
x:=0, y:=0

10<=y enter

40<=y

y:=0 leave x==1

x:=0

work 10<=y

y:=0

(a) (b)

**Fig. 1. Timed Automata and Location Invariants**

*Timed Büchi Automata A guard on an edge of an automaton is only an enabling con-*
dition of the transition represented by the edge; but it can not force the transition to
be taken. For instance, the example automaton may stay forever in any location, just

idling. In the initial work by Alur and Dill [AD90], the problem is solved by introduc-
ing Büchi-acceptance conditions; a subset of the locations in the automaton are marked
as accepting, and only those executions passing through an accepting location infinitely
often are considered valid behaviors of the automaton. As an example, consider again
**the automaton in Fig. 1(a) and assume that end is marked as accepting. This implies**
**that all executions of the automaton must visit end infinitely many times. This imposes**
**implicit conditions on start and loop. The location start must be left when the value**
of^{}**is at most 20, otherwise the automaton will get stuck in start and never be able to**
**enter end. Likewise, the automaton must leave loop when**^{}is at most 50 to be able to
**enter end.**

*Timed Safety Automata A more intuitive notion of progress is introduced in timed safety*
*automata [HNSY94]. Instead of accepting conditions, in timed safety automata, loca-*
*tions may be put local timing constraints called location invariants. An automaton may*
remain in a location as long as the clocks values satisfy the invariant condition of the
location. For example, consider the timed safety automaton in Fig. 1(b), which corre-
**sponds to the Büchi automaton in Fig. 1(a) with end marked as an accepting location.**

**The invariant specifies a local condition that start and end must be left when**^{} is at
**most 20 and loop must be left when**^{} is at most 50. This gives a local view of the
timing behavior of the automaton in each location.

In the rest of this chapter, we shall focus on timed safety automata and refer such au-
*tomata as Timed Automata or simply automata without confusion.*

**2.1** **Formal Syntax**

Assume a finite set of real-valued variables ranged over by ^{}^{}*etc.standing for clocks*
and a finite alphabet^{}ranged over by^{}^{}*etc.standing for actions.*

*Clock Constraints A clock constraint is a conjunctive formula of atomic constraints of*
the form ^{}^{}or ^{}^{} ^{} ^{}for ^{}^{} ^{} ^{}^{} ^{}^{} ^{}^{}^{}and^{} ^{} ^{}. Clock
constraints will be used as guards for timed automata. We use^{} ^{}to denote the set of
clock constraints, ranged over by^{ }and also by^{}later.

**Definition 1 (Timed Automaton) A timed automaton**^{ }*is a tuple*^{ }^{} ^{}^{
}^{}^{}*where*
**–** ^{} *is a finite set of locations (or nodes),*

**–** ^{} ^{}^{}*is the initial location,*

**–** ^{
}^{}^{}^{
}^{} ^{}^{
}^{}^{
}^{} ^{
}^{} *is the set of edges and*
**–** ^{} ^{}^{}^{}^{}^{} ^{}*assigns invariants to locations*
*We shall write*^{}^{}^{}^{}^{}^{}^{}^{}*when*^{ }^{ }^{}^{}^{}^{}^{}^{}^{
}*.*

*As in verification tools e.g. U*PPAAL*[LPY97], we restrict location invariants to con-*
*straints that are downwards closed, in the form:* ^{}^{}*or* ^{}^{}*where*^{}*is a natural*
*number.*

**Concurrency and Communication To model concurrent systems, timed automata**
can be extended with parallel composition. In process algebras, various parallel com-
position operators have been proposed to model different aspects of concurrency (see
*e.g. CCS and CSP [Mil89,Hoa78]). These algebraic operators can be adopted in timed*
automata. In the UPPAALmodeling language [LPY97], the CCS parallel composition
operator [Mil89] is used, which allows interleaving of actions as well as hand-shake
synchronization. The precise definition of this operator is given in Section 5.

Essentially the parallel composition of a set of automata is the product of the automata.

Building the product automaton is an entirely syntactical but computationally expensive operation. In UPPAAL, the product automaton is computed on-the-fly during verifica- tion.

**2.2** **Operational Semantics**

The semantics of a timed automaton is defined as a transition system where a state or configuration consists of the current location and the current values of clocks. There are two types of transitions between states. The automaton may either delay for some time (a delay transition), or follow an enabled edge (an action transition).

*To keep track of the changes of clock values, we use functions known as clock assign-*
*ments mapping* to the non-negative reals . Let^{}^{}denote such functions, and use

to mean that the clock values denoted by^{}satisfy the guard^{ }. For^{}^{} , let

denote the clock assignment that maps all ^{} to^{} ^{}^{}^{}, and for^{}^{} , let

denote the clock assignment that maps all clocks in^{}to 0 and agree with^{}
for the other clocks in ^{}^{}.

**Definition 2 (Operational Semantics) The semantics of a timed automaton is a tran-***sition system (also known as a timed transition system) where states are pairs*^{}^{}*,*
*and transitions are defined by the rules:*

**–** ^{}^{}^{}^{}^{} ^{}^{}^{}^{}*if*^{}^{}^{}^{}*and*^{}^{}^{}^{}^{}*for a non-negative real*^{}^{}

**–** ^{}^{}^{}^{}^{} ^{}^{}^{}^{}^{}^{}*if*^{}^{}^{}^{}^{}^{}^{}^{}^{}^{}^{}^{ }^{}^{} ^{}^{}^{ }*and*^{}^{}^{}^{}^{}^{}^{}

**2.3** **Verification Problems**

The operational semantics is the basis for verification of timed automata. In the follow- ing, we formalize decision problems in timed automata based on transition systems.

**Language Inclusion A timed action is a pair**^{}^{}, where^{}^{}^{}is an action taken by
an automaton^{ }after^{}^{} time units since^{ }has been started. The absolute time^{}
*is called a time-stamp of the action*^{}*. A timed trace is a (possibly infinite) sequence of*
timed actions^{} ^{}

where^{}

for all^{}^{}^{}.

**Definition 3 A run of a timed automaton**^{ } ^{}^{} ^{}^{
}^{}^{}*with initial state*^{} ^{}^{} ^{}
*over a timed trace*^{} ^{}

*is a sequence of transitions:*

½

½

¾

¾

¿

¿

*satisfying the condition*^{}

*for all*^{}^{}^{}*.*

*The timed language*^{ }*is the set of all timed traces*^{}*for which there exists a run of*

*over*^{}*.*

*Undecidability The negative result on timed automata as a computation model is that*
*the language inclusion checking problem i.e. to check*^{ } ^{} ^{}is undecidable
[AD94,ACH94]. Unlike finite state automata, timed automata is not determinizable in
general. Timed automata can not be complemented either, that is, the complement of
the timed language of a timed automaton may not be described as a timed automaton.

The inclusion checking problem will be decidable if^{} in checking^{ } ^{} ^{}is
restricted to the deterministic class of timed automata. Research effort has been made
*to characterize interesting classes of determinizable timed systems e.g. event-clock au-*
tomata [AFH99] and timed communicating sequential processes [YJ94]. Essentially,
the undecidability of language inclusion problem is due to the arbitrary clock reset. If
all the edges labeled with the same action symbol in a timed automaton, are also labeled
with the same set of clocks to reset, the automaton will be determinizable. This covers
the class of event-clock automata [AFH99].

We may abstract away from the time-stamps appearing in timed traces and define the
*untimed language*^{}

as the set of all traces in the form^{}

for which
there exists a timed trace^{} ^{}

in the timed language of^{ }.
The inclusion checking problem for untimed languages is decidable. This is one of the
classic results for timed automata [AD94].

**Bisimulation Another classic result on timed systems is the decidability of timed**
bisimulation [Cer92]. Timed bisimulation is introduced for timed process algebras [Yi91].

However, it can be easily extended to timed automata.

**Definition 4 A bisimulation**^{}*over the states of timed transition systems and the al-*
*phabet*^{}^{} *, is a symmetrical binary relation satisfying the following condition:*

*for all*^{}

*, if*^{}

*for some*^{} ^{} ^{}^{} *and*^{}^{}*, then*^{}

*and*

*for some*^{}^{}*.*

*Two automata are timed bisimilar iff there is a bisimulation containing the initial states*
*of the automata.*

Intuitively, two automata are timed bisimilar iff they perform the same action transition at the same time and reach bisimilar states. In [Cer92], it is shown that timed bisimula- tion is decidable.

We may abstract away from timing information to establish bisimulation between au-
tomata based actions performed only. This is captured by the notion of untimed bisim-
ulation. We define^{}^{}^{}^{} ^{}^{} if^{}^{}^{}^{} ^{}^{} for some real number^{}. Untimed bisimulation is
defined by by replacing the alphabet with^{}^{}^{}in Definition 4. As timed bisimula-
tion, untimed bisimulation is decidable [LW97].

**Reachability Analysis Perhaps, the most useful question to ask about a timed automa-**
ton is the reachability of a given final state or a set of final states. Such final states may
be used to characterize safety properties of a system.

**Definition 5 We shall write**^{}^{}^{}^{}^{}^{}^{}^{}^{}*if*^{}^{}^{}^{}^{} ^{}^{}^{}^{}^{}^{}*for some*^{}^{}^{}^{} *.*
*For an automaton with initial state* ^{} ^{}^{} ^{}*,* ^{}^{}*, is reachable iff* ^{ } ^{}^{} ^{ }^{}^{}^{}*.*
*More generally, given a constraint*^{} ^{} ^{} ^{}*we say that the configuration*^{}^{}*is*
*reachable if*^{ }^{}*is reachable for some*^{}*satisfying*^{}*.*

The notion of reachability is more expressive than it appears to be. We may specify invariant properties using the negation of reachability properties, and bounded liveness properties using clock constraints in combination with local properties on locations [LPY01] (see Section 5 for an example).

The reachability problem is decidable. In fact, one of the major advances in verification
of timed systems is the symbolic technique [Dil89,YL93,HNSY94,YPD94,LPY95], de-
veloped in connection with verification tools. It adopts the idea from symbolic model
checking for untimed systems, which uses boolean formulas to represent sets of states
and operations on formulas to represent sets of state transitions. It is proven that the
infinite state-space of timed automata can be finitely partitioned into symbolic states
*using clock constraints known as zones [Bel57,Dil89]. A detailed description on this is*
given in Section 3 and 4.

**3** **Symbolic Semantics and Verification**

As clocks are real-valued, the transition system of a timed automaton is infinite, which is not an adequate model for automated verification.

**3.1** **Regions, Zones and Symbolic Semantics**

The foundation for the decidability results in timed automata is based on the notion of
*region equivalence over clock assignments [AD94,ACD93].*

**Definition 6 (Region Equivalence) Let**^{}*be a function, called a clock ceiling, map-*
*ping each clock* ^{} *to a natural number*^{} ^{}*(i.e. the ceiling of* *). For a real*
*number*^{}*, let*^{}*denote the fractional part of*^{}*, and*^{}*denote its integer part. Two*
*clock assignments*^{}^{}*are region-equivalent, denoted*^{}^{}^{
}

*, iff*

*1. for all , either*^{} ^{} ^{} ^{ }*or both*^{} ^{}^{}^{} ^{}*and*^{} ^{}^{}^{} ^{}*,*
*2. for all , if*^{} ^{}^{}^{} ^{}*then*^{} ^{} ^{}*iff*^{} ^{} ^{}*and*

*3. for all* ^{}^{} *if*^{} ^{}^{}^{} ^{}*and*^{}^{}^{}*then*^{} ^{} ^{}^{}*iff*^{} ^{} ^{}

Note that the region equivalence is indexed with a clock ceiling^{}. When the clock ceil-
ing is given by the maximal clock constants of a timed automaton under consideration,
we shall omit the index and write ^{}^{
} instead. An equivalence class^{ }induced by ^{}^{
} is
*called a region, where*^{ }denotes the set of clock assignments region-equivalent to^{}.
The basis for a finite partitioning of the state-space of a timed automaton is the follow-
ing facts. First, for a fixed number of clocks each of which has a maximal constant, the
number of regions is finite. Second,^{}^{}^{
} ^{}implies^{}^{}and^{}^{}are bisimilar w.r.t.

the untimed bisimulation for any locaton^{}of a timed automaton. We use the equivalence
classes induced by the untimed bisimulation as symbolic (or abstract) states to construct
*a finite-state model called the region graph or region automaton of the original timed*
automaton. The transition relation between symbolic states is defined as follows:

y

x
**Fig. 2. Regions for a System with Two Clocks**

**–** ^{}^{ }^{}^{}^{ }if^{ }^{}^{}^{}^{} ^{ }^{}for a positive real number^{}and
**–** ^{}^{ }^{}^{}^{}^{}^{ }if^{}^{}^{}^{}^{} ^{}^{}^{}^{}for an action^{}.

Note that the transition relation^{}is finite. Thus the region graph for a timed automaton
is finite. Several verification problems such as reachability analysis, untimed language
inclusion, language emptiness [AD94] as well as timed bisimulation [Cer92] can be
solved by techniques based on the region construction.

However, the problem with region graphs is the potential explosion in the number of re- gions. In fact, it is exponential in the number of clocks as well as the maximal constants

appearing in the guards of an automaton. As an example, consider Fig. 2. The figure
shows the possible regions in each location of an automaton with two clocks and^{}.
The largest number compared to is 3, and the largest number compared to^{}is 2. In
the figure, all corner points (intersections), line segments, and open areas are regions.

Thus, the number of possible regions in each location of this example is 60.

A more efficient representation of the state-space for timed automata is based on the
*notion of zone and zone-graphs [Dil89,HNSY92,YL93,YPD94,HNSY94]. In a zone*
graph, instead of regions, zones are used to denote symbolic states. This in practice
gives a coarser and thus more compact representation of the state-space. The basic
operations and algorithms for zones to construct zone-graphs are described in Section 4.

As an example, a timed automaton and the corresponding zone graph (or reachability graph) is shown in Fig. 3. We note that for this automaton the zone graph has only 8 states. The region-graph for the same example has over 50 states.

**off**

**dim**

**bright**
press?

x:=0

x<=10 press?

x>10 press?

press?

**off**^{}^{} ^{}

**off**^{}^{}^{} ^{}

**off**^{}^{}^{} ^{}

**dim**^{}^{}^{} ^{}

**dim**^{}^{}^{} ^{}

**bright**^{}^{} ^{}

**bright**^{}^{}^{ }^{} ^{}

**bright**^{}^{}^{} ^{}

**Fig. 3. A Timed Automaton and its Zone Graph**

*A zone is a clock constraint. Strictly speaking, a zone is the solution set of a clock*
constraint, that is the maximal set of clock assignments satisfying the constraint. It
is well-known that such sets can be efficiently represented and stored in memory as
*DBMs (Difference Bound Matrices) [Bel57]. For a clock constraint*^{}, let^{ }denote
the maximal set of clock assignments satisfying^{}. In the following, to save notation,
we shall use^{}to stand for^{ }without confusion. Then^{} ^{}denotes the set of zones.

A symbolic state of a timed automaton is a pair^{}^{}representing a set of states of the
automaton, where^{}is a location and^{} is a zone. A symbolic transition describes all
the possible concrete transitions from the set of states.

**Definition 7 Let**^{}*be a zone and*^{}*a set of clocks. We define*^{}^{} ^{}^{}^{}^{}^{}^{}^{}

*and*^{} ^{} ^{}^{ }^{}^{}^{}^{}*. Let* *denote the symbolic transition relation*
*over symbolic states defined by the following rules:*

**–** ^{}^{} ^{}^{}^{}^{}^{}^{}

**–** ^{}^{} ^{ }^{}^{}^{}^{}^{ }^{}^{}^{}^{}*if*^{}^{}^{}^{}^{}^{}^{}^{}

We shall study these operations in details in Section 4 where^{}^{}is written as up^{}

and^{}as reset^{}^{}^{} ^{}. It will be shown that the set of zones^{} ^{}is closed un-
der these operations, in the sense that the result of the operations is also a zone. Another
important property of zones is that a zone has a canonical form. A zone^{}*is closed un-*
*der entailment or just closed for short, if no constraint in*^{}can be strengthened without
reducing the solution set. The canonicity of zones means that for each zone^{}^{}^{} ^{},
there is a unique zone^{}^{}^{}^{} ^{}such that^{}and^{}^{}have exactly the same solution set
and^{}^{} is closed under entailment. Section 4 describes how to compute and represent
the canonical form of a zone. It is the key structure for the efficient implementation of
state-space exploration using the symbolic semantics.

The symbolic semantics corresponds closely to the operational semantics in the sense
that^{}^{} ^{}^{}^{}^{}^{}^{}implies for all^{}^{} ^{}^{}^{},^{}^{}^{}^{}^{}^{}^{}^{}^{}for some^{}^{}^{}. More
generally, the symbolic semantics is a correct and full characterization of the operational
semantics given in Definition 2.

**Theorem 1 Assume a timed automaton with initial state**^{ } ^{}^{} ^{}*.*
*1. (soundness)*^{} ^{}^{} ^{} ^{}^{}

*implies*^{} ^{}^{} ^{}^{}^{}^{}

*for all*^{}

*.*
*2. (Completeness)*^{ } ^{}^{} ^{}^{}^{} ^{}

*implies*^{} ^{}^{} ^{} ^{} ^{}

*for some*^{}

*such that*^{}

The soundness means that if the initial symbolic state^{} ^{}^{} ^{}may lead to a set of
final states^{ }

according to , all the final states should be reachable according to the concrete operational semantics. The completeness means that if a state is reachable according to the concrete operational semantics, it should be possible to conclude this using the symbolic transition relation.

Unfortunately, the relation is infinite, and thus the zone-graph of a timed automaton
may be infinite, which can be a problem to guarantee termination in a verification pro-
cedure. As an example, consider the automaton in Fig. 4. The value of clock^{} drifts
away unboundedly, inducing an infinite zone-graph.

*The solution is to transform (i.e. normalize) zones that may contain arbitrarily large*
constants to their representatives in a class of zones whose constants are bounded by
*fixed constants e.g. the maximal clock constants appearing in the automaton, using an*
abstraction technique similar to the widening operation [Hal93]. The intuition is that
once the value of a clock is larger than the maximal constant in the automaton, it is no
longer important to know the precise value of the clock, but only the fact that it is above
the constant.

**3.2** **Zone-Normalization for Automata without Difference Constraints**

In the original theory of timed automata [AD94], difference constraints are not allowed to appear in the guards. Such automata (whose guards contain only atomic constraints in

**start**

**loop**
**x<=10**

**end**
x:=0,
y:=0

y>=20 x:=0, y:=0

x==10 x:=0

**start**^{}^{}^{}^{}

**loop**^{}^{}^{ }^{} ^{}^{}^{}^{}

**loop**^{}^{ }^{} ^{}^{}^{ }^{} ^{}^{}^{}^{}^{}^{} ^{}

**loop**^{}^{}^{ }^{} ^{}^{}^{ }^{} ^{}^{}^{}^{}^{}^{} ^{}

**loop**^{}^{ }^{} ^{}^{}^{ }^{} ^{}^{}^{}^{}^{}^{} ^{}

**end**^{}^{}^{}^{}

.. .

**Fig. 4. A Timed Automaton with an Infinite Zone-Graph**

the form ^{}^{}) are known as diagonal-free automata in the literature in [BDGP98]. For
diagonal-free automata, a well-studied zone-normalization procedure is the so-called

*-normalization operation on zones [Rok93,Pet99]. It is implemented in several verifi-*
*cation tools for timed automata e.g. U*PPAALto guarantee termination.

**Definition 8 (**^{}**-Normalization) Let**^{}*be a zone and*^{}*a clock ceiling. The semantics*
*of the*^{}*-normalization operation on zones is defined as follows:*

*norm*

Note that the normalization operation is indexed by a clock ceiling^{}. According to
[Rok93,Pet99],norm

can be computed from the canonical representation of^{}by
1. removing all constraints of the form ^{}^{}, ^{}^{}, ^{}^{} ^{}^{}and ^{}^{} ^{}^{}

where^{}^{}^{} ^{},

2. replacing all constraints of the form ^{}^{}, ^{}^{}, ^{}^{} ^{}^{}and ^{}^{}^{}^{}
where^{}^{}^{} ^{}with ^{}^{} ^{}and ^{}^{}^{}^{} ^{}respectively.

Let^{ }denote the resulted zone by the above transformation. This is exactly the nor-
malized zone as defined in Definition 8, that is,^{ }

As an example, the normalized zone-graph of the automaton in Fig. 4 is shown in Fig. 5 where the clock ceiling is given by the maximal clock constants appearing in the automaton.

Note that for a fixed number of clocks with a clock ceiling^{}, there can be only finitely
many normalized zones. The intuition is that if the constants allowed to use are bounded,
one can write down only finitely many clock constraints. This gives rise to a finite char-
acterization for^{}.

**Definition 9** ^{ }^{ }

*norm*

*if*^{}^{} ^{}^{}^{}^{}^{}^{}*.*

**start**^{}^{}^{}^{}

**loop**^{}^{}^{ }^{} ^{}^{}^{}^{ }

**loop**^{}^{ }^{} ^{}^{}^{ }^{} ^{}^{}^{}^{}^{}^{} ^{}

**loop**^{}^{}^{ }^{} ^{}^{}^{}^{}^{}^{} ^{}

**loop**^{}^{ }^{} ^{}^{}^{}^{} ^{}^{}^{}^{}^{}^{} ^{}

**end**^{}^{}^{ }

**Fig. 5. Normalized Zone Graph for the Automaton in Fig. 4**

For the class of diagonal-free timed automata is sound, complete and finite in the following sense.

**Theorem 2 Assume a timed automaton with initial state**^{} ^{}^{} ^{}*, whose maximal clock*
*constants are bounded by a clock ceiling*^{}*. Assume that the automaton has no guards*
*containing difference constraints in the form of* ^{}^{}^{}^{}*.*

*1. (soundness)*^{ } ^{}^{} ^{} ^{}

*implies*^{ } ^{}^{} ^{}^{}^{} ^{ }

*for all*^{}

*such that*^{}

*for all .*
*2. (Completeness)*^{ } ^{}^{} ^{}^{}^{}^{}

*with*^{}

*for all , implies*^{} ^{}^{} ^{}

*for some*^{}*such that*^{}

*3. (Finiteness) The transition relation* *is finite.*

Unfortunately the soundness will not hold for timed automata whose guards contain
difference constraints. We demonstrate this by an example. Consider the automaton
shown in Fig. 6. The final location of the automaton is not reachable according to the
operational semantics. This is because in location^{}, the clock zone is ( ^{}^{}^{}^{}and

) and the guard on the outgoing edge is ^{} ^{}^{} ^{}^{}^{}^{}which is equivalent
to ^{} ^{}^{}^{} ^{}^{} ^{}^{}^{} ^{}^{}^{}^{}. Obviously the zone at^{}can never enable the
guard, and thus the last transition will never be possible. However, because the maximal
constants for clock is^{}(and^{}for^{}), the zone in location^{}: ^{}^{}^{}^{}^{} ^{}^{}will
be normalized to ^{}^{} ^{}^{}^{} ^{}^{}by the maximal constant^{}for , which enables
the guard ^{} ^{}^{}^{} ^{}^{}^{}^{}and thus the symbolic reachability analysis based on
the above normalization algorithm would incorrectly conclude that the last location is
reachable.

The zones in canonical forms, generated in exploring the state-space of the counter example are given in Fig. 7. The implicit constraints that all clocks are non-negative are not shown.

**S0** **S1** **S2** **S3**

z:=0

y>2 y:=0

x<z+1, z<y+1

**Fig. 6. A counter example**

¼

¼

¼

¼

(a) Zones without normalization (b) Zones normalized with^{}-normalization
**Fig. 7. Zones for the counter example in Fig. 6**

Note that at^{} and^{}, the normalized and un-normalized zones are identical. The
problem is at^{}where the intersection of the guard (on the only outgoing edge) with
the un-normalized zone is empty and non-empty with the normalized zone.

**3.3** **Zone-Normalization for Automata with Difference Constraints**

Our definition of timed automata (Definition 1) allows any clock constraint to appear in
a guard, which may be a difference constraint in the form of ^{}^{}^{}^{}. Such automata
*are indeed needed in many applications e.g. to model scheduling problems [FPY02].*

It is shown that an automaton containing difference constraints can be transformed to an equivalent diagonal-free automaton [BDGP98]. However, the transformation is not applicable since it is based on the region construction. Besides, it is impractical to im- plement such an approach in a tool. Since the transformation modifies the model before analysis, it is difficult to trace debugging information provided by the tool back to the original model.

In [Ben02,BY03], a refined normalization algorithm is presented for automata that may have guards containing difference constraints. The algorithm transforms DBMs accord- ing to not only the maximal constants of clocks but also difference constraints appearing in the automaton under consideration. Note that the difference constraints correspond to the diagonal lines which split the entire space of clock assignments. A finer partitioning is needed.

We present the semantical characterization for the refined normalization operation based on a refined version of the region equivalence from Definition 6.

**Definition 10 (Normalization Using Difference Constraints) Let**^{}*stand for a finite*
*set of difference constraints of the form* ^{}^{}^{}*for* ^{}^{}^{} *,*^{}^{}^{} ^{}^{}^{}*and*

*, and*^{}*for a clock ceiling. Two clock assignments*^{}^{}*are equivalent, denoted*

*if the following holds:*

**–** ^{}^{}^{
}

*and*

**– for all**^{ }^{}^{}*,*^{}^{}^{ }*iff*^{}^{}^{ }*.*

*The semantics of the refined*^{}*-normalization operation on zones is defined as follows:*

*norm*

Note that the refined region equivalence is indexed by both a clock ceiling^{}and a finite
set of difference constraints^{}, and so is the normalization operation.

Since the number of regions induced by ^{}^{
} is finite and there are only finitely many
constraints in^{}, ^{}^{
} induces finitely many equivalence classes. Thus for any given
zone^{},norm

is well-defined in the sense that it contains only a finite set of
equivalence classes though the set may not be a convex zone, and it can be computed
effectively according to the refined regions. In general,norm^{ }^{}is a non-convex
zone, which can be implemented as the union of a finite list of convex zones. The next
section will show how to compute this efficiently.

The refined zone-normalization gives rise to a finite characterization for^{}.
**Definition 11** ^{}^{}

*norm*^{ }^{}^{}^{ }*if*^{}^{ } ^{}^{}^{}^{}^{}^{}*.*
The following states the correctness and finiteness of .

**Theorem 3 Assume a timed automaton with initial state**^{} ^{}^{} ^{}*, whose maximal clock*
*constants are bounded by a clock ceiling*^{}*, and whose guards contain only a finite set*
*of difference constraints denoted*^{}*.*

*1. (soundness)*^{} ^{}^{} ^{}^{}

*implies*^{ } ^{}^{} ^{}^{}^{}^{ }

*for all*^{}

*such that*^{}

*for all .*
*2. (Completeness)*^{ } ^{}^{} ^{}^{}^{}^{ }

*with*^{}

*for all* *implies*^{} ^{}^{} ^{}

*for some*^{}*such that*^{}

*3. (Finiteness) The transition relation* *is finite.*

**3.4** **Symbolic Reachability Analysis**

*Model-checking concerns two types of properties liveness and safety. The essential*
algorithm of checking liveness properties is loop detection, which is computationally
expensive. The main effort on verification of timed systems has been put on safety
properties that can be checked using reachability analysis by traversing the state-space
of timed automata.

**Algorithm 1 Reachability analysis**
PASSED^{}^{}WAIT^{}^{} ^{}^{} ^{}

**while W**AIT^{}^{}**do**
take^{ }^{}from WAIT

**if**^{}^{}^{} ^{}^{}^{ }^{ } ^{}^{}**then return “YES”**

**if**^{}^{}^{}^{¼}for all^{ }^{}^{¼}^{}^{}PASSED**then**
add^{ }^{}to PASSED

**for all**^{}^{¼}^{}^{}^{¼}^{}such that^{ }^{} ^{}^{}^{¼}^{}^{}^{¼}^{}**do**
add^{}^{¼}^{}^{}^{¼}^{}to WAIT

**end for**
**end if**
**end while**
**return “NO”**

Reachability analysis can be used to check properties on states. It consists of two basic
steps, computing the state-space of an automaton under consideration, and searching for
states that satisfy or contradict given properties. The first step can either be performed
*prior to the search, or done on-the-fly during the search process. Computing the state-*
space on-the-fly has an obvious advantage over pre-computing, in that only the part of
the state-space needed to prove the property is generated. It should be noted though, that
even on-the-fly methods will generate the entire state-space to prove certain properties,
*e.g. invariant properties.*

Several model-checkers for timed systems are designed and optimized for reachability analysis based on the symbolic semantics and the zone-representation (see Section 4).

As an example, we present the core of the verification engine of UPPAAL(see Algo- rithm 1).

Assume a timed automaton^{ }*with a set of initial states and a set of final states (e.g.*

the bad states) characterized as^{} ^{}^{} ^{}and^{}

respectively. Assume that^{}is the
clock ceiling defined by the maximal constants appearing in^{ }and^{}, and^{}denotes
the set of difference constraints appearing in^{ }and^{}. Algorithm 1 can be used to
check if the initial states may evolve to any state whose location is^{} and whose clock
assignment satisfies^{}. It computes the normalized zone-graph of the automaton on-
the-fly, in search for symbolic states containing location^{}and zones intersecting with

.

The algorithm computes the transitive closure of step by step, and at each step,
checks if the reached zones intersect with^{}. From Theorem 2, it follows that the algo-
rithm will return with a correct answer. It is also guaranteed to terminate because

is finite. As mentioned earlier, for a given timed automaton with a fixed set of clocks
whose maximal constants are bounded by a clock ceiling^{}, and a fixed set of diago-
nal constraints contained in the guards, the number of all possible normalized zones is
bounded because a normalized zone can not contain arbitrarily large or arbitrarily small
constants. In fact the smallest possible zones are the refined regions. Thus the whole
state-space of a timed automaton can only be partitioned into finitely many symbolic
states and the worst case is the size of the region graph of the automaton, induced by
the refined region equivalence. Therefore, the algorithm is working on a finite structure
and it will terminate.

Algorithm 1 also highlights some of the issues in developing a model-checker for timed automata. Firstly, the representation and manipulation of states, primarily zones, is cru- cial to the performance of a model-checker. Note that in addition to the operations to compute the successors of a zone according to , the algorithm uses two more op- erations to check the emptiness of a zone as well as the inclusion between two zones.

Thus, designing efficient algorithms and data-structures for zones is a major issue in
developing a verification tool for timed automata, which is addressed in Section 4. Sec-
ondly, PASSEDholds all encountered states and its size puts a limit on the size of sys-
*tems we can verify. This raises the research challenges e.g. state compression [Ben02],*
state-space reduction [BJLY98] and approximate techniques [Bal96].

**4** **DBM: Algorithms and Data Structures**

The preceding section presents the key elements needed in symbolic reachability anal- ysis. Recall that the operations on zones are all defined in terms of sets of clock assign- ments. It is not clear how to compute the result of such an operation. In this section, we describe how to represent zones, compute the operations and check properties on zones.

Pseudo code for the operations is given in the appendix.

**4.1** **DBM basics**

Recall that a clock constraint over is a conjunction of atomic constraints of the form

and ^{}^{} ^{}^{}where ^{}^{} ^{} ,^{}^{}^{} ^{}^{}^{}and^{}^{}^{} ^{}. A zone
denoted by a clock constraint^{}is the maximal set of clock assignments satisfying^{}.
The most important property of zones is that they can can be represented as matrices
*i.e. DBMs (Difference Bound Matrices) [Bel57,Dil89], which have a canonical repre-*
sentation. In the following, we describe the basic structure and properties of DBMs.

To have a unified form for clock constraints we introduce a reference clock with the
constant value 0. Let ^{}^{} ^{}. Then any zone^{} ^{} ^{} ^{}can be rewritten as a
conjunction of constraints of the form ^{}^{}^{}^{}for ^{}^{}^{} ,^{}^{}^{}and^{}^{}^{}.