黑箱连续时间动力系统的 PAC 模型检验
系统与控制
2020-07-21 v1 形式语言与自动机理论
系统与控制
摘要
本文在可能近似正确（PAC）学习的框架下，提出了一种用于黑箱连续时间动力学系统有限时间安全性验证的新型模型检验方法。黑箱动力学系统是指那些未给定模型，但对于给定输入，其在有限时间间隔内连续变化的状态可在某些离散时刻被观测到的系统。由于融入了以误差概率和置信度表述正确性保证的学习模型，该新模型检验方法被称为 PAC 模型检验。基于误差概率与置信水平，我们的方法提供了统计形式化的保证：黑箱动力学系统在有限时间域上的随时间演化轨迹落于学习模型加有界区间的范围内，从而有助于理解黑箱系统的可达性及其安全性要求的满足性。学习模型连同有界区间由情景优化获得，其归结为线性规划问题。三个例子展示了我们方法的性能。
引用
@article{arxiv.2007.10141,
title = {PAC Model Checking of Black-Box Continuous-Time Dynamical Systems},
author = {Bai Xue and Miaomiao Zhang and Arvind Easwaran and Qin Li},
journal= {arXiv preprint arXiv:2007.10141},
year = {2020}
}
备注
Accepted by IEEE TCAD. arXiv admin note: text overlap with arXiv:1207.1272 by other authors