Difference between revisions of "HYCON-EECI, Spring 2012"

From Murray Wiki
Jump to navigationJump to search
Line 27: Line 27:
|   Title  
|   Title  
| Topics
| Topics
{{eeci12 entry|L1|Tue, 9:00 | Introduction: Protocol-Based Control Systems |
{{eeci12 entry|L1|Mon, 9:00 | Introduction: Protocol-Based Control Systems |
* Introduction to networked control systems (NCS)
* Introduction to networked control systems (NCS)
* Examples: Alice, RoboFlag
* Examples: Alice, RoboFlag
}}
}}
{{eeci12 entry|L2|Tue, 10:30 | Automata Theory |L2_Automata_Theory-24Apr12.pdf|}}
{{eeci12 entry|L2|Mon, 11:00 | Automata Theory |L2_Automata_Theory-24Apr12.pdf|}}
{{eeci12 entry|L3|Tue, 13:30 | Temporal Logic |L3_ltl-24Apr12.pdf|}}
{{eeci12 entry|L3|Mon, 14:00 | Temporal Logic |L3_ltl-24Apr12.pdf|}}
{{eeci12 entry|L4|Tue, 15:30 | Model Checking and Logic Synthesis|L4_modelchecking-24Apr12.pdf|}}
{{eeci12 entry|L4|Mon, 16:00 | Model Checking and Logic Synthesis|L4_modelchecking-24Apr12.pdf|}}
{{eeci12 entry|C1|Wed, 8:30 | Computer Session: Spin |C1_spin-25Apr12.pdf|}}
{{eeci12 entry|C1|Tue, 14:00<br>16:00| Computer Session: Spin |
{{eeci12 entry|L5|Wed, 10:30 | Verification of Control Protocols |L5_protanal-25Apr12.pdf|}}
* Introduction to Promela and Spin
{{eeci12 entry|L6|Wed, 13:30 | Hybrid Systems Verification |L6_hybrid-25Apr12.pdf|}}
* Verification examples: traffic light, gcdrive
{{eeci12 entry|L7|Wed, 15:30 | Synthesis of Reactive Control Protocols |L7_reactive-25Apr12.pdf|}}
* Synthesis examples: traffic light, robot navigation
{{eeci12 entry|L8|Thu, 8:30 | Receding Horizon Temporal Logic Planning |L8_rhtlp-26Apr12.pdf|}}
}}
{{eeci12 entry|C2|Thu, 10:30 | Computer Session: TuLiP |C2_tulip-26Apr12.pdf|}}
{{eeci12 entry|L5|Wed, 9:00 | Verification of Control Protocols|
{{eeci12 entry|L9|Thu, 13:30 | Extensions, Applications, Open Questions |L9_extensions-26Apr12.pdf|}}
* Theorem proving techniques
}}
{{eeci12 entry|L6|Wed, 11:00 | Hybrid Systems Verification |L6_hybrid-25Apr12.pdf|}}
{{eeci12 entry|L7|Wed, 14:00 | Synthesis of Reactive Control Protocols |L7_reactive-25Apr12.pdf|}}
{{eeci12 entry|L8|Wed, 16:00 | Receding Horizon Temporal Logic Planning |
* Abstraction hierarchies for control systems
* Discretization of continuous state systems
}}
{{eeci12 entry|C2|Thu, 9:00&nbsp;<br>&nbsp;Thu, 11:00 | Computer Session: TuLiP |}}
{{eeci12 entry|L9|Fri, 9:00 | Receding Horizon Temporal Logic Planning |}}
{{eeci12 entry|L10|Fri, 11:00 | Extensions, Applications, Open Questions |}}
|-
|-
| &nbsp;  
| &nbsp;  

Revision as of 23:27, 29 April 2012

Eecilogo.png Specification, Design, and Verification
 
Cdslogo.png
of Distributed Embedded Systems
 

Richard M. Murray, Ufuk Topcu, and Nok Wongpiromsarn

14-18 May 2012, L'Aquila (Italy)

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.

Course information

Lecture Schedule

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.

Lec Date/time   Title Topics
L1
Mon, 9:00
Introduction: Protocol-Based Control Systems [[EECI 2012:
  • Introduction to networked control systems (NCS)
  • Examples: Alice, RoboFlag
  • Introduction to networked control systems (NCS)
  • Examples: Alice, RoboFlag

]]

{{{5}}}
L2
Mon, 11:00
Automata Theory L2_Automata_Theory-24Apr12.pdf
L3
Mon, 14:00
Temporal Logic L3_ltl-24Apr12.pdf
L4
Mon, 16:00
Model Checking and Logic Synthesis L4_modelchecking-24Apr12.pdf
C1
Tue, 14:00
16:00
Computer Session: Spin [[EECI 2012:
  • Introduction to Promela and Spin
  • Verification examples: traffic light, gcdrive
  • Synthesis examples: traffic light, robot navigation
  • Introduction to Promela and Spin
  • Verification examples: traffic light, gcdrive
  • Synthesis examples: traffic light, robot navigation

]]

{{{5}}}
L5
Wed, 9:00
Verification of Control Protocols [[EECI 2012:
  • Theorem proving techniques
  • Theorem proving techniques

]]

{{{5}}}
L6
Wed, 11:00
Hybrid Systems Verification L6_hybrid-25Apr12.pdf
L7
Wed, 14:00
Synthesis of Reactive Control Protocols L7_reactive-25Apr12.pdf
L8
Wed, 16:00
Receding Horizon Temporal Logic Planning [[EECI 2012:
  • Abstraction hierarchies for control systems
  • Discretization of continuous state systems
  • Abstraction hierarchies for control systems
  • Discretization of continuous state systems

]]

{{{5}}}
C2
Thu, 9:00 
 Thu, 11:00
Computer Session: TuLiP [[EECI 2012: |]] {{{5}}}
L9
Fri, 9:00
Receding Horizon Temporal Logic Planning [[EECI 2012: |]] {{{5}}}
L10
Fri, 11:00
Extensions, Applications, Open Questions [[EECI 2012: |]] {{{5}}}
  Thu, 3:00     Adjourn

Software Installation

We will make use of two programs during the lab sessions:

  • Spin - model checker for formal verification of distributed systems
  • TuLiP - python-based toolbox for temporal logic planning and controller synthesis

During the course, we will access these programs on a remote machine using ssh. For some parts of the course it will be useful to have a local installation of MATLAB that can be used for visualizing some simulation results.

If you would like to install the software on your own, here are some basic directions for installing the two packages:

  • Spin: if you are using Windows, you can download a binary installation. For Mac's, you need to compile from source. For this you will need a C compiler, such as the one that is part of the Xcode developer toolbox
  • TuLiP: you will need a python installation (2.6 or greater) with SciPy (0.9 or greater) installed. You might consider using the Enthought Python distribution. Once you have scipy installed, you will need to install several other python packages, including cvxopt and yices. A list of required package is available on the TuLiP project page.