BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1343
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Hybrid Automata: An Algorithmic Approach to the Specification and 
        Verification of Hybrid Systems
AUTHOR:: Alur, Rajeev
AUTHOR:: Courcoubetis, Costas
AUTHOR:: Henzinger, Thomas A. 
AUTHOR:: Ho, Pei-Hsin
DATE:: May 1993
PAGES:: 19
ABSTRACT::
We introduce the framework of hybrid automata as a model and specification 
language for hybrid systems. Hybrid automata can be viewed as a 
generalization of timed automata, in which the behavior of variables is 
governed in each state by a set of differential equations. We show that many 
of the examples considered in the workshop can be defined by hybrid automata. 
While the reachability problem is undecidable even for very restricted classes 
of hybrid automata, we present two semidecision procedures for verifying 
safety properties of piecewise-linear hybrid automata, in which all variables 
change at constant rates. The two procedures are based, respectively, on 
minimizing and computing fixpoints on generally infinite state spaces. We 
show that if the procedures terminate, then they give correct answers. We 
then demonstrate that for many of the typical workshop examples, the 
procedures do terminate and thus provide an automatic way for verifying their 
properties.
END:: CORNELLCS//TR93-1343
BODY::
Hybrid Automata:
An Algorithmic Approach to the Specification
and Verification of Hybrid Systems
Rajeev Alur*
Costas Courcoubetis**
Thomas A. Henzinger***
Pei-Hsin Ho***
TR 93-1343
May1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*AT&T Bell Laboratories, Murray Hill, NJ 07974.
**Institute of Computer Science, FORTH, and Department of Computer Science,
University of Crete, Heraklion, Greece. Supported in part by the BRA ESPRlT project
REACT.
***Department of Computer Science, Cornell University, Ithaca, NY 14853.
Supported in part by the National Science Foundation under grant CCR-9200794
and by the United States Air Force Office of Scientific Research under contract
F49620-93-1 -0056.
Hybrid Aiitomata:
An Algoritlimic Approacli to tlie Specification and Verification of
Hybrid Systems
Rajeev Alur' Costas Courcoubetis2 Thomas A. Henzinger3 Pei-Hsin Ho?
Abstract
We introduce the framework of hybrid antornala as a model and specification language for
hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which
the behavior of variables is governed in each state by aset of differential equations. We show that
many of the examples considered in the workshop can be defined by hybrid automata. While
the reachability problem is undecidable even for very restricted classes of hybrid automata, we
present two semidecision procedures for verifying safety properties of piecewise-tinear hybrid
automata, in which all variables change at constant rates. The two procedures are based,
respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show
that if the procedures terminate, then they give correct answers. We then demonstrate that
for many of the typical workshop examples, the procedures do terminate and thus provide an
automatic way for verifying their properties.
1 Introduction
More and more real-life processes, from elevators to aircrafts, are controlled by programs. These
r?active programs are embedded in continuously changing environments and must react to environ-
ment changes in real time. Obviously, correctness is of vital importance for reactive programs. Yet
traditional program verification methods allow us, at best, to approximate continuously changing
environments by discrete sampling. A generalized formal model for computing systems is needed
to faithfully represent both discrete and continuous processes within a unified framework. Hybrid
automata present such a framework.
A hybrid system consists of a discrete program within an analog environment. Hybrid automata
are generalized finite-state machines for modeling hybrid systems. As usual, the discrete transitions
of a program are modeled by a change of the program counter, which ranges over a finite set of
control locations. In addition, we allow for the possibility that the global state of a system changes
continuously with time according to the laws of physics. For each control location, the continuous
activities of the environment are governed by a set of differential equations. We label each location
also with an invariant condition that must hold while the control resides at the location, and each
transition is labeled with a guarded set of assignments. This model for hybrid systems is inspired
1AT&T Bell Laboratories, Murray Hill, NJ 07974.
2Institute of computer Science, FoRTH, and Department of computer Science, University of crete, Heraklion,
Greece. Supported in part by the BRA ESPRIT project REAcT.
3Department of computer Science, Cornell University, Ithaca, NY 14853. Supported in part by the National
Science Foundation under grant ccR-9200794 and by the United States Air Force 0ffice of Scientihc Research under
contract F49620-93-1-0056.
by the phase transition systems of [MMP92] and [NSY92], and can be viewed as a generalization
of timed automata [AD9Oj.
The current paper pursues three objectives. First, hybrid automata are defined and their
suitability for specification is demonstrated through some paradigmatic examples. Second, the
verification problem for hybrid automata is studied and shown to be intrinsically difficult even
under severe restrictions. Third, and most importantly, we successfully verify interesting properties
of truly hybrid system behaviors. We note that Nicollin et al. have independently developed an
approach similar to ours [NSOY].
For verification purposes, we restrict ourselves to linear hybrid automata. In a linear hybrid
automaton, for each variable the rate of change with time is constant though this constant may
vary from location to location and the terms involved in the invariants, guards, and assignments
are required to be linear. An interesting special case of a linear hybrid automaton is a timed
automaton [AD9oj. In a timed automaton each continuously changing variable is an accurate
clock whose rate of change with time is always 1. Furthermore, in a timed automaton all terms
involved in assignments are constants, and all invariants and guards only involve comparisons of
clock values with constants, Even though the reachability problem for linear hybrid automata is
undecidable, it is PSPACE-comNete for timed automata. In this paper, we show that some of the
algorithms for the analysis of timed automata can be extended to obtain semidecision procedures for
solving the verification problem for linear hybrid automata. In particular, we consider the fixpoint
computation method presented in [HNSY92] and the minimization procedure for timed automata
presented in [ACll+92j. Both methods perform a reachability analysis over the infinite state space
of a timed automaton by computing with sets of states, We show that the primitive steps of the
two algorithms can be performed relatively easily even in case of linear hybrid automata and, thus,
both methods can be generalized. The crucial observation is that each set of states computed by
the algorithms is definable by a linear formula; that is, it is a union of convex polyhedra. However,
as we move from timed automata to linear hybrid automata, the termination of the two procedures
is no longer guaranteed.
Both methods we consider can be used to prove invariant properties of linear hybrid systems.
We illustrate these methods on three examples, and in each case the procedures terminate, The
first example involves a water level monitor. It is a truly hybrid system, since the water level
increases and decreases continuously in phases. We show how to prove that the water level always
remains within the specified bounds. The second example proves the mutual exclusion property of
a real-time mutual exclusion protocol. Earlier algorithmic methods based on timed automata fail
when the bounds on the various delays are not known. ?`e show how to perform a symbolic analysis
so as to deduce constraints between the various bounds. Our third example involves leakage in a
gas burner. This is an example of a so-called integrator system in which we are required to prove
a bound on the ratio of two durations.
2 Modeling Hybrid Systems
We define a formal model and a specification language for hybrid systems.
2.1 Hybrid traces
An interval is a nonempty convex subset of the nonnegative real line R+. Intervals ma,y be open,
halfopen, or closed; bounded or unbounded. The left end-point of an interval 1 is denoted by Ii
and the right end-point, for bounded 1, is denoted by rj. Two intervals i?? and 12 are adjacent if
2
(1) ri1 = ?12, and (2) either li is right-open and 12 is left-closed, or li is right-closed and 12 is left-
open. An interval sequence %1112... is a finite or infinite sequence of intervals that partitions R+:
1. Any two neighboring intervals Ij and 1i+1 are adjacent.
2. For all t E R+, there is some interval 1? with t c
In particular, 1o is left-closed and 11o = 0. The last interval of any finite interval sequence is
unbounded. The interval sequence Ji refines the interval sequence `2 if Ii is obtained from J2
by splitting some intervals. We henceforth identify an interval sequence 1 with its refinement
closure ?7 I Y refines I?. Clearly, for any finite set 1 of interval sequences there is an interval
sequence fli that refines all sequences in 1.
Let V be a finite set of real-valued variables. A state is an interpretation of all variables in V.
We write ? for the set of states. A trace is a function from R+ to ?. Equivalently, a trace T is a
collection of functions r(x) from R+ to R, one for each variable x ? V. We say that the trace r
has property P if all of its constituent functions T(x), for x ? V, have property P. We will use the
following properties of functions:
o+ A function f: R+ H R is piecewise smooth if there exists an interval sequence I? --H 1_1 I_ ...
and a sequence foflf2... of C?-functions such that the restriction of f to each interval I?
coincides with the restriction of f? to I?. Each restriction of f to an interval I? is called a
phase of f. The phases of a piecewise-smooth trace T are the restrictions of T to the intervals
of the sequence TT --H flf?(X); r E VJ.
o+ A piecewise-smooth function f: R+ R is piecewise linear if each phase of f is linear.
o+ A piecewise-linear function f: R+ R is a step function if the slope of all phases of f is 1.
o+ A piecewise-linear function f: R is a clock function if the slope of all phases of f is 1.
o+ A piecewise-linear function f: R+ R is a skewed-clock function if there is some constant
k E R such that the slope of all phases of f is k.
o+ A piecewise-linear function f: R is an integrator function if the slope of each phase
off is either 0 or 1.
A timed trace T is a trace each of whose constituent functions T(x), for x ? V, is either a step
function or a clock function. A set S of traces is fusion-closed if for all traces T1, T2 E S and
all t1, t2 E R+, if T1(t1) = T2(t2), then T E S for the trace T with T(t) = Ti(t) for all t < t1 and
T(t) = r2(t + t2 --H t1) for all t > t1.
2.2 Hybrid automata
We model a hybrid system as fusion-closed set S of piecewise-smooth traces. Each trace T E S
represents a possible behavior of the system over real time. The piecewise smoothness of T ensures
that in any bounded interval of time, there are only finitely many discontinuous state changes.
The fusion closure of S ensures that each state contains ali information necessary to determine the
future evolution of the system.
We define sets of traces by graphs whose edges represent discrete transitions and whose vertices
represent continuous activities. A hybrid system A = (VD, Q,?1,[?2,tL3) is given by six components:
3
o+ A finite set VD of real-valued data variables. A data state is an interpretation of all variables
in VD. We write ?D for the set of data states.
A finite set Q of vertices called locations. We use the variable Pc ? VD as a control variable
that ranges over the set Q of locations (properly encoded in R), and let V = (pci U VD.
Thus, ? = Q x ??; that is, a (system) state is a pair (?, a) consisting of a location -? ? Q and
a data state a E ?D
o+ A labeling function ?i that assigns to each location in Q a set of possible activities. Each
activity is a C?-function from R+ to ?D
A labeling function j? that assigns to each location ? ? Q an exception set jt2(?) C ?D The
system control must leave location `before an exception ?2(?) occurs. The complement ?D
?2(?) is called the invariant of the location .
A labeling function ?? that assigns to each pair e e Q2 of locations a transition rela-
tion ?3(e) C ?D2 We require that for all locations `, ? Q and all data states a E ?D,
(a, a) E [t3(?, ?). The state (a', `) is called a successor of the state (, a) iff (a, a') E [t3(, C).
At any time instant, the state of a hybrid system specifies a control location and values for all data
variables. The state can change in two ways: (1) by an histantaneous transition that changes the
entire state according to the successor relation, and (2) by elapse of time that changes only the
values of data variables in a continuous manner according to the activities of the current location.
The exceptions of a hybrid system enforce the progress of the underlying discrete transition system:
some transition must be taken before an exception occurs. Typical exceptions are timeouts and
sensor readings that trigger a discrete state change.
Formally, a run of the hybrid system A is a finite or infinite sequence
p: ??? (?o,Io,fo) CT?? ??1 (i,Ii,fi) ??? a2 (?2,I2,f2) ?2'
of data states Q, a? E ?D locations ?j ? Q, intervals j?, and activities f? such that
1. for all ? > 0 the state (?i+i, a?+1) is a successor of the state (?j, a?');
2. 101112... is an interval sequence;
3. for all i > 0 the activity f? is in ?i('j), and (1) fj(O) = Q and
f?(rj --H 1A) = a?', and (2) for all t E Ii, fi(t --H 4?) ?
Each run p of A uniquely determines a trace 7?: for all i > 0 and t ? I?, let T(t) = (?j,f?? 1A))
Observe that, for all i > 0, if I? is left-closed, then the state at time 1A? that is, at the time of
transition from state a' 1 to state Q, is defined to be ?. On the other hand, if I? is left-open, then
the state at time 1A is defined to be a??1.
By SA we denote the set of all traces rp that correspond to runs p of the system A. The
set SA is fusion-closed, because at any time instant during a run, the configuration of the system
is completely determined by the location in which the control resides and the values of all data
variables.
4
Linear hybrid systems
A linear term Q over a set of variables V is a linear combination of the variables ill V with rational
coefficients. A linear formula ? over V is a boolean combination of inequalities between linear
terms over V.
The hybrid system A (VD, Q, ?1, t2, ??) is linear if its activities, exceptions, and transition
relations can be defined by linear expressions over the set VD of data variables:
1.
For all locations ? Ei Q,the possible activities are linear functions defined by a set of differential
equations of the form x' = kx, one for each data variable x E VD, where kx is a rational
constant:
f e ??() iff all t E R+ and x e VD, f(t)(x) = f(O)(r) + kx?t.
We write ?i(, x) = kx to define the activities of the linear hybrid system A.
2. For all locations ? E Q, the exception is defined by a linear formula ? over V?: a E ii2(?) iff
3. For all pairs e E Q2 of locations, the transition relation ji3(e) is defined by a guarded set of
assignments
I x E VDY,
where ? is a linear formula over VD and each a? is either a linear term over VD or
(a, a') E i3(e) iff a(? and for all x E VD, either ci --H? or
An assignment of the form x :=? indicates that the value of the variable x is changed nonde-
terministically to an arbitrary value. We write jt3(e, x) for the term ?x
Various special cases of linear hybrid systems are of particular interest:
0
0
0
0
If ?i(, x) = 0 for each location  ? Q, then x is a discrete variable. Thus a discrete variable
changes only when the location of control changes. A discrete system is a linear hybrid system
all of whose data variables are discrete variables.
A discrete variable x is a proposition if ?3(e, x) ? (0, lJ for all pairs e ? Q2. If all the data
variables are propositions, then a linear hybrid automaton is same as a finite-state system
whose states are labeled with propositions.
If ?i(?,x) = 1 for each location ? and ?3(e,x) ? (O,x? for each pair e e Q2, then x is a
clock. Thus the value of a clock variable increases with time uniformly; a transition of the
automaton either resets it to 0, or leaves it unchanged. A (finite?state) timed system is a
linear hybrid system all of whose data variables are propositions and clocks.
If there is a constant k ? R such that tii(, x) = k for each location  and jt3(e, x) Ei (0, x?
for each pair e E Q2, then x is a skewed clock. Thus a skewed clock is similar to a clock
variable except that it changes with time at some (fixed) rate different from 1. A multirate
timed system is a linear hybrid system all of whose data variables are propositions and skewed
clocks. An fl-rate timed system is a mukirate timed system whose skewed clocks proceed at
n different rates.
5
ffl;
x= 10
Figure 1: Graphical representation
li?1(,x) E ?0,1Y for each location  and ?3(e,r) E f0,x? for each pair e E Q2, then xis
an integrator. Thus an integrator is like a clock that can be stopped and restarted, and can
measure accumulated durations. An integrator system is a linear hybrid system all of whose
data variables are propositions and integrators.
A discrete variable is a parameter if jt3(e, x) = x for all pairs e E Q2. Thus a parameter is
a symbolic constant which can be used, for instance, in the guards of the transitions. For
different special types of linear hybrid automata defined above, we can define its parameterized
version also. For instance, a parameterized timed system is a linear hybrid system all of whose
data variables are propositions, parameters, and clocks.
Clearly, if A is linear (discrete; tin?d; multirate timed; integrator) system, then all traces in SA
are piecewise linear (step traces; timed traces; skewed-clock traces; integrator traces, respectively).
Graphical representation
Instead of using exceptions, we label locations with their invariants. We suppress location labels
of the form x' = 0 for activities and true for invariants. For transition labels, we suppress the
guard true and assignments of the form x := x. Reflexive transitions with the label true are
suppressed altogether.
As an example, consider the linear hybrid system of Figure 1 with the single data variable r.
This system has two locations, i and 2 In location i, the value of x decreases at a constant rate
of 1. The transition from i to 2 may be taken at any time after the value of x has fallen below 6,
and it must be taken before the value of x falls below 5. When the transition is taken, the value
of x is instantaneously decreased by 1. Once in location 2, the rate of x starts to increase at the
constant rate of 2. The transition back to location i is taken exactly when the value of x hits 10.
Indeed, at the very time instant when x = 10, the control of the system is already in location i,
because location 2 has the invariant x < 10.
Initial and acceptance conditions
We can turn a hybrid system A into an automaton by adding initial and acceptance conditions.
The initiality criterion is given by a labeling function ?? that assigns to each location  e Q an
initial condition [t4() ? ?D The Muller acceptance criterion is given by a collection P c 2Q of
acceptance sets of locations. The run p (t) of the hybrid Muller automaton (A,?4, F) is accepting
if
4. cTo E tt?(o);
5. either p is finite with final location ? and fn? ? F, or Poo E P for the set p0o of locations that
are visited infinitely often during p (i.e, Poc is the set f (= ? for infinitely many i >
6
The hybrid automaton (A,?4, P) is linear if A is a linear hybrid system and for all locations  E Q,
the initial condition is defined by a linear formula ? over VD (i.e., a E ii?() iff a(?)).
Parallel composition
A hybrid system typically consists of many components operating concurrently and coordinating
with each other. Such a system can be constructed from the descriptions of its components using
a product operation. Let A1 = (VA,Q1,?t,?21,?) and A2 = (VA,Q2,?21,it22,tt32) be two hybrid
systems. The product A1 x A2 of A1 and A2 is the hybrid system (VA u VA,Q' x Q2,?1,Jt2,?3)
such that
o+ An activity f belongs to [t1('1,?) iff the restriction off to the data variables VA, denoted
by fIvD1? is in ?l(?), and fIvD2 isin ?2?(?);
o+ A data state a over VA u VA is in tL2(1, ?2) iff ?Iv?l the projection of a onto the variables
VA, is in ?21(1), or is in ??2(2);
o+ (a, a') ? j3((1,?2),('1,'2)) iff(alv?l?a'lv?l) ? jt3(1,?'1) and (aIv?2?a'Iv?2) e jt3(2,t2).
It is not hard to see that traces of the product system are precisely those hybrid traces whose
projections are traces of the component systems. It follows that the product of two linear hybrid
systems is again linear, etc. An accepting run of a product automaton must meet the initial and
acceptance conditions of both component automata.
2.3 Examples of hybrid systems
We model a thermostat, a water level monitor, a clock-based mutual-exclusion protocol, and a
leaking gas burner as hybrid systems.
Temperature controller
Our first example describes a nonlinear hybrid system. The temperature of a plant is controlled
through a thermostat, which continuously senses the temperature and turns a heater on and
off [NSY92j. The temperature is governed by differential equations. When the heater is off, the tem-
perature, denoted by the variable x, decreases according to the exponential function x(t) =
where t is the time, 0 is the initial temperature, and K is a constant determined by the plant;
when the heater is on, the temperature follows the function x(l) --H 0e?Kt + A(l --H e?K?), where
h is a constant that depends on the power of the heater. Suppose that initially the temperature
is M degrees and the heater is turned off. ?`e wish to keep the temperature between m and M
degrees. The resulting system can be described by the hybrid automaton of Figure 2 (note the
representation of the initial condition x = M). The automaton has two locations: in location ?,
the heater is turned off; in location 1, the heater is on.
Water level monitor
Our next example describes a linear system. The water level in a tank is controlled through a
monitor, which continuously senses the water level and turns a pump on and off. Unlike the
temperature, the water level changes as a piecewise-linear function over time. When the pump is
off, the water level, denoted by the variable y, falls by 2 inches per second; when the pump is on,
the water level rises by 1 inch per second. Suppose that initially the water level is 1 inch and the
7
x=M
Figure 2: Temperature controller
y='			y<lO			y=lO?x:=O			x<2
x=2
ffiMS21 y=5			x:=O 4fflc??
Figure 3: Water level monitor
pump is turned on. We wish to keep the water between 1 and 12 inches. But from the time that
the monitor signals to change the status of the pump to the time that the change becomes effective,
there is a delay of 2 seconds. Thus the monitor must signal to turn the pump on before the water
level falls to 1 inch, and it must signal to turn the pump off before the water level reaches 12 inches.
The linear hybrid automaton of Figure 3 describes a water level monitor that signals whenever
the water level passes 5 and 10 inches, respectively. The automaton has four locations: in loca-
tions ? and 1, the pump is turned on; in locations ? and ?, the pump is off. The clock x is used
to specify the delays: whenever the automaton control is in location ?i or ?, the signal to switch
the pump off or on, respectively, was sent x seconds ago. In the next section, we will prove that
the monitor indeed keeps the water level between 1 and 12 inches.
Mutual-exclusion protocol
This example describes a parameterized multirate timed system. ?`e present a timing-based algo-
rithm that implements mutual exclusion for a distributed system with skewed clocks. Consider an
asynchronous shared-memory system that consists of two processes P1 and P2 with atomic read
and write operations. Each process has a critical section and at each time instant, at most one of
the two processes is allowed to be in its critical section. Mutual exclusion is ensured by a version
of Fischer's protocol [Lam87J, which we describe first in pseudocode. For each process Pj, where
t = 1,2:
8
x>bAk<>I
k:=O
y> bA k<>2
k=O?y:=O			y<a			?=2;y:=O
0
Figure 4: Mutual-exclusion protocol
repeat
repeat
await k = 0
k
delay b
until k =
Critical section
k := 0
forever
The two processes P1 and P2 share a variable k and process Pi is allowed to be in its critical
section iff k = i. Each process has a private clock. The instruction delay b delays a process for
at least b time units as measured by the process's local clock. Furthermore, each process takes
at most a time units, as measured by the process's clock, for a single write access to the shared
memory (i.e., for the assignment k := i). The values of a and b are the only information we have
about the timing behavior of instructions. Clearly, the protocol ensures mutual exclusion only for
certain values of a and b. If both private processor clocks proceed at precisely the same rate, then
mutual exclusion is guaranteed iff a < b.
To make the example more interesting, we assume that the two private clocks of the processes P1
and P2 proceed at different rates, namely, the local clock of P2 is 1.1 times faster than the clock
of P1. The resulting system can be modeled by the product of the two hybrid automata presented
in Figure 4.
Each of the two automata models one process, with the two critical sections being represented
by the locations 4 and D. The private clocks of the processes P1 and P2 determine the rate of
change of the two skewed-clock variables x and y, respectively. In the next section, we will prove
that mutual exclusion is guaranteed if a = 2 and b = 3: in this case, it will never happen that the
control of P1 is in location 4 while the control of P2 is in location D.
Leaking gas burner
Now we consider an integrator system. In [CHR9tj, the duration calculus is used to prove that a
gas burner does not leak excessively. It is known that (1) any leakage can be detected and stopped
within 1 second and (2) the gas burner will not leak for 30 seconds after a leakage has been stopped.
We wish to prove that the accumulated time of leakage is at most one twentieth of the time in any
9
y'= 1			_			y'= 1
3O<x? x:=O
Figure 5: Leaking gas burner
interval of at least 60 seconds. The system is modeled by the hybrid automaton in Figure 5. The
automaton has two locations: in location i, the gas burner leaks; ? is the nonleaking location.
The integrator I records the cumulative leakage time; that is, the accumulated amount of time
that the system has spent in location i. The clock x records the time the system has spent in
the current location; it is used to spedfy the properties (1) and (2). The clock y records the total
elapsed time. In the next section, we will prove that y > 60 201 < y is an invariant of the
system.
2.4 Undecidability of verification
The design of verification algorithms for hybrid systems is impaired by the fact that the emptiness
problem ("Does a hybrid system have a run?") is undecidable already for very restricted classes of
systems. On the positive side, the emptiness problem for timed automata (only propositions and
clocks) is PSPACE-complete [AD9oj. On the negative side, the emptiness problem is undecidable
for asynchronous timed systems (propositions and skewed clocks that proceed at different rates)
and for integrator systems (propositions and integrators).
To obtain strong undecidability results, we restrict the classes of multirate timed systems and
integrator systems further. A linear hybrid system is simple if all linear atoms in exceptions and
transition guards are of the form x < k and all assignments are of the form x := x or x :=
for x E VD and k E Z. In particular, for fl-rate timed systems the simplicity condition prohibits
the comparison of clocks with different rates.
Theorem 1 The emptiness problem is undecidable for 2-rate timed systems and for simple inte-
grator systems.
Proof. The first part of the theorem follows from the undecidability of the halting problem for
nondeterministic 2-counter machines (NCMs). Given any two distinct clock rates, a 2-rate timed
system can encode the computations of an NCM. Suppose we have three "accurate" clocks of rate 1
and two skewed clocks x1 and r2 of rate 2. Then we can encode the values of two counters in the
i-th machine configuration by the values of x? and r2 at accurate time `i: the counter value n is
encoded by the clock value l/2?.
The accurate clock y is reset whenever it reaches 1 and thus marks intervals of length 1. It is
obvious how a counter can be initialized to 0 and tested for being 0. Ilence it remains to be shown
how a counter can be incremented and decremented. To increment the counter represented by the
skewed clock x from time i to time i + 1, start an accurate clock z with x in the interval [i --H 1, i)
and reset z when it reaches 1; then nondeterministically reset x in the interval [i, i + 1) and test
x = z at time i + 1. To decrement the counter represented by the skewed clock r from time i to
time ? + 1, nondeterministically start an accurate clock in the interval [`i --H 1, i) and test x = z at
10
time i; when z reaches 1 in the interval [?,i + 1), reset x. Given an NCNI Al, we can so construct
a 2-rate timed system that has a run 1ff Al halts. (Indeed, using acceptance conditions, we can
construct a 2-rate timed automaton that has a run iff a counter is 0 infinitely often along some run
of M; this shows that the emptiness problem is ?1? complete for 2-rate timed automata [HPS83].)
The seconQpart of the theorem follows from an undecidability result for timed systems with
memory cells [Cerans].I
We point out that the emptiness problem is decidable for simple fl-rate timed automata. This is
because any simple asynchronous timed automaton can be transformed into a timed automaton by
(1) factoring into i-process timed automata, (2) scallng all i-process timed automata to the same
clock rate, and (3) constructing the product. An analogous result holds for real-time temporal
logics [WMF92].
3 Verification Procedures
Consider a ilnear hybrid system A = (VD, Q?!i1?!t2,?3) Given a linear formula ? over VD, we wish
to determine whether ? is an inVariant of A:
"Is ? true in all states that occur on some trace of A?"
Recall that ? = Q X ?D is the state space of A. We define the following read'ability relations
between states:
Time step. For all locations  E Q and data variables r ? VD, let ?1(?, x) = kx and let jt?(?) =
?. For all data states a E ?D and nonnegative reals 6 E R+, define (a + 6) ? ?D to be tile
data state that assigns to each data variable x e VD the value a(x) + 6'kx. Then ?t C ?2is
the smallest relation such that
if ?(a + 6')(?) for all 0 ? 6' < 6. then (, a) ?i (, a + 6);
? ?2 is the smallest relation such that
if ?(a + 6')(?) for all 0 < 6' < 6 then (?, a) ?? (, a + 6);
and ?& ? ?2 is the smallest relation such that
if ?(a + 6')(?) for all 0 < 6' < 6 then (`, a) ?t? (?, a + 6).
In other words, ?? = ?t A ??.
o+ Transition step. The relation ? ? "`2 is the smallest relation such that for all pairs (-C, C) ? Q2
and all data states a1,a2 ?
if (a1, a2) E jt?(, ?`), then (?, a1) ? (?`, a2).
Note that the relation ? is reflexive.
o+ Single step. For all states a1,a2 e ?,
a1 ? a2 iff there exist a11,a2, ? ? with either a1 ?? a'1 ? a21 ?T a2 or a1 ??
a11 ? a21 ?? a2.
o+ The reachability relation ?* ? ?2 is the transitive closure of the single-step relation ?.
11
The single-step reachability relation can be extended to sets of states. For a state a E "` and a
set 1? C V? of states, let a ? I? iff a ? a' for some a' ? I?; for two sets 1?1, J?2 C "2 of states, define
? B2 iff a ? 1?2 for some a C Ri. Again, ?? denotes the transitive closure of ?.
Given two sets Ri, Rj C ? of states, we wish to find out if the reachability relation Rj ? Rj
holds. A solution to this reachability problem allows the verification of safety properties of the
hybrid system A. Suppose the initial condition is given by the labeling function ij?, then take Rj to
be the set defined by (?, a) E Ri iff a E ti4(?). To check whether a linear formula ? is an invariant
of A, we consider the set Rf of "bad" states: a ? Rj iff ??(a). Now ? is an invariant iff the
readiability relation Ri ?? Rj does not hold.
From the undecidability of the emptiness problem, it follows that the reachability problem is
undecidable for linear hybrid automata. As the state space ? of A is generally infinite, we will
attempt to work on a quotient of the state-transition graph (?, ?). Our method will succeed
only if there is a finite quotient of the state space in which states are identified whenever they are
equivalent" with respect to the given reachability problem (Ri, Rj). This problem can be attacked
in many different ways:
We can choose from two definitions of state equivalence. We can move "forward" from the
initial set Ri and identify two states whenever they can be reached from Ri by the same
sequence of single steps. Alternatively, we can move "backward" from the final set R? and
identify two states whenever they can reach R; by the same sequence of single steps.
Working forward from Ri (backward from R;), we can choose to add one equivalence class
of states at a time until either the current set intersects with Rj (or Ri, respectively) or
no new states can be added. We refer to this category of verification methods as fixpoint
methods, because the computation can be viewed as the iterative approximation of a fixpoint
that defines the class of reachable states.
Alternatively, we can start with an initial partition of the state space and refine it until it
respects the equivalence relation, and thus can be used for checking reachability. The verifi-
cation methods in this category are called minirnization methods, because the computation
can be viewed as constructing a bisimulation relation, namely, the minimal (coarsest) state
partition that respects single-step reachability.
Iii this paper, we present one instance of the fixpoint computation approach and one instance of
the minimization approach. Both procedures rely on the same set of primitive operations.
3.1 Fixpoint computation
We define a backward fixpoint computation procedure that solves the reachability problem (Ri, Rj)
provided it terminates. The procedure starts with the set Rc?r Rj and repeatedly adds states
from which any state in Rc?r can be reached. The procedure terminates with the answer YES
(indicating that Rj is reachable from Ri) if at some stage an initial state in Ri is added, and it
terminates with the answer NO if no new states can be added. The procedure may, of course,
not terminate at all; it is a semidecision procedure for the reachability problem of linear hybrid
systems.
12
Backward fixpoint computation:
R0id ?; Rcwr := Rj
while Rcit? A Rj = ? and Rcnr ? 110id do
R := pre(R??)
R0id := R0id U Rc??; Rc?r R
od
return Rc? A Ri # ?.
The crucial step is the computation of the state set
pre(R) = fa E ? a ?
This computation is possible due to the fact that all state sets encountered by the procedure are
definable by linear formulas, and hence, for two state sets R and I?', the problems of deciding
whether R C R' and whether R A R' = ? have Jgorithmic solutions, A data region 1?D C ? is a set
of data states of the form fa E ?D a(?)?, for some linear formula (t)over VD. A region (?, RD) C ?
consists of a location ? E Q and a data region RD. The union R C V of regions (?, R?), one for
each location ` E Q, is called a region family. The following central frmma ensures that for linear
hybrid systems, all required state sets are computable:
Lemma 1 If R C V is a region family, then so is pre( 1?).
Proof. It suffices to show that if RD is a data region, then so is the set
pre0(RD) = fa E ?D (?,a) ?
for each pair e = ("`i, ?) of locations. Let `? be the linear formula that defines RD. ??e construct a
linear formula pre0(?) that defines the set Pree(RD) If y contains n variables, we can think of ?
as defining a set of points in n-dimensional space. This set is an n-dimensional polyhedron whose
bounding hyperplanes are linear functions with rational coefficients.
First let us extend the time-step and transition-step relations to linear formulas. For any linear
formula ? and location ? of A:
= fa E ?D ?a' e vD.(?(a) A
(? ?) = fa E ?D I aa' ? ?2D (?(a) A (, a) (, a"))1
for ?E f?i, ?T? ?&J' Then the linear formula Pree(?) is the following disjunction:
pree(?) = ?& (?i, ?(e, ?r (2 ?))) V ?? (i, ?(e, ?ir (t2, ?))).
The transition-step relation ? can be computed by substitution. Let ? be the guard of jt?(e) and
for all x ? VD, let ?3(e,?) = ??. Then:
?(e, ?) = 4) A (?[x :=
where the linear formula 4)[x := o?] is obtained by replacing all occurrences of x in 4) with ??.
The time-step relations can be computed by quantifier elimination. For all locations  of A, let
= 4)?. If ti(, x) = kx for all x E VD, then the linear formulas y+ 6 and 4) --H? 6 result from 4)
by replacing all occurrences of x with x + kx.6 or x --H kx'6, respectively. Then:
?r (,4)) = (?6> O.(4) A ?4)t)+t6 A VO < ? r 6.?4)? +?c),
13
?` (,?) = (%[` A ?o'c) v (?6 > O.$+?6 A VO < E < &??+e),
and ?1r (?, t") = ??? A ?? (, ?). It remains to be shown how the quantifiers can be elimi-
nated from these formulas. We first convert all quantifiers into existential form and translate all
quantifier-free subformulas into disjunctive normal form. Since existential quantifiers distribute over
disjunction, it suffices construct a linear formula over V that is equivalent to the formula ?6 E R. y,
where ? is a conjunction of linear inequalities over V u t61. Note that the formula ?6. y defines a
convex rational polyhedron. To eliminate the existential quantifier, (1) solve all inequalities for 6
and (2) construct the conjunction of all 6-free inequalities that are implied by transitivity. 1
As for timed systems [HNSY92], the fixpoint method can be extended to check properties of
linear hybrid systems that are specified in real-time extensions of branching-time logics such as CTL.
3.2 Minimization
Let ? be a partition of the state space Z into regions. A region I? ? ir is stable if
VI?' ? r.(R? B' implies Va ? R.a ? 1?').
The partition ir is a bisimuThtion if every region of ir is stable. The partition ir respects 1?? if for
every region R E ir, either R C llj or I? A = ?. Observe that if a partition ir that respects l?j
is a bisimulation, then it can be used for rea4?ability analysis: to see if l?j is reachable from Rj,
check if there exists a path from some ir-region Ri such that R1 A R? # ? to some ir-region R2 such
that R2 C l?j. Our objective is to construct the coarsest bisimulation provided it is finite. For
this purpose, we can adopt algorithins for performing a simultaneous reachability and minimization
analysis of transition systems [BFll9O, LY92].
The minimization procedure of [BFH90] is given below. Let ro = f(?, true)  Q? be the
initial partition of ? into regions one region per location. The initial partition is refined into
= iro A fflj, ? --H Rj? so that it respects Rj.
Minimization:
a := fifl R? # :=
while a ? P do
choose 1? ? (a --H 3)
let a' := split(1?,ir)
ifa' = tRY then
P:=Pu(RJ
a := a U (1?' E ir 1? ?
else
Ii
a := a --H tRY
if ?R' E & such that 1?' A ll? # ? then a := a 1) (R'J fi
3 --H fR' E ir R' ?
ir := (ir --H (RJ) u a'
od
return there is 1? E a such that R C Rj.
Starting from ri, the procedure selects a region R and checks if I? is stable with respect to the
current partition; if not, then 1? is split into smaller regions. Additional book-keeping is needed
14
to record which regions are reachable from the region containing the initial state. In the following
procedure, r is the current partition, 0 is the set of 7r-regions that have been found reachable
from (the region of) the initial state, and P is the set of ir-regions that have been found stable
with respect to r. The function spiit(B, 7r) splits the r-region R into subregions that are "more"
stable with respect to 7r: split(1?, 7r) := (11', 1? --H R'i if there is some region R" E r such that the
region R' = pre(R") fl 1? is a proper subset of R, and spiit(J?,r) := ?1?J otherwise. Since the
operation split is computed using pre, all state sets encountered by the minimization procedure are
again definable by linear formulas. The procedure terminates if the coarsest bisimulation has only
a finite number of equivalence classes.
If the minimization procedure terminates, we obtain a finite bisimulation of "` with respect
to =>. As with timed automata [ACH+92], the resulting reachability graph can be used to solve also
the emptiness problem for A, even in presence of acceptance conditions, and for model checking
branching-time properties. The minimization procedure may be replaced by the more efficient
procedure presented in [LY92], which can also be implemented using the primitive pre
3.3 Verification examples
In the following, we demonstrate that both the fixpoint computation procedure and the miMmiza-
tion procedure terminate in many cases.
Minimization: water level monitor
Let A be the hybrid automaton defined in Figure 3. We use the minimization procedure to prove
that the formula 1 < y < 12 is an invaflant of A. It follows that the water level monitor keeps the
water level between 1 and 12 inches.
By (??, for a linear formula ? over V, we denote the set of all states (?, a) such that a satis-
fies ?[pc := j. Let the set ft? of iMtial states be so defined by
Ri = (pe = 0 A x = 0 A y =
and let the set Rj of "bad" states be defined by
Rj = (y' < 1 v y> 12).
The initial partition is ro = f(?, ?rue)  e ?o,?1,2, &)?. We next partition each region of the
initial partition into "good" and "bad" states: ri =
Coo			=			(pc			=			0 A			1 ? y < 12),			Coi			=			(pe = 0			A (y <			1 v			y> 12)),
Cio			=			(pe			=			1 A			1 < y < 12),			Cii			=			(pe = 1			A (y <			1 v			y> 12)),
C2o			=			(pc			=			2 A			1 < y < 12),			C21			=			(pe = 2			A (y <			1 v			y> 12)),
C3o			=			(pc			=			3 A			1 < y < 12),			C31			=			(pe = 3			A (y <			1 v			y> 12))y.
The bad states are in the regions Ci1, for `i ? i0,1,2,3?. Since the initial region Rj is contained
in C00, let a = ?C00J. Considering II = C00 ? 0, we find that split(C00,r1) = f
Cooo			=			(pc = 0 A 1 < y < 10),
C001			=			(pc = 0 A 10 < y ?
Therefore, r2 = fC000, C001, C01, C10, C11, C20, C2i, C30, C31?. Now Ri C C000, so take a = ?Coo,oJ
and p = ?. Considering R = C000, we find that it is stable with respect to r2. Thus a = a U (R e
15
1? ? = ?Cooo, Cooi, 010i and ,3 = f0ooo?. Since R = C,o01 is also stable in "`2 and is not
reaching any new states not in ?, ? remains the same and 3 = ?Cooo, Cooii. However, considering
R = C10, we obtain sph't(010,r2) =
0ioo = (pc = 1 A 0 ? x ? 2 A 1 ? y ? 12),
Cioi = (pc = 1 A x> 2 A 1 < y <
These two regions together with the regions in "`2? except for C10, constitute 7r3. The new 73 is
obtained by removing ?R' E 7r 1?' ? = 0ooo from the old 73. The new ? becomes ?Cooo, Cooij.
Now R = Cooo is stable in 7r3. Hence ? = ?0ooo, C001, C100J and 73 = ?Cooo, Cooli. Since ?I? = Cioo
is stable in 7r3, we have a = ?Cooo,000i,0100,01o1,C2oY and 73 = fCooO,0001,0100Y. R = C101 is
also stable in 7r3, 50 73 = ?Cooo, C001, C100, 0101? and a remains unchanged, Considering II = C20,
we obtain spiil(C20, "`3) =
C2oo			=			(pe = 2 A 5 ? y < 12),
0201			=			(pc = 2 A 1 < y ?
Now 7r4 contains C200 and C201, and thus C100 must be reconsidered. It is split into sph?(C100, 7r4) =
C1000 = (pc = 1 A 0 ? x ? 2 A 3 ? y ? 12 A 3 < y --H x < 12),
C1001 = (pc = 1 A 0 < x < 2 A 1 ? y < 5 A 1 < y --H x ?
Thus "`5 contains C1000 and C1001. After finding that C000, C1000 and C200 all are stable, we finally
have a = ?Cooo, C001, C1000, C200, C201, 030i and 73 = f0ooo, C001, 01000, 0200?. So let 1? = C201. It
is stable, so 73 = 73 u fC2oo? and a does not change. Then II = C30 is partitioned into ?
C300 = (pc = 3 A 0 ? x ? 2 A 1 < y ? 12).
0301 = (pc = 3 A x > 2 A 1 < y <
0200 has to be considered again. It is stable with respect to the current partition. Then 1? = 0300
is considered and split(C300, "`6) = f
03000 = (pc = 3 A 0 ? x < 2 A 1 <y < 12 A 5 < y + 2x ? 14).
03001 = (pc = 3 A 0 ? x ? 2 A 1 < y ? 5 A 1 ? y + 2x <5)?.
We must consider 0200 again. It turns out that it is still stable. After considering R = 03000, we
have 73 = fCooo, Cool, 01000, 0200, 0201, 03000J and a = a U f0oooY. Now the partition is
"`7 =
(Cooo, 0001, Coi, 01000,01001,0101, Cii,
0200,0201, 021,03000,03001,0301, 031i.
Since Cooo is stable in "`?, we have a --H 3 --H ?0ooo, Cool, 01000, 0200, 0201, 03000Y. Notice that no
region in a contains any bad states from 1?;. Therefore, the invariant property has been verified.
Fixpoint computation: mutual-exclusion protocol
Let A be the product of the two hybrid autoinata defined in Figure 4, for a = 2 and b = 3. We use
the fixpoint computation procedure to prove that the formula PC $ (4, D) is an invariant of A. It
follows that the protocol ensures mutual exclusion.
16
Let ll? = (pc = (1, A)? be the region of initial states and let i?j = (pc = (4, D)) be the region
of "bad" states. Let R? denote the value of II = pre(R???) after the ?-th iteration of the algorithm.
Then ftO --H Bj and
J?1 = pre(R??) = ((PC1 = 3 A pc2 = D A 1 = k) v (pc1 = 4 A PC2 = C A 2 =
where PCj, for ? = 1,2, denotes the i-th component of the control variab? pc. N\7e keep computing
11i+1 = pre(J?i) as long as l?? and i?? are disjoint:
J?2 =
R3 -
R4 =
J?5 =
J?6 =
((PC1 = 2 A PC2 = D A x <2;) v (PC1 = 4 A PC2 = B A ? < 2)
v (PC1 = 3 A PC2 = B A y < 2 A 13 < lix --H 10 y A 1 =
v(PC1 = 2 A PC2 = C A x <2 A 8< --Hltx + lOy A 2 =
v (PC1 = 2 A PC2 = C A x <2 A 30 < l0y A 2 =
v (PC1 = 3 A PC2 = B A y < 2 A 3 < x A 1 =
((PC1 = 1 A PC2 = D A 0 = k) v (PC1 = 4 A PC2 = A A 0 =
V (PCi = 2 A PC2 = C A 2 = k A x < 2 A 8 < --Hlix + lOy)
V (PCi = 3 A pC2 = B A 1 = k A y < 2 A --H20< --HlOy A 13 < lix --H loy)
V(pC1 = 2 A pC2 = B A x <2 A y <2 A 13< --HlOy))
((PC1 = 4 A pC2 = D) v (PC1 = 3 A pC2 = D A 0 =
V (PC1 = 4 A pC2 = C A 0 = k) v (pe1 = 3 A pC2 = D A 1 =
V (PC1 = 4 A pC2 = C A 2 =
V (PC1 = 2 A pC2 = A A 8 < --H11x A 0 =
V (PC1 = 2 A ?C2 = B A y < 2 A 8 < --H11x)
V(pC1 = 2 A pC2 = B A x <2 A y <2 A 13< --HlOy)
V(pC1 = 1 A pc2=B A 0=k A y<2 A 13< --HlOy))
((PC1 = 3 A pc2 = D A 1 = k) v (pc1 = 4 A pc2 = C A 2 =
V (PC1 = 2 A pC2 = D A x <2) v (pc1 = 4 A pC2 = B A y < 2)
V (PC1 = 2 A ?C2 = A A 8< --H11x A 0 =
V(pC1 = 1 A pC2 = II A y <2 A 13< --HlOy A 0 =
V(pC1 = 2 A pC2 = C A 8< --H11x A 38< --H11x+ lOy A 0 =
V(pC1=3 ApC2=B A y<2 A 13<11x--H10yA i=k)
V (PC1 = 3 A pC2 = B A y < 2 A 3 < x A 1 =
V(pC1 =2 A pc2=C A x<2 A 8< --H11x+10y A 2=k)
V (PC1 = 2 A pC2 = C A x <2 A 3 < y A 2 =
V(pC1=3 Apc2=B A y<2 A 13<--H10yA 46<11x--H10yA 0=k))
((PC1 = 1 A ?C2 = I? A 0 = k) v (ApC1 = 4 A ?C2 = A A 0 =
V (PC1 = 2 A pC2 = D A x <2) V (PC1 = 4 A pC2 = B A y < 2)
V (PC1 = 2 A pC2 = C A 8 < --Hlix A 38 < --H11x + 10 y A 0 =
V(pC1=3 Apc2=B A y<2 A 13<11x--H10yA 1=k)
V (PC1 = 3 A pC2 = B A y < 2 A 3 < x A 1 =
V (PC1 = 2 A pC2 = 0 A x < 2 A 8 < --H11x + 10 y A 2 =
V (PC1 = 2 A pC2 = 0 A x < 2 A 3 < y A 2 =
V(pC1 = 2 A pC2 = B A x <2 A y <2 A 13< --H10y)
V(pC1 = 3 A ?C2 = B A y <2 A 13< --H10y A 46< lix --H 10y A 0 =
Since p6 C J?3 ? R?, a fixpoint is found in 6 iterations. Notice that the tixpoint Uo<i<? 11? contains
no initial states from Ri. Therefore, the invanant property has been verified.
17
Fixpoint computation: leaking gas burner
Let A be the integrator system defined in Figure 5. We use the fixpoint computation procedure to
prove that the formula y > 60 201 < y is an invariant of A. It follo'vs that the gas burner leaks
at most one twentieth of the time in any interval of at least 60 seconds. Let i?? = = 1 A I =
0 A x = 0) be the region of initial states and let l?j = > 60 A 201 > y) be the region of "bad"
states. Let P? again denote the value of R = pre(l?c??) after the `i-th iteration of the algorithm.
Then:
R0			=			Rj
R1 = ((pc = 2 A --H19<201 --H y A 11<201 + x --H y A 2<1 A 0<1 A 0< x)
v (pe = 1 A --H19<201 --H 19x --H y A 2 < I --H x A --H1 < --Hx A 0 <
R2			=			((pc = 1 A --H8 < 201 --H 19x --H y A 1 <I --H x A --H1 < --Hx A 0 <
v(pc = 2 A --H19<201 --H y A 2<1 A 11<201 + x --H y A 0< x))
J?3 = ((pc=2A --H8<201--HyA 1<1 A 22<201+x--HyA 0<?x)
v (pc = 1 A --H8 < 201 --H 19x --H y A 1 < 1 --H x A --H4 < --Hx A 0 < x))
J?4			=			((pc = 1 A 0< 1 --H x A 3< 201 --H 19x --H y A --H1 < --Hx A 0< x)
v(pc = 2 A --H8<201 --H y A 1<1 A 22<201+ x --H y A 0< x))
= ((pc = 2 A 0<1 A 3<201--H y A 33<201+ x --H y A 0< x)
v (pe = 1 A 0 < I --H x A 3 < 201 --H 19x --H y A --H1 < --Hx A 0 <
J?6			=			((pc = 1 A --H1 < 1 --H x A 14< 201 --H i9x --H y A --H1 < --Hx A 0< x)
v(pc = 2 A 0<1 A 3<201 --H y A 33<201 + x --H y A 0 <x))
R7 = ((pc = 2 A 14<201 --H y A 44<201 + x --H y A 0<1 A 0< x)
v (pc = 1 A --H1 < 1 --H x A 14 < 201 --H 19x --H y A --Hi < --Hx A 0 <
1?8			=			((PC = 1 A 25 < 201 --H 19x --H y' A --H1 <I --H x A --H1< --Hx A 0 <
v(pc = 2 A 14<201 --H y A 44<201+ x --H y A 0<1 A 0< x))
J?9 = ((pc = 2 A 25<201 --H y A 55<201 + x --H y A 0<1 A 0< x)
v (pe = 1 A 25 < 201 --H 19x --H y A --H1 <I --H x A --H1 < --Hx A 0 <
Since R9 C J?8, a fixpoint is found in 9 iterations. As the fixpoint Uo<i<8 11? contains no initial
states from l?j, the invariant property has been verified. _
Acknowledgements. Amir Pnueh and Joseph Sifakis have influenced the ideas contained in this
paper through numerous discussions.
References
[ACII+92] R. Alur, C. Courcoubetis, N. HaThwachs, D.L. Dill, and II. Wong-Toi. Minimization
of timed transition systems. In `v.R. Cleaveland, editor, CONCUl? 92: Theories of
Coneurrency, Lecture Notes in Computer Science 630, pages 340--H354. Springer-Verlag,
1992.
R. Alur and D.L. Dill. Automata for modeling real-time systems. In M.S. Paterson,
editor, ICALP 90: Autornala, Languages, and Programming, Lecture Notes in Computer
Science 443, pages 322--H335. Springer-Verlag, 1990.
[AD90j
18
[BFH9Oj
[Cera?nsj
A. Bouajjani, J.C. Fernandez, and N. Halbwachs. Mimmal model generation. In R.P.
Kurshan and E.M. Clarke, editors, CAV 90: Automatic Verification Afethodsfor Finite-
state Systems, Lecture Notes in Computer Science 531, pages 197--H203. Springer-Verlag,
1990.
K. Cerans. Deddability of bishunlation equivalence for parallel timer processes. In
CAV 92: Automatic VerificatThn Afethods for Finite-state Systems, Lecture Notes in
Computer Science. Springer-Verlag. To appear.
[CHR91] z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information
Processing Letters, 40(5):269--H276, 1991.
[HNSY92] T.A. Henzinger, 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.
[11P583] D. Harel, A. Puneli., and J. Stavi. Propositional Qynamic logic of regular programs.
Journal of Computer and System Sciences, 26(2):222--243, 1983.
[Lam87] L. Lamport. A fast mutual exclusion algorithm. AC? Transactions on Computer
Systems, 5(1):1--H1J, 1987.
[LY92j D. Lee and M. Yannakakis. Online minimization of transition systems. In Proceedings
of the 24th Annual Symposium on Theory of Computing. ACM Press, 1992.
[MMP92]
0. Maler, Z. Manna, and A. Puneli. From timed to hybrid systems. In J.?7. 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 484. Springer-Verlag, 1992.
[NSOY] X. Nicollin, J. Sifakis, A. Olivero, and 5. Yovine. An approach to the description and
analysis of hybrid systems. To appear.
[N5Y92]
X. Nicollin, J. Sifakis, and 5. Yovine. From ATP to timed graphs and hybrid systems.
In J.W. de Hakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time:
Theory in Practice, Lecture Notes in Computer Science 600, pages 549--H572. Springer-
Verlag, 1992.
[WMF92j F. ?Vang, A.K. Mok, and E.A. Emerson. Real-time distributed system specification and
verification in asynchronous propositional temporal logic. In Proceedings of the 12th
International Conference on Softu'are Engineering, 1992.
19
