Benchmark: Bouncing Ball

Model file v0.1, 2013-11-12
Goran Frehse

The bouncing ball is an academic benchmark frequently used for illustration and testing of algorithms.
Despite being extremely simple, it exhibits a several key phenomena that are typical for hybrid systems and reachability.

This model includes a model of the bouncing ball for use with the tool SpaceEx, available at http://spaceex.imag.fr/:
- bball.xml is the model file in SX format
- bball.cfg is the configuration file for SpaceEx, defining typical initial conditions and analysis parameters for reachability over an infinite time horizon.

Reachability properties to be checked:
1. boundedness of the reachable set: Approximating the reachable set with low accuracy can lead do a rapidly diverging, unbounded set. The difficulty increases as c goes to 1.
2. convergence: Verify that the velocity decreases from one jump to the next. Similar for the max. height between two consecutive jumps.

Several properties can serve as quality indicators for reachability algorithms
and tools:
1. accuracy: Since analytic solutions are available, the accuracy of the reach set approximation can be evaluated. For bounded model checking this can be the max. height after the nth jump.
2. termination of reachability algorithms: Check whether a cover of the reachable set can be computed over an innite time horizon. The number of jumps of the ball until termination combined with the accuracy of the final result are indicators for the convergence/accuracy trade-off of the algorithm.
3. Zenoness: Adding a clock to the system, check whether time can diverge.