Tim Gonschorek, Ben Lukas Rabeler, Frank Ortmeier, Dirk Schomburg: On Improving Rare Event Simulation for Probabilistic Safety Analysis. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, S. 15-24, ACM New York, NY, USA ©2017 , 2017, ISBN: 978-1-4503-5093-8.

Abstract

This paper presents a new approach for generating probability distributions for Monte Carlo based stochastic model checking. Stochastic approaches are used for quantitative analysis of safety critical systems if numerical model checking tools get overwhelmed by the complexity of the models and the exploding state space. However, sample based stochastic measures get problems when the estimated event is very unlikely (e.g. 10-6 and below). Therefore, rare event techniques, like importance sampling, increase the likelihood of samples representing model executions which depict the desired rare event, e.g., a path leading into a hazardous state.

The presented approach uses qualitative counter examples to derive appropriate distributions for the sampling, i.e., a distribution that increases the likelihood of the examined rare event and decreases the variance Therefore, we define the sampling distribution such that transitions included in the counter example become more likely. For keeping the variance small, the new distributions is calculated within an optimization problem which minimizes the variance on the counter example paths by calculating new probability distributions for the related transitions. We have evaluated this approach in four different real-world case studies and compare it to other leading stochastic and numeric model checking tools. It turned out that in the case of rare event properties, the proposed approach outperforms other techniques in run time and, slightly more important, in the accuracy of the estimation result.

BibTeX (Download)

@inproceedings{Gonschorek2017,
title = {On Improving Rare Event Simulation for Probabilistic Safety Analysis},
author = {Tim Gonschorek and Ben Lukas Rabeler and Frank Ortmeier and Dirk Schomburg},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GonschorekEtAl_OnImprovingRareEventSimulationForProbabilisticSafetyAnalysis_memocode17.pdfhttps://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/GonschorekEtAl_OnImprovingRareEventSimulationForProbabilisticSafetyAnalysis_memocode17.pdf},
doi = {10.1145/3127041.3127057},
isbn = {978-1-4503-5093-8},
year  = {2017},
date = {2017-09-29},
booktitle = {Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design},
pages = {15-24},
publisher = {ACM New York, NY, USA ©2017 },
series = {Lecture Notes in Computer Science},
abstract = {This paper presents a new approach for generating probability distributions for Monte Carlo based stochastic model checking. Stochastic approaches are used for quantitative analysis of safety critical systems if numerical model checking tools get overwhelmed by the complexity of the models and the exploding state space. However, sample based stochastic measures get problems when the estimated event is very unlikely (e.g. 10-6 and below). Therefore, rare event techniques, like importance sampling, increase the likelihood of samples representing model executions which depict the desired rare event, e.g., a path leading into a hazardous state.

The presented approach uses qualitative counter examples to derive appropriate distributions for the sampling, i.e., a distribution that increases the likelihood of the examined rare event and decreases the variance Therefore, we define the sampling distribution such that transitions included in the counter example become more likely. For keeping the variance small, the new distributions is calculated within an optimization problem which minimizes the variance on the counter example paths by calculating new probability distributions for the related transitions. We have evaluated this approach in four different real-world case studies and compare it to other leading stochastic and numeric model checking tools. It turned out that in the case of rare event properties, the proposed approach outperforms other techniques in run time and, slightly more important, in the accuracy of the estimation result.
},
keywords = {Monte Carlo Simulation, Probabilistic Model Checking},
pubstate = {published},
tppubtype = {inproceedings}
}