基于惰性切片的线性时态逻辑性质验证

Lazy slicing based method for verifying linear temporal logic property

惰性切片是一种有效的状态空间缩减方法,但是它无法直接判定一个模型是否满足所期望的线性时间性质。针对该问题,提出了一种基于惰性切片的线性时态逻辑公式验证方法。该方法首先构造给定线性时态逻辑公式的否定Büchi自动机与系统模型的乘积自动机,然后使用惰性切片算法在该乘积自动机上以惰性方式搜索可接受迹,从而把线性时间性质验证问题转换为通过可达性分析搜索可接受状态的不变性检测过程。实验结果证明,基于惰性切片的线性时态逻辑公式验证算法在不损失验证结果正确性的前提下使惰性切片算法具备了验证线性时间性质的能力,同时也有效提高了LTL模型检测方法的可扩展性。

Lazy slicing is an effective state-space reduction method, but it can not directly determine whether a model satisfies the expected linear property. A lazy slicing based method is proposed to solve this problem. First, it constructs a negation Btichi automaton for given linear temporal logic formula and a product automaton of the system model. Then it searches for an acceptable trace on this product automaton lazily. Thus, the problem of verifying a linear time property is converted into the problem of invariance validation, which makes it possible to search the acceptable state by reachability analysis. Experiment results show that this lazy slicing based algorithm not only makes lazy slicing be able to verify linear time property, but also remarkably improves the scalability of LTL model checking.