2012 edition of the EECI Graduate School
The program is available at www.eeci-institute.eu/EECI-docs2/EECI-Modules-2012.pdf.
Full information is available at www.eeci-institute.eu/GSC2012.
Specification, design and verification of distributed control systems
Professor Richard MURRAY and Dr Ufuk Topcu
California Institute of Technology - USA
Week 14-18 May, 2011
Summary: 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 distributed control systems .We combine methods from computer science (temporal logic, model checking, reactive synthesis) with those from dynamical systems and control (Lyapunov functions, sum-of-squares certificates, 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 that is designed for analyzing and synthesizing hybrid control systems using linear temporal logic and robust performance specifications. The following topics will be covered in the course:
- Transition systems and automata theory
- Specification of behavior using linear temporal logic
- Algebraic certificates for continuous and hybrid systems
- Approximation of continuous systems using discrete abstractions
- Verification of (asynchronous) control protocols using model checking
- Synthesis of control protocols and receding horizon temporal logic planning
- Case studies in autonomous navigation and vehicle management system