Skip to Main content Skip to Navigation
Conference papers

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], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/hal-00776563
Contributor : Benedikt Bollig <>
Submitted on : Tuesday, January 15, 2013 - 5:05:33 PM
Last modification on : Tuesday, March 30, 2021 - 12:12:04 PM

Identifiers

  • HAL Id : hal-00776563, version 1

Collections

CNRS | INRIA | ENS-CACHAN | ENS-PARIS-SACLAY

Citation

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

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

251

 

Contact                    Legal Notice                    Personal Data