Abstract
This paper studies the efficiency of several probabilistic model checkers by comparing verification times and peak memory usage for a set of standard case studies. The study considers the model checkers ETMCC, MRMC, PRISM (sparse and hybrid mode), YMER and VESTA, and focuses on fully probabilistic systems. Several of our experiments show significantly different run times and memory consumptions between the tools—up to various orders of magnitude—without, however, indicating a clearly dominating tool. For statistical model checking YMER clearly prevails whereas for the numerical tools MRMC and PRISM (sparse) are rather close.
This research has been partially funded by the Netherlands Organisation for Scientific Research (NWO) under FOCUS/BRICKS grant numbers 642.000.505 (MOQS) and 612.000.311 (MC=MC); the EU under grant number IST-004527 (ARTIST2); the DFG/NWO bilateral cooperation programme under project number DN 62-600 (VOSS2); and by the DFG Research Training Group 1298 (AlgoSyn).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. ENTCS 153(2), 213–239 (2006)
Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88–104. Springer, Berlin (2004)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
Baier, C., Ciesinski, F., Größer, M.: ProbMela and verification of Markov decision processes. SIGMETRICS Perform. Eval. Rev. 32(4), 22–27 (2005)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Softw. Eng. 29(6), 524–541 (2003)
Bode, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Wimmer, R., Becker, B.: Compositional Performability Evaluation for STATEMATE. In: Quantitative Evaluation of Systems: QEST, pp. 167–178. IEEE CS, Los Alamitos (2006)
Changuion, B., Davies, I., Nelte, M.: DaNAMiCS: A Petri net editor (2007), http://www.cs.uct.ac.za/Research/DNA/microweb/danamics/DNAFrameH.html
Cox, D.R.: A use of complex probabilities in the theory of stochastic processes. In: Proc. Cambridge Philosophical Society, vol. 51, pp. 313–319 (1955)
D’Aprile, D., Donatelli, S., Sproston, J.: CSL model checking for the GreatSPN tool. In: Aykanat, C., Dayar, T., Körpeoğlu, İ. (eds.) ISCIS 2004. LNCS, vol. 3280, pp. 543–552. Springer, Heidelberg (2004)
Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica 1, 115–138 (1971)
Fokkink, W., Pang, J.: Simplifying Itai-Rodeh leader election for anonymous rings. ENTCS 128(6), 53–68 (2005)
Gupta, R., Smolka, S.A., Bhaskar, S.: On randomization in sequential and distributed algorithms. ACM Comput. Surv. 26(1), 7–86 (1994)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Hartonas-Garmhausen, V., Campos, S., Clarke, E.M.: ProbVerus: probabilistic symbolic model checking. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 96–110. Springer, Heidelberg (1999)
Hermanns, H., Herzog, U., Klehmet, U., Mertsiotakis, V., Siegle, M.: Compositional performance modelling with the TIPPtool. Performance Evaluation 39(1–4), 5–35 (2000)
Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A Markov chain model checker. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000, LNCS, vol. 1785, pp. 347–362. Springer, Heidelberg (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.J., Silva, M. (eds.) Num. Sol. of Markov Chains, Zaragoza, Prensas Universitarias, pp. 188–207 (1999)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, New York (1996)
Hogg, R.V., Craig, A.T.: Introduction to Mathematical Statistics, 4th edn. Macmillan, New York (1978)
Ibe, O.C., Trivedi, K.S.: Stochastic Petri net models of polling systems. IEEE J. on Sel. Areas in Comm. 8(9), 1649–1657 (1990)
Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. and Comp. 88(1), 60–87 (1990)
Karlin, S., McGregor, J.L.: The differential equations of birth-and-death processes, and the Stieltjes moment problem. Trans. of the AMS 85(2), 489–546 (1957)
Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Quantitative Evaluation of Systems, pp. 243–244. IEEE CS, Los Alamitos (2005)
Katoen, J.-P., Zapreev, I.S.: Safe on-the-fly steady-state detection for time-bounded reachability. In: Quantitative Evaluation of Systems: QEST, pp. 301–310. IEEE CS, Los Alamitos (2006)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., et al. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)
Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal methods for performance evaluation. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)
Lassaigne, R., Peyronnet, S.: Approximate verification of probabilistic systems. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 213–214. Springer, Heidelberg (2002)
Lecca, P., Priami, C.: Cell cycle control in eukaryotes: A BioSpi model. Technical Report DIT-03-045, Informatica e Telecommunicazioni: University of Trento (2003)
Mohanty, S.G., Montazer-Haghighi, A., Trueblood, R.: On the transient behavior of a finite birth-death process with an application. Computers and Operations Research 20(3), 239–248 (1993)
Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. J. of Computer Security 14(6), 561–589 (2006)
Oldenkamp, M.: Probabilistic model checking: A comparison of tools. MSc thesis, Univ. of Twente, Netherlands (2007), http://www.cs.utwente.nl/~oldenkampha/
Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite horizon analysis of Markov chains with the Murphi verifier. STTT 8(4-5), 397–409 (2006)
Pnueli, A., Zuck, L.D.: Verification of multiprocess probabilistic protocols. Distributed Comput. 1(1), 53–72 (1986)
PRISM: Probabilistic symbolic model checker (2006), http://www.cs.bham.ac.uk/~dxp/prism/
Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)
Shedler, G.S.: Regenerative Stochastic Simulation. Academic Pr, London (1993)
Somenzi, F.: CUDD: CU decision diagram package. Public software (1997), http://vlsi.colorado.edu/~fabio/CUDD/
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)
Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216–228 (2006)
Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jansen, D.N., Katoen, JP., Oldenkamp, M., Stoelinga, M., Zapreev, I. (2008). How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison . In: Yorav, K. (eds) Hardware and Software: Verification and Testing. HVC 2007. Lecture Notes in Computer Science, vol 4899. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77966-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-77966-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77964-3
Online ISBN: 978-3-540-77966-7
eBook Packages: Computer ScienceComputer Science (R0)