EECI-IGSC 2020: Difference between revisions

From Murray Wiki
Jump to navigationJump to search
No edit summary
No edit summary
Line 33: Line 33:
|Title  
|Title  
|Topics
|Topics
{{eeci2020 entry|L1|RM|Mon, 9:00|Introduction: Protocol-Based Control Systems|
{{eeci2020 entry|L1|RM|Mon, 9:00|Introduction: Design of Self-Driving Cars|
* Introduction to networked control systems (NCS)
* Introduction to self-driving cars
* Overview of control "protocols"
* Specifications and rules of the road
* Examples: Alice, RoboFlag
* Architecture for self-driving (including layers)
* Design problem, analysis/safety
}}
}}
{{eeci2020 entry|L2|UT|Mon, 11:00|Automata Theory|
{{eeci2020 entry|L2|RM|Mon, 10:00|Automata Theory|
* Finite transition systems
* Finite transition systems
* Paths, traces and composition of finite transition systems
* Kripke structures
* Linear time properties; safety and liveness
* Automata classes (finite, Buchi,  ND, etc)
* Examples: traffic light
* Examples: stoplight, intersection
 
}}
}}
{{eeci2020 entry|L3|RM|Mon, 14:00|Temporal Logic|
{{eeci2020 entry|L3|RM|Mon, 11:30|Temporal Logic|
* Linear temporal logic
* Temporal logic
* Omega regular properties
* Linear time properties
* Buchi automata, representation of LTL using NBA
* LTL, STL
* Examples: traffic light, (RoboFlag), autonomous driving
* Examples: lane change, intersection
 
}}
}}
{{eeci2020 entry|L4|UT|Mon, 16:00|Model Checking and Logic Synthesis|
{{eeci2020 entry|L4|TW|Mon, 14:00|Model Checking|
* Basic concepts in model checking
* LTL to Buchi automatat
* Use of model checking for logic synthesis
* Ideas behind how model checkers work
* Examples: traffic light, farmer puzzle
* Use for “open loop” synthesis (if time)
* Examples: intersection
}}
}}
{{eeci2020 entry|C1|RM|Tue, 9:00 <br> Tue, 11:00|Computer Session: Spin|
{{eeci2020 entry|L5|TW|Mon, 15:30|Discrete abstractions|
* Introduction to Promela and Spin (statements, processes, messages)
* Discrete abstractions
* Verification examples: traffic light, distributed traffic light, gcdrive
* Traces for continuous systems
* Synthesis examples: traffic light, farmer puzzle, robot navigation
* Trace-inclusive abstractions
* Reading: WTM, RRT* paper
* Examples: gridworld, intersection
}}
}}
{{eeci2020 entry|L5|RM (1h)|Wed, 9:00|Deductive Verification of Hybrid Systems|
{{eeci2020 entry|L6|TW|Tue, 8:30|Probabilistic systems|
* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)
* MDP w/ properties
* Deductive verification using barrier certificates
* Computing probabilities of formulas
* Guarded command languages and CCL for asynchronous control protocols
* Probabilistic model checking (MDPs)
* Examples: multi-agent systems, RoboFlag
* Probabilistic synthesis
* Intro to PRISM (or Storm)
* Reading: B&K, Ch  10
}}
}}
{{eeci2020 entry|L6|UT (2h)|Wed, 11:00|Algorithmic Verification of Hybrid Systems|
{{eeci2020 entry|C1|RM|Tue, 10:30 <br> Tue, 11:00|Computer Session: PRISM|
* Abstraction hierarchies for control systems
* TBD
* Finite state abstractions (discretization) and model checking
* Discretization of continuous state systems
* Approximate bi-simulation (if time)
* Examples: gear changing (?), ???
}}
}}
{{eeci2020 entry|L7|RM (2h)|Wed, 14:00|Synthesis of Reactive Control Protocols|
{{eeci2020 entry|L7|RM (2h)|Wed, 8:30|Synthesis of Reactive Control Protocols|
* Open system and reactive system synthesis
* Assume/guarantee formalsms
* Satisfiability, realizability
* Two-player, asymmetric games
* Game structures, reachability/safety games
* Winning set computations, solving for strategies
* Mu-calculus (if time) and GR(1) games
* Reading: WTM
* Examples: runner-blocker
* Examples: runner-blocker, grid-world (parking lot, intersection)
}}
}}
{{eeci2020 entry|L8|UT(1h)|Wed, 16:00|Receding Horizon Temporal Logic Planning|
{{eeci2020 entry|C2|RM|Thu, 10:30 <br> Thu, 11:00|Computer Session: TuLiP|
* Receding horizon control
* Simulation setup
* Examples: reactive motion planning
* TuLiP synthesis
}}
}}
{{eeci2020 entry|C2|UT|Thu, 9:00 <br> Thu, 11:00|Computer Session: TuLiP|
{{eeci2020 entry|L7|TW|Thu, 8:30|Minimum Violation Planning|
* Introduction to TuLiP
* TBD
* Synthesis of protocols for discrete systems
* Discretization of continuous systems (and protocol synthesis)
* Examples: reactive motion planning
}}
}}
{{eeci2020 entry|L9|UT|Fri, 9:00|Advanced Topics|
{{eeci2020 entry|C2|TW|Thu, 10:30 <br> Thu, 11:00|Computer Session: MVP|
* Distributed protocols
* TBD
* Switched systems
* Optimal synthesis
}}
}}
{{eeci2020 entry|L10|RM|Fri, 11:00|Summary and Open Questions|
{{eeci2020 entry|L9|TW|Fri, 9:00|Rulebooks|
* Review of control trends and course contents
* TBD
* Discussion of open problem areas and preliminary results
}}
** Optimization-based techniques
{{eeci2020 entry|L10|RM|Fri, 10:00|Testing and evaluation|
** Probabilistic techniques
* TBD
** Others: Robustness, switching systems, timed systems
}}
* Examples: robot motion planning, electric power systems (timed)
{{eeci2020 entry|L10|RM|Fri, 11:00|Incorporating ML|
* TBD
}}
}}
|}
|}
Line 108: Line 108:


