Rare-event verification for stochastic hybrid systems
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
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
Originalsprache | Englisch |
---|---|
Titel | HSCC '12: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control |
Redakteure/-innen | Thao Dang, Ian M. Mitchell |
Herausgeber (Verlag) | Association for Computing Machinery (ACM), New York |
Seiten | 217-226 |
Seitenumfang | 10 |
ISBN (Print) | 978-1-4503-1220-2 |
Publikationsstatus | Veröffentlicht - 2012 |
Peer-Review-Status | Ja |
Konferenz
Titel | 15th International Conference on Hybrid Systems |
---|---|
Untertitel | Computation and Control |
Kurztitel | HSCC 2012 |
Veranstaltungsnummer | |
Dauer | 17 - 19 April 2012 |
Bekanntheitsgrad | Internationale Veranstaltung |
Ort | |
Stadt | Beijing |
Land | China |
Externe IDs
Scopus | 84860630791 |
---|---|
ORCID | /0000-0002-5321-9343/work/142236746 |
Schlagworte
Schlagwörter
- Probabilistic model checking, hybrid systems, rare events, statistical model checking, stochastic systems