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

DOI10.1016/J.AUTOMATICA.2022.110184zbMATH Open1485.93338arXiv2006.04260OpenAlexW3033567324MaRDI QIDQ2116657FDOQ2116657

Niklas Kochdumper, M. jun. Mazo, Matthias Althoff, Cees Ferdinand Verdier

Publication date: 18 March 2022

Published in: Automatica (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2006.04260

Recommendations

• Robustly complete synthesis of sampled-data control for continuous-time nonlinear systems with reach-and-stay objectives
• Reactive synthesis from signal temporal logic specifications
• Duality-based nested controller synthesis from STL specifications for stochastic linear systems
• Formal controller synthesis from specifications given by discrete-time hybrid automata
• Formal Guarantees in Data-Driven Model Identification and Control Synthesis

zbMATH Keywords

reachability analysistemporal logicoptimal controller synthesis for systems with uncertaintiesachievable controller performanceformal controller synthesis

Mathematics Subject Classification ID

Attainable sets, reachability (93B03) Nonlinear systems in control theory (93C10) Sampled-data control/observation systems (93C57)

Cites Work

• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Title not available (Why is that?)
• Title not available (Why is that?)
• Reachability and Control Synthesis for Piecewise-Affine Hybrid Systems on Simplices
• Title not available (Why is that?)
• Verification and Control of Hybrid Systems
• Title not available (Why is that?)
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems
• δ-Complete Decision Procedures for Satisfiability over the Reals
• Synthesis of Reactive Switching Protocols From Temporal Logic Specifications
• Robustness of temporal logic specifications for continuous-time signals
• Utilizing dependencies to obtain subsets of reachable sets
• Reactive synthesis from signal temporal logic specifications
• Robust Satisfaction of Temporal Logic over Real-Valued Signals
• Formal methods for discrete-time dynamical systems
• Feedback Refinement Relations for the Synthesis of Symbolic Controllers
• Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
• STL model checking of continuous and hybrid systems
• Set-based control for disturbed piecewise affine systems with state and actuation constraints
• Feedback control strategies for multi-agent systems under a fragment of signal temporal logic tasks
• Formal Guarantees in Data-Driven Model Identification and Control Synthesis

Cited In (1)

• Data-driven abstraction-based control synthesis

Uses Software

• z3
• dReal
• CORA

This page was built for publication: Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2116657)