## 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*,
Lecture Notes in Computer Science 736,
Springer-Verlag, 1993, pp. 209-229.