
BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR94-1404
ENTRY:: 1994-03-17
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Symbolic Model Checking for Real-Time Systems
AUTHOR:: Henzinger, Thomas A.
AUTHOR:: Nicollin, Xavier
AUTHOR:: Sifakis, Joseph
AUTHOR:: Yovine, Sergio
DATE:: January 1994
PAGES:: 40
ABSTRACT::
We describe finite-state programs over real-numbered time in a guarded-command 
language with real-valued clocks or, equivalently, as finite automata with 
real-valued clocks. Model checking answers the question which states of a 
real-time program satisfy a branching-time specification (given in an 
extension of CTL with clock variables). We develop an algorithm that computes 
this set of states symbolically as a fixpoint of a functional on state 
predicates, without constructing the state space.

For this purpose, we introduce a $\mu$-calculus on computation trees over 
real-numbered time. Unfortunately, many standard program properties, such as 
response for all nonzero execution sequences (during which time diverges), 
cannot be characterized by fixpoints: we show that the expressiveness of the 
timed $\mu$-calculus is incomparable to the expressiveness of timed CTL. 
Fortunately, this result does not impair the symbolic verification of 
``implementable'' real-time programs-those whose safety constraints are 
machine-closed with respect to diverging time and whose fairness constraints 
are restricted to finite upper bounds on clock values. All timed CTL 
properties of such programs are shown to be computable as finitely 
approximable fixpoints in a simple decidable theory.
END:: CORNELLCS//TR94-1404
BODY::
Symbolic Model Checking for
Real-Time Systems*
Thomas A. Henzinger**
Xavier Nicollint
Joseph Sifakis?
Sergio Yovinet
TR 94-1404
January 1994
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
* This paper will appear in Information and Computation. A preliminary version
appeared in the proceedings of the Seventh Annual !EEE Symposium on Logic in
Computer Science (LICS 1992), pp. 394-406.
** Partially supported by the National Science Foundation under grant CCR-9200794
and by the United States Air Force Office of Scientific Research under contract
F49620-93-1 -0056.
* Partially supported by the Esprit Basic Research Action REACT.
Symbolic Model Checking for R?e?-tirne Systems*
Thomas A. Henzingert
Computer Science Department, Cornell University
Ithaca, NN' 14853, U.S.A.
Xavier Nicollint
Joseph Sifakis? Sergio Yovinet
VERIMAG, Miniparc-ZIRST rue Lavoisier
38330 Montbonnot Saint Martin, France
Abstract. We describe finite-state programs over real-numbered time in a guarded-
command language with real-valued clocks or, equivalently, as finite automata with
real-valued clocks. Model checking answers the question which states of a real-time
program satisfy a branching-time specification (given in an extension of CTL with clock
variables). We develop an algorithm that computes this set of states symbolically as a
fixpoint of a functional on state predicates, without constructing the state space.
For this purpose, we introduce a it-calculus on computation trees over real-numbered
time. Unfortunately, many standard program properties, such as response for all
nonzeno execution sequences (during which time diverges), cannot be characterized
by fixpoints: we show that the expressiveness of the timed it-calculus is incompara-
ble to the expressiveness of timed CTL. Fortunately, this result does not impair the
symbolic verification of "implementable" real-time programs those whose safety con-
straints are machine-closed with respect to diverging time and whose fairness constraints
are restricted to finite upper bounds on clock values. All timed CTL properties of such
programs are shown to be computable as finitely approximable fixpoints in a simple
decidable theory.
1 Introduction
Model checking is a powerful technique for tbe automatic verification of finite-state systems. Model-
checking algorithms determine the states that satisfy a modal formula by a graph-theoretic analysis
of the state space (Kripke structure) [QS8l, EC82, CES86]. The main practical limitation of
model-checking algorithms is caused by the size of the state graph, which grows exponentially with
the number of parallel components in a system. 0ne approach to confine this "state explosion
problem" relies on the symbolic (rather than enumerative) representation of sets of states and
computes the set that satisfies a formula as a fixpoint of a functional on state predicates. While the
*This paper will appear in Information and Computation. A preliminary version appeared in the proceedings of
the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992), pp. 394-406.
1Partially supported by the National Science Foundation under grant CCR-9200794 and by the United States Air
Force Office of Scientific Research under contract F49620-93-1-0056.
1Partially supported by the Esprit Basic Research Action REACT.
theoretical possibility of symbolic model checking by computing fixpoints was realized early [EC8o,
Sif82], the method has become practical only recently through the symbolic representation of state
sets by binary decision diagrams (BDDs) [Bry86]. BDDs were first used for verification purposes
by [CBM89] and for model checking by [BCM+92]. By now implementations of symbolic model-
checking techniques have reported spectacular successes, in particular in the area of hardware
verification [McM93].
The history of model checking has been considerably shorter in the case of real-time systems.
First researchers focused on discrete time (the integers), for which the untimed model-checking
methods can be readily extended [EMSS90, AH92b, Eme92]. New complexities arise if we insist that
for the compositional modeling of asynchronous systems, time should not be discretized [Alu9lj.
We consider dense time (the reals). A standard dense-time approach models a real-time system as
a transition relation together with a finite set of real-valued clocks that proceed at a uniform rate
and constrain the times at which transitions may occur [AD9O, Lew90, AFH9l, AH92a, NSY93j.
Only recently a graph-theoretic model-checking algorithm was found for these systems [ACD9oj.
Since the time component causes the state space to be infinite, the algorithm depends on a clever
construction of a finite quotient of the infinite state graph. The size of this "region graph" of
equivalence classes of states grows exponentially not only with the number of components in a
system but also with the largest time constant and the number of clocks that are used to specify
timing constraints. Thus the need for an alternative, "symbolic" approach to model checking, which
avoids the explicit construction of the region graph, is particularly pressing in the real-time case.
The main problem in devising such a method lies in the definition of a proper next-state relation
whose iteration allows us to compute all program properties we wish to consider. Since our time
domain is dense, the next-state relation must not force time to advance by more than an infinitesimal
amount. Its iteration, however, must force time to advance beyond any bound. This is because
upper-bound clock constraints may restrict the time that a system can spend in a particular set of
states, say, a loop. While the system may loop any finite number of times before the time bound
expires, it cannot do so infinitely often. In other words, every upper-bound constraint hides a
fairness condition.
Both requirements on the next-state relation seem and, in a precise technical sense we will
discuss, generally are contradictory. We show that this result has, fortunately, little relevance to
the verification of concrete real-time programs, including loops with upper bounds. We define the
class of divergence-safe systems, for which inevitability is equivalent to time-bounded inevitability:
for any event of a divergence-safe system there is a time bound such that if the event need not occur
before that bound, then it need not occur ever. The class of divergence-safe systems contains all
systems without fairness constraints other than those induced by constant upper bounds, which
it may be argued?is the only "implementable" notion of fairness. In the case of divergence-safe
systems, we show that we can settle for a next-state relation that does not force time to advance
ever. Such a relation allows us to compute possibility (??) and its dual, invariance (VE), directly.
Inevitability (V?) is reducible to time-bounded inevitability, which is but an invariance: time may
not progress beyond the upper bound of any event without the event occurring.
We have now informally sketched our course of action for computing bounded and unbounded
properties of real-time systems as fixpoints of functionals that are based on a next-state relation.
Formally, we introduce a timed ?-calculus, Tj, that is interpreted over timed computation trees.
We compare this fixpoint calculus to standard real-time extensions of branching-time logics and find
their expressive powers to be incomparable: the basic operator V? of branching-time logics cannot
be characterized by fixpoints in T?. However, as hinted above, we are able to give a translation
from CTL with clock variables (TCTL of [Alu9l]) to Tjt that agrees on a class of well-behaved
2
divergence-safe models. This translation forms the basis of a symbolic model-checking procedure.
We apply this theory to a concrete real-time programming language. Real-time systems are de-
fined in a guarded-command language with clocks, which is equivalent to timed safety automata
timed automata [AD90] without acceptance conditions. Every guarded-command real-time pro-
gram defines a divergence-safe real-time system for which all formulas of Tj and TCTL can be
verified symbolically by computing fixpoints (indeed, finitely approximable fixpoints) of appropri-
ate functionals. The practical computation of these functionals rests on our ability to express, for
any given program, the next-state relation symbolically. Indeed, the extraction of the next-state
relation from a program turns out to be rather nontrivial in the case that the program is not
nonzeno [AL92, Hen92] (not machine-closed with respect to the divergence of time); that is, if it
may prevent time from diverging. We show how a symbolic fixpoint approach can be used to test
if a guarded-command real-time program (or a timed safety automaton) is nonzeno and, if not, to
convert it into an equivalent nonzeno program.
We wish to conclude this introduction by pointing out that there is, of course, nothing ?magi-
cal" about symbolic methods. Timed model checking is intrinsically difficult (PSPACE-hard) and
already the known graph-theoretic algorithm on the exponential region graph is worst-case near-
optimal [ACD90]. In practice, however, the "intuitive complexity" [BCM+92] of the state space
is typically much smaller than the region graph. Only a symbolic method can exploit this phe-
nomenon, by representing unions of regions symbolically as state predicates. Our model-checking
algorithm constructs (the equivalent of) the full region graph but in extreme cases; typically it works
on a quotient of the region graph that depends on the formula being checked. Moreover, symbolic
methods can be applied to the verification of systems with an infinite state space even if it is not
known a priori that there is a suitable finite quotient of the state space. While our symbolic model-
checking procedure will fail to terminate if no such quotient exists, the procedure remains sound
and led recently to the verification of systems with very general state spaces [ACHH93, NOSY93].
The remainder of the paper is organized as follows. In the next section, we define our model
of real-time systems. Section 3 presents a guarded-command language and an automata-based
language for the description of real-time systems. In Section 4, we review the branching-time
logic TCTL and introduce the timed ?-calculus T?. Section 5 compares the expressive power of
both specification languages. The definition of TCTL-formulas as fixpoints leads, in Section 6, to
a symbolic model-checking algorithm for both T? and TCTL.
2 A Dense-time Model for Real-time Systems
We present a branching dense-time semantics for real-time systems. Our semantics integrates
elements from several models that have been proposed in the literature; we are particularly indebted
to the clocks of [AD9oj, the dense trees of [ACD90], the transition-delay dichotomy of [HMP9l]
and [NSY93], and the relative safety of [Hen92]
2.1 State trajectories
We model time as the nonnegative real numbers R+. The state of a system is determined by the
values of a finite set P of boolean variables (propositions), representing data and control, and by
the values of a finite set C of real-valued variables (clocks). The clocks allow the system to make
time-dependent decisions.
Definition 2.1 (state) A state a is an interpretation of all propositions and clocks; that is, a
assigns to each proposition p ? P a boolean value a(p) E ?true,falseJ and to each clock x ? C a
3
nonnegative real a(x) ? R+. We write ? for the set of all states. I
For a delay 6 E R+, let a+6 denote the state that agrees with the state a E on all propositions
and assigns the value a(x) + 6 to each clock x E C. Given a set A (v1 := a1,. . . , V? a?? of
variables Vj E P u C and corresponding values a? E (true,falsei u R+, we write a[A] for the state
that assigns the value flj to the variable Vj for all 1 < i < n and agrees with the state a ? on all
other propositions and clocks.
The execution of a system generates an infinite succession of states. in each state the system
may either take a transition or let time pass. With each transition, the system changes its data and
control and resets some of the clocks; that is, the values of propositions are modified and certain
clock values are reset to 0. Whenever time passes, all clock values increase uniformly with the rate
of time. It follows that in any state the value of a clock r is equal to the amount of time that has
elapsed since the last time r was reset.
Definition 2.2 (trajectory and divergence) A (real-time) trajectory
a = a0 ho a1 hi a2 h2 a? h
consists of an infinite sequence of states Q ? and an infinite sequence of delays 6i E R+ such that
for all nonnegative integers t and all clocks x e C, either Q+1(x) = 0 or Q+i(x) = ai(x) + 6?. A
position of the trajectory a is a pair (?,6) consisting of a nonnegative integer i and a nonnegative
real 6 < 6?. The state at position (i, 6) of a is a(i, 6) = ? + 6. The time at position (i, 6) of a is
Tg(?, 6) = 6 + ?0<j<i 6?. The trajectory a diverges if for all T E R+ there is some position (i, 6)
of a with r?(i, 6) = r. If II is a set of trajectories, we write 11div for the set of divergent trajectories
in 11.i
We identify two trajectories if they can be transformed into one another by repeated replacement
of a state a with the pair a a. Given a trajectory a and a position (`i, 6) of a, we write a[..(i, 6)]
for the finite prefix
a?(0, 0) ho ... 6?i a?(i, 0) $ a(i, 6)
up to position (i, 6), and a[(i, 6)..] for the infinite suffix
a?(i, 6) ??6 a(i + 1,0) ?ffl++1 a(? + 2,0)
starting with position (i, 6). Note that a[(i, 6)..] is again a trajectory. By
= fa(?, 0) + 6 0 < 6 ? 6j?
we denote the set of states in the i-th segment of the trajectory a (without the two endpoints a(?, 0)
and a(i, 0) + 6?). The positions of a trajectory a are ordered lexicographically: the position (i, 6)
precedes the position (j,E), denoted by (i,6) ? (j,e),iffeither i ? j, or i =j and 6< 
We model the timed behavior of a system by a divergent trajectory. This decision reflects
several choices we make [AH92b]. First, the divergence requirement ensures the progress of time
past any real number. Second, we choose time to be weakly monotonic: since a delay 6? can
be 0, time need not advance between consecutive transitions. The weak monotonicity of time
allows the modellng of simultaneous activities by sequential interleaving. Not all researchers find
this abstraction convenient. Our preference for weak monotonicity is no precondition for any of the
4
results we will present and may be reversed. Third, we restrict ourselves to the modeling of systems
that satisfy the condition of finite variability: since a trajectory is a countable sequence of states
(and delays), the number of transitions in any bounded time interval of a divergent trajectory is
finite.
The possible behaviors of a system are collected in a set of real-time trajectories. This set is
closed under future, past, and fusion. Future and past closure result from the abstraction of initial
states of the system. Fusion closure asserts that the future evolution of the system is completely
determined by the present state of the system and does not depend on its past: given a fusion-closed
set II of trajectories and a state a, the subset of trajectories in II that start from a form a tree
structure of states with root a.
Definition 2.3 (future, past, and fusion closure) A set II of trajectories is future-closed (or
suffix-closed) if for all trajectories a Ei II and all positions ir of 6, the trajectory 6[ir..] is in II.
The set II is past-closed if for ail trajectories 6 e II, all states a ? ??, and all delays 6 E R+, if
a(0, 0) = a + 6 then the trajectory
a 6'e6o a-(1,0)4?6(2,0)H&a-(3,0)ffi*?.
is in II. A set II of trajectories is fusion-closed if for all trajectories 6, 6' e II and all positions (i, 6)
of 6 and (j, E) of a-', if a-(i, 6) = a-'(j, e) then the trajectory
6(0,0) ho ... 6?i a(i,0) 6, a-(i,6) 6,?? a-'(j+ 1,0) 6,?i a-'(j +2,0) 6?2
is in II. I
it is not difficult to check that the three closure conditions are pairwise independent. Also note
that the fusion closure of a set II of trajectories implies a form of stutter closure: for all trajectories
6 E II and all positions (i, 6) of 6, the trajectory
6(Q 0) ho ... 6H??1 6(i, 0) ? 6(?, 6) 646 6(i + 1,0) 6?i 6(i + 2,0) 6$+2 ...
is in II. This condition, which is sometimes called time additivity [NS9l], asserts that any delay of
6i + 62 time units can be split into two consecutive delays of 6i and 62 time units, respectively. We
write F(6) for the stutter closure of a trajectory 6; that is, F(6) is the smallest stutter-closed set
of trajectories that contains a.
Definition 2.4 (premodel and real-time system) A premodel is a set of trajectories that is
future-closed, past-closed, and fusion-closed. A real-time system is a premodel that contains only
divergent trajectories. Given a premodel fi, a state a ? Y is reachable in II if there is some
trajectory 6 E II and some position ir of 6 such that 6(r) = a. We write ?n for the set of states
that are reachable in II. I
if a set II of trajectories is closed under future (past; fusion), then so is the subset 11div C II of
divergent trajectories. We conclude that every premodel subsumes a real-time system.
Proposition 2.1 If II is a premodel, then 11di? is a real-time system.
5
2.2 Safety and divergence safety
A safety property is a set of admissible system behaviors that is closed under certain limit behaviors:
a set II of infinite state sequences is closed under limits iff for any infinite state sequence a, whenever
all finite prefixes of a are prefixes of sequences in II, then the liniit sequence a itself is in 11 [ADS86].
We define the corresponding notion of safety for real-time trajectories.
Definition 2.5 (safety) A set 11 of trajectories is safe if for any trajectory a, if for all positions Ir
of a there is some trajectory a' E 11 and some position ir' of a' such that a[..r] = a'[..?'],then a E 11.
The safety closure 11 is the smallest safe set of trajectories that subsumes 11. I
Suppose that a real-time system 11 contains a trajectory whose initial state is a. Since 11 is
closed under stuttering, its safety closure 11 must contain the trajectory
0 0			0
a			a			a
which does not diverge. It follows that no nonempty real-time system is safe. Thus we define
the less stringent requirement of divergence safety: only the divergent limit trajectories must be
present.?
Definition 2.6 (divergence safety) A set fi of divergent trajectories is divergence-safe if for
any divergent trajectory a, if for all positions r of a there is some trajectory a' ? 11 an? some
position 7r' of a' such that a[..r] = a'[..ir'], then a E 11. The divergence-safety closure 11 is the
smallest divergence-safe set of trajectories that subsumes 11. I
Example 2.1 Let Hi be the real-time system that changes the value of a proposition p from false
to true before time 10; that is, Hi is the set of all divergent trajectories a with some position r
and some clock ? E C such that for all positions r' of a,
1. if 7r' ? r then a(r')(p) = false and 0 < a(ir')(x) < 10,
2. if r' ? Ir then a(?')(p) = true, and
3. if a(ir')(x) = 0 then T?(1r') = 0.
It is not difficult to check that the set Hi is indeed closed under future, past, and fusion.
The real-time system Hi is divergence-safe. To see this, take a divergent trajectory a such
that every finite prefix of a is a prefix of a trajectory in Hi. Since a diverges, it has a position Ir
with ?(7r) > 10. Since a[..r] is a prefix of a trajectory in Hi, it satisfies all four conditions for
some position ir' ? r and some clock x. Furthermore, since a[..:r'j is a prefix of some trajectory
in Hi for all positions r' ? r of a, also a(r')(p) = true and a(r')(x)> 0 for all r' ?
Now consider the real-time system 112 that changes the value of p eventually; that is, 112 is the
set of all divergent trajectories a with some position 7F such that for all positions ?` of a,
1. if 7r' ? ? then a(r')(p) = false, and
2. if 7r' ? ? then a(r')(p) = true.
The real-time system 112 is not divergence-safe. To see this, let a be a divergent trajectory such
that a(r) = false for all positions r of a. Then every finite prefix of a is the prefix of a trajectory
in 112, but a itself is not in 112. I
1The reader fanuliar with [Ben92] will notice that the concept of divergence safety corresponds to the notion of
safety relative to the divergence of time.
6
To close a set II of trajectories under (divergent) limits, we add a (divergent) trajectory a if all
finite prefixes of a are prefixes of trajectories in II. This process need not be iterated. It follows
that the divergence-safety ctosure of a real-time system II can be obtained from the safety closure
of II simply by dropping all trajectories that do not diverge.
Proposition 2.2 For all sets II of divergent trajectories, ff = --H11div
Corollary 2.1 If the premodel II is safe, then the real-time system 11div is divergence-safe.
2.3 Next-state relations
Safe premodels and divergence-safe real-time systems can be defined by a binary transition relation
on the state space, which indicates for each state a E X the possible transition successors of a.
Each transition successor a' ? ? of a results from a' by modifying the propositional component of
the state and by resetting some of the clocks.
Definition 2.7 (transition relation) For a binary relation 5 ? on the states, we write ?s
for the union of the domain and the range of 5. The relation 5 is past-closed if for all states a E ?
and all delays 6 E R+, if a + 6 ? ?s then a C ?s. The relation 5 is self-reflexive if for all a ?
(a, a) E 5. A transition relation 5 ? ?2 is a past-closed sdfre?exive binary relation on the states
such that (a, a') E 5 implies for all clocks x ? C, either a'(x) = a(x) or a'(x) = 0. I
Every transition relation 5 determines a two-phase next-state relation ?s that first advances
time, by any amount, and then performs a transition. The iteration of the two-phase relation
generates real-time trajectories. Transition relations are required to be self-reflexive so that infinite
trajectories can be generated without the possibility of deadlock.
Definition 2.8 (generated trajectory) Given a transition relation 5 and a delay 6 ? R+, let
6 = ?(a, a + 6)1 a E ?Y and let ??6 = 6 ? 5 The transition relation 5 defines the next relation
= U6ER+ ?6?. A trajectory
a = a0			a1			a2 H62 a3
is generated by the transition relation 5 if ? ?s6 Q+i for all i > 0. We say that a is an 5-trajectory
and write lls for the set of 5-trajectories. I
It is not difficult to check that the set lls of trajectories that are generated by a transition
relation 5 is closed under future, past, fusion, and limits.
Proposition 2.3 For any transition relation 5, the set lls of 5-trajectories is a safe premodel.
Corollary 2.2 For any transition relation 5, the set 115div of divergent 5-trajectories is a divergence-
safe real-time system.
Every transition relation 5 defines, then, a unique premodel, Hs, which is safe, and a unique
real-time system, llsdiv, which is divergence-safe. Indeed, we show that the four closure condi-
tions (closure under future, past, fusion, and limits) are both necessary and sufficient for a set of
trajectories to be definable by a transition relation.
7
Definition 2.9 (induced relation) A set II of trajectories induces the smallest relation 5H ?
such that for all trajectories
6i			62			63
ao			a1			a2			a?			...
in II and for all nonnegative integers i, (Q + 6i, Q+i) ? 5H I
Let II be a set of trajectories. Since the induced relation 5H is detined locally on consecutive
states of trajectories in II, if two sets of trajectories have the same safety closure, then they induce
the same transition relation.
Proposition 2.4 For all sets fi of trajectories, Sn
Corollary 2.3 For all sets II of divergent trajectories, Sn 5n?
If a set II of trajectories is future-closed, past-closed, and stutter-closed, then the induced
relation Sn is past-closed and sdfreflexive (namely, reflexive on the states "?? that are reachable
in II).
Proposition 2.5 If II is a premodel, then the induced relation 5H is a transition relation.
We now generalize a well-known result for infinite state sequences: a set of infinite state se-
quences is generated by a binary relation on the states iff it is closed under suffixes, fusion, and
limits [Eme83] (closure under stuttering corresponds to the requirement of seWrefiexivity for the
generating relation). Every safe premodel II is definable by a transition relation, namely Sn, which
generates precisely the trajectories in fi. Likewise, every divergence-safe real-time system II can be
defined by the transition relation Sn.
Proposition 2.6 For all premodels 11, lls11 = fi.
Proof. First observe that 11 C ll?? and thus, by Proposition 2.4, also if C ?11.
To see that lls11 C if, consider a trajectory a such that for all i > 0. there is a trajectory a?t ? II
and a nonnegative integer j with a? + ? = a31 + 6? and a?+1 = a31+1. Since II is future-closed, for
all i > 0 there is a trajectory 611 E 11 with Q + 6? = 6t' and ? = 0 and 6i+1 = 6i11. Since II is
past-closed, for all i > 0 there is a trajectory 6m ? II with 6? = 6611 and ? = 6611 and 6i+1 =
From repeated application of the fusion closure of II, it follows that for all positions Ir of 6 there is
a trajectory 6+ E II and a position r+ of 6+ with 6[..rj = 6+[..r+]. Since if is closed under limits,
it follows that 6 E if. I
Corollary 2.4 For all real-time systems II, 118d211v = ii.
2.4 Nonzenoness
For untimed systems (premodels), there is a pleasing one-to-one correspondence between safety
properties (safe premodels) and next-state (transition) relations. In particular, every safe pre-
model fi can be defined operationaliy, by the induced transition relation 5n, and 5n is the only
transition relation that generates II.
Proposition 2.7 For all transition relations 5, 5r's = 5
Corollary 2.5 For all prernodeTh 11 and transition relations 5, 11 = 11s iff both 11 is safe and 5 =
511.
Corollary 2.4 allows us to define divergence-safe real-time systems operationally, by their tran-
sition relations, just as untimed safety properties can be defined by next-state relations. How-
ever, while there is a unique transition relation that generates a safe premodel Hi (namely 5111),
there are many transition relations that generate the same divergence-safe real-time system 112.
We call a transition relation 5 that generates 112 nonzeno iff it suggests an operational seman-
tics for H?; that is, iff every finite prefix of an 5-trajectory can be extended to a divergent 5-
trajectory [AL92, Hen92].2 We will see that only one of the transition relations that generate 112 is
nonzeno (namely 5112), and thus a suitable operational definition for the divergence-safe real-time
system 112.
Definition 2.10 (nonzenoness) A transition relation 5 is nonzeno if for all 5-trajectories a and
all positions ? of a, there is a divergent 5-trajectory a' with a'(0, 0) = a(r). I
A nonzeno transition relation 5 suggests a notion of execution for the divergence-safe real-
time system HsdiV defined by 5. Each execution step consists of two phases, namely, a time delay
followed by a transition from 5. A simple-minded interpreter that iterates execution steps will
generate precisely all prefixes of the trajectories in HsdiV. If, on the other hand, the transition
relation 5 is zeno, then the simple-minded interpreter can paint itself into a corner and arrive at a
state from which it cannot let time diverge (thus generating prefixes of sequences in H? that are
not prefixes of sequences in Hsdiv).
Example 2.2 The divergence-safe real-time system Hi of Example 2.1 induces the transition re-
lation
5n, =			(a,a')I
= false A a(x) < 10 A a'(p) = true A a'(x) = a(x)) v
= false A a(x) < 10 A a' = a) v
= true A a' = a)
The transition relation ?ni is nonzeno and Hi is the set of all divergent Sni -trajectories. Now
consider the transition relation
52 = 5ll? U f(a,a') a(r) ? 20 A a' =
While the set of all divergent 52-trajectories is still Hi,the transition relation 52 is zeno. To see
this, observe that no nontrivial finite prefix of the 52-trajectory
(false, 0) fl5 (false, 15) ? (false, 15) ? (false, 15) $ ...
can be extended to a divergent 52-trajectory (here (false, 0) stands for the state a with a(p) = false
and a(x) = 0). Although both transition relations S111 and 52 define the same divergence-safe real-
time system, namely Hi, only the former relation suggests an operational semantics for Hi: iterate
time delays with transitions from Sni I
2The reader familiar with the concept of machine closure [AL88] will realize that the nouzenoness requirement is a
machine closure condition, namely, machine closure with respect to the liveness property that asserts the divergence
of time
9
We 110W show the real-time analogues of Proposition 2.7 and Corollary 2.5, which reveal a one-
to-one correspondence between divergence-safe real-time systems and nonzeno transition relations.
It follows that every divergence-safe real-time system II can be defined operationally, by the induced
transition relation Sn, and 5H is the only nonzeno transition relation that defines II.
Proposition 2.8 A fransition relation 5 is nonzeno iff			= 5.
Proof. Let 5 be a transition relation. First observe that Sflds2v C 5.
Now suppose that 5 is nonzeno. To see that SC 5n??;,consider a pair (a, a') ? 5. Since 5 is
self-reflexive, there is an 5-trajectory that starts with the prefix a ? a'. Since 5 is nouzeno, there
is a divergent 5-trajectory that starts with the prefix a ? a'. It follows that (a, a') E Snds?v
Finally, we suppose that 5 is zeno and show that 5 ? 5n5d2V Since 5 is zeno, there is a
state a that occurs on an 5-trajectory but does not occur on any divergent 5-trajectory. Then
(a, a) ? Snsd?v? and (a, a) ? 5 because 5 is self-reflexive. 1
Corollary 2.6 For all real-time systems ri and nonzeno transition relations 5, fi = llsdiv iff both
II is divergence-safe and 5 =
3 Real-time Programs
We present two languages for defining divergence-safe real-time systems a guarded-command pro-
gramming language with clocks and finite-state machines with clocks. Both languages specify
transition relations.
3.1 State predicates
To assert properties of individual states, we first define a language of state predicates. Recall that
each state in ? is an interpretation of the boolean propositions in P and the real-valued clocks
in C.
Definition 3.1 (state predicate) The set of state predicates is de?ned inductively by the gram-
mar
p I x < d e < y .x + c ? y + d ? A Y'2
for propositions p E P, clocks x, y E C, and nonnegative integer constants c, 4 e N. 1
State predicates are interpreted over states. Given a state a ? ?, a state predicate b evaluates
to a truth value a(b) e ftrue,false1 in the standard way. The state a satisfies ?, denoted by a ?=
if a(b) = true. We write [[?? C ? for the set of those states that satisfy the state predicate b, and
we call them ?states. Two state predicates ?i and 92 are equivalent if [[?i? =
Standard abbreviations for state predicates, such as true, p q, x > 5 V y < 3, and 2 < x < 5,
are defined as usual. For state predicates ? and ? and a proposition p ? P, we write ?[p :=
for the state predicate that results from ? by replacing each occurrence of p with ?; similarly, for
clocks x,y E C and a constant e E N, by ?[? := cj (and ?[x := y+c]) we denote the state predicate
that is obtained from ? by replacing each occurrence of x with c (or v + c respectively). Given a
set A = fvi := a1,..., V? := a?? of replacements, we write ?[A] for the state predicate that results
from ? by simultaneously replacing each variable Vj with the corresponding expression a?. Finally,
10
for a delay 6 E R+ and the set A = fx ? + 6 I x E CY of replacements we write ?+6forthe
state predicate ?[A].
The satisfiability problem for state predicates is obviously no simpler than boolean satisfiability.
Indeed, both satisfiability problems are equally difficult.
Theorem 3.1 The satisfiability problem for state predicates is NP-complete.
Proof. Given a state predicate ?, let k be the largest constant in ? and let n be the number
of clocks in b Suppose that there is a satisfying interpretation a for ? and a(xi) < ... < a(Xn)
for the clocks .1...., X? of ?. Construct an interpretation a' that agrees with a on all propositions
and the ordering of clock values such that
--H			if a(x?) --H a(x??i) ?
--H a'(x??i) =			a(x??i) otherwise
(assuming that a(ro) = a'(xo) = 0). Then a' satisfies ? as well. Since no clock is assigned a value
greater than (k + 1). n, the interpretation a' can be guessed and checked in time polynomial in the
length of b I
3.2 Evolving state predicates
State predicates define static sets of states. if time advances from a state, the clock values change,
and so may the value of a state predicate. We describe the motion of state sets in time using
the binary evolves-to operator ?. Consider two state predicates ?i and ?2 The evolving state
predicate ?1 ?2 defines the set of states from which a state satisfying ?2 can be reached through
advancing time by some nonnegative amount, and ?i is satisfied until ?2 is reached.
Definition 3.2 (evolving state predicate) The set of evolving state predicates is obtained by
adding the evolves-to operator to the grammar of state predicates: if ?i and ?2 are evolving
state predicates, then so is ?i ?2 A state a E ? satisfies the evolving state predicate ?1
written a f= ?, if there is a nonnegative real 6 such that a + 6 = ? and for all nonnegative
reals E < 6 a + E k--H bi I
it is perhaps most intuitive to view the evolves-to operator geometrically. Suppose that the
state predicate ? contains n clock variables and no propositions. Then ? defines a finite union of
polyhedra in n-dimensional space and the evolving state predicate trtte ? defines the shadow
of b for a light source at co?:
[[frue??? =
Example 3.1 Consider the two-dimensional state predicates
= (0 < x <2 A y > 1),
= (1 < ? <3 A 2 < y < 4).
The evolving state predicates true ?2 and ?i ?2 define, then, the two polygons
?rue = [[0 < x <3 A 0 < ? < 4 A x --H 1 < y < x + 3?,
= [[0 < x <2 A 1 < y < 4 A x < y < x + 3?
shown in Figure 1. Note that both evolving state predicates are equivalent to pure state predicates.
We shall see that this is no accident. I
ii
y			y
6
true			b2
j
x
Figure 1: The graphic representations of true			?2 and ?i			b2
x
Viewed logically, the evolves-to operator extends the language of state predicates with a re-
stricted form of quantification over the real numbers R: the evolving state predicate ?1 ?2 is
equivalent to the quantifled formula
R.(6>? 0 A ?+6 A VE? R.(o < E< 6			?
By eliminating both quantifiers, we show that evolving state predicates are no more expressive
than state predicates. Since Tarski showed that the theory of the reals with order and addition
admits quantifier elimination, this should come as no surprise. To ensure that the quantifier-free
formula obtained by eliminating the evolves-to operator is a state predicate, however, we cannot
use the near-optimal decision procedure of Ferrante and Rackoff for the first-order theory of real
addition with order [FR75]. We provide a nonelernentary translation from evolving state predicates
to state predicates; the exact complexity of the satisfiability problem for evolving state predicates
is an open problem.
Theorem 3.2 For any evolving state predicate ? we can construct an equivalent state predicate b?
Moreover, the integer constants occurring in j?J are bounded by the largest integer constant in b
Proof. We repeat eliminating the innermost evolves-to operator. Consider the subformula ?i
b2 for state predicates ?i and b?:
[[?? ?? = ? R.(6>? 0 A ?+6 A ?a?? R.(o< e? 6 A ??
We proceed in two steps that eliminate the two quantifiers. First we eliminate the inner existential
quantifier. All atoms in the scope ? of the quantifier ?e. ? are of the forms 0 ? e and e < 6, p,
X + E < d c < y + e, and x + c < y + d. We convert ? into disjunctive normal form, which may
cause an exponential blowup. Observe that the existential quantifier distributes over disjunction
and atoms of the forms p and x + c < y + d. We rearrange all remaining inequalities so that they
12
provide lower and upper bounds on e, and we then solve each disjunct for e, which may cause a
quadratic blowup:
<e A e <6 A AjEIC < di --H Xj A AjEJ% --H y5 < e)? =
`[0<6 A AjEl0 < dj --H Xj A AjEJCj --H Yj <6 A AiEI,jEJCj --H < dj --H Xi? =
[[0<6 A AjEIXi <di A AjEiCi < y? + 6 A AiEI?EJXi + Cj < Yj + di?.
Next we eliminate the outer existential quantifier. All atoms in the scope ?` of the quantifier ?6. ?`
are of the forms 0 < 6 p, ir + 6 < d c < y + 6, ir + c < y + d and x < d. We convert ?` into
disjunctive normal form and solve each disjunct for 6:
`[a6.(0<6 A AiEI6<di?Xi A Aj?jQ?yj<6)? =
`[AjEl 0 < di --H Xj A AiEI,jEJ Cj --H y? < di --H Xi? =
[[AjEIXi < di A AiEThEJXi + Cj < Yj + di?. I
3.3 Guarded-command real-time programs
A real-time program consists of a set of guarded commands and a program invariant. Each transi-
tion corresponds to the execution of a guarded command. The guard of a command refers to the
values of propositions and clocks; it asserts a necessary condition for the corresponding transition
to take place. The program invariant also refers to the values of propositions and clocks; it must
not be violated by letting time advance, and thus asserts a sufficient condition for a transition
to take place. For example, the guard ir > 5, for a clock x, puts a lower bound on the time of
the corresponding transition, whid? cannot take place before the clock x reaches the value 5. The
invariant ir < 8, on the other hand, implies an upper bound on the time of the next transition:
some transition must take place before the clock x reaches the value 8. When a transition is taken,
some of the propositions are assigned new values and some of the clocks are reset to 0.
Definition 3.3 (real-time program: syntax) A (guarded-command) real-time program P --H
(G, ?O) consists of
1.
G the program body, a set of guarded commands. Each guarded command g E G is of the
form ? A, for a state predicate ? (the guard of the command) and a set A = := a? v ?
P U CJ of simultaneous assignments such that for all propositions p ? P, the expression a?
is a state predicate, and for all clocks x E C, the expression a? is either 0 (i.e., the clock x is
reset) or x (i.e., the clock x is left unchanged).
2. ?? the program invanant, a state predicate. We require ?? to be past-closed; that is, for
all states a E ? and all delays 6 ? R+, if a + 61= ?? then a --H
A guarded command defines a partial function from ? to ?. Let g = "h A be the guarded
command with A = fv := a? v ? P u CJ, and let a E ? be a state. The guarded command g
is enabled in the state a if a = ?. Any guarded command that is enabled in a may be executed
in a. The execution of g, in particular, leads to the state a[Aj, where a[Aj(v) = a(av) for all
variables v E P u C.
Definition 3.4 (real-time program: semantics) The real-time program ? = (G, ?O) defines
the transition relation Sp such that (a, a') ? S? if
13
1. either a' = a or for some guarded command g = `? A in G, a ip and a' =
2. a ?= ?? and a' ?
Each divergent Sp-trajectory is called a run of ?. We write llp = fl?d\pV for the set of runs of ?,
and ?p for the set of states that are reachable in ll?. Two real-time programs ?i and P2 are
equivalent if they have the same runs (i.e., ll? = llv2). The real-time program P is nonzeno if
the transition relation Sp is nonzeno. I
A real-time program P = (G, ?O) defines, then, the safe premodel flsp and the divergence-safe
real-time system Hp. Each transition of llp corresponds to the execution of a guarded command
in G. The past closure of the invariant ?? ensures that a = ?? for all states a E Zv that occur on
some run of P.
Example 3.2 The divergence-safe real-time system lli of Example 2.1 is defined by the real-time
program P1 with the single guarded command p := true and the invariant p V x < 10. (When
writing guarded commands, we suppress the guard true and assignments of the form v := v.) This
is because 5P? = ?ni
Alternatively, the divergence-safe real-time system lli can be defined by the real-time pro-
gram r2 with the single guarded command x ? tO p := true and the invariant p V x < 20.
Then llp1 = llp2, but Sp1 c S?2. While both real-time programs P1 and P2 have the same runs,
only ?i is nonzeno. indeed, the transition relation defined by ?2 is the zeno transition relation 52
of Example 2.2.1
The invariant b? of a real-time program P defines precisely the set ?s? of states that occur on
some Sp-trajectory. We now show that the program ? is nonzeno iff it has the strongest possible
invariant, namely, an invariant that defines precisely the set ?? of states that occur on some run
of?.
Proposition 3.1 Let ? be a real-time program with the invariant ??. Then ???? = ?Sv More-
over, the real-time program ? is nonzeno iff ???? =
Proof. Since all states that occur on an Sp-trajectory satisfy the invariant, ?? C ?Sp C
Now suppose that the state a satisfies the invariant ??. Since
0 0			0
a			a			a
is an Sp-trajectory, a E ?s?. If the real-time program ? is nonzeno, then every state that occurs
on an Sp-trajectory occurs also on a run of ? and, therefore, a E
Conversely, suppose that every state that satisfies the invariant ?? occurs on a run of P. To
show that the real-time program ? is nouzeno, it suffices to show that any state that occurs on an
S?-trajectory occurs also on a run of ?. This follows from the assumption, because all states that
occur on an Sv-trajectory satisfy the invariant pO o+
It follows that nonzeno real-time programs can be executed in a stepwise fashion: start with
any state that satisfies the invariant and then, repeatedly, either choose a guarded command that is
enabled and whose execution does not violate the invariant, or advance time without violating the
invariant. The iteration of the next relation ?Sp defined by a zeno real-time program, on the other
hand, may lead to a state from which time cannot diverge. In other words, the nonzeno real-time
programs are precisely the real-time programs that can be executed without looking ahead. If a
real-time program is zeno, then its invariant is too weak.
14
In Section 6, we will show that for every real-time program ?, the set ?p of states that occur on
some run of ? can be defined by a state predicate ?. Hence there is a nouzeno real-time program
that is equivalent to P (replace the invariant of P with ?). Indeed, `ve will give an algorithm
that automatically converts any given real-time program into an equivalent nonzeno program by
strengthening the invariant. Here, let us consider a second example.
Example 3.3 Consider the real-time program ?i = (G1, ?i?), where a is a ternary variable (short
for two boolean variables) that ranges over fa, b, cJ, and x is a clock:
G1 =			a = a			a :--H b
?1o			--H
a = b			a := a,
(a = b A x> 1)			a:
(a = a A w < 4) v (a = b A x <4) v (a =
If this program is started with a = a and x = 0, then the value of a alternates between a and b
arbitrarily (but finitely) often, until a is assigned c at some point between time 1 and 4. The lower
bound of 1 is imposed by the guard of the third guarded command; the upper bound of 4 is imposed
by the invariant. Once a is set to c, the program does nothing but let time pass.
Now consider the real-time program P2 = (C2, ?2?)
G2 =			a = a			a :--H b
a = b			a := a,
(a = b A 1< x <4)			a:
= (a = a A x < 5) v (a = b A x < 5) v (a =
It is not difficult to check that the real-time programs P1 and ?2 are equivalent. However, while
?i is nonzeno, ?2 is zeno, because the invariant ?2? is too weak. This is because any state a
with a(a) E ?a, bi and 4 < a(x) < 5 occurs on the 5?-trajectory
0 0			0
a			a			a
but a does not occur on a run of ?2 When executing ?2, a stepwise interpreter may decide to let
time pass beyond 4 in a state with a = a or a = b, in which case it commits to a "zeno run" that
must converge before time 5. I
Given a real-time program P, the guards and the invariant are state predicates, and the guarded
commands assign the value of state predicates to propositions. It follows that the transition rela-
tion Sp can be characterized syntactically as a predicate transformer that maps state predicates
to state predicates.
Definition 3.5 (precondition) For a state predicate ? and a guarded command g = A, the
weakest precondition of b with respect to g is the state predicate
preg(?) = #` A ?[A]
that characterizes all states from which a state satisfying ? can be obtained by executing the
guarded command g. For a real-time program P = (&, ?0), the weakest precondition of ? with
respect to P is the state predicate
prep(6,) = ?? A (? V ? pre9(?0 A ?)
9EG
15
that characterizes all ?C?states from which a ?0-state satisfying ? can be obtained by either doing
nothing or executing some guarded command of ?. I
Proposition 3.2 Let P be a real-time proyram and let ? be a state predicate. For all states a E ?,
a = prep(?) iff there exists a state a' E ? such that (a, a') e 5? and a'
We will use the state predicate transformer pre? to execute a nonzeno real-time program P
symbolically.
3.4 Timed safety automata
The real-time program P1 of Example 3.3 is represented graphically in Figure 2. The graph of
Figure 2 can be viewed as the transition diagram of a timed automaton [AD9O] a finite automaton
with a finite set of real-valued clocks. We now define a ctass of timed automata timed safety
automata for specifying divergence-safe real-time systems.3
Definition 3.6 (timed safety automaton: syntax) A timed safety automaton A = (L, , f, g)
is a labeled directed multigraph consisting of
1. L a finite set of vertices called Theations.
2.  C L2 a multiset of edges called transitions.
3. f--Ha vertex labeling function that assigns to each location  E L a past-closed state predi-
cate f(), the location invariant.
4. g an edge labeling function that assigns to each transition e E E a guarded command g(e).
r>1
Figure 2: The timed safety automaton A1
Example 3.4 The timed safety automaton of Figure 2 has 3 locations, a, b, and c. The location
invariant true, the guard true, and the assignment x := x are suppressed. I
The reader familtar with [AD9O] will notice that we use a nonstandard variety of timed automata that (1) permits
clock constraints on both locations and transitions and (2) is interpreted over weakly monotonic time [AH92bj.
Furthermore, to ensure that a timed automaton defines a divergence-safe real-time system, we assume that all
locations of the automaton are Biichi accepting.
16
Instead of defining the transition relation 5A of a timed safety automaton A directly, we trans-
late the automaton into a real-time program. For this purpose, we use a new proposition p? for each
location  E L of the automaton A. We write a =  for the state predicate p? A AmEL--H?? ?Pm,
and a :=  for the set ?Pe truei U ?Pm false m ? L --H ??? of assignments.
Definition 3.7 (timed safety automaton: semantics) Given a timed safety automaton A =
(L,E,Lg), we define a real-time program ?A = (G,?0): for each transition e = (1,2) in , if e
is labeled with the guarded command g(e) = ? A, then G contains the guarded command
(a = ? A ff") A u ?a :=
and the program invariant ?? is the (past-closed) state predicate
A f(b
?EL
The timed safety automaton A defines the transition relation 5A = 5?A ?Ve write 11A = 11?A for
the set of runs of A. I
Figure 3: The timed safety automaton A2
Example 3.5 The zeno timed safety automaton A2 of Figure 3 corresponds to the zeno real-time
program P2 = PA2 of Example 3.3..
Conversely, it is not difficult to translate any real-time program P into a timed safety automa-
ton Ap with a single location and a transition for each guarded command of P, such that P and Ap
define the same transition relation.
4 Real-time Logics
We present and compare two branching-time logics for specifying properties of real-time systems---H
the timed computation tree logic TCTL and the timed jt-calculus Tjt. Both languages use clocks
and arithmetic constraints on clock values to specify timing requirements.
4.1 Timed computation tree logic
Many important properties of systems find a natural expression in temporal logic [Eme90]. We first
review the real-time temporal logic TCTL [ACD9o], which extends the branching-time logic CTL
[EC82] with clock variables. The formulas of TCTL, which are interpreted over the states of a
17
given premodel II, are built from state predicates by boolean connectives, the two temporat until
operators ?U (possibly) and vU (inevitably), and a reset quantifier for clocks. Intuitively, the
formula p?Uq (pVUq) holds in a state a of II iff the proposition q becomes true on some (every)
trajectory in II that starts from a, and the proposition p is true until q becomes true.
The formulas of TCTL contain three kinds of variables. Propositional variables from P and
clock variables from C occur freely and refer to the states of the given premodel II. In addition,
we may bind certain clock variables by reset quantifiers to express the timing requirements of a
specification. A specification clock z C C is a clock that does not control the behavior of any system
under consideration; that is, we consider only trajectories a such that for all positions ? of 6,
6(ir)(z) = 6(0, O)(z) + r?(ir).
We write C? C C for the set of specification clocks. The reset quantifier z., which binds and resets
the specification clock z, is inspired by the freeze quantifier of Timed Temporal Logic [AH89]: for
example, the formula
z. (trueVU(q A z < 5)
asserts that the proposition q becomes necessarily true within 5 time units.
Definition 4.1 (syntax of TCTL) The formulas ? of the timed computation tree logic TCTL
are defined inductively by the grammar
pjr+c<? y+dI ??J ? V? I
for propositions p E P, clocks r, y E C, specification clocks z ? C?, and nonnegative integer
constantsc,d? N. I
Additional arithmetic, boolean, and temporal operators, such as =, A, and ??, are defined
as usual. In particular, the temporal operators ??y and VC? stand for true?Uy and ????y,
respectively, and the temporal operators V?? and a?? stand for trueVU? and ?V???, respectively.
Also note that all state predicates are definable in TCTL; for example, the state predicate x < 5
abbreviates the TCTL-formula z. (x < z + 5).
The formulas of TCTL are interpreted over the states of a premodel. The propositions and
the free clock variables of a TCTL-formula ? are evaluated in states. To evaluate bound clock
variables, we use clock environments. A clock environment C is a partial function from the set
of specification clocks to the nonnegative reals R+. The empty clock environment ? is undefined on
all specification clocks. The clock environment ? + 6, for a delay 6 E R+, maps the clock z ?
to the value ?(z) + 6 if the environment g is defined on z; otherwise g + 6 is undefined on z. We
write ?[v := a] for the environment that agrees with the environment ? on all variables except v,
which is mapped to the value a.
Definition 4.2 (semantics of TCTL) Let II be a premodel and let a ? ?n be a state that is
reachable in II. The state a satisfies the TCTL-formula ? in II, denoted by a I=n y, if a I=n,? ?
for the empty clock environment ?. The satisfaction relation K--HH,? is defined inductively for all
clock environments C:
a I=n,c p iff a(p) = true;
a I=n? x+c< y+d iff f(x)+c<? f(y)+d,
where f(v) = ?(v) if ? is defined on v, and f(v) = a(v) otherwise;
18
a I=n,? ?? iff a ?H,? ??
a K--HH,? ? V ? iff a j=n,? Yi or a --HHE ?
a Kn,? ?1?M?2 iff for some trajectory a e II with a(0,0) a,
there exists a position (i, 6) of a such that a(?, 6) Kfl?E+?(i,6) Y2 and
for all positions (j, e) of a, if (j, ?) ? (i, 6) then a(j, e) I=fl?E+T?(j,?) ?i V ?2;
a KH,E YlVUY2 iff for all trajectories a ? II with a(0,0) = a,
there exists a position (i, 6) of a such that a?(i, 6) i=fl?+T?(i,6) ?2 and
for all positions (j, e) of a, if (j, e) ? (?,6) then a(j, e) KH,E+r?(j,?) Yi V ?2
a K--Hn,E z ? iff a KH,E[z:=Oj ?
We point out that the density of the time domain causes a subtle complication in the definition
of both until operators ?U and VU. Suppose that the formula "? until ?" holds on a trajectory a
iff ?2 becomes true in a and ?i is true in a until ?2 becomes true. In particular, the state
predicate ?2 may become true either at a position r of a or in a left-open interval immediately
foiThwing a position ? of 6 (compare the formulas "x ? 5 until x > 5" and "x < 5 until x > 5").
To account for both possibilities, we require that there is a position ? of 6 at which ? is true and
that the disjunction ?i V ??rather than ?i only---4s true at all positions of 6 before ?. It follows
that the TCTL-formula z. < 5)VU(z > 5)) holds in each state of every real-time system.
A few comments regarding our particular version of TCTL are in order. First, unlike [ACD9o],
we have opted for weakly monotonic time. Second, the time-bounded temporal operators used
in [ACD9O] are definable in TCTL. For instance, the time-bounded response requirement
VE(p			_
which asserts that every request p must be followed by a response q within 5 time units, is expressible
in TCTL by the formula
VEz. (p			V?(q A z < 5)).
Thus we will use time-bounded temporal operators such as V?<5 as abbreviations. Third, in our
version of TCTL freeze quantifiers on static time variables are replaced by reset quantifiers on
dynamic clock variables. While both approaches are equivalent [Alu9l], the clock-reset style fits in
better with our definition of real-time programs.
4.2 Finite variability
Given a premodel II, every formula ? of TCTL defines a set s C ?H of reachable states, namely,
those states that satisfy ?. We will refer to s sometimes as the characteristic set of ? (in 11) and
sometimes as the requiremefft (of fi) specified by y. The following definitions apply to all logics,
such as TCTL, whose formulas are interpreted over the states of a premodel.
Definition 4.3 (characteristic set) The characterist? set ???H of a formula ? in a premodel II
is the set of all reachable states that satisfy ? in II:
t[?H = ?aE?nIaI=n?Y.
19
When interpreting a formula over a premodel 11, it will often be convenient to consider, in place
of a subformula, a set 5 C ? of states. For example, we write ???s?? for the set of states from
which a trajectory in 11 leads to a state in 5. Formally, for all states a ? ?? and all environments g,
let a s iff a E 5.
Definition 4.4 (finite variability) Given a trajectory a and a nonnegative integer i, recall that
s?(a?) stands for the set of states in the i-th segment of a (Section 2.1). The trajectory a respects
a set 5 C ? of states if for all i E N, either s?(a) C 5 or si(a) A 5 = ?. The set 5 is finitely variable
along a if there is a trajectory a' ? F(a) in the stutter closure of 6 such that 6' respects 5. The
set 5 is finitely variable over a set 11 of trajectories if 5 is finitely variable over all trajectories in 11.
A logic is finitely variable over a class C of premodels if for all formulas ? and all premodels 11 e
the characteristic set [[??n is finitely variable over 11. I
Let 6 be a trajectory. We defined trajectories so that the characteristic sets of all atomic state
predicates are finitely variable along 6. Moreover, the state sets that are finitely variable along 6
are closed under complement, union, and finite intersection. It follows that all state predicates
define finitely variable sets.
Proposition 4.1 The logic of state predicates is finitely variable over all premodeis.
TCTL, however, is not finitely variable over all premodels. The following example presents a
TCTL-formula ? and a divergence-safe real-time system 113 such that the characteristic set
is not finitely variable over 113.
Example 4.1 Let 113 be the real-time system that first changes the value of a proposition p from
false to true at time 2 --H 21m' for some positive integer m > 0, and then changes the value of p
back to false at time 2 --H 2m1+1 More precisely, 113 is the set of divergent 3-trajectories, where the
transition relation 5 is the reflexive closure of the binary relation
(a, a')			(a(p) = false A a(?) =2--H
?rn> 0.			(a(p)			--H			A a'(p) = true A a'(x) = a(x)) v
= true A a(x) = 2 2m+1 A a'(p) = false A a'(x) =
Then 113 is divergence-safe and the TCTL-formula ??=iP is not finitely variable over 11?:
1 1
???=1P?H3 = ta I ?rn> 0. (a(p) = false A 2rn + ? ? 1 --H a(x) --H 2m
The branching structure of the real-time system 113 cannot be specified by a real-time program.
Indeed, if we restrict our attention to real-time systems that are definable by guarded-command
real-time programs (or timed safety automata), then TCTL is finitely variable. This is because over
real-time programs, all state sets that can be defined by TCTL-formulas can already be defined by
state predicates. These state sets are called regions.
Definition 4.5 (region) Given a real-time program P and a formula ?, let Cp C C be the set of
clocks that occur in ? (within a guard or within the program invariant) or freely in ?, and let k
be the largest integer constant that occurs in ? or in ?. A set of states 5 C ? is a (?, y)-region if
there is a state predicate ? such that 5 = [[??, all clock variables in `p are from C?, and the largest
integer constant in ? is at most k. A (?, ?)-region is minimal if it does not properly contain a
nonempty (P, ?%region. I
20
Suppose, for example, that C? ?ri, x2, x3? and k 5. Then the state predicate
= (1 < xi <2 A x2 = 3 A 4 < X3 < 5)
defines a region that is the disjoint union of three minimal regions, namely, [[? A xi + 3 < x??,
Ib A xi + 3 = x3?, and [[? A xl + 3> x3?.
Some observations about regions are immediate, Let P be a real-time program and let y be
a TCTL-formuta. First, there are only finitely many (?, y)-regions: if ? and `:` contain n clocks
and no constant larger than k, then there are O(nk . n!) minimal (P, ?)-regions [Alu9l]; and every
(P, `:`)-region is a finite disjoint union of minimal (?, ?)-regions. Second, the (P, `:`)-regions are
closed under all boolean operations. Third, since the real-time system H? is closed under past,
Theorem 3.2 implies the following lemma, which asserts that the (?, ?)-regions are closed under
time delays.
Lemma 4.1 Let P be a real-time program, let `:` be a TCTL-formula, and let ? and b2 be two
state predicates. If [[?i? and [[?2? are (?, y)-regions, then ??i " ?2? is a (?, `:`)-region.
We now restate in our framework the main theorem for timed automata from Alur's thesis. By
Proposition 4.1, we obtain the finite variability of TCTL over real-time programs as a corollarv.
Theorem 4.1 [Alu91] For every real-time program ? and every TCTL-formula ?, the character-
istic sets			and [[??n? are (?, ?)-regions.
Corollary 4.1 TCTL is finitely variable over the class of real-time programs.
4.3 The timed ?-calculus
We now introduce T?, a dense-time ?-calculus with clocks. The formulas of T? are built from state
predicates by boolean connectives, a temporal next operator, the reset quantifier for clocks, and a
least-fixpoint quantifier. While discrete-time t-calculi rely on a unary next-time operator [Koz83,
Eme92], there is no notion of "next time" when time is modeled by the real numbers. Instead, we
use the binary next operator ?, which is best viewed as a "single-step until" operator of temporal
logic:4 roughly speaking, the formula p ? q asserts that p is true now and stays true until some
transition is taken, and this transition establishes q. In particular, the "next" transition may be
arbitrarily close in time or arbitrarily far away. For example, the formula
z.(true?(q A z <5))
asserts that q can be established by a single transition taken within 5 time units.
The formulas of T? contain four kinds of variables. In addition to free propositional variables,
free clock variables, and specification clocks that are bound by reset quantifiers, Tjt-formulas may
contain formula variables that are bound by least-fixpoint quantifiers. We use V as the set of
formula variables and write jX. for a least-fixpoint quantifier that binds the formula variable X.
Definition 4.6 (syntax of T?) The formuThs ? of the timed ?-calcnlus Tj are defined inductively
by the grammar
::= X p x + c < y + d			?i V ?2 ? ? ?2 1			iiX. ?
4A modal operator similar to our next operator has been proposed for a dense-time extension of Hennessy-Milner
logic [HLW9ij.
21
for formula variables X E V, propositions p E P, clocks x, y E C, specification clocks z E C?, and
nonnegative integer constants c, d ? N. We require that every occurrence of a formula variable X E
V in ? is bound (i.e, it appears within the scope of a least-fixpoint quantifier ?X.) and positive
(i.e., it appears within an even number of negations from the quantifier ?X. that binds X). I
The standard condition that all formula variables must occur positively ensures that the argu-
ments of all least-fixpoint quantifiers define monotonic functionals, which guarantees the existence
of the corresponding fixpoints. Additional arithmetic and boolean operators are defined as usual
and, as in the case of TCTL, all state predicates are definable in T?. We write ?[X := a] for the
T?-formula that results from ? by replacing each free occurrence of the formula variable X with
the expression a. The abbreviation vX. ? denotes a greatest-fixpoint quantifier and stands for the
T?formula ?iX. (??[X
The formulas of T? are interpreted over the states ? of a given premodel. For this purpose,
the environment needs to be extended to provide values for both specification clocks and formula
variables. A T?-environment g consists of a clock environinent Ci together with a total function C2
from the set V of formula variables to the power set 2? of states; that is, for all specification
clocks z E C?, either ?(z) ? R+ or ?(z) is undefined, and for all formula variables X E V,
C ?. The Tjt-environment ? is empty if its clock component is empty (i.e., ti ?). The
T?envirnnment ? + 6, for a delay 6 ? R+, consists of the clock component ? + 6 and the formula-
variable component g2
Definition 4.7 (semantics of T?) Let II be a premodel and let a ? ?? be a state that is
reachable in II. The state a satisfies the Tjt-formuh ? in II, denoted by a I=n ?, if a
for all empty T?-environments ?. The satisfaction relation Kn?? is defined inductively for all
T?-environments g; only the following clauses differ from the definition of the semantics for TCTL:
a Kn? X iff a E ?(X);
a I=n,? ?1 ? ?2 iff for some state a' ? ?? and some delay 6 e R+,
a			a' and a' kH,E+6 ?2, and
for all delays e E R+, if e < 6 then a + e K--Hn,?+? Yi V ?2
a Kn,? iX. y iff a E fl?s C ?? fa' e ?n a' Kfl?[X:=s] ?J =
For a formula y of T?, we write [[??n C ?? for the set of reachable states that satisfy ?. I
Let II be a premodel and let g be a Tjt-environment. Now consider the subformula jtX. ?
of a T?-formula; that is, ?X. ? may contain free formula variables. The semantic clause for
the least-fixpoint quantifier ensures that the formula ?X. ? defines the least fixpoint of the func-
tional F?(X) = [[??n? from 2?? to 2?H: for 5 C ?n and a ? ??, a ? F?(s) iff a K?H,?[X:=s] ?. The
least fixpoint of the functional F? exists by the Tarski-Knaster theorem, because ?? is a monotonic
functional on the complete lattice (2?n, C?) (i.e., ?i ? ?2 implies P?(s1) C F?(s2)). To see this,
recall that all free occurrences of X in ? are positive and observe that disjunction, conjunction,
and, by the following lemma, the next operator are monotonic in both arguments.
Lemma 4.2 Let II be a premodet. For all sets 5, ?i, ?2 C ??, if ?i C ?2 then [[s-i ? s?n C
and [[s ? si?n C [[s ?
22
The semantic clause for the next operator ? uses existential quantification over successor states.
The dual operator, a unary next operator with universal force, is definable in T?: for all premod-
els II, T?-environments ?, and reachable states a e
a Kn,g ?(true ?
iff for all states a' E ?n and all delays 6 E R+, if a ?6?11 a' then a' K--Hfl?+6 y (the stutter closure
of II implies, then, that a + e k?fl,?+E ? for all delays 0 < e < 6).
4.4 Computing fixpoints
Let II be a premodel and let [X. ? be a formula of Tj. Since the characteristic set [[?X. y?ij is the
least fixpoint of the functional F(x) = [[??H, it follows that
= ?
iEO
for a sufficiently large ordinal 0; that is, the characteristic set ??A?. y?n is the lin?t of the successive
approximation sequence
?, F(?), P2(?), F3(?),...
We now show that, over the class of real-time programs, all elements of this sequence are regions.
Indeed, we construct the state predicates that define the regions.
The following lemma is fundamental for computing fixpoints over both zeno and nonzeno real-
time programs by successive approximation. To accommodate nested fixpoint quantifiers, we need
to look at T?-Iormulas with several free formula variables.
Lemma 4.3 Let P be a real-time program, let ? be a fixpoint-quantifier-free subformula of a
formula with the formula variables Xi,Xn, and let A = ?X1 := 51,...,Xn := sn? be a set
of assignments of state sets to formula variables. If the state sets ..... . , s? are (?, ?)-regions,
then so is the characteristic set [[?[A]?nsp Aioreover, f the real-time program ? is nonzeno, then
Proof. Let ?? be the invariant of the real-time program ?. We use induction on the structure
of the subformula ?. Throughout the proof, let II = 11Sp and, if ? is nonzeno, II = ll?.
Suppose that ? is the formula variable Xj and the region 5j is defined by the state predicate %.
From Proposition 3.1 it follows that ??[A]?11 is defined by the state predicate ?? A %.
If ? is a proposition or a clock constraint, then [[?[A]?n is defined by the state predicate ?? A y.
The boolean cases follow from the fact that the (?, ?)-regions are closed under all boolean
operations.
If ? is of the form z. ? and ??[A]?n is defined by the state predicate ?, then [[y[A]?n is defined
by the state predicate ?[z := 0].
Finally, suppose that ? is of the form ?1 ? ?2 and the characteristic sets [[`y'j[A]]]n, for i = 1,2,
are defined by the state predicates ?. From Proposition 3.2 it follows that ?y[A]?n is defined by
the evolving state predicate
(? v
The lemma follows from Theorem 3.2.1
Let ? be a nonzeno real-time program. Since there are only finitely many (?, ?)-regions,
[[`ix. `;`?flp =			?
O<i<m
23
for a sufficiently large integer m; that is, the limit of the successive approximation sequence is
reached within a finite number of steps. This observation is the basis for the symbolic model-
checking algorithm presented in Section 6.1. More precisely, the number m of iterations of the
functional F that are necessary to compute the least fixpoint of F is bounded by the number of
minimal (P, y)-regions, which is exponential in the representations of ? and y. In general, the
number of iterations that are required by this method to compute the characteristic set [[??n? of
an arbitrary T?-formula ? depends exponentially not only on the number of clocks and the size of
the largest constant in P and ?, but also on the nesting depth of least-fixpoint quantifiers in y.
In Section 6.3 we will show that for every real-time program, there is an equivalent nonzeno
program. The theorem below follows.
Theorem 4.2 For every real-time program ? and every Tjtformula y, the characteristic sets
and I??n? are (P, y)-regions.
Corollary 4.2 T? is finitely variable over the class of real-time programs.
By contrast, T? is not finitely variable over all premodels (consider the divergence-safe real-time
system 113 of Example 4.1 and the T?-formula z. (true ? (p A z 1))).
5 The Expressive Power of Fixpoints
We now compare the expressive power of the timed ?-calculus T? with the expressive power of the
timed computation tree logic TCTL. The expressive power of a logic is measured by determining
which requirements of a given class of premodels are definable in the logic.
Definition 5.1 (expressiveness) Let C be a class of premodels. The formula ?A is equivalent
to the formula ?B over the class C if ([YA?n = ([?B?n for all premodels II ? C. The logic A is as
expressive as the logic B over the class C if for every !3-formula ?B there is an A-formula ?A that
is equivalent to ?B over C. I
Depending on the class of premodels under consideration, we obtain different results about the
relative expressiveness of two logics. In particular, we will show that while some TCTL-requirements
of real-time systems cannot be specified in Tjt, all TCTL-requirements of guarded-command real-
time programs can be specified in Tjt. Recall that TCTL is based on the temporal until operators ?M
and vU, and T? is based on the temporal next operator ?. We proceed in three steps. First, we
show that the possibility operator ?U is definable as a fixpoint over all premodels. Second, we show
that the inevitability operator W? is not definable as a fixpoint over all real-time systems. Third,
we show that the inevitability operator VU is definable as a fixpoint over safe premodels and, for
finitely variable arguments, also over divergence-safe real-time systems.
5.1 Possibility over premodels
Let us begin with a couple of positive results. We show that, over all premodels, the possibility
(reachability) operator ?U is definable in T?, and the next operator ? is definable in TCTL.
Proposition 5.1 For all premodels II and all sets ?i, ?2 ? ?n of reachable
t[si?Us2?n = j[?X. (52 V (si ?
24
Proof. We first show that the set ?siaus2?n is a solution of the equation X = ?52 V (si ?X)?u;
that is,
= ??2 V (si ?(si???s2))?n.
Let a Ei ?n be a reachable state. Since a a, if a I=H s1?Us2 and a ? ?2, then a I=n s1?(si?Us2).
Conversely, if a E ?2 then a I=n s1aus2; and since II is future-closed and fusion-closed, if a
? (s1?Us2) then a kn s1?Us2.
It remains to be shown that the set ??1aM?2?? is the least solution of the equation X = ??2 V
(5i ?X)?n. Let 5 C ?n be such that 5 = ??2 V (si ?s)?n; we show that ([si?Ms2jJn C s. Let a Ci
be such that a I=n s1?Us2. Then there is a trajectory a Ci II and a position (i, 6) of a such
that a(0, 0) = a, a?(i, 6) Ci ?2, and for all positions (j, e) of a, if (j, e) ? (i, 6) then a(j, e) Ci (5i U 52).
By induction on m Ci N, it follows that a(i --H m, 0) Ci 5 for all 0 < m < ?. In particular, a Ci 5.1
In other words, the characteristic set of the formula 5i ?Us2 is the least fixpoint of the functional
F(X) = [[52 V (si ?X)?n.
From the proof of Proposition 5.1 it follows, moreover, that
[[si?Us2?n = ?
jEN
Intuitively, the set Fi(?) contains all states from which a state in ?2 can be reached by at most ? tran-
sitions along a path in si u ?2 We point out that the functional F, while monotonic (Lemma 4.2),
is not necessarily continuous.5
The next operator ? is definable in TCTL, provided that the set Puc of propositions and clocks
is, as we have assumed, finite. To define the formula ?i ? Y2 using the possibility operator ?U, we
must ensure in the first argument of ?U that no proposition changes its value and no clock is reset
no clock changes from a positive value to the value 0). This assurance can be given by a finite
disjunction of formulas of the form
(? A ?i)?U(?2 V ((? A ?i)???2)),
where the state predicates ? enumerate all possible proposition values (boolean) and clock values
(zero or positive), and the state predicate ? agrees with ? on all propositions while asserting that
all clocks are positive. It follows that for every TCTL-formula ? with next operators, there is a
TCTL-formula without next operators that is equivalent to ? over all premodels.
5.2 Inevitability over real-time systems
The following observation is instrumental for characterizing the expressive power of fixpoints: the
timed ?-calculus cannot distinguish between premodels that induce the same transition relation.
Proposition 5.2 For all premodels lli and 112 and all T?-formulas Y, if Sn1 = Sn2 then [[??n? --H
Proof. First observe that 5?1 = ?r'2 implies ?lii = ?fl2 It is straightforward to show by
induction on the structure of y that, for all reachable states a Ci ??111 and all T?-environments g,
a k--Hn1? ? iff a Kn2,c ?. I
5Consider a real-time system II that contains only trajectories along which some clock x is never reset including a
trajectory that starts with z = 0. Let 81 = = 0?n 82 = I., and X:' = t[x > for a]l i > 1. Then F(Ut>i X?) =
and ??>1 F(X?) = I.
25
Corollary 5.1 Let ? be a formula of T?. For all premodels II, [[??n = and for all real-time
systems II, ???n =
We apply Proposition 5.2 to two examples. First, consider the TCTL-formula
?div = VEz.V?(z = 1).
The formula ?div is satisfied in a state a of a premodel II iff time diverges along all trajectories
that start with a. Consequently, ([?div?H = ?n iff the premodel II is a real-time system. It is
not difficult to see that no T?-formula is equivalent to the TCTL-formula ?di? over all premodels
(note that the Tj-formula true is trivially equivalent to ?div over the class of real-time systems).
For suppose that there is some T?-formula ? asserting that a premodel II is a real-time system
(i.e., [[??H = ?? iff II is a real-time system), then by Corollary 5.1, 11 is also a real-time system,
which is a contradiction (no real-time system is safe). It follows that the timed ?-calculus T?
is, over all premodels, not as expressive as the branching-time logic TCTL. Indeed, we will now
strengthen this observation to the class of real-time systems.
Second, recall the real-time system 112 of Example 2.1, which eventually changes the value
of the proposition p from false to true. The safety closure 112 contains a trajectory a such that
= false for all positions 7r of a. Thus, while all reachable states of 112 satisfy the TCTL-
formula V?p, this it not the case for 112. From Corollary 5.1 it follows that the property V?p
cannot be defined in T? over the class of real-time systems. Hence we have the first part of the
following result.
Theorem 5.1 T? is not as expressive as TCTL over the class of real-time systems, and TCTL is
not as expressive as T? over the class of real-time programs.
a1			? > ?
a0
x>O `			a1			x > 0
x := 0			a0
mm
Figure 4: Timed safety automata Ai and !3j
Proof. We need to show only the second part of Theorem 5.1. First recall that CTL is strictly
less expressive than the propositional ?-calculus; in particular, the CTL*-formula
?E]?p = vX.??(pA?OX),
26
which asserts that there is a trajectory that contains infinitely many ?states, cannot be defined
in CTL [EC8o]. We modify a combinatorial proof of this result [EH86] to show that the T?formula
= uX. ??(r = 0 A ((x = 0) ? ((x > 0) ?
is not definable in TCTL over the class of real-time programs.
The proof proceeds by contradiction. Suppose that there is a TCTL-formula ? such that
= ???q?n? for all real-time programs ?. Let z be nesting depth of temporal operators in ?,
and let P c p be a set of propositions that do not occur in ?.
Now consider the two sequences Aj and Bj, for i e N, of timed safety automata defined in
Figure 4. The automata modify the control variable ?, whose value a(?) E ?a?, bi I ? E N? is
encoded using propositions from P, and the two clocks x and ?. We write ? c ? for the set of
states a with 0 < a(x) < a(v) < 1. Given a state a e ?, a clock environment g is a a-environment
if ?(z) < a(y) for all specification clocks ? C?. To avoid cumbersome notation, we write a[] for
the state a[a := ] and suppress automaton designators whenever possible (note that every A?-run
that starts from a state a[a?], where i > j, is a B?-run from a[?], and vice versa).
We show four claims:
1. For all states a E ? and all i ? N, a[a?] W
2. For all states a E ? and all i e N, a[bi] 1= ?i4
3. For all TCTL-formulas ? of depth at most i that contain no propositions from P, for all
states a E ? and a-environments C, and for all integers j, k > i, a[?] WE y iff a[a?] I=E ?
4. For all TCTL-formulas ? of depth at most i that contain no propositions from P, for all
states a e ? and all a-environments ?, a[a?] K--HE ? iff a[b?'J WE y.
The second part of Theorem 5.1 follows from Claims 1, 2, and 4 applied to i = i; Claim 3 will be
used to establish Claim 4.
To show Claim 1, use induction on ?.
To show Claim 2, let 5 = ?a[b?] a ? ?? and observe that6
5 = [[??(x = 0 A ((x = 0) ? ((x > 0) ?
The proofs of Claims 3 and 4 are mostly technical and given in the appendix. I
Theorem 5.1 should come as no surprise. It is true that in the untimed case, the branching-time
logic CTL is strictly less expressive than the propositional ?-calcuius [EC8o]. ?Iore precisely, the
until operators ?U and VU are definable in the propositional jt-calculus over all systems that are gen-
erated by transition relations. This result, however, is somewhat misleading: if systems are assumed
to be closed under stuttering, then only safe systems are generated by transition relations [Eme83].
Indeed, the inevitability operator VU of CTL cannot be defined in the propositional ?-calculus over
stutter-dosed systems, because the propositional ?-calculus cannot distinguish between a system
and its safety closure. Over stutter-closed systems that are safe, the CTL-formula Y1VU?2 is triv-
ially equivalent to its second argument. As the following proposition shows, this observation applies
also in the timed case.
6Note that the T?-formuIa ?,nJ does not define the set 5' of states ? ? ?n? for which the state predicate r = 0
is true at infinitely many positions of some B?-run that starts from a (the set s' is empty). Rather, the characteristic
set [[?inj?n? is the set s of states from which z = 0 may become true arbitrarily (but finitely) often.
27
Proposition 5.3 Let II be a premodel and let 5i, ?2 C ?? be two sets of reachable states. If II is
safe, then [[s1VUs2?n =
Proof. First observe that ?2 C [[s1VUs2?H for all premodels II.
Now assume that the premodel II is safe. To see that [[siVUs??n C ?2, let a ? Yn be a reachable
state and suppose that a ?n ?1??2 Since II is future-closed, stutter-closed, and safe, it contains
the trajectory
0 0			0
a			a			a.??
From a I=n s1VUs2, it follows that a ? ?2 1
In the following subsection, we will show that Tv is as expressive as TCTL over the class of
real-time programs, which will allow us to compute the characteristic sets of TCTL-formulas over
real-time programs as fixpoints. Our proof will depend on (1) the divergence safety of real-time
programs and (2) the finite variability of TCTL over real-time programs. Whi]e our proof of the first
part of Theorem 5.1 shows that finite variability by itself is not a sufficient condition for defining
inevitabillty in Tv, we do not know if divergence safety by itself is sufficient. In other words, it is
an open problem if Tv is as expressive as TCTL over the class of divergence-safe real-time systems.
5.3 Inevitability over real-time programs
We now show in two steps that for the class of real-time programs there is a fixpoint characteriza-
tion of inevitability. First, recall that real-time programs define divergence-safe real-time systems.
Proposition 5.4 will show that over divergence-safe real-time systems, the inevitability operator WI
can be defined as a least fixpoint of the time-bounded inevitability operator VU<c, for any positive
integer constant c > 0. Second, recall that all TCTL-requirements are finitely variable over the
class of rea?time programs (Corollary 4.1) and that for all premodels there is a fixpoint character-
ization of possibility (Proposition 5.1). Lemma 5.1 will show that for finitely variable arguments,
the time-bounded inevitability operator vU<c is, over the class of real-time systems, definable by
the possibility operator ?U.
Proposition 5.4 Let II be a real-time system, let 5i, ?2 ? ?? be two sets of reachable states, and
let c > 0 be a positive integer constant. If II is divergence-safe,7 then
[[s1VUs2?H = ?vX. (52 V (siVU<c X))?n.
Proof. First observe that the set [[s1vUs2?n is a solution of the equation X = [[52 V (5iVU<c X)?u;
that is,
[[sivUs??n = [[52 V (5iVU<c (siWIs?))?n.
Now assume that the real-time system II is divergence-safe. We show that the set [[51VUs2?n
is the least solution of the equation X = [[52 V (5iVU<c X)?n. Let 5 C ?H be such that 5 =
[[52 V (5iVU<c s)?n; we show that [[s1WIs2?n C s. Assume that there is a state a0 E ([[s1WIs2?n --H
we show a contradiction.
We construct inductively an infinite sequence of states Q e ([[s?VUs2?n --H s), for i E N. Suppose
that we have already constructed a?. Since Q' ? s, since II is future-closed, and since all trajectories
7We point out that while the condition of divergence safety is not necessary (consider the real-time system that
consists of all divergent trajectories along which the value of the proposition p changes finitely often) it cannot be
omitted. To see this recall once again the real-time system 112 of Example 2.1 which eventually changes the value of
the proposition p from ft?ise to true. From Corollary 5.1 it follows that ?uX. (p v v?<1 x)l112 = [[uX. (p vV?<1 X)?-n2,
whereas [[V?p?n2 # [[V?p??n2.
28
in II diverge, there is a trajectory (7j E II with o(O, 0) --H ? and a position 7rj of (7j with Tu(7ri) =
such that either
1. for some position 7r ? 7rj of 6?, a?j(r) ? si and for all positions ?` ? 7r of (7j? aj(ir') ? 5; or
2. for all positions r ? ? of a?, 6j(7r) E (5i --H s).
But since (7j Wn 51VU52 and 52 ? 5, Condition 1 cannot happen and Condition 2 implies
3. for all positions 7r ? 7rj of (7j, 6j(ir) E ([[siV?s??n --H
We choose ?j+i =
Now consider the trajectory 6 that results from concatening the trajectory pretixes 6?[..r?] for
all?> 0:
a = 6o[..roj ? 6i[..ri] ? 62[..r2] ....
The trajectory 6 diverges, because c > 0. Since II is fusion-closed and divergence-safe, 6 E II.
Furthermore, 6(0,0) = ao and, by Condition 3, 6(r) ? s for all positions it of 6. Since ?2 C 5, it
follows that ?o Wn ?1??2, a contradiction. I
There is a folk theorem (formalized in [Hen92]) that all time-bounded properties are safety
requirements. Consider the two time-bounded properties VE<5 ?q and V?<? q. The time-bounded
invariance property VE]<? ?q, which puts a lower time bound on the occurrence of a q-state, is
written in TCTL as the VEl-formula
z.VE)(z < 5
which is easily recognized as an invariance. On the other hand, the time-bounded response prop-
erty V?<s q, which puts an upper time bound on the occurrence of a q-state, is written in TCTL
as the V?-formula
z.V?(z <5 A q).
This formula is, over the class of real-time systems, equivalent to the negated possibility (i.e., in-
variance)
?z. ((?q)?U(z> 5)).
Intuitively, a q-state is inevitable within time 5 on all divergent trajectories iff it is not possible
that more than 5 time units pass without a q-state occurring.
The generalization of this observation to binary bounded-inevitability operators VU<c is sur-
prisingly subtle: if the first argument of VU<c is different from true, we must restrict ourselves to
real-time systems over which the second argument is tinitely variable.
Lemma 5.1 Let II be a real-time system, let ?i, 52 C ?n be two sets of reachable states, and let
c Ei N be a nonnegative integer constant. If ?2 is finitely variable over II, then
I[siVU<c 52?H = ??Z ((?s2)?U(??(si V 52) V > c))?n.
Proof. First, recall that 5iVlA<c ?2 stands for z. (siVU(52 A z < c)), which over all premodels
is equivalent to
z. ((5i A z < c)VU(s2 A <
which over the class of real-time systems is equivalent to
z. ((5i A z < c)VU(s2 A <
29
where the unless operator VU is defined as follows: for all premodels II, clock environments g, and
reachable states (7 E ?n,
(7K--Hn,E ?1VUy2
iff for all trajectories (7 E II with (7(0, 0) = (7, either
1. there exists a position (i, 6) of (7 such that (7(i, 6) Kll,?+?(i,?) Y2 and
for all positions (j, e) of (7, if (j, e) ? (i, 6) then 6(j, e) I=fl,?+?&(j,?) Y'i V ?2 or
2. for all positions (i, 6) of (7, (7(i, 6) l=11,?+T?(i,?) Vi
Second, we show that for all premodels II and all sets 5i, ?2 ? ?n of reachable states, if ?2 is
finitely variable over 11,8 then
[[siVUs2?n = [[?((?s2)?U(?5i A ?s2))?H.
Let (7 E ?n be a reachable state. If (7 I=n (?s2)?U(?si A ?s2), then (7 WH s1VUs2. Conversely,
assume that (7 ?H s1VUs2. Then there is a trajectory (7 E II with (7(0,0) = (7 such that
1. for all positions r of(7 with (7(r) E ?2, there is a position ir' ? r of(7 such that (7?(r) ? (sius2);
and
2. there is a position 7r of 6 such that (7(r) ? si.
If ?(r) ? ?2 for all positions r of 6, then Condition 2 implies that (7 j=? (?s2)?U(?si A ?s2).
Otherwise, let r be the infimum of all positions r' of 6 with 6(r') E 52; that is, for all positions r' ?
r of 6, 6(r') ? 52, and either 6(r) E ?2 or, since ?2 is finite?y variable along the trajectory 6, there
is a position r' ? r of 6 such that for all positions r ? r" ? r' of 6, 6(r11) ? ?2 In either case,
Condition 1 implles that (71=11 (?s2)?U(?si A ?s2). I
5.4 Translating timed computation tree logic into the timed ?-calculus
Together, Propositions 5.1 and 5.4, Corollary 4.1, and Lemma 5.1 prescribe a method for computing,
over real-time programs, all TCTL-requirements as fixpoints of Tjt. Speci?cally, we can translate
any TCTL-formula ? into a T?-formula ?` by
o+ first replacing each subformula of the form ?iVU#'2 with the formula
MX. (? V ?z. ((?X )?U(?(? V X) V z> c))),
for any positive integer constant c> 0,0 and
o+ then replacing each subformula of the form ?1?U?2 with the formula MX. (?2 V (?i ?
The resulting T?-formula ?` is equivalent to the original TCTL-formula y over the class of all
real-time programs. We conclude the following theorem.
Theorem 5.2 TM is as expressive as TCTL over the class of real-time programs. More specifically,
for each TCTL-formula `:` we can construct a T?formuTh ?` whose size is linear in the size of ?
such that ? and ?` are equivalent over the class of real-time programs.
5To see that the finite-variability condition cannot be omitted, consider a real-time system II that does not reset
the clock z E C. Let Si = = O?n and 52 = ?a ? ?? an > O.a(z) = ?`J If a E ?n with a(z) = 0, then
a ?n a1VUs2 and a ?n (?s2)3U(?si A 52).
The choice of c may effect the number of iterations performed by the symbolic model-checking algorithm of
Section 6.1.
30
6 Symbolic Model Checking
Let ? be a formula of TCTL or T?. A premodel II meets (is correct with respect to) the require-
ment ? if all reachable states of II satisfy the formula y; that is, if [[??n = ??. The verification
question of deciding if a given premodel, specified in a system description language A, meets a
given requirement, specified in a logic B, is called the model-checking problem for A and !3.
The model-checking problem for verifying TCTL-specifications ? of real-time programs ? was
solved by Alur, Courcoubetis, and Dill [ACD90]. Their solution relies on the explicit construction
of a finite quotient graph, called the region graph, of the infinite state-transition graph that is
defined by the input program ?. The construction of the region graph, whose vertices are minimal
(?, ?)-regions, leads to a model-checking algorithm that is exponential in both the number of input
clocks and the size of the largest input constant. The following theorem tells us that we cannot
expect more from a general verification procedure.
Theorem 6.1 [ACD9O] The model-checking problem for real-time programs and TCTL is PSPACF-
complete.
In practice, however, it is often unnecessary to construct the entire region graph. We take
advantage of this observation (1) by representing only those state sets that are required for solving a
specific problem instance (?,?) and (2) by representing state sets symbolically as state predicates.
In other words, rather than enumerating all minimal (?, ?)-regions, a symbolic model-checking
algorithm computes regions selectively and symbolically.
6.1 The algorithm
Let ? be a real-time program and let y be a formula of TCTL or Tjt. By Theorems 4.1 and 4.2,
there is a state predicate b such that ???Hp = ???. We call ? a characteristic predicate of y
for P. We compute characteristic predicates for TCTL-formulas ? in two steps. First, we apply
Theorem 5.2 and translate ? into an equivalent T?-formula ?`. Second, we apply the following
algorithm and compute a characteristic predicate for ?` by successive approximation of fixpoints.
The algorithm is defined inductively on the structure of T?-formulas.
Algorithm 6.1 (symbolic model checking)
(1) a real-time program ? with the invariant ?? and
(2) a T?-formula ?.
a state predicate ??j such that
Input:
0utput:
o+ I?I := b0Ap;
o+ Ir+c<y+dI := ?? A r+c<??+d;
o+ := b? A ?I?I;
o+ I?ivy?I := lyil v I??I;
o+ I??Y2I :=			V			__			see Definition 3.5 for a definition of pre? and
I(I?i			1Y2i)			pre?(jy2j)j;			Theorem 3.2 for the computation of I?i			?2I
o+ Iz. ?I := I?I[z := 0];
o+ I?X. ? is the result of the following iteration:
31
false;
repeat
bv I?[X:=biI
until ?b? =
return ?.
The test [[? = ???, for two state predicates ? and ?, can be decided by using Theorem 3.1
to check the satisfiability of the state predicate ? ? ?. The termination and correctness of Algo-
rithm 6.1 follow from the constructive proof of Lemma 4.3.
Theorem 6.2 Let ? be a real-time program and let ? be a formula of T?. On input (?, ?),
Algorithm 6.1 yields as output, within a finite number of steps, a state predicate ? such that
Moreover, if the real-time program ? is nonzeno, then
Algorithm 6.1 can, therefore, be used to verify TCTL-specifications and T?-specifications of
nonzeno real-time programs: a nouzeno real-time program T meets the requirement ? iff the
characteristic predicate j? is equivalent to the program invariant ?? (use Theorem 3.1 to decide
the equivalence of state predicates).
Corollary 6.1 The model-checking problem for real-time programs and T? is decidable.
On one hand, using the region graph of a real-time program, the model checking of T?-formulas
can be done in time that is exponential in the number of input clocks, the size of the largest input
constant, and the nesting depth of fixpoint quantifiers. On the other hand, from the PSPACE-
hardness of the reachability problem for timed automata [Alu91], it follows that the model-checking
problem for real-time programs and T? is PSPACE-hard. The exact complexity, however, is not
known to date even for the untimed problem of model checking the propositional ?-calculus.
Many optimizations for computing fixpoints of the propositional ?-caIculus apply also to Al-
gorithm 6.1; for example, intermediate results can be reused when nested fixpoints of the same
polarity are computed [EL86]. The practicality of a symbolic method depends, furthermore, on the
representation of state predicates. While Algorithm 6.1 can be used to compute the characteris-
tic predicates of T?-formulas directly on the region graph of the input program, we know of two
implementations that represent state sets symbolically and thus avoid the costly construction of
the region graph. A verification system at Grenoble [NSY92] represents state predicates by differ-
ence matrices over the integers [Dil89]; a verification system at Cornell [AHH93] represents state
predicates as Mathematica formulas.
6.2 A verification example
We consider the gate controller of a railroad crossing. The system consists of two parallel processes,
namely, a train and a controller. The two processes are modeled as the two timed safety automata
shown in Figure 5.
32
M
app
y < 2
up y < 1			down Ii < y < 2
out			2
y < 1			:= 0
Figure 5: Railroad gate controller
The control variable a of the train automaton ranges over three locations: a = 0 if the train
is far from the crossing; a = 1 if the train is close to the crossing; a = 2 if the train is in the
crossing. When the train approaches the crossing (i.e., proceeds from location 0 to location 1), it
sends the signal app to the gate controller. This happens at least 2 minutes before the train enters
the crossing. When the train leaves the crossing (i.e., proceeds from location 2 to location 0), it
sends the signal out to the gate controller. This happens at most 5 minutes after the app signal.
The control variable p of the controller automaton ranges over four locations: p = 0 if the
controller is waiting for the train to arrive; P = 1 if the signal app has been received; P = 2 if the
gate is down; p = 3 if the signal out has been received. When the controller receives the app signal
from the train, it responds by closing the gate within no less than 1 minute and no more than 2
minutes. When the controller receives the out signal, it responds by opening the gate within 1
minute.
We can define a product of timed safety automata that combines the train process and the
controller process by synchronizing on the app and out signals. Instead of providing a formal
definition of parallel composition (see, for instance, [AD90]), we present a real-time program ? =
(G, ?O) that specifies the resulting system:
G = f (a = 0 A ? = 0) `app a := 1,? := 1,x := O,y =0,
(a = 1 A 2 < x < 5) ?:`n a := 2,
= 1 A 1 ? y < 2) ?down ? := 2,
(a = 2 A P = 2 A x <5)			?? a := 0,73: 3,y :0,
(73 = 3 A ? < 1) ?ap 73 := 0 J;
=			a ? fQ1,2J A 73 ? f0,1,2,3? A
(a E ?1,2?			x <5) A
(73 = 1			y < 2) A (73 = 3			? < 1).
It is not difficult to check that the real-time program ? is nonzeno.
We wish to verify that the gate is never closed for more than 5 minutes. This requirement is
33
expressed by the TCTL-formula
= ?nit			VE](P = 2			= 0),
for the initial condition
?nit = (a = 0 A ? = 0 A x = 0 A y = 0).
By Theorem 5.2, the TCTL-formula ? is over the real?time program P equivalent to the T?-formula
= ?nit			??Y.((P = 2 A z.?X.(z>5 v ((? #0) ? X))) v (true ?
We now apply Algorithm 6.1 to compute the characteristic predicate j?'J.
The state predicate ItLX.(z > 5 v ((p # 0) ? X))j that defines the inner fixpoint is computed
iteratively as = Vi>0 ?, where ?o = false and
= ? v (?O A z> 5) v ((?? A P # 0) ?
for all i> 0. We have:
= ?? A z> 5
= ? v ((a = 0 v ((a = 1 v a = 2) A x <5 A z> x)) A
= 1 A y < 2 A z> y + 3) v p = 2 v (p = 3 A ?J < 1 A z> ? + 4)));
= ? v (a = 0 A f3 = 1 A y < 2) v
((a = 1 v a = 2) A ? = 1 A x < 5 A y < 2 A z> x A ? > x --H 4) v
(a = 2 A ? = 2 A x <5 A z> x --H 1);
= ? v (x < 5 A z > x --H 1 A ((a = 1 A ? = 2) v
(a = 2 A ? = 1 A ? < 2 A ? > x --H 4)));
= ? v (a = 1 A ? = 1 A x <5 A z> x --H 1 A y < 2 A `y > x --H 4).
We find that ??6? = [[??? and the fixpoint computation terminates with ? = `u'? Next we compute
the state predicate Iz. ?I = := 0]:
= (a = 0 v ((a = 1 v a = 2) A x < 1)) A ((P = 1 A y < 2) v p = 2).
Now we compute the outer fixpoint iteratively as = Vi>0 %, where ? = false and
= ? v (?O A ? = 2 A W) v (?O ?
for all i> 0. This computation converges with ? =
= = 2 A ?`;
= ? v ((a = 0 v ((a = 1 v a = 2) A x < 1 A x <y)) A ? = 1 A y < 2).
Finally, it is not difficult to check that the the state predicate (?O A ?init) ?? is equivalent to
the program invariant ??, which implies that the real-time program ? meets the specification ?.
34
6.3 Symbolic nonzenoness analysis
Algoritlim 6.1 can be used (1) to check if a real-time program ? is nonzeno and, if not, (2) to
convert ? into an equivalent nonzeno real-time program. To check if ? is nonzeno, we compute
the characteristic predicate of the possibility requirement z. ??(z = 1), which is true in all states
from which time can advance by 1 time unit.
Proposition 6.1 Let P be a real-time program with the invariant ??. Then ? is nonzeno iff
[[z.??(z= 1)?Hsp =
Proof. Recall that [[?E? = ??? (Proposition 3.1). Therefore [[z. ??(z = 1)?ns? C ????.
Now consider a state a0 ? Vsp that occurs on an S?-trajedory. If the real-time program ?
is nonzeno, then every state that occurs on an 5?-trajectory occurs also on a run of ? and,
therefore, a0 K?ns? z. ??(z = 1). Conversely, if all states a E ?Sp that occur on Sp-trajectories
satisfy a W?flsp z. ??(z = 1), then we can inductively construct a divergent S?-trajedory that
starts from a0 (for all i E N, add a segment whose length is exactly 1 time unit from Q to a
state Q+i) I
To convert a zeno real-time program ? into an equivalent nonzeno program, we need to
strengthen the program invariant so that the new invariant rules out all states from which time
cannot diverge. The "bad" (zeno) states of flsv are the states that do not satisfy the T?-formula10
Ynz = uX. z. ??(z = 1 A X),
which is true in all states that occur on an S?-trajectory along which time advances infinitely often
by 1 time unit; that is, ?? characterizes precisely the states that occur on runs of ?.
Proposition 6.2 For every real-time program P, [[Ynz?ns? =
The characteristic predicate of the greatest-fixpoint formula ??? can be computed with Algo-
rithm 6.1. Since the invariant ?? of any nonzeno real-time program ? defines precisely the set ?p
of states that occur on runs of ? (Proposition 3.1), the invariant ?? is equivalent to the character-
istic predicate I?nzI (Proposition 6.2). On the other hand, if the real-time program ? is zeno, then
the invariant ?? is weaker than and can be replaced by Ynz to obtain an equivalent nonzeno
program.
Theorem 6.3 For every real-time program ? there is an equivalent nonzeno real-time program,
which can be obtained from ? by replacing the program invariant with the state predicate I?nzI (as
computed by Algorithm 6.1).
6.4 Concluding remarks
We discussed two applications of symbolic model checking the automatic conversion of a real-time
program into an equivalent nouzeno program, and the verification of nonzeno real-time programs.
The ideas that underly our method can be used to devise various different symbolic verification
strategies. Suppose that we wish to check for the real-time program P that no ?2-state can
be reached from a ?1-state (?i might define the initial states of ? and ?2 some set of "bad"
10The T?-forrnula u'nz is not equivalent to ally TCTL-formula over all premodels. However one can define an ex-
tension TCTL of TCTL, analogous to the extension CTL [EH86J of CTL which separates the trajectory quantifiers
(e.g., V) from the temporal operators (e.g. 0). In TCTL*, the formula ??? can be written as ?Oz. ?(r = 1).
35
states). We solve this problem "backwards": starting from the set of ?2-states, we iterate the
precondition operator pre? (program transitions) and the evolves-to operator (time delays) to
compute the set ????2]]11? of states that reach a ?2-state; then we check if this set contains a
bi-state. Alternatively, one can define a symbolic postcondition operator post? and a symbolic
evolves-from operator ?--H? to solve the reachability problem "forwards": starting from the set of
bi-states, iterate post? and ?--H? to compute the set 5 of states that are reachable from a ?1-state;
then check if s contains a ?2-state. A third strategy constructs, also by successive approximation,
the coarsest bisimulation of the state space that separates all ?1-states from ?2-states. This strategy,
too, can be implemented using the precondition and evolves-to operators [ACH+92].
We conclude by pointing out that a natural extension of our method allows the analysis of
so-called hybrid systems, which contain variables that change continuously in more general ways
than clocks [ACHH93, NOSY93].
Acknowledgment. We thank Peter Kopke for a careful reading.
Appendix
Completion of the proof of Theorem 5.1. To show Claim 3, we define an equivalence
relation on pairs consisting of states and clock environments. Let (a?,t.i) (a2,?2) iff for all state
predicates ?, a1[C1] = b iff a?[??] k--H ?; that is, (a?,C1) and (a2,C2) differ at most in the fractional
parts of clock values and the relative order of all fractional parts of clock valties is preserved. For
example, for five clocks r, y, z, u, and v,
1, y := 1.1, z := 1.9, u := 3.5, v := 7.9] := 1, y := 1.6, z := 1.8, u := 3.7, v := 7.8].
Let P be a real-time program and assume that (ai, ?) (a?, ?2). Then a1[?1] and a2[?]
belong to the same minimal (?, ?)-region, for any TCTL-formula ?. From Theorem 4.1 it follows
that for all TCTL-formulas ?, ai[?] Kn? ? iff a2[?2] Knv ?; that is, al b iff a2 W--Hn?,? ?
We call this observation the equivalent-values lemma.
Now let us turn to Claim 3. It suffices to show by induction on the structure of':' that for
all j > i, a[?+i] I=c ? iff a[aj] ?`:`. The case that `:`is atomic (i = 0) depends on the assumption
that `:` contains no propositions from P. The cases that `:`is of the form ??, t"i V t"2, or z. are
straightforward. So assume that a[?+i] I=E ?iSUt'?2; that is, there exist two delays 6j+i, 6j > 0
such that a(y) + 6,'+i + ? < 1 and
o+ a[a5+i] + 6j+i K?+6j+i ?2 and
for all e < 6j+i, a[a5+1] + e --H?+? ff'i V ?`2, or
o+ (a[a5] + 6j+i)[x := 0] + 6j K--H&+?+,+a, ?2, and
for all E < 6j, (a[a?] + ?+i)k := 0] + e K?+6j+i+? ?1 V ?2, and
for all e < 6j+1, a[?+i] + e I=?+t ?1 V ip'?, or
(a[a5?1] + 6j+1 + ?)[r := 0] KE+?+1+? ?1?U?2, and
for all e < 6?, (a[?] + ?+i)k := 0] + e K?+?+i+? ?1 V ?2, and
for all E < ?+i, a[%+i] + e K--H?+c ? V ?.
Observe that 6j+i > 0 implies
((a[??i] + 6?+i + ?)[r := 0],? + ?+i + ?) ((a[%?i] + ?+1)[r := 0],? + ?+i)
Using the induction hypothesis and, in the last case, the equivalent-values lemma, we conclude
that a[?] ? `ki?U?2; namely,
36
o+ a[aj] + 6j+1 kE+Sj+i ?2 and
for all E < 6?+1, a[aj] + E I=?+c #`i V `Y'2, or
(a[a??ii + 6j+i)[? oi + 6? K--H?+6,+?+6? #2, and
for all E < 6J, ((7[%--Hii + 65+i)[x 0] + ? K?+6,+,+? ?1 V ?2, and
for all E < 65+1, a[?] + E W--Hc+? ?1 V #`2, or
o+ (a[??i] + 65+i)[x := 0] K??+6y+i ?`1?U?2, and
for all E < 6j+i, a[a5] + ? ??+? ?1 V `Y'2
The converse implication and the case that ? is of the form ?`1VU?2 are checked simitarly.
To show Claim 4, we use again induction on the structure of ?. The atomic, boolean, and
reset-quantifier cases are easily checked, So assume that a[a?] --H? ?1au?2; that is, there exists a
delay 6> 0 such that a(v) + 6 < 1 and
o+ a[a?] + 6 --H?+? ?2 and
for all E < 6, a[a?] + ? t?+( `? V ff?2, or
o+ (a[ai?1] + 6)[x 0] K?+t ?1?Uff"2, and
for all E < 6, a[a?] + E ?+? ?1 V ?2'
Using the induction hypothesis, we conclude that o'[bj] ? #`i?U?2; namely,
o+ o'[bi] + 6 --H?+? ?2 and
for all e < 6, a[bi] + E f=?+? ?1 V ?2, or
o+ (o'[a??1] + 6)[r := 0] I=?+a ?1?U?2, and
for all E < 6, a[bj] + E --H?+? #`i V ?2'
Conversely, assume that a[bi] K--H? #`i?U?2; that is, there exists a sequence 6..... , 6? > 0 of delays
such that a(?) + An < 1, for A5 = Zo<k<J 6k. and
0
(a[bj] + An?i)[x := 0] + 6n K?+? ?2 and
for all E < 6?, (a[bi] + An?1)[x := 0] + E K??+A??i+c ?1 V #2. and
for all j < n and all E < 65, (a[bi] + As?1)k := 0] + E K??+Aj?i+? ti V ?2. or
o+ (a[a??1] + An)[x := 0] K?+An ?1au?, and
for all j < n and all ? ? 65, (a[bi] + As?1)k := 0] + E K?+Aj?i+? t'i1 V 4)2
Using the induction hypothesis and Claim 3, we condude that a[a?+?] --H? `Y'i??'?2; namely,
o+ (a[a?] + An?i)[x := 0] + 6n K?+& #2 and
for all E < 6?, (a[a?] + An?1)[x := 0] + E K?+An?i+? ?1 V ?2. and
for all j < n and all E < 6j, (a[ai+n--Hj] + As?1)k := 0] + E #E+A3?1+? #`i V 4'2. or
o+ (a[a??1] + An)[X := 0] K?+An ?1???2. and
for all j < n and all E < 6j, (a[a?+??5] + A5?1)[x := 0] + E K--HE+A,?1+? ?i V ?2'
Another application of Claim 3 yields a[a?] W--HE #`l?U?2 The case that ? is of the form ?1VU?2 is
checked similarly. I
37
References
[ACD90]
[ACH+92]
R. Atur, C. Courcoubetis, and D.L. Dill. Modet checking for reat-time systems. In
Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pages 414--H
425. IEEE Computer Society Press, 1990.
R. Alur, C. Courcoubetis, N. Hatbwachs, D.L. Dill, and H. N\'ong-Toi. Mimmization of
timed transition systems. In S.A. Smolka, editor, CONCUR 92: Theories of Concur-
rency, Lecture Notes in Computer Science 630, pages 340--H354. Springer-Vertag, 1992.
[ACHH93] R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algo-
rithmic approach to the specification and verification of hybrid systems. In A. Nerode,
editor, Theory of Hybrid Systems, Lecture Notes in Computer Science. Springer-Verlag,
1993.
[AD9O]
R. Alur and D.L. Dill. Automata for modeling real-time systems. In M.S. Paterson, ed-
itor, ICALP 90: Automata, Languages, and Programming, Lecture Notes in Computer
Science 443, pages 322--H335. Springer-Verlag, 1990.
[ADS86] B. Alpern, A.J. Demers, and F.B. Schneider. Safety without stuttering. Inforn?ation
Processing Letters, 23(4): 177--H180,1986.
[AFH91]
[AH89]
[AH92a]
[AH92b]
[AHH93]
[AL88]
R. Alur, T. Feder, and T.A. Henzinger. The benefits of relaxing punctuality. In Pro-
ceedings of the Tenth Annual Symposium on Principles of Distributed Computing, pages
139--H152. ACM Press, 1991.
R. Alur and T.A. Henzinger. A really temporal logic. In Proceedings of the 30th An-
nual Symposium on Foundations of Computer Science, pages 164--H169. IEEE Computer
Society Press, 1989.
R. Alur and T.A. Henzinger. Back to the future: towards a theory of timed regular
languages. In Proceedings of the 33rd Annual Symposium on Foundations of Computer
Science, pages 177--H186. IEEE Computer Society Press, 1992.
R. Alur and T.A. Henzinger. Logics and models of real time: a survey. Th J.W.
de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory
in Practice, Lecture Notes in Computer Science 600, pages 74--H106. Springer-Verlag,
1992.
R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded
systems. In Proceedings of the 14th Annual Real-time Systems Symposium, pages 2--H11.
IEEE Computer Society Press, 1993.
M. Abadi and L. Lamport. The existence of refinement mappings. In Proceedings
of the Third Annual Symposium on Logic in Computer Science, pages 165--H175. IEEE
Computer Society Press, 1988.
M. Abadi and L. Lamport. An old-fashioned recipe for real time. In J.W. de Bakker,
K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice,
Lecture Notes in Computer Science 600, pages 1--H27. Springer-Verlag, 1992.
38
[AL92]
[Alu9l] R. Alur. Techniques for Automatic Veril'cation of Real-time Systems. PliD thesis,
Stanford University, 1991.
[BCM+92] J.R. Bnrch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model
checking: 1020 states and beyond. Information and Computation, 98(2):142--H170, 1992.
[Bry86] R.E. Bryant. Graph-based algorithms for boolean function manipulation. lEFE Trans-
actions on Computers, C-35(8):677--H691, 1986.
[CBM89]
0. Coudert, C. Berthet, and J. Madre. VerifIcation of synchronous sequential macbines
based on symbolic execution. In J. Sifakis, editor, CAV 89: Automatic Verification
Methods for Finite-state Systems, Lecture Notes in Computer Science 407, pages 365--H
373. Springer-Verlag, 1989.
[CES86] E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verifIcation of fImte-state con-
current systems using temporal-logic spedfIcations. ACM Tmnsactions on Programming
Languages and Systems, 8(2):244--H263, 1986.
[Di189]
[EC8O]
[EC82]
[EH86]
[EL86]
D.L. Dill. Timing assumptions and verifIcation of fInite-state concurrent systems. In
J. Sifakis, editor, CAV 89: Automatic Verification Methods for Finite-state Systems,
Lecture Notes in Computer Science 407, pages 197--H212. Springer-Verlag, 1989.
E.A. Emerson and E.M. Clarke. Characterizing correctuess properties of parallel pro-
grams as fIxpoints. In ICALP 83: Automata, Languages, and Programming, Lecture
Notes in Computer Science 85, pages 169--H181. Spnnger-Ve4ag, 1980.
E.A. Emerson and E.M. Clarke. Using branching-time temporal logic to synthesize
synchronization skeletons. Science of Computer Programming, 2(3):241--H266, 1982.
E.A. Emerson and J.Y. Halpern. "Sometimes" and "Not never" revisited: on branching
versus linear-time temporal logic. Journal of the ACM, 33(1):151--H178, 1986.
E.A. Emerson and C. Lei. Efficient model checking in fragments of the propositional ?-
calculus. In Proceedings of the First Annual Symposium on Logic in Computer Science,
pages 267--H278. IEEE Computer Society Press, 1986.
[Eme83] E.A. Emerson. Alternative semantics for temporal logics. Theoretical Computer Science,
26(1):121--H130, 1983.
[Eme90]
[Eme92]
[EMSS90j
E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of
Theoretical Computer Science, volume B, pages 995--H1072. Elsevier Science Publishers
(North-Holland), 1990.
E.A. Emerson. Real time and the mcalculus. In J.W. de Bakker, K. Huizing, W.-P.
de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes
in Computer Science 600, pages 176--H194. Springer-Verlag, 1992.
E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative temporal reason-
ing. In R.P. Kurshan and E.M. Clarke, editors, CAV 90: Computer-aided Verification,
Lecture Notes in Computer Science 531, pages 136--H145. Springer-Verlag, 1990.
J. Ferrante and C. Rackoff. A decision procedure for the fIrst-order theory of real
addition with order. SlAM Journal on Computing, 4(1):69--H76, 1975.
39
[FR75]
[Hen92] T.A. Henzinger. Sooner is safer than later. Information Processing Letters, 43:135--H141,
1992.
[HLW91]
[HMP91]
U. Holmer, K. Larsen, and Y. Wang. Deciding properties of regular real timed processes.
In K. Larsen and A. Skou, editors, CAV9i: Computer-aided Verification, Lecture Notes
in Computer Science 575, pages 443--H453. Springer-Verlag, 1991.
T.A. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for real-time
systems. In Proceedings of the 18th Annual Symposium on Principles of Programming
Languages, pages 353--H366. ACM Press, 1991.
[Koz83] D. Kozen. Results on the propositional ?-calculus. Theoretical Computer Science,
27(3):333--H354, 1983.
[Lew90] R.R. Lewis. A logic of concrete time intervals. In Proceedings of the Fifth Annual
Symposium on Logic in Computer Science, pages 38O-?389. lEEL Computer Society
Press, 1990.
[McM93] K.L. McMillan. Symbolic Alodel Checking: An Approach to the State Explosion Problem.
Kluwer Academic Publishers, 1993.
[NOSY93] X. Nicollin, A. Olivero, J. Sifakis, and 5. Yovine. An approach to the description and
analysis of hybrid systems. In A. Nerode, editor, Theory of Hybrid Systems, Lecture
Notes in Computer Science. Springer-Verlag, 1993.
[NS91]
X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In
K. Larsen and A. Skou, editors, CAV 91: Computer-aided Verification, Lecture Notes
in Computer Science 575, pages 376--H398. Springer-Verlag, 1991.
[NSY92] X. Nicollin, J. Sifakis, and 5. Yovine. Compiling real-time spedfications into extended
automata. IEEE Transactions on Software Engineering, SE-18(9):794--H804, 1992.
[NSY93] X. Nicollin, J. Sifakis, and 5. Yovine. From ATP to timed graphs and hybrid systems.
Acta Informatica, 30:181--H202,1993.
[QS81]
J. Quellie and J. Sifakis. Specification and verification of concurrent systems in CESAR.
In M. Dezani-Ciancaglini and U. Montanari, editors, Fifth International Symposium on
Programming, Lecture Notes in Computer Science 137, pages 337--H351. Springer-Verlag,
1981.
J. Sifakis. A unified approach for studying the properties of transition systems. Theo-
retical Computer Science, 18:227--H258,1982.
40
[Sif82]
