EECI-IGSC 2020: Difference between revisions
No edit summary |
|||
Line 22: | Line 22: | ||
* Date and location: 18-22 May 2013, Belgrade (Serbia) | * Date and location: 18-22 May 2013, Belgrade (Serbia) | ||
* Sponsor: [http://www.eeci-institute.eu/GSC2013 HYCON-EECI Graduate School on Control] | * Sponsor: [http://www.eeci-institute.eu/GSC2013 HYCON-EECI Graduate School on Control] | ||
;; This buffer is for text that is not saved, and for Lisp evaluation. | |||
;; To create a file, visit it with C-x C-f and enter text in its buffer. | |||
== Lecture Schedule == | == Lecture Schedule == | ||
Line 33: | Line 37: | ||
|Title | |Title | ||
|Topics | |Topics | ||
{{ | {{eeci2020 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 | ||
}} | }} | ||
{{ | {{eeci2020 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 44: | Line 48: | ||
* Examples: traffic light | * Examples: traffic light | ||
}} | }} | ||
{{ | {{eeci2020 entry|L3|RM|Mon, 14:00|Temporal Logic| | ||
* Linear temporal logic | * Linear temporal logic | ||
* Omega regular properties | * Omega regular properties | ||
Line 50: | Line 54: | ||
* Examples: traffic light, (RoboFlag), autonomous driving | * Examples: traffic light, (RoboFlag), autonomous driving | ||
}} | }} | ||
{{ | {{eeci2020 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 | ||
}} | }} | ||
{{ | {{eeci2020 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 | ||
}} | }} | ||
{{ | {{eeci2020 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 66: | Line 70: | ||
* Examples: multi-agent systems, RoboFlag | * Examples: multi-agent systems, RoboFlag | ||
}} | }} | ||
{{ | {{eeci2020 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 73: | Line 77: | ||
* Examples: gear changing (?), ??? | * Examples: gear changing (?), ??? | ||
}} | }} | ||
{{ | {{eeci2020 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 80: | Line 84: | ||
* Examples: runner-blocker | * Examples: runner-blocker | ||
}} | }} | ||
{{ | {{eeci2020 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 | ||
}} | }} | ||
{{ | {{eeci2020 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 90: | Line 94: | ||
* Examples: reactive motion planning | * Examples: reactive motion planning | ||
}} | }} | ||
{{ | {{eeci2020 entry|L9|UT|Fri, 9:00|Advanced Topics| | ||
* Distributed protocols | * Distributed protocols | ||
* Switched systems | * Switched systems | ||
* Optimal synthesis | * Optimal synthesis | ||
}} | }} | ||
{{ | {{eeci2020 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 |
Revision as of 14:20, 5 December 2019
![]() |
Specification, Design, and Verification |
![]() |
of Networked Control Systems | ||
Richard M. Murray and Nok Wongpiromsarn | ||
9-13 March 2020, Instanbul |
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.
Reading
The following papers and textbooks will be used heavily throughout the course:
Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008.
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
- Instructors: Richard M. Murray (Caltech, CDS) and Ufuk Topcu (Caltech, CDS), and Nok Wongpiromsarn (MIT-Singapore)
- Date and location: 18-22 May 2013, Belgrade (Serbia)
- Sponsor: HYCON-EECI Graduate School on Control
- This buffer is for text that is not saved, and for Lisp evaluation.
- To create a file, visit it with C-x C-f and enter text in its buffer.
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 RM |
Mon, 9:00 | Introduction: Protocol-Based Control Systems |
|
L2 UT |
Mon, 11:00 | Automata Theory |
|
L3 RM |
Mon, 14:00 | Temporal Logic |
|
L4 UT |
Mon, 16:00 | Model Checking and Logic Synthesis |
|
C1 RM |
Tue, 9:00 Tue, 11:00 |
Computer Session: Spin |
|
L5 RM (1h) |
Wed, 9:00 | Deductive Verification of Hybrid Systems |
|
L6 UT (2h) |
Wed, 11:00 | Algorithmic Verification of Hybrid Systems |
|
L7 RM (2h) |
Wed, 14:00 | Synthesis of Reactive Control Protocols |
|
L8 UT(1h) |
Wed, 16:00 | Receding Horizon Temporal Logic Planning |
|
C2 UT |
Thu, 9:00 Thu, 11:00 |
Computer Session: TuLiP |
|
L9 UT |
Fri, 9:00 | Advanced Topics |
|
L10 RM |
Fri, 11:00 | Summary and Open Questions |
|
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.