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

A Study of Optimization Techniques about Reachability in Timed Automata

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

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

出　　处：《计算机科学》2006年第6期1-6,100,共7页Computer Science

基　　金：国家自然科学基金(No.60203009;No.60233020;No.60425204);江苏省自然科学基金(BK2003408);国家重点基础研究973计划(No.2002CB312001)的资助。

摘　　要：时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存储空间,往往超出了计算机能力的极限,导致分析和检验不能完成。这就是所谓的“状态空间爆炸”。研究人员设计了很多种优化技术来约减可达性分析所需的存储空间,以解决或者缓解这个问题。本文首先介绍了时间自动机及其可达性分析的基本概念,然后分类讨论了现有的空间约减优化技术并对此做出总结,最后提出了一些未来的研究方向。Timed automaton is a useful modeling tool for real-time systems. To check whether a system can reach a specific state, the teachability 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 con clusion. Finally, some future directions are proposed.

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

分 类 号：TP183[自动化与计算机技术—控制理论与控制工程]