Browse by author
Lookup NU author(s): Fedor Shmarov, Dr Paolo Zuliani
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License (CC BY-NC 4.0).
We develop numerically rigorous Monte Carlo approaches for computing probabilistic reachability in hybrid systems subject to random and nondeterministic parameters. Instead of standard simulation we use delta-complete SMT procedures, which enable formal reasoning for nonlinear systems up to a user-definable numeric precision. Monte Carlo approaches for probability estimation assume that sampling is possible for the real system at hand. However, when using delta-complete simulation one instead samples from an overapproximation of the real random variable. In this paper, we introduce a Monte Carlo-SMT approach for computing probabilistic reachability confidence intervals that are both statistically and numerically rigorous. We apply our technique to hybrid systems involving nonlinear differential equations.
Author(s): Shmarov F, Zuliani P
Editor(s): Roderick Bloem, Eli Arbel
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: 12th Haifa Verification Conference (HVC 2016)
Year of Conference: 2016
Pages: 152-168
Print publication date: 01/11/2016
Online publication date: 01/11/2016
Acceptance date: 05/09/2016
Date deposited: 16/09/2016
ISSN: 0302-9743
Publisher: Springer
URL: https://doi.org/10.1007/978-3-319-49052-6_10
DOI: 10.1007/978-3-319-49052-6_10
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science (LNCS)
ISBN: 9783319490519
