EECI-IGSC 2020

	Specification, Design, and Verification for Self-Driving Cars
	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:

• 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
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	Computer Session: PRISM	TBD
L7 RM	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	Computer Session: TuLiP	Simulation setup TuLiP synthesis
L8 TW	Thu, 8:30	Minimum Violation Planning	TBD
C3 TW	Thu, 10:30	Computer Session: MVP	TBD
L9 TW	Fri, 9:00	Rulebooks	TBD
L10 RM	Fri, 10:00	Testing and evaluation	TBD
L11 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