zbMATH — the first resource for mathematics

Model-checking for probabilistic real-time systems. (English) Zbl 0769.68088
Automata, languages and programming, Proc. 18th Int. Colloq., Madrid/Spain 1991, Lect. Notes Comput. Sci. 510, 115-126 (1991).
Summary: [For the entire collection see Zbl 0753.00027.]
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. The projection process is not Markov, so our most significant result is that the model-checking algorithm works.

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science