The algorithmic analysis of hybrid systems

Abstract

We extend the timed-automaton model for real-time systems [AD90] to a formal model for hybrid systems: while the continuous variables of a timed automaton are clocks that measure time, the continuous variables of a hybrid system are governed by arbitrary differential equations. We then adopt the verification methodology for timed automata [ACD90, ACD+92, HNSY92] to analyze hybrid systems: while the verification problem is decidable for timed automata, we obtain semidecision procedures for the class of hybrid systems whose continuous variables change in a piecewise linear fashion. 1 A Model for Hybrid Systems We specify hybrid systems by graphs whose edges represent discrete transitions and whose vertices represent continuous activities [ACHH93, NOSY93]. A hybrid system H = (Loc, Vat, Lab, Edg, Act, Inv) consists of six components:-A finite set Loc of vertices called locations.-A finite set Var of real-valued variables. A valuation v for the variables is a function that assigns a real-value v(x) ~ R to each variable x 6 Var. We write V for the set of valuations. A state is a pair (g, v) consisting of a location ~ 6 Loc and a valuation v ~ V. We write ~ for the set of states.-A finite set Lab of synchronization labels that contains the stutter label r ~ Lab.