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. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Jansen, D. N., Katoen, J. P., Oldenkamp, M., Stoelinga, M., & Zapreev, I. (2008). How fast and fat is your probabilistic model checker? An experimental performance comparison. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4899 LNCS, pp. 69–85). https://doi.org/10.1007/978-3-540-77966-7_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
