BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1330
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Temporal Proof Methodologies for Timed Transition Systems
AUTHOR:: Henzinger, Thomas A.
AUTHOR:: Manna, Zohar 
AUTHOR:: Pnueli, Amir
DATE:: March 1993
PAGES:: 51
ABSTRACT::
We extend the specification language of temporal logic, the corresponding 
verification framework, and the underlying computational model to deal with 
real-time properties of reactive systems. The abstract notion of timed 
transition systems generalizes traditional transition systems conservatively: 
qualitative fairness requirements are replaced (and superseded) by 
quantitative lower-bound and upper-bound timing constraints on transitions. 
This framework can model real-time systems that communicate either through 
shared variables or by message passing and real-time issues such as timeouts, 
process priorities (interrupts), and process scheduling.

We exhibit two styles for the specification of real-time systems. While the 
first approach uses time-bounded versions of the temporal operators, the 
second approach allows explicit references to time through a special clock 
variable. Corresponding to the two styles of specification, we present and 
compare two different proof methodologies for the verification of timing 
requirements that are expressed in these styles. For the 
bounded-operator style, we provide a set of proof rules for establishing 
bounded-invariance and bounded-response properties of timed transition 
systems. This approach generalizes the standard temporal proof rules for 
verifying invariance and response properties conservatively. For the  
explicit-clock style, we exploit the observation that every time-bounded 
property is a safety property and use the standard temporal proof rules for 
establishing safety properties.
END:: CORNELLCS//TR93-1330
BODY::
Temporal Proof Methodologies for
Timed Transition Systems*t
Thomas A. Henzinger
Zohar Manna
Amir Pnueli
TR 93-1330
March 1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*This research was supported in part by an IBM graduate fellowship, by the National
Science Foundation under grants CCR-891 1512, CCR-891 3641, and CCR-9200794,
by the Defense Advanced Research Projects Agency under contract N00039-84-C-
0211, by the United States Air Force Office of Scientific Research under contracts
AFOSR-90-0057 and F49620-93-1-0056, and by the European Community ESPRlT
Basic Research Action project 3096 (SPEC).
t A preliminary version of Part I of this paper appeared in the proceedings of the
1991 REX Workshop on Real Time: Theory in Practice [HMP92a]; a preliminary
version of Part II appeared in the proceediings of the 1991 ACM Symposium on
Principles of Programming Languages [HMP91 j.
Temporal Proof Methodologies
for Timed Transition Systems"2
Thomas A. Heuzinger
Department of Computer Science
Cornell University
Ithaca, NY 14853
Zohar Manna
Department of Computer Science
Stanford University
Stanford, CA 94305
Amir Puneli
Department of Applied N?Iathematics
The ?`eizmann Institute of Science
Rehovot, Israel 76100
Abstract. ?Ve extend the specification language of temporal logic, the corresponding verification
framework, and the underlying computational model to deal with real-time properties of reactive
systems. The abstract notion of timed transition systems generalizes traditional transition systems
conservatively: qualitative fairness requirements are replaced (and superseded) by quantitative
lower-bound and upper-bound timing constraints on transitions. This framework can model real-
time systems that communicate either through shared variables or by message passing and real-time
issues such as timeouts, process priorities (interrupts), and process scheduling.
We exhibit two styles for the specification of real-time systems. While the first approach uses
time-bounded versions of the temporal operators, the second approach allows explicit references
to time through a special clock variable. Corresponding to the two styles of specification, we
present and compare two different proof inethodologies for the verification of timing requirements
that are expressed in these styles. For the bounded-operator style, we provide a set of proof rules
for establishing bounded-invariance and bounded-response properties of tiined transition systems.
This approach generalizes the standard temporal proof rules for verifying invariance and response
properties conservatively. For the e plicit-ciock style, we exploit the observation that every time-
bounded property is a safety property and use the standard temporal proof rules for establishing
safety properties.
1This research was supported in part by an IBM graduate fellowship, by the Natioiial Science Foondation under
grants CCR-8911512, CCR-8913641, and CCR-9200794, by the Defense Advanced Rescarch Projects Agency under
contract N00039-84-C-0211, by the United States Air Force Office of Scientific Research under contracts AEOSR-90-
0057 and F49620?93-1-0056, and by the European Community ESPRIT Basic Research Action project 3096 (SPEC),
2A preliminary version of Part I of this paper appeared ill the proceedings of the 1991 REX ?Vorkshop on Rent
Time: Theory in Practice [HMP92a]; a preliminary version of Part fi appeared in the proceedings of the 1991 ACM
Symposium on Principtes of Programming Languages [HMP9lj.
1			Introduction
It is self-evident that the most sensitive and critical among reactive systems, and therefore the
ones for which formal methods are needed most direly, are real-time systems. The qualitative
requirement of responsiveness, that every environment stimulus p must be foliowed by a system
response q, is not adequate for systems with hard real-time deadlines; timeliness has to be ensured
through the stronger quantitative requirement of timed responsiveness, which imposes a bound on
the time interval that is permissible between the stimulus p and the response q. Temporal logic
has been used successfully for the specification and verification of qualitative properties of reactive
systems (see, for example, [Pnu86j for a survey). Over the past few years, there have been several
suggestions for extending the expressive power of temporal logic to handle quantitative timing
constraints. These attempts can be roughly ctassified into two approaches.
The first approach, to which we refer as the bounded-operntor approach, introduces for each tem-
poral operator, such as ? (eventualig) one or more time-bounded versions. For example, while the
formula ?q asserts that the event q will happen "eventually" but puts no time bound on when
it will happen, the formula ?<3 q predicts an occurrence of q within 3 time units from now. The
early proposal [B1181] can be viewed as a precursor of this approach to the specification of timing
properties, which has been advocated in [KVdR83, KdR85, Koy9Oj, where the bounded-operator
language is called Aletric Temporal Logic, and in [SPE84]. Bounded-operator temporal logics have
been analyzed for their complexity and expressiveness in [EMSS89] and in [AH9o, AFH9i].
An alternative approach to the specification of tilning constraints of reactive systems introduces no
new temporal operators but interprets, at each state, one of the nonrigid state vanables (we use the
variable now) as the current time. N\?e refer to this approach as the cxplicit-clock approach, because
the only new elen?nt is the ability to refer explicitly to the clock. Scattered examples of this method
of expressing timing properties have been presented in [PdR82j, in [RonS4], and in [Rar8?, PH88j. A
more systematic exposition of this approach and its applications can be found in [Ost90], where the
explicit-clock language is called Real-time Temporal Logic, and in [LA92j. Explicit-clock temporal
logics have been analyzed for their complexity and expressiveness in [AH9o] and in [HLP9O].
To compare the two approaches, consider the requirement of a timely response q to stimulus p
within at most 3 time units. In the bounded-operator approach, this requirenient is sped?ed by
the formula
p			_
In the explicit-clock approach, it is expressed by the formula
(p A naw = t) ? (q A now < t + 3),
where the rigid variable t is used to record the time of the p-state.
The main contribution of this paper is the elaboration of two proof systems that correspond,
respectively, to the two styles for the specification of timing requirements.
It is a well-known observation that with the introduction of an explicit-clock variable, all time-
bounded properties can be defined by safety formulas ([Hen92]). For example, the timed response
property that, in either style, is expressed above by a liveness-like formula (employing the liveness
operator ?) can alternatively be specified by a formula that uses the clock variable now and the
safety operator U (unless):
(p A now = t)			(now < t + 3) U q.
2
This formula asserts that if p happens at time t, then from this point on the time will not exceed
t + 3 either forever (which is ruled out by an axiom that requires tirne to progress eventually)
or until q happens. Consequently, q must occur within 3 time units from p. It follows from this
translation that no new proof rules are necessary for the explicit-clock style of timed specification;
all time-bounded properties can, in principle, be verified using a standard, uniform set of timeless
rules.
On the other hand, when pursuing the bounded-operator style of timed specification, one discerns a
clear dichotomy between upper-bound properties such as the bounded-response formula p ?<3 q
considered above, and Thwer-bound properties, such as the bounded-invariance formula
p
which states that q cannot happen sooner than 3 time units after any occurrence of p. While
upper-bound properties assert that something good" will happen within a specified amount of
time, lower-bound properties assert that `?nothing bad" will happen for a certain amount of tiine.
Clearly, while the class of upper-bound properties bears a close resemblance to liveness properties,
the class of lower-bound properties closely resembles safety properties. The proof system we present
cultivates both similarities by including separate proof principles for the classes of lower-bound and
upper-bound properties. These proof principles can easily be seen to be natural extensions of the
standard proof rules for the untimed safety (invariance) and liveness (response) classes, respectively.
In our model, we assume a global, discrete, and asynchronous clock, whose actions (clock ticks)
are interleaved with the other system actions ([HMP9oj). 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+88j).
One of the points that we demonstrate in this paper is a refutation of this 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.
Part I discusses the modeling of real-time systems by transition systems. In Section 2, we intro-
duce the abstract computational modd of timed transition systems. The subsequent two sections
illustrate how concrete real-time systems can be mapped into this model and how typical real-time
phenomena can expressed within the model. We begin, in Section 3, with the representation of
real-time processes that are executed in parallel and communicate either through a shared mem-
ory 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 multiprogramming, where several tasks reside on the sanie 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.
Part II follows with techniques for the verification of timed transition systems. Section 5 intro-
duces the bounded-operator specification language, and Section 6 presents a proof system for this
language. In Section 7, we discuss the alternative, explicit-clock, approach. Section 8 concludes by
giving completeness results for both methods.
3
Part I
Modeling Real-time Systems
We define the formal semantics of a real-time system as a set of timed execution sequences. This
is done in two steps. First, we introduce the absfract notion 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 to interpret the concrete constructs within
the abstract modd. We demonstrate that this framework can model a wide variety of real-time
phenomena that are encountered in practice, including the timed execution of both multiprocessing
and multiprogramming systems.
2 Abstract Model: Timed Transition Systems
The basic computational model we use is that of transition systems ([Kd76, Pnu77J). We generalize
this model by imposing timing constraints on the transitions and show that the timing constraints
can be interpreted operationally. Similar state-transition formailsrns with minimal and maximal
delays on the transitions have been defined in [PH88j, in [Ost90J, and in [LA 90, MMT9lJ.
2.1 Transition systems
A transition system is a set of states together ?4th a set of transitions (actions) that transform
states. In this paper, we will be concerned with a concrete notion of state that provides values for a
certain set of variables. Hence we define a transition system S = (V, V, ?., T? as a tupie consisting
of four components:
1. a finite set V of variables.
2. a set ?? of states. Every state a C V is an interpretation of V; that is, it assigns to every
variable x ? V a value a(:r) in its domain.
3. a subset 0- C ? of initial states.
4.
a finite set 1 of transitions, including the idle transition ?I Every transition 7 ? 1 is a binary
relation on ?; that is, it defines for every state a Ei ? a (possibly empty) set of 7-successors
7(a) C ?. We say that the transition 7 is enabled on a state a iff ?(a) $ ?. In particular,
the idle (stutter) transition
is enabled on every state.
An infinite sequence a = a0a1a2 ... of states is an initialized computation (execution sequence, run)
of the transition system S = (V, V?, ?., 1) iff it satisfies the following two requirements:
Initiality a0 ? 0-.
Consecution For all > 0 there is a transition 7 ? I such that Q+i C 7(Q) (which is also denoted
by aj ? ai+i). We say that the transition 7 is taken at position i and completed at position
i + 1 of a.
4
Any execution sequence can, therefore, be thought as consisting of an initial state and an infi-
nite sequence of transitions. Finite (terminating as well as deadlocking) execution sequences are
generally represented by infinite extensions that add only idle transitions. The computations of
a transition system are obtained by closing the set of initialized computations under suffixes: the
state sequence a is a computation of 5 iff a is a suThx of an initialized computation of 5.
2.2 Adding timing constraints to transition systems
We incorporate time into the transition system modA 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
tower bound of 0; the absence of an upper-bound requirement by an upper bound of no. For
notational convenience, we assume that no > n for all n ?
A timed transition system 5 = (?`, ?, 0-, `T, I, u? consists of an undeHying transition system 5 --H
as well as
.?. a minimal delay l? ? N for every transition r C I. We require that l?? = 0.
6. a maximal delay u? ? N u fno? for every transition ? ? T. We require that UT > 1T for all
7 E T, and that UT = no if ? is enabled on any initial state in 0. In particular. UTr = no.
Let % c T be the set of transitions with the maximal delay 0. To ailow time to progress, we
put the following operationality rcstriction on these transitions: there is no sequence
T0 Ti
a0 --H a1 --H . --H
of states and transitions such that n > jT0 and Tj ? T0 for all 0 < i ?
The requirement that all transitions that are initially enabled are not constrained by a finite
maximal delay will be consistent with our interpretation that the initial state of an execution
sequence is the state in which the system has resided for an infinite amount of past time. The
operationality requirement that there is no loop of transitions with a combined maximal delay of 0
will ensure that the system cannot prevent time from advancing.
Timed state sequences
We model the values of a fictitious global clock by the integers Z. The clock ticks are interleaved
with the system actions, and thus at any point of an execution sequence of a timed system, either
the system state changes or the dod: value changes (or neither). A timed state sequence p = (a, T)
consists of an infinite sequence a of states Q ? ?, where i > 0, and an infinite sequence T of
corresponding times (clock values) Tj e Z that satisfy the following conditions:
Bounded monotonicity For all i > 0
either Tj+1 = Tj,
or Tj+1 = Tj + 1 and Q+i =
that is, time never decreases. It may increase, by at most 1, 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 stuttering step; the case that the time increases by 1 is called a clock tick.
5
Progress For all i > 0 there is some j > ? such that 1) ? T??; that is, time never stagnates. Thus
there are infinitely many clock ticks in every timed state sequence.
We will also write the timed state sequence p as an infinite sequence
(ao, T0) --H (ai,T?) --H (a2,T2) --H (a3,T3) --H
of state-time pairs. By p? = (ai, T?) we denote the ?-th svffix of the timed state sequence p;
it consists of the infinite sequence a = ?jQ+1Q+2 ... of states and the infinite sequence T? =
TjTj+1Tj+2 . . . of times. Note that p? is, for all `i > 0 again a timed state sequence; that is, the set
of timed state sequences is closed under suffixes.
Timed execution sequences
Just as the execution sequences of transition systems are infinite state sequences, we modA the
execution sequences of timed transition systems by timed state sequences. The timed state sequence
p = (a,T) is an initialized cornputatio'n of the timed transition system S = (V, v, ?, T, I, u) iff the
state sequence a is an initialized computation of the underlying transition system 3--H and
Lower bound For every transition 7 E I and all positions i > 0 and j > iwfth % < Tj + IT
if 7 is taken at position j,
then 7 is enabled on Q.
in other words, once enabled, 7 is delayed for at least 1T clock ticks; it can be taken only
after being continuously enabled for 1T 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).
Upper bound For every transition 7 ? I and position i > 0 there is some position j > with
Tj --H			+ Ur such that
either 7 is not enabled on
or 7 is taken at position j.
in other words, once enabled, 7 is delayed for at most Ur clock ticks; it cannot be continu-
ously enabled for more than flr time units without being taken. Since the maximal delay of
every transition that is enabled initially must be cc, the first state change of an initialized
computation may occur at any (integer) time.
We point out that the lower-bound condition does not rule out that a transition 7 is taken several
times within a time interval of length 1?; this situation may occur if 7 stays enabled after being
taken and, if undesirable, can be prevented by refining the state space. Also note that at both
stuttering steps and clock ticks of an initiahzed computation, the idle transition 7i is taken. Thus
an execution sequence of a timed transition system consists of an initial state and a fair merge of
(1) a (finite or infinite) sequence of transitions and (2;) an infinite sequence of clock ticks.
A timed state sequence p is a compumtion of the timed transition system 5 iff p is a suffix of an
initialized computation of 5. 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 com-
putations of 5 is also satisfied by all computations of 5. The converse, however, is generally not
6
true. The timing constraints of 5 can be viewed as filters that prohibit certain possible behaviors
of 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--H, the tatter adds to 5 a weakfaim?ess (justice)
assumption in the sense of [MP92]: T cannot be continuously enabled without being taken. By
ST we denote the weakly-fair transition system that is obtained from the transition system 5--H
underlying 5 by adding weak-fairness requirements for all transitions with infinite maximal delays.
Closure properties
Both the computations and the initialized computations of any timed transition system are closed
under stuttering and under shfting the origin of time:
o+ The addition of finitely many stuttering steps to a timed state sequence does not alter the
property of being an (initialized) computation of 5.
The addition of an integer consta?t to all times of a timed state sequence does not alter the
property of being an (initialized) computation of 5. In other words, timed transition systems
cannot refer to absolute time. Thus we will often assume, without loss of generality, that the
time of the first state change of a computation is 0.
2.3 Operationality of timed transition systems
In this subsection, we show that the timed transition system model is operational (machine-closed
[AL88]), in the sense that execution sequences can be generated increinentally by a machine that
adds one state at a time. Untimed transition systems specify safety properties and are, therefore,
trivially "executable" in a stepwise fashion:
Start with an initial state, and at each point during the stepwise construction of an
execution sequence choose, nondeterministicaily, any one of the enabled transitions.
To generate an execution sequence of a timed transition system, at each step we have to either choose
a transition (without incrementing time) or iucrement time (while taking the idle transition). In
addition, a timed execution sequence has to meet the liveness requirements imposed by maximal
transition delays of co and by the progress condition on time. While maximal delays of oo are
standard fairness conditions that can always be met ([AFK88]), we need to show that the stepwise
execution of a timed transition system cannot lead to a situation in which time cannot advance
ever.
Let 5 = (V, v?, ?, T, I, u? be a timed transition system. A finite prefix p = (a, T) of a thiied state
sequence is a partial computation of 5 iff it satis?es the initiality, consecution, and lower-bound
requirements of initialized computations, and
Finite upper bound Let n be the number of state-time pairs in p. For every transition 7 E T
and position 0 < i < n, either Tn?1 < Tj + UT or there is some position i ? 1 < n with
Tj < Tj + ?r such that either 7 is not enabled on aj, or 7 is taken at position j.
Proposition 1. Each partial computation of a timed transition system 5 is a prefix of an initialized
computation of 5.
Proof. We use the following strategy to extend a partial computation of the timed transition
system 5. Let T be the transition set of 5 and let N > (IT + 1)2 be any sufficiently large integer
constant. We alternate two phases:
Phase 1 For at least N positions, increment time whenever possible; that is, if all enabled transi-
tions can be delayed for another time unit. On the other hand, if there are any transitions
whose (finite) upper-bound requirements prevent the progress of time, take any one of these
transitions.
Phase 2 Once every i? positions, take every transition with a maximal delay of oo that has been
enabled long enough. This phase satisfies all infinite upper-bound requirements.
The only way for this strategy not to yield an initialized computation of 5 is because, from some
point on, time does not advance. Iii this case, there has to be a phase-I sequence p of length I\T + 1
of the form
(Q,Ti) Ji (Q+i,T) Th1 ... Ti+N?1 (ai+N,Ti,).
The sequence p must contain a subsequence p' of length I? + 1 such that every transition in p' has
been taken at least once before in p. It is not hard to see that, contrary to our assumption, the
state component of p' violates the operationallty restriction on maximal delays. I
Proposition 1 guarantees that a madiine that incrementally generates partial computations cannot
arrive in a situation in which the progress condition on time cannot be satisfied. It follows that timed
transition systems are machine-dosed with respect to the progress of time (nonzeno [Ren92, LA92]);
they may be "executed" using the following procedure:
Start with an initial state, and at each point during the stepwise construction of an
execution sequence either choose a transition that has been enabled long enough, or
increment time provided that all enabled transitions can be delayed for another time
unit.
3 Concrete Model: 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 timeouts 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
II IIP?,i
Each process Pj, 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 boolean
expression 0, called the data precondition of P, restricts the initial values of the variables in
U = U5u ? Uj.
The real-time programs Pj can be alternativdy 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 labehng transitions with minimal and maximal
time delays. A timed transition diagram for the process 1) is a finite directed graph whose vertices
= f0?,.. ?nt..Y are called Theations. The entry location --H? usually % is indicated as follows:
The intended meaning of the entry location 0? is that the control of the process Pi starts at the
location b 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 over the variables in
U8 u Uj, a minimal delay 1 ? N and a maximal delay u ? N u foo? such that it > I:
where the guard c is a boolean expression, x is a vector of variables, and (T an equally typed vector
of expressions (the guard true and the delay interval [0, cc] 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 I ensures the
process Pj may proceed to tlie location ?k?. only if the control of Pi has resided at the location 4;
for at least 1 time units during which the guard c has been continuously true; such a move from
to kk occurs "instantaneously" and assigns the current values of e to the variables ?. The maximal
delay it ensures that the control of some process in P must proceed before the control of Pi would
have resided at the location 4 for more than it time units with the guard c continuously true; such
a move can be accomplished either by Pj itself or by a competing process that falsifies the value
of c. It follows that the control of a process 1) may remain at a location 4 forever only in one of
two situations: if 4 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 4 is false infinitely often, we say that
Pi has deadlocked. The second condition is necessary (afthough not sufficient) for 14 to deadlock,
because if one guard is true forever, then the corresponding maximal delay II ? cc guarantees the
progress of Pi.
3.2 Semantics: Timed transition systems
The informal operational view of timed transition diagrams can be captured formally by a simple
translation into the abstract model of timed transition systems. With the given shared-variables
multiprocessing system
P : [()?[Pill . 11Pm],
we associate the following timed transition system Sp = (V, ?, 0, T, 1, it):
1. V = U U ....... rmY. Each control variable for 7rj, where 1 ? _ m. ranges over the set
Li U [I;'. The value of r? indicates the location of the control of the process P?; it is I
(undefined) before the process 14 starts.
2. ? contains all interpretations of V.
3. 0 is the set of all states a ? "` such that () is true in a and a(ir?) = I for all 1 ? i < m.
4. T contains, in addition to the idle transition Tj, an entry transition mi for every process 14,
where 1 < i < m, as well as a transition TE for every edge  in the timed transition diagrams
for Pi,... Pm. In particular, a' ? %i(a) iff
9
= I and a'(ir?) =
= a(?) for all y ? V --H
if  connects the source location to the target location ?k? and is labeled by the instruction
c			e, then a' E 7?(a) iff
= ft and a'(?) =
c is true in a and a'(x) = a(eD),
= a(?) for all y E V --H (r?, x??.
If ? is uniquely determined by its source and target locations, we wnte 7j?k
5. If T is an entry transition, then IT = 0. For every edge F labeled by the minimal delay I, let
iTE =1
6. If T is an entry transition, then UT = 00. For every edge  labeled by the maximal delay u,
let ?TE =
This translation detines the set of possible computations of the concrete real-time system P as a
set of timed state sequences. The ma?mal delays of 00 for all entry transitions guarantee that each
component process of P is started at some time. The condition on timed transition diagrams that
every cycle contains at least two edges ensures that, except for the idle transition, each transition of
the timed transition system Sp is disabled upon completion; the condition that every cycle contains
at least one positive (nonzero) maximal delay ensures that Sp is operational.
For instance, the initialized 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 the two sequences
(1,0)			(?, 0)			(i, 0)			(i, 1) --H?e
(1,0)			(?o,0)			(o,l)			(i,1)
under stuttering and shifting the origin of time (there are no data variables).
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 00). Then the state components of the initialized
computations of Sp are precisely the legal execution sequences of P, as de?ned in the interleaving
model of concurrency, that are weakly fair with respect to every transition ([??P92J): 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: Timeout and timely response
To demonstrate the scope of the timed transition diagram language, we model two common real-
time phenomena as shared-variables mukiprocessing systems. in the first example (timeout), a
process checks if an external event (i.e., an event caused by another, parallel, process) happens
within a certain amount of time. iii 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.
Timeout
To see how a timeout situation can be programmed, consider the process P with the following
timed transition diagram:
true?
When at the location o, the process F attempts, for 10 time units, to proceed to the location i 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 2 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 might 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 valtie of x at
least once every u time units. Consequently, if the value of x is 0 for more than u time units, this
will be detected. On the other hand, the value of x being 0 may go undetected if it ?uctuates 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 PE. Whenever the request button is pushed, the
shared boolean variable request is set to true:
Ji?:
request := true
Recall that the edge labels true? and [0, oc] are suppressed; thus there are no restridions on the
frequency of requests.
We want to design a traffic light controller Pc 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, in comparison, the time needed for
local operations within ?c is negligible. Now let us specify the desired process Pc. The controller
?c should behave in such a way that the combined system
P: (request = false, light = red? [P?IIPc]
satisfIes the following three correctness conditions:
(A) Whenever request is true, then light is green within 5 time units for at least 5 time units.
l1
(B) V\rhenever request is true, then request is false within 25 time units.
(C) ?Vhenever 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 tilne units to do so. The second condition, (B), ensures that the
request button is reset and the third condition, (C), prevents the light from being always green.
[1,1] _
light := green
Th
It is not hard to convince ourselves that, once it is started, the following process Pc satisfies the
specification:
?request
liQht:=red
[1,1]
request := false [0, 0]
light := green
request
request := false
for any delay 4 < 6 < 23. This implementation of the traffic tight controller turns the light green
as soon as possible after a request is received and then waits for 6 time units. If the request button
has been pushed in the meantime, the light stays green for another 6 time units; otherwise the light
is turned red again.
Multiple traffic lights
We now generalize the traffic light example and design a system that reacts to two different types
of external events. For this purpose, it will be convenient to accept some additional assumptions
about the frequencies of the external events. In particular, we modify our example by adding the
assumption that any two requests are at least 15 time units apart; that is,
[15, [0,0] request: true
AMY
Under this assumption, we can simplify the traffic light controller to
Pc,:			light:=red
[1,1]
request := false [0, 0]
1
12
for any delay 4 < ? < 17. The combined system
: ?request = false, light = red? [P?'IIPc']
still satisfies the three correctness requirements (A), (B), and ((?).
Now consider a more complex traffic light configuration, with two lights and two re(juest buttons
on two independent streets. The second light is designed for the speciat convemence of pedestrians
in a hurry: it is required to turn green within 3 time units of a request but, 011 the other hand,
has to stay green for only 3 time units. ?Vhile pedestrians arrive at the first light with a frequency
of at most one pedestrian every 15 tilne units, we assume that the more urgent requests are less
frequent only one every 30 time units:
[15, co] [0, 0] request1 := true [30, cc12I [0, ()] request2 := true
P?1: MAcol			P?2:
The controller for both lights executes the following two processes:
light := red
[1,1]
request1
request1 := false [0, 0]
[1,1]
green
Thqh4M=red
[1,1]
request2
request2 := false [0, 0]
21			?qht2 := green
If the combined traffic light controller makes use of two processors and the processes Pc1 and 1)c2
are executed in a truly concurrent fashion, then the correctness of the entire system
Pi : (request1 = request2 = false, light1 = light2 = red? [PE1IIPE2 IPc1IIPc2]
follows from the correctuess of its parts. Specifically, if 4 ? ?1 < 17 and 2 < ? ? 23, then all runs
of Pi 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 tinie units.
13
(B1) Whenever request1 is true, then request1 is false within 25 time units.
(B2) Whenever request2 is true, then request2 is false within 25 time units.
(C1) Whenever request1 has been false for 25 time units, then light1 is red.
(C2) Whenever request2 has been false for 25 time units, then light2 is red.
A more interesting case arises if only a single processor is available to control both lights and the
two processes Pc1 and Pc2 have to share it. Vsing the interleaving (shuffle) operator II of [Hoa85]
(to be defined), we will denote the resulting system by the expression
Pi ?request1 = request2 = false, light1 = light2 = red? [PE1 IlPE2 II(Pc1 I?IPc2)].
Note that the behavior of the environment PE1 IlPE2 is still truly concurrent to the behavior of the
traffic light controller 1)c1 I Pc2, which executes both processes Pc1 and `)c2 on a single processor
in an interleaved fashion.
Let us assume that 6i = 10 and 62 = 2, in which case Pi is correct. However, if we have no
knowledge about the strategy by which the processes Pc1 and Pc2 are scheduled on the processor
they share, other than that it is fair (i.e., the turn of each process will come eventually), then P11
does not satisfy the specification consisting of the requirements (Aj), (Bi), and (Ci) for `i = 1,2.
For suppose that the process Pc1 is always given priority over the process Pc2, and the traffic light
controller receives a request for the second light only one time tillit 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 (?42) On the other hand, if the process Pc2 that serves the more
urgent yet less frequent requests is always given priority over the process Pc11 then p1j1 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 formalize the interleaved execution of processes and discuss the modeling of priorities
and interrupts in detail, we first introduce message-passing operations for the parallel execution of
processes.
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 synclironization and communication of
parallel processes.
Syntax
A (message-passing) multiprocessing system P has the lorm
[oY[P111 . . . IIi?ni1
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 Us of data variables (in the case of pure message-passing
systems, U5 = ?) and a set of message channels. We use again timed transition diagrams to represent
processes, but enrich the repertoire of instructions by guarded send and receive operations. The
14
send operation o'!e outputs the value of the expression e on the channel ?. The receive operation
a?r reads an input vallie from the chaund 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:
p?.			t			a!e
14i:			i;			c --H a?x
For any two matching comn?unication instructions with the delay intervals [I, u] and [I', n'], respec-
tively, we require that niax(i, I') ? min(%L, u').
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(1, 1') time units, the control of the process 14 has resided
at the location and the control of the process 141 has resided at the location and the guards c
and c' have been continuously true. Then 14 and 141 may proceed, synchronously, to the locations
? and ?71, respectively, and the current value of e is assigned to r. On the other hand, if 14 has
resided at and 14, has resided at ?, and the guards c and c' have been continuously true for
min(u, n') time units, then either both processes must proceed with the communication, or a third
process must falsify one of c and c'.
Semantics
Synchronous message passing can be modeled formally by timed transition systems. ?`e defIne
the timed transition system Sp = (V, ?, 0, T, I, n? 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 
(from ,? to k?) and ` (from ft? to ?) in the timed transition diagrams for 14 and 14, are labeled
by the matching instructions c a!e and c' a?x, respectively. Then
T contains, for the matching edges  and E', a transition TF?L:1 such that a' E 7?,?i(a) iff
= ft and a'(r?) =
a(r?i) = j?!1 and a'(ir?,) =
c and e' are true in a and a'(x) =
= a(y) for all y ? V --H fr?, TI,
o+ If the matching edges  and ` are labeled by the minimal delays I and 1', respectively, let
1TEEl = max(i, 1').
o+ If the matching edges  and E' are labeled by the maximal delays n and n', respectively, let
UTE,EI = min(u, 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.
15
Process syncbronization
Recall that the component processes of the multiprocessing system pi j?p2 may start at arbitrary,
even vastly different, times. An irnportant application of synchronous message passing is the syn-
chronization of parallel processes. Let pi and P2 be two real-time processes whose timed transition
diagrams have the entry locations 0? and o2, respectively, and let a be a channel. Now consider
the two processes pi and p2 whose timed transition diagrams are obtained from the transition
diagrams for pi and pi by adding new entry locations:
The added message-passing operations have the effect of synchronizing the start of the two processes
pi and pi (whenever message passing is used for the purpose of process synchronization only, the
data that is passed between processes is immatenal and the data coniponents 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 lispi for the system p whose component processes pi and pi start
sync?ronously; that is, the notation ?1ij8pi is an abbreviation for the message-passing system
Pil?pi. Equivalently, we can directly defIne the formal semantics Sp of the synchronoiis multipro-
cessing system p1il5pi as containing a single entry transition Tot?2 for both processes pi and pi;
namely, a' ? m1,2(a) iff
a(ri) = a(ir2) = I,
= oi and a'(ir2) = o2,
= a(y) for all ? c V --H ??i, ir21.
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 Concrete Model: Multiprogramming Systems
While the interleaving model for concurrency identifIes true parallelism (multiprocessing) with
nondeterminism (multiprogramming), the discussion of the traffic I?kt example in the previous
section showed that the ability of a system to meet its real-time constraints depends crucially botli
on the number of processors that are available and on the process allocation algorithm. This is
vividly demonstrated by the following trivial system consisting of the two processes Ft and pi:
16
If both processes are executed in parallel on two processors, we denote the resulting system by
pi 1P2 (or Pi11sP2, 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 will be denoted by pillip2.
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
(ol,o2) Pi (ii,o2) ?P2 (il,2i) --H
(oi,o2) ?f?? (oi,2i) A (?ii,i2) --H
(a state is an interpretation of the two control variables r? and it2). 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 Pi li8P2 we obtain as initialized computations the tinied state se-
quences that result from closing the two sequences
(1,1,0) --H (oi,o2,0) --H (o1,o2, 1) ?1 (ii,o2,1) ??2 (t,21,J) --H (iI,2i.2) --H
(I,I,0) --H (0i,02,0) --H (0i,02,-l) P? (i 2i,1) Ri (i',2i'1) --H (t.,i2,2) --H
under stuttering and shifting the origin of time (the third component of every triple denotes
the time). Note that the system Pi IP2 has more initialized computations. because the time
difference between the start of Pi and the start of P2 can be arbitrarily large.
2. In the time-sharing case P1lilP2, the set of initiallzed computations will be defined to be
essentially the closure ofthe twosequences
(1,0) --H (0i,02,0) --H (0i,02,i) Pi (i1'o2'1) --H (1i?o2,2) ?2 (i',i2,2) --H
(1,0) --H (0i,02,0) --H (oi,o2,l) P2 (ol,i2,1) --H (M 2 2) ?1 (i1,2i'2) --H
under stuttering and shifting the origin of time. ?Ve write `?ssentially,' 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 ofprocesses is
instantaneousandthat neither processhas priorityovertheother process. Alloftheseissues
will be discussed in detail.
Thus, when measuring time, we can no longer ignore the difference between muitiprocessing 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 niultiprogramming systems,
in which several processes share a pool of processors statically or dynamically.
17
4.1 Syntax and semantics
A multiprogramming system P has the torm
(oY[P1111 . . . I?Pmi.
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. ?Ve represent
the real-time programs Pi by timed transition diagrams as before. Note, however, that in the
multiprogramming case the controi of the (single) processor resides at one particular location of
one particular process. Thus the intended operational meaning of the edge
is as follows. The minimal delay 1 guarantees that whenever the control (of the single processor)
has resided at the location ? for at least I time units and the guard c is true, then the control may
proceed to the location k? The maximal delay u ensures that whenever the control has resided
at for u time units and the guard c is true, then it must proceed to tA,. This is because, in the
single-processor case, no other process can interfere with the active process and change the value
of
The operational view of the concrete model is again captured forniafly by a translation into timed
transition systems. With the given multiprogramming system P, we associate tile following timed
transition system Sp = (V, Z, 0-, T, I, `u):
1.
v = uu??, ..... rm1 There are two kinds of control variables: the processor control variable
ij ranges over the set .1.... ni, I?; each process control variable 7r?, for 1 < i < m, ranges over
the set Lj of locations of the process !`?. The value of the processor control variable jt is I
(undefIned) before the (single) processor starts executing processes. Thereafter the control of
the processor resides at the location :r? of the process P,,. NVe say that P1? is active, white all
other processes Pj, for i ? ?, 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 Pi gains control of the processor.
2. ? contains all interpretations of V.
3. 0- is the set of all states a ? "`? such that 0 is true in a, and a(?) = I, and a(ri) = % for all
1 < i < rn.
4. T contains, in addition to the idle transition Tj, an action transition TE for every edge 
in the timed transition diagrams for P1,... Pm. If  connects the source location to the
target location ?k? and is labeled by the instruction c := e, then a' E r?(a) ill'
= and a'(r?) = tk,
c is true in a and a'(?) = a(effl),
= a(y) for all y E V --H (ir?, x?.
Furthermore, there are scheduling transitions T ? T that change the status of the processes
by resuming a suspended process: a' ? r(a) implies that
= a(y) for all y E U.
The scheduling policy determines the set of scheduling transitions. A scheduling transition
7 is called an entry transition iff it is enabled on some initial states. ?Ve restrict ourselves
to scheduling policies with a single entry transition, ?o, that is enabled on all initial states.
Moreover, we require that a' ? 7o(a) implies that
= I,
= a(y) for all y ? V --H
that is, the entry transition ?o is enabled precisely on the initial states and activates, perhaps
nondeterministically, one of the competing processes.
5. For every edge E labeled by the n?nimal delay I, let 1TE = 1. Furthermore, 1To = 0.
6. For every edge  labeled by the maximal delay u,let 117E = ? 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 assuluptions about the scheduling
policy: correctness of an untimed multiprogramming system is generally shown for all fair schedul-
ing strategies. It makes, however, little sense to desire that a multiprogramming system satisiies a
real-time requirement under all (fair) scheduling strategies, because it is the scheduling aigorithm
which usually determines if a system meets its timing constraints. Indeed, fair scheduling strate-
gies admit thrashing: by switching control too often between processes, only scheduling transitions
might be performed; thus the system might not make make any real progress and will certainly not
meet nontrivial real-time deadlines. Consequently, we study the correctness of real-time multipro-
gramming systems always with respect to a particular given scheduling policy.
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 modd.
Throughout this subsection, we assume a fixed multiprogramming system
-P. tOf[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 grc'edy. According
to this policy, the process that is currently in control of the processor remains active untli all its
transitions are disabled. At this point an arbitrary other process with an enabted transition takes
over. Formally, the set T of transitions of Sp contains, in addition to the entry transition m, a
single scheduling transition, 7G, with a' ? 7c(a) iff
= a(y) for all y E V --H
7E(a) = ? for all action transitions 7E,
7?(a') $ ? for some action transition 7E
19
If there is no cost associated with swapping processes, then 1?G flTG = 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 resunie(s), where 5 C ......
determines a subset of processes. The scheduling operation resunie(s) suspends the currently active
process, say, i?? and activates, nondeterministically, one of the processes Pj with j ?
We write resume(j) for resume([j?) and suspend for resume(?1 ? j < m. 1 # i?); 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 P1,... Pm. If  connects
the source location ft to the target location tk' and is labeled by the instruction c resume(s),
then a' E r?(a) iff
= i and a'(?) E 5,
0'(7ri) = 4 and a'(7r?) =
c is true in a,
= a(y) for all y' E V --H f[?, 7riJ.
Furthermore, for every scheduling edge  iab4ed by the minimal delay I and the maximal delay u,
let 1TE = I and ?TE =
Delays and timers
Note that the instruction
models a busy wait; the process Pi occupies the processor for 0 time units while waiting. To
implement a nonbusy wait, in which Pj releases the processor to a competing process for 10 time
units before resuming execution, we use a timer (alarm clock) process P[Tio?io] as a parallel process:
resume(i) [10,I0]? [0,0] t?
P?%,10j: ?
t := false
We make sure that the timer process P1Tio?io1 is started (i.e., waiting for activation) when the process
Pi becomes active. Then the timer is activated by the sequence
20
In general, a timer process PTt,ui marks nondeterministically a tii?e period between I and u time
units and is executed in parael to the other processes of a system:
fo1[(P1I?I . . IIIPm)IIsP?fu1i
The activation of the timer process PFt,u] is abbreviated by the dc-lay instruction
which delays the current? active process Pi for at least I and at most u time units and activates
a process from the set 5. The delay instruction allows us to program nonbusy delays without
explicitly mentioning timers; we simply assume that there exists, implicitly, a unique timer process
for every process in a timed transition diagram (even though the result is `veil-defined, it should be
avoided that a delayed process is reactivated before the corresponding timer expires).
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 (P111IP2)118P5,
the scheduler process
??5U?p?(2) yM1 ?`[1o? 10] resunie(1)
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 scheduler
processes as well.
4.3 Processor allocation
Both the multiprogramming system with a timer process and the mukiprogramming system with
a central scheduler process are, in fact, combinations of multiprocessing and multiprogramming
systems in which several tasks compete for some of the processors. In these systems, the question of
scheduling, which determines the processor time that is granted to individual processes, is preceded
by the question of processor alTheation, 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 tits into our framework
and can be modeled by timed transition systems. A static (shared-variables or message-passing)
system P with k processors is of the form
foY[(P1,1111 . . . tIJPi,?ni)II . . . II(PklIII . . I?I
21
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 Jtj, 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 r?, for 1 <i < k.
To model systems in which a process competes for more than one processor, we simply 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,r), which interrupts the process that is currently active
on processor x and activates, on processor .r, one of the processes from the set 5.
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 transitions that have the highest priority among all enabled transitions
belong to suspended processes, then the currently active process is interrupted and the execution
of one of the suspended processes is resumed.
A priority system P is a (shared?vanables or message-passing, static or dynamic) system in wMch
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:
ffi
We formalize the priority semantics only for simple multiprogramniing systems; the generalization
to systems with several processors is straightforward. N\rith a given priority system
P :			Iii . . 111Pm],
we associate the following timed transition system Sp (V, ?, 0, ?, 1, u):
o+ V, ?, and 0- are as before.
o+ 1 contains, in addition to ??, an action transition TE for every assigninent edge  in the
transition diagrams for Pi,...Pm. If  connects the source location 4 to the target location
k? and is labeled by the instruction p: c := eD, then a E a' iff
= 4 and a'(?) =
c is true in a and a'(r) =
= a(y) for all y E V --H (jt, irj,
Then a' E r?(a) iff
22
a HE a' and a(?) = a'(jt) = ? and
there is no edge ` that is tabeled by a higher priority p' < p such that a ?E' a"
for some a".
For any matching pair of communication edges  and ` that are labeled by the priorities p
and p', respectively, we take the higher priority ?in(p, p';) for the combined transition TE?E?
(although this choice is arbitrary and may be reversed, if the need arises).
Furthermore, there is, in addition to the entry transition ?, a scheduling transition Tp such
that a' E rp(a) iff
# I,
= a(y) for all y E V --H
= ? for all action transitions TE,
? for some action transition TE.
o+ Let 1?? and UTE be as before, and choose 1Tp and ?Tp to represent the cost of swapping
processes.
Note that if all transitions have equal priority, then the sd?eduling strategy is greedy (that is,
TG = TP). 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 wQv. It is, however,
often more convenient to model dynamic sciieduling strategies, which change over time, by dunamic
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. N:Ioreover, they
are easily incorporated into our framework. We simply use as priorities data variables that range
over the nonnegative integers. 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.
?Ve have not yet pointed out that our interpretation of message passing is not entirely conservative
over the untimed case: there the set of legal execution sequences usually is restricted by strong-
fairness assumptions for communication transitions ([?IP92]). This is convenient for the study
of time-independent properties of a system, where simple fairness assumptions about ??nondeter-
ministic" branching points abstract complex implementation details. Consider, for example, the
multiprocessing system ?1IIP2IIQ that consists of the following three processes P1, P2, and Q:
a! [10, 10] [0, 0] a?			?3! [10, 10] [0,0] ??
P1:			P2: AMA
23
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 J 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 IN and P2 is shut out from its critical section
forever: the arbiter cannot ahvays 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
infirntary 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:
p: a!
q: p!
(We use semicolons to concatenate instructions; the default value of priorities is assumed to be 0.)
The arbiter Qt modifies the priorities p and q of its nondeterministic alternatives to ensure that
the system
= q = 0Y[PiIIi?IIQ']
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 nondetern?nistic 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
synclironization, 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
24
competitor of a transition 7 can be taken more than n times without T itself being taken (a
similar concept has been called bounded fairness in [Jay88]). 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.
Part II
Verifying Real-time Systems
We define a formal language that is interpreted over timed state sequences. This language is used
to specify timed transition systems: a timed transition system 5 meets the specification ? iff ali
computations of 5 satisfy ?. We present two proof methodologies bounded-operator reasoning
and explicit-clock reasoning for verifying that a timed transition system meets its specification.
Relative-completeness results are given for both proof techniques.
5 Specification Language
As a specification language, we use an extension of linear temporal logic with time-bounded tempo-
ral operators. We distinguish between state formulas, which assert properties of individual states
of a computation, and temporal formulas, which assert properties of entire computations.
5.1 State formulas
Let 5 = (V, ?, 0, I, I, u? be a timed transition system. Typically 5 is associated with a concrete
real-time system that belongs to one of the classes we discussed in Part I. Throughout this part,
we use the foliowing additional assumptions about the set V of variables:
We assume that, in addition to data and control variables, V contains sufficiently many
auxiliary variables that range over the integers and are not changed by any of the transitions
of 5. We will on occasion need a "new, rigid" variable, and for this purpose we employ one
of the auxiliary variables that have not been used previously.
o+ We assume that, for every variable x ? V, there is a corresponding unique primed variable
V that ranges over the same domain as x.
We are given an assertion language ---H a first-order language with equality that contains interpreted
function and predicate symbols to express operations and relations on the domains of the variables
in V. A state formula (assertion) is a first-order formula p of the assertion language such that only
variables from V occur freely in p. Thus, every state in ?? provides an interpretation for the state
formulas. If the state formula p is true in state a, we say that a is a p-state.
We use the foliowing abbreviations for state formulas:
o+ For any transition 7 e T, the enabling condition enabThd(r) asserts that ? is enabled. In
particular, enabThd(?1) is equivalent to true for the idle transition TI.
o+ For any transition 7 E 1 and state formulas p and q, the verification condition ?p? 7
asserts that if p is true of a state a ? ?, then q is true of all 7-successors of a. In particular,
25
fpY ?I ?q? stands for the universat closure of the formula p q. For any set T' c ? of
transitions, we write ?py T' ?qJ for the conjunction
A fp???q?
rET'
of all individual verification conditions.
For any transition r E I and state formulas p and q, the 2flverse verification condition
fpj 7 ?q? asserts that if p is true of a state a E ?, then q is true of all r-predecessors
of a. Observe that all inverse verification conditions are definable by ordinary verification
conditions:
fpj T fq? is equivalent to ??q? 7
In particular, ?PY ?F ?q? is equivalent to ?p? 71 ?q? for the idle transition 7J. For any set
I' c I of transitions, we write fp? I'--H fqj for the conjunction of the inverse verification
conditions for all transitions in I'.
Note that while the truth value of an enabling condition depends on the state in which it is inter-
preted, the verification conditions are state-independent and, thus, equivalent to closed formulas.
In the case that the timed transition system 5 is associated with a shared-variables multiprocessing
system P, it is not hard to see that the enabling and verification conditions of all transitions can
indeed be expressed by state formulas. Suppose that P consists of the m' processes Pj, for I < i < m,
and the data precondition 0, which is a state fonnula:
fOY[PiI?...IIPm]
Let us assume that each process Pj, for 1 < i < m is given by a timed transition diagram with
the locations f0t?????tj? and the entry location %. ?Te wnte atiffl for Tj = 1, and atJ? for
7r? = ft; that is, the control of the process Pj is at tbe location ?. ?Ve abbreviate any disjunction
at?ft V at?tk further, to
1. For each entry transition % E I of Sp, the enabling condition enabThd(r0?) is equivalent to
the state formula
atj?j,
and the verification condition t?1 7o? ?q? is equivalent to the universal closure of the formula
(p A enabIed(m?) A (atJ0?? A			A (i" = ?J))
where the formula q' is obtained from q by replacing every variable with its primed version;
for example, (at?0?)' stands for r?' = 0?. The inverse verification condition ??i (70i)? fqj is
equivalent to the universal closure of the formula
(pt A enabThd(?0?) A (atJ0?Y A A (j?' =
YEV?4'Ti?
2. All other nonidle transitions of Sp correspond to edges in the timed transition diagrams for
the processes Pj. Let rj?k ? I be such a transition and assume that the corresponding edge
26
that connects the location ft to the location ? is labeled by the instruction c x
Then, the enabling condition CflabiCd(Tj??) is equivatent to the state formula
atj,t A c,
and the verification condition (Pi Tj?k (qJ is equivalent to the universal closure of the formula
(p A enabied(%??) A (atJ??Y A (x' = e) A			A			(v' = v))
The inverse verification condition (?y (rj?k) (qJ is equivalent to the universal closure of the
formula
(p' A CflabICd(Tj??) A (atJ??.Y A (x' = e?) A			A			(y' = v))
yEV--H4
It is also straightforward to express the enabling and verification conditions as state formulas if the
timed transition system 5 is associated with any of the other concrete real-time systems that we
discussed in Part I, such as message-passing, multiprogramming, dynamic, and priority systems.
Synchronous multiprocessing systems
Our examples will be drawn from timed transition systems 5 that are associated with multipro-
cessing systems P of the form
(O?[P? Is . . . 115Pm],
all of whose component processes start synchronously (i.e., at the exact same time). The cor-
responding timed transition system has a single entry transition that sets all control variables,
simultaneously, to the entry locations of the individual processes. I?r muhiprocessing Qystems P,
it is convenient to define the following two additional abbreviations for state formulas:
o+ The ready condition ready holds precisely in the initial states () of Sp; it indicates that none
of the processes of P has started yet. Consequent?, ready stands for the state formula
0 A ( A atjtj).
o+ The synchronous starting condition start indicates that all processes of P have entered their
entry locations, but none has proceeded any further; that is, start abbreviates the state
formula
0 A ( A ati0? ).
1<i<m
Note that if p is synchronous, then the two verification conditions
(readyj T--H7? (starti,
(starti (`T--H71) fready?
are valid (by T--Hr we denote the set difference T--H(TJ).
27
5.2 Temporal formulas
Temporal formulas are constructed from state formulas by boolean connectives and time-bounded
temporal operators. They are interpreted over timed state sequences. In this paper, we are in-
terested in proving two important classes of real-time properties bounded-invariance properties
and bounded-response properties. Thus we restrict ourselves to the following temporal formulas:
o+ Every state formula p is a temporal formula; it is true over the tiiiied state sequence p = (a, T)
iff the initial state a0 is a p-state.
o+ Every boolean combination of temporal formulas is a temporal formula, whose truth over a
timed state sequence is determined from the truth of its components in the standard way.
Bounded-unless formulas: If p is a state formula, 6 a temporal formula, and I E N, then
p U>i 6 is a temporal formula; it is true over the timed state sequence p = (a, T) iff either
all a?, for `i > 0 are p-states, or there is some position i > 0 sucb that Tj > T0+1, and 6 is true
over the i-th suffix p? of p, and all a5, for 0 < j < i, are p-states. We use the abbreviations
p U 6 and ?<1 p for the formulas p U>o 6 and p U>t trne, respectively.
Bounded-eventually formulas: If 6 is a temporal formula and ? ? N, then ?<u 6 is a temporal
formula; it is true over the timed state sequence p = (a, T) iff there is some position i > 0
such that Tj < T0 + u and 6 is true over the i-th suffix p? of p.
Temporal-logic aficionados will readily recognize the operators ?<j, _ , and U>1 as time-bounded
versions of the standard (untimed) aLways, eventually, and strict `unicss operators. In particular,
the bounded-unless formula p U>o q is true over a timed state seqtience p = (a, T) iff the untimed
(strict) unless formula p U q is true over the state component a of p:
either all a?, for i > 0, are p-states,
or there is some position i > 0 such that q is true over the ?-th suffix a of a and all a5,
for 0 < j < i, are p-states.
For a general addition of time-bounded operators to linear temporal logic, see [AH90]. From now
on, we use the convention that the letters p, q, r as well as ? (and pnmed versions) denote state
formulas, while the letters 6, ?, and ,y stand for temporal formulas.
5-validity and 5-soundness
Let 5 be a timed transition system. A temporal formula 6 is 5- vaI?? iff it is true over all compu-
tations of 5. While (general) validity truth over all timed state sequences implies 5-validity
for the given system 5, the converse does not necessarily hold. In fact, even a state formula p that
is 5-valid may not be true in some states of 5 that do not occur along any run of 5 and, hence, p
may not be generally valid. To show that the given system 5 meets the specification 6, it suffices
to show that 6 is 5-valid.
A proof rule is 5-sound iff the 5-vJidity of all premises implies the 5-validity of the conclusion.
Note that a (generally) sound proof rule whose conclusion is valid if all premises are valid
might not be 5-sound for the given system 5, and vice versa. For verifying properties of a timed
transition system 5, we are interested in 5-sound rules.
Bounded invariance and bounded response
Two important classes of timing requirements for real-time systems can be defined by temporal
formutas:
o+ A bounded-invariance property asserts that a condition iio]ds continuously for a certain
amount of time; it is often used to specify that something does not happen for a certain
amount of time. Formally, we express bounded-invariance properties by temporal formulas
of the form
p --H 1Z<Iq,
for state formulas p and q and a nonnegative integer I e N. The formnla P --H ?<t q is 5-valld,
for a timed transition system 5, iff for all (initialized) computations p = (a, T) of 5 and all
i> 0 and j> i,
if ? is a p-state and 7) < Ti + 1,
then ? and a5 are q-states;
that is, every p-state is a q-state and no 13-state is followed by a ?q-state within time less
than I. A typical application of bounded invariance states a lower bound I on the termination
of a multiprocessing system P with the termination condition r: the temporal formula
ready --H
asserts that, if not started before time t, then P will not reach a final state before time t + 1.
o+ A bounded-response property asserts that something happens within a certain amount of time.
Formally, we express bounded-response properties by temporal formulas of the form
13 --H
for state formulas p and q and a nonnegative integer u C N. The formula 13 --H ?<u q is
5-valid, for a timed transition system 5, iff for all (initialized) computations p = (a, T) of 5
and all i > 0
if a? is a 13-state,
then there is some q-state a,, with j > i, such that 7? ? Tj + I
that is, every 13-state is followed by a q-state within time n. A typicai appllcation of bounded
response states an upper bound u on the termination of a multiprocessing system P with the
termination condition r: the temporal formula
start --H			r
asserts that if all component processes of P are started synclironously at time t, then P is
guaranteed to reach a final state no later than at time t + n.
As the computations of timed transition systems are closed under shifting the origin of time,
we shall, without loss of generality, henceforth assume that the starting time t of a synchronous
multiprocessing system is 0.
29
Monotonicity rules
We flow introduce two important proof rules that are 5-sound for every timed transition system 5.
The monotonicity rule U-MON allows tis to weaken any of the three arguments of the bounded-
unless operator:
U-MON pp'?--H9"ii?I
--H (p'U>vo"')
A second monotonidty rule, ?-MON, weakens either argument of the bounded-eventually operator:
?-MON			?--H?u1>v
w
It is not hard to see that both monotonidty rules are 5-sound for every timed transition system 5.
Since propositional reasoning, too, is 5-sound for every system 5, we will refer to applications of
the two weakening rules and propositional reasoning in derivations through the simple annotation
"by monotonicity." For example, from the hounded-unless formula
p --H
we can establish, by monotonicity, both the bounded-invariance formula
--H E<1q
and the (unbounded) unless formula
1) --H q U r.
6 Bounded-operator Reasoning
Let 5 = (V, ?, 0-, I, I, u? be a timed transition system. We present a deductive system for estab-
lishing the 5-validity of bounded-invariance and bounded-response properties. The proof rules fall
into four categories:
1. The single-step rules derive real-time properties that follow froni the lower-bound or upper-
bound requirement for a single transition.
2.
The tiansitivity rules combine two real-time properties of the same type that is, either
two bounded-invariance properties or two bounded-response properties --H- into a composite
timing property.
3. The induction rules combine arbitrarily many real-time properties of the same type into a
composite timing property.
4. The crossover rules combine two real-time properties of opposite types into a composite
timing property.
30
?Ve begin by presenting this "bounded-operator" methodology for the restricted case of determin-
istic systems that can be verified without crossover reasoning: the tiined transition system 5 is
deterministie iff it is associated with a multiprocessing system P and any two guards on outgoing
edges of the same vertex in the tiined transition diagram representation of P are disjoint. It follows
that for deterministic systems, on each state the idle transition and at most one nonidle transition
per process are enabled. Nondeterministic systems require more complex (conditional) single-step
reasoning, which is treated in the subsequent subsection. The need for crossover reasoning arises
in connection wfth the completeness argument of Section 8 and wiH be discussed there.
6.1 Deterministic rules
In a first attempt at proving time-constrained response formulas, we decorate the proof rules for
establishing unconstrained response formulas ([NIP84j) with time bounds. Furthermore, for each
of these upper-bound rules for deriving bounded-response properties, there is corresponding lower-
bound rule for deriving bounded-invariance properties. In keeping with our standard order, we wm
introduce each lower-bound rule before the corresponding upper-bound rule.
Single-step rules
The sin?Th-step Thwer-bound rule uses the minimal delay 1T E N of a transition T ? I to infer a
bounded-unless formula:
U-SS
p ??enabled(r)
fy?? I-r (?J
(y A enabled(r))			r
p qU>t?r
The rule U-SS derives a temporal (bounded-unless) formula from premises all of which are state
formutas, whose 5-validity typically is shown by proving them generally valid. The state formula y
is called the invariant of the rule. Choosing r to be true, the rule infers a bounded-invariance
property,
p
(note that the last premise holds trivialiy in this case). ?b see why the rule U-SS is 5-sound,
observe that whenever the transition 7 is not enabled, it cannot be taken for at least i time units.
During this time, the invariant y is true.
The single-step upper-bound rule uses the maximal delay ?r ? N of a transition 7 c I to infer a
bounded-response formula:
?-SS p			(? V q)
enabfrd(r)
(??I--Hr(? V q?
?`,,)?fqJ
p ?<? q
31
This rule derives a temporal bounded-response formula from premises all of which are state for-
mulas. The state formula ? is again called the invanant of the rule. To see why the rule ?-SS is
5-sound, recall that the transition r has to be taken before it would be continuously enabled for
more than ur time units.
To demonstrate a typical applicatioii of the single-step rules, we consider the single-process system
P with the data precondition r = 0 and the following timed transition diagram:
=			x = 0?
The process P confirms that x = 0 and proceeds to the location i. Because of the delay interval
[2,3] of the transition T0?1, the final location ?i cannot be reached before time 2 and must be
reaclied by time 3 (recall that P is taken to start at time 0). Using single-step reasoning, we
can carry out a formal proof of this analysis. The bounded-invariance property that P does not
terminate before time 2,
ready			?<2?ati1,
is established by an application of the single-step lower-bound rule U-SS with respect to the tran-
sition 7b?i (let the invariant y be atij,o). The bounded-response property that P terminates by
time 3,
start			?<3ati1,
follows from the single-step upper-bound rule ?-SS with respect to the transition T0?1 (use the
invariant ati0 A x = 0).
Transitivity rules
To combine a finite nuntlier of successive timing constraints into a more complicated real-time
property, we introduce transitivity rules. `The transitive Thwer-bound rnie combines two bounded-
unless formulas:
U-TRANS ?			pU>11 ,y
qU>?24i,
(p v q) U>11+? ?
We refer to the formula ? as the link of the rule. The transitive nppcr-bound rule combines two
bounded-response formulas:
?-TRANS ?			?<u1 N?
?<u1+ti2 `?`
The formula )Q is again called the link of the rule. Both transitivity rules are easily seen to be
5-sound for every timed transition system 5.
We demonstrate the application of the transitivity rules by examining the single-process system P
with the following timed transition diagram:
32
?Ve want to show that P terminates not before time 4 and not after time 6. First, we prove the
lower bound on the termination of P:
ready			[JJ<4?ati2.
By the transitive lower-bound rule U-TRANs, it suffices to show the two premises
ready (?ati2)U>2ati0,
ati0			(?ati2)U>2tr'ue.
(1)
(2;)
Both premises can be established by single-step lower-bound reaso'iing. To show the premise (1),
we apply the rule U-SS with respect to the transition T0?1, using the invanant at-ij,0; the premise
(2) follows from the rule U-SS with respect to the transition r1?2 and the invariant ati0,1.
The upper bound on the termination of P,
start			?<6ati2,
is concluded by the transitive upper-bound rule ?-TRANS. It suffices to show the premises
start			?<?(ati1 A x			0).
(atii A x = 0)			?<3 at?t2
both of which can be established by single-step upper-bound reasoning (we use the two invariants
ati0 A r = 0 and ati? A x = 0, respectively). Note that for lower-bound reasoning the hal: ati0
identifies the last state before the transition r0?1 is taken, while for upper-bound reasoning the
link ati1 A r = 0 refers to the first state after Th?i is taken.
For an example with a (deterministic) branching structure, consider the process PI with the fol-
lowing timed transition diagram:
x ? 0?			2
We show that P' terminates either at time 3 or at time 4. The proof requires a case analysis on
the initial value of x, whid? determines which path of the transition diagram is taken. The lower
bound
ready			E<3?ati3
is implied by the two bounded-invariance formulas
(ready A x = 0)			?<3 ?ati3,
33
(ready A r ? 0)			?<? ?at%3,
both of which can be derived by transitive lower-bound reasoning (as links use the two state formulas
atij,0 A x = 0 and atij,0 A x ? 0, respectivety). The upper bound
start --H ?<4 ati3
follows by a similar case analysis and transitive upper-bound reasoning.
So far we have examined only single-process examples. In general, several processes that commu-
nicate through shared variables interfere with each other. Consider the synchronous two-process
shared-variables multiprocessing system with the data precondition x = 1 and the following timed
transition diagrams:
P1:			ol			x=O?			(1
P2:			o2			x := 0			2
The fIrst process, P1, is identical to a previous example; with a minimal delay of 2 time units and
a maximal delay of 3 time units, it confirms that x = 0 and proceeds to the location ?. However,
this time the value of x is not 0 from the very beginning, but set to 0 by the second process, P2,
only at time 1. Thus, P1 can reach its final location li no earlier than at time 3 and no later than
at time 4.
For a formal proof we need the transitivity rules. The bounded-invariance property
ready			?<3?atit
is established by an application of the transitive lower-bound rule U-TRANs. It suffices to show
the premises
ready			(?ati11) U>i (ati11,0 A x = 1),
(ati11,0 A x = 1)			(?atiJ) U>2 true,
both of which follow from single-step lower-bound reasoning. Similarly, the transitive upper-bound
rule ?-TRANS is used to show the bounded-response property
from the link ati01 A r = 0.
Induction rules
start --H ?<? ati11
To prove lower and upper bounds on the execution time of program ]oops, we need to combine a
state-dependent number of bounded-invariance or bounded-response properties. For this purpose
it is economical to have induction schemes.
The induetive Thwer-bound rule U-IND generalizes the transitive lower-bound rule U-TRANS;
it combines a potentially large number of similar bounded-unless formulas in a single proof step.
Assume that the new, rigid variable i ? V ranges over the integers Z; for every positive integer n > 0:
34
U-IND (y(?)A`i>0)pU>ty(?--H1
_________________ pU>n.t?(O)
By y(? --H 1;) we denote the state formula that results from the inductive invariant y(?) by replacing
all occurrences of the variable i with the expression ? --H 1; the formulas y(n) and ?(O) are obtained
analogously. Note that every instance of the rule U-IND, for any constant n > 0, is derivable from
the transitive lower-bound rule U-TRANS.
For a demonstration of inductive lower-bound reasoning, we consider tile following single-process
system P:
x := x --H 1 [2,3]			x ? 0?
= 51
-yX[0)0)?2
The process P decrements the value of x until it is 0, at which point F proceeds to the location 2'
Since r starts out with the value 5 and each decrement operation takes at least 2 time units, while
the tests are instantaneous, the ?nal location 2 cannot be reached before time 10. This lower
bound,
ready			rl<io?at?2,
follows by transitivity and monotonicity from the two bounded-unless formulas
ready			(?ati2) U>2 (atii A x = 5),			(1)
(atii A x = 5) --H (?ati2)U>8(ati1 A x = 1).			(2)
The fIrst property, (1), is enforced by two single-step lower bounds; the second property, (2), can
be derived by the inductive lower-bound rule U-IND from the premise
(atii A x=i+l A i>O) (?ati2)U>2(ati1 A x=i),
which is concluded by transitive reasoning.
The inductive lower-bound rule has a twin that combines several similar bounded-response formulas
by adding up their upper bounds n. In fact, both induction rules can be generalized, by letting
the bounds I and v vary as functions of i. In its more general form, we state only the induetive
upper-bound rule. It uses again a new, rigid variable i e V that ranges over the integers Z; for
every nonnegative integer n > 0:
?-IND (?(i)Ai>0)--H?<?,
Every instance of this rule, for any constant n > 0 is derivable from the transitive upper-bound
rule ?-TRANS.
The general form of the inductive upper-bound rule is usefut to prove upper bounds for programs
with loops whose execution time is not uniform. An example for such a system is the following
odd-even variant of the process P:
35
odd(x) --H+ x:=x--Ht [2,2]			[0,0] r#o? [2,3] even(x)			r:=x--Hi
The upper bound
start			?<i2ati2
follows by transitivity from the bounded-response property
start --H ?<12(ati0 A x = 0),
which can be concluded by the inductive upper-bound rule ?-IND fron? the premise
(at?o A x = i A i > 0)			?<2+even(?) (at?('0 A r = --H 1)
(the expression even(i) evaluates to either 1 or 0 depending on whether the vahie of `i is even). This
bounded-response formula follows from transitive reasoning.
6.2 Conditional rules
Unfortunately, the proof rules we have designed are not strong enough to show tight bounds on
nondeterniinistic systems. To see this, consider the following nondeterministic variant P of a
process encountered previously:
true?			true?
2
As before, P terminates either at time 3 or at time 4. However, during an execution of P, one of
the two transitions T0?1 and ?o?2 is chosen nondetermimstically. Thus we cannot carry out a case
analysis with respect to a state formula that selects a unique guard. Instead, we proceed in two
steps. First we establish an untimed safety formula that enumerates all possible nondeterministic
choices. Then we decorate the unbounded temporal formula with time bounds.
Step 1 To establish the S-validity of a temporal formula ? that contains only unbounded unless
operators (i.e., U>o), it suffices to show that ? is true over all run fragments of the untimed
transition system S that underlies 5. This can be achieved with the help of any conventional
timeless proof system (for instance, the proof system given in [NIPS3]).
For example, to derive the lower bound 3 on the termination of our example P, we show the untimed
formula
ready			((atii U ati0 U ati?) V (atJ1 U at?& U ati2))
(nested unless operators associate to the nght).
Step 2 To add time bounds to this disjunction of nested unless formulas, we need conditional
single-step rules. They establish single-step real-tiiue bounds under the assumption that
a particular disjunct has been chosen. The time bounds can, then, be combined by the
transitivity rules.
36
Nondeterministic lower bounds
The conditional single-step Thwer-bound rule uses the minimal delay 1T ? N of a transition ? ?
u-css			p			??enabThd(r)
(pU>tqu(rA?)			(pU>iqU>i?(r A ?)
The rule U-CSS is 5-sound for any temporal formula ?. The second premise ensures that only the
transition T can establish r A ?, but to do so, it must be enabled for at least 1T time units, during
which q is true.
In our example, we use the conditional single-step lower-bound rule U-CSS with respect to the
transitions r0?1 and ?o--H2 to derive the conditional single-step bounds
(atJj U atJ0 U atJ1) (atJ1 U atJ0 U>2 atji),
(atjj U atJ0 U atJ2) (atJ1 U atj0 U>1 ati2).
They allow us to conclude, from (t)?
ready ((atij U atft0 U>2 atii) v (atij U at?0 U>? ati2)).
To collapse nested bounded-unless operators, we use the temporal formula U-COLL:
U-COLL (p U>j1 q U>12 y) ((p V q) U>11+12 Q,')
Note that this temporal formula, which is genera?y valid, can be derived by from the transitive
lower-bound rule U?TRANS by using the two tautologies
(p U>t1 q U>12 y)			(p U>i1 q U>j2 o,?),
(qU>t2?)			(qU>t2?).
From (++) we obtain by collapsing and monotonicity
ready ((atij? U>2 atii) v (atij? U>i at?&2));
that is, using the (untimed) validity p U true and monotonicity,
ready			((atij?0 U>2 ati1 U true) v (atij?0 U>1 ati2 U true),).
Adding conditional single-step lower bounds for the transitions T1??3 and r2?3 gives
ready			((atij0 U>2 ati1 U>i true) v (atijj? U>i ati2 U>2 true)),
and by collapsing and monotonicity we finally arrive at the desired bounded-invariance property
ready			E<3?ati3.
37
Nondeterministic upper bounds
Conditional upper-bound reasoning does not require the nesting of unless operators. The condi-
tional single-step upper-bound rule uses the maximal delay u7 E N of a transition 7 ?
?-CSS p			enabled(r)
Clearly, the rule ?-CSS is S-sound for any temporal formula 9. Note that the second premise of
this rule is trivially valid if 7 becomes disabled by being taken, as is the case for all transitions of a
timed transition system that is given by timed transition diagrams (recall that we have ruled out
self-loops in transition diagrams). It is also worth pointing out that both conditional lower-bound
and conditional upper-bound reasoning rely only on assumptions that are built only from state
formulas by positive boolean connectives and unbounded unless operators and, therefore, define
untimed safety properties. Accordingly, the first step of conditional reasoning can be carried out
by any untimed method for deriving safety properties.
To derive the upper bound 4 on the termination of our example ?, we show first the untimed
formula
start --H ((at?o U at?1) v (at??0 U at?t2)).
By the conditional single-step upper-bound rule ?-CSS with respect to the transitions To?i and
Th?2, we derive the conditional single-step bounds
(atJo U atJ1)			?<2 atJ1
(atJo U atJ2) --H ?<2 atJ2
They allow us to conclude
start --H (?<2 atJ1 V ?<2 at?C'2).
Now we can proceed by unconditional upper-bound reasoning to arrive at the desired bounded-
response property
start --H ?<4atJ3.
7 Explicit-clock Reasoning
None of our state formulas is able to refer to the value of the time, because the only real-time
references that are admitted in temporal lormulas are time bounds on temporal operators. In this
section, we investigate the consequences of extending the notion of state, by adding a variable now
that represents, in every state, the current time. This extension is interesting, because once we are
given explicit access to the global clock through the clock variable now, both bounded-invariance
and bounded-response properties can alternatively be formulated as unbounded unless formulas
and, consequently, be verified by conventional timeless techniques for establishing safety properties
of transition systems.
38
7.1 Explicit-clock transition systems
Let 5 = (V, ?, 0-, T, 1, n? be a timed transition system. ?Ve introduce the following new variables:
o+ A clock variable now that ranges over the integers; it records, ill every state a? of a compu-
tation p = (a, T), the corresponding time Tj.
o+ For every transition ? ? `T, a deThy counter 6? that ranges over the set ?0, .... . UTY of
nonnegative integers; it records, in every state of a computation, for how many clock ticks
the transition 7 has been continuously enabled without being taken. ?Ve write short
for
The explicit-clock transition system 5 = (V?, ??, 0- `T?? associated with 5 is defined to be the
following untimed transition system:
1 v --H v u fnow? U ?? I 7 ?
2.
contains all interpretations of v?. Thus, every explicit-clock state a ? ?? of 5 is a tuple
that contains a state a ? `2 of 5, a value a(now) ? Z for tile clock variable now, and a value
E N for each delay counter 6T
3. An explicit-clock state a E ? is initial itt it extends an initial state of 5:
a e 0			iff a ? 0-.
4. Every transition of 5 is extended: f* contains, for every 7 ? T, a transition 7 such that
(a1, a2) ? 7* ifffor all 71 E T
(ai?,a??) E 7,
ai(6?) > Ir,
a2(now) = a1(now),
--H			ai(6??)			if 7' # 7 and 7' is enabled on a2?,
--H			0			otberwise.
The second clause, ai(??) > l,r, enforces all lower-bound requirements on computations.
In addition, ?? contains the idle transition ?i and the tick transition 7T' which advances
time: (a1,a2) ? 7T itt for all 7' ?
aT = a2
a2(now) = a1(now) + 1,
a2(6?i) =			0ai(6?') + 1
a2(67,) < ?r'
if 71 ? 7 and 7' is enabled on a2
otherwise,
The last clause enforces all finite upper-bound requirements 011 computations.
From 5 we obtain a fair transition system ([Nt1P92]) by adding the following fairness requirements:
5. A weak-fairness (justice) assumption stipulates that a transition cannot be continuously en-
abled without being taken. Let the weaklyfair extension Si of 5- be the fair transition
system that is obtained from 5 by adding a weak-fairness assumption for every transition 7*
itt 7 has a maximal delay of oc
39
6.
A strong-fairness assumption stipulates that a transition cannot be enabled infinitely often
without being taken. Let the strong1?-friir extension 5! of 5* be the fair transition system
that is obtained from Si by adding a strong-fairness assumption for the tick transition TT.
The weak-fairness requirements enforce all infinite upper-bound requirements on computations.
The strong-fairness requirement for the tick transition ensures the progress of time: from the
operationality restriction of 5 it follows that every initialized computation of 5! contains infinitety
many tick transitions.
If a = a0a1a2 .. is an infinite sequence of explicit-clock states from ??, we write a for the
corresponding sequence aJa?a2?... of states from V It is not hard to see that the timed transition
system 5 and the fair explicit-clock transition system 5? are related in the following way:
For every initialized computation (a, `T) of 5, there is an infinite sequence a* of explicit-clock
states with (a*) = a and a?(now) = T such that a* is an initialized computation of 5!
(in the first state of a*, choose the delay counters of all enabled transitions larger than all
minimat delays of 5; otherwise, let all delay counters record the times that the corresponding
transitions have been enabled).
o+ For every initialized computation a of 5!, the timed state sequence (a--H, a(now)) is an ini-
tialized computation of 5.
7.2 Explicit-clock formulas
We now translate every bounded-in variance and bounded-response formula ? over V into an Un-
timed unless formula ?? that contains the clock variable now. The explicit-clock formuTh ? is
constructed such that it is 5*-valid iff ? is 5-valid:
o+ The explicit-clock translation of the bounded-invariance formula P ?<i q is
(p A now = t) q U (now > t + I),
for a new, rigid variable t E V that ranges over the integers Z (recall that V supplies suitable
variables that occur neither in the description of 5 nor in p or
o+ The explicit-clock translation of the bounded-response formula p ?<u q is
(p A ?q A now = t) (now ? t + u) U q.
for a new, rigid variable t ? V that ranges over
Both unless formulas use the rigid variable t to record the time of the p-state. In the case of bounded-
response properties, the explicit-clock translation exploits the fact that the time is guaranteed to
reach and surpass t + u, for any value of t. We emphasize that neither of the state formulas p and
q may contain free occurrences of the clock variable or any of the delay counters.
From the correspondence between the computations of the timed transition system 5 and the fair
explicit-clock transition system 5! it follows that the explicit-clock formula ? is 5!?valid iff ? is
5-valid. Indeed, since the explicit-clock translations of bounded-invanance and bounded-response
properties are safety formulas, there is no need to add fairness assumptions to the explicit-clock
transition system:
Proposition 2. If 5 is a timed transition system andp is a bounded-invariance or bounded-response
formula, then the explicit-clock translation 0,' is 5*-valid iff ?; is 5-valid.
40
7.3 Untimed temporal reasoning about real time
Proposition 2 leads to an atternative and quite different approach to the verification of reJ-time
properties: to prove the 5-validity of a real-time property ? (over V), we establish instead the
5*-validity of the untimed safety formula Q (over V*). To show the unbounded unless formulas
that result from translating bounded-invariance and bounded-response properties, a singie timeless
unless rule suffices ([MP83]):
UNLESS
(MT?(? V 4
y?q
p			q Li
We point out that all three premises of the unless rule are state formulas over the augmented set
V* of variables; their 5*-validity typically is shown by proving them generally valid. The state
formula y is called the inVariant of the rule, because the main (i.e., second) premise asserts that ?
is preserved by all transitions of the system 5 (unless the desired state condftion r is established).
To demonstrate this kind of "explicit-clock" real-time reasoning, consider again the single-process
system P with the data precondition `r 0 and the following timed transition diagram:
tx =			?			x = 0?
The lower bound on the termination of P,
ready			L]<2?ati1,
is translated into the explicit-clock formula
(ready A now = t) (?ati1) U (now > t + 2),
which can be derived by the unless rule from the invariant
(at?j A now > t) V (at?o A now > t + 6o?i)
(recall that the delay counter ?o?? of the transition To?? ranges over the set (0,1,2, 3? only). The
upper bound on the termination of P'
start			?<3at?1,
is translated into the untimed unless formula
(start A ?atJ1 A now = t) (now < t + 3) U ati1,
which can be concluded by the unless rule from the invariant
ati0 A x = 0 A t < now <t + 3 A now <t + 6o?i
41
8 Completeness
Throughout this section, we consider completeness relative to state reasoning (relative to assertional
validity); that is, we assume to be given an oracle that decides the validity of closed state formulas.
The unless rule is known to be complete relative to state reasoning for establishing unless formulas
of transition systems, provided the underlying assertion language is sufficiently expressive to encode
computations ([MP83]). From Proposition 2 it follows immediately that explicit-clock reasoning is
relative complete for showing bounded-invariance as well as bounded-response properties of timed
transition systems. As for bounded-operator reasoning, we first show relative completeness in the
case that all real-tin? constraints are either lower-bound constraints or upper-bound constraints.
Then we motivate the need for crossover reasoning in the general case and present crossover rules
to combine lower-bound and upper-bound constraints.
8.1 Crossover-free reasoning
Given a timed transition system 5, we assume that all untimed safety properties of 5 can be derived;
that is, we assume an untimed proof system that is complete for untimed safety reasoning. Although
such a proof system cannot exist for most data domains, there are temporal proof systems that are
complete relative to state reasoning ([N1P89]). In addition, we suppose that the nontrivial timing
constraints of 5 are either all minimal delays or all maximal delays. The following theorem shows
that under these assumptions, our bounded-operator rules can derive every bounded-invariance and
bounded-response property of 5.
Theorem. Let 5 = (V, ?, 0-, ?, I, n) be a timed transition system such that either IT = 0 for all
7 Ei ? or u? = oc for all r E T. Let ? be a bounded-invariance or a bounded-response formuTh.
If b is 5-valid, then it can be derived by the monotonicity, transitivity, and conditional single-step
rules relative to untimed safety reasoning.
Proof. (I) Suppose that all maximal delays of 5 are oc. First we observe that, under the given
restrictions, untimed reasoning is complete for untimed properties of 5. This is because, in the
absence of finite maximal delays, there is a time sequence T for every computation a of the untimed
weaHy-fair transition system 57 that underlies 5 such that (a, T) is a computation of 5 (choose
all time steps large enough). It follows that any untimed temporal formula that is 5-valid is also
57 valid and, thus, can be established by untimed reasoning.
Any bounded-response property is either trivially not 5-valid or can be established by untimed
safety reasoning. Now suppose that the bounded-invariance property
p			(1)
is 5-valid; we show that it can be derived within our proof system. The main idea is to see that
in order for (1) to be valid, for any p-state in an initialized computation of 5 there has to be a
sequence of nonoverlapping single-step lower bounds that add up to at least I before a q-state can
be reached. ?Ve show that there are only finitely many such ways in which a q-state can be delayed
for I time units; hence they can be enumerated by a single untimed formula.
Consider an arbitrary computation ,o = (a, T) of 5 such that Q, for i > 0. is a p-state. Let a5 be
the first q-state with j > i; if no such state exists, let j = no. We write 7k for the transition that is
completed at position k > 0 of p. A lower-bound i-constraint pattern for Q..j is a finite sequence
of nonoverlapping single-step lower bounds between i and j that add up to at least I. Formally,
42
a constraint pattern C' is a sequence of transitions Tj1... Tjn' The pattern C is a lower-bound
i-constraint pattern iff
? tTik > 1?
1<k<n
it is a lower-bound constraint pattern for aj..5 iff
(a) i = i0 ? ii < ... ? < j and
(b) for all 1 < k < n the transition Tik is not enabled on some state aj? such that
?k?1 < ik < ?k
A lower-bound constraint pattern for ?.4 can be visualized by annotating the computation p with
backward arrows that represent single-step lower bounds:
a:
ji			?i			ii2i2
*
j
Two constraint patterns are equivalent iff one is a subpattern of the other (i.e., can be obtained by
omitting transitions). It is not hard to show the following t?? properties of lower-bound constraint
patterns:
Property A There is a lower-bound i-constraint pattern for aj.4 (use the truth of (1) over the
?-th suffix of p).
Property B There are only tinitely many different equivalence classes of lower-bound i-constraint
patterns.
We add, for every transition T E T, the boolean variable con?pThted? to our assertion language;
compiefrd? is intended to be true in a state ?, for ? > 0 of a computation p = (a, T) iff the
transition T is completed at the position i of p. For our purpose, it will suffice that cornpThted7
satisfies the two axioms (which are state forwulas)
ftrne? T (compicted??,
ftni?? T--HT f?COrnPl6ted?Y
By Property A, there is an untinied formula of the form
(?q) U0 (?q A ?cnabicd(m1)) U (?q) U (?q A cornpiefrd?1 ) U
U (?q A compThtedr??)
that is true over the i-th suffix of p (where pU0? stands for ? V (pU0y')). Since there are, by
Property B, only finitely many formulas of this form, p ? for some finite disJunction u of nested
unless formulas is 5-valid and, thus, given by untimed safety reasoning. From (t) we infer by the
conditional single-step lower-bound rule U-CSS with respect to any transition T ? ? that
(?CflabI?d(T))U>ty?U(Carnpieted? A o') --H
(??nabThd(?)) U>jy U>Ir (con?pk-t?d7 A ?`)
43
for any state formula y and temporal formula ?. Hence we can decorate the untimed nested
untess formula with time bounds. By repeated collapsing and monotonicity similar to the sample
lower-bound derivation of Subsection 6.2, we arrive at the desired bounded-invariance property (1).
(11) Now suppose that all minimJ delays of 5 are 0; the proof proceeds similarly to the previous
case. Untimed reasoning is complete for untimed properties of 5, because 5 is operational. Any
bounded-invariance property is either trivially not 5-valid or can be established by untimed safety
reasoning. So let us assume that the bounded-response property
p			(2)
is 5-valid. Consequently, every p-state in an initialized computation of 5 has to be followed by a
q-state that can be reached by a sequence of overlapping single-step upper bounds that add up to
at most tt. We visualize single-step upper bounds by forward arrows:
a:
j
Formally, let p = (a,T) be a computation of 5 such that Q, for i > 0. is a p-state, and let % be
the fIrst q-state with j > i. For the sake of simplicity, ?? assume that the transition Tk, which is
completed at the position k > 0 of p, is not enabled on a? (otherwise split Tk into two identical
transitions with different names). A constraint pattern T%?? . . . Thn is an upper-bound u-constraint
pattern iff
`11Tik < u;
it is an upper-bound constraint pattern for a?,?3 iff
(a) `i = i0 < ji ? ... < ???1 <? < ?? and
(b) for all 1 < k < n, the transition 1t?k is enabled but not completed at all states
such that ?k'--H1 < ik ?
It is not hard to see that upper-bound constraint patterns, too, satisfy two crucial properties:
Property A There is an upper-bound fl-constraint pattern for Q..j (use the truth of (2) over the
?-th suffix of p).
Property B There are only tinitely many different equivalence classes of upper-bound fl-constraint
patterns (use the operationality of 5).
By Property A, there is an untimed formula of the form
(enabIed(r?1) A ?compThted?1 ) U (enab1cd(r?2) A ?compietcd?2) u .
U (?nabIed(r??) A ?C0?PTht6drin) U q
that is true over the i-th suffix of p. By Property B, there is again a fInite disjunction `yi of
nested unless formulas such that the implication p 4) is 5-valid and, therefore, given by untimed
safety reasoning. By repeated application of the conditional single-step upper-bound rule ?-CSS,
transitivity, and monotonicity, we arrive at the desired bounded-response property (2). Niore
specifIcally, to collapse nested bounded-ev?nt?aily operators, we can use the valid temporal formula
?-COLL, which is derivable from the transitive upper-bound rule ?-TRANS:
[?-coLL(?<ui?<u2?)--H?<u1+u2??
44
8.2 Crossover reasoning
So far, we have used lower-bound rules to derive bounded-invariance properties and we have used
upper-bound to derive bounded-response properties. In general, the situation is more complicated:
both the lower-bound and the upper-bound rules may be necessary to derive a bounded-invariance
(or bounded-response) property. Indeed, we may need additional crossover rules, which combine
lower-bound and upper-bound requirements.
x = 0?
[0,0]
Let us now formally prove the upper bound 130 on the tenmuation of P1 by explicit-clock reasoning.
To simplify the derivation, we may assume that both processes start simultaneousky at time 0. Then
we can infer the explicit-clock formula
Assun?ng that assignments cost at least 2 time units (instead of 1), tests stili being free, the
maximal value of y would be only 6, implying termination by time SO: the increase of individ-
ual lower bounds decreases the composite apper bound! This phenomenon vividly demonstrates
that real-time reasoning amounts to more than simply adding up minimal delays or maximal de-
lays of individual transitions; it shows that lower-bound and upper-bound requirements are not
independent, but may jointly affect the global titne bounds for tlie execution time of a system.
Note that the first process, P1, consumes the maximal amount of time if its first loop, in which
the value of y is incremented, is executed as often (fast) as possible ii tilnes: the control of P1
may enter the first loop 11 times before and at time 10, the latest time at which the second process
closes the loop, and it may spend another 10 time units in the first loop after the guard has been
reversed. In this worst (slowest) case, the first loop is left at time 20 with ? = 11 and, thus, the
second loop may use up no more than 110 time units. It follows that P1 terminates by time 130.
(start A now = 6o'?i = %2?i = 0)			(now ? 130) 0 ati41
We wish to analyze the worst-case (maximal) running time of the synchronous two-process shared-
variables multiprocessing system
ti' = i,y'= 01[P?IIsP2].
Example: R?ce condition
The need for crossover rules can be illustrated by a mukiprocessing system that looks innocent
at first glance but turns out to be rather intricate, because its execution time depends on an
interesting interplay of the minimal delays and the maximal delays for transitions that belong to
different processes. This increment-decrement system is defined by the following timed transition
diagram:
y:=y'tl [1,10]			[0,0] r$0?
14:
= l,'y = 0)
P2: -A
1[1,10i31 [0,0] ij#0?
ffii?)ThM%?4i
x := 0			2
[1,10]			1
y := y --H
45
by the unless rule from the following global invariant:
(ati01 A ati02 A
(atil A ati02 A
(ati01 A ati21 A
(atil A ati21 A
(ati2i A ati21 A
(ati31 A at 2i A
= now = 6o2?i = 0 v 1 < y < now = ?--Hi)) V
y + 6i1?o < flow = 6o2?i) V
1 ? y ? ii A now < 20) v
y ? 10 A now < 10 + ?--Ho) V
y < ii A naw + jOy < 130) v
1 < y ? 11 A now + lOy < 130 + 631?2).
This proof of timely termination resembles a mechanical, exhaustive case analysis of all possible
state-time combinations that can occur during an execution of the two processes of the ?ncrernent-
decrement system. The bounded-operator proof of the desired bound on termination, on the other
hand, closely follows the intuitive arguinent we outlined above.
Crossover rules
To mimic the informal argument for the timely termination of the increment-decrenient system by
a bounded-operator proof, we use the crossover upper-bound rule:
?-MIX
`0<
P			?<uP
q			E<tq
t?t (I--H 71) fq)
p --H ?`ready
p			?<u(PAiQ)
This rule is a modification of the temporal formula
(?<up A [J<iq))			?<u(p A q?,
which is valid if u < 1. The more complicated form of the rule is needed, because reasoning
about lower bounds and reasoning about upper bounds are asymmetric: while bounded-invariance
formulas refer, intuitively, to the last state before a transition is taken, bounded-response formulas
refer to the first state after a transition is taken. This dichotomy is captured by the inverse
verification condition
?p? (T--Hr1) (q?,
which requires that in any computation p = (a, T) of 5, if Q+i is a p-state and Q+i ? Q, then ?
is a q-state. Also observe that every computation of 5 whose first state falsifies the ready condition
is the suffix of another computation of 5 whose first state satisfies ready. The 5-soundness of the
rule ?-MIX follows.
?Ve give here only a brief sketch of the bounded-operator proof for the bounded-response property
start			?<130at??
of the increment-decrement system. The derivation relies, as expected, on an interplay of lower-
bound and upper-bound rules. First we show that within 10 time units P1 can increase the value
of y at most to 10:
ready ?<ii (y < 10);
46
this is done by inductive lower-bound reasoning. Then we apply the crossover upper-bound rule
?-MIX to the single-step upper bound
start			?<io(ati21 A x = 0),
thus obtaining the bounded-response property
start			?<io(v < 10 A at?21 A x = 0).
From here we proceed by pure upper-bound reasoning, performing a case analysis on the locations
of P1.
While the crossover upper-bound rule combines a bounded-invanance property and a bounded-
response property into a bounded-response property, its counterpart, the crossover lower-bound
rule, yields a bounded-unless formula:
U?MIX u < I
p
q
(p? I--Hri (q?
(qU(qA?f?))
p			_
This rule is S-sound, because it originates with the valid temporal formula (for u < l)
(?<tp A ?<?(qU (q? A ??)))
Note that the last premise, whid? contains only an unbounded unless operator, can be established
by untimed reasoning.
The crossover lower-bound rule U-MIX can be used to derive the lower bound
read?j			[Z<2?at?4?
of the increment-decrernent system.
9 Discussion
The inerernent-decrernent example of the previous section illustrates the trade-off between bounded-
operator reasoning and explicit-clock reasoning. Compare the two proofs of the upper bound on
termination: while the bounded-operator (or "hidden-clock") style of real-time verilication refers to
time only through the relative offsets of time-bounded temporal operators, the explicit-clock style
uses ordinary untimed temporal operators and refers to the absolute time in state formulas. Both
styles trade off the complexity of the temporal proof structure against the complexity of the state
invariants:
The hidden-clock approach combines the conclusions of single-step rules within complex proof
structures similar to the proof lattices for establishing ordinary (untimed) liveness properties
([OL82],[MP84]). Each application of a single-step rute, however, uses a simple local invanant
that refers to a few system locations only.
47
o+ The explicit-clock method employs only the plain unless rule an (untimed) safety rule
but requires a powerful global invariant that relates all system locations.
An alternative proof of the lower and upper bounds on the termination of the increment-deerement
system can be found in [LA9O]; the proof presented there uses global mappings between time-
constrained automata with explicit references to time and is siinilar to our explicit-clock approach.
Open problems and recent developments
There are several problems that have been left open in this paper and some progress has been made
since its submission. First, we presented bounded-operator proof rules and explicit-clock transla-
tions for the verification of bounded-invariance and bounded-response properties only. While these
two classes seem to cover the most important timing constraints, naturally we wish to classify more
complex real-time properties of systems and provide the corresponding bounded-operator proof
rules and explicit-clock translations. Recall, for example, the traffic light system from Subsec-
tion 3.3. ?Vhile the two correctuess conditions (A) and (B) can be speci?ed by temporal formulas,
request			?<? ?<? (light = green),			(A)
request			?<25 ?request,
the third part of the specification, condition (C'), is most naturally expressed using the time-
constrained past temporal operator ?<25 ("throughout the last 25 time units"):
( ?<25 ?request) --H+ light = red.
Only the formula (B) defines a simple bounded-response property. The formula (A) follows by
monotonicity from the bounded-response property
request			?<5 (compThted1?2 v compieted3?2)
and the bounded-invariance property
(completed1?2 v compieted3?2)			?<5 (light = green)
(we write compThted??5 short for the boolean condition that indicates the completion of the tran-
sition from ? to %; also assume ? = 4).
Second, we proved the relative completeness of bounded-operator reasoning only in the case that the
lower bounds and the upper bounds do not interfere with each other. in [Hen9lJ it has been shown
that some history information, say, in form of time-constrained past temporal operators is necessary
to achieve relative completeness in the general case. Note that some information about the past
of a state in a computation is available in explicit-clock reasoning, namely, in form of the delay
counters. An alternative method of incorporating history information relies on an age operator
that indicates, in each state of a computation, for how long a formula has been continuously true
([MMP92]).
Third, we used the discrete time domain of the integers. This does not necessarily mean that all
events occur at integer points in time, only that the time of events is recorded by a fiditious digital
clock with finite precision ([AH92]). While the general verification problem is more difficult for a
dense model of time ([AR90]), it has been shown that bounded-invariance and bounded-response
properties of timed transition systems can be established over the real numbers as time domain
using the proof methods presented in this paper ([HMP92bj).
Acknowledgment. We thank Rajeev Alur for many helpful discussions.
48
References
[AFH9t]
R. Atur, 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.
[AFK88] K.R. Apt, N. Francez, and 5. Katz. Appraising fairness in languages for distributed
programming. Distributed Computing, 2(4):226--H241, 1988.
[AH90]
[AH92]
[AL88]
[BH8tj
[EMSS89]
[Har88]
[Hen91]
[Hen92j
[HLP90]
[HMP90]
[RMP91]
R. Alur and T.A. Henzinger. Real-time logics: complexity and expressiveness. in
Proceedings of the Fifth Annual Syn?osium on Logic in (?mputer Science, pages 390--H
401. IEEE Computer Society Press, 1990.
R. Atur and T.A. Heuzinger. Logics and models of real time: a survey. 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 74--H106. Springer?Verlag,
1992.
M. Abadi and L. Lamport. The existence of refinement mappings. In Proceedings
of the Third Annual Symposium on Logic in Computer Science, pages 165?175. IEEE
Computer Society Press, 1988.
A. Bernstein and P.K. Harter, Jr. Proving real-time properties of programs with tem
poral logic. In Proceedings of the Eighth Annual Symposium on Operating System
PnncipThs, pages 1--H11. AC?4 Press, 1981
E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative temporal rea-
soning. Presented at the First Annual ?Vorkshop on Computer-aided Verification,
Grenoble, France, 1989.
E. Harel. Temporal analysis of real-time systems. Master's thesis, The ?Veizmann
Institute of Science, Rehovot, Israel, 1988.
T.A. Henzinger. The Temporal Specification and I'?rification of Real-time Systems.
PhD thesis, Stanford University, 1991.
T.A. Henzinger. Sooner is safer than later. InformatThn Procesing Letters, 43:135--H141,
1992.
E. Haret, 0. Lichtenstein, and A. Pnueli. Explidt-docl: temporal logic. In Proceedings
of the Fifth Annual Symposium on Logic in Computer Science, pages 402--H413. IEEE
Computer Society Press, 1990.
T.A. Henzinger, Z. Manna, and A. Puneli. An inteileaving model for real time. In
Proceedings of the Fifth Jerusakm 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 Pnnciples of Programming
Languages, pages 353--H366. ACM Press, 1991.
49
[HMP92a]
[HMP92b]
T.A. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In J.W.
de Bakker, K. Huizing, ?V.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory
in Practice, Lecture Notes in Computer Science 600, pages 226--H251. Spnnger-Verlag,
1992.
T.A. Heuzinger, Z. Manna, and A. Pundi. N\?hat good are digital clocks? In ?V. Kuich,
editor, ICALP 92: Automata, Languages, and Programmii?g, Lecture Notes in Com-
puter Science 623, pages 545--H558. Springer-VeHag, 1992.
[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.
[KdR85]
R. Koymans and W.-P. de Roever. Examples of a real-time temporal specifIcation. In
B.D. Denvir, W.T. Harwood, M.I. Jackson, and M.J. N\ray, editors, The Analysis of
Concurrent Systems, Lecture Notes in Computer Science 207, pages 231--H252. Springer-
Verlag, 1985.
[Ke176] R.M. Keller. Formal verification of parallel progranis. Communications of the A CAl,
19(7):371--H384, 1976.
[Koy90] R. Koymans. Specifying real-time properties with metric temporal logic. Real-time
Systems, 2(4):255--H299, 1990.
[KSdR+ 88]
[KVdR83]
[LA9O]
[LA92]
[MMP92]
[MMT91]
R. Koymans, R.K. Shyaniasundar, ?V.-P. de Roever, R. Gerth, and 5. Arun-Kumar.
Compositional semantics for real-time distributed computing. Information and Com-
putation, 79(3):210--H256, 1988.
R. Koymans, J. Vytopil, and ?V.-P. de Roever. Real-time programming and asyn-
ct?ronous message passing. In Proceedings of the Second Annual Symposium on Prin-
ciples of Distributed Computing, pages 187--H197. ACNI Press, 1983.
N.A. Lynch and H. Attiya. Using mappings to prove timing properties. In Proceedings
of the Ninth Annual Symposium on Principles of Distributed Computing, pages 265--H
280. ACM Press, 1990.
L. Lamport and NI. Abadi. An old-fashioned recipe for real time. in J.?V. de Bakker,
K. Huizing, ?V.- P. de Roever, and G. Rozenberg, editors, Real Time: iheory in Prac-
tice, Lecture Notes in Computer Science 600, pages 1--H27. Springer-Veilag, 1992.
0. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker,
K. Huizing, W.- P. de Roever, and G. Rozenberg, editors, Real Time: 7heory in Prac-
tice, Lecture Notes in Computer Science 600, pages 447--H481. Spnnger-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 Concurrency, Lecture
Notes in Computer Science 527, pages 408--H423. Spnnger-Verlag, 1991.
Z. Nianna and A. Pnueli. Proving precedence properties: the temporal way. In J. Diaz,
editor, ICALP 83: Automam, Languages, and Programming, Lecture Notes in Com-
puter Science 154, pages 491--H512. Springer-Verlag, 1983.
[MP83]
50
[MP84] Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness proper-
ties of concurrent programs. Science of Computer Programming, 4(3):257--H289, 1984.
[MP89]
Z. Manna and A. Pnueli. Completing the temporal picture. In G. Ausiello, M. Dezani-
Ciancaglini, and 5. Ronchi Delia Rocca, editors, ICALP 89: Automata Languages, and
Programming, Lecture Notes in Computer Science 372, pages 534--H558. Springer-Verlag,
1989.
[MP92] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems:
Specification. Springer-Verlag, 1992.
[OL82] 5. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACAJ
Transactions on Programming Languages and Systems, 4(3) :455--H495,1982.
J.S. Ostroff. Temporal Logic of ReaPtime Systems. Researd? Studies Press, 1990.
[Ost9O]
[PdR82]
[PH88]
[Pnu 77]
[Pnu86]
A. Pnueli and ?`.-P. de Roever. Rendez-vous with Ada: a proof-theoretical view. In
Proceedings of the SIGPLAN AdaTEC Conference on Ada, pages 129--H?37. ACM Press,
1982.
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 98. Springer-Verlag, 1988.
A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Sym-
posium on Foundations of Computer Science, pages 46--H57. lEEE Computer Society
Press, 1977.
A. Pnueii. Applications of temporal logic to the spedfication and verification of reac-
tive systems: a survey of current trends. In J.?V. de Bakker, W.- P. de Roever, and
G. Rozenberg, editors, Current Trends in Concurrency, Lecture Notes in Computer
Science 224, pages 510--H584. Springer-Verlag, 1986.
[Ron84] D. Ron. Temporal verification of communication protocols. Master's thesis, The ?V&z-
mann Institute of Science, Rehovot, Israel, 1984.
[SPE84] D.E. Shasha, A. Pnueli, and ?V. Ewald. Temporal verification of carrier-sense local
area network protocols. In Proceedings of the 11th Annvai Symposium on Principles
of Programming Languages, pages 54--H65. ACM Press, 1984.
51
