Benchmarks for 2024, changes n falsified specifications from 2023

benchmarks/ACC/Specifications.txt

@@ -0,0 +1,21 @@
+Parameters:
+
+a_lead = -2
+T_gap = 1.4
+D_default = 10
+
+Initial states:
+x_lead = x(1) = [90, 110]
+v_lead = x(2) = [32, 32.2]
+γ_lead = x(3) = 0
+x_ego  = x(4) = [10, 11]
+v_ego  = x(5) = [30, 30.2]
+γ_ego  = x(6) = 0
+
+t = 5 seconds
+control period = 0.1 s
+
+Safety Property:
+
+x_lead - x_ego >= D_safe, where D_safe = D_default + T_gap * v_ego;
+

benchmarks/ACC/dynamicsACC.m

@@ -0,0 +1,21 @@
+function [dx]=dynamicsACC(x,a_ego)
+
+mu=0.0001; % friction parameter
+
+% x1 = lead_car position
+% x2 = lead_car velocity
+% x3 = lead_car internal state
+
+% x4 = ego_car position
+% x5 = ego_car velocity
+% x6 = ego_car internal state
+
+% lead car dynamics
+a_lead  = -2; 
+dx(1,1) = x(2);
+dx(2,1) = x(3);
+dx(3,1) = -2 * x(3) + 2 * a_lead - mu*x(2)^2;
+% ego car dyanmics
+dx(4,1) = x(5); 
+dx(5,1) = x(6);
+dx(6,1) = -2 * x(6) + 2 * a_ego - mu*x(5)^2;

benchmarks/Airplane/dynamics.m

@@ -0,0 +1,79 @@
+function [dstates] = dynamics(states,actions)
+% Ex_airplane
+% constants as per the documentation Ix=Iy=Iz = 1; Ixz = 0; m = 1; g= 1;
+% description of the pararameters in these equations can be found here
+% https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf
+
+x = states(1);
+y = states(2);
+z = states(3);
+u = states(4);
+v = states(5);
+w = states(6);
+phi = states(7);
+theta = states(8);
+psi = states(9);
+r = states(10);
+p = states(11);
+q = states(12);
+
+Fx = actions(1);
+Fy = actions(2);
+Fz = actions(3);
+Mx = actions(4);
+My = actions(5);
+Mz = actions(6);
+
+T_psi = [cos(psi), -sin(psi), 0.;
+         sin(psi),  cos(psi), 0.;
+         0.,        0.,       1.];
+
+T_theta = [cos(theta), 0., sin(theta);
+           0.        , 1., 0.        ;
+          -sin(theta), 0., cos(theta)];
+
+T_phi = [1., 0.,        0.      ;
+         0., cos(phi), -sin(phi);
+         0., sin(phi),  cos(phi)];
+
+mat_1 = T_psi * T_theta * T_phi;
+
+mat_2 = [cos(theta), sin(theta) * sin(phi),  sin(theta) * cos(phi);
+         0.,         cos(theta) * cos(phi), -cos(theta) * sin(phi);
+         0.,         sin(phi),               cos(phi)];
+mat_2 = 1 / cos(theta) * mat_2;
+
+a1 = [u; v; w];
+a2 = mat_1 * a1;
+
+dx = a2(1);
+dy = a2(2);
+dz = a2(3);
+
+a3 = [p; q; r];
+a4 = mat_2 * a3;
+
+dphi = a4(1);
+dtheta = a4(2);
+dpsi = a4(3);
+
+du = -sin(theta)            + Fx - q * w + r * v;
+dv =  cos(theta) * sin(phi) + Fy - r * u + p * w;
+dw =  cos(theta) * cos(phi) + Fz - p * v + q * u;
+
+dp = Mx;
+dq = My;
+dr = Mz;
+
+dstates(1,1) = dx;
+dstates(2,1) = dy;
+dstates(3,1) = dz;
+dstates(4,1) = du;
+dstates(5,1) = dv;
+dstates(6,1) = dw;
+dstates(7,1) = dphi;
+dstates(8,1) = dtheta;
+dstates(9,1) = dpsi;
+dstates(10,1) = dr;
+dstates(11,1) = dp;
+dstates(12,1) = dq;

benchmarks/Airplane/specifications.txt

@@ -0,0 +1,23 @@
+Initial states:
+
+x1 = 0
+x2 = 0
+x3 = 0
+x4 = [0.0, 1.0]
+x5 = [0.0, 1.0]
+x6 = [0.0, 1.0]
+x7 = [0.0, 1.0]
+x8 = [0.0, 1.0]
+x9 = [0.0, 1.0]
+x10 = 0
+x11 = 0
+x12 = 0
+
+t = 20 control steps = 2 seconds
+control step = 0.1
+
+Property:
+
+x2 should be in [-1, 1] and x7,x8,x9 should be in [-1.0,1.0] (modified from original specification)
+
+Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf

benchmarks/Attitude Control/Specifications.txt

@@ -0,0 +1,17 @@
+Initial states:
+x1 = [-0.45, -0.44]
+x2 = [-0.55, -0.54]
+x3 = [0.65, 0.66]
+x4 = [-0.75, -0.74]
+x5 = [0.85, 0.86]
+x6 = [-0.65, -0.64]
+
+t = 3 seconds
+control period = 0.1 s
+
+Safety Property:
+We would like to verify whether the system will reach the following unsafe
+set Xu in 3 seconds (30 time steps), where Xu is defined as a 6-dimensional region:
+
+x1 ∈ [-0.2,0],     x2 ∈ [-0.5, -0.4],  x3 ∈ [0, 0.2]
+x4 ∈ [-0.7, -0.6]  x5 ∈ [0.7, 0.8],  x6 ∈ [-0.4, -0.2]

benchmarks/Attitude Control/dynamics.m

@@ -0,0 +1,9 @@
+function dx = dynamics(x,u)
+% Attitude Control, rigid body with 6 states (x) and 3 inputs (u).
+dx(1,1) = 0.25*(u(1)+x(2)*x(3));
+dx(2,1) = 0.5*(u(2)-3*x(1)*x(3));
+dx(3,1) = u(3) + 2*x(1)*x(2);
+dx(4,1) = 0.5*(x(2)*(x(4)^2 + x(5)^2 + x(6)^2 - x(6)) + x(3)*(x(4)^2 + x(5)^2 + x(5) + x(6)^2) + x(1)*(x(4)^2 + x(5)^2 + x(6)^2 + 1));
+dx(5,1) = 0.5*(x(1)*(x(4)^2 + x(5)^2 + x(6)^2 + x(6)) + x(3)*(x(4)^2 - x(4) + x(5)^2 + x(6)^2) + x(2)*(x(4)^2 + x(5)^2 + x(6)^2 + 1));
+dx(6,1) = 0.5*(x(1)*(x(4)^2 + x(5)^2 - x(5) + x(6)^2) + x(2)*(x(4)^2 + x(4) + x(5)^2 + x(6)^2) + x(3)*(x(4)^2 + x(5)^2 + x(6)^2 + 1));
+end

benchmarks/Benchmark10-Unicycle/Specifications.txt

@@ -0,0 +1,17 @@
+Initial states:
+
+x1 = [9.5, 9.55]
+x2 = [-4.5, -4.45]
+x3 = [2.1, 2.11]
+x4 = [1.5, 1.51]
+
+t = 10 seconds
+control period = 0.2 s
+
+Property:
+
+Prove that the system reaches the states:
+x1 = [-0.6, 0.6]
+x2 = [-0.2, 0.2]
+x3 = [-0.06, 0.06]
+x4 = [-0.3, 0.3]

benchmarks/Benchmark10-Unicycle/dynamics10.m

@@ -0,0 +1,24 @@
+function [dx] = dynamics10(x,u)
+% Ex_car_model
+  %vehicleODE Bicycle model of a vehicle with
+  % states
+  %       x(1), x(2): x,y positions
+  %       x(3): Yaw angle (\psi)
+  %       x(4): velocity
+  % control inputs
+  %       u(1): acceleration m/s^2
+  %       u(2): steering angle of front wheel
+  % disturbance input
+  %       w: disturbance with a range (-10^-4,10^4)
+  % Initial state range [9.5, 9.55] × [-4.5, -4.45] × [2.1, 2.11] × [1.5, 1.51]
+%
+% The output of the neural network f(x) needs to be normalized 
+% in order to obtain u(1) and u(2).
+% Namely, u(i) = f(x)(i) - 20 
+%
+dx(1,1) = x(4) * cos(x(3));
+dx(2,1) = x(4) * sin(x(3));
+dx(3,1) = u(2)-20;
+dx(4,1) = u(1)-20;
+
+end

benchmarks/Benchmark9-Tora/Specifications.txt

@@ -0,0 +1,15 @@
+Initial states:
+
+x1 = [0.6, 0.7]
+x2 = [-0.7, -0.6]
+x3 = [-0.4, -0.3]
+x4 = [0.5, 0.6]
+
+t = 20 seconds
+control period = 1s
+
+Property:
+
+The system states always stays within the box x ∈ [-2,2]
+
+

benchmarks/Benchmark9-Tora/dynamics9.m

@@ -0,0 +1,15 @@
+function [dx] = dynamics9(x,u)
+% Ex_tora
+% Initial state range:
+% [0.6, 0.7] � [-0.7, -0.6] � [-0.4, -0.3] � [0.5, 0.6]
+%
+% The output of the neural network f(x) needs to be normalized 
+% in order to obtain u.
+% Namely, u = f(x) - 10 
+%
+dx(1,1) = x(2);
+dx(2,1) = - x(1) + 0.1*sin(x(3));
+dx(3,1) = x(4);
+dx(4,1) = u(1)-10;
+
+end

benchmarks/Docking/dynamics.m

@@ -0,0 +1,17 @@
+function [dstates] = dynamics(states,actions)
+    m = 12;
+    n = 0.001027;
+
+    x = states(1);
+    y = states(2);
+    x_dot = states(3);
+    y_dot = states(4);
+
+    Fx = actions(1);
+    Fy = actions(2);
+
+    dstates(1,1) = x_dot;
+    dstates(2,1) = y_dot;
+    dstates(3,1) = 2*n*y_dot + 3*(n^2)*x + Fx/m;
+    dstates(4,1) = -2*n*x_dot + Fy/m;
+end

benchmarks/Docking/specification.txt

@@ -0,0 +1,10 @@
+Initial States:
+    x1 = [70, 106]
+    x2 = [70, 106]
+    x3 = [-0.28, 0.28]
+    x4 = [-0.28, 0.28]
+
+control step = 1 second
+
+Property:
+    sqrt(x3^2 + x4^2) <= 0.2 + 2*0.001027*sqrt(x1^2 + x2^2)

benchmarks/Double_Pendulum/Specifications.txt

@@ -0,0 +1,20 @@
+Initial states:
+
+x1 = [1.0, 1.3]
+x2 = [1.0, 1.3]
+x3 = [1.0, 1.3]
+x4 = [1.0, 1.3]
+
+t = 20 steps
+
+1) controller double pendulum less robust:
+ - control step = 0.05
+ - Property:
+     - Each of the states should be in [−1.7, 2]
+
+2) controller double pendulum more robust
+ - control step = 0.02
+ - Property:
+     - Each of the states should be in [-1.5, 1.5]
+
+Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf