Formal Synthesis of Analytic Controllers for Sampled-Data Systems via Genetic Programming
This addresses the challenge of formal controller synthesis for nonlinear systems, which is incremental as it builds on existing methods like genetic programming and SMT solvers.
The paper tackles the problem of automatically synthesizing controllers for nonlinear sampled-data systems with safety and reachability specifications, using genetic programming to generate Control Lyapunov Barrier-like functions and controller modes, with correctness verified via a Satisfiability Modulo Theories solver, and demonstrates effectiveness on multiple systems.
This paper presents an automatic formal controller synthesis method for nonlinear sampled-data systems with safety and reachability specifications. Fundamentally, the presented method is not restricted to polynomial systems and controllers. We consider periodically switched controllers based on a Control Lyapunov Barrier-like functions. The proposed method utilizes genetic programming to synthesize these functions as well as the controller modes. Correctness of the controller are subsequently verified by means of a Satisfiability Modulo Theories solver. Effectiveness of the proposed methodology is demonstrated on multiple systems.