ProbReach is an application for computing a probabilistic bounded δ-reachability in hybrid systems with continuous random initial parameter. ProbReach obtains an interval of arbitrarily small length ε containing the exact value of the probability that a hybrid system reaches an unsafe region in a finite number of steps. This website displays two graphs visualizing the results computed by ProbReach.

The top graph presents a Borel set B containing the values of the random parameter satisying the bounded δ-reachability property. The graph contains a series of intervals highlighted in different colors.

The bottom graph shows the evolution of the probability interval with respect to CPU time (parallel implementation). ProbReach guarantees that at any point in time the exact probability of reaching the unsafe region is inside the shaded area of the graph.

Choose a precomputed result from the list below: