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

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

再线性化得:

c 01 −c 02 +1.5c 11 −2c 12 −c 22 −c 32 −ς ⩾ 0.
∂B
X 上通过定理 2 (x) f(x)+λB(x) ⩽ 0 区间化得:
在 将不等式
∂x

λc 0 +(λ+1)c 1 [−2,2]+(λ+1)c 2 [−2,2]+(λ+16)c 3 [−2,2] ⩽ 0.
再线性化得:

λc 01 −λc 02 +2(λ+1)c 11 +2(λ+1)c 12 +2(λ+1)c 21 +2(λ+1)c 22 +2(λ+16)c 31 +2(λ+16)c 32 ⩽ 0.
∫
λ = 0.132 ς = 0.05 , 令第 1 π = {X } ,
(1)
(1)
目标是最小化 B(x,c)dx 和不满足约束条件的点的个数, 令 , 轮划分
1
X 0
其中 X (1) = X 0 . 从 X (1) 中随机采样 K 个样本点, 通过大 M 法学习 PAC 障碍证书:
1 1

(1)
B = −13.709+11.603x 1 +2.989x 2 −3.446x 3 ,
1
(1)
验证样本点是否满足 B (x) ⩽ 0 , 得到 (0.999,0.841,0.013) 、 (0.983,0.936,0.142) 、 (0.963,0.984,0.024) 这 3 个反例
1
(2)
(2)
(2)
3
点. 将 X (1) 存入到临时存储空集 T 中, 并构造 T 的加细划分, 赋给 π (2) , 此时 π = {X ,X } , 其中 X (2) = {x ∈ R :
1 1 2 1
3
0 ⩽ x 1 ⩽ 0.5,0 ⩽ x 2 , x 3 ⩽ 1} X (2) = {x ∈ R : 0.5 ⩽ x 1 ⩽ 1,0 ⩽ x 2 , x 3 ⩽ 1} .
,
2
从 X (2) 中随机采样 K 个样本点, 通过大 M 法学习 PAC 障碍证书:
1

(2)
B = −9.749+12.389x 1 +3.717x 2 −4.284x 3 ,
1
(2)
(2)
验证样本点是否满足约束条件 B (x) ⩽ 0 , 可知不存在反例点, 此时组合式 PAC 障碍证书集合 CPBC = {B } .
1 1
从 X (2) 中随机采样 K 个样本点, 通过大 M 法学习 PAC 障碍证书:
2

(2)
B = −6.103+6.835x 1 +8.882×10 −16 x 2 ,
2
(2)
验证样本点是否满足 B (x) ⩽ 0 , 得到 (0.946,0.957,0.980) 、 (0.903,0.782,0.762) 、 (0.992,0.267,0.109) 这 3 个反例
2
(3)
(3)
3
(3)
点. 将 X (2) 存入到临时存储空集 T 中, 并构造 T 的加细划分, 赋给 π (3) , 此时 π = {X ,X } , 其中 X (3) = {x ∈ R : 0.5 ⩽
2 1 2 1
3
x 1 ⩽ 1,0 ⩽ x 2 ⩽ 0.5,0 ⩽ x 3 ⩽ 1} X (3) = {x ∈ R : 0.5 ⩽ x 1 , x 2 ⩽ 1,0 ⩽ x 3 ⩽ 1} .
,
2
从 X (3) 中随机采样 K 个样本点, 通过大 M 法学习 PAC 障碍证书:
1

(3)
B = −3.216+2.564x 1 +0.747x 2 −0.860x 3 ,
1
(3)
(2)
(3)
验证样本点是否满足约束条件 B (x) ⩽ 0 , 可知不存在反例点, 此时组合式 PAC 障碍证书集合 CPBC = {B ,B } .
1 1 1
从 X (3) 中随机采样 K 个样本点, 通过大 M 法学习 PAC 障碍证书:
2

(3)
B = −3.223+2.415x 1 +0.264x 2 −0.429x 3 ,
2
(2)
(3)
(3)
(3)
验证样本点是否满足 B (x) ⩽ 0 , 可知不存在反例点, 此时组合式 PAC 障碍证书集合 CPBC = {B ,B ,B } . 由于
2 1 1 2
(3)
(2)
此时没有将 T 赋值, 所以 T 为空集, 因此组合式 PAC 障碍证书为 B ,B ,B (3) . 可以验证在置信度至少为 1−10 −12
1 1 2
的条件下, 系统满足安全性质的概率至少为 0.9.

6 实验结果及分析
在本节中, 我们对提出的 CPBC 算法进行了评估, 以实现对 11 个非线性连续动力系统进行概率安全验证. 同
时比较了 CPBC 算法和 Xue 等人提出的 PACBC 方法 [5] , 并采用基于微分中值定理的区间化方法 PACBC-DM 进
行了实验. 所有实验都是在 Ubuntu 系统下使用 3.30 GHz Intel(R) Xeon(R) Gold 6246 处理器、NVIDIA GeForce
RTX 2080 Ti CPU 和 64 GB RAM 的机器上运行的. 本文使用数值优化器 Gurobi 求解混合整数规划问题, 实验结
果见表 1.
针对 11 个基准样例进行了对比实验, 其中包括高达 200 维的样例, 以评估基于微分中值定理区间化方法的优
势以及 CPBC 与 PACBC 方法之间的效果差异. 对于 15 维以上的高维样例, 从 Ratschan 的研究中选取了一个可扩
展性样例 [38] , 并针对几个有代表性的样例进行了深入分析. PACBC 方法通过在初始区域的约束中引入松弛变量,
并在目标函数中最小化这一变量来求解障碍证书. 在将非线性不等式线性化时, PACBC 直接采用区间乘法运算.