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.