Benchmarks of continuous and hybrid systems

Introduction

We collected a set of benchmarks for the reachability analysis of continuous and hybrid systems. In the following content, they are classified according to the types of dynamics.

Linear continuous benchmarks

name # of variables Flow* file SpaceEx file
H2 Based N Vehicle Platoon 15-30  vehicle_platoon_5
vehicle_platoon_10
5_vehicles
10_vehicles

Non-linear continuous benchmarks

name # of variables Flow* file
Van der Pol oscillator 2 download
Brusselator 2 download
Jet engine model 2 download
Buckling column model 2 download
Lotka-Volterra model 2 download
Lac operon 2 download
Lorentz system 3 download
Roessler attractor 3 download
Steam governor 3 download
Spring pendulum 4 download
Coupled Van der Pol oscillator 4 download
Biological model I 7 download
Biological model II 9 download

 

Linear hybrid benchmarks

The SpaceEx and Flow* model files are provided in the pages for model description.

name # of variables # of modes # of jumps
Bouncing ball 2 1 1
Two tank system 2 4 7
Two tank system with controller 22 34 296
Rod reactor 3 2 2
Cruise control 3 6 11
Linear switching system 5 5 5
Three vehicle platoon 9 2 2
Filtered oscillator 6-34 4 4
Leaking tank system with controller 12 11 34
Thermostat system with controller 8 8 18

Non-linear hybrid benchmarks

The Flow* model files are provided in the pages for model description.

name # of variables # of modes # of jumps
Non-holonomic integrator 3 4 5
Spiking neurons 2 1 1
Glycemic control 4 2-3 1-4
Glycemic control (polynomial version) 4 6,9 10,18
Non-linear transmission line circuits n 3 2

Related links

Download the source code of Flow* v1.2.2b

ARCH 2014 hybrid benchmarks collection

HyST source transformation tool