2020 Benchmark Proposal: Pendulum and Airplane by Chelsea Sidrane and Amir Maleki
Details here with writeup:
https://github.com/amaleki2/benchmark_closedloop_verification
(I decided to write here rather than in the general 2021 thread because this discussion is problem specific.)
We have simulation results for all models and they are mostly consistent with (i.e., contained in) the flowpipes depicted in the report; the only exception is the "Single Pendulum" model. I checked our modeling (compared to the description linked above, the description in the report, and the modeling in NNV from [1]) several times and cannot spot an error (I tried both the .nnet and .mat files for the neural network).
The only thing I observed is that NNV uses a third state variable that I cannot explain (x3(0) = 1, x3' = 20); it should not have any effect because it does not occur in the other equations and in the end it is projected away as far as I can tell, but this is just my superficial understanding of the script.
We have at least one simulation that starts in the subset that NNV starts from, so at least the flowpipe is inconsistent with the simulations and one of the results is incorrect. Of course the error may be on our side. As mentioned, the other models yield consistent results, and together with the fact that the model is very simple, I am fairly confident in our results.
I am not sure what to do. Maybe the NNV authors have a comment?
Assuming that the simulations are correct, the model should instead be verifiable (see the attached plot). Showing a bunch of simulations is of course no proof.
[1] https://github.com/verivital/ARCH-COMP2020/tree/master/benchmarks/Single_Pendulum
The third variable was just used to plot the results with respect to time (in this case the steps), but has no effect on the other state variables.
Taking a closer look at this benchmark again, I am not sure there is any difference on the dynamics, but there may be some mistakes/confusion around the specifications.
Based on the original proposal for last year: (Single Pendulum) , we understand that the safety specification is for the period between control period 10 to 20 (nt), not 10 to 20 seconds, that is where the difference may be. The specifications from the GitHub repository seem to be incorrect, but we will update them now.
Thanks for the quick reply. Great finding, that explains it indeed. Note that the spec also needs to be fixed in the report.
Then I can confirm that our simulations (attached) also falsify the model.