Abstract
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 language | English (US) |
|---|---|
| Article number | WeA01.1 |
| Pages (from-to) | 1394-1399 |
| Number of pages | 6 |
| Journal | Proceedings of the IEEE Conference on Decision and Control |
| Volume | 2 |
| DOIs | |
| State | Published - 2004 |
| Event | 2004 43rd IEEE Conference on Decision and Control (CDC) - Nassau, Bahamas Duration: Dec 14 2004 → Dec 17 2004 |
Keywords
- 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