The Theory of Rectangular Hybrid Automata

A {\em hybrid automaton\/} consists of a finite automaton interacting with a dynamical system. Hybrid automata are used to model embedded controllers and other systems that consist of interacting discrete and continuous components. A hybrid automaton is {\em rectangular\/} if each of its continuous variables~x satisfies a nondeterministic differential equation of the form a≤dxdt≤b, where a and~b are rational constants. Rectangular hybrid automata are particularly useful for the analysis of communication protocols in which local clocks have bounded drift, and for the conservative approximation of systems with more complex continuous behavior. We examine several verification problems on the class of rectangular hybrid automata, including reachability, temporal logic model checking, and controller synthesis. Both dense-time and discrete-time models are considered. We identify subclasses of rectangular hybrid automata for which these problems are decidable and give complexity analyses. An investigation of the structural properties of rectangular hybrid automata is undertaken. One method for proving the decidability of verification problems on infinite-state systems is to find finite quotient systems on which analysis can proceed. Three state-space equivalence relations with strong connections to temporal logic are bisimilarity, similarity, and language equivalence. We characterize the quotient spaces of rectangular hybrid automata with respect to these equivalence relations.