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

Jansen, D.N. and Katoen, J.P. and Oldenkamp, M. and Stoelinga, M.I.A. and Zapreev, I.S. (2008) How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. In: Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007, 23-25 Oct 2007, Haifa, Israel.

PDF
Restricted to UT campus only: Request a copy
4Mb

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
Item Type:	Conference or Workshop Item
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/62646
Official URL:	http://dx.doi.org/10.1007/978-3-540-77966-7_9
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 255052