摘要
对时间自动机的转换系统进行改进,提出了一个状态空间的极小化构造方法。该方法用位置和停留在该位置时的可能时钟值集合来表示状态,以此隐藏因时间流逝而引发的无穷状态,得到了改进的转换系统——时间段转换系统;并通过对转换可能发生时间的分析,去除无效转换;然后使用转换互模拟合并等价状态,实现了状态空间的极小化,有效地避免了状态空间爆炸。
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.
出处
《计算机工程与应用》
CSCD
北大核心
2007年第14期30-33,共4页
Computer Engineering and Applications
基金
国家自然科学基金(No.69873040)~~
关键词
时间自动机
转换系统
可达性
状态空间
模型检测
timed automata
transition systems
teachability
state space
model checking
