| 摘要: |
| 连续动力系统安全验证是一个重要的研究问题, 多年来各类验证方法所能处理的问题规模非常受限. 对此, 对于给定的连续动力系统, 提出通过反例制导方法生成一组组合式概率近似正确(PAC)障碍证书的算法, 最终给出无限时间范畴安全验证问题在概率统计意义下的形式化描述. 通过建立和求解基于大M法的混合整数规划方法, 将障碍证书的求解转化为约束优化问题. 通过微分中值定理将非线性不等式进行区间线性化. 最后, 实现组合式PAC障碍证书生成工具CPBC, 并在11个基准系统上评估其性能. 实验结果表明, CPBC均能成功验证每个动力系统在指定不同的安全需求阈值下的安全性. 与现有方法相比, 所提方法可以更高效地为复杂系统或高维系统生成可靠的概率障碍证书, 验证的样例规模已高达百维. |
| 关键词: 连续动力系统 障碍证书 PAC 区间线性化 混合整数规划 |
| DOI：10.13328/j.cnki.jos.007176 |
| 分类号:TP311 |
| 基金项目:国家重点研发计划(2022YFA1005101); 国家自然科学基金(12171159, 62272397); 上海市可信工业互联网软件协同创新中心; “数字丝绸之路”上海市可信智能软件国际联合实验室项目(22510750100) |
|
| Compositional Probabilistic Barrier Certificate Generation Based on PAC Learning |
|
YANG Zi-Xuan1, ZENG Xia2, REN Meng-Xin3, WANG Jian-Lin3, ZENG Zhen-Bing4, YANG Zheng-Feng1
|
|
1.Software Engineering Institute, East China Normal University, Shanghai 200062, China;2.College of Computer and Information Science, Southwest University, Chongqing 400715, China;3.School of Computer and Information Engineering, Henan University, Kaifeng 475001, China;4.College of Sciences, Shanghai University, Shanghai 200444, China
|
| Abstract: |
| Continuous dynamical systems safety verification is an important research issue, and over the years, various verification methods have been very limited in the scale of the problems they can handle. For a given continuous dynamical system, this study proposes an algorithm to generate a set of compositional probably approximately correct (PAC) barrier certificates through a counterexample-guided approach. A formal description of the infinite-time domain safety verification problem is given in terms of probability and statistics. By establishing and solving a mixed-integer programming method based on the big-M method, the barrier certificate problem is transformed into a constrained optimization problem. Nonlinear inequalities are linearized in intervals using the mean value theorem of differentiation. Finally, this study implements the compositional PAC barrier certificate generator CPBC and evaluates its performance on 11 benchmark systems. The experimental results show that CPBC can successfully verify the safety of each dynamical system under specified different safety requirement thresholds. Compared with existing methods, the proposed method can more efficiently generate reliable probabilistic barrier certificates for complex or high-dimensional systems, with the verified example scale reaching up to hundreds of dimensions. |
| Key words: continuous dynamical system barrier certificate probably approximately correct (PAC) interval linearization mixed-integer programming |
