| 时间自动机可达性分析中的状态空间约减技术综述 |
| |
| 引用本文： | 陈铭松,赵建华,李宣东,郑国梁.时间自动机可达性分析中的状态空间约减技术综述[J].计算机科学,2006,33(6):1-6. |
| |
| 作者姓名： | 陈铭松 赵建华 李宣东 郑国梁 |
| |
| 作者单位： | 南京大学计算机软件新技术国家重点实验室,南京大学计算机科学与技术系,南京210093 |
| |
| 基金项目： | 国家自然科学基金;江苏省自然科学基金;国家重点基础研究发展计划(973计划) |
| |
| 摘 要： | 时间自动机是检验实时系统建模的有效工具，其可达性分析可以检验系统是否可能达到某些特定的状态，其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量，时间自动机的可达性分析算法会产生大量的中间状态，需要巨大的存储空间，往往超出了计算机能力的极限，导致分析和检验不能完成。这就是所谓的“状态空间爆炸”。研究人员设计了很多种优化技术来约减可迭性分析所需的存储空间，以解决或者缓解这个问题。本文首先介绍了时间自动机及其可达性分析的基本概念，然后分类讨论了现有的空间约减优化技术并对此做出总结，最后提出了一些未来的研究方向。
|
| 关 键 词： | 实时系统 时间自动机 状态空间爆炸 可达性分析 |
A Study of Optimization Techniques about Reachability in Timed Automata |
| |
| CHEN Ming-Song,ZHAO Jian-Hua,LI Xuan-Dong,ZHENG Guo-Liang.A Study of Optimization Techniques about Reachability in Timed Automata[J].Computer Science,2006,33(6):1-6. |
| |
| Authors: | CHEN Ming-Song ZHAO Jian-Hua LI Xuan-Dong ZHENG Guo-Liang |
| |
| Affiliation: | National Laboratory of Novel Software Technology,Department of Computer Science and Teehnology,Nanjing University,Nanjing 210093 |
| |
| 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 |
| |
| Keywords: | Real-time system Timed automata State space explosion Reachability analysis |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
