Rare-event verification for stochastic hybrid systems
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-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 language | English |
---|---|
Title of host publication | HSCC '12: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control |
Editors | Thao Dang, Ian M. Mitchell |
Publisher | Association for Computing Machinery (ACM), New York |
Pages | 217-226 |
Number of pages | 10 |
ISBN (print) | 978-1-4503-1220-2 |
Publication status | Published - 2012 |
Peer-reviewed | Yes |
Conference
Title | 15th International Conference on Hybrid Systems |
---|---|
Subtitle | Computation and Control |
Abbreviated title | HSCC 2012 |
Conference number | |
Duration | 17 - 19 April 2012 |
Degree of recognition | International event |
Location | |
City | Beijing |
Country | China |
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