# Formal Synthesis of Analytic Controllers for Sampled-Data Systems via Genetic Programming

## TL;DR

This paper introduces an automated method using genetic programming to synthesize formal controllers for nonlinear sampled-data systems, ensuring safety and reachability, verified through SMT solvers, applicable beyond polynomial systems.

## Contribution

It develops a novel, generalizable genetic programming approach for synthesizing safety-critical controllers with formal guarantees for nonlinear sampled-data systems.

## Key findings

- Successfully synthesized controllers for multiple systems
- Verified correctness using SMT solvers
- Applicable to non-polynomial systems

## Abstract

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.