State explosion is a well-known problem that impedes analysis and testing b
ased on state-space exploration. This problem is particularly serious in re
al-time systems because unbounded time values cause the state space to be i
nfinite even for simple systems. in this paper, we present an algorithm tha
t produces a compact representation of the reachable state space of a real-
time system. The algorithm yields a small state space, but still retains en
ough information for analysis. To avoid the state explosion which can be ca
used by simply adding time values to states, our algorithm uses history equ
ivalence and transition bisimulation to collapse states into equivalent cla
sses. Through history equivalence, states are merged into an equivalence cl
ass with the same untimed executions up to the states. Using transition bis
imulation, the states that have the same future behaviors are further colla
psed. The resultant state space is finite and can be used to analyze real-t
ime properties. To show the effectiveness of our algorithm, we have impleme
nted the algorithm and have analyzed several example applications.