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 δ
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.
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: