用于未知离散时间系统增量输入到状态稳定性的形式化验证神经网络控制器
系统与控制
2025-10-28 v2 系统与控制
摘要
本工作旨在合成一个控制器，确保未知离散时间系统是增量输入到状态稳定的（δ-ISS）。在本工作中，我们引入了 δ-ISS 控制 Lyapunov 函数（δ-ISS-CLF）的概念，该概念与控制器结合，确保闭环系统是增量 ISS 的。为了处理系统的未知动力学，我们将控制器以及 δ-ISS-CLF 参数化为神经网络，并利用未知系统状态空间的采样数据进行学习。为了形式化验证得到的 δ-ISS-CLF，我们开发了一个有效性条件，并将该条件纳入训练框架，以确保训练过程结束时具有可证明的正确性保证。最后，通过多个案例研究证明了所提出方法的有用性——第一个是具有非仿射非多项式结构的标量系统，第二个例子是单连杆操纵器系统，第三个系统是喷气发动机的非线性 Moore-Grietzer 模型，最后一个是旋转刚体航天器模型。
引用
@article{arxiv.2503.04129,
title = {Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems},
author = {Ahan Basu and Bhabani Shankar Dey and Pushpak Jagtap},
journal= {arXiv preprint arXiv:2503.04129},
year = {2025}
}