On-the-Fly Confluence Detection for Statistical Model Checking

Arnd Hartmanns, Mark Timmer

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

21 Downloads (Pure)

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 paper, 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 languageEnglish
Title of host publicationProceedings of the 5th International NASA Formal Methods Symposium (NFM 2013)
EditorsGuillaume Brat, Neha Rungta, Arnaud Venet
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages337-351
Number of pages15
ISBN (Electronic)978-3-642-38088-4
ISBN (Print)978-3-642-38087-7
DOIs
Publication statusPublished - 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume7871
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Model checking
Random processes
Explosions
Statistical methods
Simulators
Acoustic waves
Statistical Models

Cite this

Hartmanns, A., & Timmer, M. (2013). On-the-Fly Confluence Detection for Statistical Model Checking. In G. Brat, N. Rungta, & A. Venet (Eds.), Proceedings of the 5th International NASA Formal Methods Symposium (NFM 2013) (pp. 337-351). (Lecture Notes in Computer Science; Vol. 7871). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-38088-4_23
Hartmanns, Arnd ; Timmer, Mark . / On-the-Fly Confluence Detection for Statistical Model Checking. Proceedings of the 5th International NASA Formal Methods Symposium (NFM 2013). editor / Guillaume Brat ; Neha Rungta ; Arnaud Venet. Berlin, Heidelberg : Springer, 2013. pp. 337-351 (Lecture Notes in Computer Science).
@inbook{169403597cd54e33bfa0ad12a135f7f1,
title = "On-the-Fly Confluence Detection for Statistical Model Checking",
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 paper, 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.",
author = "Arnd Hartmanns and Mark Timmer",
year = "2013",
doi = "10.1007/978-3-642-38088-4_23",
language = "English",
isbn = "978-3-642-38087-7",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "337--351",
editor = "Guillaume Brat and Neha Rungta and Arnaud Venet",
booktitle = "Proceedings of the 5th International NASA Formal Methods Symposium (NFM 2013)",

}

Hartmanns, A & Timmer, M 2013, On-the-Fly Confluence Detection for Statistical Model Checking. in G Brat, N Rungta & A Venet (eds), Proceedings of the 5th International NASA Formal Methods Symposium (NFM 2013). Lecture Notes in Computer Science, vol. 7871, Springer, Berlin, Heidelberg, pp. 337-351. https://doi.org/10.1007/978-3-642-38088-4_23

On-the-Fly Confluence Detection for Statistical Model Checking. / Hartmanns, Arnd ; Timmer, Mark .

Proceedings of the 5th International NASA Formal Methods Symposium (NFM 2013). ed. / Guillaume Brat; Neha Rungta; Arnaud Venet. Berlin, Heidelberg : Springer, 2013. p. 337-351 (Lecture Notes in Computer Science; Vol. 7871).

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

TY - CHAP

T1 - On-the-Fly Confluence Detection for Statistical Model Checking

AU - Hartmanns, Arnd

AU - Timmer, Mark

PY - 2013

Y1 - 2013

N2 - 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 paper, 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.

AB - 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 paper, 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.

U2 - 10.1007/978-3-642-38088-4_23

DO - 10.1007/978-3-642-38088-4_23

M3 - Chapter

SN - 978-3-642-38087-7

T3 - Lecture Notes in Computer Science

SP - 337

EP - 351

BT - Proceedings of the 5th International NASA Formal Methods Symposium (NFM 2013)

A2 - Brat, Guillaume

A2 - Rungta, Neha

A2 - Venet, Arnaud

PB - Springer

CY - Berlin, Heidelberg

ER -

Hartmanns A, Timmer M. On-the-Fly Confluence Detection for Statistical Model Checking. In Brat G, Rungta N, Venet A, editors, Proceedings of the 5th International NASA Formal Methods Symposium (NFM 2013). Berlin, Heidelberg: Springer. 2013. p. 337-351. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-38088-4_23