Simulation and Bisimulation for Probabilistic Timed Automata

Probabilistic timed automata are an extension of timed automata with discrete probability distributions. Simulation and bisimulation relations are widely-studied in the context of the analysis of system models, with applications in the stepwise development of systems and in model reduction. In this paper, we study probabilistic timed simulation and bisimulation relations for probabilistic timed automata. We present an EXPTIME algorithm for deciding whether two probabilistic timed automata are probabilistically timed similar or bisimilar. Furthermore, we consider a logical characterization of probabilistic timed bisimulation.