## The Theory of Rectangular Hybrid Automata

*Peter W. Kopke*

A *hybrid automaton* consists of a finite automaton interacting
with a dynamical system. Hybrid automata are used to model embedded
controllers and other systems that consist of interacting discrete and
continuous components. A hybrid automaton is *rectangular* if
each of its continuous variables *x* satisfies a nondeterministic
differential equation of the form *a < dx/dt < b*, where
*a* and *b* are rational constants. Rectangular hybrid
automata are useful for the analysis of communication protocols in
which local clocks have bounded drift, and for the conservative
approximation of systems with more complex continuous behavior.

We examine several verification problems on the class of rectangular
hybrid automata, including reachability, temporal-logic model
checking, and controller synthesis. Both dense-time and discrete-time
models are considered. We identify subclasses of rectangular hybrid
automata for which these problems are decidable and give complexity
analyses.

An investigation of the structural properties of rectangular hybrid
automata is undertaken. One method for proving the decidability of
verification problems on infinite-state systems is to find finite
quotient systems on which analysis can proceed. Three state-space
equivalence relations with strong connections to temporal logic are
bisimilarity, similarity, and language equivalence. We characterize
the quotient spaces of rectangular hybrid automata with respect to
these equivalence relations.

Ph.D. thesis, Technical Report CSD-TR96-1601, Cornell University,
August 1996, 195 pages.

Download
PostScript /
PDF document.