时间自动机可达性分析中的状态空间约减技术综述

摘要：

时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间.因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存储空间,往往超出了计算机能力的极限,导致分析和检验不能完成.这就是所谓的"状态空间爆炸".研究人员设计了很多种优化技术来约减可达性分析所需的存储空间,以解决或者缓解这个问题.本文首先介绍了时间自动机及其可达性分析的基本概念,然后分类讨论了现有的空间约减优化技术并对此做出总结,最后提出了一些未来的研究方向.

关键词：实时系统、时间自动机、状态空间爆炸、可达性分析

所属期刊栏目：33

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金60203009;60233020;60425204;江苏省自然科学基金BK2003408;国家重点基础研究发展计划973计划2002CB312001

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

页数：共6页

页码：1-6,100