loading...
Model Checking of Continuous-Time Markov Chains by Closed-Form Bounding Distributions
Riverside, California September 11-September 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2006.33Third International Conference on the ...
 This Article 
 
PDF
HTML
IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Mouad Ben Mamoun, Universite Mohammed V, Rabat, Maroc
Nihal Pekergin, Universite Paris 1, France
Sana Younes, PRiSM, Universite Versailles St Quentin, France
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.
Citation:
Mouad Ben Mamoun, Nihal Pekergin, Sana Younes, "Model Checking of Continuous-Time Markov Chains by Closed-Form Bounding Distributions," qest, pp.189-198, Third International Conference on the Quantitative Evaluation of Systems - (QEST'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.