Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking

Cyrille Jégourel 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 exponential growth of states associated with probabilistic model checking by estimating prop-erties from multiple executions of a system and by giving results within confidence bounds. Rare properties are often very important but pose a particular challenge for simulation-based approaches, hence a key ob-jective under these circumstances is to reduce the number and length of simulations necessary to produce a given level of confidence. Impor-tance sampling is a well-established technique that achieves this, however to maintain the advantages of statistical model checking it is necessary to find good importance sampling distributions without considering the entire state space. Motivated by the above, we present a simple algorithm that uses the notion of cross-entropy to find the optimal parameters for an importance sampling distribution. In contrast to previous work, our algorithm uses a low dimensional vector of parameters to define this distribution and thus avoids the often intractable explicit representation of a transition matrix. We show that our parametrisation leads to a unique optimum and can produce many orders of magnitude improvement in simulation efficiency. We demonstrate the efficacy of our methodology by applying it to models from reliability engineering and biochemistry.
Type de document :
Communication dans un congrès
Computer Aided Verification, Jul 2012, Berkeley, United States. pp.327 - 342, 2012, 〈10.1007/978-3-642-31424-7_26〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01087341
Contributeur : Cyrille Jegourel <>
Soumis le : mardi 25 novembre 2014 - 19:34:12
Dernière modification le : mercredi 11 avril 2018 - 02:00:21
Document(s) archivé(s) le : jeudi 26 février 2015 - 12:30:14

Fichier

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

Identifiants

Citation

Cyrille Jégourel, Axel Legay, Sean Sedwards. Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking. Computer Aided Verification, Jul 2012, Berkeley, United States. pp.327 - 342, 2012, 〈10.1007/978-3-642-31424-7_26〉. 〈hal-01087341〉

Partager

Métriques

Consultations de la notice

427

Téléchargements de fichiers

78