We present a model-checking algorithm for a system presented as a generalized semi-Markov process and a specification given as a deterministic timed automaton. This leads to a method for automatic verification of timing properties of finite-state probabilistic real-time systems.
Real-Time: Theory in Practice, REX Workshop, LNCS 600, pp. 28-44, 1991.