随机微分动力学系统的无界时间安全性验证
动力系统
2020-06-04 v1 最优化与控制
摘要
在本文中，我们提出一种方法，用于界定随机微分方程（SDE）系统在无限时间范围内违反安全规范的概率上界。SDE 是随机过程的数学模型，刻画了状态如何随时间连续演化。它们广泛应用于众多领域，如工程系统（例如，建模行人在交叉路口的移动）、计算金融（例如，建模股票期权价格）以及生态过程（例如，种群随时间变化）。此前，安全性验证问题已通过多种不同方法在有限与无限时间范围内得到处理。本文的方法试图联结这两种视角：首先确定一个有限时间界，超过该界后安全违反概率可被一个可忽略的小数值界定。这是通过发现一个指数障碍证书来实现的，该证书证明了随时间呈指数收敛的安全违反概率上界。一旦找到有限时间间隔，便采用有限时间验证方法来界定该间隔内的违反概率。我们在文献中若干有趣的例子上演示了我们的方法，其中我们的方法可用于找到无限时间范围内安全性质违反概率的紧界。
引用
@article{arxiv.2006.01858,
title = {Unbounded-Time Safety Verification of Stochastic Differential Dynamics},
author = {Shenghua Feng and Mingshuai Chen and Bai Xue and Sriram Sankaranarayanan and Naijun Zhan},
journal= {arXiv preprint arXiv:2006.01858},
year = {2020}
}
备注
To appear in Proc. of CAV 2020