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

  • 3 Citations

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 languageUndefined
Pages (from-to)429-456
Number of pages28
JournalInternational journal on software tools for technology transfer
Volume17
Issue number4
DOIs
StatePublished - Aug 2015

Fingerprint

Model checking
Random processes
Explosions
Statistical methods
Simulators
Removal
Modeling languages

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

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

Vol. 17, No. 4, 08.2015, p. 429-456.

Research output: Scientific - peer-reviewArticle

@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",
volume = "17",
pages = "429--456",
number = "4",

}

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

Vol. 17, No. 4, 08.2015, p. 429-456.

Research output: Scientific - peer-reviewArticle

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

IS - 4

ER -