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

    43 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
    EventHardware 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

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Number2008/16200
    Volume4899

    Conference

    ConferenceHardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel
    CityLondon
    Period1/02/08 → …

    Keywords

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

    Cite this