We organize the models by the type of nonlinearities (if there are some), and whether they are purely continuous or present discrete transitions, i.e. hybrid systems. We have added a column with the associated scientific domain, and another column with the number of state variables. Roughly speaking, a higher number of state variables usually corresponds to problems which are harder to solve, although strictly speaking, this usually depends on the property to be verified.

Column P.V. refers to the cases where the example is presented with at lest one instance with parameter variation.

Further examples

In addition to those present in this manual, a larger collection of examples can be found in the models library ReachabilityModels.jl. For further instructions see the section Model library.

Linear continuous

NameAreaState dim.
Damped oscillatorPhysics2
BuildingMechanical Engineering48
Transmission line circuitPower Systems Stability4 to 40
International Space StationAerospace Engineering270
Modified Nodal Analysis 1Electronics1002
Modified Nodal Analysis 2Electronics10913
Heat PDEPhysics125 to 125000

Linear hybrid

NameAreaState dim.
Amplifier circuitElectronic Engineering2
Electromechanic breakElectronic Engineering
GearboxMechanical Engineering
PlatoonAutonomous Driving
PowertrainMechanical Engineering

Nonlinear continuous

NameAreaState dim.
Laub-LoomisMolecular Biology7
Lorenz system
Production-DestructionElectrical engineering
SEIR Model
Van der Pol

Nonlinear hybrid

NameAreaState dim.
Lotka-Volterra w/crossingBiology, Nonlinear physics