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

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

Verdier, C.F. (Hardt Hyperloop)
Kochdumper, Niklas (Technische Universität München)
Althoff, Matthias (Technische Universität München)
Mazo, M. (TU Delft Team Manuel Mazo Jr)

2022

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.

Achievable controller performance
Formal controller synthesis
Optimal controller synthesis for systems with uncertainties
Reachability analysis
Temporal logic

http://resolver.tudelft.nl/uuid:f25b9a4e-5ee7-42f1-8776-b93a50bc6495

https://doi.org/10.1016/j.automatica.2022.110184

0005-1098

Automatica, 139

Institutional Repository

journal article

© 2022 C.F. Verdier, Niklas Kochdumper, Matthias Althoff, M. Mazo