Statistical probabilistic delta-reachability

We develop statistical approaches for computing probabilistic reachability in dynamic models subject to random parameters. To address ordinary differential equations (ODE) we work in the delta-complete framework, which enables formal reasoning up to a user-definable numeric precision. We introduce two statistical approaches for computing confidence intervals for reachability probabilities when using delta-complete simulation procedures. Our approaches compute confidence intervals that are both statistically and numerically rigorous. One approach exploits the Chernoff-Hoeffding bound, while the other employs a sequential Bayesian estimation method. We apply our techniques to several examples of biological system models involving nonlinear ODEs with random parameters.