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

摘要：

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

关键词：离散时间自动机、非空性检测、线性时序逻辑性质

分类号：N945.12(系统科学)

资助基金：国家自然科学基金资助项目60673051,60421001;国家973计划资助项目2002cb312200

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

页数：共4页

页码：80-83