Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
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.
Code (0)
등록된 구현이 없습니다.
Tasks
FormSimilar Papers 제목 키워드 기반
Data-Driven Abstraction-Based Control Synthesis
This paper studies formal synthesis of controllers for continuous-space systems with unknown dynamics to satisfy requirements expressed as linear temporal logic formulas. Formal abstraction-based synthesis schemes rely o…
Sampled-Data Controller Synthesis using Dissipative Linear Periodic Jump-Flow Systems with Design Applications
In this paper, we will propose linear-matrix-inequality-based techniques for the design of sampled-data controllers that render the closed-loop system dissipative with respect to \textcolor{blue}{quadratic supply functio…
Formal Synthesis of Analytic Controllers for Sampled-Data Systems via Genetic Programming
This paper presents an automatic formal controller synthesis method for nonlinear sampled-data systems with safety and reachability specifications. Fundamentally, the presented method is not restricted to polynomial syst…
LPV Delay-Dependent Sampled-Data Output-Feedback Control of Fueling in Spark Ignition Engines
We propose a delay-dependent sampled-data output-feedback LPV control technique to address the air-fuel ratio (AFR) regulation problem in spark ignition (SI) engines. AFR control and advanced fueling strategies are essen…
SchedulingProgram Synthesis Over Noisy Data with Guarantees
We explore and formalize the task of synthesizing programs over noisy data, i.e., data that may contain corrupted input-output examples. By formalizing the concept of a Noise Source, an Input Source, and a prior distribu…
Program Synthesis