Bouncing ball


# of variables # of modes # of jumps
2 1 1
Type Continuous dynamics Guards & Invariants Resets
hybrid linear polynomial half-space linear


Flow* flow*_files
SpaceEx spaceEx_files

Model description

The classical bouncing ball example consists of a ball dropped from a predefined height. It hits the ground after a certain time, loses energy and then bounces back into the air and starts to fall again. This physical phenomena can be represented as the following hybrid automaton:


In the discrete state, the motion of the ball, assumed to have a mass of m=1 kg, is governed by the following differential equation: \begin{array}{ll} \dot{x}= & v\\ \dot{v} = & -9.81 \end{array} where x is the ball’s height from the ground, v is the ball’s vertical velocity, and 9.81ms^{-2} is the earth’s gravitational force. The invariant x \geq 0 enforces that the ball always bounces when it reaches the ground. The guard x=0\wedge v\leq0 of the single discrete transition, which models the bouncing, ensures that bouncing happens after falling when reaching the ground. The corresponding reset condition v:=-c \cdot v accounts for the loss of energy due to the ball’s deformation, where c\in\left[0,1\right] is a constant.

Reachability settings

We consider the inital set

  • x \in [10;10.2]
  • v = 0.

We use a time horizon of 40s and set the constant c = 0.75. The set of bad states is the set of all states where v \geq 10.7.


These are the results from the bouncing ball benchmark created with SpaceEx: