The navigation benchmark [1] deals with an autonomous vehicle moves on the plane.
Dynamics
Mode 0
$$\left \{ \begin{array}{l} \dot x = v_x \\ \dot y = v_y \\ \dot v_x = -1.2 v_x+0.1 v_y-0.1 \\ \dot v_y = 0.1 v_x-1.2 v_y + 1.2 \end{array} \right.$$
invariant
$$(x \leq 1 \| v_x \leq 0)~ \&\& ~(y \leq 1 \| v_y \leq 0)$$
Mode 1
$$\left \{ \begin{array}{l} \dot x = v_x \\ \dot y = v_y \\ \dot v_x = -1.2 v_x+0.1 v_y-4.8 \\ \dot v_y = 0.1 v_x-1.2 v_y + 0.4 \end{array} \right.$$
invariant
$$(x \geq 1 \| v_x \leq 0) ~\&\& ~(y \leq 1 \| v_y \leq 0)$$
Mode 2
$$\left \{ \begin{array}{l} \dot x = v_x \\ \dot y = v_y \\ \dot v_x = -1.2 v_x+0.1 v_y+2.4 \\ \dot v_y = 0.1 v_x-1.2 v_y – 0.2 \end{array} \right.$$
invariant
$$(x \leq 1 \| v_x \leq 0) ~\&\& ~(y \geq 1 \| v_y \geq 0)$$
Mode 3
$$\left \{ \begin{array}{l} \dot x = v_x \\ \dot y = v_y \\ \dot v_x = -1.2 v_x+0.1 v_y + 3.9 \\ \dot v_y = 0.1 v_x-1.2 v_y -3.9 \end{array} \right.$$
invariant
$$(x \geq 1 \| v_x \geq 0) ~\&\&~ (y \geq 1 \| v_y \geq 0)$$
Properties
Please see details in the attached file
Reachtube generated by C2E2
Safe reachtube
Unsafe reachtube
Link to the example file: navSafe.hyxml navUnsafe.hyxml
references:
[1] Fehnker, Ansgar, and Franjo Ivančić. “Benchmarks for hybrid systems verification.” In Hybrid Systems: Computation and Control, pp. 326-341. Springer Berlin Heidelberg, 2004.