Computing Approximating Automata for a Class of Linear Hybrid Systems

Approximating automata are finite-state representations of the sequential inputoutput behaviors of hybrid systems characterized by threshold events that trigger discrete changes in the continuous dynamic equations. Procedures proposed for constructing approximating automata require forward and backward mappings of sets of continuous state trajectories -- mappings which are not available for arbitrary continuous dynamics. This paper develops the foundations for constructing approximating automata automatically for hybrid systems in which the continuous dynamics are defined by convex polytopes in the vector space of the derivatives of the continuous state trajectories. The computations are illustrated for a simple example which also demonstrates the use of approximating automata to solve verification problems that may be intractable using fixed-point computations for linear hybrid automata. 1 Introduction This paper concerns the generation of purely discrete models (finite automata) for..