Computing Approximating Automata for a Class of Hybrid Systems

Abstract

This paper presents a new algorithm for generating finite-state automata models of hybrid systems in which the continuous-state dynamics can be switched when the continuous-state trajectory generates threshold events. The automata state transitions correspond to threshold events and the automata states correspond to portions of the threshold surfaces in the continuous state space. The hybrid system dynamics are approximated by the automata models in the sense that the languages of threshold event sequences generated by the automata contain the threshold event language for the hybrid system. Properties of the algorithm for constructing and refining the approximating automata are demonstrated and the application of approximating automata for system verification is illustrated for a switching controller for an inverted pendulum. Relationships to other approaches to hybrid system synthesis and verification are also discussed.