基于障碍证书的随机系统数据驱动安全验证
系统与控制
2021-12-24 v1 系统与控制
摘要
本文提出一种数据驱动方法，用于形式化验证（潜在的）未知离散时间连续空间随机系统的安全性。所提出的框架基于障碍证书的概念以及从未知系统轨迹收集的数据。我们首先将基于障碍的安全验证重新表述为一个鲁棒凸问题（RCP）。一般而言，求解所获得的 RCP 是困难的，因为不仅系统状态存在于连续集合中，而且更成问题的是，未知模型出现在 RCP 的一个约束中。相反，我们利用有限数量的数据，并相应地将 RCP 转化为情景凸问题（SCP）。然后我们将 SCP 的优化器与 RCP 的优化器联系起来，从而以先验保证的置信度对未知随机系统提供安全保证。我们通过从系统轨迹收集采样数据，将我们的方法应用于一个未知的室温系统，并形式化验证房间温度在有限时间范围内以期望的置信度处于舒适区。
引用
@article{arxiv.2112.12709,
title = {Data-driven Safety Verification of Stochastic Systems via Barrier Certificates},
author = {Ali Salamati and Abolfazl Lavaei and Sadegh Soudjani and Majid Zamani},
journal= {arXiv preprint arXiv:2112.12709},
year = {2021}
}