SReach: A Bounded Model Checker for Stochastic Hybrid Systems

Understand

In this paper we describe a new tool, SReach, which solves probabilistic bounded reachability problems for two classes of stochastic hybrid systems.

• The first one is (nonlinear) hybrid automata with parametric uncertainty.
• The second one is probabilistic hybrid automata with additional randomness for both transition probabilities and variable resets.
• Standard approaches to reachability problems for linear hybrid systems require numerical solutions for large optimization problems, and become infeasible for systems involving both nonlinear dynamics over the reals and stochasticity.