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

【Abstract】 Timed automaton is a useful modeling tool for real-time systems. To check whether a system can reach a specific state,the reachability analysis algorithms explore the state space of timed automata by enumeration of symbolic states. Since clocks are used in timed automata,the algorithms generate large number of temporary states during state space exploration,so it requires a huge amount of computer memory. When such requirement excesses the feasible limitation,the model checking algorithm fails to return a result. This is the so called ’state space explosion’ problem. Many researchers contrive various optimization techniques to solve or mitigate this headache problem. This paper firstly presents the basic introduction of timed automata, then discusses some useful optimization techniques and gives a conclusion. Finally, some future directions are proposed.更多还原