BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR92-1263
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Timed Transition Systems
AUTHOR:: Henzinger, Thomas A.
AUTHOR:: Manna, Zohar 
AUTHOR:: Pnueli, Amir   
DATE:: January 1992
PAGES:: 25
ABSTRACT:: 
We incorporate time into an interleaving model of concurrency. In timed 
transition systems, the qualitative fairness requirements of traditional 
transition system are replaced (and superseded) by quantitative lower-bound 
and upper-bound timing constraints on transitions. The purpose of this paper 
is to explore the scope of applicability for the abstract model of timed 
transition systems. We demonstrate that the model can represent a wide 
variety of phenomena that routinely occur in conjunction with the timed 
execution of concurrent processes. Our treatment covers both processes that 
are executed in parallel on separate processors and communicate either 
through shared variables or by message passing, and processes that time-share 
a limited number of processors under a given scheduling policy. Often it is 
this scheduling policy that determines if a system meets its real-time 
requirements. Thus we explicitly address such questions as time-outs, 
interrupts, static and dynamic priorities.
END:: CORNELLCS//TR92-1263
BODY::
Timed Transition Systems*
Thomas A. Henzinger
Zohar Manna
Amir Pnueli
IR 92-1263
January1992
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
This research was supported in part by the National Science Foundation grants
CCR-89-1 1512 and CCR-89-1 3641, by the Defense Advanced Research Projects
Agency under contract N00039-84-C-021 1, by the United States Air Force Office of
Scientific Research under contract AFOSR-90-0057 and by the European Community
ESPRlT Basic Research Action Project 3096 (SPEC).
Timed Transition Systems1
Thomas A. Heuzinger
Computer Science Department
Cornell University
Ithaca, NY 14853
Zohar Manna
Computer Science Department
Stanford University
Stanford, CA 94305
and
Department of Applied Mathematics
Weizmann Institute of Science
Rehovot 76100, Israel
Arnir Pnueli
Department of Applied Mathematics
Weizmann Institute of Science
Rehovot 76100, Israel
Abstract. We incorporate time into an interleaving model of concurrency. In timed
transition systems, the qualitative fairness requirements of traditional transition system
are replaced (and superseded) by quantitative lower-bound and upper-bound timing
constraints on transitions. The purpose of this paper is to explore the scope of appli-
cability for the abstract model of timed transition systems. We demonstrate that the
model can represent a wide variety of phenomena that routinely occur in conjunction
with the timed execution of concurrent processes. Our treatment covers both processes
that are executed in parallel on separate processors and communicate either through
shared variables or by message passing, and processes that time-share a limited number
of processors under a given scheduling policy. Often it is this scheduling policy that
determines if a system meets its real-time requirements. Thus we explicitly address
such questions as time-outs, interrupts, static and dynamic priorities.
This research was supported in part by the National Science Foundation grants CCR-89-11512 and CCR-89-
13641, by the Defense Advanced Research Projects Agency under contract N00039-84-C-o211, by the United States
Air Force Office of Scientific Research under contract AFOSR-90-0057, and by the European Community ESPRIT
Basic Research Action project 3096 (SPEC).
1 Introduction
In [HMP9l], we extended the specification language of temporal logic and the corresponding ver-
ification framework to prove timing properties of reactive systems. To model the timed execution
of reactive systems, we generalized the computational model of transition systems conservatively
by imposing timing requirements on the transitions. We claimed that a wide variety of real-time
phenomena that are encountered in practice can be represented and analyzed within the model
of timed transition systems. In this paper, we substantiate that claim. We use timed transition
systems to model the timed execution of both multiprocessing and multiprogramming systems.
Specifically, we address issues that routinely occur in real-time process communication, such as
time-outs, and issues of real-time process control, including typical time-sharing strategies. By
doing so, we enlargen the scope of applicability of the temporal proof methodologies for verifying
timing properties of reactive systems that were presented in [HMP9l].
In our model, we assume a global, fictitious, real-valued clock, whose actions advance time by
nonuniform amounts. The clock actions are interleaved with the system actions, which have no
duration in time. In some other work aimed at the formal analysis of real-time systems, it has been
claimed that while this interleaving model of computation may be adequate for the qualitative
analysis of reactive systems, it is inappropriate for the real-time analysis of programs, and a more
realistic model, such as maximal parallelism, is needed [KSdR+88]. One of the points that we
demonstrate in this paper is a refutation of that claim. We show that by a careful incorporation of
time into the interleaving model, we can still model adequately most of the phenomena that occur
in the timed execution of programs. Yet we retain the important economic advantage of interleaving
models, namely, that at any point only one transition can occur and has to be analyzed.
We define the formal semantics of a real-time system as a set of timed execution sequences. This
is done in two steps. First, in Section 2, we review the abstract computational model of timed
transition systems and identify the possible timed execution sequences (computations) of any such
system. Then, we consider concrete real-time systems and show how the concrete constructs can
be interpreted within the abstract model. We begin, in Section 3, with the representation of real-
time processes that are executed in parallel and communicate either through a shared memory
or by message passing. Although the timeless interleaving of concurrent activities identifies true
parallelism with (sequential) nondeterminism, when time is of the essence, we can no longer ignore
the difference between multiprocessing, where each parallel task is executed on a separate machine,
and multiprogrammin9, where several tasks reside on the same machine. This is because questions of
priorities, interrupts, and scheduling of tasks may strongly influence the ability of a system to meet
its timing constraints. These issues in modeling time-sharing systems are discussed in Section 4.
2 Timing Constraints for Transition Systems
Timed transition systems generalize the basic computational model of transition systems [Kel76,
Pnu77] by associating minimal and maximal time delays with the transitions. We use the real line
as time domain and adapt the definition of timed transition systems that was given for a discrete
time domain in [HMP91]. Similar notions of transition systems with timing constraints have been
defined, for integer time, in [Har88, PH88, llMP9O, Ost90].
A transition system S = (V, ?, 0,7) consists of four components:
1. a finite set V of variables.
2
2. a set ? of states. Every state a E ? is an interpretation of V; that is, it assigns to every
variable x E V a value a(x) in its domain.
3. a subset 0- c ? of initial states.
4. a finite set T of transitions, including the idle transition ri. Every transition r E T is a binary
relation on ?; that is, it defines for every state a E ? a (possibly empty) set of r-successors
--H(a) C ?. We say that the transition r is enabled on a state a iff r(a) # ?. In particular,
the idle (stutter) transition
ri = ?(Qa)ia??J
is enabled on every state.
All infinite sequence a = ....... of states is a computation (execution sequence, run) of the
transition system 5 = (V, ?, 0-, T) iff it satisfies the following two requirements:
Initiality a0 E 0.
Consecution For all i> 0, there is a transition r E T such that Q+i E r(a?) (which is also denoted
by a? Th Q+i). We say that the transition r is taken at position i of the computation a.
We incorporate time into the transition system model by assuming that all transitions happen
"instantaneously," while real-time constraints restrict the times at which transitions may occur. The
timing constraints are classified into two categories: lower-bound and upper-bound requirements.
They ensure that transitions occur neither too early nor too late, respectively. All of our time
bounds are nonnegative integers N. The absence of a lower-bound requirement is modeled by a
lower bound of 0; the absence of an upper-bound requirement, by an upper bound of 00. For
notational convenience, we assume that oo _ n for all n E N.
A timed transition system 5 = (V, ?, 0, T, 1, u? consists of an underlying transition system 5 --H
(V, ?, 0,7) as well as
5. a minimal delay lT c N for every transition r E T. We require that lri = 0.
6. a maximal delay ?T E N u ?oo) for every transition - E T. We require that Ur > lr for all
r E T, and that Ur = oo if r is enabled on any initial state in 0. In particular, Uri = 00.
Let T0 C T be the set of transitions with the maximal delay 0. To allow time to progress, we
put a restriction on these transitions. We require that there is no sequence
To			Ti			Tn?1
a0			a1			... ___
of states and transitions such that n > JT0J and rj E T0 for all 0 < i < n. This condition
ensures the operationality (machine-closure) of timed transition systems [Hen9la].
Timed state sequences
We model time by the real numbers R. A timed state sequence p = (a,T) consists of an infinite
sequence a of states a? E ?, where i> 0 and an infinite sequence T of corresponding times Ti E R
that satisfy the following two conditions:
3
Monotonicity For all i> 0
either Tj+1 = Ti,
or Tj+1 > Tj and a?+I =
that is, time never decreases. It may increase, by any amount, only between two consecutive
states that are identical. The case that the time stays the same between two identical states
is referred to as a stutter step; the case that the time increases is called a time step.
Progress For all t E R, there is some i > 0 such that Tj > t; that is, time never converges. Since
the time domain R contains no maximal element, there are infinitely many time steps in every
timed state sequence.
It follows that a timed state sequence alternates state activities with time activities. Throughout
state activities, time does not advance; throughout time activities, the state does not change.
Since all state activities are represented by finite subsequences, timed state sequences observe the
condition of finite variability, namely, that the state changes only finitely often throughout any
finite interval of time [BKP86].
A set II of timed state sequences is closed under stuttering iff (1) the sequence
is in II precisely when the sequence
is in II, and (2) the sequence
--H+ (a?,T?) (oj,Tj)
...			(Q",%')			(ai,Ti+1)
is in II precisely when the sequence
...			(ai,Ti)			(ai,t)			(a?,T?+1) --H+ .
is in II for Ti < t < Ti+i. To close a set of timed state sequences under stuttering, then, we must
(1) add and delete finitely many stutter steps, and (2) spllt and merge finitely many time steps.
Timed execution sequences
Just as the execution sequences of transition systems are infinite state sequences, we model the
execution sequences of timed transition systems by timed state sequences. The timed state sequence
p = (a, T) is a computation of the timed transition system S = (V, ?, 0, T, 1, u) iff the state sequence
a is a computation of the underlying transition system S- and
Lower bound For every transition T E ? and all positions i> 0 and j > i with Tj < Ti + Ir,
if r is taken at position j of a,
then r is enabled on Q.
In other words, once enabled, r is delayed for at least 17 time units; it can be taken only
after being continuously enabled for l? time units. Any transition that is enabled initially, on
the first state of a timed state sequence, can be taken immediately (as if it has been enabled
forever).
4
Upper bound For every transition 7 E T and position i > 0 there is some position j > i with
Tj < Ti + ?r such that
either 7 is not enabled on
or 7 is taken at position j of a.
In other words, once enabled, ? is delayed for at most Ur time units; it cannot be continuously
enabled for more than Ur time units without being taken. Since the maximal delay of every
transition that is enabled initially must be 00, the first state change of a computation may
occur at any time.
Note that at both stutter steps and time steps, the idle transition ?I is taken. The idle transition
marks phases of time activity throughout a computation; the other transitions are interleaved
during phases of state activity. We consider all computations of a timed transition system to
be infinite. Finite (terminating as well as deadlocking) computations are represented by infinite
extensions that add only idle transitions; that is, a final, infinite phase of time activity.
It is not difficult to check that the computations of any timed transition system 5 are closed
(1) under stuttering and (2) under shifting the origin of time. The former property ensures that
timed transition systems can be refined [Hen9ib]; the latter property means that timed transition
systems cannot refer to absolute time. Specifically, the addition of a real constant to all times of a
timed state sequence does not alter the property of being a computation of 5. Thus we will often
assume, without loss of generality, that the time of the first state change of a computation is 0.
Since the state component of any computation of 5 is a computation of the underlying untimed
transition system 5--H, ordinary timeless reasoning is sound for timed transition systems: every
untimed property of infinite state sequences that is satisfied by all computations of 5-, is also
satisfied by all computations of 5. The converse, however, is generally not true. The timing
constraints of 5 can be viewed as filters that prohibit certain possible behaviors of the untimed
transition system 5--H. Special cases are a minimal delay 0 and a maximal delay oo for a transition 7.
While the former does not rule out any computations of 5-, the latter adds to 5 a weak-fairness
(justice) assumption in the sense of [MP89]: 7 cannot be continuously enabled without being taken.
The choice of the real numbers as time domain is taken for the sake of concreteness. Indeed, any
total ordering with an appropriate definition of addition by a unit (i.e., t < t + 1, and t < i' implies
t + 1 < t' + 1) can be chosen as a time domain. In the case that the time domain is any one-element
set, timed transition systems are easily seen to coincide with ordinary fair transition systems (with
a weak-fairness requirement for every transition).
3 Modeling Time-critical Multiprocessing Systems
The concrete real-time systems we consider first consist of a fixed number of sequential real-time
programs that are executed in parallel, on separate processors, and communicate through a shared
memory. We show how time-outs and real-time response can be programmed in this language.
Then we add message passing primitives for process synchronization and communication.
3.1 Syntax: Timed transition diagrams
A shared-variables multiprocessing system P has the form
fol[P1l1 . . 11Pm].
5
Each process Pi, for 1 < i < m is a sequential nondeterministic real-time program over the finite
set Uj of private (local) data variables and the finite set U5 of shared data variables. The formula 0,
called the data precondition of P, restricts the initial values of the variables in
U = U5u ? Uj.
1<i<m
The real-time programs Pi can be alternatively presented in a textual programming language or as
transition diagrams. We shall use the latter, graphical, representation. For this purpose, we extend
the untimed transition diagram language by labeling transitions with minimal and maximal time
delays.
A timed transition diagram for the process Pi is a finite directed graph whose vertices Lt --H
(4,... tn'j J are called locations. The entry location usually 4 --H is indicated as follows:
-M
The intended meaning of the entry location 4 is that the control of the process Pi starts at the
location 4. The component processes of a system are not required to start synchronously (i.e., at
the same time). Each edge in the graph is labeled by a guarded instruction, a minimal delay 1 E; N
and a maximal delay u E N u (ooJ such that n> 1:
where the guard c is a boolean expression, x is a vector of variables, and e an equally typed vector
of expressions (the guard true and the delay interval [0, co] are usually suppressed; for the empty
vector nil, the instruction c nil := nil is abbreviated to c?). We require that every cycle in the
graph consists of no fewer than two edges, at least one of which is labeled by a positive (nonzero)
maximal delay.
The intended operational meaning of the given edge is as follows. The minimal delay 1 guarantees
that whenever the control of the process Pi has resided at the location for at least 1 time units
during which the guard c has been continuously true, then Pi may proceed to the location ?k?.
The maximal delay u ensures that whenever the control of the process Pi has resided at ?for tt
time units during which the guard c has been continuously true, then Pi must proceed to ?kt (or,
more precisely, time cannot advance before either the guard c becomes false, which may be caused
by process parallel to Pi, or the process Pi proceeds). In doing so, the control of Pi moves to the
location ik? "instantaneously," and the current values of e are assigned to the variables x. In general,
a process may have to proceed via several edges all of whose guards have been continuously true
for their corresponding maximal delays. In this case, any such edge is chosen nondeterministically.
It follows that the control of a process Pj may remain at a location g forever only in one of two
situations: if has no outgoing edges, we say that Pi has terminated; if each of the guards that
are associated with the outgoing edges of the location is false infinitely often, we say that Pi has
deadlocked. The second condition is necessary (although not sufficient) for stagnation, because if
one guard is true forever, then the corresponding maximal delay u < oc guarantees the progress of
Pi.
6
3.2 Semantics: Timed transition systems
The operational view of timed transition diagrams can be captured by a simple translation into
the abstract model of timed transition systems. With the given shared-variables multiprocessing
system
P: ?o1[P1II... 11Pm],
we associate the following timed transition system Sp = (V, ?, 0, T, 1, u?:
1. V = Uu??,.. 7rmJ Each control variable ?i, where 1< i < m, ranges over the set LjUfIJ.
The value of 7r? indicates the location of the control for the process P?; it is 1 (undefined)
before the process Pi starts.
2. ? contains all interpretations of V.
3. 0 is the set of all states a E ? such that 0 is true in a and a(?) = 1 for all 1 < i < m.
4. T contains, in addition to the idle transition ri, an entry transition r0i for every process Pi,
where 1 < i < m as well as a transition TE for every edge E in the timed transition diagrams
for Pi,... Pm. In particular, a' E r?(a) iff
= 1 and a'(r?) = 0i,
= a(y) for all y E V --H firij.
If  connects the source location to the target location k? and is labeled by the instruction
c := e? then a' E r?(a) iff
= and a'(?) =
c is true in a and a'(x) =
= a(y) for all yE V --H
5. If r is an entry transition, then lT = 0. For every edge E labeled by the minimal delay 1, let
lr? = 1.
6. If r is an entry transition, then Ur = 00. For every edge E labeled by the maximal delay tt,
let Ur? =
This translation defines the set of possible computations of the real-time system P as a set of timed
state sequences. For instance, the computations of the trivial system P that consists of a single
process with the timed transition diagram
are exactly the timed state sequences that result from closing all sequences of the form
(1,0)			(o,O)			(C0,t)			(?1,t)			(C1,1)			(C1,2)
where 0 < t < 1, under stuttering and shifting the origin of time. The condition on timed transition
diagrams that every cycle contains at least one positive (nouzero) maximal delay ensures that
the timed transition system Sp is operational. (The condition that every cycle contains at least
7
two edges guarantees that once a transition is taken, it cannot stay enabled, which simplifies the
reasoning about timed transition systems [HMP9t].)
We remark that our semantics of shared-variables multiprocessing systems is conservative over the
untimed case. Suppose that the system P contains no delay labels (recall that, in this case, all
minimal delays are 0 and all maximal delays are co). Then the state components of the computa-
tions of Sp are precisely the legal execution sequences of P, as defined in the interleaving model
of concurrency, that are weakly fair with respect to every transition [MP89]: no process can stop
when one of its transitions is continuously enabled. Weak fairness for every individual transition
and, consequently, progress for every process is guaranteed by the maximal delays 00.
3.3 Examples: Time-out and timely response
We now model two typical real-time constructs as shared-variables multiprocessing systems to
demonstrate the scope of the timed transition diagram language. In the first example (time-out), a
process checks if an external event happens within a certain amount of time. In the second example
(traffic light), a process reacts to an external event and is required to do so within a certain amount
of time. A third example combines several processes.
Time-out
To see how a time-out situation can be programmed, consider the process P with the following
timed transition diagram:
true?
We assume that the variable x ma?y be altered by some other process that is executed in parallel
to P. When at the location C0, the process P attempts, for 10 time units, to proceed to the
location Ci by checking the value of x. If the value of x is not found to be 0, then P does not
succeed and proceeds to the alternative location C2 after 10 time units. The choice of the maximal
delay u determines how often P checks the value of x. For example, if u > 10 then P may not
check the value of x at all before timing out after 10 time units. If 0 < u < 10, then P has to check
the value of x at least once every u time units. Consequently, if the value of x is 0 for more than
u time units, it will be detected. On the other hand, the value of x being 0 may go undetected if
it fluctuates too frequently, even in the case of u = 0.
Traffic light
To give another typical real-time application of embedded systems, let us design a traffic light
controller that turns a pedestrian light green within 5 time units after a button is pushed. The
environment is given by the following process E. Whenever the request button is pushed, the
shared boolean variable request is set to true:
8
[0, 0] request			true
#Meo
Recall that the edge labels true? and [0, oo] are suppressed; thus we have no knowledge about the
frequency of requests.
We wish to design a traffic light controller Q that controls the status of the traffic light through
the variable light, whose value is either green or red. As unit of time we take the amount of time
it takes to switch the light; for simplicity, we also assume that the time needed for local operations
within Q is negligible. Now let us specify the desired process Q. The controller Q should behave
in such a way that the combined system
[request false, light			redj [IIQ]
satisfies the following two correctness conditions:
(A) Whenever request is true, then light is green within 5 time units for at least 5 time units.
(B) Whenever request has been false for 25 time units, then light is red.
The first condition, (A), ensures that no pedestrian has to wait for more than 5 time units to
cross the road and is given another 5 time units to do so. The second condition, (B), prevents the
light from being green indefinitely (under the assumption that any controller Q resets the variable
request to false whenever it is read and found to be true).
It is not hard to convince ourselves that, once it is started, the following process Q satisfies the
specification:
?request
_			[6,6] [0,0] request
request :--H false [0, 0]			request := false
light := green
for any delay 4 < 6 < 23. This implementation of the traffic light controller turns the light green
as soon as possible after a request is received and then waits for 6 time units before turning the
light red again. If the request button has been pushed in the meantime, the light stays green for
another 6 time units.
Multiple traffic lights
We now generalize the traffic light example and design a system that reacts to several external
events. We wish to do so by composing, in paraliel, processes that are similar to Q. At this point it
is convenient to accept some additional assumptions about the frequencies of the external events.
In our example, we suppose that the distance between any two requests is at least 15 time units;
that is,
9
[1,1]
light			green
request			true
Under this assumption, we can simplify the traffic light controller to
request			false [0, 0]
for ally delay 4 < ? < 17. The combined system
:			?request			false, light = redj [E'(tQ']
still satisfies both correctness requirements (A) and (B).
Now consider a more complex traffic light configuration, with two lights and two request buttons.
In particular, we assume that the second light is designed for the spedal convenience of pedestrians
in a hurry: it is required to turn green within 3 time units of a request but, on the other hand,
has to stay green for only 3 time units. While pedestrians arrive at the first light with a frequency
of at most one pedestrian every 15 time units, we assume that the more urgent requests are less
frequent at most one every 30 time units:
i: #&??[0?0] request1 := true E?: $Mi?[o?o] request2 := true
The controller for both lights executes the following two processes:
l0
Qi:
request1
request1 :=false [0,0]
tight1 := red
[1,1]
Th
p1
[1,1]
light1 := green
light2 := red
[1,1]
request2 :=false [0,0]
t2
[1,1]
MW'			light2 := green
If the combined traffic light controller makes use of two processors and the processes Qi and Q2
are executed in a truly concurrent fashion, then the correctness of the entire system
:			frequest1			request2			false, light1			light2 = red] [111E211Q111Q2]
follows from the correctness of its parts. Specifically, if 4 s < 17 and 2 < 62 < 23, then all runs
of P satisfy the following conditions:
(A1) Whenever request1 is true, then light1 is green within 5 time units for 5 time units.
(A2) Whenever request2 is true, then light2 is green within 3 time units for 3 time units.
(B1) Whenever request1 has been false for 25 time units, then light1 is red.
(B2) Whenever request2 has been false for 25 time units, then light2 is red.
A more interesting case is obtained if only a single processor is available to control both lights and
the two processes Qi and Q2 have to share it. Using the interleaving (shuffle) operator of [Hoa85],
we denote the resulting system by the expression
P111: frequest1 = request2 =false, light1 = light2 = red] [iII211(QiiIIQ2)].
Note that the behavior of the environment E111E2 is still truly concurrent to the behavior of the
traffic light controller Q1111Q2, which executes both processes Qi and Q2 on a single processor in
an interleaved fashion.
Let us assume that 6i = 10 and 62 = 2, a case in which the multiprocessing P\i is correct. However,
if we have no knowledge about the strategy by which the processes Qi and Q2 are scheduled 011 the
processor they share, other than that it is fair (i.e., the turn of each process will come eventually),
then the time-sharing system P?j does not satisfy the specification consisting of the requirements
(A1), (A2), (B1), and (B2). This is easy to see. Suppose that the process Qi is, for some time,
given priority over the process Q2, and the traffic light controller receives a request for the second
light only 1 time unit after it has received a request for the first light. Then it will serve the first
request by turning light1 green and (busy) waiting for 10 time units, thus violating (A2). On the
11
other hand, if the process Q2 that serves the more urgent yet less frequent requests is always given
priority over the process Qi, then the system Pjj is correct. This is because of the low frequency
of requests for the second light only one such request can interrupt the service of a request for the
first light.
Before we discuss the modeling of time-sharing, priorities, and interrupts in greater detail, let us
first stay with truly concurrent processes and introduce message-passing operations.
3.4 Message passing
Asynchronous message passing can be modeled by shared variables that represent message channels.
In this subsection, we extend our timed transition diagram language by a primitive for synchronous
(CSP-style) message passing, which can be used for the synchronization and communication of
parallel processes.
Syntax
A (message-passing) multiprocessing system P has the form
f?J[P1ll . . 11Pm],
where 0 is a data precondition and each process Pi, for 1 < i < m, is a sequential nondeterministic
real-time program over the finite set Uj U U8 of data variables (in the case of pure message-passing
systems, U5 = ?). We employ again timed transition diagrams to represent processes, but enrich the
repertoire of instructions by guarded send and receive operations. The send operation a!e outputs
the value of the expression e on the channel a. The receive operation a?x reads an input value
from the channel a and assigns it to the variable x. A send instruction and a receive instruction
match iff they belong to different processes and address the same channel:
For any two matching communication instructions with the delay intervals [1, u] and [1', tt,], respec-
tively, we require that max(l, i') < min(u, tt').
Since we use the paradigm of synchronous message passing, a send operation can be executed only
jointly with a matching receive operation. Thus the intended operational meaning of the given two
edges is as follows. Suppose that, for max(l, 1') time units, the control of the process Pj has resided
at the location C? and the control of the process Pj' has resided at the location and the guards c
and c' have been continuously true. Then Pj and Pjt may proceed, synchronously, to the locations
2k and ?,, respectively. On the other hand, if Pi has resided at e,i. and pi' has resided at e3ii, and
the guards c and c' have been continuously true for min(u, u') time units, then both processes must
proceed. In doing so, the current value of e is assigned to x.
12
Semantics
Synchronous message passing can be modeled formally by timed transition systems. We define
the timed transition system Sp = (V, ?, e, T, 1, u? that is associated with the given message-
passing multiprocessing system P as in the shared-variables case, only that T contains an additional
transition for every matching pair of communication instructions. Suppose that the two edges E
(from 4 to Ctk) and E' (from 41, to Ck?',) in the timed transition diagrams for Pi and Pji are labeled
by the matching instructions c e!o and c' a?x, respectively. Then
o+ T contains, for the matching edges E and E', a transition rE?EI such that a' E r?,?t(a) iff
= 4. and a'(r?) =
= 41, and a'(r?i) =
c and c' are true in a and a'(x) =
= a(y) for all YE V --H fri,rjt,xJ.
o+ If the matching edges  and ` are labeled by the minimal delays 1 and 1', respectively, let
1?E,E' = max(1,1').
o+ If the matching edges  and E' are labeled by the maximal delays u and n', respectively, let
UTEEI = min(tt,u').
This translation defines the set of possible computations of any distributed real-time system P
whose processes communicate either through shared variables or by message passing.
Process synchronization
Recall that the component processes of the multiprocessing system P1j?P2 may start at arbitrary,
even vastly different, times. An important appllcation of synchronous message passing is the syn-
chronization of parallel processes. Let P1 and P2 be two real-time processes whose timed transition
diagrams have the entry locations ? and o2, respectively, and let a be a channel. Now consider
the two processes P1 and P2 whose timed transition diagrams are obtained from the transition
diagrams for P1 and P2 by adding new entry locations:
P1:			[0,0]			0
P2:			[0,0]			0
The added message-passing operations have the effect of synchronizing the start of the two processes
P1 and P2 (whenever message passing is used for the purpose of process synchronization only, the
data that is passed between processes is immaterial and the data components of the send and receive
instructions are usually suppressed). It follows that the component processes of the multiprocessing
system P1iP2 start synchronously, at the exact same (arbitrary) time.
From now on, we shall write P1??,P2 for the system P whose component processes P1 and P2 start
synchronously; that is, the notation P1 iisP2 is an abbreviation for the message-passing system
P1 liP2. Equivalently, we can directly define the formal semantics Sp of the synchronous multipro-
cessing system P1J?8P2 as containing a single entry transition rJ'2 for both processes Pi and P2;
namely, a' E r?'2(a) iff
13
= a(?2) = I,
= ? and a'(r2) --H
= a(y) for all yE V --H ?r1,r2J.
It is not hard to generalize our notion of synchronous message passing to synchronous broadcasting,
which allows arbitrarily many parallel processes to synchronize simultaneously on joint transitions.
4 Modeling Time-critical Multiprogramming Systems
While the interleaving model for concurrency identifies true parallelism (multiprocessing) with
nondeterminism (multiprogramming), the traffic light example of the previous section suggests
that the ability of a system to meet its real-time constraints depends crucially on the number of
processors that are available and on the process allocation algorithm. This dependence is already
vividly demonstrated by the following trivial system consisting of the two processes pi and P2:
If both processes are executed in parallel on two processors, we denote the resulting system by
pi lip2 (or Pi JI8P2, if the processes are started at the same time); if they share a single processor
and are executed one transition at a time according to some scheduling strategy, the composite
system is denoted by Pill P2.
In the untimed case, it is the very essence of the interleaving semantics to identify both systems
with the same set of possible (interleaved) execution sequences the stuttering closure of the two
state sequences
(?0i,e02) ? (4,o2) ? (4,?)
(?oi,?o2) ff42 (?oi,?) ff4 (4,4) ,` ...
(a state is an interpretation of the two control variables irj and 7r2). Real time, however, can
distinguish between true concurrency and sequential nondeterminism: if both processes start syn-
chronously, then the parallel execution of p1 and P2 terminates within 1 time unit; on the other
hand, any interleaved sequential execution of P1 and p2 takes 2 time units. This distinction must
be captured by our model:
1. In the two-processor case p1 ??8p2, we obtain as computations the timed state sequences that
result from closing the two sequences
(1,1,0)			(0i,02,0)			(?0i,02,1) ff4 (4,e02,i) ff4 (4,i2,1)			(4,4,2)
(1,1,0)			(?0i,?02,0)			(0i,02,1) ff4 (?0i,4,1) ff4 (4,i2,l)			(4,4,2)
under stuttering and shifting the origin of time (the third component of every triple denotes
the time). The system p1 ??p2 has more computations, because the time difference between
the start of P1 and the start of p2 can be arbitrarily large.
14
2. In the time-sharing case P1 lIP2, the set of computations will be defined to be essentially the
closure of the two timed state sequences
(1,0)			(01,e02,o)			(o1,?o2,1) ? (1i,?o2,1)			(4,#o2,2) ? (4,?2i,2)
(1,0)			(C01,t02,o)			(?o1,?o2,1) ??2 (e01,?,1)			(?o1,?2i,2) ? (4,2i,2)
under stuttering and shifting the origin of time. We write "essentially," because we will
augment the states by information about the status of the two processes (either active or
suspended). Also, observe that we have silently assumed that the swapping of processes is
instantaneous and that neither process has priority over the other process. All of these issues
will be discussed in detail.
Thus, for modeling time-critical applications, we can no longer ignore the difference between mul-
tiprocessing and multiprogramming. In this section, we first show how our model extends to
concrete real-time systems that consist of a fixed number of sequential programs that are executed,
by time-sharing, on a single processor. Then we use our framework to represent general, distributed
multiprogramming systems, in which several processes share a pool of processors statically or dy-
namically.
4.1 Syntax and semantics
A multiprogramming system P has the form
toJ[P1111 . . 111Pm].
Each process Pj, for 1 < i < m is again a sequential nondeterministic real-time program over the
finite set U of data variables, whose initial values satisfy the data precondition 0. We represent
the real-time programs Pi by timed transition diagrams as before. Note, however, that in the
multiprogramming case the control of the (single) processor resides at one particular location of
one particular process. Thus the intended operational meaning of the edge
4.			ffi
is as follows. The minimal delay 1 guarantees that whenever the control (of the single processor)
has resided at the location j? for at least 1 time units and the guard c is true, then the control may
proceed to the location ?kt. The maximal delay u ensures that whenever the control has resided
at for n time units and the guard c is true, then it must proceed to tk. This is because, in the
single-processor case, no other process can interfere with the active process and change the value
of c.
The operational view of the concrete model is again captured formally by a translation into timed
transition systems. With the given multiprogramming system P, we associate the following timed
transition system Sp = (V, ?, 0, T, 1, u):
1. V = Uu??,?1,... 7rm). There are two kinds of control variables: the processor control variable
? ranges over the set .1.... m, IJ; each process control variable 7rj, for 1 < i < m ranges
over the set Li of locations of the process Pi. The value of the processor control variable ? is
I (undefined) before the (single) processor starts executing processes. Thereafter the control
15
of the processor resides at the location r? of the process P?. We say that the process P? is
active, while all other processes Pj, for i $ `t, are suspended (if the value of ? is undefined,
then all processes are suspended). The process control variable 7rj of a suspended process
indicates the location at which the execution of Pj will resume when Pj (re)gains control of
the processor.
2. ? contains all interpretations of V.
3. e is the set of all states a E ? such that 0 is true in a, and a(?) = I, and a(r?) = e0? for all
1 <i < m.
4.
T contains, in addition to the idle transition ri, an action transition TE for every edge E
in the timed transition diagrams for P1,... Pm. If E connects the source location t3? to the
target location k? and is labeled by the instruction c e, then a' E r?(a) iff
= and a'(?) = tk,
c is true in a and a'(x) =
= a(y) for all YE V
Furthermore, there are scheduling transitions T E T that change the status of the processes
by resuming a suspended process: a' E ?(a) implies that
= a(y) for all Y E U.
The schedullng policy determines the set of scheduling transitions. A scheduling transition
r is called an entrY transition iff it is enabled on some initial states. We restrict ourselves
to schedullng pollcies with a single entry transition, r0, that is enabled on all initial states.
Moreover, we require that a' E m(a) implies that
= I,
= a(y) for all Y E V --H
that is, the entry transition ?0 is enabled precisely on the initial states and activates, perhaps
nondeterministically, one of the competing processes.
5. For every edge E labeled by the minimal delay 1, let iTE = 1. Furthermore, iro = 0.
6. For every edge  labeled by the maximal delay u, let UTE = U. Furthermore, UT0 = 00.
The computations of Sp clearly depend on the scheduling transitions and their delays. In the
untimed case, the scheduling issue can be reduced to fairness assumptions about the scheduling
policy: correctness of an untimed multiprogramming system is generally shown for all fair scheduling
strategies. It makes, however, little sense to to desire that a multiprogramming system satisfies
a real-time requirement under all (fair) scheduling strategies, because the scheduling algorithm
usually determines if a system meets its timing constraints. In fact, fair scheduling strategies admit
thrashing: by switching control too often between processes, no action transition may be enabled
long enough so that it has to be taken and only scheduling transitions will be performed. Thus
the system may make no real progress at all and may certainly not meet any real-time deadlines.
Consequently, we study the correctuess of real-time multiprogramming systems always with respect
to a particular given scheduling policy.
16
4.2 Scheduling strategies
Our selection of scheduling strategies is neither intended to be categorical nor comprehensive; we
simply try to examine what we think is a representative variety of different scheduling mechanisms
and, in the process, hope to convince ourselves of the utility of the timed transition system model.
Throughout this subsection, we assume a fixed multiprogramming system
P: fOJ[PiIII...IIIPm]
and define the scheduling transitions of the associated timed transition system Sp for various
scheduling algorithms.
Greedy scheduling
The simplest reasonable scheduling strategy, as well as our default strategy, is yreedy. According
to this policy, the process that is currently in control of the processor remains active until all its
transitions are disabled. At this point an arbitrary other process with an enabled transition takes
over. Formally, the set T of transitions for the timed transition system Sp contains, in addition to
the entry transition ?, a single scheduling transition, 7G, with a' E T?(a) iff
= a(y) for all y E V --H
= ? for all action transitions TE,
r?(a') $ ? for some action transition TE.
If there is no cost associated with swapping processes, then 1?o = UTG = 0. If switching processes
is not instantaneous, then the minimal and maximal delays of TG should be adjusted accordingly.
Scheduling instructions
More flexible scheduling strategies can be implemented with explicit scheduling operations. For this
purpose, we enrich our programming language by the instruction resume(s), where 5 C .1....
determines a subset of processes. The scheduling operation resume(s) suspends the currently active
process, say, Pi and activates, nondeterministically, one of the processes i?' with i' E 5:
We write resume(i') for resume(fi'?) and suspend for resume(?l < i' < m i' $ iJ); that is,
the instruction suspend delegates the control from the currently active process to any one of the
competing processes.
Formally, the set T of transitions of Sp contains, in addition to the entry transition To, a scheduling
transition TE for every resume edge E in the timed transition diagrams for Pi... . Pm. If  connects
the source location to the target location Ck? and is labeled by the instruction c resume(s),
then a' E T?(a) iff
= i and a'(?) E 5,
= and a'(r?) = kt,
c is true in a,
= a(y) for all YE V --H fit.
Furthermore, for every scheduling edge E labeled by the minimal delay 1 and the maximal delay u,
let 1TE = 1 and ?rE =
17
Delays and timers
Note that the instruction
models a busy wait; the process Pi occupies the processor for 10 time units while waiting. To
implement a nonbusy wait, in which Pi releases the processor to a competing process for 10 time
units before resuming execution, we use a timer (alarm clock) T[io,ioj as a parallel process:
resume(i) [10, 10]1 [0,0] t?
T?io,ioj: #mto
t := false
We make sure that the timer T[10,10] is started (i.e., waiting for activation) when the process Pi
becomes active, with the precondition [t false]. Then the timer is activated by the process Pi
with the sequence
which releases the control of the processor to one of the processes in the set 5. After exactly 10 time
units, the timer process, which operates in parallel, will return the control of the processor to the
process Pi.
In general, a timer process T[i,u] marks nondeterministically a time period between 1 and n time
units and is executed in parallel to the other processes of a system:
f?][(P1III . . . IIIPm)IIsijtu]].
The activation of the timer T[t,uj is abbreviated by the delay instruction
The delay instruction allows us to program nonbusy delays without exp?citly mentioning timers;
we simply assume that there exists, implicitly, a unique timer process for every delay instruction
in a timed transition diagram. The parameter 5 of the instruction delay(s) determines the set of
processes from which a process is selected when the active process is delayed.
18
Round-robin scheduling
A construction that is similar to the timer example allows us to implement a round-robin scheduling
strategy for two processes P1 and P2 that share a single processor. In the system (P1 111P2)118s, the
scheduler
resume(2) [10, ???1??o, 10] resume(1)
MAto
gives each of the two processes P1 and P2 in turn 10 time units of processor time. Needless to say,
the explicit scheduling instructions give us the ability to design more sophisticated schedulers as
well.
4.3 Processor allocation
Both the multiprogramming system with a timer and the multiprogramming system with a central
scheduler are, in fact, combinations of multiprocessing and multiprogramming systems in which
several tasks compete for some of the processors. For these systems, the question of scheduling,
which determines the processor time that is granted to individual processes, is preceded by the
question of processor allocation, which determines the assignment of processes to processors. This
assignment can be either static, if every process is assigned to a fixed processor, or dynamic, if a
set of processes competes for a pool of processors and processes may reside, over time, at different
processors. We only hint how this very general notion of real-time system fits into our framework
and can be modeled by timed transition systems.
A static (shared-vanables or message-passing) system P with k processors is of the form
[oJ[(P1,1111 . . . iiIPi,m1 )II . . II(Pk,lIII . . . IIIPk,m?)];
that is, m? processes compete for the i-th processor. The definition of the associated timed transition
system Sp is straightforward: every processor has its own process control variable jt?, for 1 < i < k,
which ranges over the set of competing processes .1.... m?, I] and designates the active process.
Furthermore, every processor operates according to a local scheduling policy with a single entry
transition Tht for 1 <i < k.
To model systems in which a process competes for more than one processor, we write
for the dynamic system in which m processes compete for k processors according to some global
processor allocation and scheduling policy. To define dynamic systems, it is useful to have a more
general scheduling instruction, resume(s, x), which interrupts the process that is currently active
on processor x and activates, on processor x, one of the processes from the set s.
19
4.4 Priorities and interrupts
While the scheduling instruction resume gives us the flexibility to design a scheduler, we often wish
to adopt a simple, static scheduling strategy without having to explicitly construct a scheduler. In
this subsection, we offer this possibility by generalizing the greedy strategy. We assign a priority to
every transition, and at any point in a computation, choose only among the transitions with the
highest priority. If the transition with the highest priority belongs to a suspended process, then
the currently active process is interrupted and the execution of the suspended process is resumed.
A priority system P is a (shared-variables or message-passing, static or dynamic) system in which
a priority is associated with every instruction; that is, with every edge in the timed transition
diagrams for P. We use nonnegative integers as priorities (0 being the highest priority) and annotate
an edge with a priority p E N as follows:
We formalize the priority semantics only for simple multiprogramming systems; the generalization
to systems with several processors is straightforward. With a given priority system
P : ?oJ[P1III . . 111Pm],
we associate the foliowing timed transition system Sp = (V, ?, e, T, I, u):
o+ V, ?, and 0- are as before.
T contains, in addition to Tr, an action transition r? for every assignment edge E in the
transition diagrams for P1,... Pm. If E connects the source location to the target location
?tk and is labeled by the instruction p: c := e, then the transition rE competes in state
a and would lead to state a' (which is denoted by a ?E a') iff
= and a'(??) =
c is true in a and a'(x) =
a'(y) = a(y) for ally E V --H
Then a' E r?(a) iff
a ?E a' and a(?) = a'(jt) = i and
there is no edge E' that is labeled by a higher priority p' <p such that a ?E' a"
for some a
For any matching pair of communication edges E and ` that are labeled by the priorities p
and p', respectively, we take the higher priority min(p, p') for the combined transition TE,EI
(although this choice is arbitrary and may be reversed, if the need arises).
Furthermore, there is, in addition to the entry transition r0, a scheduling transition rp such
that a' E rp(a) iff
a'(y) = a(y) for all y E V --H
= ? for ali action transitions TE,
? for some action transition TE.
20
o+ Let 1TE and ttrE be as before, and choose 1rp and ttTp to represent the cost of swapping
processes.
Note that if all transitions have equal priority, then the scheduling strategy is greedy (that is,
rc = rp). Thus priorities generalize our previous discussion conservatively: all systems can be
viewed as priority systems whose instructions have the same default priority, unless they are anno-
tated with explicit priorities.
Dynamic priorities
Priorities can be combined with explicit scheduling operations in the obvious way. It is, however,
often more convenient to model dynamic scheduling strategies, which change over time, by dynamic
priorities, which can be modified by any process during execution. Dynamic priorities offer exciting
possibilities, such as the ability of a process to increase or decrease its own priority. Moreover, they
are easily incorporated into our framework. We simply use data variables that range over the
nonnegative integers N as priorities. Instead of giving the formal semantics of dynamic priorities,
which is constructed straightforwardly from the semantics of constant (static) priorities, we present
an interesting real-time application of dynamic priorities.
We have not yet pointed out that our interpretation of message passing is not entirely conser-
vative over the untimed case: there the set of legal execution sequences usually is restricted by
strong-fairness assumptions for communication transitions [MP89]. This is convenient for the study
of time-independent properties of a system, where simple fairness assumptions about "nondeter-
mirnstic" branching points abstract complex implementation details. Consider, for example, the
multiprocessing system P1IIP2IIQ that consists of the following three processes P1, P2, and Q:
a! [10, 10] [0,0] a?			p! [10,10] [0,0] p?
P1:			P2:
a!
(Recall that we may omit the data components of message-passing operations, if they are im-
material.) The arbiter Q mediates between the two processes P1 and P2 and uses synchronous
communication on the two channels a and ? to ensure mutual exclusion: P1 and P2 can never be
simultaneously in their critical sections ?i1 and ?2i, respectively.
Strong-fairness assumptions on the communication transitions are used to guarantee that, in addi-
tion to mutual exclusion, neither of the two processes P1 and P2 is shut out from its critical section
21
forever: the arbiter cannot always prefer one process over the other. Any such infinitary fairness
assumption, however, is clearly without bearing on the satisfaction of a real-time requirement such
as the demand that a process has to wait at most 10 time units before being able to enter its
critical section. As has been the case with scheduling, we encounter again a situation in which the
infinitary notion of "fairness" is adequate for proving untimed properties, yet entirely inadequate
for proving timing constraints. To verify compliance with real-time requirements, we can no longer
forgo an explicit description of how the arbiter Q decides between the two processes P1 and P2
when both are waiting to enter their critical sections. For instance, the following refinement Q' of
Q never makes the same "nondeterministic" choice twice in a row:
a?;p:=l; =0
p: a!
p := 0; q := 1
q: fi!
(We use semicolons to group several instructions to an atomic transition, which is defined in the
obvious fashion. The default value of priorities is assumed to be 1.) The arbiter Q' modifies the
priorities p and q of its nondeterministic alternatives to ensure that the system
fp = q = 11[P1IIP2IIQ']
satisfies the requirement that each process has to wait at most 10 time units before being able to
enter its critical section. Note that none of the two nondeterministic alternatives is ever disabled,
but, at any time, one of them is "preferred."
Finitary branching fairness
Since infinitary fairness assumptions, such as weak fairness for scheduling and strong fairness for
synchronization, are insufficient to guarantee the satisfaction of real-time deadlines, one may choose
to add finitary branching conditions to timed transition systems. Such a finitary notion of fairness
would restrict the nondeterminism of a system. We may want to require, for example, that no
competitor of a transition r can be taken more than n times without r itiself being taken (a
similar concept has been called bounded fairness in [Jay88j). We prefer, both for scheduling and
synchronization, an explicit description of the selection process to such implicit assumptions. Since
all selection processes that we have found useful can be described within our language, we see no
need to introduce additional concepts that would only complicate any verification methodology.
5 Conclusion
With timed transition systems, we presented an abstract model for real-time systems. We then
explored its scope and demonstrated its practicality by modeling many important constructs of
real-time computing. We conclude by pointing out that any abstract description of a real-time
system ought to meet certain theoretical requirements as well. In [Hen9lb], we suggested that
system descriptions be (1) refinable, (2) digitizable, and (3) operational, and we showed that timed
transition systems satisfy all three criteria:
22
1.
2.
We associated a fixed set of global states with every real-time system. This static view
prohibits the study of large systems for managerial reasons. With each step in the hierarchical
specification, design, and verification of a complex system, the state space must be refinable
through expansion of its visible portion [Lam83]. The vertical decomposition of systems
can be formalized by refinement mappings between increasingly detailed system descriptions
[AL88j. Since expanding the visible portion of the state space may increase the frequency at
which state changes occur, the timed state sequence semantics of a system description needs
to be closed under our notion of stuttering to guarantee the existence of refinement mappings.
The refinability of timed transition systems is further discussed in [llen9lb].
For verification, it is often convenient, and sometimes necessary, to assume a fictitious digital
clock, which records the times of state changes with finitary precision only [AH89]. The
integers suffice as time domain for such a digital-clock model. For the direct use of a digital-
clock model, a system description must be independent of the time domain, in the sense
that digitizing all execution sequences of a system can be achieved by simply changing the
time domain from the reals to the integers. Sets of timed state sequences that enjoy this
property are called digitizable. The digitizability of timed transition systems and the ensuing
amenability to discrete-time verification methods is discussed in [Hen9lb].
3. We want a system description to be executable. For untimed systems, this is the case if the
liveness component of a system description does not preclude any safe prefixes of execution
sequences; that is, a stepwise interpreter cannot "paint itself into a corner" from which no
continuation is possible [AFK88]. The issue is more subtle in the timed case because of the
implicit liveness requirement that time must progress eventually. In other words, we wish to
rule out system descriptions that prevent time from progressing. Such system descriptions are
called operational [Hen9laJ (or machine-closed [LA]). The operationality of timed transition
systems is discussed in [Hen9lb].
No study of an abstract model for real-time systems is complete without progress on the verification
front. Let P be a real-time system whose set of possible timed executions is the set ?P? of timed
state sequences and let ? be a specification that is satisfied by the timed state sequences in the set
[?. Verification of P with respect to ? amounts, then, to checking the containment
of sets of timed state sequences. Systems are given as expressions of an implementation language;
specifications as expressions of a specification language. We presented the implementation language
of timed transition diagrams and defined the set ?P? of timed executions for systems that are
given in the timed transition diagram language as the set of computations for the timed transition
system Sp. Verification methods of timed transition systems have been developed for various
logical specification languages. The methods include both algorithmic techniques for finite-state
systems [AH89, AH9O, HLP90, Ost90, Hen9lb] and deductive techniques based on proof systems
[Hen90, Ost90, HMP9l, Hen9lb]. For an overview of the verification methods for timed transition
systems, we refer to the article Logics and Models of Real Time in this volume.
Acknowledgment. The authors thank Rajeev Alur and Eddie Chang for many helpful comments.
23
References
[AFK88] K.R. Apt, N. Francez, and 5. Katz. Appraising fairness in languages for distributed
programming. Distributed Computing, 2(4):226--H241, 1988.
[AH89] 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.
[AH9O]
[AL88]
[BKP86]
[Har88]
[Hen9Oj
R. Alur and T.A. Henzinger. Real-time logics: complexity and expressiveness. In
Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pages 390--H
401. IEEE Computer Society Press, 1990.
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.
II. Barringer, R. Kuiper, and A. Pnueli. A really abstract concurrent model and
its temporal logic. In Proceedings of the 13th Annual Symposium on Principles of
Programming Languages, pages 173--H183. ACM Press, 1986.
E. Harel. Temporal analysis of real-time systems. Master's thesis, The Weizmann
Institute of Science, Rehovot, Israel, 1988.
T.A. Henzinger. Half-order modal logic: how to prove real-time properties. In Proceed-
ings of the Ninth Annual Symposium on Principles of Distributed Computing, pages
281--H296. ACM Press, 1990.
[Hen91a? T.A. Henzinger. Sooner is safer than later. Technical report, Stanford University, 1991.
[Hen91b] T.A. Henzinger. The Temporal Specification and Verification of Real-time Systems.
PliD thesis, Stanford University, 1991.
[HLP9O]
[HMP9o]
[HMP91]
E. Harel, 0. Lichtenstein, and A. Pnueli. Explicit-clock temporal logic. In Proceedings
of the Fifth Annual Symposium on Logic in Computer Science, pages 402--H413. IEEE
Computer Society Press, 1990.
T.A. Heuzinger, Z. Manna, and A. Pnueli. An interleaving model for real time. In
Proceedings of the Fifth Jerusalem Conference on Information Technology, pages 717--H
730. IEEE Computer Society Press, 1990.
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.
[Hoa85] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
[Jay88] D.N. Jayasimha. Communication and Synchronization in Parallel Computation. PhD
thesis, University of Illinois at Urbana-Champaign, 1988.
[Kel76] R.M. Keller. Formal verification of parallel programs. Communications of the ACM,
19(7):371--H384, 1976.
24
[KSdR+ 88]
[LA]
[Lam83]
[MP89]
[Ost9O]
[PH88]
R. Koymans, R.K. Shyamasiindar, W.-P. de Roever, R. Gertli, and 5. Arun-Kumar.
Compositional semantics for real-time distributed computing. Information and Com-
putation, 79(3):210--H256, 1988.
L. Lamport and M. Abadi. Refining and composing real-time specifications. This
volume.
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--H
668. Elsevier Science Publishers (North-Holland), 1983.
Z. Manna and A. Pnuell. The anchored version of the temporal framework. In J.W.
de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time,
and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer
Sdence 354, pages 201--H284. Springer-Verlag, 1989.
J.S. Ostroff. Temporal Logic of Real-time Systems. Research Studies Press, 1990.
A. Pnueli and E. Harel. Applications of temporal logic to the specification of real-
time systems. In M. Joseph, editor, Formal Techniques in Real-time and Fault-tolerant
Systems, Lecture Notes in Computer Science 331, pages 84--H98. Springer-Verlag, 1988.
[Pnu77] A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Sym-
posium on Foundations of Computer Science, pages 46--H57. IEEE Computer Society
Press, 1977.
25
