Formal synthesis of analytic controllers

Abstract

Control design for modern safety-critical cyber-physical systems still requires significant expert-knowledge, since for general hybrid systems with temporal logic specifications there are no constructive methods. Nevertheless, in recent years multiple approaches have been proposed to automatically synthesize correct-by-construction controllers. However, typically these methods either result in enormous look-up tables, require online optimization, or are highly dependent on expert-knowledge. The goal of this thesis is to propose a novel approach that overcomes these limitations, i.e. to propose a framework for automatic controller synthesis, capable of synthesizing closed-form controllers for hybrid systems with temporal logic specifications, without a heavy reliance on expert-knowledge. To this end, we draw inspiration from the human design process and utilize two methods that show great similarities to it, namely evolutionary algorithms and counterexample-guided inductive synthesis (CEGIS). Specifically, we use genetic programming (GP), an evolutionary algorithm capable of evolving entire programs. This makes it possible to automatically discover the structure of a solution. Moreover, it enables the synthesis of compact closed-form controllers, circumventing the need for look-up tables or online optimization. In combination with GP, we use the concept of CEGIS to refine candidate solutions based on counterexamples, until the controller is guaranteed to satisfy the desired specification. In this thesis we propose two CEGIS-based synthesis frameworks, which differ in the employed verification paradigms, namely utilizing either (co-synthesized) Lyapunov-like functions or reachability analysis. Both frameworks result in correct-by-construction compact closed-form controllers, where the use of expert-knowledge is optional. Both frameworks are capable of synthesizing sampled-data controllers, enabling implementation in embedded hardware with limited memory and computation power, forming a stepping stone towards faster automation.