时间自动机的LTL性质模型检测研究  

LTL Model Checking for Timed Automata

作　　者：彭云全[1,2] 魏绪凯[1,2] 李广元[1] 

机构地区：[1]中国科学院软件研究所,北京100080 [2]中国科学院研究生院,北京100049

出　　处：《计算机仿真》2009年第5期92-95,共4页Computer Simulation

基　　金：国家自然科学基金(60673051,60736017,60721061);国家973计划资助(2002cb312200)

摘　　要：为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略。采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题。与DTSp in等著名的模型检测工具进行了实验比较,取得了较好的实验结果。The research on model checking based on timed automata is done in order to enhance the model checking tool＇ s ability and efficiency. The process of the state - space＇ s generation is further analyzed. The design and implementation of the model checking tool that cheeks LTL properties is well studied, and the results of different strategies are discussed. Some improvements of the generation and storage of the state - space are made to enhance the model checking tool＇ s ability and efficiency. A data structure named BDD（ Binary Decision Diagram） is used to reduce the consumption of memory in the process of state - space generation. The experimental results show that this tool is more effective than other similar tools, such as the famous DTSpin.

关 键 词：时间自动机 模型检测 线性时序逻辑性质 二叉决策图共享存储 

分 类 号：N945.12[自然科学总论—系统科学]