Caltech/AFRL, Spring 2012

From Murray Wiki
Jump to navigationJump to search
Cdslogo.png 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 Lecture notes
  Tue, 8:30     Registration
  L1     Tue, 9:00     Introduction: Protocol-Based Control Systems     L1_intro-24Apr12.pdf  
  L2     Tue, 10:30     Automata Theory     L2_Automata_Theory-24Apr12.pdf  
  L3     Tue, 13:30     Temporal Logic     L3_ltl-24Apr12.pdf  
  L4     Tue, 15:30     Model Checking and Logic Synthesis     L4_modelchecking-24Apr12.pdf  
  C1     Wed, 8:30     Computer Session: Spin     C1_spin-25Apr12.pdf  
  L5     Wed, 10:30     Verification of Control Protocols     L5_protanal-25Apr12.pdf  
  L6     Wed, 13:30     Hybrid Systems Verification     L6_hybrid-25Apr12.pdf  
  L7     Wed, 15:30     Synthesis of Reactive Control Protocols     L7_reactive-25Apr12.pdf  
  L8     Thu, 8:30     Receding Horizon Temporal Logic Planning     L8_rhtlp-26Apr12.pdf  
  C2     Thu, 10:30     Computer Session: TuLiP     C2_tulip-26Apr12.pdf  
  L9     Thu, 13:30     Extensions, Applications, Open Questions     L9_extensions-26Apr12.pdf  
  Thu, 3:00     Adjourn

Software Installation

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

  • Spin - model checker for formal verification of distributed systems
  • 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:

  • Spin: if you are using Windows, you can download a 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 Xcode developer toolbox
  • TuLiP: you will need a python installation (2.6 or greater) with SciPy (0.9 or greater) installed. You might consider using the Enthought Python distribution. Once you have scipy installed, you will need to install several other python packages, including cvxopt and yices. A list of required package is available on the TuLiP project page.