使用惰性切片算法验证LTL性质的核心步骤是把Kripke模型上的LTL性质验证问题转换为 上的不变性验证过程, 也即通过可达性分析对 进行穷尽搜索的过程。其中 为 对应的NBA, 的乘积自动机。

定义7 令 为给定系统的Kripke模型, 为所期望的LTL性质 对应的否定NBA, 且有 和 的乘积可定义为:

式中: 是由规则 确定的迁移集合, 其中 属于构成 的程序事件集; 为初始状态集合; 并且 即

注意到 的原子命题集合中的元素构成, 令:

为 上的一条路径, 则有

是 上的路径, 且

是 上的一个运行, 且有

被 接受。

构造出 后, 就可以通过判断 是否为空来确定 的模型, 也即判断 上是否存在可被 接受状态的过程。这样就把LTL性质验证问题转换为不变性检测问题, 也即通过可达性分析在 上搜索 可接受文字的过程。令命题逻辑公式

表示 可接受状态集合, 同时这个公式也是不变性检测过程中所要验证的不变性性质, 记为 于是LTL性质验证问题最终被归约为 是否是 的模型这一不变性检测过程。这为应用惰性切片算法验证 创造了充分条件。

应用惰性切片算法对 进行搜索的前提是构建 的过近似切片(Overapproximate slice), 而构建过近似切片的关键步骤是确定切片标准。

定义8 的一个切片标准是一个二元组 表示所有出现在 中的命题变量集合。

令 为 的过近似切片模型。由于相对 的状态空间规模很小, 所以 决定。为了减小计算 的过近似切片的代价, 实际应用中不直接计算 而是首先通过移除 的过近似切片 然后由 和 导出 的计算共有如下3个步骤。

步骤1 计算 的变量集 其不动点迭代计算公式如下:

当在迭代计算过程中第一次出现 时, 说明由 计算得到 时 相对于 不再变化, 此时有

步骤2 计算 的事件集合 。

步骤3 根据 计算 的初始状态集 式(4)给出了 的定义。

式中: 表示 在 下的投影状态。

步骤1~3从 的过近似切片标准 出发, 分别给出了变量集合 事件集合 及初始状态集合 的计算方法, 根据定义1知, 可直接由 和 诱导, 且 于是可通过步骤4和步骤5计算

步骤4 构造 的初始状态集

步骤5 根据 计算 的状态集 和迁移集 下面给出 和 的递归定义。

定义9 和 中的元素满足如下条件:

(1)

(2)对任意 如果存在 使得式(6)所示规则成立, 则有

(3)有限次使用条件(1)和(2)直到 和 中的元素不再发生变化, 此时的 和 即为 的状态集合和迁移集合。

和 可由定义7直接计算。 是 关于切片标准 的一个过近似切片。惰性切片算法可以在 上通过惰性搜索寻找标签被 接受的状态。如果惰性搜索算法找到标签被 接受的状态, 说明 不满足LTL性质 此时可终止搜索并返回由当前搜索路径生成的反例; 否则说明 满足

下面使用文献[10]中的进程互斥模型介绍如何计算 令 表示其Kripke模型, 表示待验证性质, 其中 表示 , 即进程 位于非关键区, 表示 即 尝试进入关键区。为了使用惰性切片技术分析验证 是否满足 首先构造 的非确定性Bü chi自动机 则 对应的NBA如图1所示。

图1

Fig.1

	Figure Option ViewDownloadNew Window
	图1 对应的非确定性Bü chi自动机Fig.1 Nondetermistic Bü chi automata of

图1中被有尾无头箭头标记的状态为初始状态, 如 黑边圆表示可接受状态, 如 所有状态到自身的迁移被省略。由于切片标准 中的 仅涉及 和 两个命题, 所以 而 的事件集中仅有 和 包含指派目标变量为 的指派表达式, 根据式(2)可得 由式(3)及文献[10]给出的优化方法可得 如图2所示。

图2

Fig.2

	Figure Option ViewDownloadNew Window
	图2 Ko对应的状态迁移系统Fig.2 State transition system of Ko

