Formal Controller Synthesis via Genetic Programming

Abstract

<p>This paper presents an automatic controller synthesis method for nonlinear systems with reachability and safety specifications. The proposed method consists of genetic programming in combination with an SMT solver, which are used to synthesize both a control Lyapunov function and the modes of a switched state feedback controller. The resulting controller consists of a set of analytic expressions and a switching law based on the control Lyapunov function, which together guarantee the imposed specifications. The effectiveness of the proposed approach is shown on a 2D pendulum.</p>