George Pappas: Temporal logic control of continuous systems

Abstract: Emebbeded systems, which merge information systems with physical systems, are ubiquitous. Computational systems operating in parallel with dynamical or control systems give rise to tremendous modeling and design challenges for the modern engineer. On one hand, control theory has historically focused on properties such as stability, controllability, and optimality. Advances in control theory usually focused on the complexity of the model, but not the complexity of the specification. Embedded systems require very novel, very challenging specifications that have to deal with synchronization, sequencing, and temporal ordering of different tasks. Mathematically formulating such desired specifications cannot be naturally described using traditional formulations in control theory. On the other hand, concurrency theory and formal verification have popularized the use of several temporal logics such as Linear Temporal Logic (LTL), and Computation Tree Logic (CTL) to describe such complex specifications. However, the emphasis has been on verification of these properties for purely discrete systems, and not on synthesis for systems with a continuous component.

In this talk, I will present an algorithmic approach for automatically synthesizing hybrid controllers for continuous systems in order to satisfy specifications that are expressed in temporal logics. In particular, given a controllable linear system, and a finite set of predicates in a special form, we present an algorithm that extracts a property-dependent, finite abstraction which is equivalent (bi-similar) to the original control system. This enables the use of algorithmic procedures for controller synthesis based on powerful automata theoretic techniques, bridging a semantic gap between control theoretic models and computer science specifications. The discrete controllers for the abstracted model are then formally refined to hybrid controllers for the original control system that are formally correct by construction. A Matlab implementation receives as inputs a control system, the temporal logic formula, and automatically generates a StateFlow/Simulink supervisor.

This is joint work with Paulo Tabuada and George Fainekos.