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.