Overview

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

Linear hybrid

Nonlinear continuous

Nonlinear hybrid