Sound statistical model checking for MDP using partial order and confluence reduction

Arnd Hartmanns, Mark Timmer

    Research output: Contribution to journalArticleAcademicpeer-review

    6 Citations (Scopus)
    24 Downloads (Pure)

    Abstract

    Statistical model checking (SMC) is an analysis method that circumvents the state space explosion problem in model-based verification by combining probabilistic simulation with statistical methods that provide clear error bounds. As a simulation-based technique, it can in general only provide sound results if the underlying model is a stochastic process. In verification, however, models are very often variations of nondeterministic transition systems. In classical exhaustive model checking, partial order reduction and confluence reduction allow the removal of spurious nondeterministic choices. In this paper, we show that both can be adapted to detect and discard such choices on-the-fly during simulation, thus extending the applicability of SMC to a subclass of Markov decision processes. We prove their correctness in a uniform way and study their effectiveness and efficiency using an implementation in the modes simulator for the Modest modelling language. The examples we use highlight the different strengths and limitations of the two approaches. We find that runtime may be affected by unnecessary recomputations, and thus also investigate the feasibility of caching results to speed up simulation at the cost of increased memory usage.
    Original languageEnglish
    Pages (from-to)429-456
    Number of pages28
    JournalInternational journal on software tools for technology transfer
    Volume17
    Issue number4
    DOIs
    Publication statusPublished - Aug 2015

    Fingerprint

    Model checking
    Acoustic waves
    Random processes
    Explosions
    Statistical methods
    Simulators
    Data storage equipment
    Statistical Models

    Keywords

    • EC Grant Agreement nr.: FP7/295261
    • EC Grant Agreement nr.: FP7/318490
    • EC Grant Agreement nr.: FP7/2007-2013
    • EWI-26155
    • Markov Decision Processes
    • Confluence reduction
    • Statistical Model Checking
    • Partial order reduction
    • METIS-314922
    • IR-98145
    • Simulation

    Cite this

    @article{9462b11013e041f58bd28a449b4e7f29,
    title = "Sound statistical model checking for MDP using partial order and confluence reduction",
    abstract = "Statistical model checking (SMC) is an analysis method that circumvents the state space explosion problem in model-based verification by combining probabilistic simulation with statistical methods that provide clear error bounds. As a simulation-based technique, it can in general only provide sound results if the underlying model is a stochastic process. In verification, however, models are very often variations of nondeterministic transition systems. In classical exhaustive model checking, partial order reduction and confluence reduction allow the removal of spurious nondeterministic choices. In this paper, we show that both can be adapted to detect and discard such choices on-the-fly during simulation, thus extending the applicability of SMC to a subclass of Markov decision processes. We prove their correctness in a uniform way and study their effectiveness and efficiency using an implementation in the modes simulator for the Modest modelling language. The examples we use highlight the different strengths and limitations of the two approaches. We find that runtime may be affected by unnecessary recomputations, and thus also investigate the feasibility of caching results to speed up simulation at the cost of increased memory usage.",
    keywords = "EC Grant Agreement nr.: FP7/295261, EC Grant Agreement nr.: FP7/318490, EC Grant Agreement nr.: FP7/2007-2013, EWI-26155, Markov Decision Processes, Confluence reduction, Statistical Model Checking, Partial order reduction, METIS-314922, IR-98145, Simulation",
    author = "Arnd Hartmanns and Mark Timmer",
    note = "eemcs-eprint-26155",
    year = "2015",
    month = "8",
    doi = "10.1007/s10009-014-0349-7",
    language = "English",
    volume = "17",
    pages = "429--456",
    journal = "International journal on software tools for technology transfer",
    issn = "1433-2779",
    publisher = "Springer",
    number = "4",

    }

    Sound statistical model checking for MDP using partial order and confluence reduction. / Hartmanns, Arnd; Timmer, Mark.

    In: International journal on software tools for technology transfer, Vol. 17, No. 4, 08.2015, p. 429-456.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Sound statistical model checking for MDP using partial order and confluence reduction

    AU - Hartmanns, Arnd

    AU - Timmer, Mark

    N1 - eemcs-eprint-26155

    PY - 2015/8

    Y1 - 2015/8

    N2 - Statistical model checking (SMC) is an analysis method that circumvents the state space explosion problem in model-based verification by combining probabilistic simulation with statistical methods that provide clear error bounds. As a simulation-based technique, it can in general only provide sound results if the underlying model is a stochastic process. In verification, however, models are very often variations of nondeterministic transition systems. In classical exhaustive model checking, partial order reduction and confluence reduction allow the removal of spurious nondeterministic choices. In this paper, we show that both can be adapted to detect and discard such choices on-the-fly during simulation, thus extending the applicability of SMC to a subclass of Markov decision processes. We prove their correctness in a uniform way and study their effectiveness and efficiency using an implementation in the modes simulator for the Modest modelling language. The examples we use highlight the different strengths and limitations of the two approaches. We find that runtime may be affected by unnecessary recomputations, and thus also investigate the feasibility of caching results to speed up simulation at the cost of increased memory usage.

    AB - Statistical model checking (SMC) is an analysis method that circumvents the state space explosion problem in model-based verification by combining probabilistic simulation with statistical methods that provide clear error bounds. As a simulation-based technique, it can in general only provide sound results if the underlying model is a stochastic process. In verification, however, models are very often variations of nondeterministic transition systems. In classical exhaustive model checking, partial order reduction and confluence reduction allow the removal of spurious nondeterministic choices. In this paper, we show that both can be adapted to detect and discard such choices on-the-fly during simulation, thus extending the applicability of SMC to a subclass of Markov decision processes. We prove their correctness in a uniform way and study their effectiveness and efficiency using an implementation in the modes simulator for the Modest modelling language. The examples we use highlight the different strengths and limitations of the two approaches. We find that runtime may be affected by unnecessary recomputations, and thus also investigate the feasibility of caching results to speed up simulation at the cost of increased memory usage.

    KW - EC Grant Agreement nr.: FP7/295261

    KW - EC Grant Agreement nr.: FP7/318490

    KW - EC Grant Agreement nr.: FP7/2007-2013

    KW - EWI-26155

    KW - Markov Decision Processes

    KW - Confluence reduction

    KW - Statistical Model Checking

    KW - Partial order reduction

    KW - METIS-314922

    KW - IR-98145

    KW - Simulation

    U2 - 10.1007/s10009-014-0349-7

    DO - 10.1007/s10009-014-0349-7

    M3 - Article

    VL - 17

    SP - 429

    EP - 456

    JO - International journal on software tools for technology transfer

    JF - International journal on software tools for technology transfer

    SN - 1433-2779

    IS - 4

    ER -