Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains

• Autorzy: Hahn E.M. , Hermanns H. , Wachter B. , Zhang L.
• Języki publikacji: EN

Abstrakty

EN

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism that captures such performance and dependability properties, and makes them analyzable by model checking. In this paper, we focus on time-bounded probabilistic properties of infinite-state CTMCs, expressible in a subset of continuous stochastic logic (CSL). This comprises important dependability measures, such as time-bounded probabilistic reachability, performability, survivability, and various availability measures like instantaneous, conditional instantaneous and interval availabilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This paper presents a method that only explores the model up to a finite depth. The required depth is determined on the fly by an algorithm that is configurable in order to adapt to the characteristics of different classes of models. We provide experimental evidence showing that our method is effective.

Słowa kluczowe

EN

Markov chains; model checking; truncation; uniformization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 95, nr 1
• Strony: 129--155
• Opis fizyczny: Bibliogr. 35 poz., tab.

Twórcy

autor

Hahn E.M.

autor

Hermanns H.

autor

Wachter B.

autor

Zhang L.

• Department of Computer Science, Saarland University, Saarbrücken, Germany,

Bibliografia

• [1] M. Abramowitz and I. A. Stegun. Handbook of mathematical functions. 1964.
• [2] R. Alur and T. A. Henzinger. Reactive Modules. Formal Methods in System Design, 15(1):7-48, 1999.
• [3] W. J. Anderson. Continuous-Time Markov Chains: An Applications-Oriented Approach. Springer Verlag, 1991.
• [4] A. Aziz, K. Sanwal, V. Singhal, and R. K. Brayton. Model-Checking Continuous-TimeMarkov Chains. ACM Trans. Comput. Log, 1(1):162-170, 2000.
• [5] C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. On the Logical Characterisation of Performability Properties. In ICALP, volume 1853 of Lecture Notes in Computer Science, pages 780-792. Springer, 2000.
• [6] C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Model-CheckingAlgorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng, 29(6):524-541, 2003.
• [7] C. Baier, J.-P. Katoen, H. Hermanns, and V. Wolf. Comparative Branching-Time Semantics for Markov Chains. Information and computation, 200(2):149-214, 2005.
• [8] M. D. Beaudry. Performance-Related Reliability Measures for Computing Systems. IEEE Trans. on Comp. Sys, 27(6):540-547, 1978.
• [9] A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. SymbolicModel Checking without BDDs. In TACAS, volume 1579 of Lecture Notes in Computer Science, pages 193-207. Springer, 1999.
• [10] E. A. Emerson and E. M. Clarke. Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Sci. Comput. Program, 2(3):241-266, 1982.
• [11] B. L. Fox and P. W. Glynn. Computing Poisson Probabilities. Commun. ACM, 31(4):440-445, 1988.
• [12] W. K. Grassmann. Finding Transient Solutions in Markovian Event Systems Through Randomization. In Numerical Solution of Markov Chains, pages 357-371, 1991.
• [13] P. J. E. Gross and J. Peccoud. Quantitative modeling of stochastic systems in molecular biology by using stochastic Petri nets. Proc. Natl. Acad. Sci., 95:6750-6755, 1998.
• [14] E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. Infamy: An infinite-state markov model checker. In CAV, 2009 (to appear).
• [15] B. R. Haverkort, H. Hermanns, and J.-P. Katoen. On the Use ofModel Checking Techniques for Dependability Evaluation. In SRDS, pages 228-237, 2000.
• [16] A. Hinton, M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In TACAS, volume 3920 of Lecture Notes in Computer Science, pages 441-444. Springer, 2006.
• [17] G. J. Holzmann. The Model Checker SPIN. IEEE Trans. Software Eng., 23(5):279-295, 1997.
• [18] J. Jackson. Networks of Waiting Lines. Operations Research, 5:518-521, 1957.
• [19] J.-P. Katoen, M. Khattri, and I. S. Zapreev. A Markov Reward Model Checker. In QEST, pages 243-244. IEEE Computer Society, 2005.
• [20] J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf. Three-Valued Abstraction for Continuous-Time Markov Chains. In CAV, volume 4590 of Lecture Notes in Computer Science, pages 311-324. Springer, 2007.
• [21] J.-P. Katoen, M. Z. Kwiatkowska, G. Norman, and D. Parker. Faster and Symbolic CTMC Model Checking. In PAPM-PROBMIV, volume 2165 of Lecture Notes in Computer Science, pages 23-38. Springer, 2001.
• [22] M. Z. Kwiatkowska, G. Norman, and D. Parker. Stochastic Model Checking. In SFM, volume 4486 of Lecture Notes in Computer Science, pages 220-270. Springer, 2007.
• [23] J. F. Meyer. Performability Evaluation: Where It Is and What Lies Ahead. IEEE Int. Comp. Perf. And Dependability Symp, pages 334-343, 1995.
• [24] B. Munsky and M. Khammash. The Finite State Projection Algorithm for the Solution of the Chemical Master Equation. Journal of Chemical Physics, 124(044104), 2006.
• [25] B. Munsky and M. Khammash. A Multiple Time Interval Finite State Projection Algorithm for the Solution of the Chemical Master Equation. Journal of Computational Physics, 2007.
• [26] B. Munsky and M. Khammash. Computation of Switch Time Distributions in Stochastic Gene Regulatory Networks. In American Control Conference, pages 2761-2766, 2008.
• [27] A. Remke and B. R. Haverkort. CSL Model Checking Algorithms for Infinite-State Structured Markov Chains. In FORMATS, volume 4763 of Lecture Notes in Computer Science, pages 336-351. Springer, 2007.
• [28] A. Remke, B. R. Haverkort, and L. Cloth. CSL Model Checking Algorithms for QBDs. Theor. Comput. Sci, 382(1):24-41, 2007.
• [29] W. J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994.
• [30] N. M. van Dijk. On the finite horizon Bellman equation for controlled Markov jump models with unbounded characteristics. Stochastic Proc. Appl, 28:141-157, 1988.
• [31] A. P. A. van Moorsel. Performability Evaluation Concepts and Techniques. PhD thesis, Universiteit Twente, 1993.
• [32] A. P. A. vanMoorsel andW. H. Sanders. Adaptive Uniformization. Communications in Statistics - Stochastic Models, 10(3):619-647, 1994.
• [33] B. Wachter, L. Zhang, and H. Hermanns. Probabilistic Model Checking Modulo Theories. In QEST, pages 129-138. IEEE Computer Society, 2007.
• [34] H. L. S. Younes. Ymer: A statistical model checker. In CAV, volume 3576 of Lecture Notes in Computer Science, pages 429-433. Springer, 2005.
• [35] L. Zhang, H. Hermanns, E. M. Hahn, and B. Wachter. Time-Bounded Model Checking of Infinite-State Continuous-TimeMarkov Chains. In ACSD, pages 98-107. IEEE, 2008.