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

1916 软件学报 2025 年第 36 卷第 5 期

B (x) 存入集合 X (i) X (i) T 中.
(i)
将 CPBC; 否则 中存在反例点, 将 存入到
j j j
T = {}, 则返回组合式 PAC 障碍证书集合 π (i) T 中
(4) 若 CPBC; 否则, 令 i = i+1 , 构造 为 T 的加细划分, 即将
每一个元素 X j 划分成两个子块, 使得其中一个子块包含 X j 的 K 个样本点中所有的反例点, 另一子块包含非反例点.
i = L 则结束, 否则重复步骤 (2)–(4).
(5) 若

B
学习 验证

采样样本点 样本点代入原始条件
区间线性化
连续系统 场景优化 一组 B
x˙=f (x)
B 满足初始 是
区域的安全性?
基于大 M 法的混合整数规划
否

将包含反例点的区域进行划分
图 2 组合式 PAC 障碍证书构造框架

由于优化问题采用基于大 M 法的混合整数规划方法, 在约束中引入了新的变量, 因此可能存在反例点. 通过
将包含反例点的区域进行划分后再分别对每个区域计算 PAC 障碍证书, 能够更好地逼近原问题的约束, 从而生成
一组组合式 PAC 障碍证书来共同验证动力系统的概率安全性, 提高验证的准确性. 这种反例制导方法允许在优化
过程中纠正由于样本和概率不完备性导致的误差, 并且能够改善验证结果.
在应用场景方面, 生成一组组合式 PAC 障碍证书的方法适用于各种安全攸关系统, 如机器人控制系统、自动
驾驶等, 从而验证系统的概率安全性. 例如, 在给定安全需求阈值参数和置信度水平参数的条件下, 对机器人控制
系统进行验证, 以确保机器人在复杂环境中执行任务时不会出现意外行为. 对自动驾驶系统验证其在不同交通条
件和道路情况下的概率安全性, 确保驾驶的可靠性和安全性.
因此, 本文提出的求解组合式障碍证书的方法为验证动力系统的概率安全性提供了一种有效的、全面的、可
靠的方式, 在许多复杂系统的概率安全性验证中具有重要作用, 并在自动化、机器学习等领域中有广泛的应用潜力.

5 算法与用例展示

本节首先介绍使用混合整数规划方法生成一组组合式 PAC 障碍证书的算法, 再通过一个三维实例进行详细
介绍.

5.1 算 法
算法 1 展示了本文所提出的组合式 PAC 障碍证书的生成算法. 对于一个给定的连续动力系统和非安全区域,
首先定义安全验证的安全需求阈值参数 ε 和置信度水平参数 β , 给定一个很大的正常数 M , 将划分 π (i) 初始化为
X 0 , 将临时存储集合 τ 初始化为空集, 将组合式障碍证书集合 CPBC 初始化为空集, 将变量 i 初始化为 1, L 初始化
为 100, K 为满足定理 6 的随机采样数. 当 i 小于 L 时, 开始循环 (第 1 行). 对于 π (i) 中每一个划分块 ¯ U (第 2 行), 随
机采样 K 个点得到样本点集 ¯ u (第 3 行), 并将 (7) 通过定理 2 使非线性不等式区间化, 再由命题 1 将区间不等式转
化为线性不等式, 将问题转化为第 4.1 节所提出的基于大 M 法的混合整数规划方法, 可以直接带入数值优化器
Gurobi 进行求解, 得到 PAC 障碍证书 B (第 4 行). 将 ¯ u 中样本点带回初始区域上的原始约束条件 (5), 验证是否满
足 B 的值在样本点上非正的安全性条件, 若满足则将 B 加入 CPBC 集合中 (第 5、6 行), 若不满足则将该划分块 ¯ U