BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1344
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Towards Refining Temporal Specifications into Hybrid Systems
AUTHOR:: Henzinger, Thomas A.
AUTHOR:: Manna, Zohar 
AUTHOR:: Pnueli, Amir
DATE:: May 1993
PAGES:: 15
ABSTRACT::
We propose a formal framework for designing hybrid systems by stepwise 
refinement. Starting with a specification in hybrid temporal logic, we make 
successively more transitions explicit until we obtain an executable system.
END:: CORNELLCS//TR93-1344
BODY::
Towards Refining Temporal
Specifications into Hybrid Systems*
Thomas A Henzinger
Zohar Manna
Amir Pnueli
TR 93-1344
May1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
?his research was supported in part by the National Science Foundation under
grants CCR-92-00794 and CCR-92-23226, by the Defense Advanced Research
Projects Agency under contract NAG 2-703, by the United States Air Force Office of
Scientific Research under contracts F49620-93-1 -0056 and F49620-93-1 -0139, and
by the European Community ESPRIT Basic Research Action Project 6021 (REACT).
Towards Refining Temporal Specifications into Hybrid Systems1
Thomas A. Henzinger
Computer Science Department
Cornell University
Ithaca, NY 14853
e-mail: tahGQThcs.cornell.edu
Zohar Manna
Computer Science Department
Stanford University
Stanford, CA 94305
e-mail: zm?cs.stanford.edu
Amir Pnueli
Department of Applied Mathematics
W&zmann Institute of Science
Rehovot 76100, Israel
e-mail: an?rCQDwisdom.weizmann.ac.il
Abstract. We propose a formal framework for designing hybrid systems by stepwise
refinement. Starting with a specification in hybrid temporal logic, we make successively
more transitions explicit until we obtain an executable system.
1 Introduction
We present the foundations of a methodology for the systematic development of hybrid systems.
As high-level specification language, we suggest Abstract Phase Transition Systems (APTS's). The
behavior of an APTS consists of a sequence of phases, and each phase may be described implicitly
by temporal constraints. For this purpose we introduce Hybrid Temporal Logic (HTL), a hybrid
extension of interval temporal logic. The notion of one APTS refining (implementing) another is
defined, and corresponds to inclusion between the sets of behaviors allowed by each system. We also
propose a criterion for judging an APTS to be executable, i.e., directly implementable on available
architectures. A development sequence, then, is envisioned to start at a high-level implicit APTS,
which is refined by a sequence of steps into an executable APTS. Ultimately, each refinement step
ought to be accompanied by verification.
1This research was supported in part by the Nationai Science Foundation under grants CCR-92-()0794 and CCR-
92-23226 by the Defense Advanced Research Projects Agency under contract NAG2-703, by the United States Air
Force Office of Scientific Research under contracts F49620-93-1-0056 and F4962()-93-1-0139, and by the European
Community ESPRIT Basic Research Action Project 6021 (REACT),
2 Hybrid Temporal Logic
The behavior of a hybrid system is modeled by a function that assigns to each real-numbered time
a system state, i.e., values for all system variables. We require that, at each point, the behavior
function has a limit from the left and a limit from the right. Discontinuities are points where the
two limits differ. We assume the following uncertainty principle: limits of flinction values (defined
over nonsingular intervals) are observable; individual function values (at singular points) are not
observable that is, we cannot know (and do not care) if at a discontinuity the function value
coincides with the limit from the left or the limit from the right.
To specify properties of behavior functions, we use an interval temporal logic with a chop oper-
ator denoted by semicolon [Mos85]. Consistent with our interpretation of behavior functions, only
limits and derivatives of the behavior function can be constrained by atomic formulas; individual
function values cannot appear in specifications.
Syntax
Let V be a set of typed variables. The allowed types include boolean, integer, and real. We view
the booleans and the integers as subsets of the reals, where faThe and true correspond to 0 and 1,
respectively. For a variable x E V, we write #x and YT for the limit from the right (the right limit)
and the limit from the left (the left limit) of r. and x and x for the first derivative from the right
(the right derivative) and the first derivative from the left (the left derivative) of x.
A local formula is an atomic formula over the right and left limits and derivatives of variables
in V. The formulas ? of Hybrid Temporal Logic (HTL) are defined inductively as follows:
9 := o+?"i?'?I?v?I?;?IVx.9
where x ? V and ? is a local formula.
A state formula is an atomic formula over the variables in V. If 4) is a state formula, we write
H4) (and ?) for the local formula that results from 4) by replacing each variable occurrence x in 4)
with its right limit ? (left limit ?, respectively).
Semantics
Let R be the set of real numbers. A state a : V R is a type-consistent interpretation of the
variables in V (i.e., boolean variables may only be interpreted as 0 or 1, and a similar restriction
holds for integer variables). We write ?v for the set of states,
Time is modeled by the nonnegative real line R+. An open interval (a, b), where a, b ?
and a < b, is the set of points t E R+ such that a ? t < b; that is, we consider only open intervals
that are nonempty and bounded. Let I (a, b) be an open interval. A function f: I R is
piecewise smooth on I if
o+ at a, the right limit and all right derivatives of f exist;
o+ at all points t E I, the right and left limits and all right and left derivatives of f exist, and f
is continuous either from the right or from the left;
o+ at b, the left limit and all left derivatives of f exist.
Two functions f, g: I R are indistinguishable on I if they agree on almost all (i.e. all but finitely
many) points t E I. Thus, if two piecewise smooth functions are indistinguishable on the open
2
interval I, then they agree on all limits and derivatives throughout I, on the right limit and right
derivatives at a, and on the left limit and left derivatives at b.
A phase P = (b, f) over V is a pair consisting of
1. A positive real number b> 0, the length of P.
2. A type-consistent family f = (fx 1 x e V? of functions f?: I R that are piecewise smooth
on the open interval I = (0, b) and assign to each point t ? I a value for the variable x E V.
It follows that the phase P assigns to every real-valued time t e I a state f(t) E ?v. Furthermore,
the right limit of f at 0 and the left limit of f at b are defined. We write
P=li?(f(t) 0< t < b?
for the left limiting state P E ?v of the phase P, and
P=li?(f(t)l0<!<by
for the right limiting state			e ?v of P.
Let P1 = (b,f) and P2 = (c,g) be two phases. The phases P1 and P2 are indistinguishable
(equivalent) if b = c and for all variables x ? V, the two functions fx and g? are indistinguishable
on the open interval (0, b). The phase P2 is a subphase of P1 at position a, where 0 < a < b, if
o+ a + c < b and
o+ for all 0 < t < c, g(t) = f(a + t).
If a = 0, then P2 is a leftmost subphase of P1; if a = b --H e, a rightmost subphase. The two phases P1
and P2 partition a third phase P = (d, h) if
o+ d=b+c,
o+ P1 is a leftmost subphase of P, and
o+ P2 is a rightmost subphase of P.
Notice that since P is a phase, for all variables x e V, at b the function hx is continuous either
from the right or from the left. Hence, if P1 and P2 partition P, then the value hx(b) is either
the left limit of fx at b or the right limit of g? at 0. It follows that there are several phases that
are partitioned by the two phases IN and P2. All of these phases, however, are indistinguishable,
because they disagree at most at b.
The formulas of hybrid temporal logic are interpreted over phases. -? phase P = (b, f) satisfies
the hybrid temporal formula ?, denoted P ? ?, according to the following inductive definition:
P ? b iff the local formula ?` evaluates to true, where
--H ? is interpreted as the right limit of fx at 0,
= ?)m(fx(t)l0<t<b?;
3
--H 7 is interpreted as the left limit of f? at b,
7 = li$fljfx(t) 0<1< bi;
--H r is interpreted as the right derivative of fx at 0,
= li?f(fAF)--H?VtIo<t<b?;
--H x is interpreted as the left derivative of f? at b,
r = lim6kfxY)--H7VU--Hb)IO<t<b?.
P ? ?? iff P ?
P ? ?i V ? iff P ? bi or P ?- ?.
P ? ?i; ?2 iff there are two phases P1 and P2 that partition P such that P1 ?--H ?i and P2 ?
P ? Vx. ? iff P' L ? for all phases P' = (b, f') that differ from P at most in the interpreta-
tion f? of x.
Notice that right limits and right derivatives are applied at the left end of a phase, while left limits
and left derivatives are applied at the right end. Also observe that if two phases Pi and P2 are
indistinguishable, then Pi ? b iff P2 ? ?; that is, IITL-formulas cannot distinguish between phases
that differ only at finitely many points.
From now on, we shall write x and x synonymous for the right limit 7 and the right deriva-
tive x, respectively. This convention allows us to read a state formula `? as a hybrid temporal
formula, namely, as the local formula ?
Some sample formulas
It is convenient to define abbreviations for common temporal formulas. The following abbreviations
express that a leftmost subphase, a riglitmost subphase, or any subphase of a phase satisfies the
formula b:
?b			stands for			? V (?; true)
?b			stands for			? V (true; b)
??			stands for			(??) V (?b) V (true; b; true)
Thus we can express that all subphases of a phase satisfy ?:
?b stands for ????
We now define temporal until and unless operators over a phase P. The until formula ?i U?
asserts that the phase P can be partitioned into two subphases P1 (which may be empty) and P2 such
that ?i holds throughout Pi and ?2 holds on a leftmost subphase of P2; the unless formula ?1W?2
asserts that either ?i holds throughout the phase P, or P satisfies ?i U?2:
?Ub2			stands for			(?b2) V
?Wb2			stands for			(??i) V (biUQ'2)
4
The following formula asserts that the variable u ? V is rigid on a phase; that is, the function fu
is constant throughout the phase:
u E Rigid stands for E(? =
Using rigid variables, we can specify that a function is continuous, and that its first derivative is
continuous throughout a phase:
x E C0 stands for Vu,v e Rigid. ?Z+x = u);(Hx = v) v =
x E C1 stands for x E C0 A Vu,v E Rigid. [(x= u);(%L v) v = vi
The formula x E C0 requires that for any partition of a phase P into two subphases, the left and
right limits of r at the point of partitioning coincide; the formula x E C? adds the analogous
requirement for the first derivatives of x.
Hybrid temporal logic subsumes many real-time temporal logics [A1192] and the duration cal-
culus [CHR92]. For example, the formula
?Vx E C0. [(p A x = 0 A E)(x = 1) A rr > 5)
asserts that every p-state of a phase is followed within 5 time units either by a q-state or by the
end of the phase. The variable x is a ??dock" that measures the length of all subphases starting
with a p-state. The formula
VxEC0.[?=OAr'(P?x=l)AE(?PHx=o))			ffiT<lO]
asserts that the cumulative time that p is true in a phase is at most 10. Here the variable x is an
"integrator" that measures the accumulated duration of p-states.
3 Phase Transition Systems
Following [MMP92] and [NSY92j, we model hybrid systems as transition systems. Just as dis-
crete transitions are usually represented as binary relations on states, hybrid transitions can be
represented as binary relations on phases.
Abstract phase transition systems
An abstract phase transition system (APTs) S = (V, ?, ?o ?F, I) consists of five components:
1. A finite set V of state variables.
2. A set P of phases over V.
3. A set ?? C ? of initial phases.
4. A set PF C P of final phases.
5. A set T of transitions. Each transition T ? ? is a binary relation on the phases in ?,
e_ T C P2.
A phase sequence is a finite or infinite sequence of phases. Let P = P0, ..... . P? be a finite
phase sequence with Pj = (bi, fi) for all 0 < i < n. The finite phase sequence P partitions a
phase P = (b, f) if
o+ b = Zo<i<n bi and
o+ for all 0 < i < n Pi is a subphase of P at position Zo<j<i bj.
The finite phase sequence P can thus be viewed as a set of indistinguishable phases, namely, those
phases that are partitioned by T. Consequently, we may interpret HTL-formulas over finite phase
sequences. The finite phase sequence P satisfies the hybrid temporal formula ?, denoted T ? ?, if
some phase that is partitioned by P satisfies ?.
Two finite phase sequences Pi and P2 are equivalent if there are two indistinguishable phases P1
and P2 such that Pi partitions P1 and T2 partitions P2. It follows that all equivalence classes of
finite state sequences are closed under stuttenng: if a phase Pi of the finite phase sequence P is
split into two phases P' and P" that partition Pi, the resulting finite phase sequence
P0,?. .i4--Hi,P',P",Pj+i,. ..P?
is equivalent to P.
Let P = P0,P1,P2,... be an infinite phase sequence with Pi = (bj,fj) for all i > 0. The
infinite phase sequence T diverges if the infinite sum Zi>0 bi of phase lengths diverges, i.e., for all
nonnegative reals t E R+ there is an integer n> 0 such tZhat t < Z0<i<n bi.
A finite phase sequence T is a run fragment of the APT5 S if P is equivalent to a finite phase
sequence P0, ..... . Pn that satisfies three conditions:
Initiality P0 E Po.
Continuous activities For all 0 ? i < fl, Pi e
Discrete transitions For all 0 ? < n, there is a transition ? I such that (Pi, Pi+i) E T.
The run fragment P is complete if Pn ? PF
An infinite phase sequence P is a run (coniputation) of the APTS S if
Safety All finite prefixes of P are run fragments of S.
Liveness T diverges.
The APTS S satisfies a hybrid temporal formula ?, written S ? ?, if all run fragments of S satisfy ?.
Activity transition graphs
Both timed transition systems [11MP92] and timed safety automata [llNSY92] specify APT5's. We
use activity transition graphs to specify APTS's.
An activity transition graph (ATG) is a directed labeled multigraph A = (VD, L, , ?i, ?2, t3, ?)
consisting of the following components:
o+ A finite set VD of data variabThs.
o+ A finite set L of vertices called locations. Each location e E L is labeled by
--H an initial condition ?i(?), a state formula over the variables in ED,
--H an activity [t2(), a hybrid temporal formula over ED, and
--H a final condition ??(?), a state formula over ED.
(3
ye
w = 68 A v = 0 A corn = off
t
= 8 --H 16 v
: E] (corn = on A v < 1) HH t? = 1
(corn=offAv>O) v=--Hi
60 < w < 76
A
A
A
corn := off			$
Figure 1: Specification A
corn := on
A finite set  of edges between the locations in L. Each edge e E E is labeled by a guarded
command ?(e) = (? ?), where ? is a state formula over the variables in VD (the guard
of e) and ? is an assignment to some of the variables in VD.
The ATG A defines the APTS SA =
1. The state variables are V = VDUf7r?, where the control variable 7r ranges over the locations L.
2. For each location C ? T' contains all phases P such that
P ? ?(ir=?)A $)DXECO) Ajt2()
3. For each location  E L, P0 contains all phases P c ? such that
P ? (? = ? A ?(-?
4. For each location  e L, ?F contains all phases P ? P such that
P ?
where ? = ?3(e) is the final condition of .
5. For each edge e E , T contains a transition 7e ? ?2, Let i?? ? L be the source and target
locations of the edge e, and let ? and 0 be the guard and assignment associated with e. Then
(P1,P2) ? r'e iff
pi ?
P2 ?
and P2 results from P1 by executing the assignment 0.
7
Specifications
An ATG with a single location is called a specification.
Consider, for example, the specification A presented in Figure 1. The ATG A specifies a water
level controller that opens and closes a valve regulating the outflow of water from a container. The
container has an input vent through which water flows at the constant rate 8. When the valve is
fully open, there is an outflow of 16, leading to an overall water level decrease of 16 --H 8 = 8 per
time unit. The contro?er can command the valve to open and close using the switch corn.
The specification A refers to three variables:
The boolean variable corn, ranging over the values ?on, off?, represents the latest command
issued by the controller. The value on causes the opening of the valve; the value off, the
closing of the valve.
The real-valued variable v represents the status of the valve. It assumes values between 0
and 1, corresponding to the valve being fully closed (zero water outflow) and fully open,
respectively. When corn = on and v r 1, v increases at the constant rate of 1. When
corn = off and v> 0, v decreases at the same constant rate. By default, when none of these
conditions hold, v maintains a constant value, satisfying the equation i = 0.
The real-valued variable o+w represents the water level. When the valve is fully closed, w in-
creases at the rate 8; when the valve is fully open, `w decreases at the rate 8. At intermediate
values of v, the water level increases at the rate 8 --H 16. v.
The controller is supposed to keep the water level between 60 and 76 units. The two transitions
represent the ability of the controller to set the variable corn to the values on and off.
We point out that the specification describes both the actions of the controller (giving com-
mands to open and close the valve) and the response of the controlled environment (valve closing
and opening and water level rising and falling). When specifying controllers, the set of data vari-
ables VD = Vc U VE of an ATG can be partitioned into a set Vc of controlled vanabks, which may
be modified by the controller, and a set VE of environrnent van'abfrs, which vary according to the
laws of physics. In our example, the switch corn is a controlled variable, while the valve v and
water level tv are environment variables. Note, however, that the equations for the behavior of the
environment variable v are influenced by the value of the controlled variable corn.
4 Stepwise Refinement
Let Si and 82 be two APT5's over the sets V1 and V2 of state variables, respectively. The AFT5 Si
refines the APT5 82 if V2 C V1 and the projection of every run of Si to the variables in V2 is a run
of 82.
Hierarchical activity transition graphs
An APT5 that is given by an ATG can be refined by expanding activities i.e., hybrid temporal
formulas labeling locations into ATG's. Thus we obtain hierarchical (nested) activity transition
graphs (HATG's), which are defined inductively:
8
1. Every ATG is an HATG.
2.
Let 1? = (VD,L,,[t1,Jt2,?3,K) and C be two HATG's, and let A be the tuple B[? := Cc]
that results from B by replacing the activity ?2() of the location ? e L with the HATG Cc.
Then C is also an HATG.
Every HATG A defines an AFTS SA. Roughly speaking, a location ? whose activity is defined by an
HATG Cc contributes all phase sequences P such that P satisfies E](r = ) and some extension ofT
is a complete run fragment of C?. The phase sequence P needs to be extended by data variables
that are local to Cc and a control variable for Cc.
To define the AFTS 5A formally, we inductively translate the nested HATO A into a fiat ATG flal(A).
If A is an ATG, then flat(A) = A; otherwise, A is of the form B[' := Cc], for two ATG's B =
(VD, L, , ?1, It2, ?3, ?) and Cc = (Vc, Lc, Ec, t'i, V2, v3, A) (we assume that the locations in L and L?
are disjoint). Then the ATG flat(A) is defined as follows:
o+ The data variables of flat(A) are VD U Vc.
o+ The locations of flat(A) are (L --H ??) U Lc.
Each location C E (L --H fJ) is labeled by the initial condition jti(?), the activity ?2(?)
and the final condition u3(r").
Each location ? E Lc is labeled by the initial condition ??(?) A vi(?), the activity v2(?),
and the final condition jt3() A v3(C).
0 The graph flat(A) contains the following edges.
Let e ?  be an edge of B from i to `2 where ?i, ?2 E (L --H tY) Then flat(A) contains
an edge from `i to (2 that is labeled by the guarded command ?(e).
Let e E Ec be an edge of Cc from i to (2 Then flat(A) contains an edge from `i to (2
that is labeled by the guarded command A(e).
Let e E F be an edge of B from (? to (, where & ? --H f()) and ?e) = (?
Then flat(A) contains, for all locations (2 ? Vj;, an edge from (i to (2 that is labeled by
the guarded command
(v1((2) A ?)			a.
Let e ? E be an edge of B from (to (2, where (2 E (L --H ((?) and ?(e) = (? a).
Then flat(A) contains, for all locations (i C Vc, an edge from (i to (2 that is labeled by
the guarded command
(v3((1) A ?) --H a.
A run (fragment) of the HATO A, then, is a run (fragment) of the ATG flat(A).
For example, the specification A of the water level controller can be refined into the HATG
presented in Figure 2, which separates the phases at which corn = on from those at which corn --H
off. The two conjuncts ?(w = 8 --H 16. v) and ?(6O ? w ? 76), whid? label the location (, are
common to both locations (o and (i of the inner graph. Also note that the initial conditions of the
inner graph are represented by special entry edges: the initial condition of (o is true and the initial
condition of i is false. All final conditions are, by default, true.
9
: w = 68 A v = 0 A corn = off
?: E(w = 8 --H 16 v) A E](60 < w ? 76)
________L________
0
t)= --H1)
$corn := on
corn := off!
: ?(v ? 1			= 1)
Figure 2: Refinement B
Verification conditions
Let B be all ATG over the set VD of data variables and let ir be a control variable for B. A
refinement step replaces a hybrid temporal formula ? defining the activity of a location  of B with
an ATG 0. The refinement step is correct if the projection of every run of the resulting two-level
HATG B[ := 0] to the variables in VD U ?r] is a run of A.
Suppose that the replaced formula ? is an invariant, i.e., of the form E]?. Then the following
two conditions suffice to establish the correctness of a refinement step:
1. For every edge of the ATO 0 labeled by			the guarded command ? ?, the ATG B contains
a reflexive edge from  to (labeled by ?`			o such that the state formula ? implies the state
formula ?`.
2. There exists a state formula p over VD such that
(?)			SB			#			= 			o+`)`) A			# (			(ir # ) W (7r =  A
(ii)			Sc			#			`?"
The first condition ensures that all discontinuities of the inner graph 0 are admitted by the outer
graph B. The proof obligation (i) asserts that the state formula `?` is true in every left limiting
state of a phase in which the control of the outer graph B enters the location (. Now let P be
a run fragment of the inner graph 0 such that ? is true in the left limiting state of T. The
proof obligation (i?) guarantees that the hybrid temporal formula y holds over T, and since ? is
an invariant, it also holds over any continuous segment off.
For example, to show that the water level controller B refines the specification A, we obtain
two proof obligations:
(?) SA?#
(7r =			= 68 A v = 0 A corn = off))			A
(7r # ) W (w = 68 A v = 0 A corn = off A 7r =
(ii)			SB? ? (w=68Av=0Acorn=off)			[Z
w = 8 --H 16 v			A
(corn =			on A v ?			1)			v = 1			A
(corn =			on A v =			1)			v. = 0			A
(corn =			off A `v =			0)			v = o			A
(corn =			off A v>			0)			v = --H1			A
60 < w			< 76
a
where Bk is the ATG labeling the location  in the refinement B. In a future paper, we will present
a proof system for verifying that an APT5 satisfies a hybrid temporal formula.
Executability
The refinement of a specification typically proceeds ill several stages until we reach an HATG that can
be directly implemented, i.e., executed by stepwise simulation. l?rmally, an HATG A is executable
if two conditions are met:
Effectiveness For each hybrid temporal formula ? defining an activity of A, the set of models
of ? (i.e., the set of phases that satisI, ?) is effectively computable.
NonZenoness The APTS SA is nonZeno: an APT5 5 is nonZ?no if every run fragment of 5
is a finite prefix of a run of 5.
The runs of an executable HATG can be generated by adding one phase at a time. The ef-
fectiveness condition ensures that, in each state, a stepwise interpreter can compute the set of
possible successor phases. The nonZenoness condition ensures that the stepwise interpreter cannot
make a nondeterministic choice among the possible successor phases that will result, later on, in a
deadlock state from which the system cannot proceed or hi a Zeno state from which time cannot
diverge [Hen92, LA92].
It is not difficult to see that both system? -? and B violate the nouZenoness condition and,
therefore, are not executable. For the system A, consider the phase P = (1, f), where f(t) interprets
the data variables as follows, for all 0 < t < 1:
kom(1)			=			off
fv(t)			=			0
fw(t)			=			68+8.t
Thus, as t approaches 1, the value of w approaches 76. This leads to the right limiting state
= ?corn = off, v = 0, w = 76?.
This state is a deadlock state. There is no way to proceed from P without violating the con-
straint w < 76. The same phase caii be reproduced by the system B.
In Figure 3, we present a further refinement of the system B. The refinement C improves on
the system B in two respects. First, the phase in which corn = on and v = 1 has been separated
from the phase in which corn = on aiid v is still increasing. This has beeii achieved by refining the
l1
: w = 6? A v = 0 A corn = off
= 8 --H 16. v)
:			?(% = --H1) A
> 72
= 1) A
?(v < 1)
corn := on
w < 64			corn			off!
2 :
v = 1
Figure 3: Implementation c
location i of the HATG B with a graph consisting of the two locations i (initial condition true,
final condition false) and 2 (initial condition false, final condition true) of the IIATG C. A similar
separation has been carried out for the case that corn = off.
The more important improvement, however, is that the system C forces the setting of corn to
on before w rises above 74, and the setting of corn to off before w falls below 62. This ensures that
the valve starts opening or closing in time to guarantee that w never exceeds the range [60, 76].
Indeed, the system C cannot deadlock and is, therefore, executable.
We say that the HATG A irnpThrnents the specification B if SA refines 5B and A is executable.
For example, the water level controller C implements the specification A.
Environment versus control
In the example of the water level controller, the environment controls the environment variables v
and w only through differential equations (activities); the environment does not modify any vari-
ables through guarded commands (transitions). If the environment can modify variables through
transitions, we have to adopt a stricter notion of refinement. In particular, a refinement step should
not introduce new constraints on the environment [AL9o].
Consider, for example, the ATG D presented in Figure 4. The specification D is a generalization
of the specification A. The container now has two valves, v? and v0. The valve v0 controls, as
before, the rate of outflow. The valve Vj controls the infiow of water into the container and, similar
to v0, can assume a real value between 0 and 1. The two valves are regulated by the two boolean
command variables corn? and corn0 that can assume the values 0 (off) and 1 (on). The conditional
differential equation
corn? = 2. corn --H 1
M
K ?
: w = 68 A Vj = 0 A v0 = 0 A corn? = 0 A C0rflo = 0
t
E
= 8 Vj --H 16. v0
(vi # corn?) t;j = 2. corn? --H 1
(v0 # corn0) v% = 2. C0Tn0 --H 1
60 ? w ? 76
A
A
A
corn0 :? fQ l?			! corn? :? (Ql?
Figure 4: Specification D
: w = 68 A Vj = 0 A v0 = 0 A C0Tflj = 0 A corn0 = 0
i__________________
w =			68			A
: E]			v? =			v0			= 0			A
corn?			=			corn0 = 0
Figure 5: Lazy refinement 
should be interpreted as a compact representation of the two cases
((corn? = 1 A Vj ? 1)			= 1)			A
((corn? = 0 A Vj ? 0)			= --H1)
The only variable that can be directly modified by the controller is the outflow switch corn0.
All other variables, including the inflow switch corn?, are environment variables. The continuous
environment variables W, Vj, and v0 are governed by differential equations. The boolean environment
variable corn?, however, is modified by transitions. The notation corn? :? (0, l? labeling the edge
in Figure 4 means that there are two transitions setting corn? nondeterministically to 0 or 1,
respectively.
We will assume that all transitions of an APTS can be partitioned into systern transitions, which
modify only controlled variables, and enviionrnent transitions, which modify only environment
variables. For example, the specification D contains two system transitions, which update corn0,
and two environment transitions, which update corn?.
Let us consider what type of refinements the specification D can have. If we retain the notion
of refinement as defined above, namely, that the APTS S1 refines the AFTS S2 if every computation
of S2 is also a computation of Si, we can point at the HATG  of Figure 5 as a possible refinement
of D. This refinement omits all transitions and, as a result, the command variables corn? and corn0
13
and, consequently, the valve variables Vj and v0 all remain at 0, leading to a constant value of the
water level w at 68, which is well within the prescribed range.
It is quite obvious that  cannot be accepted as a reasonable implementation of D. The easy
solution that  opted for is to prevent the environment from ever commanding the valve Vj to open.
By contrast, the intended meaning of the specification D is that, no matter how the environment
commands the input valve to open or close, the controller will find a way to open and close the
output valve so that the water level will remain within the prescribed limits.
Consequently, in the presence of environment transitions, we adopt the following definition for
refinement between two APTS's. Let 81 and 82 be two APTs's over the sets V1 and V2 of state
variables, respectively, such that V2 C V1 and VE C ?) is a set of environment variables. The
APTS Si r?fines the APTS 82 if
1. The projection of every run of Si to the variables in V2 is a run of 82.
2.
Every environment transition of 82 is duplicated in 8?; that is, if (P1, P2) is an environment
transition of 82 and the Si-phases P1, and P2, are extensions of the 82-phases P1 and P2 to
the variables in V1, then (P1,, P2,) is a transition of 81
Thus, the refinement of a specification must respect all environment transitions that appear in the
specification.
= 68 A Vj = 0 A v0? = 0 A con1? = 0 A corn0 = 0
= 8 Vj --H 16. v0) A
$ corni)			= 2. cam --H l)
t
0
< 74)
72			corn0 := on
1
= 1) A
< l)
= 0
Y
3
= --Hl) A
?(v?>0)
w < 66 corn0 := off)
ffi -???_ _
v0 = 1
2
E](64 <
M
com? :E fO, l?
Figure 6: Proper implementation F
?Tith this more stringent notion of refinement, the IIATG E no longer refines the specification D,
because it fails to duplicate the environment transitions?f D. In Figure 6 we present an HATG F
that does implement the specification V, i.e., F refines V and is executable. The self-loop on the
bottom represents the environment transitions that may set com? to a new value at any point.
14
Drawing a self-loop at an enclosing box is interpreted as if there is a similar self-loop at each of the
four internal locations.
Acknowledgements. We gratefully acknowledge the help of Luca de Alfaro, Eddie Chang,
Arjun Kapur, and Henny Sipma for their careful reading of the manuscript and thank them for
many helpful suggestions.
References
[AL9O]
[AH92j
M. Abadi and L. Lamport. Composing specifIcations. In J.W. de Bakker, W.-
P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems,
Lecture Notes in Computer Science 430. Springer-Verlag, 1990.
R. Alur and T.A. Henzinger. Logics and models of real time: a survey. In J.W. de Bakker,
K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice,
Lecture Notes in Computer Science 600,pages 74--H106. Springer-Verlag, 1992.
[C11R92] z. Chaochen, C.A.R. Hoare, and A.P. Rayn. A calculus of durations. Information
Processing Letters, 40:269--H276,1992.
[Hen92] T.A. Henzinger. Sooner is safer than later. Information Processing Letters, 43:135--H141,
1992.
[HMP92]
T.A. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In J.W. de Bakker,
K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice,
Lecture Notes in Computer Science 600,pages 226---251. Springer-Verlag, 1992.
[HNSY92j T.A. IIenzinger, X. Nicollin, J. Sifakis, and 5. Yovine. Symbolic model checking for real-
time systems. In Proceedings of the Seventh Annual Symposium on Logic in Computer
Science, pages 394--H406. IEEE Computer Society Press, 1992.
[LA92j
[MMP92]
L. Lamport and M. Abadi. An old-fashioned recipe for real time. In J.W. de Bakker,
K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice,
Lecture Notes in Computer Science 600,pages 1--H27. Springer-Verlag, 1992.
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: Theory in Practice,
Lecture Notes in Computer Science 600,pages 447--H4S4. Springer-Verlag, 1992.
[Mos85] 13. Moszkowski. A temporal logic for multi-level reasoning about hardware. IEEE
Computer, 18(2):10--H19, 19S5.
X. Nicollin, J. Sifakis, and 5. Yovine. From ATP to timed graphs and hybrid systems.
In J.W. de Bakker, K. Huizing, ?V.-P. de Roever, and G. Rozenberg, editors, Real Time:
Theory in Practice, Lecture Notes iii Computer Science 600, pages 549--H572. Springer-
Verlag, 1992.
15
[N5Y92]