根据步骤4、步骤5可得 的过近似切片 其对应的状态迁移系统如图3所示。由图2、图3可以看出, 中共有3个状态, 也仅有4个可达状态。在 上完成对性质 的验证所需代价比在 上进行验证低两个量级。获得 后, 验证 是否满足 的问题, 就被转换为通过可达性分析在 上搜索 的可接受迹的过程, 这个验证过程就是不变性检测。因此可以把 作为惰性切片算法的初始输入。与基于CEGAR的切片方法相似, 当验证过程中出现反例时, 可使用文献[10]给出的方法对反例进行具体化, 从而判定该反例是否是伪反例。

图3

Fig.3

	Figure Option ViewDownloadNew Window
	图3 的状态迁移系统Fig.3 State transition system of

由于 共有4个可接受状态 和 而 上除了 外, 其他三个状态 和 都包含了 的可接受状态, 由初始状态出发到这些可接受状态的路径构成反例, 并且这些反例能够在 上找到对应的路径(能够具体化)。即可以在 上找到满足给定LTL性质 的路径, 这条路径就是 不满足 的证据, 该验证结果与实际情况一致。

算法1给出了基于惰性切片的LTL性质验证算法 该算法输入为给定系统模型 和LTL性质 算法获得输入后首先计算 的否定Bü chi自动机 接着构造由 的过近似切片模型 和 的乘积自动机 惰性搜索, 从而把LTL性质验证问题转换为在 上搜索可接受迹的过程, 当算法发现可接受迹时反回false, 同时把找到的可接受迹作为反例一并返回; 否则说明模型 满足 算法返回true并结束。

算法 1 LazySlicing_LTL(K, φ _LTL)

Require:Kripke model K, LTL formula φ _LTL

Ensure: return true if K|=φ _LTL, otherwise return false plus a counterexample

1.Compute ;

2.Compute K^o according to C_􀱋=(I_􀱋, var(􀱑F));

3.Get from K^o and ;

4.Let :=V^o, R:=∅, U:=null, flag:=false;

5.While 􀱑flag∧ ≠ ∅ do

6. Get a state s from and remove it from ;

7. Push(s, U);

8. R:=R∪ {s};

9. Repeat

10. s':=top(U);

11. If s|≠ 􀱑F then

12. If U is an real counterexample then

13. flag:=true;

14. Else

15. Refine then search lazily;

16. End If

17. Else

18. Search the successor of s' lazily;

19. End If

20. Until flag∨ U=null

21.End while

22.If 􀱑flag then

23. Return true;

24.Else

25. Return Reverse(U);

26.End If

LazySlicing_LTL(K, φ _LTL)通过把LTL性质验证过程转换为乘积自动机上的惰性搜索过程, 使惰性切片算法能够对LTL性质进行分析验证。由于这种基于惰性切片的LTL验证方法构造的乘积自动机本质上就是一种过近似切片, 所以在乘积自动机上展开的惰性搜索过程就是惰性切片过程。所以由文献[10]中对惰性切片算法的部分正确性定理和可终止性定理可得LazySlicing_LTL(K, φ _LTL)的部分正确性定理和可终止性定理。

定理1 令 为原始Kripke模型, 对任意 的可终止运行, 有①如果 返回true, 则对 中的任意状态 在 中必有一个状态覆盖 其中 为由 构造的NBA, 存储 搜索过的状态集合; ②否则, 返回一个混合精度反例 在 上可具体化, 且 上最后一个状态的标签为 的可接受状态。

定理2 是一个有限状态Kripke模型, 具备的LTL性质, 则 在 和 上的一次运行可终止, 即 可终止。

定理1、定理2保证了 算法本身的正确性, 其证明过程与文献[10]中对惰性切片算法的部分正确性和可终止性证明相同。

由于 把LTL性质验证问题转换为在乘积自动机 上的不变性验证过程, 所以当 返回true时仅能得出 满足 的结论, 当其返回反例时也仅得到了一个 不满足 的证据。然而, 算法的最终目的是验证 是否满足 也即下述性质是否成立。

定理3 返回true时 成立, 反回路径 时有 成立。

证明 令 当 返回true时, 对任意 有 成立, 也即 为 的可接受状态集合; 于是对 上的任意路径 有 所以:

成立, 也即 为空, 所以可得 即 当 返回一条路径 时, 令 为 上最后一个状态, 且有 即 于是有 于是可得 不为空, 也即 不为空, 所以 是 的证据, 即