#### Transcript Architectures for Secure and Robust Distributed

Stability of Hybrid Automata with Average Dwell Time: An Invariant Approach Sayan Mitra Daniel Liberzon Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology [email protected] Coordinated Science Laboratory University of Illinois at Urbana-Champaign [email protected] IEEE CDC 2004, Paradise Island, Bahamas 1 HIOA: A Platform Bridging the Gap Hybrid Systems Control Theory: Dynamical system with boolean variables Stability Controllability Controller design Computer Science: State transition systems with continuous dynamics Safety verification model checking theorem proving HIOA: math model specification Expressive: few constraints on continuous and discrete behavior Compositional: analyze complex systems by looking at parts Structured: inductive verification Compatible: application of CT results e.g. stability, synthesis [Lynch, Segala, Vaandrager] 2 Hybrid I/O Automata V= U Y X: input, output, internal variables Q: states, a set of valuations of V : start states A = I O H: input, output, internal actions D Q A Q: discrete transitions T: trajectories for V, functions describing continuous evolution Execution (fragment): sequence 0 a1 1 a2 2 …, where: Each i is a trajectory of the automaton, and Each (i.lstate, ai , i+1.fstate) is a discrete step 3 HIOA Model for Switched Systems Switched system: is a family of systems is a switching signal Switched system modeled as HIOA: Each mode is modeled by a trajectory definition Mode switches are brought about by actions Usual notions of stability apply Stability theorems involving Common and Multiple Lyapunov functions carry over 4 Stability Under Slow Switchings V (t ) (t ) 1 decreasing sequence 2 1 2 t Slow switching: # of switches on (t , T ) average dwell time (τa) Assuming Lyapunov functions for the individual modes exist, global asymptotic stability is guaranteed if τa is large enough [Hespanha] 5 Verifying Average Dwell Time Average dwell time is a property of the executions of the automaton Invariant approach: Transform the automaton A A’ so that the a.d.t property of A becomes an invariant property of A’. Then use theorem proving or model checking tools to prove the invariant(s) Invariant I(s) proved by base case : induction discrete: continuous: 6 Transformation for Stability Simple stability preserving transformation: counter Q, for number of extra mode switches a (reset) timer t Qmin for the smallest value of Q A A’ Theorem: A has average dwell time τa iff Q- Qmin ≤ N0 in all reachable states of A’. invariant property 7 Case Study: Hysteresis Switch Inputs: Initialize Find no ? yes Used in switching (supervisory) control of uncertain systems Under suitable conditions on (compatible with bounded noise and no unmodeled dynamics), can prove a.d.t. ......................................................... See CDC paper for details 8 Beyond the CDC paper MILP approach: Search for counterexample execution by maximizing N(α) - α.length / τa over all executions Sufficient condition for violating a.d.t. τa: exists a cycle with N(α) α.length / τa > 0 This is also necessary condition for some classes of HIOA [Mitra, Liberzon, Lynch, “Verifying average dwell time”, 2004, http://decision.csl.uiuc.edu/~liberzon] Future work: Input-output properties (external stability) Supporting software tools [Kaynar, Lynch, Mitra] Probabilistic HIOA [Cheung, Lynch, Segala, Vaandrager] and stability of stochastic switched systems [Chatterjee, Liberzon, FrA01.1] 9