THE ALGORITHMIC ANALYSIS OF HYBRID SYSTEMS

We present a general framework for the formal specification and algori thmic analysis of hybrid systems. A hybrid system consists of a discre te program with an analog environment. We model hybrid systems as fini te automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict o urselves to linear hybrid systems, where all variables follow piecewis e-linear trajectories. We provide decidability and undecidability resu lts for classes of linear hybrid systems, and we show that standard pr ogram-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization proce dures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definab le as unions of convex polyhedra in multidimensional real space. We al so present approximation techniques for dealing with systems for which the iterative procedures do not converge.