基于PAC学习的组合式概率障碍证书生成
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP311

基金项目:

国家重点研发计划(2022YFA1005101); 国家自然科学基金(12171159, 62272397); 上海市可信工业互联网软件协同创新中心; “数字丝绸之路”上海市可信智能软件国际联合实验室项目(22510750100)


Compositional Probabilistic Barrier Certificate Generation Based on PAC Learning
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    连续动力系统安全验证是一个重要的研究问题, 多年来各类验证方法所能处理的问题规模非常受限. 对此, 对于给定的连续动力系统, 提出通过反例制导方法生成一组组合式概率近似正确(PAC)障碍证书的算法, 最终给出无限时间范畴安全验证问题在概率统计意义下的形式化描述. 通过建立和求解基于大M法的混合整数规划方法, 将障碍证书的求解转化为约束优化问题. 通过微分中值定理将非线性不等式进行区间线性化. 最后, 实现组合式PAC障碍证书生成工具CPBC, 并在11个基准系统上评估其性能. 实验结果表明, CPBC均能成功验证每个动力系统在指定不同的安全需求阈值下的安全性. 与现有方法相比, 所提方法可以更高效地为复杂系统或高维系统生成可靠的概率障碍证书, 验证的样例规模已高达百维.

    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.

    参考文献
    相似文献
    引证文献
引用本文

杨紫萱,曾霞,任勐鑫,王建林,曾振柄,杨争峰.基于PAC学习的组合式概率障碍证书生成.软件学报,,():1-17

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2023-09-11
  • 最后修改日期:2023-10-30
  • 录用日期:
  • 在线发布日期: 2024-11-06
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号