Probably Approximate Safety Verification of Hybrid Dynamical Systems
Probably Approximate Safety Verification of Hybrid Dynamical Systems
复制标题
DOI：
10.1007/978-3-030-32409-4_15
复制
发表时间：
2019-11
影响因子：
12.7
通讯作者：
Bai Xue;M. Fränzle;Hengjun Zhao;N. Zhan;A. Easwaran
中科院分区：
文献类型：
--
作者：
Bai Xue;M. Fränzle;Hengjun Zhao;N. Zhan;A. Easwaran
在本文中，我们提出了一种基于线性规划的方法，该方法有助于对无限时间范围内受到扰动输入的混合动力系统进行可靠的安全验证。该验证算法应用了可能近似正确（PAC）学习框架，因此可以被视为统计形式验证，因为它提供了使用错误概率和置信度表示的形式安全保证。该框架中混合系统的安全性是通过计算所谓的 PAC 屏障证书来验证的，该证书可以通过解决线性规划问题来计算。基于场景方法，线性程序由一系列独立且同分布的状态样本构建。通过这种方式，我们可以对现有方法无法处理的混合动力系统进行验证。一些初步实验证明了我们方法的性能。
In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems subject to perturbation inputs over the infinite time horizon. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach.