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.