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

An Algorithm to Dynamically Reduce the State Space of Timed Automata during the Reachability Analysis

作　　者：陈铭松[1] 赵建华[1] 李宣东[1] 郑国梁[1] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室

出　　处：《计算机科学》2007年第1期213-218,共6页Computer Science

基　　金：国家自然科学基金(No60573085);国家重点基础研究973计划(No2002CB312001)的资助

摘　　要：时间自动机的可达性分析算法通常采用对符号状态的枚举来遍历其状态空间。符号状态由位置与时间区域组成,时间区域用形如x-y≤(<)n的原子公式的合取式来表示。在对时间自动机进行可达性分析的过程中,分析算法将生成大量的符号状态,往往导致对计算机内存的需求超出了可行的范围。本文给出了一个消减符号状态个数的方法。该方法通过对符号状态间的依赖关系进行分析,在不影响分析结果的前提下消去某些时间区域的原子公式,从而扩展符号状态。扩展后的符号状态包含有更加多的其它的状态,通过删除掉那些被包含的符号状态可以减少算法存储的状态个数,节省存储空间。本文最后给出了相关的案例分析,结果表明这个算法有效地减少了某些时间自动机可达性分析过程中所需的存储空间。The reachability analysis algorithm explores the state space of a timed automaton by enumeration of symbolic states. Each symbolic state consists of a location and a time zone which are conjunctions of automatic formulae in the form x-y≤（〈）n. Sometimes the amount of generated symbolic states is very large, the memory required to store the generated symbolic states is not feasible. In this paper, we present an approach to reduce the memory requirement of the teachability analysis algorithm. By analyzing the dependence relation between symbolic states, we can expand some of the symbolic states by removing Specific kinds of atomic formulae without changing the reachabUity analysis result. The expanded states can contain more symbolic states. Removing these contained states can reduce the memory requirement of reachability analysis. The case studies presented in this paper show that our algorithm can save memory in the practical application efficiently.

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

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]