Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications. (May 2022)

• Record Type: Journal Article
• Authors: Verdier, Cees Ferdinand; Kochdumper, Niklas; Althoff, Matthias; Mazo, Manuel
• Is Part Of: Automatica. Volume 139(2022)
• Publication Date: 2022-05
• Subjects: Achievable controller performance -- Optimal controller synthesis for systems with uncertainties -- Formal controller synthesis -- Temporal logic -- Reachability analysis; Automatic control -- Periodicals; Automation -- Periodicals; 629.805
• DOI: 10.1016/j.automatica.2022.110184
• Languages: English
• ISSNs: 0005-1098

Abstract

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.