We will make use of two programs during the lab sessions:
We will make use of two programs during the lab sessions:
* [http://spinroot.com Spin] - model checker for formal verification of distributed systems
* PRISM/Storm
* [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.
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:
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]
* Storm: TBD
* 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.
* TuLiP: TBD


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

Revision as of 03:25, 3 February 2020

Eecilogo.png Specification, Design, and Verification for Self-Driving Cars
 		 Cdslogo.png
of Networked Control Systems
 

Richard M. Murray and Nok Wongpiromsarn

9-13 March 2012, 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
L1
RM 		Mon, 9:00 Introduction: Design of Self-Driving Cars
  • Introduction to self-driving cars
  • Specifications and rules of the road
  • Architecture for self-driving (including layers)
  • Design problem, analysis/safety
L2
RM 		Mon, 10:00 Automata Theory
  • Finite transition systems
  • Kripke structures
  • Automata classes (finite, Buchi, ND, etc)
  • Examples: stoplight, intersection


L3
RM 		Mon, 11:30 Temporal Logic
  • Temporal logic
  • Linear time properties
  • LTL, STL
  • Examples: lane change, intersection


L4
TW 		Mon, 14:00 Model Checking
  • LTL to Buchi automatat
  • Ideas behind how model checkers work
  • Use for “open loop” synthesis (if time)
  • Examples: intersection
L5
TW 		Mon, 15:30 Discrete abstractions
  • Discrete abstractions
  • Traces for continuous systems
  • Trace-inclusive abstractions
  • Reading: WTM, RRT* paper
  • Examples: gridworld, intersection
L6
TW 		Tue, 8:30 Probabilistic systems
  • MDP w/ properties
  • Computing probabilities of formulas
  • Probabilistic model checking (MDPs)
  • Probabilistic synthesis
  • Intro to PRISM (or Storm)
  • Reading: B&K, Ch 10
C1
RM 		Tue, 10:30
Tue, 11:00 		Computer Session: PRISM
  • TBD
L7
RM (2h) 		Wed, 8:30 Synthesis of Reactive Control Protocols
  • 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
Thu, 11:00 		Computer Session: TuLiP
  • Simulation setup
  • TuLiP synthesis
L7
TW 		Thu, 8:30 Minimum Violation Planning
  • TBD
C2
TW 		Thu, 10:30
Thu, 11:00 		Computer Session: MVP
  • TBD
L9
TW 		Fri, 9:00 Rulebooks
  • TBD
L10
RM 		Fri, 10:00 Testing and evaluation
  • TBD
L10
RM 		Fri, 11:00 Incorporating ML
  • TBD

Software Installation

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

  • PRISM/Storm
  • 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:

  • Storm: TBD
  • TuLiP: TBD
Retrieved from "https://murray.cds.caltech.edu/index.php?title=EECI-IGSC_2020&oldid=23331"