View article

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 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 …