Abstract: The reachability analysis based on timed automata is one of the most used methods for model checking. Its’ major weakness is the state-space-explosion problem. In this paper, we developed the traditional transition system and advanced a method of state space minimization. The method described 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 was brought by time elapsing. We removed the invalid transition by analyzing the possible occurring time of the transition. Then we minimized the transition system by utilizing the transition bisimulation, and avoided the state-space-explosion problem effectively.

Key words: timed automata, transition systems, reachability, state space, model checking

摘要： 基于时间自动机的可达性分析是模型检测最常用的方法之一，但该方法饱受状态空间爆炸问题的困扰。本文对时间自动机的转换系统进行改进，提出了一个状态空间的极小化构造方法。该方法用位置和停留在该位置时的可能时钟值集合来表示状态，以此隐藏因时间流逝而引发的无穷状态，得到了改进的转换系统——时间段转换系统；并通过对转换可能发生时间的分析，去除无效转换；然后使用转换互模拟合并等价状态，实现了状态空间的极小化，有效地避免了状态空间爆炸。

关键词: 时间自动机, 转换系统, 可达性, 状态空间, 模型检测