### Abstract

Original language | Undefined |
---|---|

Pages (from-to) | 429-456 |

Number of pages | 28 |

Journal | International journal on software tools for technology transfer |

Volume | 17 |

Issue number | 4 |

DOIs | |

State | Published - Aug 2015 |

### Fingerprint

### 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

}

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

Research output: Scientific - peer-review › Article

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 -