CHAPTER 7
VERIFICATION USING
TIMED AUTOMATA
Finite automata and temporal logics have been used extensively to formally ver-
ify qualitative properties of concurrent systems. The properties include deadlock- or
livelock-freedom, the eventual occurrence of an event, and the satisfaction of a pred-
icate. The need to reason with absolute time is unnecessary in these applications,
whose correctness depends only on the relative ordering of the associated events
and actions. These automata-theoretic and temporal logic techniques using finite-
state graphs are practical in a variety of verification problems in network protocols,
electronic circuits, and concurrent programs. More recently, several researchers have
extended these techniques to timed or real-time systems while retaining many of the
desirable features of their untimed counterparts.
In this chapter, we present two automata-theoretic techniques based on timed au-
tomata. The Lynch–Vaandrager approach [Lynch and Vaandrager, 1991; Heitmeyer
and Lynch, 1994] is more general and can handle finite and infinite state systems, but
it lacks an automatic verification mechanism. Its specification can be difficult to write
and understand, even for relatively small systems. The Alur–Dill approach [Alur,
Fix, and Henzinger, 1994] is less ambitious and is based on finite automata, but it of-
fers an automated tool for verification of desirable properties. Its dense-time model
can handle time values selected from the set of real numbers, whereas discrete-time
models such as those in Statecharts and Modecharts use only integer time values.
7.1 LYNCH–VAANDRAGER AUTOMATA-THEORETIC APPROACH
[Heitmeyer and Lynch, 1994] advocate the use of three specifications to formally
describe a real-time system. A specification consists of the description of one or more
187
Real-Time Systems: Scheduling, Analysis, and Verification. Albert M. K. Cheng
Copyright
¶
2002 John Wiley & Sons, Inc.
ISBN: 0-471-18406-3

A
s

is used instead of (s,π,s

) ∈ steps(A),whereA is a timed automaton. The
subscript A is often omitted when no ambiguity exists.
7.1.1 Timed Executions
Having defined the concept of a timed automaton, we next consider its behavior by
observing its execution from one point in time to another. A timed execution is a se-
quence of internal, visible, and time-passage actions, connected by their intervening
states, and augmented with the notion of trajectories for each time-passage action. A
trajectory indicates the state changes during time-passage steps. To formally define
a time execution, we first define the notion of a timed execution fragment.
Timed Execution: A timed execution fragment is a finite or infinite alternating se-
quence
α = ω
0
π
1
ω
1
π
2
ω
2
...,
LYNCH–VAANDRAGER AUTOMATA-THEORETIC APPROACH
189
where (1) each ω

define timed traces to represent the visible behavior of timed automata for solving
verification problems.
7.1.2 Timed Traces
A timed trace of any timed execution is the sequence of visible events that occur in
the timed execution, paired with their times of occurrence. This sequence has the
form
(π
1
, t
1
), (π
2
, t
2
), (π
3
, t
3
),...,
where the πs are non-time-passage actions and the ts are non-negative real-valued
times.
The notation ttrace(α) denotes the timed trace of the timed execution α. The timed
traces obtained from all the admissible timed executions of a timed automaton A
constitute the set attraces(A) of admissible timed traces of A.
Example. Consider a traffic semaphore with three light signals. Initially, there is no
light when the system is off. Once it is turned on at time 0, the event turn
green
makes the green light turn on. Next, the event turn
yellow, occurring 20 s later, turns
the green light off and then the yellow light on. Next, the turn


A
, s

B
) exists iff s
A
π
−→
A
s

A
if π ∈ acts(A),else
s
A
= s

A
,ands
B
π
−→
B
s

B
if π ∈ acts(B),elses
B
= s

and upper(C),where0≤ lower(C)<∞ and 0 < upper(C) ≤∞. In other words,
the lower bounds cannot be infinite and the upper bounds cannot be 0.
Since an MMT automaton can represent the time differences between certain ac-
tions in the modeled system or its component, the execution of the MMT automaton
shows the behavior of the modeled system over time. A timed execution of an MMT
automaton is an alternating sequence of the form s
0
,(π
1
, t
1
), s
1
,..., where the πs
can be input, output, or external actions. For each i , s
i
π
j+1
−→ s
j+1
must hold such that
the successive times are nondecreasing and are required to satisfy the specified lower
and upper time bound requirements.
The points at which the bounds for a class C begin to be measured are called
initial indices. Index i is defined as an initial index for a class C enabled in state s
i
,
and one of the following must hold: i = 0, C is not enabled in s
j−1
,orπ

