Rare-event verification for stochastic hybrid systems

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
TitelHSCC '12: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control
Redakteure/-innenThao Dang, Ian M. Mitchell
Herausgeber (Verlag)Association for Computing Machinery (ACM), New York
Seiten217-226
Seitenumfang10
ISBN (Print)978-1-4503-1220-2
PublikationsstatusVeröffentlicht - 2012
Peer-Review-StatusJa

Konferenz

Titel15th International Conference on Hybrid Systems
UntertitelComputation and Control
KurztitelHSCC 2012
Veranstaltungsnummer
Dauer17 - 19 April 2012
BekanntheitsgradInternationale Veranstaltung
Ort
StadtBeijing
LandChina

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