Coupling and Importance Sampling for Statistical Model Checking

Benoît Barbot 1, 2 Serge Haddad 1, 2 Claudine Picaronny 1
1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Statistical model-checking is an alternative verification technique applied on stochastic systems whose size is beyond numerical analysis ability. Given a model (most often a Markov chain) and a formula, it provides a confidence interval for the probability that the model satisfies the formula. One of the main limitations of the statistical approach is the computation time explosion triggered by the evaluation of very small probabilities. In order to solve this problem we develop a new approach based on importance sampling and coupling. The corresponding algorithms have been implemented in our tool cosmos. We present experimentation on several relevant systems, with estimated time reductions reaching a factor of 10^120.
Type de document :
Communication dans un congrès
Flanagan, Cormac and König, Barbara. Proceedings of the 18th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'12), 2012, Tallinn, Estonia. Springer, 7214, pp.331-346, 2012, 〈10.1007/978-3-642-28756-5_23〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00776795
Contributeur : Benedikt Bollig <>
Soumis le : mercredi 16 janvier 2013 - 11:18:44
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | ENS-CACHAN

Citation

Benoît Barbot, Serge Haddad, Claudine Picaronny. Coupling and Importance Sampling for Statistical Model Checking. Flanagan, Cormac and König, Barbara. Proceedings of the 18th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'12), 2012, Tallinn, Estonia. Springer, 7214, pp.331-346, 2012, 〈10.1007/978-3-642-28756-5_23〉. 〈hal-00776795〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

210

Contact


archive-ouverte@inria.fr