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

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

∫

∑
K
 (i)
 min B(x,c)dx+ y


 i=1
 c,y (i) ,i=1,...,K
 X 0


  ∧

 (i) (i) (i)
  B(x ,c)− My ⩽ 0, (6)
  x ∈ X 0
 
 

 i=1,2,...,K
 
 


 
s.t. B(x,c)−ς ⩾ 0,

 ∀x ∈ X u
 
 
 
 
   ∂B
  
  
   (x,c) f(x)+λB(x,c) ⩽ 0, ∀x ∈ X (7)
 
∂x
(2)
(1)
其中, ς 为一个很小的常数, λ 为一个固定的常数, x , x ,..., x (K) 是从初始区域 X 0 中随机采样的 K 个样本点. M
为一个很大的正数, 通过预先定义来确保该约束对目标函数的影响足够大, 从而实现对 y (i) 的取值的限制. 当
(i) (i) (i) (i) (i) 为一个反例点. 通过最小化反例
y = 0 时, 对应的 x 满足约束条件. 当 y = 1 时, 约束条件对 x 不产生影响, x
K (i)
∑
y 来获得具有鲁棒性和可信度的障碍证书, 以提高系统的概率安全性保障.
点的数量
i=i
定理 6. 若 c 是上述优化问题的最优解, 在给定安全需求阈值参数 ε ∈ (0,1) 和置信度水平参数 β ∈ (0,1) 的条件
∗
下, 随机采样数 K 满足:

( )
2 1
K ⩾ ln +m+1 ,
ε β
∗
其中, m 为 B(x,c) 中优化变量的个数, 则在至少 1−β 的置信度下 P({x ∈ X 0 | B(x,c ) ⩽ 0}) ⩾ 1−ε , 即动力系统 C = ( f,X 0 ,
Ω,X) 满足安全性质的概率至少为 1−ε .
直接求解上述优化问题是很困难的, 因为求解公式 (7) 是一个 NP 难问题. 通过基于微分中值定理的区间线性
化方法, 将公式 (7) 转化为线性不等式, 从而将障碍证书的求解转化为线性优化问题, 便于直接通过数值优化器 Gurobi
进行求解, 为 PAC 障碍证书的计算提供了一个新方法. 在将公式 (7) 通过区间不等式线性化之前, 首先要将所给非
安全区域 X u 和系统状态空间 X 分别用区间 I X u 和 I X 表示, 其中 X u ⊆ I X u ,X ⊆ I X . 先通过定理 2 将非线性不等式转化
为区间不等式, 再使用命题 1 将每个优化变量用两个非负变量的差表示, 从而转化为线性不等式. 本文通过实验证
明了该区间线性化方法在验证复杂动力系统时, 能在更高的安全概率下成功验证动力系统的概率安全性. 这表明
使用定理 2 能有效减小区间长度, 更接近准确解, 从而大大提高区间运算的效率.

4.2 组合式障碍证书
由于将原始优化问题 (5) 转化为基于大 M 法的混合整数规划方法存在一个潜在的问题, 即从初始区域中随
机采样的样本点可能存在部分样本点不满足原始优化问题 (5) 的约束条件的情况, 也就是计算出来的障碍证书在
某些样本点处的值并不满足在初始区域上非正的条件. 基于此, 本文提出学习一组组合式 PAC 障碍证书 (composi-
tional PAC barrier certificates, CPBC) 来解决动力系统概率安全性验证的问题. 通过场景优化方法和基于大 M 法的
混合整数规划方法学习 PAC 障碍证书. 将样本点代入原问题中进行验证, 不满足初始区域上的约束条件的点作为
反例点. 本文通过使用反例制导方法学习一组组合式的 PAC 障碍证书, 来提高动力系统概率安全验证的保障. 为
了能更具体地说明本文所提方法的应用和优势, 通过例 2 进行阐述.
例 2: 给定一个连续动力系统

   
 ˙x 1  −x 1 + x 1 x 2 
   
   ,

  = 
   
˙ x 2 −x 2
2 2
系统状态空间 X = {x ∈ R : −2.5 ⩽ x 1 , x 2 ⩽ 2.5} , 初始区域 X 0 = {x ∈ R : −0.5 ⩽ x 1 ⩽ 0,−1 ⩽ x 2 ⩽ 1} X 0 服从均匀分布,
,
2
非安全区域 X u = {x ∈ R : 1.2 ⩽ x 1 ⩽ 2,−2 ⩽ x 2 ⩽ −0.17} .
4
若安全需求阈值参数 ε = 0.1 , 置信度水平参数 β = 10 −12 , M = 10 . 由定理 6 可知在初始区域中随机采样的样
本数 K = 813 . 通过基于大 M 法的混合整数规划方法, 在初始区域中随机采样 813 个样本点学习 PAC 障碍证书
B 0 = −12.858+8.958x 1 −15.0x 2 .
如图 1 (a) 所示, 绿框和红框分别代表初始区域和非安全区域, B 0 由黑色直线表示, 目标是希望 B 0 将两个区域
分隔开. 接下来通过将 K 个样本点代入 B 0 , 验证是否满足初始区域上的原始约束条件 B 0 (x) ⩽ 0 . 计算可知存在 5