EECI 2013: Deductive Verification of Hybrid Systems
Prev: Computer Session: Spin  Course home  Next: Algorithmic Verification 
This lecture focuses on the verification of hybrid systems using deductive (theorem proving) methods. We describe hybrid systems that combine continuous and discrete states. We then describe two methods for deductive verification. First, we discuss a computational procedure for constructing Lyapunovtype functions (e.g., barrier certificates) that witness the fact that a hybrid system satisfies certain temporal specifications. Second, we consider control protocols for cooperation and decision making in multiagent systems, as illustrated by the RoboFlag example introduced in the first lecture. We show how to implement a simple protocol for distributed target assignment in a simplified version of the problem (the "RoboFlag drill") and prove stability of the protocol.
Lecture Materials
 Lecture slides: Deductive Verification of Hybrid Systems
Further Reading

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.

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).

A Computation and Control Language for MultiVehicle Systems, E. Klavins. Int’l Conference on Robotics and Automation, 2004.

Distributed Algorithms for Cooperative Control, E. Klavins and R. M. Murray. IEEE Pervasive Computing, 2004.
Additional Materials
 Slides from a short course (Quantitative Local Analysis of Nonlinear Systems Using SumofSquares Decompositions) by Balas, Packard, Seiler, and Topcu.