HYCON-EECI, Spring 2012 - Revision history

Murray at 13:11, 16 May 2012

2012-05-16T13:11:18Z

← Older revision		Revision as of 13:11, 16 May 2012
Line 4:		Line 4:
	<td align=center><font color='blue' size='+2'>Specification, Design, and Verification <br>  </font></td>		<td align=center><font color='blue' size='+2'>Specification, Design, and Verification <br>  </font></td>
	<td rowspan=4 align=center"> [[Image:cdslogo.png\|90px]]</td></tr>		<td rowspan=4 align=center"> [[Image:cdslogo.png\|90px]]</td></tr>
	<tr><td align=center><font color='blue' size='+2'>of ~~Distributed Embedded~~ 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>14-18 May 2012, L'Aquila (Italy)</p></font></td></tr>		<tr valign=top><td align=center><font color='blue' size='+0'><p>14-18 May 2012, L'Aquila (Italy)</p></font></td></tr>

Utopcu: Undo revision 14048 by Utopcu (Talk)

2012-05-14T10:14:03Z

Undo revision 14048 by Utopcu (Talk)

← Older revision		Revision as of 10:14, 14 May 2012
Line 80:		Line 80:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci12 entry\|L8\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning ~~and Compositional Synthesis~~\|		{{eeci12 entry\|L8\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|
	* Receding horizon control		* Receding horizon control
	* Distributed control		* Distributed control

Utopcu: /* Lecture Schedule */

2012-05-14T10:12:40Z

Lecture Schedule

← Older revision		Revision as of 10:12, 14 May 2012
Line 80:		Line 80:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci12 entry\|L8\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|		{{eeci12 entry\|L8\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning and Compositional Synthesis\|
	* Receding horizon control		* Receding horizon control
	* Distributed control		* Distributed control

Murray: /* Lecture Schedule */

2012-05-07T21:59:07Z

Lecture Schedule

← Older revision		Revision as of 21:59, 7 May 2012
Line 80:		Line 80:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci12 entry\|L9\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|		{{eeci12 entry\|L8\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|
	* Receding horizon control		* Receding horizon control
	* Distributed control		* Distributed control
	* 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\|		{{eeci12 entry\|L9\|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

Murray: /* Lecture Schedule */

2012-05-07T21:58:43Z

Lecture Schedule

← Older revision		Revision as of 21:58, 7 May 2012
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\|Verification of ~~Control Protocols~~\|		{{eeci12 entry\|L5\|RM\|Wed, 9:00\|Deductive Verification of Hybrid Systems\|
	* Brief introduction to ~~abstraction hierarchies for control~~ systems		* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)
	* Approaches: deductive ~~approaches~~, algorithmic ~~approaches~~		* Deductive verification using barrier certificates
	* (Guarded command languages and CCL)		* Guarded command languages and CCL for asynchronous control protocols
	* Lyapunov-based proof techniques
	* Deductive verification and barrier certificates
	* Examples: multi-agent systems, RoboFlag		* Examples: multi-agent systems, RoboFlag
	}}		}}

Murray: /* Lecture Schedule */

2012-05-07T19:42:48Z

Lecture Schedule

← Older revision		Revision as of 19:42, 7 May 2012
Line 21:		Line 21:
	The schedule below lists the lectures that will be given as part of the course. Each lecture will last approximately 90 minutes. The individual lecture pages give an overview of the lecture and links to additional information.		The schedule below lists the lectures that will be given as part of the course. Each lecture will last approximately 90 minutes. The individual lecture pages give an overview of the lecture and links to additional information.

	{\| border=1		{\|border=1 cellpadding=2
	\|-		\|-
	\| align=center \| Lec		\|align=center\|Lec
	\| align=center \| Date/time		\|align=center\|Date/time
	\| ~~ ~~ Title		\|Title
	\| Topics		\|Topics
	{{eeci12 entry\|L1 ~~<br>~~RM\|Mon, 9:00 \| Introduction: Protocol-Based Control Systems \|		{{eeci12 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 ~~<br>~~NW\|Mon, 11:00 \| Automata Theory \|		{{eeci12 entry\|L2\|NW\|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 ~~<br>~~UT\|Mon, 14:00 \| Temporal Logic \|		{{eeci12 entry\|L3\|UT\|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 ~~<br>~~NW\|Mon, 16:00 \| Model Checking and Logic Synthesis\|		{{eeci12 entry\|L4\|NW\|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 ~~<br>~~ RM\|Tue, 14:00<br>16:00\| Computer Session: Spin \|		{{eeci12 entry\|C1\|RM\|Tue, 14:00 <br> Tue, 16: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 ~~<br>~~ RM\|Wed, 9:00\| Verification of Control Protocols \|		{{eeci12 entry\|L5\|RM\|Wed, 9:00\|Verification of Control Protocols\|
	* Brief introduction to abstraction hierarchies for control systems		* Brief introduction to abstraction hierarchies for control systems
	* Approaches: deductive approaches, algorithmic approaches		* Approaches: deductive approaches, algorithmic approaches
Line 62:		Line 62:
	* Examples: multi-agent systems, RoboFlag		* Examples: multi-agent systems, RoboFlag
	}}		}}
	{{eeci12 entry\|L6 ~~<br>~~ UT\|Wed, 11:00\| Algorithmic Verification of Hybrid Systems\|		{{eeci12 entry\|L6\|UT\|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 69:		Line 69:
	* Examples: gear changing (?), ???		* Examples: gear changing (?), ???
	}}		}}
	{{eeci12 entry\|L7 ~~<br>~~ NW\|Wed, 14:00\| Synthesis of Reactive Control Protocols\|		{{eeci12 entry\|L7\|NW\|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 76:		Line 76:
	* Examples: runner-blocker		* Examples: runner-blocker
	}}		}}
	{{eeci12 entry\|C2 ~~<br>~~ NW\|Thu, 9:00~~ ~~<br>~~ ~~Thu, 11:00 \| Computer Session: TuLiP\|		{{eeci12 entry\|C2\|NW\|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 82:		Line 82:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci12 entry\|L9 ~~<br>~~ UT\|Fri, 9:00 \| Receding Horizon Temporal Logic Planning\|		{{eeci12 entry\|L9\|UT\|Fri, 9:00\|Receding Horizon Temporal Logic Planning\|
	* Receding horizon control		* Receding horizon control
	* Distributed control		* Distributed control
	* Examples: reactive motion planning, electric power systems (distributed)		* Examples: reactive motion planning, electric power systems (distributed)
	}}		}}
	{{eeci12 entry\|L10 ~~<br>~~ 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

Murray: /* Lecture Schedule */

2012-05-02T15:50:11Z

Lecture Schedule

← Older revision		Revision as of 15:50, 2 May 2012
Line 44:		Line 44:
	* Examples: traffic light, (RoboFlag), autonomous driving		* Examples: traffic light, (RoboFlag), autonomous driving
	}}		}}
	{{eeci12 entry\|L4 <br>UT\|Mon, 16:00 \| Model Checking and Logic Synthesis\|		{{eeci12 entry\|L4 <br>NW\|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
Line 62:		Line 62:
	* Examples: multi-agent systems, RoboFlag		* Examples: multi-agent systems, RoboFlag
	}}		}}
	{{eeci12 entry\|L6 <br> UT\|Wed, 11:00\| Algorithmic \|		{{eeci12 entry\|L6 <br> UT\|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

Murray: /* Lecture Schedule */

2012-05-02T15:47:31Z

Lecture Schedule

← Older revision		Revision as of 15:47, 2 May 2012
Line 82:		Line 82:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci12 entry\|L9 \|Fri, 9:00 ~~<br> UT~~ \| Receding Horizon Temporal Logic Planning\|		{{eeci12 entry\|L9 <br> UT\|Fri, 9:00 \| Receding Horizon Temporal Logic Planning\|
	* Receding horizon control		* Receding horizon control
	* Distributed control		* Distributed control

Murray: /* Lecture Schedule */

2012-05-02T15:46:05Z

Lecture Schedule

← Older revision		Revision as of 15:46, 2 May 2012
Line 27:		Line 27:
	\|   Title		\|   Title
	\| Topics		\| Topics
	{{eeci12 entry\|L1\|Mon, 9:00 \| Introduction: Protocol-Based Control Systems \|		{{eeci12 entry\|L1 <br>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\|Mon, 11:00 \| Automata Theory \|		{{eeci12 entry\|L2 <br>NW\|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
	* ~~Nondeterministic finite automata~~		* Linear time properties; safety and liveness
	* Buchi automata, Rabin automata (if time)
	* Examples: traffic light		* Examples: traffic light
	}}		}}
	{{eeci12 entry\|L3\|Mon, 14:00 \| Temporal Logic \|		{{eeci12 entry\|L3 <br>UT\|Mon, 14:00 \| Temporal Logic \|
	* Linear temporal ~~properties and LTL~~		* Linear temporal logic
	* ~~Safety and liveness~~ properties		* Omega regular properties
	* NBA ~~and DRA representations~~		* Buchi automata, representation of LTL using NBA
	* Examples: traffic light, RoboFlag		* Examples: traffic light, (RoboFlag), autonomous driving
	}}		}}
	{{eeci12 entry\|L4\|Mon, 16:00 \| Model Checking and Logic Synthesis\|		{{eeci12 entry\|L4 <br>UT\|Mon, 16:00 \| Model Checking and Logic Synthesis\|
	* Basic concepts in model checking		* Basic concepts in model checking
	* Buchi automata, representation of LTL using NBA
	* 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\|Tue, 14:00<br>16:00\| Computer Session: Spin \|		{{eeci12 entry\|C1 <br> RM\|Tue, 14:00<br>16: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\|Wed, 9:00 \| Verification of Control Protocols \|		{{eeci12 entry\|L5 <br> RM\|Wed, 9:00\| Verification of Control Protocols \|
	* Brief introduction to abstraction hierarchies for control systems		* Brief introduction to abstraction hierarchies for control systems
	* Approaches: deductive approaches, algorithmic approaches		* Approaches: deductive approaches, algorithmic approaches
Line 64:		Line 62:
	* Examples: multi-agent systems, RoboFlag		* Examples: multi-agent systems, RoboFlag
	}}		}}
	{{eeci12 entry\|L6\|Wed, 11:00 \| ~~Hybrid Systems Verification~~ \|		{{eeci12 entry\|L6 <br> UT\|Wed, 11:00\| Algorithmic \|
	* 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 71:		Line 69:
	* Examples: gear changing (?), ???		* Examples: gear changing (?), ???
	}}		}}
	{{eeci12 entry\|L7\|Wed, 14:00 \| Synthesis of Reactive Control Protocols\|		{{eeci12 entry\|L7 <br> NW\|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 78:		Line 76:
	* Examples: runner-blocker		* Examples: runner-blocker
	}}		}}
	{{eeci12 entry\|C2\|Thu, 9:00 <br> Thu, 11:00 \| Computer Session: TuLiP\|		{{eeci12 entry\|C2 <br> NW\|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 82:
	* Examples: reactive motion planning		* Examples: reactive motion planning
	}}		}}
	{{eeci12 entry\|L9\|Fri, 9:00 \| Receding Horizon Temporal Logic Planning\|		{{eeci12 entry\|L9 \|Fri, 9:00 <br> UT \| Receding Horizon Temporal Logic Planning\|
	* Receding horizon control		* Receding horizon control
	* Distributed control		* Distributed control
	* Examples: reactive motion planning, electric power systems (distributed)		* Examples: reactive motion planning, electric power systems (distributed)
	}}		}}
	{{eeci12 entry\|L10\|Fri, 11:00 \| Extensions, Applications, Open Questions \|		{{eeci12 entry\|L10 <br> 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

Murray: /* Lecture Schedule */

2012-05-02T15:30:12Z

Lecture Schedule

← Older revision		Revision as of 15:30, 2 May 2012
Line 57:		Line 57:
	}}		}}
	{{eeci12 entry\|L5\|Wed, 9:00 \| Verification of Control Protocols \|		{{eeci12 entry\|L5\|Wed, 9:00 \| Verification of Control Protocols \|
	* Brief introduction abstraction hierarchies for control systems		* Brief introduction to abstraction hierarchies for control systems
			* Approaches: deductive approaches, algorithmic approaches
	* (Guarded command languages and CCL)		* (Guarded command languages and CCL)
	* Lyapunov-based proof techniques		* Lyapunov-based proof techniques