@Article{MLL:TECS08, author = {Sayan Mitra and Daniel Liberzon and Nancy Lynch}, title = {Verifying Average Dwell Time of Hybrid Systems}, journal = {ACM Transactions on Embedded Computing Systems}, year = {2008}, volume = {8}, abstract = {Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this article, we present a set of techniques for verifying ADT properties. The stability of a hybrid system A can be verified by combining these techniques with standard methods for checking stability of the individual modes of A. We introduce a new type of simulation relation for hybrid automata�switching simulation�for establishing that a given automaton A switches more rapidly than another automaton B. We show that the question of whether a given hybrid automaton has ADT ta can be answered either by checking an invariant or by solving an optimization problem. For classes of hybrid automata for which invariants can be checked automatically, the invariant-based method yields an automatic method for verifying ADT; for automata that are outside this class, the invariant has to be checked using inductive techniques. The optimization-based method is automatic and is applicable to a restricted class of initialized hybrid automata. 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 and the invariant-based methods can be used in combination to find the unknown ADT of a given hybrid automaton.}, biburl = {http://users.crhc.illinois.edu/mitras/research.html}, issue = {1}, keywords = {Hybrid systems, Control theory}, pdfurl = {research/2008/TECS-2006-0040-Final.pdf}, publisher = {ACM}, url = {http://portal.acm.org/citation.cfm?id=1457246.1457249&coll=portal&dl=ACM&idx=J840&part=transaction&WantType=Transactions&title=ACM%20Transactions%20on%20Embedded%20Computing%20Systems%20(TECS)}, }