Page 9 - 《软件学报》2025年第5期
P. 9

杨紫萱 等: 基于   PAC  学习的组合式概率障碍证书生成                                                 1909


                    ● 将问题转化为基于大        M  法的混合整数规划问题, 使不满足约束条件的点的数量最小化, 从而提高障碍证书
                 的鲁棒性和可信度.
                    ● 通过场景优化方法和基于微分中值定理的区间化方法将非线性不等式转化为线性不等式, 能够更加近似原
                 始约束, 提高优化问题的求解效率.
                    ● 实现了组合式     PAC  障碍证书生成工具      CPBC, 并在  11  个基准系统上评估其性能. 实验结果表明该工具成功
                 验证了所有样例的概率安全性, 并且相比现有方法对于验证复杂系统或高维系统更高效.
                    本文第   1  节介绍相关工作. 第     2  节介绍预备知识. 第    3  节介绍动力系统概率安全验证任务. 第            4  节介绍组合
                 式  PAC  障碍证书的动机和计算方法. 第        5  节介绍算法流程, 并通过具体例子展示计算方法. 第             6  节对  11  个非线性
                 连续动力系统进行实验评估. 第         7  节总结全文.

                 1   相关工作


                    在实际应用中, 许多安全攸关系统都是基于连续动力系统构建的. 对于验证连续动力系统的安全性, 不变量生
                 成是一种成熟的近似方案, 可为系统在无限时间范围内的安全性提供可靠的证明. 不变量可以采用多种形式构建,
                 比如通过障碍证书       [12] 证明系统在无限时间范围内的安全性. 通过预先指定的模板, 可以将问题简化为数值优化或
                 约束求解问题     [13−16] . 使用障碍证书进行验证的最初想法是由         Prajna 等人  [17] 提出的. 障碍证书能否成功合成与     3  个
                 因素密切相关, 即障碍证书模板的形式、障碍证书条件的编码以及生成障碍证书的计算方法. 研究一直致力于各
                 种形式的障碍证书, 力图在表达性和合成可行性之间取得平衡. 障碍证书可以按照其形式和验证方法的不同, 分为
                 确定形式和概率形式.
                    确定形式的障碍证书通常用于验证确定性连续动力系统的安全性. 其中, 障碍证书的形式是一个确定的函数
                 或多项式, 能够精确地描述系统的安全区域和边界. 确定形式的障碍证书可以通过数值计算或数学推导方法来判
                 断其是否存在, 并可用于保证系统在给定约束条件下保持在一个安全区域内. Prajna 等人                        [17,18] 采用正立方体定理
                 推导出障碍证书的平方和程序, 这导致了一个属于                NP  难问题的双线性矩阵不等式求解问题. Sloth          等人  [19] 建立了
                 一种组合形式的条件, 用于验证特定类别的动力系统的安全性. Kapinski 等人                  [20] 提出了一种基于   Lyapunov  函数的
                 障碍证书, 比   Prajna 等人提出的障碍证书更保守但更易于处理. Platzer 等人           [21] 探讨了微分不变量来扩展障碍证书
                 的思想, 考虑多项式等式和不等式的布尔组合, 扩展了障碍证书的范围, 从而可以描述更广泛的系统安全性问题.
                 Sogokon  等人  [22] 采用一种称为类  Lyapunov  函数方法的技术, 来放宽障碍证书的导数条件, 以保持搜索空间的凸
                 性, 从而能够搜索具有更一般特征的更广泛的障碍证书. 对于障碍证书条件的编码, 一种常用方法是使用平方和多
                 项式和半定规划理论将验证条件转化为凸优化问题                  [18,23,24] . 另一种方法是使用  Hamilton-Jacobi 可达性分析的概念,
                 将验证条件编码为偏微分方程           [25] . 在确定形式的障碍证书生成的计算方面, 最广泛使用的方法是平方和编程和
                 BMI 求解  [23] , 已成功应用于各种类型的系统. Zeng     等人  [26] 提出使用  Darboux  形式的障碍证书来保证系统的安全
                 性, 其基于代数曲线定义, 并可以对系统的轨迹施加约束.
                    概率形式的障碍证书适用于具有确定性或随机性的系统, 可以描述系统在一定概率下保持在安全区域内的可
                 能性, 更全面地考虑系统的不确定性. 现有研究大多数采用统计模型检验                       [27,28] 或概率可达集计算  [29,30] 来验证随机
                 系统. 但统计模型检验只能提供统计保证             [31] . 概率形式的障碍证书可以通过随机模型或随机过程来定义. 随机模
                 型通常基于概率分布函数或随机变量, 用于描述系统的随机性质. 随机过程是一种描述随机行为随时间演变的数
                 学工具. Xue 等人   [5] 使用  PAC  框架定义概率障碍证书, 旨在研究在给定样本和一定置信度的情况下, 如何从训练
                 数据中学习出一个在未知数据上表现良好的模型, 来验证受扰动输入的动力系统的概率安全性. Huang                               等人  [32] 提
                 出一种基于障碍证书的随机初始状态半代数混成系统的概率安全验证方法, 将概率安全验证问题转化为在初始状
                 态空间中寻找可找到的障碍证书的最大内切区域的问题. Kumar 等人                    [33] 使用高斯过程对残差动态的投影建模为
                 控制障碍函数, 结果表明相比神经网络的确定性方法, 概率方法能够显著减少安全违规次数. Luo                           等人  [34] 提出了概
                 率安全障碍证书      (PrSBC), 使用控制障碍证书来定义概率安全的可能控制动作的空间, 通过约束机会约束安全集
   4   5   6   7   8   9   10   11   12   13   14