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

Cees Ferdinand Verdier, Niklas Kochdumper, Matthias Althoff, Manuel Mazo*

*Corresponding author for this work

Research output: Contribution to journalArticleScientificpeer-review

6 Downloads (Pure)

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.

Original languageEnglish
Article number110184
Number of pages13
JournalAutomatica
Volume139
DOIs
Publication statusPublished - 2022

Keywords

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

Fingerprint

Dive into the research topics of 'Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications'. Together they form a unique fingerprint.

Cite this