Abstract

A cyber-physical system (CPS) integrates computation and communication with
the control of physical processes. 
CPSs are ubiquitous: for example, automotive control systems, medical devices, energy grids, etc are all examples of CPSs. An important question is to come up with a cost effective yet high confidence design and verification methodology for these systems. This is a very broad problem. In this sequence of lectures, we focus on one particular aspect: design of reactive controllers for CPSs from declarative specifications. In particular, we describe the basis of a control design
technique called abstraction-based control design (ABCD). In ABCD, one abstracts a continuous-state, time-sampled dynamical system into a finite 2-person game and uses reactive synthesis algorithms from finite-state games. A strategy extracted from the finite game can be refined to a controller for the original system. We shall describe the basics of reactive synthesis, starting with basic algorithms for safety and reachability games, and going on to describing general algorithms using the mu-calculus, showing how abstraction works, and how ABCD can be optimized using multi-level abstractions. Along the way, we show connections to foundational questions in logic and automata theory.