### Abstract

Statistical model checking 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 only provide sound results if the underlying model is a stochastic process. In verification, however, models are usually variations of nondeterministic transition systems. The notion of confluence allows the reduction of such transition systems in classical model checking by removing spurious nondeterministic choices. In this presentation, we show that confluence can be adapted to detect and discard such choices on-the-fly during simulation, thus extending the applicability of statistical model checking to a subclass of Markov decision processes. In contrast to previous approaches that use partial order reduction, the confluence-based technique can handle additional kinds of nondeterminism. In particular, it is not restricted to interleavings. We evaluate our approach, which is implemented as part of the modes simulator for the MODEST modelling language, on a set of examples that highlight its strengths and limitations and show the improvements compared to the partial order-based method.

Original language | English |
---|---|

Title of host publication | Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013) |

Place of Publication | Trieste |

Publisher | University of Trieste |

Pages | 19 |

Number of pages | 4 |

Publication status | Published - Mar 2013 |

Event | 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013 - Rome, Italy Duration: 23 Mar 2013 → 24 Mar 2013 Conference number: 11 http://eptcs.web.cse.unsw.edu.au/content.cgi?QAPL2013 |

### Publication series

Name | |
---|---|

Publisher | University of Trieste |

### Workshop

Workshop | 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013 |
---|---|

Abbreviated title | QAPL 2013 |

Country | Italy |

City | Rome |

Period | 23/03/13 → 24/03/13 |

Internet address |

### Keywords

- EC Grant Agreement nr.: FP7/295261
- EC Grant Agreement nr.: FP7/2007-2013
- EC Grant Agreement nr.: FP7/318490

## Fingerprint Dive into the research topics of 'On-the-fly confluence detection for statistical model checking'. Together they form a unique fingerprint.

## Cite this

Hartmanns, A., & Timmer, M. (2013). On-the-fly confluence detection for statistical model checking. In

*Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)*(pp. 19). Trieste: University of Trieste.