Skip to main content
placeholder image

Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters

Journal Article


Abstract


  • Probabilistic model checking is a verification technique that has been the focus of intensive research for over a decade. One

    important issue with probabilistic model checking, which is crucial for its practical significance but is overlooked by the state-of-the-art

    largely, is the potential discrepancy between a stochastic model and the real-world system it represents when the model is built from

    statistical data. In the worst case, a tiny but nontrivial change to some model quantities might lead to misleading or even invalid

    verification results. To address this issue, in this paper, we present a mathematical characterization of the consequences of model

    perturbations on the verification distance. The formal model that we adopt is a parametric variant of discrete-time Markov chains

    equipped with a vector norm to measure the perturbation. Our main technical contributions include a closed-form formulation of

    asymptotic perturbation bounds, and computational methods for two arguably most useful forms of those bounds, namely linear

    bounds and quadratic bounds. We focus on verification of reachability properties but also address automata-based verification of

    omega-regular properties. We present the results of a selection of case studies that demonstrate that asymptotic perturbation bounds

    can accurately estimate maximum variations of verification results induced by model perturbations.

UOW Authors


  •   Guoxin Su
  •   Feng, Yuan (external author)
  •   Chen, Taolue (external author)
  •   Rosenblum, David (external author)

Publication Date


  • 2016

Citation


  • Su, G., Feng, Y., Chen, T. & Rosenblum, D. (2016). Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters. IEEE Transactions on Software Engineering, 42 (7), 623-639.

Ro Metadata Url


  • http://ro.uow.edu.au/eispapers1/158

Number Of Pages


  • 16

Start Page


  • 623

End Page


  • 639

Volume


  • 42

Issue


  • 7

Abstract


  • Probabilistic model checking is a verification technique that has been the focus of intensive research for over a decade. One

    important issue with probabilistic model checking, which is crucial for its practical significance but is overlooked by the state-of-the-art

    largely, is the potential discrepancy between a stochastic model and the real-world system it represents when the model is built from

    statistical data. In the worst case, a tiny but nontrivial change to some model quantities might lead to misleading or even invalid

    verification results. To address this issue, in this paper, we present a mathematical characterization of the consequences of model

    perturbations on the verification distance. The formal model that we adopt is a parametric variant of discrete-time Markov chains

    equipped with a vector norm to measure the perturbation. Our main technical contributions include a closed-form formulation of

    asymptotic perturbation bounds, and computational methods for two arguably most useful forms of those bounds, namely linear

    bounds and quadratic bounds. We focus on verification of reachability properties but also address automata-based verification of

    omega-regular properties. We present the results of a selection of case studies that demonstrate that asymptotic perturbation bounds

    can accurately estimate maximum variations of verification results induced by model perturbations.

UOW Authors


  •   Guoxin Su
  •   Feng, Yuan (external author)
  •   Chen, Taolue (external author)
  •   Rosenblum, David (external author)

Publication Date


  • 2016

Citation


  • Su, G., Feng, Y., Chen, T. & Rosenblum, D. (2016). Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters. IEEE Transactions on Software Engineering, 42 (7), 623-639.

Ro Metadata Url


  • http://ro.uow.edu.au/eispapers1/158

Number Of Pages


  • 16

Start Page


  • 623

End Page


  • 639

Volume


  • 42

Issue


  • 7