一种基于离散时间自动机的LTL性质检测工具

• 作者: 张文亮 彭云全
• 来源期刊: 计算机仿真
• 学科: 地球科学
• 关键词: 离散时间自动机 非空性检测 线性时序逻辑性质
• 年，卷（期）: 2008,（4）
• 所属期刊栏目: 建模与验模
• 页码范围: 80-83
• 页数: 4页
• 分类号: N945.12
• 字数: 3741字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-9348.2008.04.021

摘要

模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点.目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低.介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度.实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张文亮	中国科学院软件研究所计算机科学国家重点实验室	3	25	2.0	3.0
5	彭云全	中国科学院软件研究所计算机科学国家重点实验室	2	2	1.0	1.0