## Model-Checking for Probabilistic Real-Time Systems

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