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

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

17. if R[0,0] = −1 then return true; ▷ 路径 p 与 ¬φ 冲突, 过滤该路径
18. return false; ▷ 保留该路径
]
具体来说, 面向目标规约的路径过滤算法 1 在第 4 行初始化了一个动态规划表 R, 其中 R i, j 将用来存储公
[
式 ϕ[i] 在节点 q j 是否冲突, 其中 1 表示 ϕ[i] 总成立 (一定不冲突), −1 表示一定冲突, 否则为 0. 该算法自底向上依
次计算 ¬φ 的语法解析树中的原子谓词, 子公式和最顶层公式在路径各节点的冲突情况 (第 5–16 行), 每次都从路
径上的最后一个节点向前计算到初始节点 (第 6–16 行). 该动态规划算法在计算每个公式在每个节点上的冲突情
况时, 通过动态规划表 R 重用了该公式在后续节点的冲突计算结果以及其子公式的冲突计算结果, 从而避免了重
复计算. 我们根据公式 ϕ[i] 的语法分情况讨论.
• ϕ[i] := true 时, ϕ[i] 在节点 q j 上总成立 (第 7 行);
• ϕ[i] := θ(X) ⩾ d 时, 使用 SMT 求解器判断节点 q j 上的不变式等约束与 ϕ[i] 是否总冲突, 若总冲突说明 ϕ[i]
在该节点一定不成立 (默认节点内的不变式等约束有解, 否则该节点可以被提前删去). 类似地, 判断节点上的约束
与 ¬ϕ[i] 是否总冲突, 若总冲突则说明 ϕ[i] 在该节点一定成立. 否则, ϕ[i] 在该节点的冲突情况为未知 (第 8–11 行);
• ϕ[i] := ¬φ 1 时, 若 φ 1 在节点 q j 上总成立则 ϕ[i] 在节点 q j 上总冲突, 若 φ 1 在节点 q j 上总冲突则 ϕ[i] 在节点 q j
上总成立, 否则未知 (第 12 行);
• ϕ[i] := φ 1 ∨φ 2 时, ϕ[i] 的冲突情况为 φ 1 或 φ 2 在节点 q j 上的最好情况 (第 13 行);
• ϕ[i] := φ 1 U I φ 2 时, 若 φ 2 在当前节点以及后续所有节点都冲突, 则 ϕ[i] 在当前节点一定冲突; 否则, 由于路径
I 的关系无法明确, 所以冲突情况未知 (第 14–16 行).
节点与时间区间
譬如给定在图 3 所示的地图内移动的车辆导航系统, 车辆在不同网格有不同的期望速度, 网格内的蓝色箭头
代表期望速度的方向. 绿色网格为车辆出发点, 蓝色网格为目的点, 红色区域为危险区域. 因此, 导航系统的反例生
(2,2) 为中心的边长为 1 的红色正方形
成目标规约为 ¬F(|x−2| < 0.5 ∧ |y−2| < 0.5), 即车辆应总避免进入地图上以
危险区域. 在该导航系统对应的混成自动机中, 连续变量包括车辆的位置 x,y 等, 离散节点则与 25 个网格对应, 标
q 1 −q 25 , 相邻网格对应的节点间具有离散跳转. 在每个节点上, 不变式约束由网格位置决定. 由于该混成自动机
为
的初始节点为 q 19 , 终止节点为 , 因此, 图上的黑色路径 p = {q 19 ,q 14 ,q 9 ,q 4 ,q 3 ,q 2 } 即为一条系统路径.
q 2

5
4

3

2

1

0
0 1 2 3 4 5
图 3 导航系统的二维网格地图

根据算法 1 计算路径 p 是否需要被过滤的流程如表 2 所示. 对目标规约取反得到 φ neg = F(|x−2| < 0.5 ∧ |y−
2| < 0.5). 针对 φ neg 中包含的所有公式, 依次 (逐行) 计算公式在路径 p 每个节点上的约束满足情况, 从节点 q 2 自后
向前依次计算. 譬如节点 q 2 的不变式约束为 1 < x < 2∧0 < y < 1, 与公式 |x−2| < 0.5 不冲突, 与公式 ¬(|x−2| < 0.5)
也不冲突, 故约束满足情况未知, 记为 0; 而节点 q 4 的不变式约束为 3 < x < 4∧0 < y < 1, 与公式 |x−2| < 0.5 冲突,
故约束满足情况记为–1. 最终, 最后一列的公式 φ neg 在第 1 个节点 q 19 上沿该路径的约束满足情况为–1, 即冲突. 因