HYCON-EECI, Spring 2013 - Revision history

Murray at 21:35, 12 May 2013

2013-05-12T21:35:16Z

← Older revision		Revision as of 21:35, 12 May 2013
Line 6:		Line 6:
	<tr><td align=center><font color='blue' size='+2'>of Networked Control Systems<br>   </font></td></tr>		<tr><td align=center><font color='blue' size='+2'>of Networked Control Systems<br>   </font></td></tr>
	<tr valign=top><td align=center><font color='blue' size='+0'><p> Richard M. Murray, Ufuk Topcu, and Nok Wongpiromsarn </p></font></td></tr>		<tr valign=top><td align=center><font color='blue' size='+0'><p> Richard M. Murray, Ufuk Topcu, and Nok Wongpiromsarn </p></font></td></tr>
	<tr valign=top><td align=center><font color='blue' size='+0'><p>18-22 ~~May~~ 2013, Belgrade (Serbia)</p></font></td></tr>		<tr valign=top><td align=center><font color='blue' size='+0'><p>18-22 March 2013, Belgrade (Serbia)</p></font></td></tr>
	</table> __NOTOC__		</table> __NOTOC__

Murray: /* Lecture Schedule */

2013-03-22T08:22:29Z

Lecture Schedule

← Older revision		Revision as of 08:22, 22 March 2013
Line 90:		Line 90:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci13 entry\|L9\|UT\|Fri, 9:00\|Advanced Topics ~~in Protocol Synthesis~~\|		{{eeci13 entry\|L9\|UT\|Fri, 9:00\|Advanced Topics\|
	* Distributed ~~control~~		* Distributed protocols
	* ~~Switching~~		* Switched systems
	* ~~Examples: reactive motion planning, electric power systems (distributed)~~		* Optimal synthesis
	}}		}}
	{{eeci13 entry\|L10\|RM\|Fri, 11:00\|~~Extensions, Applications,~~ Open Questions\|		{{eeci13 entry\|L10\|RM\|Fri, 11:00\|Summary and Open Questions\|
	* Review of control trends and course contents		* Review of control trends and course contents
	* Discussion of open problem areas and preliminary results		* Discussion of open problem areas and preliminary results

Utopcu: /* Lecture Schedule */

2013-03-16T09:19:38Z

Lecture Schedule

← Older revision		Revision as of 09:19, 16 March 2013
Line 90:		Line 90:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci13 entry\|L9\|UT\|Fri, 9:00\|~~Receding Horizon Temporal Logic Planning~~\|		{{eeci13 entry\|L9\|UT\|Fri, 9:00\|Advanced Topics in Protocol Synthesis\|
	* Distributed control		* Distributed control
	* Switching		* Switching

Murray: /* Reading */

2013-03-11T04:09:21Z

Reading

← Older revision		Revision as of 04:09, 11 March 2013
Line 17:		Line 17:
	* <p>[http://www.cds.caltech.edu/~murray/papers/2012z_wtm12-us.html Synthesis of Control Protocols for Autonomous Systems], N. Wongpiromsarn, U. Topcu and R. M. Murray. ''Unmanned Systems'', 2013 (submitted)		* <p>[http://www.cds.caltech.edu/~murray/papers/2012z_wtm12-us.html Synthesis of Control Protocols for Autonomous Systems], N. Wongpiromsarn, U. Topcu and R. M. Murray. ''Unmanned Systems'', 2013 (submitted)
	Additional references for individual topics are included on the individual lecture pages.		Additional references for individual topics are included on the individual lecture pages.


	== Course information ==		== Course information ==

Murray at 04:09, 11 March 2013

2013-03-11T04:09:12Z

← Older revision		Revision as of 04:09, 11 March 2013
Line 11:		Line 11:
	== Course Description ==		== Course Description ==
	Increases in fast and inexpensive computing and communications have enabled a new generation of information-rich control systems that rely on multi-threaded networked execution, distributed optimization, sensor fusion and protocol stacks in increasingly sophisticated ways. This course will provide working knowledge of a collection of methods and tools for specifying, designing and verifying networked control systems. We combine methods from computer science (temporal logic, model checking, synthesis of control protocols) with those from dynamical systems and control (Lyapunov functions, trajectory generation, receding horizon control) to analyze and design partially asynchronous control protocols for continuous systems. In addition to introducing the mathematical techniques required to formulate problems and prove properties, we also describe a software toolbox (TuLiP) that is designed for analyzing and synthesizing hybrid control systems using linear temporal logic and robust performance specifications.		Increases in fast and inexpensive computing and communications have enabled a new generation of information-rich control systems that rely on multi-threaded networked execution, distributed optimization, sensor fusion and protocol stacks in increasingly sophisticated ways. This course will provide working knowledge of a collection of methods and tools for specifying, designing and verifying networked control systems. We combine methods from computer science (temporal logic, model checking, synthesis of control protocols) with those from dynamical systems and control (Lyapunov functions, trajectory generation, receding horizon control) to analyze and design partially asynchronous control protocols for continuous systems. In addition to introducing the mathematical techniques required to formulate problems and prove properties, we also describe a software toolbox (TuLiP) that is designed for analyzing and synthesizing hybrid control systems using linear temporal logic and robust performance specifications.

			== Reading ==
			The following papers and textbooks will be used heavily throughout the course:
			* <p>[http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 Principles of Model Checking], C. Baier and J.-P. Katoen, The MIT Press, 2008. </p>
			* <p>[http://www.cds.caltech.edu/~murray/papers/2012z_wtm12-us.html Synthesis of Control Protocols for Autonomous Systems], N. Wongpiromsarn, U. Topcu and R. M. Murray. ''Unmanned Systems'', 2013 (submitted)
			Additional references for individual topics are included on the individual lecture pages.


	== Course information ==		== Course information ==

Murray: /* Lecture Schedule */

2013-03-11T04:01:31Z

Lecture Schedule

Murray at 03:59, 11 March 2013

2013-03-11T03:59:16Z

← Older revision		Revision as of 03:59, 11 March 2013
Line 111:		Line 111:

	[[Category:Courses]]		[[Category:Courses]]
	[[Category:~~2011~~-12 Courses]]		[[Category:2012-13 Courses]]

Murray: /* Course information */

2013-03-11T03:58:05Z

Course information

← Older revision		Revision as of 03:58, 11 March 2013
Line 14:		Line 14:
	== Course information ==		== Course information ==
	* Instructors: [http://www.cds.caltech.edu/~murray/wiki/Main_Page Richard M. Murray] (Caltech, CDS) and [http://www.cds.caltech.edu/~utopcu/index.php/Main_Page Ufuk Topcu] (Caltech, CDS), and [http://www.cds.caltech.edu/~nok/ Nok Wongpiromsarn] (MIT-Singapore)		* Instructors: [http://www.cds.caltech.edu/~murray/wiki/Main_Page Richard M. Murray] (Caltech, CDS) and [http://www.cds.caltech.edu/~utopcu/index.php/Main_Page Ufuk Topcu] (Caltech, CDS), and [http://www.cds.caltech.edu/~nok/ Nok Wongpiromsarn] (MIT-Singapore)
	* Date and location: 14-18 May ~~2012~~, ~~L'Aquila~~ (~~Italy~~)		* Date and location: 18-22 May 2013, Belgrade (Serbia)
	* Sponsor: [http://www.eeci-institute.eu/~~GSC2011~~ HYCON-EECI Graduate School on Control]		* Sponsor: [http://www.eeci-institute.eu/GSC2013 HYCON-EECI Graduate School on Control]

	== Lecture Schedule ==		== Lecture Schedule ==

Murray: /* Lecture Schedule */

2013-03-01T14:28:32Z

Lecture Schedule

Murray: /* Lecture Schedule */

2013-03-01T14:15:56Z

Lecture Schedule

← Older revision		Revision as of 14:15, 1 March 2013
Line 67:		Line 67:
	* Examples: gear changing (?), ???		* Examples: gear changing (?), ???
	}}		}}
	{{eeci12 entry\|RM\|Wed, 14:00\|Synthesis of Reactive Control Protocols\|		{{eeci12 entry\|L7\|RM\|Wed, 14:00\|Synthesis of Reactive Control Protocols\|
	* Open system and reactive system synthesis		* Open system and reactive system synthesis
	* Satisfiability, realizability		* Satisfiability, realizability

← Older revision		Revision as of 04:01, 11 March 2013
Line 27:		Line 27:
	\|Title		\|Title
	\|Topics		\|Topics
	{{~~eeci12~~ entry\|L1\|RM\|Mon, 9:00\|Introduction: Protocol-Based Control Systems\|		{{eeci13 entry\|L1\|RM\|Mon, 9:00\|Introduction: Protocol-Based Control Systems\|
	* Introduction to networked control systems (NCS)		* Introduction to networked control systems (NCS)
	* Overview of control "protocols"		* Overview of control "protocols"
	* Examples: Alice, RoboFlag		* Examples: Alice, RoboFlag
	}}		}}
	{{~~eeci12~~ entry\|L2\|UT\|Mon, 11:00\|Automata Theory\|		{{eeci13 entry\|L2\|UT\|Mon, 11:00\|Automata Theory\|
	* Finite transition systems		* Finite transition systems
	* Paths, traces and composition of finite transition systems		* Paths, traces and composition of finite transition systems
Line 38:		Line 38:
	* Examples: traffic light		* Examples: traffic light
	}}		}}
	{{~~eeci12~~ entry\|L3\|RM\|Mon, 14:00\|Temporal Logic\|		{{eeci13 entry\|L3\|RM\|Mon, 14:00\|Temporal Logic\|
	* Linear temporal logic		* Linear temporal logic
	* Omega regular properties		* Omega regular properties
Line 44:		Line 44:
	* Examples: traffic light, (RoboFlag), autonomous driving		* Examples: traffic light, (RoboFlag), autonomous driving
	}}		}}
	{{~~eeci12~~ entry\|L4\|UT\|Mon, 16:00\|Model Checking and Logic Synthesis\|		{{eeci13 entry\|L4\|UT\|Mon, 16:00\|Model Checking and Logic Synthesis\|
	* Basic concepts in model checking		* Basic concepts in model checking
	* Use of model checking for logic synthesis		* Use of model checking for logic synthesis
	* Examples: traffic light, farmer puzzle		* Examples: traffic light, farmer puzzle
	}}		}}
	{{~~eeci12~~ entry\|C1\|RM\|Tue, 9:00 <br> Tue, 11:00\|Computer Session: Spin\|		{{eeci13 entry\|C1\|RM\|Tue, 9:00 <br> Tue, 11:00\|Computer Session: Spin\|
	* Introduction to Promela and Spin (statements, processes, messages)		* Introduction to Promela and Spin (statements, processes, messages)
	* Verification examples: traffic light, distributed traffic light, gcdrive		* Verification examples: traffic light, distributed traffic light, gcdrive
	* Synthesis examples: traffic light, farmer puzzle, robot navigation		* Synthesis examples: traffic light, farmer puzzle, robot navigation
	}}		}}
	{{~~eeci12~~ entry\|L5\|RM (1h)\|Wed, 9:00\|Deductive Verification of Hybrid Systems\|		{{eeci13 entry\|L5\|RM (1h)\|Wed, 9:00\|Deductive Verification of Hybrid Systems\|
	* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)		* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)
	* Deductive verification using barrier certificates		* Deductive verification using barrier certificates
Line 60:		Line 60:
	* Examples: multi-agent systems, RoboFlag		* Examples: multi-agent systems, RoboFlag
	}}		}}
	{{~~eeci12~~ entry\|L6\|UT (2h)\|Wed, 11:00\|Algorithmic Verification of Hybrid Systems\|		{{eeci13 entry\|L6\|UT (2h)\|Wed, 11:00\|Algorithmic Verification of Hybrid Systems\|
	* Abstraction hierarchies for control systems		* Abstraction hierarchies for control systems
	* Finite state abstractions (discretization) and model checking		* Finite state abstractions (discretization) and model checking
Line 67:		Line 67:
	* Examples: gear changing (?), ???		* Examples: gear changing (?), ???
	}}		}}
	{{~~eeci12~~ entry\|L7\|RM (2h)\|Wed, 14:00\|Synthesis of Reactive Control Protocols\|		{{eeci13 entry\|L7\|RM (2h)\|Wed, 14:00\|Synthesis of Reactive Control Protocols\|
	* Open system and reactive system synthesis		* Open system and reactive system synthesis
	* Satisfiability, realizability		* Satisfiability, realizability
Line 74:		Line 74:
	* Examples: runner-blocker		* Examples: runner-blocker
	}}		}}
	{{~~eeci12~~ entry\|L8\|UT(1h)\|Wed, 16:00\|Receding Horizon Temporal Logic Planning\|		{{eeci13 entry\|L8\|UT(1h)\|Wed, 16:00\|Receding Horizon Temporal Logic Planning\|
	* Receding horizon control		* Receding horizon control
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{~~eeci12~~ entry\|C2\|UT\|Thu, 9:00 <br> Thu, 11:00\|Computer Session: TuLiP\|		{{eeci13 entry\|C2\|UT\|Thu, 9:00 <br> Thu, 11:00\|Computer Session: TuLiP\|
	* Introduction to TuLiP		* Introduction to TuLiP
	* Synthesis of protocols for discrete systems		* Synthesis of protocols for discrete systems
Line 84:		Line 84:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{~~eeci12~~ entry\|L9\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|		{{eeci13 entry\|L9\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|
	* Distributed control		* Distributed control
	* Switching		* Switching
	* Examples: reactive motion planning, electric power systems (distributed)		* Examples: reactive motion planning, electric power systems (distributed)
	}}		}}
	{{~~eeci12~~ entry\|L10\|RM\|Fri, 11:00\|Extensions, Applications, Open Questions\|		{{eeci13 entry\|L10\|RM\|Fri, 11:00\|Extensions, Applications, Open Questions\|
	* Review of control trends and course contents		* Review of control trends and course contents
	* Discussion of open problem areas and preliminary results		* Discussion of open problem areas and preliminary results

← Older revision		Revision as of 14:28, 1 March 2013
Line 54:		Line 54:
	* Synthesis examples: traffic light, farmer puzzle, robot navigation		* Synthesis examples: traffic light, farmer puzzle, robot navigation
	}}		}}
	{{eeci12 entry\|L5\|RM\|Wed, 9:00\|Deductive Verification of Hybrid Systems\|		{{eeci12 entry\|L5\|RM (1h)\|Wed, 9:00\|Deductive Verification of Hybrid Systems\|
	* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)		* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)
	* Deductive verification using barrier certificates		* Deductive verification using barrier certificates
Line 60:		Line 60:
	* Examples: multi-agent systems, RoboFlag		* Examples: multi-agent systems, RoboFlag
	}}		}}
	{{eeci12 entry\|L6\|UT\|Wed, 11:00\|Algorithmic Verification of Hybrid Systems\|		{{eeci12 entry\|L6\|UT (2h)\|Wed, 11:00\|Algorithmic Verification of Hybrid Systems\|
	* Abstraction hierarchies for control systems		* Abstraction hierarchies for control systems
	* Finite state abstractions (discretization) and model checking		* Finite state abstractions (discretization) and model checking
Line 67:		Line 67:
	* Examples: gear changing (?), ???		* Examples: gear changing (?), ???
	}}		}}
	{{eeci12 entry\|L7\|RM\|Wed, 14:00\|Synthesis of Reactive Control Protocols\|		{{eeci12 entry\|L7\|RM (2h)\|Wed, 14:00\|Synthesis of Reactive Control Protocols\|
	* Open system and reactive system synthesis		* Open system and reactive system synthesis
	* Satisfiability, realizability		* Satisfiability, realizability
Line 73:		Line 73:
	* Mu-calculus (if time) and GR(1) games		* Mu-calculus (if time) and GR(1) games
	* Examples: runner-blocker		* Examples: runner-blocker
			}}
			{{eeci12 entry\|L8\|UT(1h)\|Wed, 16:00\|Receding Horizon Temporal Logic Planning\|
			* Receding horizon control
			* Examples: reactive motion planning
	}}		}}
	{{eeci12 entry\|C2\|UT\|Thu, 9:00 <br> Thu, 11:00\|Computer Session: TuLiP\|		{{eeci12 entry\|C2\|UT\|Thu, 9:00 <br> Thu, 11:00\|Computer Session: TuLiP\|
Line 80:		Line 84:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci12 entry\|L8\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|		{{eeci12 entry\|L9\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|
	* Receding horizon control
	* Distributed control		* Distributed control
			* Switching
	* Examples: reactive motion planning, electric power systems (distributed)		* Examples: reactive motion planning, electric power systems (distributed)
	}}		}}
	{{eeci12 entry\|L9\|RM\|Fri, 11:00\|Extensions, Applications, Open Questions\|		{{eeci12 entry\|L10\|RM\|Fri, 11:00\|Extensions, Applications, Open Questions\|
	* Review of control trends and course contents		* Review of control trends and course contents
	* Discussion of open problem areas and preliminary results		* Discussion of open problem areas and preliminary results