Difference between revisions of "EECI 2012: Algorithmic Verification of Hybrid Systems"

From Murray Wiki
Jump to navigationJump to search
(Created page with '{{eeci-sp12 header|prev=Deductive Verification of Hybrid Systems|next=Synthesis of Reactive Control Protocols}} This lecture focuses on the verification of hybrid systems. We fi…')
 
Line 1: Line 1:
 
{{eeci-sp12 header|prev=Deductive Verification of Hybrid Systems|next=Synthesis of Reactive Control Protocols}}
 
{{eeci-sp12 header|prev=Deductive Verification of Hybrid Systems|next=Synthesis of Reactive Control Protocols}}
  
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 move to deductive verification and a computational procedure for constructing Lyapunov-type 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.
+
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.
  
  
 
{{righttoc}}
 
{{righttoc}}
 
  
  
 
==  Lecture Materials ==
 
==  Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L6_Hybrid_Systems_Verification.pdf Hybrid Systems Verification]
+
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/EECI2012/L5_abstractions_16May12.pdf Abstractions for the Analysis and Synthesis of Control Protocols for Hybrid Systems]
  
 
== Additional Material and Further Reading ==
 
== Additional Material and Further Reading ==

Revision as of 10:08, 14 May 2012

Prev: Deductive Verification of Hybrid Systems Course home Next: Synthesis of Reactive Control Protocols

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

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