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 horizontal axis represents the value of the random parameter.

The vertical axis corresponds the values of the probability density function of the random parameter.
The graph contains a series of intervals highlighted in different colors.

Blue color: intervals guaranteed to be in the Borel set B.

Red color: intervals guaranteed to be outside the Borel set.

Transparent: intervals not verified by ProbReach because the desired precision was already achieved.
The bottom graph shows the evolution of the probability interval with respect to CPU time (parallel implementation).

The horizontal axis represents CPU time in seconds.

The vertical axis represents the upper and the lower bounds on the probability.

Blue color highlights the lower bound of the probability interval.

Red color hightlights the upper bound of the probability interval.
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: