## The Algorithmic Analysis of Hybrid Systems

*Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs,
Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero,
Joseph Sifakis, and Sergio Yovine*
We present a general framework for the formal specification and algorithmic
analysis of hybrid systems.
A hybrid system consists of a discrete program with an analog environment.
We model hybrid systems as finite automata equipped with variables that
evolve continuously with time according to dynamical laws.
For verification purposes, we restrict ourselves to linear hybrid systems,
where all variables follow piecewise-linear trajectories.
We provide decidability and undecidability results for classes of linear
hybrid systems, and we show that standard program-analysis techniques can be
adapted to linear hybrid systems.
In particular, we consider symbolic model-checking and minimization
procedures that are based on the reachability analysis of an infinite state
space.
The procedures iteratively compute state sets that are definable as unions of
convex polyhedra in multidimensional real space.
We also present approximation techniques for dealing with systems for which
the iterative procedures do not converge.

*Theoretical Computer Science* 138:3-34, 1995.
A preliminary version appeared in the
*Proceedings of the 11th International
Conference on Analysis and Optimization of Systems: Discrete-event Systems*,
Lecture Notes in Control and Information Sciences 199,
Springer-Verlag, 1994, pp. 331-351.