How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison

D.N. Jansen, Joost P. Katoen, M. Oldenkamp, Mariëlle Ida Antoinette Stoelinga, I.S. Zapreev

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

40 Citations (Scopus)

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
Original languageUndefined
Title of host publicationHardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007
EditorsK. Yohav
Place of PublicationLondon
PublisherSpringer
Pages69-85
Number of pages17
ISBN (Print)978-3-540-77964-3
DOIs
Publication statusPublished - Feb 2008

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Number2008/16200
Volume4899

Keywords

  • EWI-14722
  • METIS-255052
  • IR-62646

Cite this

Jansen, D. N., Katoen, J. P., Oldenkamp, M., Stoelinga, M. I. A., & Zapreev, I. S. (2008). How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. In K. Yohav (Ed.), Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007 (pp. 69-85). [10.1007/978-3-540-77966-7_9] (Lecture Notes in Computer Science; Vol. 4899, No. 2008/16200). London: Springer. https://doi.org/10.1007/978-3-540-77966-7_9
Jansen, D.N. ; Katoen, Joost P. ; Oldenkamp, M. ; Stoelinga, Mariëlle Ida Antoinette ; Zapreev, I.S. / How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007. editor / K. Yohav. London : Springer, 2008. pp. 69-85 (Lecture Notes in Computer Science; 2008/16200).
@inproceedings{0e61e4dde9344b4e9c3fab4cb8c418f3,
title = "How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison",
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",
keywords = "EWI-14722, METIS-255052, IR-62646",
author = "D.N. Jansen and Katoen, {Joost P.} and M. Oldenkamp and Stoelinga, {Mari{\"e}lle Ida Antoinette} and I.S. Zapreev",
note = "10.1007/978-3-540-77966-7_9",
year = "2008",
month = "2",
doi = "10.1007/978-3-540-77966-7_9",
language = "Undefined",
isbn = "978-3-540-77964-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "2008/16200",
pages = "69--85",
editor = "K. Yohav",
booktitle = "Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007",

}

Jansen, DN, Katoen, JP, Oldenkamp, M, Stoelinga, MIA & Zapreev, IS 2008, How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. in K Yohav (ed.), Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007., 10.1007/978-3-540-77966-7_9, Lecture Notes in Computer Science, no. 2008/16200, vol. 4899, Springer, London, pp. 69-85. https://doi.org/10.1007/978-3-540-77966-7_9

How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. / Jansen, D.N.; Katoen, Joost P.; Oldenkamp, M.; Stoelinga, Mariëlle Ida Antoinette; Zapreev, I.S.

Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007. ed. / K. Yohav. London : Springer, 2008. p. 69-85 10.1007/978-3-540-77966-7_9 (Lecture Notes in Computer Science; Vol. 4899, No. 2008/16200).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison

AU - Jansen, D.N.

AU - Katoen, Joost P.

AU - Oldenkamp, M.

AU - Stoelinga, Mariëlle Ida Antoinette

AU - Zapreev, I.S.

N1 - 10.1007/978-3-540-77966-7_9

PY - 2008/2

Y1 - 2008/2

N2 - 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

AB - 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

KW - EWI-14722

KW - METIS-255052

KW - IR-62646

U2 - 10.1007/978-3-540-77966-7_9

DO - 10.1007/978-3-540-77966-7_9

M3 - Conference contribution

SN - 978-3-540-77964-3

T3 - Lecture Notes in Computer Science

SP - 69

EP - 85

BT - Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007

A2 - Yohav, K.

PB - Springer

CY - London

ER -

Jansen DN, Katoen JP, Oldenkamp M, Stoelinga MIA, Zapreev IS. How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. In Yohav K, editor, Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007. London: Springer. 2008. p. 69-85. 10.1007/978-3-540-77966-7_9. (Lecture Notes in Computer Science; 2008/16200). https://doi.org/10.1007/978-3-540-77966-7_9