EECI 2012: Deductive Verification of Hybrid Systems - Revision history

Murray: /* Further Reading */

2012-05-16T10:37:36Z

Further Reading

← Older revision		Revision as of 10:37, 16 May 2012
Line 9:		Line 9:

	== 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://resolver.caltech.edu/CaltechETD:etd-05272005-144358 Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. </p>		* <p>[http://resolver.caltech.edu/CaltechETD: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://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>

Utopcu: /* Lecture Materials */

2012-05-16T08:11:49Z

Lecture Materials

← Older revision		Revision as of 08:11, 16 May 2012
Line 5:		Line 5:
	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L5_deductive-16May12.pdf Deductive Verification of Hybrid Systems]		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L5_deductive-16May12.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 ==

Utopcu: /* Further Reading */

2012-05-16T08:10:01Z

Further Reading

← Older revision		Revision as of 08:10, 16 May 2012
Line 7:		Line 7:

	== 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://resolver.caltech.edu/CaltechETD:etd-05272005-144358 Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. </p>		* <p>[http://resolver.caltech.edu/CaltechETD: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://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>

Murray: /* Lecture Materials */

2012-05-16T06:55:47Z

Lecture Materials

← Older revision		Revision as of 06:55, 16 May 2012
Line 4:		Line 4:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L5_deductive.pdf Deductive Verification of Hybrid Systems]		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L5_deductive-16May12.pdf Deductive Verification of Hybrid Systems]

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

Murray: /* Further Reading */

2012-05-16T04:54:16Z

Further Reading

← Older revision		Revision as of 04:54, 16 May 2012
Line 8:		Line 8:
	== 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://~~etd~~.caltech.edu/~~etd/available/~~etd-05272005-144358/ Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. </p>		* <p>[http://resolver.caltech.edu/CaltechETD: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://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://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>

Murray: /* Further Reading */

2012-05-14T09:50:14Z

Further Reading

← Older revision		Revision as of 09:50, 14 May 2012
Line 7:		Line 7:

	== Further Reading ==		== 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://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://etd.caltech.edu/etd/available/etd-05272005-144358/ Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. </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://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://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://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1271797 A Computation and Control Language for Multi-Vehicle Systems], E. Klavins. Int’l Conference on Robotics and Automation, 2004. </p>		* <p> [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1271797 A Computation and Control Language for Multi-Vehicle Systems], E. Klavins. Int’l Conference on Robotics and Automation, 2004. </p>
	* <p> [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1269132 Distributed Algorithms for Cooperative Control], E. Klavins and R. M. Murray. ''IEEE Pervasive Computing'', 2004. </p>		* <p> [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1269132 Distributed Algorithms for Cooperative Control], E. Klavins and R. M. Murray. ''IEEE Pervasive Computing'', 2004. </p>

	== Additional Materials ==		== Additional Materials ==

Murray: Created page with '{{eeci-sp12 header|prev=Computer Session: Spin|next=Algorithmic Verification}} This lecture focuses on the verification of hybrid systems using deductive (theorem proving) metho…'

2012-05-14T09:48:49Z

Created page with '{{eeci-sp12 header|prev=Computer Session: Spin|next=Algorithmic Verification}} This lecture focuses on the verification of hybrid systems using deductive (theorem proving) metho…'

New page

{{eeci-sp12 header|prev=Computer Session: Spin|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 ==
* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L5_deductive.pdf Deductive Verification of Hybrid Systems]

== 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. 
* [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1271797 A Computation and Control Language for Multi-Vehicle Systems], E. Klavins. Int’l Conference on Robotics and Automation, 2004. 
* [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1269132 Distributed Algorithms for Cooperative Control], E. Klavins and R. M. Murray. ''IEEE Pervasive Computing'', 2004. 

== Additional Materials ==