Benchmark

A verification benchmark is a model together with a list of properties to be checked on the model.
forum

Visible to the public 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.

forum

Visible to the public CNLN: Quadcopter (Crazyflie)

From:
da Cunha, A.E.C.: Benchmark: Quadrotor attitude control.
Dreossi T., Dang T., Piazza C.: Reachability Computation for Polynomial Dynamical Systems.

Dynamics:
pn' = u*(2*pow(q0v,2) + 2*pow(q1v,2) - 1) - v*(2*q0v*q3v - 2*q1v*q2v ) + w*(2*q0v*q2v + 2*q1v*q3v )
pe' = v*(2*pow(q0v,2) + 2*pow(q2v,2) - 1) + u*(2*q0v*q3v + 2*q1v*q2v ) - w*(2*q0v*q1v - 2*q2v*q3v )
h' = w*(2*pow(q0v,2) + 2*pow(q3v,2) - 1) - u*(2*q0v*q2v - 2*q1v*q3v ) + v*(2*q0v*q1v + 2*q2v*q3v )

forum

Visible to the public CNLN: Phosphorelay

From:
Klipp, E., Herwig, R., Kowald, A., Wierling, C., Lehrach, H.: Systems biology in practice: concepts, implementation and application.
Dreossi T., Dang T., Piazza C.: Reachability Computation for Polynomial Dynamical Systems.

Dynamics:
x1' = -0.4*x1 + 5*x3*x4
x2' = 0.4*x1 - x2
x3' = x2-5*x3*x4
x4' = 5*x5*x6 - 5*x3*x4
x5' = -5*x5*x6 + 5*x3*x4
x6' = 0.5*x7 - 5*x5*x6
x7' = -0.5*x7 + 5*x5*x6

Parameters:
Delta = 0.01 (for Euclid discretization)

forum

Visible to the public CNLN: Generalized Lotka-Volterra

From:
Wildenberg,J.,Vano,J.,Sprott,J.:Complex spatiotemporal dynamics in Lotka-Volterra ring systems.
Dreossi T., Dang T., Piazza C.: Reachability Computation for Polynomial Dynamical Systems.

Dynamics:
x1' = x1*(1 - (x1 + alpha*x2 + beta*x5))
x2' = x2*(1 - (x2 + alpha*x3 + beta*x1))
x3' = x3*(1 - (x3 + alpha*x4 + beta*x2))
x4' = x4*(1 - (x4 + alpha*x5 + beta*x3))
x5' = x5*(1 - (x5 + alpha*x1 + beta*x4))

Parameters:
alpha = 0.85
beta = 0.50
Delta = 0.01 (for Euclid discretization)

forum

Visible to the public CNLN: SIR Epidemic Model

From:
Kermack, W.O., McKendrick, A.G.: A contribution to the mathematical theory of epidemics.
Dreossi T., Dang T., Piazza C.: Reachability Computation for Polynomial Dynamical Systems.

Dynamics:
s' = -beta*s*i/N
i' = beta*s*i/N - gamma*r
r' = gamma*i

Parameters:
beta = 0.34
gamma = 0.05
N = 1.0
Delta = 0.1 (for Euclid discretization)

Initial set:
s(0) \in [0.79, 0.80]
i(0) \in [0.19, 0.20]
r(0) \in [0.00, 0.00]

forum

Visible to the public CNLN: Rossler attractor

From:
Rossler, O.E.: An equation for continuous chaos.
Dreossi T., Dang T., Piazza C.: Reachability Computation for Polynomial Dynamical Systems.

Dynamics:
x' = -y-z
y' = x + a*y
z' = b + z(x-c)

Parameters:
a = 0.1
b = 0.1
c = 14.0
Delta = 0.025 (for Euclid discretization)

Initial set:
x(0) \in [0.09, 0.10]
y(0) \in [4.99, 5.00]
z(0) \in [0.09, 0.10]

file

Visible to the public FuelControl_M1.zip

file

Visible to the public FalsificationProblems.pdf

file

Visible to the public Embcontroller_M2.zip

forum

Visible to the public Two falsification problems

Hi All,

We present two falsification problems.

See the PDF attached with a description of the two problems, along with compressed files for the two models.

Cheers,

Bardh Hoxha

Computer Science

Cyber-Physical Systems Lab

Arizona State University

http://www.public.asu.edu/~bhoxha/