Difference between revisions of "EECI 2013: Deductive Verification of Hybrid Systems"

From Murray Wiki
Jump to navigationJump to search
 
(One intermediate revision by the same user not shown)
Line 4: Line 4:


==  Lecture Materials ==
==  Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L5_deductive-20Mar13.pdf Deductive Verification of Hybrid Systems]
* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp13/L5_deductive-20Mar13.pdf Deductive Verification of Hybrid Systems]
 
Some of the slides are from a short course ([http://www.cds.caltech.edu/~utopcu/index.php/Short_Course:_Quantitative_Local_Analysis_of_Nonlinear_Systems_Using_Sum-of-Squares_Decompositions Quantitative Local Analysis of Nonlinear Systems Using Sum-of-Squares Decompositions]) by Balas, Packard, Seiler, and Topcu.


== Further Reading ==
== Further Reading ==
Line 17: Line 15:


== Additional Materials ==
== Additional Materials ==
* Slides from a short course ([http://www.cds.caltech.edu/~utopcu/index.php/Short_Course:_Quantitative_Local_Analysis_of_Nonlinear_Systems_Using_Sum-of-Squares_Decompositions Quantitative Local Analysis of Nonlinear Systems Using Sum-of-Squares Decompositions]) by Balas, Packard, Seiler, and Topcu.

Latest revision as of 08:05, 21 March 2013

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 Lyapunov-type 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 multi-agent 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

Further Reading

Additional Materials