A verification benchmark is a model together with a list of properties to be checked on the model.
forum
Submitted by sschupp on Fri, 12/09/2016 - 6:50am
I was wondering how existing ARCH benchmarks come into play reagarding the competition and the presentation of certain benchmarks in the respective groups. As others are maybe wondering as well, here's a more comprehensive task description (Thanks Goran):
forum
Submitted by stanleybak on Wed, 12/07/2016 - 11:01am
This benchmark is taken from the paper "Large-Scale Linear Systems from Order-Reduction", by Hoang-Dung Tran, Luan Viet Nguyen, and Taylor T. Johnson.
Description from the paper: "The building model is a model of the Los Angeles University Hospital with 8 floors, each of which has 3 degrees of freedom. This system has 48 state variables in which we are mostly interested in the twenty-fifth state x_25(t), which is the motion of the first coordinate."
forum
Submitted by frehse on Wed, 11/30/2016 - 8:53am
This is a piecewise affine system with 10 state variables and nondeterministic switching between two modes. Reachability should be over an infinite time- and switching horizon.
It does not look easy for forward reachability to find a fixed point. Methods for invariant generation may perform much better.
forum
Submitted by JensOehlerking on Wed, 05/20/2015 - 4:55am
Hello everybody,
I have attached a new version of the experimental brake model containing some changes: