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

Arnd Hartmanns, Mark Timmer

Research output: Contribution to journalArticle

  • 5 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.
LanguageUndefined
Pages429-456
Number of pages28
JournalInternational journal on software tools for technology transfer
Volume17
Issue number4
DOIs
StatePublished - Aug 2015

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 = "Undefined",
volume = "17",
pages = "429--456",
journal = "International journal on software tools for technology transfer",
issn = "1433-2779",
publisher = "Springer Berlin Heidelberg",
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 journalArticle

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

T2 - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

SN - 1433-2779

IS - 4

ER -