An Algorithm to Dynamically Reduce the State Space of Timed Automata during the Reachability Analysis
一种动态消减时间自动机可达性搜索空间的方法

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