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

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

化. 与直接通过区间乘法运算得到的结果相比, 该方法得到的区间长度更短, 更加近似精确值. 接下来通过一个例
子说明直接进行区间乘法运算与基于微分中值定理区间化方法的不同之处.
例 1: 假设连续函数 g(x) = x −2x +4x, x ∈ [4,5] , 通过单调性可知 g(x) ∈ [48,95] . 如果对于函数的每一项直接
3
2
g(x) 进
通过区间乘法运算后可以得到 g(x) ∈ [30,113] . 基于微分中值定理的区间化方法首先得到中点 ˘ x = 4.5, 再将
′
′ 2 g (x) 通过定义 ′
行求导得 g (x) = 3x −4x+4, x ∈ [4,5] . 将 3 进行区间运算得 g (x) ∈ [32,63] , 所以 g(x) ∈ g(4.5)+
′
g (x)(x−4.5) = [37.125,100.125] , 区间长度比 [30,113] 小.
通过例 1 的演示, 可以发现, 使用定理 2 进行区间化运算相比于直接对连续函数的每一项进行区间乘法运算,
更加接近于原问题的准确值.

3 动力系统的概率安全验证
在动力系统的安全性验证方面, 一种流行的方法是使用障碍证书. 由于动力系统的安全性验证问题通常具有
不确定性, 即使对于具有简单动力学的系统也是如此. 近年来, 对于系统的概率安全性分析问题受到广泛关注, 其
中一种方法是通过定量安全性取代定性安全性, 即不要求系统轨迹一定不能到达某个非安全区域. 本节首先介绍
通过障碍证书 (barrier certificate, BC) 来验证系统的安全性概念, 属于定性安全性. 然后介绍概率障碍证书验证系
统的安全性概念, 属于定量安全性.

3.1 障碍证书
障碍证书是一种提供形式化框架的方法, 通常用一个函数来定义, 具体形式取决于系统的特定要求和约束, 可
以是多项式函数、线性不等式或差分不等式. 障碍证书将系统的状态空间划分为两个区域, 分别包含初始状态的
前向可达状态集和非安全区域的反向可达状态集. 障碍证书的设计满足一定的条件, 即系统的状态始终保持在定
义的安全边界内, 并满足所需的安全属性. 通过验证障碍证书的存在性, 可以确定系统是否能完全避免进入非安全
区域, 正式证明系统的安全性. 在没有精确解的情况下, 也能够确保系统满足非线性方程的要求. 障碍证书有多种
变体, 对应多种不同的计算方法. 本文将障碍证书定义为多项式形式, 但本文的方法并不局限于多项式形式.
定理 3 (障碍证书) [22] . 给定一个连续动力系统 C = ( f,X 0 ,Ω,X) 和相应的非安全区域 X u ⊆ X , 若障碍证书
n
B : R → R 存在, 则需要满足以下条件:
BC1. ∀x ∈ X 0 , B(x) ⩽ 0;
BC2. ∀x ∈ X u , B(x) > 0;
∂B
∀x ∈ X,
BC3. (x) f(x)+λB(x) ⩽ 0 , 其中, λ ∈ R 为一个固定的常数.
∂x
B(x) 的
障碍证书 B(x) 将可达区域中的所有状态映射为非正实数, 将非安全区域中的所有状态映射为正实数.
零级集合将初始区域与非安全区域分开, 要求系统状态在连续演化过程中, 当 B(x) = 0 时不会将满足 B(x) ⩽ 0 的状
B(x) > 0 的状态 [36] . 定理 3 将障碍证书视为与时间无关的量来刻画系统的安全性. 若能找到一个满
态演变为满足
足 BC1–BC3 的 B(x) , 则可以说明该系统是安全的.
3.2 概率障碍证书
概率障碍证书用于验证动力系统的概率安全性. Xue 等人 [5] 通过限制系统出现不安全行为的概率在一定置信
度下保持在定量安全的目标范围内, 将满足这一性质的系统称为概率近似安全的. 通过统计推断和有限样本建模,
利用 PAC 障碍证书验证动力系统的概率安全性, 可以更全面地评估复杂动力系统或高维动力系统的安全性. 基
于 PAC 学习的保证和场景优化方法将训练数据的大小与安全需求阈值参数 ε 和置信度水平参数 β 相关联. 基于
定理 3, 提出了通过学习连续动力系统的 PAC 障碍证书 (probably approximately correct barrier certificates, PBC) 来
证明系统的概率近似安全性.
定义 4 (PAC 障碍证书). 给定一个连续动力系统 C = ( f,X 0 ,Ω,X) 和相应的非安全区域 X u ⊆ X , 若 B : R → R
n
是关于安全需求阈值参数 ε ∈ (0,1) 和置信度水平参数 β ∈ (0,1) 的 PAC 障碍证书, 则需满足下述条件: