## Verifying Automata Specifications of Probabilistic Real-Time Systems

*Rajeev Alur, Costas Courcoubetis, and
David L. Dill*
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.