Difference between revisions of "EECI-IGSC 2020"

From Murray Wiki
Jump to navigationJump to search
Line 5: Line 5:
<td rowspan=4 align=center"> [[Image:cdslogo.png|90px]]</td></tr>
<td rowspan=4 align=center"> [[Image:cdslogo.png|90px]]</td></tr>
<tr valign=top><td align=center><font color='blue' size='+0'>Richard M. Murray and Nok Wongpiromsarn</font></td></tr>
<tr valign=top><td align=center><font color='blue' size='+0'>Richard M. Murray and Nok Wongpiromsarn</font></td></tr>
<tr valign=top><td align=center><font color='blue' size='+0'>9-13 March 2012, Istanbul (Turkey)</font></td></tr>
<tr valign=top><td align=center><font color='blue' size='+0'>9-13 March 2020, Istanbul (Turkey)</font></td></tr>
</table> __NOTOC__
</table> __NOTOC__

Revision as of 20:56, 1 March 2020


Specification, Design, and Verification for Self-Driving Cars

Richard M. Murray and Nok Wongpiromsarn
9-13 March 2020, Istanbul (Turkey)

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 control protocols for autonomous systems, including self-driving cars. We combine methods from computer science (temporal logic, model checking, reactive synthesis) with those from control theory (abstraction methods, optimal control, invariants sets) 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 temporal logic and robust performance specifications.


The following papers and textbooks will be used heavily throughout the course:

Additional references for individual topics are included on the individual lecture pages.

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
Mon, 9:30 Welcome and course administration
Mon, 10:00 Course Introduction
  • Introduction to self-driving cars
  • Specifications and rules of the road
  • Architecture for self-driving (including layers)
  • Design problem, analysis/safety
Mon, 12:45 Automata Theory
  • Finite transition systems
  • Kripke structures
  • Automata classes (finite, Buchi, ND, etc)
  • Examples: stoplight, intersection
Mon, 14:15 Temporal Logic
  • Temporal logic
  • Linear time properties
  • LTL, STL
  • Examples: lane change, intersection
Mon, 15:45 Model Checking
  • LTL to Buchi automata
  • Ideas behind how model checkers work
  • Use for “open loop” synthesis
  • Examples: intersection
Tue, 8:30 Probabilistic Systems
  • Stochastic models: Markov chains, Markov decision processes
  • Sigma algebra
  • Reachability, regular safety and omega-regular properties
  • PCTL
Tue, 10:30 Computer Session: Stormpy
  • Probabilistic model checking
  • Probabilistic synthesis
  • TuLiP interface to stormpy
Tue, 14:15 Discrete Abstractions
  • Finite-state approximation of hybrid systems
  • Use of model checking for the verificatino of hybrid systems
  • Construction of finite-state abstractions for synthesis
Wed, 8:30 Reactive Synthesis
  • Assume/guarantee formalsms
  • Two-player, asymmetric games
  • Winning set computations, solving for strategies
  • Reading: WTM
  • Examples: runner-blocker, grid-world (parking lot, intersection)
Thu, 10:30 Computer Session: TuLiP
  • Simulation setup
  • TuLiP synthesis
Thu, 8:30 Minimum Violation Planning
  • Weighted automaton
  • Prioritized safety specification
  • Minimum violation planning problem and solution for finite state systems
  • Incremental sampling-based algorithm for continuous systems
Thu, 10:30 Computer Session: MVP
  • TBD
Fri, 9:00 Behaviour Specifications of Autonomous Vehicles
  • Challenges
  • Behavior specification using rulebooks
  • Singapore examples
Fri, 10:00 Safety-Critical Systems
  • Requirements for safety-critical control systems
  • Incorporating ML into autonomous sytems
  • Testing and evaluation
Fri, 11:00 Course Summary
  • Summary of key concepts from the course
  • Open issues for future research
  • Discussion

Software Installation

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

  • stormpy
  • 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: