Stability of hybrid automata with average dwell time: An invariant approach

Research output: Contribution to journalConference article


A formal method based technique is presented for proving the average dwell time property of a hybrid system, which is useful for establishing stability under slow switching. The Hybrid Input/Output Automaton (HIOA) of [12] is used as the model for hybrid systems, and it is shown that some known stability theorems from system theory can be adapted to be applied in this framework. The average dwell time property of a given automaton is formalized as an invariant of a corresponding transformed automaton, such that the former has average dwell time if and only if the latter satisfies the invariant. Formal verification techniques can be used to check this invariance property. In particular, the HIOA framework facilitates inductive invariant proofs by systematically breaking them down into cases for the discrete actions and continuous trajectories of the automaton. The invariant approach to proving the average dwell time property is illustrated by analyzing the hysteresis switching logic unit of a supervisory control system.

Original languageEnglish (US)
Pages (from-to)1394-1399
Number of pages6
JournalProceedings of the IEEE Conference on Decision and Control
StatePublished - Dec 1 2004
Event2004 43rd IEEE Conference on Decision and Control (CDC) - Nassau, Bahamas
Duration: Dec 14 2004Dec 17 2004



  • Average dwell time
  • Hybrid I/O automaton
  • Hybrid systems
  • Hysteresis switching
  • Invariant, stability

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Modeling and Simulation
  • Control and Optimization

Cite this