Rare-event verification for stochastic hybrid systems

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

Abstract

In this paper we address the problem of verifying in stochastic hybrid systems temporal logic properties whose probability of being true is very small --- rare events. It is well known that sampling-based (Monte Carlo) techniques, such as statistical model checking, do not perform well for estimating rare-event probabilities. The problem is that the sample size required for good accuracy grows too large as the event probability tends to zero. However, several techniques have been developed to address this problem. We focus on importance sampling techniques, which bias the original system to compute highly accurate and efficient estimates. The main difficulty in importance sampling is to devise a good biasing density, that is, a density yielding a low-variance estimator. In this paper, we show how to use the cross-entropy method for generating approximately optimal biasing densities for statistical model checking. We apply the method with importance sampling and statistical model checking for estimating rare-event probabilities in stochastic hybrid systems coded as Stateflow/Simulink diagrams.

Details

Original languageEnglish
Title of host publicationHSCC '12: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control
EditorsThao Dang, Ian M. Mitchell
PublisherAssociation for Computing Machinery (ACM), New York
Pages217-226
Number of pages10
ISBN (print)978-1-4503-1220-2
Publication statusPublished - 2012
Peer-reviewedYes

Conference

Title15th International Conference on Hybrid Systems
SubtitleComputation and Control
Abbreviated titleHSCC 2012
Conference number
Duration17 - 19 April 2012
Degree of recognitionInternational event
Location
CityBeijing
CountryChina

External IDs

Scopus 84860630791
ORCID /0000-0002-5321-9343/work/142236746

Keywords

Keywords

  • Probabilistic model checking, hybrid systems, rare events, statistical model checking, stochastic systems