| 时间自动机状态空间的一个极小化构造方法 |
| |
| 引用本文： | 姬莉霞,周清雷,李占波,苏锦祥.时间自动机状态空间的一个极小化构造方法[J].计算机工程与应用,2007,43(14):30-33. |
| |
| 作者姓名： | 姬莉霞 周清雷 李占波 苏锦祥 |
| |
| 作者单位： | 1. 郑州大学,软件技术学院,郑州,450002
2. 郑州大学,信息工程学院,郑州,450052 |
| |
| 摘 要： | 对时间自动机的转换系统进行改进,提出了一个状态空间的极小化构造方法。该方法用位置和停留在该位置时的可能时钟值集合来表示状态,以此隐藏因时间流逝而引发的无穷状态,得到了改进的转换系统——时间段转换系统;并通过对转换可能发生时间的分析,去除无效转换;然后使用转换互模拟合并等价状态,实现了状态空间的极小化,有效地避免了状态空间爆炸。
|
| 关 键 词： | 时间自动机 转换系统 可达性 状态空间 模型检测 |
| 文章编号： | 1002-8331（2007）14-0030-04 |
| 收稿时间： | 2006-9-21 |
| 修稿时间： | 2006-12 |
Minimizing the state space of timed automata |
| |
| JI Li-xia,ZHOU Qing-lei,LI Zhan-bo,SU Jin-xiang.Minimizing the state space of timed automata[J].Computer Engineering and Applications,2007,43(14):30-33. |
| |
| Authors: | JI Li-xia ZHOU Qing-lei LI Zhan-bo SU Jin-xiang |
| |
| Affiliation: | 1.College of Software Teehnology,Zhengzhou University,Zhengzhou 450002,China ;2.College of Information Engineering,Zhengzhou University,Zhengzhou 450052,China |
| |
| Abstract: | In this paper,we develope the traditional transition system and advance a method of state space minimization.The method describes the state by location and the possible set of clocks staying in this location.We name that as time segment transition system.It hid the infinite state which is brought by time elapsing.We remove the invalid transition by analyzing the possible occurring time of the transition.Then we minimize the transition system by utilizing the transition bi-simulation,and avoide the state-space-explosion problem effectively. |
| |
| Keywords: | timed automata transition systems teachability state space model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
|
