Page 7 - 《软件学报》2025年第5期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(5):1907−1923 [doi: 10.13328/j.cnki.jos.007176] [CSTR: 32375.14.jos.007176] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
基于 PAC 学习的组合式概率障碍证书生成

杨紫萱 1 , 曾 霞 2 , 任勐鑫 3 , 王建林 3 , 曾振柄 4 , 杨争峰 1

1
(华东师范大学 软件工程学院, 上海 200062)
2
(西南大学 计算机与信息科学学院, 重庆 400715)
3
(河南大学 计算机与信息工程学院, 河南 开封 475001)
4
(上海大学 理学院, 上海 200444)
通信作者: 曾霞, E-mail: xzeng0712@swu.edu.cn

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

中文引用格式: 杨紫萱, 曾霞, 任勐鑫, 王建林, 曾振柄, 杨争峰. 基于PAC学习的组合式概率障碍证书生成. 软件学报, 2025,
36(5): 1907–1923. http://www.jos.org.cn/1000-9825/7176.htm
英文引用格式: Yang ZX, Zeng X, Ren MX, Wang JL, Zeng ZB, Yang ZF. Compositional Probabilistic Barrier Certificate Generation
Based on PAC Learning. Ruan Jian Xue Bao/Journal of Software, 2025, 36(5): 1907–1923 (in Chinese). http://www.jos.org.cn/1000 -
9825/7176.htm

Compositional Probabilistic Barrier Certificate Generation Based on PAC Learning
2
1
4
3
3
YANG Zi-Xuan , ZENG Xia , REN Meng-Xin , WANG Jian-Lin , ZENG Zhen-Bing , YANG Zheng-Feng 1
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.

* 基金项目: 国家重点研发计划 (2022YFA1005101); 国家自然科学基金 (12171159, 62272397); 上海市可信工业互联网软件协同创新中心;
“数字丝绸之路”上海市可信智能软件国际联合实验室项目 (22510750100)
本文由“形式化方法与应用”专题特约编辑曹钦翔副教授、宋富研究员、詹乃军研究员推荐.
收稿时间: 2023-09-11; 修改时间: 2023-10-30, 2023-12-13, 2024-01-08; 采用时间: 2024-02-29; jos 在线出版时间: 2024-11-06
CNKI 网络首发时间: 2024-11-07