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

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

的二次规划来确定安全控制器. Jing 等人 [35] 提出了一种安全性和性能规范的障碍证书, 该证书通过在长期概率上
定义的前向不变性的新概念, 集成了基于可达性和基于不变性的方法, 能保证多全局目标的随机安全控制技术. 随
着概率形式障碍证书技术的发展, 其将在越来越多的实际应用中发挥重要作用, 为复杂系统的概率安全性提供更
全面的保障.

2 预备知识

本节将介绍动力系统的概率安全性问题、场景优化方法和基于微分中值定理的区间线性化方法.

2.1 动力系统安全性

考虑一类由自治型常微分方程建模的连续动力系统:

˙ x = f(x) (1)
n
n + n n D ⊆ R 上定义的向
,
其中, x ∈ R 是状态向量, ˙ x 表示其时间导数 dx/dt t ∈ R 表示时间, f : R → R 是在状态空间
0
量场. 假设 f 满足局部利普希茨条件, 使得在状态空间 D 中对于每个初始状态 x 0 , 存在一个有限的时间区间 [0,T] ,
在该区间内动力系统有唯一解 x(x 0 ,t) .
动力系统 (1) 通常配有系统状态空间 X ⊆ D 和初始区域 X 0 ⊆ X X 为一个有界紧集. Ω 为 X 0 服从的分布, 用
,
于选择初始连续状态. 将动力系统表示为四元组 C = ( f,X 0 ,Ω,X) . 然而, 动力系统在实际应用中面临着安全性的挑
战. 安全性指系统在运行过程中具有始终不会进入非安全区域的性质. 对于连续动力系统而言, 安全性的保证至关
X 0 出
重要, 因为系统的异常状态可能导致严重的后果. 给定一个预先指定的非安全区域 X u ⊆ X , 如果从初始区域
发的系统轨迹在任意时间内都不会进入非安全区域 X u , 则称动力系统 C 是安全的.
定义 1 (安全性). 对于一个连续动力系统 C = ( f,X 0 ,Ω,X) 和给定的非安全区域 X u ⊆ X , 其中 X u ∩ X 0 = ∅ , 若系
统轨迹始终在 X 中并且不会进入非安全区域 X u , 即对任意 x 0 ∈ X 0 , 任意 T ⩾ 0 :

∀t ∈ [0,T], (x(x 0 ,t) ∈ X)∧(x(x 0 ,T) < X u ),

则称该系统是安全的.
定义 1 是对于动力系统安全性的语义定义, 旨在确保系统在运行过程中始终不会进入非安全区域. 动力系统
通常由非线性常微分方程表示, 由于难以获得精确解, 对于动力系统的安全性验证一直以来是一个具有挑战性的
问题. 目前能够验证的问题规模受到一定的限制, 一般局限在 20 维以内. 然而, 如果允许系统在一定概率情况下不
满足安全性质, 即不要求所有从初始区域出发的状态轨迹都完全避开非安全区域, 这样的系统被称为概率安全系
统. 动力系统的概率安全性对系统的安全性进行定量分析, 扩展了问题规模的可行性, 使其适应更为复杂的实际工
业问题, 有效地处理了不确定性因素. 定义 2 为动力系统的概率安全性定义.
定义 2 (概率安全性). 连续动力系统 C = ( f,X 0 ,Ω,X) 关于 ε ∈ (0,1) 和 β ∈ (0,1) 是概率近似安全的, 如果在至少
1−β 的置信度下, 动力系统满足安全性质的概率大于等于 1−ε .
定义 2 表明若动力系统是概率近似安全的, 则在至少 1−β 的置信度下, 从满足 Ω 的随机初始状态 x 0 出发的状
态点在后续演化中不会进入非安全区域的概率至少为 1−ε . 系统的概率安全性是通过 PAC 学习框架定义的.
PAC 学习框架广泛应用于机器学习领域, 是一种基于统计学习理论的方法. 该方法提供了在有限数据集上通过随
机采样评估系统安全性的方法. 目的是在给定安全需求阈值参数和置信度水平参数的情况下保证学习部分的训练
Ω 为均匀分布的情况, 然而, 本文的方法也适用于其他分布
效果, 使得该框架适用于形式验证的目的. 本文仅考虑
情况.

2.2 场景优化方法
场景优化方法 (scenario optimization approach) 是一种用于解决具有无限个约束的凸优化问题的有效技术.
[6]
在这种方法中, 假设对不确定性进行概率描述, 通过一组 ∆ 以及 ∆ 上的概率分布 P 来表示不确定性, 将不确定性引
入优化问题的建模中, 具有统计形式的保证. 由于在计算中无法处理大量的约束 h δ (γ) ⩽ 0,∀δ ∈ ∆ , 通过概率分布 P