Difference between revisions of "EECI-IGSC 2020"

From Murray Wiki
Jump to navigationJump to search
 
(41 intermediate revisions by 2 users not shown)
Line 1: Line 1:
<table width="100%" cellspacing=0>
<table width="100%" cellspacing=0>
<tr valign=top>
<tr valign=middle>
<td rowspan=4 align=center> [[Image:eecilogo.png|90px]]</td>
<td rowspan=4 align=center> [[Image:eecilogo.png|90px]]</td>
<td align=center><font color='blue' size='+2'>Specification, Design, and Verification for Self-Driving Cars <br> &nbsp;</font></td>
<td align=center><font color='blue' size='+2'><p>Specification, Design, and Verification for Self-Driving Cars</p> </font></td>
<td rowspan=4 align=center"> [[Image:cdslogo.png|90px]]</td></tr>
<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'>Richard M. Murray and Nok Wongpiromsarn</font></td></tr>
<tr valign=top><td align=center><font color='blue' size='+0'><p> Richard M. Murray and Nok Wongpiromsarn </p></font></td></tr>
<tr valign=top><td align=center><font color='blue' size='+0'>9-13 March 2020, Istanbul (Turkey)</font></td></tr>
<tr valign=top><td align=center><font color='blue' size='+0'><p>9-13 March 2012, Istanbul (Turkey)</p></font></td></tr>
</table> __NOTOC__
</table> __NOTOC__


Line 33: Line 32:
|Title  
|Title  
|Topics
|Topics
{{eeci2020 entry|L1|RM|Mon, 9:00|Introduction: Design of Self-Driving Cars|
|-
|
| Mon,10:00
| Welcome and course administration
|
{{eeci2020 entry|L1|RM|Mon, 10:30|Course Introduction|
* Introduction to self-driving cars
* Introduction to self-driving cars
* Specifications and rules of the road
* Specifications and rules of the road
Line 39: Line 43:
* Design problem, analysis/safety
* Design problem, analysis/safety
}}
}}
{{eeci2020 entry|L2|RM|Mon, 10:00|Automata Theory|
{{eeci2020 entry|L2|RM|Mon, 12:45|Automata Theory|
* Finite transition systems
* Finite transition systems
* Kripke structures
* Kripke structures
* Automata classes (finite, Buchi,  ND, etc)
* Automata classes (finite, Buchi,  ND, etc)
* Examples: stoplight, intersection
* Examples: stoplight, intersection
}}
}}
{{eeci2020 entry|L3|RM|Mon, 11:30|Temporal Logic|
{{eeci2020 entry|L3|RM|Mon, 14:15|Temporal Logic|
* Temporal logic
* Temporal logic
* Linear time properties
* Linear time properties
* LTL, STL
* LTL, STL
* Examples: lane change, intersection
* Examples: lane change, intersection
}}
}}
{{eeci2020 entry|L4|TW|Mon, 14:00|Model Checking|
{{eeci2020 entry|L4|TW|Mon, 15:45|Model Checking|
* LTL to Buchi automatat
* LTL to Buchi automata
* Ideas behind how model checkers work
* Ideas behind how model checkers work
* Use for “open loop” synthesis (if time)
* Use for “open loop” synthesis
* Examples: intersection
* Examples: intersection
}}
}}
{{eeci2020 entry|L5|TW|Mon, 15:30|Discrete abstractions|
{{eeci2020 entry|L6|TW|Tue, 8:30|Probabilistic Systems|
* Discrete abstractions
* Stochastic models: Markov chains, Markov decision processes
* Traces for continuous systems
* Sigma algebra
* Trace-inclusive abstractions
* Reachability, regular safety and omega-regular properties
* Reading: WTM, RRT* paper
* PCTL
* Examples: gridworld, intersection
}}
}}
{{eeci2020 entry|L6|TW|Tue, 8:30|Probabilistic systems|
{{eeci2020 entry|C1|TW|Tue, 10:30|Computer Session: Stormpy|
* MDP w/ properties
* Probabilistic model checking
* Computing probabilities of formulas
* Probabilistic model checking (MDPs)
* Probabilistic synthesis
* Probabilistic synthesis
* Intro to PRISM (or Storm)
* TuLiP interface to stormpy
* Reading: B&K, Ch  10
}}
}}
{{eeci2020 entry|C1|RM|Tue, 10:30|Computer Session: PRISM|
{{eeci2020 entry|L5|TW|Tue, 14:15|Discrete Abstractions|
* TBD
* Finite-state approximation of hybrid systems
* Use of model checking for the verificatino of hybrid systems
* Construction of finite-state abstractions for synthesis
}}
}}
{{eeci2020 entry|L7|RM|Wed, 8:30|Synthesis of Reactive Control Protocols|
{{eeci2020 entry|L7|RM|Wed, 8:30|Reactive Synthesis|
* Assume/guarantee formalsms
* Assume/guarantee formalsms
* Two-player, asymmetric games
* Two-player, asymmetric games
Line 84: Line 84:
* Examples: runner-blocker, grid-world (parking lot, intersection)
* Examples: runner-blocker, grid-world (parking lot, intersection)
}}
}}
{{eeci2020 entry|C2|RM|Thu, 10:30 <br> Thu, 11:00|Computer Session: TuLiP|
{{eeci2020 entry|C2|RM|Thu, 10:30|Computer Session: TuLiP|
* Simulation setup
* Simulation setup
* TuLiP synthesis
* TuLiP synthesis
}}
}}
{{eeci2020 entry|L8|TW|Thu, 8:30|Minimum Violation Planning|
{{eeci2020 entry|L8|TW|Thu, 8:30|Minimum Violation Planning|
* TBD
* Weighted automaton
* Prioritized safety specification
* Minimum violation planning problem and solution for finite state systems
* Incremental sampling-based algorithm for continuous systems
}}
}}
{{eeci2020 entry|C3|TW|Thu, 10:30 <br> Thu, 11:00|Computer Session: MVP|
{{eeci2020 entry|C3|TW|Thu, 10:30|Computer Session: MVP|
* TBD
Minimum violation planning using TuLiP
* Defining system and prioritized safety specification
* Solving minimum violation planning problem
}}
}}
{{eeci2020 entry|L9|TW|Fri, 9:00|Rulebooks|
{{eeci2020 entry|L9|TW|Fri, 9:00|Behaviour Specifications of Autonomous Vehicles|
* TBD
* Challenges
* Behavior specification using rulebooks
* Singapore examples
}}
}}
{{eeci2020 entry|L10|RM|Fri, 10:00|Testing and evaluation|
{{eeci2020 entry|L10|RM|Fri, 10:00|Safety-Critical Systems|
* TBD
* Requirements for safety-critical control systems
* Incorporating ML into autonomous sytems
* Testing and evaluation
}}
}}
{{eeci2020 entry|L11|RM|Fri, 11:00|Incorporating ML|
{{eeci2020 entry|L11|RM|Fri, 11:00|Course Summary|
* TBD
* Summary of key concepts from the course
* Open issues for future research
* Discussion
}}
}}
|}
|}
Line 108: Line 119:


We will make use of two programs during the lab sessions:
We will make use of two programs during the lab sessions:
* PRISM/Storm
* [https://moves-rwth.github.io/stormpy stormpy]
* [http://tulip-control.sf.net TuLiP] - python-based toolbox for temporal logic planning and controller synthesis
* [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.
The above link provides instructions on how to install the software on your own. I highly recommend the use of virtual environments (either through [https://packaging.python.org/guides/installing-using-pip-and-virtual-environments/ python virtualenv] or [https://docs.conda.io/projects/conda/en/latest/user-guide/tasks/manage-environments.html 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


If you would like to install the software on your own, here are some basic directions for installing the two packages:
Note that the last one has to be python3 even if in the virtual environment, python is a symbolic link to python3 already.
* Storm: TBD
* TuLiP: TBD


[[Category:Courses]]
[[Category:Courses]]
[[Category:2019-20 Courses]]
[[Category:2019-20 Courses]]

Latest revision as of 13:15, 8 April 2020

Eecilogo.png

Specification, Design, and Verification for Self-Driving Cars

Cdslogo.png
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:

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,10:00 Welcome and course administration
L1
RM
Mon, 10:30 Course Introduction
  • Introduction to self-driving cars
  • Specifications and rules of the road
  • Architecture for self-driving (including layers)
  • Design problem, analysis/safety
L2
RM
Mon, 12:45 Automata Theory
  • Finite transition systems
  • Kripke structures
  • Automata classes (finite, Buchi, ND, etc)
  • Examples: stoplight, intersection
L3
RM
Mon, 14:15 Temporal Logic
  • Temporal logic
  • Linear time properties
  • LTL, STL
  • Examples: lane change, intersection
L4
TW
Mon, 15:45 Model Checking
  • LTL to Buchi automata
  • Ideas behind how model checkers work
  • Use for “open loop” synthesis
  • Examples: intersection
L6
TW
Tue, 8:30 Probabilistic Systems
  • Stochastic models: Markov chains, Markov decision processes
  • Sigma algebra
  • Reachability, regular safety and omega-regular properties
  • PCTL
C1
TW
Tue, 10:30 Computer Session: Stormpy
  • Probabilistic model checking
  • Probabilistic synthesis
  • TuLiP interface to stormpy
L5
TW
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
L7
RM
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)
C2
RM
Thu, 10:30 Computer Session: TuLiP
  • Simulation setup
  • TuLiP synthesis
L8
TW
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
C3
TW
Thu, 10:30 Computer Session: MVP

Minimum violation planning using TuLiP

  • Defining system and prioritized safety specification
  • Solving minimum violation planning problem
L9
TW
Fri, 9:00 Behaviour Specifications of Autonomous Vehicles
  • Challenges
  • Behavior specification using rulebooks
  • Singapore examples
L10
RM
Fri, 10:00 Safety-Critical Systems
  • Requirements for safety-critical control systems
  • Incorporating ML into autonomous sytems
  • Testing and evaluation
L11
RM
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

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.