On-the-fly confluence detection for statistical model checking (extended version)

Arnd Hartmanns, Mark Timmer

    Research output: Book/ReportReportAcademic

    15 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
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages18
    Publication statusPublished - Mar 2013

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
    No.TR-CTIT-13-04
    ISSN (Print)1381-3625

    Fingerprint

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

    Keywords

    • Confluence
    • EWI-23163
    • On-the-fly algorithm
    • Statistical Model Checking
    • Markov Decision Processes
    • IR-85175
    • METIS-296354

    Cite this

    Hartmanns, A., & Timmer, M. (2013). On-the-fly confluence detection for statistical model checking (extended version). (CTIT Technical Report Series; No. TR-CTIT-13-04). Enschede: Centre for Telematics and Information Technology (CTIT).
    Hartmanns, Arnd ; Timmer, Mark. / On-the-fly confluence detection for statistical model checking (extended version). Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 18 p. (CTIT Technical Report Series; TR-CTIT-13-04).
    @book{802b0abb5f024e51ba067af665b04f64,
    title = "On-the-fly confluence detection for statistical model checking (extended version)",
    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.",
    keywords = "Confluence, EWI-23163, On-the-fly algorithm, Statistical Model Checking, Markov Decision Processes, IR-85175, METIS-296354",
    author = "Arnd Hartmanns and Mark Timmer",
    year = "2013",
    month = "3",
    language = "English",
    series = "CTIT Technical Report Series",
    publisher = "Centre for Telematics and Information Technology (CTIT)",
    number = "TR-CTIT-13-04",
    address = "Netherlands",

    }

    Hartmanns, A & Timmer, M 2013, On-the-fly confluence detection for statistical model checking (extended version). CTIT Technical Report Series, no. TR-CTIT-13-04, Centre for Telematics and Information Technology (CTIT), Enschede.

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

    Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 18 p. (CTIT Technical Report Series; No. TR-CTIT-13-04).

    Research output: Book/ReportReportAcademic

    TY - BOOK

    T1 - On-the-fly confluence detection for statistical model checking (extended version)

    AU - Hartmanns, Arnd

    AU - Timmer, Mark

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

    KW - Confluence

    KW - EWI-23163

    KW - On-the-fly algorithm

    KW - Statistical Model Checking

    KW - Markov Decision Processes

    KW - IR-85175

    KW - METIS-296354

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - On-the-fly confluence detection for statistical model checking (extended version)

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede

    ER -

    Hartmanns A, Timmer M. On-the-fly confluence detection for statistical model checking (extended version). Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 18 p. (CTIT Technical Report Series; TR-CTIT-13-04).