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 recent 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 talk about 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.
About Calin Belta
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.