CSRL model checking with closed-form bounding distributions
Article No.: 21, Pages 1 - 10
Abstract
Continuous Stochastic Logic (CSL) which lets to express real time probabilistic properties on Continuous Time Markov Chains (CTMC) has been augmented by reward structures to check also performability measures. Thus Continuous Stochastic Reward Logic (CSRL) defined on Markov Reward Models (MRM) provides a framework to verify performance-related and as well as dependability-related measures. Probabilistic model checking can be provided through bounding transient, steady-state distributions of the underlying Markov chain, since models are checked to see if the considered measures are guaranteed or not. We propose to extend the model checking algorithm that we have proposed for CSL to the CSRL operators. This method is based on the construction of bounding models having closed-form transient and steady-state distributions by means of Stochastic Comparison technique. In the case when the model can be checked by this method we gain significantly in time and memory complexity. However in case when we can not conclude if the considered formula is satisfied or not, we may apply classical model checking algorithms.
References
[1]
A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model checking continuous time markov chains. In ACM Trans. on Comp. Logic, pages 162--170, 2000.
[2]
C. Baier, B. Haverkort, H. Hermanns, and J. Katoen. Automated performance and dependability evaluation using model checking. LNCS, 2459:64--88, 2002.
[3]
C. Baier, B. Haverkort, H. Hermanns, and J. Katoen. Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng., 29:524--541, 2003.
[4]
C. Baier, J. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time markov chains. In CONCUR LNCS 1664, pages 146--162, 1999.
[5]
E. Clarke, A. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 8:244--263, 1986.
[6]
L. Cloth. Model Checking Algorithms for Markov-Reward Models. PhD thesis, University of Twente, 2006.
[7]
B. Haverkort. Performance of Computer Communication Systems: A Model- Based Approach. John Wiley & Sons, 1998.
[8]
B. Haverkort, L. Cloth, H. Hermanns, J. Katoen, and E. Baier. Model checking performability properties. In Dependability Systems and NETWORKS (DSN), IEEE CS Press, 2002.
[9]
H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A tool for model-checking markov chains. International Journal on Software Tools for Technology Transfer, 4(2):153--172, 2003.
[10]
M. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic symbolic model checker. In PAPM/PROBMIV 2001 Tools Session, 2001.
[11]
M. B. Mamoun and N. Pekergin. Closed-form stochastic bounds on the stationary distribution of markov chains. Prob. in the Eng. and Inform. Science, 16:403--426, 2002.
[12]
M. B. Mamoun and N. Pekergin. Computing closed-form stochastic bounds on transient distributions of markov chains. In SAINT, 2005.
[13]
M. B. Mamoun, N. Pekergin, and S. Younès. Model checking of continuous-time markov chains by closed-form bounding distributions. In QEST: DBLP, IEEE Computer Society, 2006.
[14]
A. Muller and D. Stoyan. Comparison Methods for Stochastic Models and Risks. Wiley, New York, 2002.
[15]
N. Pekergin and S. Younès. Stochastic model checking with stochastic comparison. In EPEW/WS-FM, 2005.
[16]
T. S. Rappaport. Wireless Communication. Principles and Practice. Upper Saddle River, NJ. Prentices-hall, 1996.
[17]
P. R. D'Argenio, B. Jeannet, H. E. Jensen, and K. Larsen. Reduction and refinement strategies for probabilistic analysis. In PAPM-PROPMIV, 2001.
[18]
B. Sericola. Occupation times in markov processes. Communications in Statistics-Stochastic Models, 16(5):479--510, 2000.
[19]
M. Shaked and J. Shantikumar. Stochastic Orders and Their Applications. Academic Press, San Diago, 1994.
[20]
H. L. S. Younes and R. G. Simmons. Probabilistic verification of discrete event systems using acceptance sampling. In 14th International Conference on Computer Aided Verification (CAV), 2002.
- CSRL model checking with closed-form bounding distributions
Recommendations
Fluid model checking
CONCUR'12: Proceedings of the 23rd international conference on Concurrency TheoryIn this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a ...
Model checking single agent behaviours by fluid approximation
In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a ...
Model Checking of Continuous-Time Markov Chains by Closed-Form Bounding Distributions
QEST '06: Proceedings of the 3rd international conference on the Quantitative Evaluation of SystemsContinuous-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 ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
- Create-Net
Publisher
ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering)
Brussels, Belgium
Publication History
Published: 20 October 2008
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 59Total Downloads
- Downloads (Last 12 months)16
- Downloads (Last 6 weeks)4
Reflects downloads up to 26 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in