Caltech/AFRL, Spring 2012

	Specification, Design, and Verification
	of Networked Control Systems
	Richard M. Murray and Ufuk Topcu
	24-26 April 2012

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 networked control systems. We combine methods from computer science (temporal logic, model checking, synthesis of control protocols) with those from dynamical systems and control (Lyapunov functions, trajectory generation, receding horizon control) 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 linear temporal logic and robust performance specifications.

Course information

• Instructors: Richard M. Murray (Caltech, CDS) and Ufuk Topcu (Caltech, CDS)
• Date and location: 24-26 April 2012, Dayton, OH
• Sponsors: Air Force Research Laboratory (AFRL), Multi-Scale Systems Center (MuSyC), Boeing Corporation, United Technologies Corporation

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	Reaching
	Tue, 8:30	Registration
L1	Tue, 9:00	Introduction: Protocol-Based Control Systems
L2	Tue, 10:30	Automata Theory
L3	Tue, 13:30	Temporal Logic
L4	Tue, 15:30	Model Checking and Logic Synthesis
C1	Wed, 8:30	Computer Session: Spin
L5	Wed, 10:30	Verification of Control Protocols
L6	Wed, 13:30	Hybrid Systems Verification
L7	Wed, 15:30	Synthesis of Reactive Control Protocols
L8	Thu, 8:30	Receding Horizon Temporal Logic Planning
C2	Thu, 10:30	Computer Session: TuLiP
L9	Thu, 13:30	Extensions, Applications, Open Questions
	Thu, 3:00	Adjourn

Software Installation

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

• Spin model checker
• TuLiP temporal logic planning toolbox (python-based)