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 Materials
- Lecture slides: Hybrid Systems Verification
Additional Material and Further Reading
Material on part III. Links to software packages, slides, and notes on quantitative analysis of nonlinear systems. Shorter version is in these slides
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.
