BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR94-1403
ENTRY:: 1994-03-17
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Real-Time System = Discrete System + Clock Variables
AUTHOR:: Alur, Rajeev 
AUTHOR:: Henzinger, Thomas A.
DATE:: January 1994
PAGES:: 34
ABSTRACT::
How can we take a programming language off the shelf and upgrade it into 
a real-time programming language? Programs such as device drivers and plant 
controllers must explicitly refer and react to time. For this purpose, a 
variety of language constructs-including delays, timeouts, and watchdogs-has 
been put forward. We advocate an alternative answer, namely, to designate 
certain program variables as clock variables. The value of a clock variable 
changes as time advances. Timing constraints can be expressed, then, by 
conditions on clock values. A single new language construct-the guarded wait 
statement-suffices to enforce the timely progress of a program.

Our presentation proceeds in two steps. First, we extend untimed systems 
(Section 1) with clock variables (Section 2); then we introduce the guarded 
wait statement (Section 3). The usage of clock variables and the guarded wait 
statement is illustrated with real-time applications such as round-robin 
(timeout-driven) scheduling, priority (interrupt-driven) scheduling, and 
embedded process control (Section 4). Indeed, clock variables generalize 
naturally to variables that measure environment parameters other than time 
(Section 5). In keeping with an expository style, all references are 
clustered in bibliographic remarks at the end of each section. We conclude by 
pointing to selected literature on formal methods and support tools for our 
approach to real-time programming (Section 6).
END:: CORNELLCS//TR94-1403
BODY::
Real-Time System
Discrete System + Clock Variables*
Rajeev Alur
Thomas A. Henzinger**
TR 94-1403
January 1994
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
* A preliminary version of this paper appeared in the Proceedings of the First AMAST
Workshop on Real-Time Systems, Iowa City, IA, 1993.
** 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.
R?eal-time Systen?
Discrete Systen? + Clock Variables*
Rajeev Alur
AT&T Bell Laboratories
600 Mountain Avenue
Murray Hill, NJ 07974
alur?research.att.com
Thomas A. Henzingert
Computer Science t)epartment
Cornell University
Ithaca, NY 14S53
tah?cs.cornell.edu
How can we take a programming Thnguage off the shelf and upgrade it into a
real-time programming language? Programs such as device drivers and plant
controllers must explicitly refer and react to time, For this purpose, a variety
of language constructs including delays, timeouts, and watchdogs has been
put forward, We advocate an alternative answer, namely, to designate certain
program variables as clock variables, The value of a clock variable changes as
time advances, Timing constraints can be expressed, then, by conditions on
clock values, A single new language construct?the guarded wait statement
suffices to enforce the timely progress of a program.
Our presentation proceeds in two steps. First we extend untimed systems
(Section 1) with clock variables (Section 2); then we introduce the guarded wait
statement (Section 3). The usage of clock variables and the guarded wait state-
ment is illustrated with real-time applications such as round-robin (timeout-
driven) scheduling, priority (interrupt-driven) scheduling, and embedded pro-
cess control (Section 4). Indeed, clock variables generalize naturally to variables
that measure environment parameters other than time (Section 5). In keeping
with an expository style, all references are clustered in bibliographic remarks
at the end of each section. We conclude by pointing to selected literature on
formal methods and support tools for our approach to real-time programming
(Section 6).
A preliminary version of this paper appeared in the Proceedings of the First AMAST
Workshop on Real-time Systems, Iowa City, IA 1993.
tFartially supported by the National Science Foundation under grant CCR?92OO794 and
by the United States Air Force 0flice of Scientific Research under contract F49620-93-1-oo56.
1 Untimed Systems
1.1 States
At any time, the state of a system is determined by the values of a finite set of
variables. For example, the state of a chess game is determined by the hoard
positions of all pieces and a bit that indicates whether white or black gets to
move next; the state of a circuit is determined by the boolean values of all
wires and flip-flops; the state of a while program is determined by the value of
the program counter and the values of all program variables (the state of a C
program, by contrast, is determined by the values of all memory locations that
contain the run-time environment of the program).
We use V as the finite set of variables. We assume that all variables in V are
typed and use suggestive names like m and n for nonnegative integer variables
and x and y for real-valued variables. A state is a function that maps every
variable in V to a value of the corresponding type.
A state predicate is a proposition that is either true or false for each state.
For example, the proposition "The black king is attacked by the white queen"
is either true or false for each state of a chess game; the proposition "All output
wires are low" is either true or false for each state of a circuit: the proposition
= n + 2" is either true or false for each state of a while program.
Formally, a state predicate is a formula of predicate logic whose free variables
are taken from V. The truth value of the state predicate ? for the state a is
obtained by interpreting each free variable v in ? as a(v). For example, the
state predicate ? = n + 2 is true for a state a iff a(m) = a(n) + 2. Every state
predicate ? defines, then, the set of states, denoted by [[??, for which ? is true.
1.2 Actions
The state of a system changes over time. We refer to the state changes of a
system as actions. An action is a pair (a, a') of states that consists of a source
state a and a target state a'. Intuitively, if a system is in the source state a
then the action (a, a') takes the system into the target state a'. N\? say that
an action is enabled in its source state and disabled in all other states. Two
actions (a1, a') and (a2, a'2) are consecutive if the second action is enabled in
the target state of the first action i.e., if a; = a2. The action (a, a') is a null
action if a = a
Null actions arise in two situations. First, every state provides a system
description that is necessarily abstract- i.e., given at a certain level of detail.
Consequently, any action that modifles only detail that is not included in a state
appears as a null action. Recall, for instance, that we represent the state of a
while program by values for the program counter and the program variables.
So the action "Load the value of m into the accumulator," which, at a level
of greater detail, may be part of the execution of a while program, appears as
2
a null action, because it changes neither the value of the program counter nor
the value of any program variable. Second, every system is embedded in an
environment. Any environment action that does not modify the system state
appears also as a null action.
An action predicate is a proposition that is either true or false for each
action. For example, the proposition "A black piece is captured" is either true
or false for each move of a chess game; the proposition "Some output wire goes
from low to high" is either true or false for each clock cycle of a synchronous
circuit; the proposition "The value of in is incremented" is either true or false
for each execution step of a while program.
When describing an action, we use variables like v ? V to refer to the value
of v in the source state of the action, and primed variables like v' ? V to refer
to the value of v in the target state of the action. The action predicate "The
value of m is incremented," for instance, will be written as "m' = m + 1"; that
is, the new value of rn is one greater than the old value of m.
Formally, let V' be the set of primed variables whose unprimed versions occur
in V. An action predicate is a formula of predicate logic whose free variables
are taken from V and V'. The truth value of the action predicate ii for the
action (.,.`) is obtained by interpreting each free unprimed variable v in ?`
as ?(v) and each free primed variable v' in ii as &(v). For example, the action
predicate m' = m + 1 is true for an action (.,&) iff &(m) = ?(m) + 1. Every
action predicate i4? defines, then, the set of actions, denoted by [[il?, for which ?
is true.
1.3 Behaviors
We restrict ourselves to systems that are nondeterministic, discrete, and closed.
While the actions of a probabilistic system occur with certain likelihoods, each
action of a nondeterministic system is, in every state, either possible (enabled) or
impossible (disabled). While a continuous system-?such as the solar system
may perform infinitely many actions in a finite interval of time, the behavior
of a discrete system results from a countable sequence of actions. While the
behavior of an open system may depend on the environment of the systeni, every
environment action of a closed system appears as a null action. We assume that
the environment never terminates; the actions of a system that terminates after
a finite number of actions are, therefore, followed by infinitely many null actions.
A behavior of a system, then, is a countably infinite sequence of states.
Alternatively, a behavior & = ?i, ?1, a2, .3.... can be viewed as the countably
infinite sequence of actions (oi. a?+i), integer i > 0 with the property that any
two neighboring actions are consecutive. For example, a legal sequence of moves
possibly interspersed with null actions, constitutes a behavior of the game of
chess; a sequence of consecutive execution steps, possibly interspersed with null
actions, constitutes a behavior of a given while program.
We use state and action predicates to describe behaviors. A state predicate
restricts the first state of a behavior: the state predicate ? is initially true for
the behavior a if ? is true for the first state of a. An action predicate restricts
all actions of a behavior except for environment actions: the action predicate ?
is invariantly true for the behavior a if ii is true for all actions of a that are not
null actions, Consider, for instance, the behavior a whose odd actions, starting
from 0, increment the value of m and whose even actions are null actions:
= 0,1,1,2,2,3,3,..
The state predicate m = 0 is initially true for a and the action predicate m? =
rn + 1 is invariantly true for 0.
1.4 Systems
A system defines a set of possible behaviors. For example, the game of chess
defines the initial board configuration and the set of all legal move sequences; a
while program defines a set of execution-step sequences, one sequence for each
combination of input values.
Formally, a system S = (?o, ii?) is a pair that consists of a state predi-
cate ?0?the initial condition of S and an action predicate ??---Hthe transition
condition of S. The behavior 0 is a behavior of the system 8 if (1) the initial
condition ?o is initially true for 0 and (2) the transition condition u'? is invari-
antly true for 0. Every system 8 defines, then, the set of its behaviors, which
is denoted by ?S?.
Consider, for instance, the system 8o that, starting froni 0., increments the
value of m arbitrarily often. The system S0 has the initial condition m = 0 and
the transition condition m' = m + 1. here are some behaviors of S0:
0i(m)			=			0 1 2 3 4 5
02(m)			=			0,1,1,2,2,3,3,4,..
=			0 0 0 1 2 2 2,3,4,..
04(m)			=			0 1 2 2 2 2 2,2,2,2,...
Not every set of behaviors can be defined by a system. First a system
cannot prevent environment actions: if, between any two actions, we add a null
action to a behavior of the system 8, then we obtain another behavior of 8
(this property of systems is called stutter closure). Second, the future evolution
of a system is determined completely by the current state of the system and is
independent of the past history of the system: if two behaviors Oi and 02 of
the system 8 share a state a, then by composing the past of a according to Oi
and the future of a according to 02 we obtain another behavior of 8 (fusion
closure). Third, the operation of a system is characterized completely by local
conditions on individual states and actions and there are no global conditions on
the behaviors of a system: if all finite prefixes of a behavior 0 can be extended
4
program NdUpDown:
initially m := 0; n = 1;
loop trne
or			rn =
or			m =
end.
___ m := 1
0			n := n + 1
I A n > 0			n := n --H 1
Figure 1: Guarded-command program
to behaviors of the system S, then a itself is a behavior of S (limit closttre).1
The three closure properties of systems have two important ramifications on
the executability of systems. First the behaviors of a system can be generated
action by action: start with a state for which the initial condition is true and
repeatedly choose either a null action or an enabled action for which the transi-
tion condition is true. Second, a system need not progress: when generating a
behavior action by action, from any point on we may choose null actions only.
1.5 Programs
We use a guarded-command programming language to define systems. A ?ua?d-
ed-command program P consists of a set of assignments, which defines the initial
condition of?, followed by a set of guarded commands, which defines the tran-
sition condition of ?. The program P is executed in a stepwise fashion: first,
starting from any state, execute the inital assignments to obtain an initial state
of D; then continue to select, nondeterministically, either a null action or a
guarded command whose guard is true. We write [[P? for the set of execution
sequences of the guarded-command program P.
Consider, for instance, the guarded-command program NdUpDown of Fig-
ure 1. The program NdUpDown starts from an initial state a with a(m) = 0
and a(n) = 1. The value of n is incremented arbitrarily often before the program
may change the value of m to 1. Thereafter, the value of n may be decremented
repeatedly as long as it remains nonnegative.
The guarded-command program NdUpDown defines a system whose be-
haviors are the execution sequences of NdUpDown. The initial condition of
NdUpDown is given by the state predicate ?o and the transition condition of
1Conversely, if we adrnit infinitary forennias as state and action predicates, then every set
of behaviors that is closed under stuttering, fusion, and limits is definable by a system.
5
NdUpDown is given by the action predicate `?:
= 0 A n = 1)
= 1)n V
(m=OAn'=n+1)m v
= 1 A n > 0 A n' = n --H 1)m
The expression (?)?v, for an action predicate `1) and a vector v of variables,
is an abbreviation for the action predicate ? A ?v' --H v; that is, the variables
listed as a subscript remain unchanged. Each guarded command of the program
NdUpDown contributes a disjunct called an action schema to the transition
condition. We leave it to the reader to translate an arbitrary guarded-command
program ? into an initial condition and a transition condition that generate the
set [[?? of behaviors.
Bibliographic remarks. Our system model is fairly standard, provided one
accepts the interleaving view of concurrent activities (see, for example, the TLA
approach of Lamport [Lam9i] and the transition system approach of Manna and
Pnueli [MP92]). As a word of caution, we point out that our actions are pairs
of states rather than, as in TLA, sets of pairs of states. Our choice leads to
a pleasant parallelism between state predicates and action predicates: a state
predicate defines a set ofstates; an action predicate defines a set of actions. Stut-
ter closure has been advocated by Lamport [Lam83]; limit closure (safety) was
formally defined by Alpern, Demers, and Schneider [ADS86j; the relationship
between systems and closure properties was studied by Emerson [Eme83J; the
executability (machine closure) of systems, by Apt, Francez, and Katz [AFK88].
Guarded commands were introduced by Dijkstra [Dij75j; our guarded-command
language is inspired by the UNITY language of Chandy and Misra [CM88].
2 Timed Systems 1: Safety
2.1 Clocks and delays
The state of a timed system is determined by two kinds of variables system
variables and clock variables. The value of each system variable is changed ex-
plicitly by the transition condition of the system; the value of each clock variable
increases implicitly as time advances. Formally, we partition the finite set V
of variables into system variables and clock variables. The clock variables or
clocks range over the nonnegative real numbers. We reserve the letters x, y,
and z for clocks. Given a state 0 and a nonnegative real number 6, we write
0 + 6 for the state that maps all system variables m to 0(?) and all clocks x
to o(x) + 6.
The behavior of a timed system results from two kinds of actions system
actions and time actions. System actions update the values of the system vari-
ables and reset some of the clocks to 0; time actions do not modify the value
6
of any system variables and uniformly advance the values of all clocks. It is
perhaps best to think of time actions as environment actions: the environment
can advance time and, in doing so, increases the values of the clocks by the same
amount; the system, on the other hand, has only one way of changing the value
of a clock, namely, to restart it. In other words, timed systems are open systems
whose environment actions appear as both time actions and null actions.
Formally, the action (?, a') is asystem action iffor all clock variables x, either
= a(x) or a'(x) = 0; the action (a, a') is a time action--H-?r delay if there
is a nonnegative real 6?the duration of the delay such that & = a+6. System
actions have duration 0. Every null action is, by definition, both a system action
and a delay of duration 0.
We henceforth write (a, 6) for a delay with source state a and duration 6. A
state a' is passed by the delay (a, 6) if a' = a+e for some nonnegative real e < 6.
In particular, no state is passed by a null action, and while the source state a
is passed by a delay (a, 6) with positive duration 6 > 0, the target state a + 6
is not passed by the delay (a, 6)
A timed behavior of a system, then, is a countably infinite sequence of system
actions and delays such that any two neighboring actions are consecutive. Given
a timed behavior a, let 6? be the duration of the i-th action of a. The timed
behavior a diveryes if the infinite sum Zi>0 6j of durations diverges. A state a
occurs in the timed behavior a if either a Th the source state of a system action
of a, or a is passed by a delay of a.
2.2 Clock constraints
State sets and action sets of timed systems are, as before, defined by formulas
of predicate logic with free variables from V and V'. We restrict, however, the
way in which clocks may appear in such formulas to rule out timed systems that
within a finite interval of time make infinitely many decisions on how to proceed.
For example, we do not wish to consider system actions that are enabled iff the
value of a certain clock is rational.
Let (a, 6) be a delay, let ? be a state predicate, and let ? be an action
predicate. The characteristic function of ? maps each nonnegative real e < 6 to
1 if ? is true for a+ e, and otherwise to 0; the characteristic function of ii maps
e to 1 iff ? is enabled in a+e. A state or action predicate varies finitely over the
delay (a, 6) if its characteristic function has finitely many discontinuities in the
interval (0, 6). Abstractly, we restrict ourselves to state predicates and action
predicates that vary finitely over all delays.
Concretely, we offer a syntax for the timed systems that base their decisions
on comparisons of clock values with each other and with integer constants: a
clock constraint is a formula of the form x < d, c < y, or x + c ? y + d, where x
and y are clocks, and c and d are nonnegative integers. Moreover, every system
action leaves the value of a clock either unchanged or reset to 0: a reset condition
is a formula of the form x' = x or x' = 0, for a clock v.
7
A timed state predicate, then, is a formula of predicate logic whose free vari-
ables are taken from V such that all clocks occur in clock constraints only; a
timed action predicate is a formula of predicate logic whose free variables are
taken from V and V, such that all clocks and primed clocks occur in clock con-
straints and reset conditions only (in particular, all primed clocks of a timed
action predicate occur in reset conditions only). ?Vhile, for example, the for-
mulay < x < y+3 Az = x+1 is atimedstate predicate, the fom?ulas x+y = 3
and 2x < y are not. It is not difficult to check that every timed state predicate
and every timed action predicate varies finitely over all delays.2
The timed action predicate ii is invariantly Irne for the timed behavior a if n
is true for all actions of a that are not delays. Consider, for instance, the timed
behavior 0 whose even actions increment the value of the system variable in
and restart the clock x, and whose odd actions are delays of duration 2:
0(in, x) = (0,0), (0,2), (10), (1,2), (2,0), (2.2), (3,0), (3,2), (4,0),
The timed action predicate x = 2 A in' = in + 1 A x' = 0 are invariantly true
for a.
2.3 Clock-constrained systems
A clock-constrained system 8 = (?o ??) is a pair that consists of a timed state
predicate ?o the initial condition of 8 and a timed action predicate ?`?? the
transition condition of 8. The timed behavior a is a behavior of the clock-
constrained system 8 if (1) the initial condition of 8 is initially true for 0
and (2) the transition condition of 8 is invariantly true for 0. Every clock-
constrained system 8 defines, then, the set of its divergent behaviors which is
denoted by [[8?.
Consider, for instance, the clock-constrained system Si that, starting from 0,
increments the value of in arbitrarily often such that the time difference between
consecutive increment operations is at least 1 time unit and at most 2 time
units. The system Si has the initial condition m = 0 A x = 0 and the transition
condition 1 < x < 2 A in' = m + 1 A x' = 0. Here are some divergent behaviors
ofSi:
0i(in, x)			=
02(in,x)			=
03(in,x)			=
04(in,x)			=
(0,0), (0,1), (1,0), (1,1), (2,0), (2,1), (3,0),
(0,0), (0,2), (1,0), (1,2), (2,0), (2,2), (3,0),...
(0,0), (0,0.5), (0,1.2), (1,0), (1,0), (1,1.5), (2,0),.
(0,0), (0,1), (0,1.5), (0,2), (0,10),..
2This is the case also for timed state and action predicates that are infinitary formulas,
because the set V of variables is finite. Conversely, there is an infinitary formula with addition
of clocks that does not vary finitely over all delays (` = 1 v 2r = 1 v 3x = ? v...). Decidability
considerations, too, suggest the restriction of clock constraints to successor and comparison
operations on clocks.
8
Not every set of divergent timed behaviors can be defined by a clock-con-
strained system. First, the options of a clock-constrained system change only
finitely often within a finite interval of time: the transition condition `y'? of
8 varies finitely over all delays of behaviors of 8 (finitely varying 6ranching).
Second, if we split a delay of a behavior of 8 into two consecutive delays1 or if
we merge two consecutive delays of a behavior of 8 into a single delay, then we
obtain another behavior of S (closure under timed stuttering; as a delay may be
split into itself followed by a mill action, closure under timed stuttering implies
stutter closure). Third, the behaviors of 8 are closed under fusion and, fourth,
under divergent limits: if all finite prefixes of a divergent timed behavior a can
be extended to behaviors of 8, then a itself is a behavior of 8 (as the infinite
sequence of null actions is not a behavior of 8, no clock-constrained system is
closed under limits). Fifth, a clock-constrained system cannot prevent delays:
if a finite prefix of a behavior of 8 is extended by a delay, then we obtain again
a prefix of a behavior of 8 (closure under waiting).
Consequently, the divergent behaviors of a clock-constrained system can be
generated action by action: (1) start with a state for which the initial condition
is true and repeatedly choose either a delay or an enabled action for which the
transition condition is true; (2) to generate divergent timed behaviors, make
sure to choose appropriate delays??i.e., choose a sequence of delays whose sum
diverges. Furthermore, a clock-constrained system need not progress: when
generating a divergent behavior action by action, from any point on we may
choose delays only.
2.4 Clock-constrained programs
A clock-constrained program P consists of a set of assignments followed by a set
of guarded commands such that (1) all assignments to clocks are of the form x
o and (2) all guards are timed state predicates. The program ? is executed in a
stepwise fashion: first, starting from any state, execute the inital assignments to
obtain an initial state of P; then continue to select, nondeterministically, either
a delay or a guarded command whose guard is true. We write ?P? for the set
of divergent execution sequences of the clock-constrained program ?.
Consider, for instance, the clock-constrained program Cc UpDown of Fig-
ure 2. The program CcUpDown contains a system variable, n, and two clocks
x and y. The program starts from an initial state in which n has the value 1
and both x and y have the value 0. Within the first 10 time units, the value
of n is incremented arbitrarily often as long as the time difference between con-
secutive increment operations is at least 1 time unit and at most 5 time units.
Beginning at time 12, the value of n may be decremented repeatedly, under the
same timing constraints, as long as n remains nonnegative.
The clock-constrained program Cc UpDown defines a clock-constrained sys-
tem whose behaviors are the divergent execution sequences of Cc UpDown. The
initial condition of Cc UpDown is given by the timed state predicate 4)o and the
9
program Cc UpDown:
declare x, y: clock;
initially n := 1; x := 0; y := 0;
loop x<10A l<y<S n:=n+1; y:=O
or x> 12 A 1 < y < 5 A n> 0 n n --H 1; y := 0
end,
Figure 2: Clock-constrained program
transition condition of Cc UpDown is given by the timed action predicate ??:
= 1 A x = 0 A y = 0)
< 10 A 1 < y ? 5 A n' = n + 1 A y' = 0)? V
> 12 A 1 < y < 5 A n> 0 A n' = n --H 1 A y' =
Each guarded command of the program CcUpDown contributes a disjunct---
called a syslem action schema to the transition condition. ??Te leave it to the
reader to translate an arbitrary clock-constrained program ? into an initial con-
dition and a transition condition that generate the set [[?) of timed behaviors.
Bibliographic remarks. Clock variables---as we use them were first intro-
duced in temporal logic [A1189j (originally as so-called "freeze" quantifiers) and
in finite automata [AD9o]. Both papers realized the importance of the choice
of clock constraints that are admitted by a system; this choice has immediate
ramifications on semantic issues and verification problems. The dichotomy of
system actions versus time actions, which had been advocated repeatedly by
various proponents of the interleaving view of concurrency, was perhaps stan-
dardized by the real-time system model of timed transition systems [HNlP91J.
In particular, the timed transition system model has led to the study of closure
under timed stuttering, divergent limits (divergence safety)., and finitely varying
branching [11en91, Hen92, HNSY92j.
3 Timed Systems 2: Progress
3.1
Delay predicates
Neither untimed systems nor clock-constrained systems need to progress??. e.,
at any point a system may fail to perform another action while the environment
keeps performing actions. To ensure the progress of an untimed system, one
typically assumes fairness requirements on the system actions: a system action
must not be enabled forever (or infinitely often) without being taken. To ensure
the progress of a timed system', it will suffice to assume a fairness requirement
10
on the time actions: time must advance beyond any bound. While we have seen
that a restriction to divergent timed behaviors does not ensure progress per se,
we will use the divergence of time to enforce system actions by constrailling
time actions. For this purpose, we introduce delay predicates. A delay pred-
icate typically enforces a system action by limiting the amount by which the
environment may advance time in a given state.
A delay predicate is a proposition that is either true or false for each de-
lay. For example, tbe proposition "Throughout the delay, the clock x shows
at most 5" is either true or false for a delay; we will write this proposition
as "x < 5," using variables like x to refer to the value of x in all states that
are passed by the delay. The delay predicate x < 5, then, prevents time from
advancing past a state in which the value of the clock x is 5.
Formally, the syntax of delay predicates is identical to the syntax of timed
state predicates. The delay predicate ? is true for a delay if ?, viewed as a
timed state predicate, is true for all states that are passed by the delay. For
example, the delay predicate x < 5 is true for a delay (a, 6) iff a(x) + 6 < 5
(since, by definition, the target state of a delay is not passed by the delay, the
delay predicates x < 5 and z < 5 are true for the same delays). Every delay
predicate ? defines, then, the set [[x? of delays for which ,? is true. In particular,
the set ??? contains all null actions and is closed under both the splitting and
the merging of delays; that is, a delay predicate ? is true for two consecutive
delays (a, 6i) and (a + 6i, 62) iff ? is true for the combined delay (a, 6i + 62).
While a timed action predicate restricts the system actions of a timed be-
havior, a delay predicate restricts the delays of a timed behavior. The delay
predicate ? is invariantly true for the timed behavior a if ,y' is true for all delays
of a. Consider again the timed behavior a whose even actions increment the
value of the system variable m and restart the clock x, and whose odd actions
are delays of duration 2:
a(m, x) = (0,0), (0,2), (1,0), (1,2), (2,0), (2,2), (3,0), (3,2), (4,0),
The delay predicate x < 2 is invariantly true for a; the delay predicate x # 1 is
not.
3.2 Real-time systems
A real-time system S = (?o, ??, xo) is a triple that consists of a clock-con-
strained system (?o, #`?) and a delay predicate ,?o the environment condition
of S. The timed behavior a is a behavior of the real-time system 8 if (1) a is a
behavior of the clock-constrained system that underlies 8 and (2) the environ-
ment condition of 8 is invariantly true for a. Every real-time system 8 defines
then, the set of its divergent behaviors, whicb is denoted by ?8?.
The transition condition of a real-time system asserts necessary conditions
on system actions and the environment condition asserts sufficient conditions on
11
system actions. For example, the following real-time system S2 = (?o, ??, xn)
changes the value of m from 0 to 1 at time 3 at the earliest and at time 5 at the
latest:
= (m = 0 A x = 0)
4 = (x> 3 A m' = 1)
=			= 0 A x < 5) v
While the requirement x > 3 of the transition condition ensures the lower time
hound of 3?the system transition that changes the value of m may happen at
or after time 3 the requirement x < 5 of the environment condition ensures the
upper time bound 5 the transition must happen at or before time 5, because
time cannot advance past 5 before the value of Tn has changed to 1.
Not every set of divergent timed behaviors can be defined by a real-time
system. While all real-time systems exhibit finitely varying branching and are
closed under timed stuttering, fusion, and divergent limits: they are not nec-
essarily closed under waiting. This is because the environment condition can
enforce the progress of a real-time system.
3.3 Real-time executability
There is a price to be paid, however, for progress: the divergent behaviors of a
real-time system may no longer be generated action by action. By starting with
a state for which the initial condition is true and repeatedly choosing either a
delay that does not violate the environment condition or an enabled action for
which the transition condition is true, we may be led into a situation from which
time cannot diverge.
Consider, for example, the following variant Sz of the real-time system S2:
= = 0 A x = 0)
4 = (3<x<5Am'=1)
= (m = 0 A x < 10) v
The real-time systems S2 and Sz have the same divergent behaviors--H-formally,
[[S2? = ?Sz??namely, all divergent timed behaviors in which the value of m
changes from 0 to 1 at time 3 at the earliest and at time 5 at the latest. Only the
real-time system S2, however, can be executed in a stepwise fashion. Executing
the real-time system S? we might start from the initial state by choosing a
delay of duration, say, 8, which does not violate the environment condition.
But there is no divergent continuation from the resulting state a with a(rn) = 0
and a(x) = 8: we have painted ourselves into a corner by having chosen an
initial delay whose duration was greater than 5.
Real-time systems that do not exhibit this problem are called nonzeno: a
real-timed system S is nonzeno if every finite prefix of a behavior of S is a
12
finite prefix of a divergent behavior of S. In particular, while the real-time
system S2 is nonzeno, the real-time system Sz is not. Nonzenoness, then, is
a property of a real-time system (syntax) rather than a property of a set of
timed behaviors (semantics). Indeed, every set of timed behaviors that can be
defined by a real-time system can also be defined by a nonzeno real-time system,
whose environment condition is suitably strengthened. For instance, the real-
time system Sz can be transformed into an equivalent nonzeno real-time system
by strengthening the environment condition to (x < 5) v (m 1).
3.4 Rea1-tjme programs
A guarded wait statement is an instruction of the form y wait, where the
guard ? is a delay predicate. A guarded wait statement delays the program
execution by an arbitrary amount of time, but at most until the guard, viewed as
a timed state predicate, becomes false. The guarded wait statement ? wait
results, then, in a delay that satisfies the delay predicate ,?. In particular,
the guarded wait statement false wait results in a null action, and the
guarded wait statement true wait results in a delay of arbitrary duration.
We generally prefer the guard x < 5 over the equivalent delay predicate x < 5,
perhaps because we like to think of the guarded wait statement x < 5 wait
as delaying execution as long as the value of x is less than 5, and terminating
as soon as the value of x becomes 5.
A real-time program P is a clock-constrained program that contains guarded
wait statements in addition to guarded commands. The program ? is executed
in a stepwise fashion: first, starting from any state, execute the inital assign-
ments to obtain an initial state of T'; then, continue to select, nondeterminis-
tically, either a guarded wait statement or a guarded command whose guard
is true. Since it may not be possible to merge the consecutive execution of
two different guarded wait statements into a single execution step, the resulting
set [?] of divergent execution sequences is not necessarily closed under timed
stuttering. The set ?P? of behaviors of the real-time program P, therefore, is
defined as the timed stutter closure of [PJ?i. e.,the smallest superset of [P]
that is closed under timed stuttering.
Consider, for instance, the real-time program lltUpDownl of Figure 3. The
program Ri UpDownl behaves like the clock-constrained program Cc UpDown
except that the value of n must be incremented or decremented (depending on
how much time has elapsed since the program was started) at least once every
5 time units, until n reaches the value 0.
The real-time program RtUpDownl defines a real-time system that has the
same behaviors. The initial condition of Rt UpDownl is given by the timed
state predicate ?o, the transition condition of RtUpDownl is given by the timed
action predicate ??, and the environment condition of Rt UpDownl is given by
13
program ?tUpDawnI:
declare x, y: clock;
initially n 1; x := 0; y 0;
loop x < 10 A y > 1
or n?0Ax>12Ay>1
or n > 0 A y < 5
or n = 0
end.
n := n + 1; y := 0
n --H 1; y := 0
wait
wait
the delay predicate )co
Xo =
Figure 3: Real-time program
= 1 A x = 0 A y = 0)
< 10 A y > 1 A n' = n + 1 A y, = 0)? v
> 12 A y > 1 A n> 0 A n' = n --H 1 A gi = 0)x
(n> 0 A y < 5) v
Each guarded command of the program ?t UpDowni contributes disjunct (a sys-
tem action schema) to the transition condition, and each guarded wait statement
of RtUpDowni contributes a disjunct?called a delay schema?to the environ-
ment condition. We leave it to the reader to translate an arbitrary real-time
program ? into an initial condition, a transition condition, and an environment
condition that define the set ?D? of timed behaviors. A clock-constrained pro-
gram, in particular, is a real-time program with the guarded wait statement
trae wait, which yields the environment condition true.
The execution strategy for real-time programs succeeds only if it cannot lead
to a state from which there is no divergent continuation of actions. A real-time
program D, then, is executable if it defines a nouzeno real-time system. The
real-time program Rt UpDownj, for example, is not executable. To see this
observe that the stepwise execution of RlUpDowni may lead to a state a with
= 5, a(x) = 11, and a(y) = 5, and there is no divergent sequence of actions
continuing from (7. Figure 4 shows an executable real-time program that has the
same behaviors as ?tUpDown1. The environment condition of the executable
program RtUpDown2 is
xo: (x <10 A y <5) V (x > y+7 A y< 5) v (n = 0).
The real-time program RtUpDown2 terminates i.e., the value of n reaches 0
and execution continues with delays only within at most 75 time units (to
calculate this time bound on the termination of RtUpDown2, observe that the
value of n can be at most 12 when x = 11).
14
program R?UpDown2:
declare x, y: clock;
initiallyn:=l; x:=O; y:=O;
loop x?<1OAy>1
or n > 0 A x> 12
or x < 10 A y < 5
or x > y +7 A y < 5
or n = 0
end.
n:=n+1; y:=O
A y> 1 n:=n--H1; y:=0
wait
wait
wait
Figure 4: Executable real-time program
Bibliograpbic remarks. Nonzenoness (timed executability) was defined inde-
pendently by several researchers [AL92, 11en92]; Abadi and Lamport coined the
phrase. The first proposal for environment conditions as a means of ensuring the
progress of a timed system advocated the use of program invariants [llNSY92];
that paper also presents an algorithm for transforming a real-time system into
an equivalent nonzeno system. The real-time program RtUpDownl is derived
from an example, due to Pnueli [HMP9lj, that illustrates that an increase in the
lower bound on the duration of a delay may lead to a decrease in the running
time of a program (to see this, replace the lower bounds of 1 on the clock y by 2;
then RtUpDown2 will terminate within 50 time units).
4 Real-time Programming
4.1 Sequential real-time processes
Our choice of guarded commands as programming language has largely been
instructionally motivated. In general, we may add clocks and guarded wait
statements to any programming language. To illustrate this thesis, we now
extend a language of while programs with clocks and guarded wait statements.
As in synchronous programming languages, all instructions of a while program
are executed immediately and instantaneously; all delays are indicated explicitly
by guarded wait statements.
It is convenient to introduce abbreviations for several common applications
of guarded wait statements. First, the instruction wait delays the program
execution for an arbitrary amount of time; it stands for the guarded wait state-
ment trtte wait. Second, the instruction wait watching ? delays the
program execution for an arbitrary amount of time, but at most until the
timed state predicate ? becomes true; it stands for the guarded wait state-
ment ?? wait. Third, the instruction await ? delays the program execu-
15
program RtUpDown3:
declare z, y: clock;
n := 1; x 0;
wait [1,5];
while x < 10 do
n:=n+1; y:=O;
repeat
if z < y+7
then wait watching x > 10 v y > 5
else wait watching y > 5
fi
until y > 1
od;
repeat wait watching y> 5 until x> 12;
while n > 0 do
n			n --H 1;
wait [1,5]
od.
Figure 5: Real-time while program
tion precisely until the timed state predicate ? becomes true; it stands for the
program segment
repeat wait watching ? until ?.
Fourth, the instruction wait [c, di delays the program execution at least c and
at most d time units, for nonnegative integers c and d with c ? d' it stands for
the program segment
z := 0; repeat wait watching z > d until z> c
where z is a new clock. We write wait c short for wait [cc],
Now consider the real-time while program RtUpDown3 of Figure 5. We
present a formal semantics for real-time while programs such that the pro-
gram RtUpDown3 defines essentially the same real-time system as the guard-
ed-command program ?tUpDown2 of Section 3,4.
We construct the real-time system that is defined by a while program T'
by encoding the control structure of T' as a formula. For this purpose, we
introduce a new system variable--Hthe program connier PC that ranges over
the control locations of D. If ?o is the initial control location, then the initial
condition of P is PC = o. An execution step of ? is a move between control
locations and corresponds to the execution of a guarded command (typically, an
16
assignment or a test) or the execution of a guarded wait statement. Each such
execution step contributes a system action schema to the transition condition
of P; each guarded wait statement contributes, in addition, a delay schema to
the environment condition of P.
Consider, for example, the initial program segment
0: n := 1; ? : x =0
of the while program RtUpDown3; it contributes the system action schema
(pc = o A pc? = i A n' =
to the transition condition of RtUpDown3. The program segment
2: wait watching x >10 v y >5 ? until y > 1
contributes to the transition condition of IttUpDown3 the system action schema
(pc = 2 A pc' =
and contributes to the environment condition of RtUpDown3 the delay schema
(pc = 2 A x < 10 A y < 5).
We leave it to the reader to define the transition condition of 1?IUpDown3
as the disjunction of all system action schemata and the environment con-
dition of RtUpDown3 as the disjunction of all delay schemata. If we adjust
the resulting timed behaviors by (1) projecting out the program counter and
(2) merging certain consecutive states (for example, the consecutive assign-
ments n := n + 1; y := 0 of the while program RtUpDown3 constitute a
single action of the guarded-command program ?tUpDown2), then we obtain
precisely the real-time system that is defined by the guarded-command pro-
gram RtUpDown2. It follows, in particular, that the real-time while program
RtUpDown3 is executable.
4.2 Concurrent real-time processes
So far, we have discussed sequential processes and sequential real-time processes.
We now illustrate that concurrent processes, too, accommodate naturally the
introduction of timing constraints through clocks and guarded wait statements:
while every concurrent while program defines a system, every concurrent real-
time program defines a real-time system.
The actions of concurrent untimed processes are interleaved. Consider, for
instance, the concurrent while program Par Up of Figure 6. The program Par Up
consists of two independent processes. The ?`lett" process repeatedly increases
the value of the variable m; the ?right" process repeatedly increments the value
17
program Par Up:
initially rn := 0; n := 0;
cobegin
loop 0: m			m + 1; 1: m := rn + 2 end
loop k0:n:=n+lend
coend.
Figure 6: Concurrent while program
of n. A behavior of Par Up interleaves, without regard to any fairness require-
ments, null actions with actions of either process: an action of the left process
may be followed by any number of actions of the right process, and vice versa.
llere are some behaviors of Par Up:
?(rn,n)			=
cr2(m,n)			=
a3(m,n)			=
T4(m,n)			=
(0,0), (1,0), (1,1), (3,1), (3,2), (4,2), (4,3),...
(0,0), (1,0), (3,0), (4,0), (6,0), (6,1), (7,1),
(0,0), (0,1), (0,2), (0,3), (1,3), (1,4), (1,5),
(0,0), (0,1), (0,1), (1,1), (3,1), (4,1), (4,2),
The behavior al, for example, alternates the actions of both processes.
To define the semantics of the program Par Up formally, we use two program
counters, left and right---Hone for each process (since the right process has a single
control location, there is actually no need for the program counter right in this
example). Each execution step of either process contributes an action schema
to the transition condition of Par Up. The concurrent program Par Up defines,
then, the system with the initial condition ?? and the transition condition ??:
(left = o A right = k0 A m = 0 A n = 0)
(left = o A left' = i A m' = m + 1)r?ht,n V
(left = j A left' = ? A m' = m + 2)r?ht,n V
= n + l)iqt,n??t,rn
The interleaving of the actions of concurrent untimed processes reflects an
underlying assumption that the execution speeds of the processes are unknown
independent, possibly very different and even varying. Timing constraints rela-
tivize the assumption of speed independence by ruling out certain interleavings
of the system actions of concurrent timed processes. This is because, while
the system actions of concurrent timed processes are interleaved, their delays
overlap.
Consider, for instance, the concurrent real-time program RtParUp of Fig-
ure 7. The real-time program RtParUp is obtained from the untimed program
18
program RtParUp:
initially m 0; n := 0;
cobegin
loop wait 3; m m + 1; wait 1; Tn := rn + 2 end
loop wait 7; n := n + 1 end
coend.
Figure 7: Concurrent real-time program
ParUp by adding delays between consecutive assignments. During the execu-
tion of RtParUp, a delay of the left process will overlap with one or more delays
of the right process, and vice versa. Also, a system action of the left process
may interrupt a delay of the right process, and vice versa.
Figure 8 shows the program RiParUp without abbreviations and annotated
with control locations. Here are two behaviors of RiParUp:
a?5(m,n,x,y)			=
a?6(m,n,x,y)			=
(0,0,0,0),(0,0,3,3),(1,0,3,3),(1,0,0,3),(1,0,1,4),
(3,0,1,4),(3,0,0,4),(3,0,3,7),(4,0,3,7),(4,1,3,7),
(0,0,0,0),(0,0,3,3),(1,0,3,3),(1,0,0,3),(1,0,1,4),
(3,0,1,4), (3,0,0,4), (3,0,3.7), (3,1,3,7), (4,1,3,7),
In particular, the timing constraints of RtParUp rule out the strict alternation of
system actions from the left process and the right process; that is, no behavior of
the real-time program RtParUp corresponds to the behavior ?i of the untimed
program ParUp.
When defining the semantics of RtParUp, each execution step of either pro-
cess contributes a system action schema to the transition condition of RtParup.
In addition, each pair of guarded wait statements?one from the left process and
the other one from the right process contributes a delay schema to the envi-
ronment condition of RtParUp. The concurrent real-time program RtParUp
defines, then, the real-time system of Figure 9. This real-time system is the
cartesian product of the two real-time systems that are defined by the compo-
nent processes.
4.3 Embedded real-time processes
At last, we illustrate our approach to real-time programming by designing typi-
cal application programs such as schedulers and embedded controllers. A sched-
uler is a real-time process that runs concurrently to the tasks that are being
scheduled; an embedded controller runs concurrently to continuous environment
processes.
19
program RtParUp:
declare x, y: clock;
initially rn			0; n			0;
cobegin
loop
0:x:=O; repeat
Tn := m + 1;
4:x:=0; repeat
7: m := m + 2
end
1: wait watching x >3 2: untilx >3
? wait watching x > 1 6: until x > 1'
II
loop
k0: y := 0; repeat k1: wait watching y > 7 k2: until y > 7;
k3: n := n + 1
end
coend.
Figure 8: Annotated concurrent real-time program
The simple round-robin scheduler RonndRobin of Figure 10 schedules a task
for exactly 10 time units, and then moves on to the next task. The more
sophisticated round-robin scheduler TtRoundRobiii of Figure 11 schedules a task
either for 10 time units or until the task terminates, whatever happens first. The
variable i indicates which task is currently running; the bit done[i] indicates if
task i has terminated.
The priority scheduler Priority of Figure 12 schedules a task until it termi-
nates or until an interrupt arrives from a task with higher priority, whatever
happens first. The scheduler Priority is a real-time process even though it does
not use a clock: the guarded wait statement ensures that Priority waits un-
til a high-priority task sets the bit interrupt. If we wish to guarantee that no
interrupt is lost, we must assume that no two high-priority tasks arrive simul-
taneously at precisely the same instant in real-numbered time; alternatively, we
could provide a separate bit interrnpt[i] for each task i.
The real-time process Gate Controller of Figure 13 controls the gate at a rail-
road crossing. The gate is closed 5 time units after a train signals its approach
by setting the bit arrival, and the gate is opened again as soon as the train
signals its exit from the crossing by setting the bit exit. The more sophisticated
controller MtGateControlier of Figure 14 accommodates multiple trains, per-
haps on parallel tracks, in the crossing. This controller uses the variable n to
count the number of trains that are currently in the crossing under the assump-
tion that no two trains arrive simultaneously. The gate is opened only when all
20
= (left = o A right = k0 A m = 0 A n = 0)
(left = o A left' = j A x' = O)n??at,m?n,? V
(left = i A left' = ?)n??t?m?n?x,? V
(left = 2 A x < 3 A left' = 1)r?ght?m?,??y V
(left = 2 A x > 3 A left' = ?)??ht?m?n?x?y V
(left = ? A left' = ? A m' = rn + 1)n9htn,?,y V
(left = ? A left' = ? A z' = O)r?ht?m?n?y V
(left = ? A left' = 6)n9ht?m,n?x?? V
(left = 6 A x < 1 A left' = 5)nght,m,n??y V
(left = 6 A x > 1 A left' = ?)n??tm,n;?? V
(left =  A left' = o A ??` = m + 2)r,??t,n,x',y V
(right = k0 A right' = k1 A y, = O)iqt?m?n,? V
(right = k1 A right' = k?)iqt,m,n,x,y V
(right = k2 A y < 7 A right' = ki)Thft??n?xy V
(right = k2 A y > 7 A right' = k3)?ft,m?n?x,j, V
(right = k3 A right' = k0 A n' = n + 1)iqt??,y
Xo = (left = i A right = k1 A x' < 3 A g' ? 7) v
(left = ? A right = k1 A x' < 1 A y' < 7)
Figure 9: Real-time system (?o ?? xo) defined by the program RtParUp
trains have left the crossing i. e., when the value of n is 0.
Bibliographic remarks. The synchronicity assumption that program in-
structions are instantaneous and time is introduced through the environment is
due to Berry, whose ESTEREL language inspired also the wait watching macro
(for an introduction to synchronous programming languages, see the monograph
by llalbwachs [Hal93j). The use of control-location labels to define the system
actions of a while program is standard practice of the interleaving school for
concurrency [Lam9i., MP92]. Schedulers and railroad gate controllers pervade
the real-time literature as examples.
5 Timed Systems 3: Continuous Environment
5.1 Drifting clocks
So far, we have assumed that all clocks are mathematically precise. In dis-
trihuted systems, however, one is often confronted with physical clocks, which
are necessarily imprecise. Typically all that is known about a process clock x is
that the drift of x is hounded; that is, in any time interval of length 1 the clock
21
program Rounditobin:
initially i := FirstTask;
loop
ResttmeTask(i);
wait 10;
SttspendTask(i);
NextTask(i)
end.
Figure 10: Round-robin scheduler
program TtRoundRobin:
declare x: clock;
initially i := FirstTask;
loop
ResumeTask(i);
x := 0; await x ? 10 v doneU];
if ?done[i] then SnspendTask(i) fi;
i := NextTask(i)
end.
Figure 11: Round-robin scheduler for terminating tasks
may deviate from the actual time by ?e, for a real number e > 0. We indicate
that the drift of a clock x is bounded by e with the clock declaration declare x:
clock drift e (the condition drift 0 is suppressed as usual). For example, Fig-
ure 15 shows the railroad gate controller of the previous section (Figure 13),
assuming that the drift of the controller clock x is bounded by e = 0.1. This
version of the controller may close the gate as early as 4.5 time units and as late
as 5.5 time units after the train signals its approach.
The behavior of drifting clocks during delays is best described by differential
constraints. For this purpose, let ?) be the first derivative of the variable v.
Then, if the drift of the clock z is bounded by 0.1, all states that are passed
by delays satisfy the differential constraint 0.9 < x < 1.1. The resulting system
is called ?hybrid," because it consists of both discrete system variables that
are updated by system actions and continuous environment variables namely,
drifting clocks?that are updated by the environment during delays.
22
program Priority.
initially interrupt := false;
loop
i MaxPriorityTask;
ResumeTask(i);
await interrupt v done[i];
if interrupt then interrupt false fi;
if ?done[i] then SuspendTask(i) fi
end.
Figure 12: Priority scheduler
program Gate Controller:
initially arrival :=false; exit :=faThe;
loop
await arrival; arrival := false;
wait 5;
Close Gate
await exit; exit :=false;
Open Gate
end.
Figure 13: Railroad gate controller
5.2 Hybrid systems
We now illustrate that clock variables can be generalized to model not only time
or drifting physical clocks, but arbitrary continuous environment parameters
such as temperature or position.
The behavior of a hybrid system results from system actions and hybrid
delays. A hybrid delay (f, 6) consists of a nonnegative real number 6 the dura-
tion of the delay and a differentiable function f from the closed interval [0, 6j
of the real line to states (a function f from the reals to states is differentiable
if for every variable v, the projection f(v) is differentiable). The state f(0) is
the source state of the hybrid delay (f, 6); the state f(6) is its target state. A
state 0' is passed by the hybrid delay (f, 6) if & = f(e) for some nonnegative
real e < 6. A hybrid behavior is a countably infinite sequence of system ac-
tions and hybrid delays such that any two neighboring sequence elements are
consecutive.
Hybrid delays are described by hybrid delay predicates. Let V be the set of
23
program MiGateController:
declare x: clock
initially arrival false; exit false;
loop
await arrival; arrival :=false n 1;
x := 0;
repeat
wait watching arrival V exit V x > 5.
if arrival then arrival := false; n n + 1 fi;
if exit then exit false; n := n --H 1 fi
until x > 5
Close Gate;
repeat
wait watching arrival V exit;
if arrival then arrival := false; n n + 1 fi;
if exit then exit false; n := n --H 1 fi
until n = 0;
Open Gate
end.
Figure 14: Railroad gate controller for multiple trains
dotted variables whose undotted versions occur in V. A hybrid delay predicate
is a formula of predicate logic whose free variables are taken from V and V.
The hybrid delay predicate ? is true for a hybrid delay if x is true for all states
that are passed by the delay. The hybrid delay predicate ?` is invariantly true
for a hybrid behavior a if x is true for all hybrid delays of a.
A hybrid system, then, is a real-time system whose environment condition
is a hybrid delay predicate. The hybrid behavior a is a behavior of the hybrid
system s if (1) the initial condition of S is initially true for a- and (2) the
transition condition and the environment condition of S are invariantly true
for a-. Suppose that S is a hybrid system with the environment condition X'o A
variable m is a (discrete) system variable of s if the environment condition Xo
implies iii = 0; that is, the variable in is not modified during delays. All other
variables in V are (continuous) environment variables. In particular, a variable x
is a clock if the environment condition ?o implies x = 1; the variable y is a clock
with bounded drift e > 0 if the environment condition Xo implies 1 --H y <
1 + e; the variable z is a stopwatch if the environment condition Xo implies (i =
0) v (i = 1).
Environment variables, however, are not limited to measuring time. Consider
the example of a thermostat that regulates the room temperature. Suppose that
24
program DcGate Controller:
declare x: clock drift 0.1;
initiafly arrival :=false' exit `--Hfalse;
loop
await arrival; arrival :=false;
x := 0; await x = 5;
Close Gate'
await exit; exit := false;
Open Gate
end.
Figure 15: Railroad gate controller with a drifting clock
the initial room temperature is (38 degrees and the heat is turned on. When the
temperature reaches 70 degrees, the heat is turned off, and the temperature 0
decreases over time t according to the exponential function 0(t) --H 70e?cot
where c0 is a constant determined by the room; when the temperature falls to
65 degrees, the heat is turned on, and the temperature 0 increases according to
the exponential function 0(1) = 65e?c?t + cj(1 --H e?cut), where c1 is a constant
determined by the power of the heater. The resulting hybrid system is defined
by the initial condition ?o, the transition condition ??, and the environment
condition xo:
(heat = on A 0 = 68)
(heat = off A 0 < 65 A heat' = on)e V
(heat = on A 0> 70 A heat' = off)o
(heat = on A 0',= co(ci --H 0) A 0<70) v
(heat = off A 0 = --Hc00 A 0 > 65)
Here, the status of the heater is modeled by the discrete (boolean-valued) system
variable heat; the room temperature, by the continuous (real-valued) environ-
ment variable 0.
5.3 Hybrid programs
We define hybrid systems by while programs such as the Train process of Fig-
ure 16. Clock variables (possibly drifting) are declared, as before, as clock; all
other environment variables, as continuous. In particular, the environment
variable d represents the distance, in meters, of the train from a railroad cross-
ing. The dotted variable d represents, then, the speed of the train in meters
per time unit. All undeclared variables, such as the bits arrival and exit, are
discrete by default.
25
program Train:
declare d: continuous;
loop
0: wait;
i: d := 5000;
repeat
2: wait[--H55 < <--H45] watching d < 1000
3:untild< 1000;
?: arrival := Irve;
repeat
?: wait[--H50 < <--H35] watching d < --H100
6:unhld< --H100;
7: exi? := true
end.
Figure 16: Hybrid program
Given a hybrid delay predicate ? and a vector v of variables, we write (xYv for
the hybrid delay predicate ? A v --H 0' that is, the variables listed as a subscript
remain unchanged. Given a hybrid program, let m be the vector of discrete
variables, let x be the vector of clocks, and let e be the corresponding vector of
drift bounds. The instruction wait[x] watching ? maintains the hybrid delay
predicate x while delaying the program for an arbitrary amount of time, but at
most until the timed state predicate ? becomes true; it stands for the guarded
wait statement
_			? A ??)m			wait.
In our example, the speed of the train stays between 45 and 55 meters per time
unit until the train is 1,000 meters from the crossing. At this point, the train
signals its approach, by setting the bit arrival, and slows down to 35 to 50
meters per time unit. After the train is 100 meters past the crossing, it leaves
and may return along a cyclic track at any time, provided the length of the
loop is at least 5,000 meters. The hybrid program Train defines, therefore, the
hybrid system of Figure 17.
At last, we may wish to combine, using the p&allel-composition operator
the Train process with the gate controller DcGateConlroller into a concurrent
hybrid program. The corresponding hybrid system is defined, as usual, as the
cartesian product of the component systems: the initial condition is obtained by
taking the conjunction of the initial conditions of the components; the transition
condition, by taking the disjunction of the transition conditions of the compo-
nents; and the hybrid delay schemata of the environment condition result from
26
= (pc=0)
ik? --H
xo --H
(pc = o A pc' = I)arnva1,e?t?d V
(pc = i A pc' = 2 A d' = SOOO)arnvai,e?t V
(pc = 2 A pc' = 3)arr??1,ez?t,d V
(pc = ? A d > 1000 A pC' = 2)arr?va?e?t,d V
(PC = ? A d < 1000 A pc' = 4)arnvaI?e?t?d V
(pC = 4 A pC' = ? A arrival' = trne)e?t,? V
(pC = ? A pC' = 6)a?r?va?e?t?d V
(pC = 6 A d> --H100 A pC' = s)arr?a?e?t?? V
(PC = 6 A d < --H100 A pC' = 7)arnvai?e?t?d V
(pc = ? A pC' = 0 A exit' = trae)arr?vai?d
(pC = o)arr?vai?e?t V
(pC = 2 A --H55 < d < --H45 A d < 1OOO)arrwui?e?t V
(pC = ? A --H50 < d < --H35 A d < --HlOO)arrwai?e?t
Figure 17: Hybrid system (?o ??, x'o) defined by the program Train
taking all pairwise ConjunCtions of the component delay schemata. We leave the
details to the ambitious reader.
Bibliographic remarks. The bounded-drift assumption underlies the clock
synchronization problem for distributed systems (see, for example, the survey
by Schneider [Sch87]). A recent workshop proceedings provides an excellent
current overview of computer-science models for hybrid systems [Ner93]. The
dichotomy of discrete system actions versus continuous environment activities
(hybrid delays) was introduced by Manna, Maler, and Pnueli [MMP92J. The
use of environment conditions (invariants) to model hybrid systems in gen-
eral [AC111193], and drifting clocks in particular [AH1193], was first worked out
in an automata-theoretic framework. The thermostat example is due to Nicollin
Sifakis, and Yovine [NSY92].
6 Analysis of Timed Systems
Now that we have defined the formal semantics of real-time systems, we wish
to develop both methods and tools for proving the correctness of real-time pro-
grams. The verification problem has been addressed by several papers in recent
years; here we attempt only to direct the reader to some of this literature.
27
6.1 Specification
First, we need a specification language for stating the correctuess requirements
of a given real-time program. Process algebras, temporal logics, arid automata
are popular specification languages for untimed systems. Hence a variety of
real-time extensions of these languages has been proposed and investigated, in-
cluding the process algebras TCSP [RR88], ATP [NRSv9o], and TCCS [Wan9O];
the temporal logics RTL [JM86], TPTL [AH89], TCTL [ACD9o], MTL [AH9O,
Koy9O], and RTTL [Ost9O]; as well as timed automata [AD9()] and timed 1/0 au-
tomata [MMT9l, LV92a] (see [NS9i] for a survey of real-time process algebras;
[A1192] for a survey of logic-based and automata-based real-time languages; and
[dBlldRR92] for a variety of applications).
Particularly compatible with our approach are the temporal logics TPTL
(linear time) and TCTL (branching time), as well as timed automata: TPTL
and TCTL are obtained by adding clock variables, reset quantifiers, and clock
constraints to temporal logic; timed automata are obtained by adding clocks,
reset conditions, and clock constraints to finite automata. If the acceptance
condition of a timed automaton is replaced by an environment condition the
resulting timed safety automaton [HNSY92] corresponds precisely to our notion
of real-time system.
To illustrate the use of clocks for specification, let us specify a few proper-
ties of the real-time while program RtUpDown3 (Figure 5) using the temporal
logic TPTL. First, consider the invariance formula
?1: 0 (n < 12).
A (timed) behavior ? satisfies the formula ?i iff the (timed) state predicate n <
12 is true for all states that occur in ?; a (real-time) program ? satisfies ?i iff
every behavior of ? satisfies ?i.
Second, we wish to specify the timing behavior of the program RtUpDown3.
Let x be a clock. The time-bounded response formula
x := O.?(x <75 An = 0)
asserts that the timed state predicate n = 0 becomes true, in all behaviors of a
real-time program, within at most 75 time units from the initial state. Dually,
the time-bounded invariance formula
x			0. 0 (x < 15			n ? 0)
asserts that the value of n does not become 0, in all behaviors of a real-time
program, before time 15. The reader may check that, indeed, the program
RtUpDown3 satisfies all three TPTL-formulas Yi ?2, and y?. ?Ve conclude
that the real-time program RtUpDown3 takes at least 15 time units and at
most 75 time units to terminate.
28
6.2 Verification
Second, we need to verify that a given real-time program satisfies its specifica-
tion. For this purpose, most methods for proving the correctness of untimed
programs have been extended to timed programs, including assertional meth-
ods [Hoo92, SBM92], proof systems for temporal logics [HMP9l, AL92], and
simulation methods [LA9o, Lv92bj. None of these approaches, however use
clocks, and we would like to see a proof system for real-time programs with
clocks.
On the other hand, clocks have been central to the finite-state approach to
verification. A (real-time) system is finite-state if all (system) variables range
over finite domains. The verification problem for untimed flnit&state systems is
decidable, and a variety of software tools have been developed and successfully
applied particularly to the verification of protocols and circuits. Real-time
systems are more complex: even in the case of real-time finite-state systems,
the clocks range over the infinite domain of the nonnegative real numbers. It
is possible, however, to construct a finite quotient of the infinite state space
that is adequate for solving the reachability problem for real-time finite-state
systems. This observation led to verification algorithms for finite-state real-time
systems [ACD9o, AD9O, AFH9l].
The efficiency and scope of the finite-state approach to the verification of
real-time systems has been improved along several directions. First, algorithms
for constructing the minimal adequate quotient of an infinite state space have
been developed [ACH+92, LY92J. Second, to cope with the high computational
complexity of analyzing clock constraints, an incremental approach has been
implemented [AIKY92]: initially all clock constraints are ignored; then the clock
constraints are added one by one, as needed to prove a given specification. For
example, the real-time program RtUpDown3 continues to satisfy the properties
?i and ?2 without the clock constraint x> 12.
A third technique for improving both the efficiency and the scope of veri-
fication algorithms is based on symbolic computation [HNSY92]. Suppose, for
instance, we wish to prove that a certain property is an invariant of a real-time
system. For this purpose. we need to compute the set of states that appear
along all behaviors of the system. The timed state predicate that characterizes
this set of reachable states is the least fixpoint of an equation on timed state
predicates. The fixpoint can be computed by symbolic execution of the system,
which is guaranteed to terminate if the system is finite-state. The efficiency of
the fixpoint computation depends on the representation of state predicates; in
the case of untimed systems, binary decision diagrams have turned out to pro-
vide a cost effective data structure for representing state predicates [McM93].
A hybrid system is piecewise tinear if all continuous variables are bounded
by piecewise-linear functions. In particular, clocks and stopwatches are piece-
wise linear; drifting clocks are bounded by piecewise-linear functions; all other
variables can be approximated by piecewise-linear envelopes. The symbolic ver-
29
ification method applies also to the class of piecewise-linear hybrid systems,
albeit it may not terminate [ACHH93]. Prototype implementations are under
way both at Cornell [AHH93] and in Grenoble [NOSY93j.
Acknowledgments. The authors thank Limor Fix, David Karr, Peter Kopke,
and Fred Schneider for helpful comments.
References
[ACD90]
[ACH+92]
[ACHH93j
[AD9o]
R. Alur, C. Courcoubetis, and D.L. Dill. Model checking for real-
time systems. In Proceedings of the FiflA Annual Symposium on
Logic in Computer Science, pages 414--H425. IEEE Computer So-
ciety Press, 1990.
R. Alur, C. Courcoubetis, N. Halbwachs, D.L. Dill, and H. Wong-
Toi. Minimization of timed transition systems. In S.A. Smolka,
editor, CONCUR 92: Theories of Concurrency, Lecture Notes in
Computer Science 630, pages 340--H354. Springer-Verlag, 1992.
H. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hy-
brid automata: an algorithmic 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.
It. Alur and D.L. Dill. Automata for modeling real-time systems.
In M.S. Paterson, editor, ICALP 90: Automata, Languages, and
Programming, Lecture Notes in Computer Science 443, pages 322--H
335. Springer-Verlag, 1990.
[ADS86] B. Alpern, A.J. Demers, and F.B. Schneider. Safety without stut-
tering. Information Processing Letters, 23(4):177--H180, 1986.
[AFH91]
[AFK88]
It. Alur, T. Feder, and T.A. Henzinger. The benefits of relaxing
punctuality. In Proceedings of the Tenth Annual Symposium on
Principles of Distributed Computing, pages 139--H152. ACM Press
1991.
K.R. Apt, N. Francez, and 5. Katz. Appraising fairness in
languages for distributed programming. Distributed Computing,
2(4):226--H241, 1988.
It. Alur and T.A. Henzinger. A really temporal logic. In Proceed-
ings of the 30th Annual Symposium on Foundations of Computer
Science, pages 164--H169. IEEE Computer Society Press, 1989.
[AH89]
30
[A1190]
[AH92]
[A111193]
[A!KY92]
[AL92]
[CM88]
R. Alur and T.A. Henzinger. Real-time logics: complexity and
expressiveness. In Proceedings of the Fiflh Annual Symposium
on Logic in Computer Science, pages 390--H401. IEEE Computer
Society Press, 1990.
R. Alur and T.A. llenzinger. Logics and models of real time: a
survey. 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 74--H106. Springer-Verlag,
1992.
R. Alur, T.A. llenzinger, and P.-B. Ho. Automatic symbolic ver-
ification of embedded systems. In Proceedings of the 1?th Annual
Real-time Systems Symposium, pages 2--H1 1. IEEE Computer So-
ciety Press, 1993.
R. Alur, A. Itai, R.P. Kurshan, and M. Yannakakis. Timing ver-
ification by successive approximation. In G. Bochmann, editor,
CAV 92: Computer-aided Verification, Lecture Notes in Com-
puter Science. Springer-Verlag, 1992.
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. Rozen-
berg, editors, Real Time: Theory in Practice, Lecture Notes in
Computer Science 600, pages 1--H27. Springer-Verlag, 1992.
K.M. Chandy and 1. Misra. Parallel Program Design: A Founda-
tion. Addison-Wesley Publishing Company, 1988.
[dBHdRR92] J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozen-
berg, editors. Real Time: Theory in Practice. Lecture Notes in
Computer Science 600. Springer-Verlag, 1992.
[Dii 75]
[Eme83]
[Hal93]
[Hen91]
E.W. Dijkstra. Guarded commands, nondeterminacy, and formal
derivation of programs. Communications of the ACM, 18(8):453--H
457,1975.
E.A. Emerson. Alternative semantics for temporal logics. Theo-
retical Computer Science, 26(1):121--H130, 1983.
N. Halbwachs. Synchronous Programming of Reactive Systems.
Kluwer Academic Publishers, 1993.
T.A. Henzinger. The Temporal Specification and Verification of
Real-time Systems. PhD thesis, Stanford University, 1991.
T.A. Heuzinger. Sooner is safer than later. Information Processing
Letters, 43(3):135--H141, 1992.
[Hen92]
31
[HMP91]
[HNSY92j
[Hoo92]
[JM86]
[Koy9O]
[LA9O]
[Lam83]
[Lam91]
[LV92a]
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.
T.A. Henzinger, X. Nicollin, J. Sifakis, and 5. Yovine. Symbolic
model checking for real-time systems. In Proceedings of the Sev-
enth Annual Symposium on Logic in Computer Science, pages
394--H406. IEEE Computer Society Press, 1992.
J. Hooman. Compositional verification of real-time systems us-
ing extended Hoare trples. 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 252--H290.
Springer-Verlag, 1992.
F. Jahanian and A.K. Mok. Safety analysis of timing properties in
real-time systems. lEEB Transactions on Sofiware Engineering,
SE-12(9):890--H904, 1986.
R. Koymans. Specifying real-time properties with metric temporal
logic. Real-time Systems, 2(4):255--H299, 1990.
N.A. Lynch and II. Attiya. Using mappings to prove timing prop-
erties. In Proceedings of the Ninth Annual Symposium on Princi-
ples of Distributed Computing, pages 265--H280. ACNI Press, 1990.
L. Lamport. What good is temporal logic? In R.E.A. Mason
editor, Information Processing 83: Proceedings of the Ninth IFIP
World Computer Congress, pages 657--H668. Elsevier Science Pub-
lishers (North-Holland), 1983.
L. Lamport. The temporal logic of actions. Technical Report 79,
DEC Systems Research Center, Palo Alto, California, 1991.
N. Lynch and F. Vaandrager. Action transducers and timed au-
tomata. In S.A. Smolka, editor, CONCUR 92: Theories of Con-
currency, Lecture Notes in Computer Science 630, pages 436--H455.
Springer-Verlag, 1992.
N. Lynch and F. Vaandrager. Forward and backward simulations
for timing-based systems. 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 397--H446.
Springer-Verlag, 1992.
[LV92b]
32
[LY92]
[McM93j
[MMP92]
[MMT91j
[MP92]
[Ner93]
[NOSY93J
[NRSV90]
[NS9l]
[NSY92]
[Ost90]
D. Lee and M. Yannakakis. Online minimization of transition
systems. In Proceedings of the 2?th Annnai Symposiitm on Theory
of Compitting, pages 264--H274. ACM Press, 1992.
K.L. McMillan. Symbolic Model Checking: An Approach to the
State Explosion Problem. Kiuwer Academic Publishers, 1993.
0. Maler, Z. Manna, and A. Pnueli. From timed to hybrid sys-
tems. 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 447--H484. Springer-Verlag,
1992.
M. Merritt, F. Modugno, and M.R. Tuttle. Time-constrained
automata. In J.C.M. Baeten and J.F. Groote, editors, CONCUR
91: Theories of Con currency, Lecture Notes in Computer Science
527, pages 408--H423. Spnnger-Verlag, 1991.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and
Concurrent Systems: Specification. Springer-Verlag, 1992.
A. Nerode, editor. Theory of Hybrid Systems. Lecture Notes in
Computer Science. Springer-Verlag, 1993.
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.
X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron. ATP: an al-
gebra for timed processes. In M. Broy and C.B. Jones, editors,
Proceedings of the IFIP WG2.2/2.3 Working Conference on Pro-
gramming Concepts and Methods, pages 415--H442. Elsevier Science
Publishers (North-Holland), 1990.
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.
X. Nicollin, J. Sifakis, and 5. Yovine. From ATP to timed graphs
and hybrid systems. In J.?V. de Bakker, K. Huizing, W.-P.
de Roever, and G. Rozenberg, editors, Real Time: Theory in
Practice, Lecture Notes in Computer Science 600, pages 549--H572.
Springer-Verlag, 1992.
J.S. Ostroff. Temporal Logic of Real-time Systems. Research Stud-
ies Press, 1990.
33
[RR88]
[SBM92]
[Sch87j
G.M. Reed and A.W. Roscoe.
nicating sequential processes.
58(1/2/3):249--H261, 1988.
A timed model for comnin-
Theoretical Cornpaler Science
F.B. Schneider, B. Bloom, and K. Marzuilo. Putting time into
proof outlines, In J.W. de Bakker, K. Huizing, `v.-P. de Roever,
and G. Rozenberg, editors, Real Time: Theory in Practice, Lec-
ture Notes in Computer Science 600, pages 618--H639. Springer-
Verlag, 1992.
F.B. Schneider. Understanding protocols for byzantine clock syn-
chronization. Technical Report 87-859, Cornell University, 1987.
Y. Wang. Real-time behavior of asynchronous agents. In J.C.M.
Baeten and J.W. Kiop, editors, CONCUR 90: Theories of Con-
currency, Lecture Notes in Computer Science 458, pages 502--H520.
Springer-Verlag, 1990.
34
[Wan90]
