Abstract
The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism, where performance and dependability properties are analyzable by model checking. We present INFAMY, a model checker for arbitrarily structured infinite-state CTMCs. It checks probabilistic timing properties expressible in continuous stochastic logic (CSL). Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and impossible if the model is infinite. INFAMY only explores the model up to a finite depth, with the depth bound being computed on-the-fly. The computation of depth bounds is configurable to adapt to the characteristics of different classes of models.
This work is supported by the NWO-DFG bilateral project VOSS, by the DFG as part of the Transregional Collaborative Research Center SFB/TR 14 AVACS and the Graduiertenkolleg “Leistungsgarantien für Rechnersysteme”, and has received funding from the European Community’s Seventh Framework Programme under grant agreement no 214755.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-Checking Continuous-Time Markov Chains. ACM Trans. Comput. Log 1, 162–170 (2000)
Fox, B.L., Glynn, P.W.: Computing Poisson Probabilities. Commun. ACM 31, 440–445 (1988)
Grassmann, W.K.: Finding Transient Solutions in Markovian Event Systems Through Randomization. In: NSMC 1991, pp. 357–371 (1991)
van Moorsel, A.P.A., Sanders, W.H.: Adaptive Uniformization. Communications in Statistics - Stochastic Models 10, 619–647 (1994)
Munsky, B., Khammash, M.: The Finite State Projection Algorithm for the Solution of the Chemical Master Equation. Journal of Chemical Physics 124 (2006)
Zhang, L., Hermanns, H., Hahn, E.M., Wachter, B.: Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. In: ACSD, pp. 98–107 (2008)
Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng. 23, 279–295 (1997)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model checking meets performance evaluation. SIGMETRICS Performance Evaluation Review 32, 10–15 (2005)
Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate Probabilistic Model Checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004)
Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)
Zapreev, I.S.: Model Checking Markov Chains: Techniques and Tools. Ph.D thesis, University of Twente, Enschede, The Netherlands (2008)
Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. Technical Report No. 47, SFB/TR 14 AVACS (2009); To appear in Fundamenta Informaticae
Katoen, J.P., Klink, D., Leucker, M., Wolf, V.: Three-Valued Abstraction for Continuous-Time Markov Chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007)
Gross, P.J.E., Peccoud, J.: Quantitative modeling of stochastic systems in molecular biology by using stochastic Petri nets. Proc. Natl. Acad. Sci. USA 95, 6750–6755 (1998)
Haverkort, B.R., Hermanns, H., Katoen, J.P.: On the Use of Model Checking Techniques for Dependability Evaluation. In: SRDS, pp. 228–237 (2000)
Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Plateau, B., Stewart, W., Silva, M. (eds.) NSMC, pp. 188–207 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L. (2009). INFAMY: An Infinite-State Markov Model Checker. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_49
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_49
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)