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

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

优化问题难以求解. 相反, 基于微分中值定理的区间化方法提供了更精确的区间估计. 在 PACBC 无法找到解的情
况下, 通常需要划分区间或增加障碍证书模板的次数来寻找可行解, 但这可能导致求解复杂度呈指数型增加. 相比
之下, PACBC-DM 无需进行额外区域划分就能找到可行解, 显著提高了计算效率.
在样例 C 1 C 5 和 C 10 中, CPBC 和 PACBC 都能成功验证动力系统的概率安全性, 适应不同的安全需求阈值要
–
求. 从表 1 中的 T(s) 列数据可以看出, 就时间效率而言, CPBC 在这些样例中的表现均优于 PACBC. 例如, 对于样
例 C 5 , 在安全阈值 1−ε 为 0.95 的情况下, PACBC 耗时 2 639.76 s 以验证系统的概率安全性, 而 CPBC 仅需 40.05 s,
效率是 PACBC 的 65 倍. 对于样例 C 3 , 在安全阈值为 0.95 的情况下, PACBC 需耗时 315.03 s 在 2 次障碍证书模
板下验证系统的概率安全性, 而 CPBC 只需 20.33 s 即可生成组合形式的 1 次 PAC 障碍证书, 效率是 PACBC 的
15 倍. 样例 C 3 对于不同要求的安全阈值均生成多个 PAC 障碍证书来验证系统的概率安全性, 实验效率明显高于
PACBC, 表明多个 1 次的 PAC 障碍证书具有表达力的同时生成效率更高. 与 PACBC 不同的是, CPBC 在将非线
性不等式线性化时采用基于微分中值定理的方法, 有效改善了区间扩张现象, 提高了计算结果的精确性. 在
PACBC 未能获得可行解的情况下, 不得不对非安全区域和系统状态域进行区域划分以解决由于区间扩张导致的
问题, 但这也增加了求解时间的开销. 在实验中, 对于 PACBC, 首先尝试在不划分区域的情况下在 1 次障碍证书模
板下求解, 若无解则对区域进行划分. 考虑到求解时间随划分数的指数型增长, 每个维度的最大划分数设为 4, 通
过逐步提高区域划分的细度来迭代求解. 若在 1 次障碍证书条件下仍然无解, 则采用 2 次障碍证书进行计算.
–
在样例 C 6 C 9 中, 观察到 CPBC 能成功验证所有样例在不同安全阈值下的概率安全性. 与此相比, PACBC 只
能在样例 C 7 和 C 8 中, 在安全阈值为 0.8 时成功验证系统的概率安全性, 而 CPBC 能在安全阈值为 0.95 的情况下
成功验证, 且时间效率至少快 14 倍. CPBC 通过求得组合式 PAC 障碍证书, 迅速验证了系统的概率安全性. 对于
PACBC 验证失败的情况, 我们进行了一系列探索和尝试: 首先, 在 1 次障碍证书模板下, 对非安全区域和系统状态
域的各个维度进行最多 4 次划分并求解, 以缓解由区间扩张导致的无可行解问题. 如果仍无解, 则采用 2 次障碍证
书进行验证, 在必要时对非安全区域和系统状态域的各个维度进行划分后求解. 如果在最大运行时间范围内仍无
解, 则用横杠表示验证失败. 这些实验结果表明, PACBC 的验证过程高度依赖于障碍证书的复杂表达力, 主要受非
线性不等式在区间化时直接通过区间乘法运算带来的误差影响. 相比之下, CPBC 通过使用基于微分中值定理的
区间化方法, 无需对区域进行划分即可成功验证样例的概率安全性. 这不仅体现了其验证的有效性, 还表现出其在
复杂动力系统概率安全验证方面的广泛适用性.
本文还针对两个 101 维的样例进行了对比实验, 样例 C 9 源自 Ratschan 等人 [38] 的工作, 样例 C 10 则是 Xue 等
[5]
人对 Ratschan 样例的修改, 其中系统状态空间每个维度被限制在 [−0.3,0.3] 的范围内. 对于样例 C 9 , 其系统状态空
间的范围较广 ( [−10,10] ), 这在区间线性化的过程中凸显了 PACBC 方法直接采用区间乘法运算引入的误差问题.
如果对每个维度进行区域划分处理, 我们发现即使是在最大允许的运行时间内, 也无法求解. 我们尝试将区域随机划分为
1 024、2 048 和 4 096 个区域进行运算, 但在所有这些尝试中, 都未能在规定的最大运行时间内求解. 如果不进行区
域划分, 由于区间扩张的问题, 同样无法找到可行解. 相比之下, CPBC 通过成功求解单个 1 次障碍证书, 有效地进
行了动力系统的概率安全验证, 这进一步证明了, 基于微分中值定理进行的区间线性化方法, 相比直接区间相乘方
法, 在优化问题求解上能更接近原始问题的解. 对于样例 C 10 , 由于其较小状态空间范围, PACBC 在区间相乘操作
中的劣势不太明显, 从而在区间线性化时能够有效地求解. 然而, 实验结果显示, CPBC 在效率方面仍然表现得更
优越. 此外, 本文还进一步探索了一个 201 维的样例, 我们发现, 在 PACBC 无法验证动力系统的概率安全性的情
况下, CPBC 在不进行区域划分的前提下, 成功地验证了动力系统的概率安全性.
综上所述, 基于 CPBC 算法框架的 PAC 障碍证书生成方法在实验中展现了出色的性能. 对于 PACBC 无法验
证的情况, CPBC 通过生成组合式 PAC 障碍证书, 更高效地实现了动力系统的概率安全验证. 而基于 PACBC 算法
框架的方法在一些复杂的动力系统下表现出较差的效果, 尤其是在高维动力系统中. 因此, 本文提出的 CPBC 算法
在提升动力系统的概率安全保障方面具有显著潜力和优势, 为高维动力系统的概率安全验证提供了一种有效的解
决方案.