Title
Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
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.
Year
DOI
Venue
2022
10.1016/j.automatica.2022.110184
Automatica
Keywords
DocType
Volume
Achievable controller performance,Optimal controller synthesis for systems with uncertainties,Formal controller synthesis,Temporal logic,Reachability analysis
Journal
139
Issue
ISSN
Citations 
1
0005-1098
0
PageRank 
References 
Authors
0.34
4
4
Name
Order
Citations
PageRank
Verdier Cees F.100.34
Kochdumper Niklas200.34
Matthias Althoff338350.89
Manuel Mazo Jr467349.71