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

Arnd Hartmanns, Mark Timmer

    Research output: Contribution to journalArticleAcademicpeer-review

    9 Citations (Scopus)
    91 Downloads (Pure)


    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
    Issue number4
    Publication statusPublished - Aug 2015


    • 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


    Dive into the research topics of 'Sound statistical model checking for MDP using partial order and confluence reduction'. Together they form a unique fingerprint.

    Cite this