On-the-fly confluence detection for statistical model checking

Arnd Hartmanns, Mark Timmer

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    12 Citations (Scopus)
    29 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 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 languageEnglish
    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
    Publication statusPublished - Mar 2013
    Event11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013 - Rome, Italy
    Duration: 23 Mar 201324 Mar 2013
    Conference number: 11
    http://eptcs.web.cse.unsw.edu.au/content.cgi?QAPL2013

    Publication series

    Name
    PublisherUniversity of Trieste

    Workshop

    Workshop11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013
    Abbreviated titleQAPL 2013
    CountryItaly
    CityRome
    Period23/03/1324/03/13
    Internet address

    Fingerprint

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

    Keywords

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

    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.
    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. pp. 19
    @inproceedings{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 = "EC Grant Agreement nr.: FP7/295261, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490",
    author = "Arnd Hartmanns and Mark Timmer",
    year = "2013",
    month = "3",
    language = "English",
    publisher = "University of Trieste",
    pages = "19",
    booktitle = "Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)",

    }

    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, 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013, Rome, Italy, 23/03/13.

    On-the-fly confluence detection for statistical model checking. / 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: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    TY - GEN

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

    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 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 - EC Grant Agreement nr.: FP7/295261

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

    KW - EC Grant Agreement nr.: FP7/318490

    M3 - Conference contribution

    SP - 19

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

    PB - University of Trieste

    CY - Trieste

    ER -

    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