EECI 2012: Hybrid Systems Verification
This lecture focuses on the computational verification of temporal specifications for hybrid, nonlinear dynamical systems and associated software packages. We discuss a procedure for computing algebraic functions (e.g., Lyapunov, storage, barrier functions) that witness the fact that a dynamical system satisfies certain temporal specifications. We discuss applications of this procedure to stability, input-output gain, safety, and eventuality verification. The notion of approximate bisimulations is introduced and use of so-called bisimulation functions in temporal property verification is discussed.
- Lecture slides: Hybrid Systems Verification
Additional Material and Further Reading
Stephen Prajna's dissertation on verifying temporal properties for hybrid dynamical systems.
Help on SOS: a paper on the very basics of sum-of-squares programming and their use in nonlinear system verification.
Minimizing Polynomial Functions by P. Parrilo and B. Sturmfels on global optimization of polynomial functions and Positivstellensatz (generalizations of the S-procedure).
Lecture Notes on Hybrid Systems (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course.