| Categories and Subject Descriptors: D. Software [D.2 Software Engineering]: D.2.4. Software/Program (2008) | |||||||||||||||||
Abstract | |||||||||||||||||
| The switched system model abstracts away the discrete mechanisms of a hybrid system in terms of an exogenous switching signal. Dwell Time and Average Dwell Time (ADT) criteria, introduced by Morse and Hespanha, define restricted classes of switching signals that guarantee stability of the whole system, provided the individual modes of the switched system are stable. In this paper, we present a set of techniques for establishing stability through verification of ADT properties. We introduce a new type of simulation relation for hybrid automata—switching simulation—that allows us to show that the ADT of one automaton is no less than that of another. We show that the question of whether a given hybrid automaton has ADT τa can be answered by checking a carefully designed invariant or by solving an optimization problem. The invariant-based method is applicable to any hybrid automaton. For suitable classes of automata the invariant in question can be checked automatically. The optimization-based method is applicable to a restricted class of initialized hybrid automata. For this class, a solution of the optimization problem either gives a counterexample execution that violates the ADT property, or it confirms that the automaton indeed satisfies the property. The optimization-based approach is automatic and complements the invariant-based method in the sense that they can be used in combination to find the unknown ADT of a given hybrid automaton. | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||