Home // SIMUL 2012, The Fourth International Conference on Advances in System Simulation // View article

Importance Sampling for Model Checking of Continuous Time Markov Chains

Authors:
Benoit Barbot
Serge Haddad
Claudine Picaronny

Keywords: statistical model checking; rare events; importance sampling; coupling; uniformization

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. Our method produces a reliable confidence interval with respect to classical statistical model checking on rare events.

Pages: 30 to 35

Copyright: Copyright (c) IARIA, 2012

Publication date: November 18, 2012

Published in: conference

ISSN: 2308-4537

ISBN: 978-1-61208-234-9

Location: Lisbon, Portugal

Dates: from November 18, 2012 to November 23, 2012