Utopcu at 03:02, 22 April 2012

2012-04-22T03:02:55Z

← Older revision		Revision as of 03:02, 22 April 2012
Line 1:		Line 1:
	{{~~eeci-sp11~~ header\|prev=~~Computer Lab I~~ \|next=~~Autonomous Driving~~}}		{{AFRL12 header\|prev=... \|next=...}}

			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 computational verification of temporal specifications for hybrid, nonlinear dynamical systems and associated software packages. We discuss a procedure for computing algebraic functions (e.g., Lyapunov, storage, barrier functions) that witness the fact that a dynamical system satisfies certain temporal specifications. We discuss applications of this procedure to stability, input-output gain, safety, and eventuality verification. The notion of approximate bisimulations is introduced and use of so-called bisimulation functions in temporal property verification is discussed.

	{{righttoc}}		{{righttoc}}

Utopcu: Created page with '{{eeci-sp11 header|prev=Computer Lab I |next=Autonomous Driving}} This lecture focuses on the computational verification of temporal specifications for hybrid, nonlinear dynamic…'

2012-04-22T02:55:06Z

Created page with '{{eeci-sp11 header|prev=Computer Lab I |next=Autonomous Driving}} This lecture focuses on the computational verification of temporal specifications for hybrid, nonlinear dynamic…'

New page

{{eeci-sp11 header|prev=Computer Lab I |next=Autonomous Driving}}

This lecture focuses on the computational verification of temporal specifications for hybrid, nonlinear dynamical systems and associated software packages. We discuss a procedure for computing algebraic functions (e.g., Lyapunov, storage, barrier functions) that witness the fact that a dynamical system satisfies certain temporal specifications. We discuss applications of this procedure to stability, input-output gain, safety, and eventuality verification. The notion of approximate bisimulations is introduced and use of so-called bisimulation functions in temporal property verification is discussed.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L6_Hybrid_Systems_Verification.pdf Hybrid Systems Verification]

== Additional Material and Further Reading ==
* [http://www.cds.caltech.edu/~utopcu/index.php/Short_Course:_Quantitative_Local_Analysis_of_Nonlinear_Systems_Using_Sum-of-Squares_Decompositions Material on part III]. Links to software packages, slides, and notes on quantitative analysis of nonlinear systems. Shorter version is in these [http://www.cds.caltech.edu/~utopcu/cdc10vvslides/UfukTopcu.pdf slides]
* [http://etd.caltech.edu/etd/available/etd-05272005-144358/ Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. 
* [http://www.cds.caltech.edu/~utopcu/images//9/9b/TPSB-CSM-2010.pdf Help on SOS]: a paper on the very basics of sum-of-squares programming and their use in nonlinear system verification.
* [http://arxiv.org/abs/math.OC/0103170 Minimizing Polynomial Functions] by P. Parrilo and B. Sturmfels on global optimization of polynomial functions and Positivstellensatz (generalizations of the S-procedure). 
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf 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.

EECI 2012: Hybrid Systems Verification - Revision history

Utopcu at 03:02, 22 April 2012

Utopcu: Created page with '{{eeci-sp11 header|prev=Computer Lab I |next=Autonomous Driving}} This lecture focuses on the computational verification of temporal specifications for hybrid, nonlinear dynamic…'