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 dynamical control systems with state and control constraints, a cost, and correctness temporal logic specifications, generate an optimal control strategy that satisfies the specifications and the constraints.