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

doi:10.1007/978-3-540-77966-7_9

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

45 Citations (Scopus)

9 Downloads (Pure)

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 language	Undefined
Title of host publication	Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007
Editors	K. Yohav
Place of Publication	London
Publisher	Springer
Pages	69-85
Number of pages	17
ISBN (Print)	978-3-540-77964-3
DOIs	https://doi.org/10.1007/978-3-540-77966-7_9
Publication status	Published - Feb 2008
Event	Hardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel: Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007 - London Duration: 1 Feb 2008 → …

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Number	2008/16200
Volume	4899

Conference

Conference	Hardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel
City	London
Period	1/02/08 → …

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Keywords

EWI-14722
METIS-255052
IR-62646

Access to Document

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

http://eprints.eemcs.utwente.nl/secure2/14722/01/hvc07.pdf

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). Article 10.1007/978-3-540-77966-7_9 (Lecture Notes in Computer Science; Vol. 4899, No. 2008/16200). Springer. https://doi.org/10.1007/978-3-540-77966-7_9

Jansen, D.N. ; Katoen, Joost P. ; Oldenkamp, M. et al. / 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 ; Hardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel ; Conference date: 01-02-2008",

year = "2008",

month = feb,

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",

address = "Germany",

}

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, Hardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel, London, 1/02/08. 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. et al.
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 proceeding › Conference contribution › Academic › peer-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

T2 - Hardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel

Y2 - 1 February 2008

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). doi: 10.1007/978-3-540-77966-7_9