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. UPPAAL
[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 . Clockcontrols the execution of the entire automaton. The automaton may leave start at any time point whenis in the interval between 10 and 20; it can go from loop to end whenis 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 ofis at most 20, otherwise the automaton will get stuck in start and never be able to enter end. Likewise, the automaton must leave loop whenis 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 alphabetranged over byetc.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 bylater.
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. UPPAAL[LPY97], we restrict location invariants to con- straints that are downwards closed, in the form: or whereis 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 . Letdenote such functions, and use
to mean that the clock values denoted bysatisfy the guard . For , let
denote the clock assignment that maps all to , and for , let
denote the clock assignment that maps all clocks into 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, whereis 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 tracesfor 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 bisimulationover 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 within 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 somesatisfying .
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, letdenote the fractional part of, anddenote its integer part. Two clock assignmentsare 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 numberand – if for an action.
Note that the transition relationis 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 tois 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 useto 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 Letbe a zone anda 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 whereis written as up
andas 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 zoneis closed un- der entailment or just closed for short, if no constraint incan be strengthened without reducing the solution set. The canonicity of zones means that for each zone , there is a unique zone such thatandhave 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. UPPAALto guarantee termination.
Definition 8 ( -Normalization) Letbe 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 ofby 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 somesuch 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(andfor), the zone in location : will be normalized to by the maximal constantfor , 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) Letstand for a finite set of difference constraints of the form for , and
, and for a clock ceiling. Two clock assignmentsare 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 somesuch 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 PASSEDWAIT
while WAITdo take from WAIT
if then return “YES”
if¼for all ¼ PASSEDthen 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 , anddenotes 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 constraintis 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.
