基于障碍证书的数据驱动随机系统验证与综合
系统与控制
2023-09-12 v2 系统与控制
摘要
在本工作中,我们研究未知离散时间随机系统上安全性规范的验证与综合问题。当系统模型可用时,障碍证书已成功用于确保安全性规范的满足。在本工作中,我们将障碍证书的计算表述为一个鲁棒凸规划(RCP)。一般而言,求解所得的 RCP 是困难的,因为出现在 RCP 某一约束中的系统模型是未知的。我们提出一种数据驱动方法,通过对系统轨迹抽取有限多个随机样本,将 RCP 中不可数无穷多的约束替换为有限多个约束。我们从而将原始 RCP 替换为场景凸规划(SCP),并展示如何关联二者的优化解。我们保证当样本数量大于一个预先计算的值时,SCP 的解以先验保证的置信度是 RCP 的解。这为原始未知系统提供了安全概率的下界,并在综合情形下附带一个控制器。我们还讨论了将验证方法推广到关联鲁棒规划为非凸的情况,并展示如何应用类似方法。最后,通过三个案例研究说明了所提方法的适用性。
引用
@article{arxiv.2111.10330,
title = {Data-driven verification and synthesis of stochastic systems via barrier certificates},
author = {Ali Salamati and Abolfazl Lavaei and Sadegh Soudjani and Majid Zamani},
journal= {arXiv preprint arXiv:2111.10330},
year = {2023}
}