EECI-IGSC 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.
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 Nok Wongpiromsarn (UT Austin/Iowa State)
- Date and location: 9-13 March 2020, Istanbul (Turkey)
- Sponsor: European Embedded Control Institute (EECI) Internataional 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.
Lec | Date/time | Title | Topics |
Mon,10:00 | Welcome and course administration | ||
L1 RM |
Mon, 10:30 | Course Introduction |
|
L2 RM |
Mon, 12:45 | Automata Theory |
|
L3 RM |
Mon, 14:15 | Temporal Logic |
|
L4 TW |
Mon, 15:45 | Model Checking |
|
L6 TW |
Tue, 8:30 | Probabilistic Systems |
|
C1 TW |
Tue, 10:30 | Computer Session: Stormpy |
|
L5 TW |
Tue, 14:15 | Discrete Abstractions |
|
L7 RM |
Wed, 8:30 | Reactive Synthesis |
|
C2 RM |
Thu, 10:30 | Computer Session: TuLiP |
|
L8 TW |
Thu, 8:30 | Minimum Violation Planning |
|
C3 TW |
Thu, 10:30 | Computer Session: MVP |
Minimum violation planning using TuLiP
|
L9 TW |
Fri, 9:00 | Behaviour Specifications of Autonomous Vehicles |
|
L10 RM |
Fri, 10:00 | Safety-Critical Systems |
|
L11 RM |
Fri, 11:00 | Course Summary |
|
Software Installation
We will make use of two programs during the lab sessions:
The above link provides instructions on how to install the software on your own. I highly recommend the use of virtual environments (either through python virtualenv or anaconda).
TuLiP (use the eeci2020 branch where minimum violation planning is implemented):
$ git clone https://github.com/tulip-control/tulip-control.git $ cd tulip-control $ git checkout eeci2020 $ pip install wheel $ pip install cvxopt $ pip install -r requirements.txt $ python setup.py install
polytope: Make sure you have version 0.2.2 or higher of polytope installed
$ python -c "import polytope; print(polytope.__version__)"
If the version is not '0.2.2' (possibly followed by some additional text, e.g., 0.2.2.dev0+f12c87a64641fed4d36a0fe904613495c434577d), then you need to install the latest version of polytope from source:
$ git clone https://github.com/tulip-control/polytope.git $ python setup.py install
matplotlib: matplotlib is not required for TuLiP but will be used in the course for visualization
$ pip install matplotlib
dot: dot is not required for TuLiP but is used for visualization. The dot program is part of the graphviz package available on most *nix systems. A typical way to install the package is to use the following command
$ sudo apt-get install graphviz
Stormpy: stormpy requires multiple packages, including carl, pycarl, z3 and storm. First, get all the required libraries. I summarize it here based on Ubuntu. (I tried it on Ubuntu18.04 but other versions should work too.)
$ sudo snap install cmake --classic $ sudo apt install build-essential libgmp3-dev libeigen3-dev libboost-all-dev libcln-dev ginac-tools autoconf glpk-utils hwloc libginac-dev automake libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev
carl:
$ git clone https://github.com/smtrat/carl.git $ cd carl $ git checkout master14 $ mkdir build && cd build $ cmake -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON .. $ make lib_carl
pycarl:
$ git clone https://github.com/moves-rwth/pycarl.git $ cd pycarl/ $ python setup.py develop
z3:
$ git clone https://github.com/Z3Prover/z3.git $ cd z3 $ python scripts/mk_make.py $ cd build $ make $ sudo make install
Note down where z3 is installed. If you use virtualenv, it should be something like venv_path/bin/z3 where venv_path is the path to the virtual environment.
storm:
$ git clone -b stable https://github.com/moves-rwth/storm.git $ cd storm $ export STORM_DIR=path_to_storm $ mkdir build $ cd build $ cmake -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON .. $ ccmake .. Change the followings: Z3_EXEC: venv_path/bin/z3 Z3_INCLUDE_DIR: venv_path/include Z3_LIBRARY: venv_path/lib/libz3.so $ make
stormpy:
$ git clone https://github.com/moves-rwth/stormpy.git $ cd stormpy $ git checkout 7ae4d0806edde02093d4f90ee25d381b344180ff $ python3 setup.py develop
Note that the last one has to be python3 even if in the virtual environment, python is a symbolic link to python3 already.