On-the-fly confluence detection for statistical model checking

Arnd Hartmanns, Arnd Hartmanns, Mark Timmer

  • 11 Citations

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 languageUndefined
Title of host publicationProceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)
Place of PublicationTrieste
PublisherUniversity of Trieste
Pages19
Number of pages4
ISBN (Print)not assigned
StatePublished - Mar 2013

Publication series

Name
PublisherUniversity of Trieste

Fingerprint

Model checking
Random processes
Explosions
Statistical methods
Simulators

Keywords

  • EWI-23226
  • EC Grant Agreement nr.: FP7/295261
  • IR-85420
  • EC Grant Agreement nr.: FP7/2007-2013
  • METIS-296380
  • EC Grant Agreement nr.: FP7/318490

Cite this

Hartmanns, A., 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.

Hartmanns, Arnd; Hartmanns, Arnd; Timmer, Mark / On-the-fly confluence detection for statistical model checking.

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

Research output: Scientific › Conference contribution

@inbook{6d5f09f2a0294ccda7bb77056867b6b9,
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 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.",
keywords = "EWI-23226, EC Grant Agreement nr.: FP7/295261, IR-85420, EC Grant Agreement nr.: FP7/2007-2013, METIS-296380, EC Grant Agreement nr.: FP7/318490",
author = "Arnd Hartmanns and Arnd Hartmanns and Mark Timmer",
note = "eemcs-eprint-23226",
year = "2013",
month = "3",
isbn = "not assigned",
publisher = "University of Trieste",
pages = "19",
booktitle = "Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)",

}

Hartmanns, A, 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). University of Trieste, Trieste, pp. 19.

On-the-fly confluence detection for statistical model checking. / Hartmanns, Arnd; Hartmanns, Arnd; Timmer, Mark.

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

Research output: Scientific › Conference contribution

TY - CHAP

T1 - On-the-fly confluence detection for statistical model checking

AU - Hartmanns,Arnd

AU - Hartmanns,Arnd

AU - Timmer,Mark

N1 - eemcs-eprint-23226

PY - 2013/3

Y1 - 2013/3

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

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

KW - EWI-23226

KW - EC Grant Agreement nr.: FP7/295261

KW - IR-85420

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - METIS-296380

KW - EC Grant Agreement nr.: FP7/318490

M3 - Conference contribution

SN - not assigned

SP - 19

BT - Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)

PB - University of Trieste

ER -

Hartmanns A, Hartmanns A, Timmer M. 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). Trieste: University of Trieste. 2013. p. 19.

Access to Document