## Hybrid Automata:
An Algorithmic Approach to the Specification and Verification of Hybrid Systems

*Rajeev Alur, Costas Courcoubetis,
Thomas A. Henzinger,
and Pei-Hsin Ho*

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.

*Hybrid Systems I*,
Lecture Notes in Computer Science 736,
Springer, 1993, pp. 209-229.
An extended version appeared under the title
*
The Algorithmic Analysis of Hybrid Systems*.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1993 Springer.