Simulation-based CTMC Model Checking: An Empirical Evaluation

Joost P. Katoen, I.S. Zapreev

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

    11 Citations (Scopus)
    195 Downloads (Pure)


    This paper provides an experimental study of the efficiency of simulation-based model-checking algorithms for continuous-time Markov chains by comparing: MRMC - the only tool that implements (new) confidence-interval-based algorithms for verification of all main CSL formulae; Ymer - that allows for verification oftime-bounded and time-interval until using sequential acceptance sampling; and VESTA - that can verify time-bounded and unbounded until by means of simple hypothesis testing. The study shows that MRMC provides the most accurate verification results. Ymer and VESTA, unlike MRMC, have almost constant memory consumption. Ymer requiresthe least number of observations to assess the model-checking problem, but MRMC is mostly the fastest. This indicates that the tools' efficiency does not so muchdepend on sampling but is rather determined by extra computations.
    Original languageUndefined
    Title of host publicationSixth International Conference on the Quantitative Evaluation of Systems
    Place of PublicationLos Alamitos
    Number of pages10
    ISBN (Print)978-1-42444-942-2
    Publication statusPublished - Sept 2009
    Event6th International Conference on Quantitative Evaluation of SysTems, QEST 2009 - Technical University of Budapest, Budapest, Hungary
    Duration: 13 Sept 200916 Sept 2009
    Conference number: 6

    Publication series

    PublisherIEEE Computer Society Press


    Conference6th International Conference on Quantitative Evaluation of SysTems, QEST 2009
    Abbreviated titleQEST
    Internet address


    • METIS-264290
    • EWI-17103
    • IR-69307

    Cite this