BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR94-1437 
ENTRY:: 1994-08-26
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Model Checking Strategies for Linear Hybrid Systems 
AUTHOR:: Henzinger, Thomas A.  
AUTHOR:: Ho, Pei-Hsin
DATE:: July 1994 
PAGES:: 15 
ABSTRACT::
Linear hybrid systems are dynamical systems whose variables change
both discretely and continuously along piecewise linear trajectories;
they are useful for modeling digital real-time programs that are
embedded in analog environments. Model checking is an algorithmic
technique for anlayzing finite- state systems that has recently been
extended to certain infinite-state systems, including linear hybrid
systems.  The method has been implemented in HyTech (The Cornell
Hybrid Technology Tool), a symbolic model checker for linear hybrid
systems.  We report on a new implementation and several experiments
with HyTech.

The core of HyTech is a semidecision procedure that, given a linear
hybrid automaton describing a system and a temporal formula describing
a requirement, computes the so-called target region-the linear set of
system states that satisfy the requirement.  Unfortunately, the
verification procedure may not return the target region using a
reasonable amount of time and space, or it may not terminate in
principle.  Thus we have reimplemented the model checker using more
efficient data structures that represent linear state sets
geometrically, as unions of convex polyhedra, and we have experimented
with several strategies that are designed to improve the performance
of the model checker further: we (1) simultaneously compute the target
region from different directions, (2) encode data as finite-state
control, (3) approximate the target region by dropping constraints,
and (4) iteratively refine the approximation until sufficient
precision is obtained.  Interestingly, symbolic model checking
(fixpoint computation by iteration) and the polyhedral approximation
strategies (3) can be viewed as the abstract interpretation of linear
hybrid systems.
END:: CORNELLCS//TR94-1437 
BODY::
Model Checking Strategies for
Linear Hybrid Systems*t
Thomas A. Henzingertt
Pei-Hsin Ho
TR 94-1437
July 1994
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*This research was supported in part by the National Science Foundation under grant
CCR-9200794, by the United States Air Force Office of Scientific Research under
contract F49620-93-1 -0056, and by the Defense Advanced Research Projects
Agency under grant NAG2-892.
tA presentation based on this paper was given at the Workshop on Formalisms for
RepresentThg and ReasonThg about Time, organized by 5. B. Seidman and H. Gill as
part of the Seventh International Conference on Industrial and EngTheerThg
Appllcations ofArtificial Intelligence and Expert Systems on May 31, 1994, in Austin,
Texas. Since then, it has come to the authors' attention that a group in France has
been working on approximation strategies for analyzing linear hybrid systems similar
to those presented in this paper [HRP94].
ttphone: (607)255-3009. FAX: (607) 255-4428.
Model Checking Strategies
for Linear Hybrid 5ystems*t
Pei-Hsin Ho
Thomas A. Henzingert
Computer Science Department
Cornell University
(tah ho)?cs.cornell.edu
Extended Abstract
Abstract. Linear hybrid systems are dynamical systems whose variables change both
discretely and continuously along piecewise linear trajectories; they are useful for mod-
eling digital real-time programs that are embedded in analog environments. Model
checking is an algorithmic technique for analyzing finite-state systems that has recently
been extended to certain infinite-state systems, including linear hybrid systems. The
method has been implemented in HyTech (The Cornell Hybrid Technology Tool), a
symbolic model checker for linear hybrid systems. We report on a new implementation
and several experiments with HyTech.
The core of HyTech is a semidecision procedure that, given a linear hybrid automa-
ton describing a system and a temporal formula describing a requirement, computes
the so-called targetregion--Hthe linear set of system states that satisfy the requirement.
Unfortunately, the verification procedure may not return the target region using a rea-
sonable amount of time and space, or it may not terminate in principle. Thus we have
reimplemented the model checker using more efficient data structures that represent
linear state sets geometrically, as unions of convex polyhedra, and we have experi-
mented with several strategies that are designed to improve the performance of the
model checker further: we (1) simultaneously compute the target region from different
directions, (2) encode data as finite-state control, (3) approximate the target region
by dropping constraints, and (4) iteratively refine the approximation until sufficient
precision is obtained. Interestingly, symbolic model checking (fixpoint computation by
iteration) and the polyhedral approximation strategies (3) can be viewed as the abstract
interpretation of linear hybrid systems.
This research was supported in part by the National Science Foundation under grant CCR?92oo794, by the
United States Air Force Office of Scientific Research under contract F4962O?93-1-OO56, and by the Defense Advanced
Research Projects Agency under grant NAG2?s92.
tA presentation based on this paper was given at the Work?hop on Forma!isms for Representing and Reasoning
abo?t Time, organized by S.B. Seidman and H. Gill as part of the Seventh International Conference on Indvstrial
and Engineering Applications of Artificial Intelligence and Expert S?stems on May 31, 1994, in Austin, Texas. Since
then, it has come to the authors' attention that a group in France has been working on approximation strategies for
analyzing linear hybrid systems similar to those presented in this paper [HRP94].
tphone: (607) 255-3009. FAX: (607) 255-4428.
0
1 Introduction
Hybrid systems extend discrete programs with continuous activities [MMP92]. Consider a commu-
nication protocol A with k propositional variables (values 0 or 1), and a robot 13 with k propositional
control variables and n real-valued status variables (e.g., the position of the robot). Let d = k
A state of A is a point in k-dimensional boolean space; a state of 13, a point in d-dimensional et-
clidean space. Each transition of A is a k-dimensional boolean transformation; if 13 is tinear, then
each discrete control transition of 13 is a d-dimensional linear transformation and each continuous
activity of 13 is a d-dimensional piece-wise linear motion. It is this geometric intuition that inspired
the model-checking strategies developed in this paper.
For the finite-state system A, model-checking algorithms compute the state set (target region)
that satisfy a given temporal requirement specification, by iterative approximation of the target
region as a fixpoint. This is done either enumeratively [CES86] or symbolically, by representing
state sets (regions) as boolean expressions [BCM+92]. Since the state space of the linear hybrid
system 13 is infinite, enumerative model checking is no longer possible, and regions must be rep-
resented symbolically. A symbolic model-checking algorithm for linear hybrid systems has been
developed [ACHH93, NOSY93, ACH+94, HNSY94], and implemented (HyTech) by representing
regions as real-valued linear expressions [AHH93]. The linearity condition is key so that if the
target region is a finitely approximable fixpoint, then it can be computed in the theory of the
reals with addition, at "tolerable" cost. The most serious limitation of finite-state model checking,
the state-explosion problem, reoccurs for the infinite state spaces of linear hybrid systems in three
guises. The main theoretical limitation of the method is that termination (i.e., finite approximabil-
ity) is not guaranteed (problem A); the main practical limitation of the implementation is its cost,
which is largely due to two factors. First, continuous activities correspond to quantifier-elimination
steps on real-valued linear expressions (problem B); second, if expressions are transformed into
disjunctive normal form for further manipulation, then the number of disjunctions grows rapidly
(problem C).
Having identified the three problems, we improved the performance of HyTech by using algorithms
that manipulate geometric objects rather than expressions, and by adding various heuristic strate-
gies, both exact and approximate, to guide the fixpoint computation of the target region.1 To
address problem A, we approach the target region simultaneously from several directions, so that
success is guaranteed even if only one direction terminates (Section 3.1). To address problem B, we
represent regions as unions of convex polyhedra, so that quantifier elimination is replaced by linear
operations on polyhedra. Instead of computing in a single d-dimensional space, it is usually prof-
itable to work with k n-dimensional spaces (Section 3.2). To address problem C, we approximate
the union of several convex polyhedra by a single convex polyhedron. We discuss two approxi-
mation operators--Hconvex-hull approximation (Section 4.1) and extrapolation (Section 4.2). Each
approximation can be iteratively refined to achieve the desired precision (Section 4.3) [DW93].
We wish to point out that the fixpoint computation by iteration and the approximation strategies
of Section 4 are but the old technique of abstract interpretation [CC77] applied to a new domain--H
that of linear hybrid systems. Convex-hull approximation [CH78] and widening [CC77], which
is related to our extrapolation operation, has been used for the static analysis of sequential and
synchronous programs [Hal93], i.e., for the analysis of discrete state spaces. We feel that both
1The new version of HyTech, including tactics, is available by anonymous ftp from ftp.cs.cornell.edu, direc-
tory pub/tahIHyTech. As far as we know, HyTech is the only implementation of model checking for the full class of
linear hybrid systems.
Figure 1: The water-tank automaton
approximations are particularly suited for the analysis of the continuous and linear state spaces,
because a polyhedron more naturally represents all of its interior points rather than just the grid
of interior integer points, and because the linear regions are closed under both approximation
operations. This feeling is substantiated by the experimental results we report in Section 3.2,
where polyhedra approximate continuous regions more efficiently than discrete regions.
This abstract presents only overapproximation operators. In the full paper we also discuss the
sound use of underapproximation operators, and the iterative application of alternating over- and
underapproximation for linear hybrid systems.
2 Linear Hybrid Automata
We model systems as hybrid automata [ACHH93]. A (linear) hybrid automaton A consists of a finite
set X of real-valued variables and a labeled graph (V, E). The edges E represent discrete system
transitions and are labeled with guarded commands on X; the vertices V represent continuous
environment activities and are labeled with differential equations and constraints on X. A state
(v, s) of the hybrid automaton A consists of a control state v C V (a vertex) and a data state 5:
X R (a function that assigns values to all variables). A set of (data) states is called a (data)
region. A run of A is a function from the nonnegative real line ?+ to states. The reachability
problem for A asks, given an initial region 5 and a final region T, if there is a run of A that leads
from an initial state in 5 to a final state in T. If T represents the set of "unsafe" states of a safety
requirement, then the requirement can be checked by reachability analysis.
Example: water tank
The hybrid automaton of Figure 1 models a water-level controller that opens and shuts the outflow
of a water tank. The automaton has two variables (data), x and y, and two vertices (control), A
and B. The variable x represents a clock of the water-level controller and the variable y represents
the water level in the tank. Since the clock x measures time, the first derivative of x is always 1
(i.e., x = 1). In vertex A, the outflow of the water tank is shut and the water level increases 1 inch
per sec (? = 1); in vertex B, the outflow of the water tank is open and the water level decreases
2 inches per sec (y = --H2). The transition from B to A (shut the outflow) is taken as soon as the
water tank becomes empty: the guard y = 0 on the transition ensures that the transition may
be taken only when the water level is 0; the constraint y > 0 on B ensures that the transition to
A must be taken before the water level becomes negative. The transition from A to B (open the
2
3
A
9
y
3			6
Figure 2: A run of the water-tank automaton
outflow) is taken every 3 sec: the transition is taken whenever x = 3, and the transition restarts
the clock x at 0. If the automaton is started from the state A A x =y =0,2 then Figure 2 shows
how the water level y changes as a piecewis&linear function of time.
The symbolic model checker HyTech
In this paper, we study the performance of HyTech, a fully automatic model checker for hybrid
automata [AHH93], on reachability problems. HyTech is implemented within Mathematica as
a collection of procedures that manipulate jinear regions: if n is the number of variables, then
a linear data region is the union of convex polyhedra in n-dimensional space; a linear region
R = UvEv(V, R[v]) is a collection of linear data regions R[v], one for each control state v. While
the original implementation of HyTech represented each region as a boolean combination of linear
constraints, the new version of HyTech represents each convex polyhedron by its extreme points
(corners) and extreme rays (generators). The polyhedral operations are implemented as
subroutines that call on a polyhedral library [Hal93j. The algorithms and implementation details
will be given in the full paper. The speedup achieved by the geometric algorithms over the original
(pure Mathematica) version of HyTech is about a factor of 4.
3 Exact Verification Strategies
We discuss some degrees of freedom offered by the HyTech verifler and show how a particular choice
of parameters may influence its performance on a given reachability problem.
3.1 Forward versus Backward Analysis
Suppose that we wish to check if the final region T is reachable from the initial region S. There are
two possible approaches for solving the reachability problem by symbolic model checking [ACHH93]:
we may compute the target region post*(S) of states that can be reached from the initial region
S and check if post*(S) nT = ? (forward reachability analysis), or we may compute the target
region pre*(T) of states from which the final region T can be reached and check if pre*(T)fl5=
(backward reachability analysis). For any given reachability problem, one approach may perform
2We define states and regions by formulas. For example, the formula A A x> 1defines the set of all states whose
control component is A and whose data component assigns to the variable xa value greater than 1.
3
3-			3
(a)
3 z
T0 I =
3 x
Figure 3: Exact forward and backward reachability
better than the other approach; indeed, it may be that one approach terminates and the other does
not.
Recall, for example, the water-tank automaton of Figure 1 We wish to check if the final state
t = (A A x = 3 A y = 2) can be reached from the initial state 5 = (A A x = y = 0). The
symbolic model-checking procedure computes the two regions post*(s) and pre* (t) as the limits of
two sequences of regions. Let Sj+1 = post(Si) be the region of states that can be reached from 5
by i + 1 discrete transitions, and let Tj+1 = pre(Tj) be the region of states that can reach t by i + 1
discrete transitions. Then post*(s) is the limit Uj>0 Sj, and pre*(t) is the limit U1>0 Tj. Since
(Figure 3(a)) and
S2j = (A A y+l+ 2i =? Ax <3)
2t+1 --H (BA2x+?=2+
the forward computation of post*(s) does not terminate within any finite number of iterations. The
backward computation, however, converges in a single iteration with the result
T0 = T2 = (A A 1 <x <3 A x = y+ 1)
(Figure 3(b)) and
It follows that
T1 = T3 = (BAx+2y=2).
pre*(t) = (A A 1 <x <3 A x = y + 1) v (B A x + 2y = 2).
Since 5 ? pre*(t), we conclude that the final state t cannot be reached from the initial state 5. For
optimal performance, we have implemented a strategy that dovetails both approaches by computing
the alternating sequence S0, T0, s1, T1,S2,... of regions.
4
Zi > 10
Xi			:= 0; k1			k1+1
X2 >20
z2 := 0; k2 := k2 + 1
Z2 = 1
k1 := k1 --H 1; Yi := 0
inti
int,
3.2 Data versus Control
Figure 4: The priority scheduler, data version
Data variables that range over a finite domain of values can be encoded within the control of
a hybrid automaton. Our experience has been that HyTech performs better if all finite-state
variables are encoded in the control. We illustrate this observation with two examples taken from
scheduling--Ha priority scheduler and a round-robin scheduler. Schedulers are examples of hybrid
systems with stop watches--Hvariables whose slope is sometimes 0 and sometimes 1 which measure
the accumulated amount of execution time for each task.
Example: priority scheduler
The two smail hybrid automata on the left of Figure 4 model an environment that generates two
types of interrupts: an interrupt of type inti arrives at most once every 10 sec; an interrupt
of type int?, at most once every 20 sec. For every ifltj interrupt, a task of type i needs to be
executed: each type-i task requires 4 sec; each type-2 task, 8 sec. Moreover, only one processor
is available for the execution of ail tasks, and type-2 tasks have priority over type-i tasks and
interrupt their execution. The resulting priority scheduler is modeled by the hybrid automaton
on the right of Figure 4. in vertex Task1, a type-i task is being executed; in vertex Task2, a
type-2 task. The variable ki represents the number of incomplete (i.e., running and pending) tasks
of type i; the variable Vi represents the execution time of the current task of type i. The three
automata synchronize on the edge labels inti and int?; that is, whenever an inti interrupt arrives,
the scheduler takes a transition that is labeled with inti. The entire scheduling system, then, is the
product of the three component automata [ACHH93]. Using HyTech, we verified that in any run
starting from the region Idle A k1 = k2 = 0 the number of incomplete type-i tasks never exceeds 2
and the number of incomplete type-2 tasks never exceeds 1; that is, no state that satisfies k1 > 2
or k2 > 1 is reachable.
5
int2
Idle ???4)nt2 ??			2 0 int2
2			0			2			0
Figure 5: The priority scheduler, control version
Since the variables k1 and k2 range over finite domains, they can be encoded in the control of
the scheduler. The control version of the priority scheduler (Figure 5), then, contains a vertex
(k1, k2) for all possible values of the variables k1 (namely, 0, 1, and 2) and k2 (0 and 1). The vertex
Overflow represents any state with k1 > 2 or k2 > 1. We checked that the region Overflow cannot
be reached from the region Idle = (0,0). We also increased the number of interrupt and task types
and the results of these experiments, which were performed on a Sparc 670MP station, are shown
in Figure 6. Clearly, our verifier handles finite-state control more efficiently than real-valued data.
Example: round-robin scheduler
Figure 7 shows a round-robin scheduler. The two task types are assigned alternating time slices of
2 sec, as measured by the clock z. if all tasks of one type are completed, the scheduler starts a new
time slice for the tasks of the other type. Again we check that the number of incomplete type-i
tasks is bounded by 2 and the number of incomplete type-2 tasks is bounded by 1, which allows us
to encode the variables k1 and k2 in the control of the scheduler. The verification results are also
shown in Figure 6.
4 Approximate Verification Strategies
Sometimes the exact computation of a target region is prohibitively expensive or does not termi-
nate, independent of both the system description (data vs. control) and the verification strategy
(forward vs. backward). in such cases, we approximate the target region and iteratively refine
the approximation until sufficient precision is obtained. We discuss two approximation operators--H
convex-hull approximation and extrapolation--Hwhich can be turned on or off by the user of HyTech.
6
Priority scheduler, 2 tasks, data version 590 sec
Priority scheduler, 2 tasks, control version 57 sec
Priority scheduler, 3 tasks, data version 33,326 sec
Priority scheduler, 3 tasks, control version 686 sec
Priority scheduler, 4 tasks, data version out of memory
Priority scheduler, 4 tasks, control version 49,024 sec
Round-robin scheduler, 2 tasks, data version 1,965 sec
Itound-robin scheduler, 2 tasks, control version ??2 sec
Figure 6: Performance data (CPU time)
Both operators overapproximate the union of convex polyhedra by a single convex polyhedron and
thus reduce the time and space requirements of the verifier; indeed, either operator, or the com-
bination of both operatofs, may cause the termination of an otherwise infinite computation. If
we overapproximate, by 5, the target region post*(s) of states that are reachable from the initial
region 5 (i.e., post*(s) c 5), and 5contains no final state from T, then we can conclude that T is
not reachable from 5; if, on the other hand, 5 does contain a final state, then we cannot reach a
valid conclusion and must refine the approximation.
We acknowledge the work of Nicolas Halbwachs, who has used a convex-hull operator and a so-
called widening operator, which is similar in spirit to our extrapolation operator, for the analysis
of synchronous programs [Ha193]3; also, the current implementation of HyTech makes use of Halb-
wachs's polyhedral library. The idea of iteratively refining approximations originated with David
Dill and Howard Wong-Toi for the analysis of real-time systems [DW93j.
4.1 Convex-hull Approximation
An approximationoperator+is a binary operator on data regions such that for two data regions R
and R', (1) RUR' C R+R', (2) R+R' is convex, and (3) if R and R' are linear, then so is R+R'.
Every approximation operator extends to regions as follows: for two regions R = UvEV (v,R[v])
and R' = UvEv(V,R'[V]), R + R' = UvEv(V,R[V] + R'[v]). Clearly, the convex-hull operator &,
which maps two data regions R and R' to the convex hull of the union R u R', is an approximation
operator.
Recall once again the water-tank automaton of Figure 1. Now we wish to check if the final state
= (A A x = ?21 A y = 0) can be reached from the initial state 5 = (A A x = y = 0). Again,
the forward computation of the target region post*(s) does not terminate. This time, however, we
can make the forward approach work with the help of convex-hull approximation. If we naively
take the convex hull 52 of the two regions 5o and 52 (Figure 8(a)), then the forward computation
terminates with the overapproximation 52 of the A-component post*(s)[A] of the target region,
because post2(S?) --H 52 Since 5o contains t', however, we cannot conclude that t' is or is not
reachable from 5. Thus we apply the convex-hull operator only if the resulting region does not
contain any final states;4 that is, we approximate the target region post*(5) = Uj>0Si by the
3Halbwachs' widening operator causes a coarser approximation than extrapolation but, unlike extrapolation,
guarantees the convergence of iterative application.
4This strategy is sensible for all approximation operators.
7
Idle
= 4 A k2 = 0 A k1 > 2 = A k1 = 1 A
k1			k1 --H 1;yi =0			k2 0			k1 =0			k2 k2 --H			=0
z = 3 A k2 = 0			z := 0			z = 3 A k1 = 0			z 0
Figure 7: The round-robin scheduler
limit S = Uj>0 Sj, where
Si+1[v] --H			post(Si)[v]&Si[v]
post(Si) [v]
if (post(Si)[v] & Si[v]) n T
otherwise.
For Qe water-tank example, this strategy, then, computes So = So, 52 = 52, 54 = S4&S2,
and 56 = 54 (Figure 8(b)). So we obtain the limit So U 54 as an overapproximation of the A-
component post*(s) [A] of the target region. Since So U 54 does not contain t', we conclude that the
final state t' is not reachable from the initial state 5.
4.2 Extrapolation
Convex-hull approximation may be found useful for systems with variables whose values are bounded,
such as the water-tank automaton. By contrast, if the regions in the sequence Ui>0 Sj grow with-
out bound, we may want an extrapolation operator that "guesses" an overapproximation of the
limit Uj>0 Sj. Consider, for example, the hybrid automaton of Figure 9, which models the movement
of a robot in the (x, y)-plane. The robot can be in one of two modes--Hheading roughly northeast
(vertex A) or heading roughly southeast (vertex B): in mode A, the derivatives of the coordinates
? and y vary within the closed interval [1, 2]; in mode B, the derivative of x remains between 1 and
2, while the derivative of ? changes its sign and varies between --H1 and --H2. The robot changes its
mode every 1 to 2 min, according to its clock z. Moreover, there is a wall at the x = 0 line, causing
the system invariant r > 0. Figure 10 shows how the position of the robot in the (x, ?)-plane may
change with time, assuming the robot is started in the initial state 5 = (A A x = y = z = 0).
We wish to check if the robot can reach, from s, the final position T = (x = 9 A ? = 12). At this
point, we invite the ambitious reader to prove that T cannot be reached from s. Using HyTech,
8
3-
(a)
3x
I,
3
3 x
Figure 8: Approximate forward reachability
Figure 9: The robot automaton
the backward computation of the region pre* (T) terminates within 74 sec of CPU time after seven
iterations, and 5 ? pre*(T). The forward computation of the region post*(s), by contrast, does
not terminate, because the robot keeps zig-zagging to the east and the limit Ui>o post1(s) cannot
be computed exactly.5 As convex-hull approximation does not help with this example, we define
an extrapolation operator that approximates the unbounded target region post*(s); using HyTech,
the forward computation with extrapolation, then, terminates within 8 sec of CPU time.
We first give an intuitive motivation for the extrapolation operator. Suppose that the iterative
computation of the target region leads, for a given control state, to the data region (polyhedron)
R and, in the subsequent iteration, to the polyhedron R'. Suppose, furthermore, that there is a
function f such that f maps R to R', mapping extreme points to extreme points. A reasonable
guess for the target region, then, would be f0o(R).
To formally define an operator oc that extrapolates R and f(R) to f0o(R) we need to review
some facts about convex polyhedra [NW88]. By Minkowski's theorem, every nonempty convex
polyhedron R in I?? has a unique (within scalar multiplication) representation by its extreme
5T?ue, if the target region T is reachable, then it can be reached within a finite number of discrete transitions,
and if not, then the invariant 2' > 9 becomes true after a finite number of transitions; extrapolation, however, avoids
the ad-hoc "guessing" of suitable invariants.
9
Figure 10: A run of the robot automaton
points ?Xj I i E 11 and extreme rays ?r? j E JY such that
R = ?ER?Ix = ?Ajxt+ZIijrj, whereA?,???+and SAi=1Y.
?EI			jEJ			jEl
Notice that if the point x and the ray r are in R, then so are all points of the form x + Ar,
for A E R+. The nonempty convex polyhedron R has dimension k, denoted dim(R) = k, if there
are k+1 pointsxi,x?,...,x?+i mRsuchthatthekdifferencesx2--Hxi,x3--Hxi,...,x?+1--Hxi are
linearly independent. Notice that if dim(R) = 0, then R is a point, and if dim(R) = 1, then R is
a straight line, a ray, or a line segment. The set F = ?x ? R I ax = b?, for two vectors a and b,
is a face of 1? if every point x in R satisfies the inequality ax < b. Notice that every face of R is
also a convex polyhedron. The face F is a facet of R if dim(F) = dim(R) --H 1. The set F is a
i-dimensional face of R iff F is the intersection of dim(R) --H 1 facets of R (t)
Now consider two polyhedra R and R'. We first compute the convex hull R&R' of R u R'. All
extreme points and extreme rays of the convex hull R&R' are extreme points and extreme rays
of R or R'. Let ?xk k E 11 be the extreme points of R&R' and R, let ?xL I 1 E l1Y be the
remaining extreme points of R&R', and let ?r? j E J? be the extreme rays of R&R'. Suppose
that k E I and 1 E I', and xk and XL are the endpoints of a i-dimensional face of R&R', which can
be checked by Criterion (t). Then it is possible that f(xk) = XL for the imaginary function f from
R to R'. Moreover, if f is applied infinitely many times, then all points of the form x? + A(xt --H xk),
for A E I[?+, are included in f0o(R). We therefore add the ray Xj --H xk into the generators of R 0:
the extrapolation operator 0: maps the two polyhedra R and R' to R oc --H
fx E I?n x = ? Ajxj+Z!i1r5+ ? ?k,L(xL--HXk), where Ai,4j,iik,L E ?+ and ? Aj =
jElUl'			jEJ			(k,L)EK			tElUl'
where (k,l) Ei K iff k ? I and 1 ? I' and both xk and XL are in the intersection of dim(R&R') --H 1
facets of R&R'. Notice that 0: is an approximation operator, that 0: is not symmetric (i.e., R oc
R' and R' 0: R may be different), and that R&R' C R 0: R'. Figure 11 shows two convex
2-dimensional polyhedra R and R' and the extrapolation result R 0:
4.3 Two-way Iterative Approximation
Suppose that an approximate forward reachability analysis is inconclusive; that is, the overapprox-
imation S of the target region post*(S) contains some final states from T. if the intersection 5 n T
10
I I I
Figure 11: Extrapolation
exact forward/backward approximate forward
approximate backward
Figure 12: Single-pass exact and approximate analysis
is a proper subset of T, then we have nonetheless obtained new information--Hnamely, that the
states in T --H s ate not reachable from S--Hand we may proceed computing backward the new target
region pre* (T --H S), or an overapproximation T of pre* (T --H s). If Tn S = ?, then T is not reachable
from S; if, on the other hand, T does contain some initial states from S, then we may continue the
two-way iterative approximation process, this time computing forward from T n s [DW93].
The two-way iterative approximation strategy is illustrated in Figures 12 and 13, assuming a 2-
dimensional state space and convex-hull approximation. The two shaded boxes in the lower left
corner of the state space represent the initial region S; the two shaded boxes in the upper right
corner represent the final region T. The first derivatives of both variables x and y are 1. While
an exact forward or backward analysis shows that T cannot be reached from S, both approximate
forward analysis and approximate backward analysis are inconclusive (Figure 12). An approximate
forward analysis followed by an approximate backward analysis is successful (Figure 13).
We now apply the two-way iterative approximation strategy to analyze the bouncing-ball automaton
11
approximate forward			intersection with T			approximate backward
Figure 13: Two-pass approximative analysis
r=--H1
z=O
Figure 14: The bouncing-ball automaton
of Figure 14. The variable x represents the horizontal distance of the ball from a reference point,
the variable ? represents the distance of the ball from the floor, and the variable z represents the
"energy" of the ball. Suppose that the ball is dropped at the position x = 14 A y = 4 in the
direction of the reference point; that is, 5 = (Down A x = 14 A y= 4 A z = 0). While the ball is
falling (vertex Down),its energy is increasing (i= 1); when the ball hits the floor (y= 0), it loses
half of its energy and bounces back up (vertex Up); on the way up, the energy decreases (i= --H1)
until it becomes 0 and the ball starts to fall again. The trajectory of the ball is shown in Figure 15.
We wish to prove that the ball never reaches the region T = < 2 A y = 0) of the floor. First
notice that the exact forward computation of the target region post*(s) does not terminate, and
convex-hull approximation is of no help. If we use extrapolation, the? we obtain the overapproxima-
tion S of the target region post*(s),and S contains the final states SnT = (x = 2 A ? = 0 A z= 0).
Since pre(SnT) = 5 n T, a second, backward, pass terminates immediately without reaching the
initial state 5. HyTech requires 12 sec CPU time for both passes. (Notice that if we were to begin
with a backward pass, attempting to compute the target region pre* (T), neither the exact com-
putation, nor the approximate computation with convex-hull approximation, nor the approximate
computation with extrapolation would terminate.)
Acknowledgments. We thank Rajeev Alur, Limor Fix, and Nicolas Halbwachs for many stimu-
lating discussions, and Nicolas for his polyhedral library.
12
T SnT
x
Figure 15: A run of the bouncing-ball automaton
References
[ACH+94]
[ACHH93]
[AHH93]
R. Alur, C. Coucoubetis, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis,
and 5. Yovine. The algorithmic analysis of hybrid systems. In Analysis and Optimization
of Discrete Event Systems, Lecture Notes in Control and Information Sciences 199,
pages 331--H351. Springer-Verlag, 1994.
R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an al-
gorithmic approach to the specification and verification of hybrid systems. In R.L.
Grossman, A. Nerode, A.P. Ram, and H. Rischel, editors, Hybrid Systems, Lecture
Notes in Computer Science 736, pages 209--H229. Springer-Verlag, 1993.
R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded
systems. In Proceedings of the 14th Annual Real-time Systems Symposium, pages 2--H11.
IEEE Computer Society Press, 1993.
[BCM+92] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model
checking: 1020 states and beyond. Information and Computation, 98(2):142--H170, 1992.
[CC77]
[CES86]
[CH78]
[DW93]
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static
analysis of programs by construction or approximation of fixpoints. In Proceedings of
the Fourth Annual Symposium on Principles of Programming Languages. ACM Press,
1977.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state con-
current systems using temporal-logic specifications. A CM Iransactions on Programming
Languages and Systems, 8(2):244--H263, 1986.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of
a program. In Proceedings of the Fifth Annual Symposium on Principles of Programming
Languages. ACM Press, 1978.
D.L. Dill and H. Wong-Toi. Using iterative symbolic approximation for timing veri-
fication. In T. Rus, editor, Proceedings of the First AMAST Workshop on Real-time
Systems, 1993.
13
[Hal93]
N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor,
CAV 93: Computer-aided Verification, Lecture Notes in Computer Science 697 pages
333--H346. Springer-Veilag, 1993.
[HNSY94j T.A. Henzinger, X. Nicollin, J. Sifakis, and 5. Yovine. Symbolic model checking for
real-time systems. Information and Computation, 111(2):193--H244, 1994.
[HRP94] N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by
means of convex approximation. Unpublished manuscript, 1994.
[MMP92]
0. Maler, Z. Manna, and A. Pnueli. FYom timed to hybrid systems. In J.W. de Bakker,
K. Huizing, W.-P. de Roever, and 0. Rozenberg, editors, Real Time: Theory in Practice,
Lecture Notes in Computer Science 600, pages 447--H484. Springer-Verlag, 1992.
[N05Y93] X. Nicollin, A. Olivero, J. Sifakis, and 5. Yovine. An approach to the description and
analysis of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and II. Rischel, ed-
itors, Hybrid Systems, Lecture Notes in Computer Science 736, pages 149--H178. Springer-
Verlag, 1993.
[NW88] G.L. Nemhauser and L.A. Wolsey. Integer and Combinatorial Optimization. Wiley,
1988.
14
