SMT-Based Reasoning for Uncertain Hybrid Domains

Many practical applications (e.g., plannning for cyber-physical systems) require reasoning about hybrid domains that contain both probabilistic and nondeterministic parametric uncertainty. In general, this is an undecidable problem. We use delta-satisfiability to sidestep undecidability, and we develop an algorithm that computes an enclosure for the range of probability of reaching a goal region in a given number of discrete steps. We utilize SMT techniques that enable reasoning in a safe way, i.e., the computed enclosure is formally guaranteed to contain the reachability probability. We demonstrate the usefulness of our technique on challenging nonlinear hybrid domains.