Probabilistic hybrid systems verification via SMT and Monte Carlo techniques

  1. Lookup NU author(s)
  2. Fedor Shmarov
  3. Dr Paolo Zuliani
Author(s)Shmarov F, Zuliani P
Publication type Conference Proceedings (inc. Abstract)
Conference Name12th Haifa Verification Conference (HVC 2016)
Conference LocationHaifa, Israel
Year of Conference2016
Source Publication Date
Series TitleLecture Notes in Computer Science (LNCS)
Full text is available for this publication:
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.
ActionsLink to this publication
Library holdingsSearch Newcastle University Library for this item