Model Checking of Continuous-Time Markov Chains by Closed-Form Bounding Distributions

Continuous-time Markov chains (CTMCs) have been largely applied with combination of high-level model specification techniques as performance evaluation and dependability, reliability analysis models for computer and communication systems. These models can be complemented by probabilistic model checking formalisms based on temporal logic to specify the guarantees on the measures of interest. We consider in this paper continuous stochastic logic (CSL) which lets to express real-time probabilistic properties on CTMCs. It has been shown that the CSL operators can be checked by means of transient or steady-state analysis of the underlying CTMC. Since models are checked to see if the considered measures are guaranteed or not, bounding techniques are useful in probabilistic model checking. We propose to apply stochastic comparison technique to construct bounding models having a special structure which provides closed-form solutions to compute both transient and steady-state distributions. We present an algorithm to provide rapid model checking by means of these closed-form bounding distributions. Obviously, bounding distributions may not let to decide if the underlying model meets the probability thresholds or not. However in the case where the model can be checked by the proposed method, we gain significantly in time and memory complexity