EECI 2012: Hybrid Systems Verification
Return to Caltech/AFRL 2012 Main Page
This lecture focuses on the verification of hybrid systems. We first discuss finitestate under and overapproximations of hybrid dynamics and how these finitestate models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we move to deductive verification and a computational procedure for constructing Lyapunovtype functions (e.g., barrier certificates) which witness the fact that a hybrid system satisfies certain temporal specifications. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties.
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 sumofsquares 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 Sprocedure).

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.