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

• 作者: 叶海智 王静 黄宏涛 黄少滨
• 来源期刊: 吉林大学学报（工学版）
• 学科: 工学
• 关键词: 计算机软件 模型检测 惰性切片 线性时态逻辑 Büchi自动机 乘积自动机
• 年，卷（期）: 2015,（1）
• 页码范围: 245-251
• 页数: 7页
• 分类号: TP311.5
• 字数: 5723字
• 语种: 中文
• DOI: 10.13229/j.cnki.jdxbgxb201501036

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄少滨	哈尔滨工程大学计算机科学与技术学院	55	319	10.0	15.0
2	叶海智	河南师范大学河南省教育信息工程技术研究中心	60	298	8.0	15.0
3	王静	中国石化管道储运公司新乡输油处信息中心	27	99	5.0	9.0
4	黄宏涛	河南师范大学河南省教育信息工程技术研究中心	17	41	4.0	5.0