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.
Type de document :
Communication dans un congrès
International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2014, Corfou, Greece. pp.143 - 159, 2014, 〈10.1007/978-3-662-45231-8_11〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087828
Contributeur : Cyrille Jegourel <>
Soumis le : mercredi 26 novembre 2014 - 17:27:42
Dernière modification le : jeudi 15 novembre 2018 - 11:58:48
Document(s) archivé(s) le : vendredi 27 février 2015 - 12:45:52

Fichier

ISOLA2014_v3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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, 2014, 〈10.1007/978-3-662-45231-8_11〉. 〈hal-01087828〉

Partager

Métriques

Consultations de la notice

344

Téléchargements de fichiers

137