TY - JOUR
T1 - Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
AU - Verdier, Cees Ferdinand
AU - Kochdumper, Niklas
AU - Althoff, Matthias
AU - Mazo, Manuel
N1 - Publisher Copyright:
© 2022 The Authors
PY - 2022/5
Y1 - 2022/5
N2 - 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.
AB - 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.
KW - Achievable controller performance
KW - Formal controller synthesis
KW - Optimal controller synthesis for systems with uncertainties
KW - Reachability analysis
KW - Temporal logic
UR - http://www.scopus.com/inward/record.url?scp=85124800673&partnerID=8YFLogxK
U2 - 10.1016/j.automatica.2022.110184
DO - 10.1016/j.automatica.2022.110184
M3 - Article
AN - SCOPUS:85124800673
SN - 0005-1098
VL - 139
JO - Automatica
JF - Automatica
M1 - 110184
ER -