arXiv:2607.08899eess.SYcs.LG2026-07

用梯度优化与集合可达性验证,为非线性系统设计鲁棒参数。

Learning-enabled Parameter Synthesis for Nonlinear Systems from Signal Temporal Logic

  • 结合梯度优化与集合可达性验证,高效搜索高维参数空间。
  • 在18维参数下仍能保证连续时间STL规范的可满足性。
  • 适合需要形式化验证的控制系统参数设计场景。

信号时序逻辑(STL)被越来越多地用于描述最优控制和学习方法中的可解释目标与约束,尤其在缺乏目标时间序列数据时。本文提出一种方法,为非线性系统合成参数,使其在不确定初始条件下,仍能鲁棒地满足连续时间STL规范。为此,我们采用基于梯度的优化,并结合基于集合的可达性验证,在高维参数空间中高效学习,同时为优化后的参数提供可证明的满足性保证。我们在三个系统上验证了该方法的有效性与可扩展性,参数维度最高达18维。

原文摘要 · Abstract (English)

Signal Temporal Logic (STL) is increasingly used to describe interpretable objectives and constraints for optimal control and learning methods, especially when no target time series data is available. In this work, we propose to synthesize parameters for nonlinear systems that robustly satisfy continuous-time STL specifications for uncertain initial conditions. To this end, we use gradient-based optimization along with set-based reachability verification to efficiently learn in high-dimensional parameter spaces while providing provable satisfaction guarantees for the optimized parameters. We demonstrate the effectiveness and scalability of our method on three systems with up to 18 parameter dimensions.

非线性系统形式化验证参数合成

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。