论文标题
在STL规格下，非线性连续时间系统的封闭形式采样数据控制器的形式合成
Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
论文作者
论文摘要
我们提出了一个反例引导的感应合成框架，用于非线性系统的封闭形式采样DATA控制器的形式合成，以满足有限时间轨迹的STL规格。我们没有考虑单个初始条件的STL规范，而是考虑一组（无限和有限的）初始条件。使用遗传编程提出了候选解决方案，该解决方案是根据有限数量的模拟来进化控制器的。随后，使用可及性分析对最佳候选人进行了验证。如果候选解决方案不满足规范，则将违反规范提取的初始条件作为反例提取。基于此反例子，将完善候选解决方案，直到最终找到解决方案（或者满足用户指定的迭代次数）。所得的采样数据控制器表示为封闭形式的表达式，可解释性和在嵌入式硬件中具有有限的内存和计算功率的实现。对于多个系统，我们的方法的有效性得到了证明。
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.
