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

Lazy slicing based method for verifying linear temporal logic property

作　　者：黄宏涛[1] 王静[2] 叶海智[1] 黄少滨[3] 

机构地区：[1]河南师范大学河南省教育信息工程技术研究中心,河南新乡453007 [2]中国石化管道储运公司新乡输油处信息中心,河南新乡453007 [3]哈尔滨工程大学计算机科学与技术学院,哈尔滨150001

出　　处：《吉林大学学报（工学版）》2015年第1期245-251,共7页Journal of Jilin University:Engineering and Technology Edition

基　　金：国家科技支撑计划项目(2012BAH08B02);河南省科技攻关计划项目(082400420250;112300410008);河南省教育厅科学技术研究重点项目(13A520508);河南师范大学博士科研启动基金项目(qd12107);河南师范大学青年科学基金项目(2013qk33)

摘　　要：惰性切片是一种有效的状态空间缩减方法,但是它无法直接判定一个模型是否满足所期望的线性时间性质。针对该问题,提出了一种基于惰性切片的线性时态逻辑公式验证方法。该方法首先构造给定线性时态逻辑公式的否定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.

关 键 词：计算机软件 模型检测 惰性切片 线性时态逻辑 BÜCHI自动机 乘积自动机 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]