induces a preorder on timed automata. The notation A ≤ B means that the set of
admissible timed traces of A is a subset of the set of admissible timed traces of B.
Example. The following MMT automaton describes the behavior of the pedals of
a simplified automobile, which has been specified in Statecharts in chapter 4. The
automobile can be in one of three states: stop, move, or slow. The inputs are ap-
ply
accelerator, apply brake,andapply hand brake. The nontrivial time bounds are
speed up: [0, t
speedup
], slow: [0, t
speedup
],andstop: [0, t
speedup
],wheret
speedup
, t
slow
,
and t
stop
are the upper bounds on the time for the car to speed up, slow, and stop, re-
spectively. The state components now, latest(speedup), latest(slow),andlatest(stop)
are also needed to add timing specifications to each state.
As in the Statecharts specification, the MMT automaton shows that (1) the tran-
sition from the state “stop” to the state “speed up” occurs when the accelerator is
applied; (2) the transition from the state “speedup” to the state “slow” occurs when
192
VERIFICATION USING TIMED AUTOMATA
the brake is applied; (3) the transition from the state “slow” to the state “speedup” oc-
curs when the accelerator is applied; and (4) the transitions from the states “speedup”


.status = to
slow
s

.latest(slow) = now + t
slow
s

.latest(speedup) =∞
s

.latest(stop) =∞
apply
hand brake
Precondition:
s.status ∈ speedup, slow
Effect:
s

.status = stop
s

.latest(stop) = now + t
stop
s

.latest(speedup) =∞
s


.status = stop
s

.latest(stop) =∞
7.1.6 Proving Time Bounds with Simulations
By including lower and upper time bounds on classes of the specification automaton,
the Larch Prover [Garland and Guttag, 1991] has been used to perform simple simu-
lation proofs for verifying timing properties of real-time and distributed systems.
7.2 ALUR–DILL AUTOMATA-THEORETIC APPROACH
To verify that an implementation of a system satisfies the specification of the system,
we first represent or encode the specification as a Buchi automaton A
S
and the imple-
mentation as a Buchi automaton A
I
. Then we check that the implementation meets
the specification iff L( A
I
) ⊆ L( A
S
), or check for the emptiness of L(A
I
)∩ L(A
S
)
C
;
that is, the intersection of the languages accepted by the implementation and the lan-
guages accepted by the complement of the specification (negation of the specifica-
tion) is empty.

observable events of the process and S is the set of the possible traces of the process.
Example. Consider a traffic semaphore with three light signals. Initially the green
light is on. Next, the green light turns off and then the yellow light turns on. Next, the
yellow light turns off and then the red light turns on. Next, the red light turns off and
then the green light turns on. This sequence is repeated infinitely often. By treating
green, yellow,andred as events, the only possible trace is:
ρ
P
={green}, {yellow}, {red}, {green}, {yellow}, {red},....
Keeping the notations simple by removing the set symbols, {}, this infinite sequence
is denoted as
green yellow red green yellow red ··· = (green yellow red)
ω
.
Process P is denoted by ({green,yellow,red},(green yellow red)
ω
).
Operations on processes exist that allow the definitions of complex processes by
combining simpler processes. These operations include projection and parallel com-
position.
7.2.2 Timed Traces
In the Alur–Dill model, a real-valued time is associated with each symbol in a word
to form a timed word.
Time Sequence: A time sequence
τ = τ
1
,τ
2
,τ
3

> 10.5) → (ρ
i
= timeout))}.
This concept of a time value associated to an event occurrence is similar to the
time value given by the occurrence function in real-time logic (chapter 6) and the
chronos variable in time ER nets (chapter 8). An occurrence function assigns a
time to the occurrence of an instance of an event. A variable chronos assigns a time-
stamp to the production of a token in a Petri net.
The following Untime operation is a projection of a timed trace (
ρ,τ) on the first
component, the sequence of event occurrences
ρ. This operation effectively deletes
the time values corresponding to the event occurrence symbols and is useful when
we do not need the absolute time values.
Untime Operation: Given a timed language L over an alphabet , Untime(L) is
the ω-language with words
ρ such that (ρ, τ) ∈ L for some time sequence τ .
Example. We apply the Untime operation to the above language L:
Untime(L) = ω-language with words containing only finitely many oks.
Timed Trace: A time trace over a set E of events is a pair (
ρ,τ) where ρ is a
(untimed) trace over the set E and
τ is a time sequence.
Timed Process: A timed process is a pair (E, L) where E is a (finite) set of events
and L is a set of timed traces over the set E.
Example. A timed process: Consider the climate control system example shown
in Figure 2.13 (chapter 2). To simply this example, we focus on the events in the
heater section. Assume that the initial instances of the events occur at fixed times and
that subsequent instances of the corresponding events occur at fixed time intervals.
The event turn

a timing-dependent climate control system. Now we introduce timing constraints to
the transitions of this automaton, yielding the timed automaton shown in Figure 7.1.
Two clocks (clock variables) are present in the transition table, c
1
and c
2
. Suppose
the automaton starts in state s
0
and reads the input symbol cold, then it takes the tran-
sition (indicating that the room temperature falls below 68
◦
F)andmovestostates
4
.
The clock c
1
is reset (set to 0 by the assignment c
1
:= 0) along this transition. In
S
1
S
3
S
2
(c < 10)?
1
(c < 2)?
1

for automatic air conditioning and heating system.