Edit Course: HYCON-EECI, Spring 2012

Free text:

<table width="100%" cellspacing=0> <tr valign=top> <td rowspan=4 align=center> [[Image:eecilogo.png|90px]]</td> <td align=center><font color='blue' size='+2'>Specification, Design, and Verification <br> &nbsp;</font></td> <td rowspan=4 align=center"> [[Image:cdslogo.png|90px]]</td></tr> <tr><td align=center><font color='blue' size='+2'>of Networked Control Systems<br> &nbsp; </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> </table> __NOTOC__ == 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 == * 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) * Sponsor: [http://www.eeci-institute.eu/GSC2011 HYCON-EECI Graduate School on Control] == 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. {|border=1 cellpadding=2 |- |align=center|Lec |align=center|Date/time |Title |Topics {{eeci12 entry|L1|RM|Mon, 9:00|Introduction: Protocol-Based Control Systems| * Introduction to networked control systems (NCS) * Overview of control "protocols" * Examples: Alice, RoboFlag }} {{eeci12 entry|L2|NW|Mon, 11:00|Automata Theory| * Finite transition systems * Paths, traces and composition of finite transition systems * Linear time properties; safety and liveness * Examples: traffic light }} {{eeci12 entry|L3|UT|Mon, 14:00|Temporal Logic| * Linear temporal logic * Omega regular properties * Buchi automata, representation of LTL using NBA * Examples: traffic light, (RoboFlag), autonomous driving }} {{eeci12 entry|L4|NW|Mon, 16:00|Model Checking and Logic Synthesis| * Basic concepts in model checking * Use of model checking for logic synthesis * Examples: traffic light, farmer puzzle }} {{eeci12 entry|C1|RM|Tue, 14:00 <br> Tue, 16:00|Computer Session: Spin| * Introduction to Promela and Spin (statements, processes, messages) * Verification examples: traffic light, distributed traffic light, gcdrive * Synthesis examples: traffic light, farmer puzzle, robot navigation }} {{eeci12 entry|L5|RM|Wed, 9:00|Deductive Verification of Hybrid Systems| * Brief introduction to hybrid systems and verification techniques (deductive, algorithmic) * Deductive verification using barrier certificates * Guarded command languages and CCL for asynchronous control protocols * Examples: multi-agent systems, RoboFlag }} {{eeci12 entry|L6|UT|Wed, 11:00|Algorithmic Verification of Hybrid Systems| * Abstraction hierarchies for control systems * Finite state abstractions (discretization) and model checking * Discretization of continuous state systems * Approximate bi-simulation (if time) * Examples: gear changing (?), ??? }} {{eeci12 entry|L7|NW|Wed, 14:00|Synthesis of Reactive Control Protocols| * Open system and reactive system synthesis * Satisfiability, realizability * Game structures, reachability/safety games * Mu-calculus (if time) and GR(1) games * Examples: runner-blocker }} {{eeci12 entry|C2|NW|Thu, 9:00 <br> Thu, 11:00|Computer Session: TuLiP| * Introduction to TuLiP * Synthesis of protocols for discrete systems * Discretization of continuous systems (and protocol synthesis) * Examples: reactive motion planning }} {{eeci12 entry|L8|UT|Fri, 9:00|Receding Horizon Temporal Logic Planning| * Receding horizon control * Distributed control * Examples: reactive motion planning, electric power systems (distributed) }} {{eeci12 entry|L9|RM|Fri, 11:00|Extensions, Applications, Open Questions| * Review of control trends and course contents * Discussion of open problem areas and preliminary results ** Optimization-based techniques ** Probabilistic techniques ** Others: Robustness, switching systems, timed systems * Examples: robot motion planning, electric power systems (timed) }} |} == Software Installation == We will make use of two programs during the lab sessions: * [http://spinroot.com Spin] - model checker for formal verification of distributed systems * [http://tulip-control.sf.net 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 [http://spinroot.com/spin/Bin/index.html 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 [https://developer.apple.com/technologies/tools/ 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 [http://enthought.com Enthought Python distribution]. Once you have scipy installed, you will need to install several other python packages, including cvxopt and yices. A [http://sourceforge.net/apps/mediawiki/tulip-control/index.php?title=Main_Page list of required package] is available on the TuLiP project page. [[Category:Courses]] [[Category:2011-12 Courses]]