带 ReLU 神经网络控制器的随机系统形式化验证
系统与控制
2021-03-10 v1 机器学习
系统与控制
摘要
在本工作中，我们解决配备 ReLU 神经网络（NN）控制器的随机信息物理系统（CPS）的形式化安全验证问题。我们的目标是从初始状态集合中找出那些以预定置信度在指定时间范围内系统不会到达不安全配置的状态。具体而言，我们考虑带高斯噪声的离散时间 LTI 系统，并用合适的图对其进行抽象。然后，我们构造一个可满足性模凸（SMC）问题来估计图中节点间转移概率的上界。利用该抽象，我们提出一种方法来计算图中节点安全概率的紧界，尽管这些节点间转移概率可能存在过近似。此外，利用所提出的 SMC 公式，我们设计了一种启发式方法来细化系统的抽象，以进一步改进估计的安全界。最后，我们考虑一个机器人导航示例并与最先进验证方案进行比较，用仿真结果证实了所提方法的有效性。
引用
@article{arxiv.2103.05142,
title = {Formal Verification of Stochastic Systems with ReLU Neural Network Controllers},
author = {Shiqi Sun and Yan Zhang and Xusheng Luo and Panagiotis Vlantis and Miroslav Pajic and Michael M. Zavlanos},
journal= {arXiv preprint arXiv:2103.05142},
year = {2021}
}