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.

• Type: Conference
• Year: 2007
• Where: HVC
• Authors: David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Mariëlle Stoelinga, Ivan S. Zapreev
• Keywords: Hardware, HVC 2007, Model Checkers, Model Checkers Etmcc, Probabilistic Model Checkers