Benchmark

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

Visible to the public ARCH-Comp Problem instance collection

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):

file

Visible to the public Building.xml

file

Visible to the public Building.cfg

forum

Visible to the public CAFF Problem Instance: Building

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."

file

Visible to the public readme.txt

file

Visible to the public platoonComp.xml

file

Visible to the public break20_box_1.cfg

forum

Visible to the public HPWA Problem Instance: Platoon

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.

file

Visible to the public EMB_hybrid.zip

forum

Visible to the public Updated Model of Experimental Brake System

Hello everybody,

I have attached a new version of the experimental brake model containing some changes: