Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications

TL;DR

This paper introduces a counterexample-guided synthesis method for designing closed-form sampled-data controllers for nonlinear systems that satisfy STL specifications over finite-time trajectories, using genetic programming and reachability analysis.

Contribution

It presents a novel framework combining genetic programming and reachability analysis for the formal synthesis of interpretable sampled-data controllers under STL constraints.

Findings

Successfully synthesized controllers for multiple nonlinear systems.

Controllers meet STL specifications over finite trajectories.

Closed-form controllers are suitable for embedded hardware.

Abstract

We propose a counterexample-guided inductive synthesis framework for the formal synthesis of closed-form sampled-data controllers for nonlinear systems to meet STL specifications over finite-time trajectories. Rather than stating the STL specification for a single initial condition, we consider an (infinite and bounded) set of initial conditions. Candidate solutions are proposed using genetic programming, which evolves controllers based on a finite number of simulations. Subsequently, the best candidate is verified using reachability analysis; if the candidate solution does not satisfy the specification, an initial condition violating the specification is extracted as a counterexample. Based on this counterexample, candidate solutions are refined until eventually a solution is found (or a user-specified number of iterations is met). The resulting sampled-data controller is expressed as a closed-form expression, enabling both interpretability and the implementation in embedded hardware with limited memory and computation power. The effectiveness of our approach is demonstrated for multiple systems.