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

摘要：

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

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

所属期刊栏目：45

分类号：TP311.5(计算技术、计算机技术)

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

在线出版日期：2016-05-17（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：245-251