Skip to Main content Skip to Navigation
Conference papers

An Effective Heuristic for Adaptive Importance Splitting in Statistical Model Checking

Cyrille Jegourel 1 Axel Legay 1 Sean Sedwards 1
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Statistical model checking avoids the intractable growth of states associated with numerical model checking by estimating the prob-ability of a property from simulations. Rare properties pose a challenge because the relative error of the estimate is unbounded. In [13] we de-scribe how importance splitting may be used with SMC to overcome this problem. The basic idea is to decompose a logical property into nested properties whose probabilities are easier to estimate. To improve perfor-mance it is desirable to decompose the property into many equi-probable levels, but logical decomposition alone may be too coarse. In this article we make use of the notion of a score function to improve the granularity of a logical property. We show that such a score function may take advantage of heuristics, so long as it also rigorously respects certain properties. To demonstrate our importance splitting approach we present an optimal adaptive importance splitting algorithm and an heuristic score function. We give experimental results that demonstrate a significant improvement in performance over alternative approaches.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01087828
Contributor : Cyrille Jegourel <>
Submitted on : Wednesday, November 26, 2014 - 5:27:42 PM
Last modification on : Tuesday, June 15, 2021 - 4:27:13 PM
Long-term archiving on: : Friday, February 27, 2015 - 12:45:52 PM

File

ISOLA2014_v3.pdf
Files produced by the author(s)

Identifiers

Citation

Cyrille Jegourel, Axel Legay, Sean Sedwards. An Effective Heuristic for Adaptive Importance Splitting in Statistical Model Checking. International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2014, Corfou, Greece. pp.143 - 159, ⟨10.1007/978-3-662-45231-8_11⟩. ⟨hal-01087828⟩

Share

Metrics

Record views

410

Files downloads

319