Command-based importance sampling for statistical model checking

Cyrille Jegourel 1 Axel Legay 2 Sean Sedwards 2
2 TAMIS - Threat Analysis and Mitigation for Information Security
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Statistical model checking avoids the exponential growth of states of numerical model checking, but rare properties are costly to verify. Importance sampling can reduce the cost if good importance sampling distributions can be found efficiently. Our approach uses a tractable cross-entropy minimisation algorithm to find an optimal parametrised importance sampling distribution. In contrast to previous work, our algorithm uses a naturally defined low dimensional vector to specify the distribution, thus avoiding an explicit representation of a transition matrix. Our parametrisation leads to a unique optimum and is shown to produce many orders of magnitude improvement in efficiency on various models. In this work we link the existence of optimal importance sampling distributions to logical properties and show how our parametrisation affects this link. We also motivate and present simple algorithms to create the initial distribution necessary for cross-entropy minimisation. Finally, we discuss the open challenge of defining error bounds with importance sampling and describe how our optimal parametrised distributions may be used to infer qualitative confidence.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2016, 649, pp.1 - 24
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01387299
Contributeur : Sean Sedwards <>
Soumis le : mardi 25 octobre 2016 - 13:38:18
Dernière modification le : mardi 16 janvier 2018 - 15:54:26

Fichier

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

Identifiants

  • HAL Id : hal-01387299, version 1

Citation

Cyrille Jegourel, Axel Legay, Sean Sedwards. Command-based importance sampling for statistical model checking. Theoretical Computer Science, Elsevier, 2016, 649, pp.1 - 24. 〈hal-01387299〉

Partager

Métriques

Consultations de la notice

248

Téléchargements de fichiers

80