Optimization-based Formal Synthesis

Abstract: In control theory, complicated dynamics such as systems of (nonlinear) differential equations are mostly controlled to achieve stability.  This fundamental property is often linked with optimality, which requires minimization of a certain cost along the trajectories of a stable system. In formal synthesis, simple systems such as finite state transition graphs modeling computer programs or digital circuits are controlled from specifications such as safety, liveness, or richer requirements expressed as formulas of temporal logics. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for controlling complex systems from rich, temporal logic specifications. In this talk, I will introduce some recents results on the connection between optimal control and formal synthesis. Specifically, I will focus on the following problem: given a cost and a correctness temporal logic specification for a dynamical system, generate an optimal control strategy that satisfies the specification.  I will first briefly review automata-based methods, in which the dynamics of the system are mapped to a finite abstraction that is then controlled using an automaton corresponding to the specification.  I will then focus on optimization-based methods, which rely on mapping the specification and the dynamics to constraints of an optimization problem. I will illustrate the usefulness of these approaches with examples from robotics and traffic control.

Biography: Calin Belta is a Professor in the Department of Mechanical Engineering at Boston University, where he holds the Tegan Family Distinguished Faculty Fellowship. He is the Director of the BU Robotics Lab and of the Center for Autonomous and Robotic Systems (CARS), and is also affiliated with the Department of Electrical and Computer Engineering and the Division of Systems Engineering at Boston University. His research focuses on dynamics and control theory, with particular emphasis on hybrid and cyber-physical systems, formal synthesis and verification, and robotics.  He received the Air Force Office of Scientific Research Young Investigator Award and the National Science Foundation CAREER Award. He is a distinguished lecturer of the IEEE Control System Society and an IEEE Fellow.

Hosted by: Paul Bogdan