Abstract:RED diagrams represent states of a timed automata in a single and integrated diagram for both the dense-time and the discrete parts of the states. This integration contributes greatly to the considerable efficiency of the model checker RED in verification of timed automata. On the other hand, the state-of-the-art model checkers for probabilistic timed automata (PTAs) still use different representations for the dense-time and the discrete parts of probabilistic states. This paper proposes an elegant way to extend RED diagrams to represent probabilistic states, yet reuses the structures of original RED diagrams and hence preserves their efficiency. It also implements a prototype tool for reachability analysis of PTAs based on the extended RED diagrams, while the PTA benchmarks distributed within the probabilistic model checkers PRISM and Modest are used to evaluate its performance. Experimental results show that our integrated representation of probabilistic state space can indeed help improve the time efficiency and scalability for PTA reachability analysis.