Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
From MaRDI portal
Publication:2116657
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.
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
Cites work
- scientific article; zbMATH DE number 3839814 (Why is no real title available?)
- scientific article; zbMATH DE number 3497315 (Why is no real title available?)
- scientific article; zbMATH DE number 795587 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems
- Feedback Refinement Relations for the Synthesis of Symbolic Controllers
- 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
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Formal methods for discrete-time dynamical systems
- Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
- Reachability and Control Synthesis for Piecewise-Affine Hybrid Systems on Simplices
- Reactive synthesis from signal temporal logic specifications
- Robust satisfaction of temporal logic over real-valued signals
- Robustness of temporal logic specifications for continuous-time signals
- STL model checking of continuous and hybrid systems
- Set-based control for disturbed piecewise affine systems with state and actuation constraints
- Synthesis of Reactive Switching Protocols From Temporal Logic Specifications
- Utilizing dependencies to obtain subsets of reachable sets
- Verification and Control of Hybrid Systems
- \(\delta \)-complete decision procedures for satisfiability over the reals
- dReal: an SMT solver for nonlinear theories over the reals
Cited in
(6)- Robustly complete synthesis of sampled-data control for continuous-time nonlinear systems with reach-and-stay objectives
- Data-driven abstraction-based control synthesis
- Duality-based nested controller synthesis from STL specifications for stochastic linear systems
- Controller synthesis against omega-regular specifications: a funnel-based control approach
- Automated formal synthesis of provably safe digital controllers for continuous plants
- Diagnosis and repair for synthesis from signal temporal logic specifications
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)
