CNLN example (7-dimensional)

M. T. Laub and W. F. Loomis. A molecular network that produces spontaneous oscillations in excitable cells of dictyostelium. Molecular Biology of the Cell, 9:3521-3532, 1998.

R. Testylier and T. Dang. Nltoolbox: A library for reachability computation of nonlinear dynamical systems. In Proc. of ATVA'13, volume 8172 of LNCS, pages 469-473. Springer, 2013.

x1' = 1.4 * x3 - 0.9 * x1
x2' = 2.5 * x5 - 1.5 * x2
x3' = 0.6 * x7 - 0.8 * x3 * x2
x4' = 2 - 1.3 * x4 * x3
x5' = 0.7 * x1 - x4 * x5
x6' = 0.3 * x1 - 3.1 * x6
x7' = 1.8 * x6 - 1.5 * x7 * x2

Time horizon [0,20]

Initial set (easy version):

x1 in [1.1,1.3]
x2 in [0.95,1.15]
x3 in [1.4,1.6]
x4 in [2.3,2.5]
x5 in [0.9,1.1]
x6 in [0,0.2]
x7 in [0.35,0.55]

Initial set (hard version)

x1 in [1,1.4]
x2 in [0.85,1.25]
x3 in [1.3,1.7]
x4 in [2.2,2.6]
x5 in [0.8,1.2]
x6 in [-0.1,0.3]
x7 in [0.25,0.65]

Unsafe set: Any set that is close to the reachable set over the time interval [10,20].