Importance Sampling for Model Checking of Continuous Time Markov Chains

Benoît Barbot 1, 2 Serge Haddad 2, 1 Claudine Picaronny 3
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
3 ENS Cachan - École normale supérieure - Cachan
Abstract : Model checking real time properties on probabilistic systems requires computing transient probabilities on continuous time Markov chains. Beyond numerical analysis ability, a probabilistic framing can only be obtained using simulation. This statistical approach fails when directly applied to the estimation of very small probabilities. Here combining the uniformization technique and extending our previous results, we design a method which applies to continuous time Markov chains and formulas of a timed temporal logic. The corresponding algorithm has been implemented in our tool cosmos. We present experimentations on a relevant system, with drastic time reductions with respect to standard statistical model checking.
Type de document :
Communication dans un congrès
Dini, Petre and Lorenz, Pascal. Proceedings of the 4th International Conference on Advances in System Simulation (SIMUL'12), 2012, Lisbon, Portugal. XPS, pp.30-35, 2012
Liste complète des métadonnées
https://hal.inria.fr/hal-00776563
Contributeur : Benedikt Bollig <>
Soumis le : mardi 15 janvier 2013 - 17:05:33
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

  • HAL Id : hal-00776563, version 1

Collections

INRIA | ENS-CACHAN

Citation

Benoît Barbot, Serge Haddad, Claudine Picaronny. Importance Sampling for Model Checking of Continuous Time Markov Chains. Dini, Petre and Lorenz, Pascal. Proceedings of the 4th International Conference on Advances in System Simulation (SIMUL'12), 2012, Lisbon, Portugal. XPS, pp.30-35, 2012. 〈hal-00776563〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

220

Contact


archive-ouverte@inria.fr