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