Dr. Belta of Boston University

In control theory, complex models of physical processes, such as systems of differential equations, are analyzed or controlled from simple specifications, such as stability and set invariance. In formal methods, rich specifications, such as formulae of temporal logics, are checked against simple models of software programs and digital circuits, such as finite transition systems. With the development and integration of cyber-physical and safety-critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications.

In this talk, I will discuss a set of approaches to the formal synthesis of control strategies for dynamical systems from temporal logic specifications. I will first show how automata games for finite systems can be extended to obtain conservative control strategies for low dimensional linear and multilinear dynamical systems. I will then present several methods to reduce conservativeness and improve the scalability of the control synthesis algorithms for more general classes of dynamics. I will illustrate the usefulness of these approaches with examples from robotics and traffic control.

Biography:

Dr. 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 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 an IEEE Fellow.

Email:

Address:United States