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