Model-checking is a method of verifying concurrent systems in which a state-graph model of the system behavior is compared with a temporal logic formula. This paper extends model-checking to {\it stochastic real-time\/} systems, whose behavior depends on probabilistic choice and quantitative time. The specification language is TCTL, a branching-time temporal logic for expressing real-time properties. We interpret the formulas of the logic over generalized semi-Markov processes. Our model can express constraints like ``the delay between the request and the response is distributed uniformly between 2 to 4 seconds''.
We present an algorithm that combines model-checking for real-time non-probabilistic systems with model-checking for finite-state discrete-time Markov chains. The correctness of the algorithm is not obvious, because it analyzes the projection of a Markov process onto a finite state space. The projection process is not Markov, so our most significant result is that the model-checking algorithm works.
Automata, Languages and Programming: Proc. of the 18th ICALP, LNCS 510, pp. 115-136, 1991.