Importance Splitting for Statistical Model Checking Rare Properties

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 probabilistic model checking by estimating the probability of a property from simulations. Rare properties are often important, but pose a challenge for simulation-based approaches: the relative error of the estimate is unbounded. A key objective for statistical model checking rare events is thus to reduce the variance of the estimator. Importance splitting achieves this by estimating a sequence of conditional probabilities, whose product is the required result. To apply this idea to model checking it is necessary to define a score function based on logical properties, and a set of levels that delimit the conditional probabilities. In this paper we motivate the use of importance splitting for statistical model checking and describe the necessary and desirable properties of score functions and levels. We illustrate how a score function may be derived from a property and give two importance splitting algorithms: one that uses fixed levels and one that discovers optimal levels adaptively.
Type de document :
Communication dans un congrès
Computer Aided Verification, Jul 2013, Saint-Pétersbourg, Russia. pp.576 - 591, 2013, 〈10.1007/978-3-642-39799-8_38〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01087826
Contributeur : Cyrille Jegourel <>
Soumis le : mercredi 26 novembre 2014 - 17:24:12
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : vendredi 14 avril 2017 - 19:53:18

Fichier

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

Identifiants

Citation

Cyrille Jegourel, Axel Legay, Sean Sedwards. Importance Splitting for Statistical Model Checking Rare Properties. Computer Aided Verification, Jul 2013, Saint-Pétersbourg, Russia. pp.576 - 591, 2013, 〈10.1007/978-3-642-39799-8_38〉. 〈hal-01087826〉

Partager

Métriques

Consultations de la notice

349

Téléchargements de fichiers

233