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
Editor(s)
Publication type Conference Proceedings (inc. Abstract)
Conference Name12th Haifa Verification Conference (HVC 2016)
Conference LocationHaifa, Israel
Year of Conference2016
Source Publication Date
Volume10028
Pages
Series TitleLecture Notes in Computer Science (LNCS)
ISBN9783319490519
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.
PublisherSpringer
URLhttps://doi.org/10.1007/978-3-319-49052-6_10
DOI10.1007/978-3-319-49052-6_10
ActionsLink to this publication
Library holdingsSearch Newcastle University Library for this item
Share