EECI 2013: Algorithmic Verification of Hybrid Systems - Revision history

Murray: /* Lecture Materials */

2014-03-02T18:04:11Z

Lecture Materials

← Older revision		Revision as of 18:04, 2 March 2014
Line 4:		Line 4:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~~~utopcu~~/~~eeci13~~/~~L6_Abstractions~~-~~2013~~.pdf Abstractions for the Analysis and Synthesis of Control Protocols for Hybrid Systems]		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp13/L6_abstractions-20Mar13.pdf Abstractions for the Analysis and Synthesis of Control Protocols for Hybrid Systems]

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

Utopcu: /* Further Reading */

2013-03-20T19:54:34Z

Further Reading

← Older revision		Revision as of 19:54, 20 March 2013
Line 13:		Line 13:
	* <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.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>		*<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>
			*<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>
			* <p>[http://www.cds.caltech.edu/~utopcu/eeci13/ltom-12-cdc.pdf Reactive controllers for differentially flat systems with temporal logic constraints], J. Liu, N. Ozay, U. Topcu, and R. Murray, Control and Decision Conference, 2012. </p>

Utopcu: Created page with "{{eeci-sp13 header|prev=Deductive Verification|next=Protocol Synthesis}} This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and ..."

2013-03-16T09:11:56Z

Created page with "{{eeci-sp13 header|prev=Deductive Verification|next=Protocol Synthesis}} This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and ..."

New page

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

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci13/L6_Abstractions-2013.pdf Abstractions for the Analysis and Synthesis of Control Protocols for Hybrid Systems]

== Further Reading ==
* [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://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. 
* [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.
* [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. 
* [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. 
* [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.