EECI 2012: Algorithmic Verification of Hybrid Systems: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
{{eeci-sp12 header|prev=Deductive Verification | {{eeci-sp12 header|prev=Deductive Verification|next=Protocol Synthesis}} | ||
This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties. | This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties. | ||
Revision as of 13:13, 16 May 2012
| Prev: Deductive Verification | Course home | Next: Protocol Synthesis |
This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties.
Lecture Materials
Additional Material and 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.
Receding horizon temporal logic planning,T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning.
Optimization based control. A page prepared for EECI 2008 with information and material on basic receding horizon control.
Multiparametric Toolbox The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. The receding horizon temporal logic planning toolbox uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT.
Automatic synthesis of robust embedded control software, T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture.
Predictive Control: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book.
