Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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
Contributor : Cyrille Jegourel Connect in order to contact the contributor
Submitted on : Wednesday, November 26, 2014 - 5:27:42 PM
Last modification on : Thursday, January 20, 2022 - 5:33:21 PM
Long-term archiving on: : Friday, February 27, 2015 - 12:45:52 PM


Files produced by the author(s)



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⟩



Record views


Files downloads