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
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: 12th Haifa Verification Conference (HVC 2016)
Year of Conference: 2016
Print publication date: 01/11/2016
Online publication date: 01/11/2016
Acceptance date: 05/09/2016
Date deposited: 16/09/2016
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science (LNCS)