Formal Synthesis of Optimal Neural Network Controllers

Abstract

Stability, safety and optimality are often sought-after properties in the field of controller synthesis. In the last century, linear control theory has matured to a level where scalable algorithms are widely available that are able to synthesize controllers with stability and optimality guarantee. However, the synthesis of safe controllers largely remains an open question. Furthermore, when nonlinear systems are considered, these methods often result in sub-optimal performance, or fail to provide a stabilizing solution at all. Current nonlinear controller synthesis methods typically lack stability, safety and/or optimality guarantee, or require computationally expensive online optimization. This thesis presents a novel method that is able to overcome these limitations. The presented controller synthesis method combines techniques from Approximate Dynamic Programming, Lyapunov theory and barrier theory, to synthesize an optimal controller in the form of a Neural Network. Alongside the controller a second Neural Network is deployed, which is trained to serve as a certificate function to provide stability and/or safety guarantee. To assure the correctness of the procedure, Satisfiability Modulo Theory and Counterexample-Guided Inductive Synthesis are utilized. We subject the method to a number of case studies, through which the versatility of the method is demonstrated. We show the method is able to work with linear and nonlinear systems, as well as systems with input and state constraints. Furthermore, we show the method yields controllers that are able to outperform linear controllers in terms of cost minimization.