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

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

Finally, this study implements the compositional PAC barrier certificate generator CPBC and evaluates its performance on 11 benchmark
systems. The experimental results show that CPBC can successfully verify the safety of each dynamical system under specified different
safety requirement thresholds. Compared with existing methods, the proposed method can more efficiently generate reliable probabilistic
barrier certificates for complex or high-dimensional systems, with the verified example scale reaching up to hundreds of dimensions.
Key words: continuous dynamical system; barrier certificate; probably approximately correct (PAC); interval linearization; mixed-integer
programming
安全验证问题是利用形式化方法证明系统在运行过程中满足指定安全需求的重要研究问题. 这类研究对涉及
安全攸关系统的应用领域尤为重要, 例如自动驾驶汽车 [1] 、医疗设备 [2] 、航空航天 [3] 等多个领域, 对人类生命安全、
环境保护以及重要基础设施的正常运行具有重大意义. 形式化验证是对动力系统进行验证的重要方法, 主要可分
为准确验证和概率验证两种方式. 而安全攸关动力系统通常涉及多个复杂因素的相互作用, 包括物理动力学、控
制算法和环境因素等. 在验证过程中, 不确定性和噪声的影响使得系统的行为难以预测. 此外, 动力系统的状态空
间通常是高维的, 增加了验证的复杂性. 因此, 通过准确验证处理这些复杂系统时常常面临极大的限制和困难, 导
致一系列方法在实际应用中问题规模受到一定限制, 一般在 20 维以内.
在许多实际应用中, 系统安全性的需求往往可以通过达到一定的概率精度来满足. 系统安全性的概率验证分
析是一个关键的研究领域. 主要包含两种类型的问题, 其中一类问题是寻求系统的概率近似安全性, 即在高置信度
下保证系统的安全性, 另一类问题通过确定系统安全概率的下界来进行安全性评估. 之前的研究中, Xue 等人采用
概率近似正确 (probably approximately correct, PAC) 学习框架 [4] , 通过生成 PAC 障碍证书 (barrier certificate, BC)
验证系统的概率安全性 [5] . 然而, 当需要达到很高的安全概率要求时, 部分样本点可能始终无法满足安全条件. 为
了应对这种情况, Xue 等人采取将这些样本点进行丢弃的方法 [5] . 本文提出了生成一组组合式 PAC 障碍证书的算
法, 在验证复杂动力系统的安全性时, 能够更加灵活地求解. 该算法采用反例制导的方法学习一组障碍证书, 直到
验证过程中没有反例点为止. 组合式障碍证书采用多个障碍证书联合的思想, 提高了整体的性能和鲁棒性, 允许在
优化问题求解过程中纠正由于样本和概率不完备性导致的误差, 并且能够有效地改善验证结果. 与先前的方法相
比, 本文提出的方法通过概率方式描述连续动力系统的安全性, 在准确验证方法无法验证系统安全性的情况下, 本
方法能够进行定量的概率分析, 从而有效地验证高维复杂系统的安全性. 需要指出的是, 虽然概率方法提供了系统
安全性的定量评估, 但这并不意味着可以确保绝对的安全.
为了学习单个 PAC 障碍证书, 本文提出一种基于大 M 法的混合整数规划方法进行求解. 在给定安全需求阈
值参数 ε 和置信度水平参数 β 的情况下, 该方法的目标是学习在初始区域上至少 1−β 的置信度下满足安全属性的
1−ε 的概率障碍证书. 通过引入常数 M 和二进制变量, 能够将不满足约束条件的点进行调整, 以满
概率大于等于
足对障碍证书的要求. 具体地, 对于每个从初始区域中随机采样的样本点, 将其对应的约束减去 M 乘以二进制变
量. 当二进制变量为 1 时, 约束条件对该点不产生影响; 当二进制变量为 0 时, 该点必须满足约束条件. 通过在优化
目标中最小化所有二进制变量的和, 目标是使不满足原问题约束条件的点的数量尽可能少, 以提高验证的效率和
可行性. 基于大 M 法的混合整数规划方法能够有效处理 PAC 学习中可能出现的不满足约束条件的情况. 为了处
理约束条件, 本文采用场景优化方法 [6] 和区间不等式线性化方法 [7−10] , 并通过基于微分中值定理的非线性不等式
区间化方法, 将非线性不等式转化为线性不等式 [11] , 使用数值优化器 Gurobi 进行求解. 这种方法相比直接进行区
间乘法运算能够更准确地近似原始约束, 并提高优化问题的求解效率. 通过求解上述优化问题, 可以计算出具有鲁
棒性和可信度的 PAC 障碍证书.
本文旨在为连续动力系统的概率安全性验证提供一种创新方法. 通过结合 PAC 学习框架、基于大 M 法的混
合整数规划和反例制导方法, 可以获得一组组合式的 PAC 障碍证书, 从而提高系统概率安全性的保障. 为了验证
方法的有效性和适用性, 本文将该方法应用于 11 个连续动力系统的概率安全性验证任务, 并与现有验证方法进行
对比实验. 结果表明, 所提方法在保证准确性的前提下, 大大减少了计算时间和空间的开销. 进一步推动连续动力
系统概率安全验证领域的发展. 综上, 本文的主要贡献包括以下内容.
● 提出了通过反例制导方法学习一组组合式 PAC 障碍证书的算法, 增强了连续动力系统的概率安全保障.