Benchmark

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

Visible to the public two_genes.txt

forum

Visible to the public PARA Problem Instance: Two-genes network

Prelude:
I know this is very late; I wanted to see what format other people use in this category - which did not work so well :D
So now I simply present a piecewise-linear problem in our tool-specific format.
I could try to convert to other formats if somebody prefers.


General problem description:
See here: http://dx.doi.org/10.1093/bioinformatics/btm362

file

Visible to the public NAV.zip

forum

Visible to the public Scalable NAV model (HPWC style)

The well known navigation (NAV) example from [1] models the motion of a point robot in a n-dimensional cube. The cube is partitioned into m^n rectangular regions and each such region is associated with a vector field described by the flow equations. It is extended in [2] to a scalable n- dimensional HPWC model to increase the complexity of the model.


In the attached files, we present a script to generate arbitatry large NAV models in HPWC style and we also provide some instances generated automatically.

file

Visible to the public benchmarks.tar.gz

file

Visible to the public motor_generate.cpp

forum

Visible to the public The scalable adaptive cruise controller model

Here is a model for an adaptive cruise controller, very similar with the one in HPWC category, http://cps-vo.org/node/31200.

Model Description, copied from http://cps-vo.org/node/31200: There are n vehicles is a queue, each of which senses the speed of the car in front an keeps this speed. The speed sensor have possible distrurbance constrained in an interval.

forum

Visible to the public HPWC instance from HyCOMP paper

We propose the following benchmarks for hybrid automata with piecewise constant dynamics.

The benchmarks we are proposing are:

- A distributed controller for a robot

- A simple system that controls a nuclear reactor

- A piecewise consant version of the navigation benchmark

The benchmark are taken and adapted from the existing literature, and are quickly described in the paper http://www.sergiomover.eu/paper/tacas15.pdf

They can already be downloaded from the link in the paper.

forum

Visible to the public CNLN: van der Pol

I have seen the van der Pol system in many papers, so probably most tools/tool authors have this example at their disposal:

x' = y

y' = (1 - x^2)*y - x

Is this interesting for the competition?

file

Visible to the public acc.tar.bz2