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

计算机科学 ›› 2006, Vol. 33 ›› Issue (6): 1-6.

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

出版日期:2018-11-17 发布日期:2018-11-17
基金资助:
本课题研究得到国家自然科学基金（No.60203009,No.60233020,No.60425204）、江苏省自然科学基金（BK2003408）和国家重点基础研究973计划（No.2002CB312001）的资助.

Online:2018-11-17 Published:2018-11-17

摘要/Abstract

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

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

Abstract: 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

Key words: Real-time system, Timed automata, State space explosion, Reachability analysis

. 时间自动机可达性分析中的状态空间约减技术综述[J]. 计算机科学, 2006, 33(6): 1-6. https://doi.org/