一种动态消减时间自动机可达性搜索空间的方法

摘要：

时间自动机的可达性分析算法通常采用对符号状态的枚举来遍历其状态空间.符号状态由位置与时间区域组成,时间区域用形如x-y≤(＜)n的原子公式的合取式来表示.在对时间自动机进行可达性分析的过程中,分析算法将生成大量的符号状态,往往导致对计算机内存的需求超出了可行的范围.本文给出了一个消减符号状态个数的方法.该方法通过对符号状态间的依赖关系进行分析,在不影响分析结果的前提下消去某些时间区域的原子公式,从而扩展符号状态.扩展后的符号状态包含有更加多的其它的状态,通过删除掉那些被包含的符号状态可以减少算法存储的状态个数,节省存储空间.本文最后给出了相关的案例分析,结果表明这个算法有效地减少了某些时间自动机可达性分析过程中所需的存储空间.

关键词：时间自动机、模型检验、符号状态、时间区域

所属期刊栏目：34

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

资助基金：国家自然科学基金60573085;国家重点基础研究发展计划973计划2002CB312001

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

页数：共6页

页码：213-218