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

3592 软件学报 2025 年第 36 卷第 8 期

“臂”) 中找到策略, 从而最大化累积奖励. 每个选择的奖励符合某个未知的概率分布, 因此, 需要通过尝试不同的选
择来估计分布, 优化选择. 该问题的形式化定义如下.
定义 n A i 每次被选择会获得符合一个未知的分
{A i } , 每个老虎机的臂
5. 多臂老虎机问题. 给定
n 个老虎机的臂
1
布 µ i 的奖励, 多臂老虎机问题旨在最大化 T 次选择的累计奖励.
多臂老虎机问题可以被视为一种特殊的优化问题. 与广义的优化问题相比, 多臂老虎机问题更强调环境的动
态不确定, 即每个选择获得的奖励均具有一定的随机性且其奖励的分布未知. 因此, 与梯度优化 (如梯度下降和随
机梯度下降)、全局优化 (如遗传算法和模拟退火) 等常见的优化算法相比, 多臂老虎机问题的求解方法更强调适
应奖励的不确定性并要求在线高效决策, 其核心是需要有效平衡“探索” (试验新的或不被经常选择的臂, 从而获取
更多的信息) 和“利用” (选择当前估计最优的臂, 从而获取高奖励).
多臂老虎机问题的常见算法包括 ε-贪心算法和上置信界 (upper confidence bound, UCB) 算法等 [35] . 其中, ε-贪
心算法每次选择时都以一个较小概率 ε 进行探索, 以 1–ε 的概率选择当前估计最优的臂, 该方法简单直接但容易
陷入次优解, 尤其是 ε 取固定值时该算法无法保证收敛. UCB 算法相对复杂但有较好的理论保障, 其核心思想是
A i 的上置信界
每次选择时都同时考虑选择的平均奖励以及不确定性, 选择具有最大上置信界的臂. 具体来说, 臂
√
UCB i = R i +c (2lnt/N i ), 其中, R i 是臂 A i 的平均奖励, 是 c UCB 算法调节平衡探索和利用的参数, t 标记当前选择
是第几次选择, N i 是臂 A i 已被选择的次数.
与 ε-贪心算法相比, 虽然 UCB 算法每轮选择的计算代价更大, 但它具有次线性遗憾的理论保证. 其中, 遗憾评
估的是算法由于不选择最优臂而造成的累计损失, 即算法策略下期望总奖励与理论最优奖励之间的差值. UCB 算
√
O( (ntlnt)). 即累计遗憾量随着选择的次数 的增加而增长, 但其增长速
t
法在 t 次选择后的遗憾已被证明不超过
度低于线性, 这意味着随着时间的推移, UCB 算法表现会越来越接近最优.

3 基于路径过滤与动态选择的 CPS 系统反例生成
本节介绍我们针对 CPS 系统的反例生成问题, 提出的基于混成自动机路径快速探索过滤与动态选择的反例
生成方法, 方法框架如图 2 所示.

面向规约的路径过滤 基于多臂老虎机的路径动态选择反例生成
STL 目标规约  调用路径反例生成 o 更新动作 i 的奖励 r
优化求解器 o i ... 1 ... 奖励 反例生成成功
SAT SAT 执行 k 轮优化 o m r>0 找到不安全行为
路径 p 1 路径 优化
生成 过滤 p 1 求解器 T 轮选择 反例生成结束
... ... ... 未找到不安全行为
p 2 ... 资源耗尽
... p m
p n ...
混成自动机 动态选择路径 p i
路径 过滤后的路径 多臂老虎机
图 2 基于混成自动机路径过滤与动态选择的 CPS 系统反例生成方法框架

首先, 我们针对系统的混成自动机模型生成系统所有可能执行的离散路径. 由于生成的路径可能数量规模巨
大, 且后续针对路径进行反例生成过程涉及根据常微分方程对系统行为轨迹进行密集计算, 非常耗时, 因此, 路径
爆炸会限制方法性能. 针对这一障碍, 我们设计了面向规约的路径快速探索与过滤方法. 根据目标规约的语法解析
树以及路径上的约束, 我们基于时序逻辑的语义以及 SMT (satisfiability modulo theories) 求解器快速过滤一定不存
在违背目标规约的合法行为的路径. 第 3.1 节将具体介绍我们面向规约的路径过滤算法.
针对过滤后的路径, 传统方法会逐条路径基于优化算法依次进行反例生成. 但无论采取什么固定次序对路径
进行优化求解和反例生成, 都可能导致在初始阶段就将过多计算资源分配给不太可能包含不安全行为的路径, 而
实际存在不安全行为的路径对应的状态空间较晚才被探索到, 浪费时间和资源. 不仅如此, 由于缺乏足够的信息来
判断各条路径上存在不安全行为的潜力, 导致传统的方法只能对每条路径平均划分计算资源, 即每条路径的反例