EECI 2012: Algorithmic Verification of Hybrid Systems - Revision history

Murray: /* Lecture Materials */

2012-05-17T07:17:00Z

Lecture Materials

← Older revision		Revision as of 07:17, 17 May 2012
Line 4:		Line 4:

	== Lecture Materials ==		== Lecture Materials ==
	* 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]		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L6_abstractions-16May12.pdf Abstractions for the Analysis and Synthesis of Control Protocols for Hybrid Systems]

	== Further Reading ==		== Further Reading ==

Murray at 07:14, 17 May 2012

2012-05-17T07:14:00Z

← Older revision		Revision as of 07:14, 17 May 2012
Line 2:		Line 2:

	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.


	~~{{righttoc}}~~


	== Lecture Materials ==		== Lecture Materials ==
	* 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]		* 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 ==		== Further Reading ==
	* <p> [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. </p>		* <p> [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. </p>
	* <p>[http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf 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. </p>		* <p>[http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf 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. </p>

Murray at 13:13, 16 May 2012

2012-05-16T13:13:57Z

← Older revision		Revision as of 13:13, 16 May 2012
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\|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.

Utopcu at 10:10, 14 May 2012

2012-05-14T10:10:20Z

← Older revision		Revision as of 10:10, 14 May 2012
Line 12:		Line 12:
	== Additional Material and Further Reading ==		== Additional Material and Further Reading ==
	* <p> [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. </p>		* <p> [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. </p>
			* <p>[http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf 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. </p>
			* <p> [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.</p>
			* <p>[http://control.ee.ethz.ch/~mpt/ 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. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. </p>
			* <p>[http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf 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. </p>
			*<p> [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 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. </p>

Utopcu at 10:09, 14 May 2012

2012-05-14T10:09:17Z

← Older revision		Revision as of 10:09, 14 May 2012
Line 11:		Line 11:

	== Additional Material and Further Reading ==		== Additional Material and Further Reading ==
	* <p> [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]</p>
	* <p>[http://etd.caltech.edu/etd/available/etd-05272005-144358/ Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. </p>
	* <p> [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.</p>
	* <p> [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). </p>
	* <p> [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. </p>		* <p> [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. </p>

Utopcu at 10:08, 14 May 2012

2012-05-14T10:08:44Z

← Older revision		Revision as of 10:08, 14 May 2012
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 ==

Utopcu: 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…'

2012-05-14T10:04:40Z

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…'

New page

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

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