A Statistical Model Checker for Nondeterminism and Rare Events

Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns, Sean Sedwards

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

    15 Citations (Scopus)
    172 Downloads (Pure)


    Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in the presence of rare events, and it cannot soundly analyse nondeterministic models. In this tool paper, we present modes: a statistical model checker that combines fully automated importance splitting to efficiently estimate the probabilities of rare events with smart lightweight scheduler sampling to approximate optimal schedulers in nondeterministic models. As part of the Modest Toolset, it supports a variety of input formalisms natively and via the Jani exchange format. A modular software architecture allows its various features to be flexibly combined. We highlight its capabilities with an experimental evaluation across multi-core and distributed setups on three exemplary case studies.
    Original languageEnglish
    Title of host publicationProceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)
    EditorsDirk Beyer, Marieke Huisman
    Place of PublicationCham
    Number of pages19
    ISBN (Electronic)978-3-319-89963-3
    ISBN (Print)978-3-319-89962-6
    Publication statusPublished - 2018

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Dive into the research topics of 'A Statistical Model Checker for Nondeterminism and Rare Events'. Together they form a unique fingerprint.

    Cite this