ReachabilityAnalysis.jl

| Documentation | Status | Community | License | |:-----------------:|:----------:|:-------------:|:-----------:| | | | | |

✨ What is Reachability Analysis?

Reachability analysis is concerned with computing rigorous approximations of the set of states reachable by a dynamical system. In the scope of this package are systems modeled by continuous or hybrid dynamical systems, where the dynamics changes with discrete events. Systems are modelled by ordinary differential equations (ODEs) or semi-discrete partial differential equations (PDEs), with uncertain initial states, uncertain parameters or non-deterministic inputs.

The library is oriented towards a class of numerical methods known as set propagation techniques: to compute the set of states reachable by continuous or hybrid systems, such methods iteratively propagate a sequence of sets starting from the set of initial states, according to the systems' dynamics.

See our Frequently asked questions (FAQ) section for pointers to the relevant literature, related tools and more.

🎯 Table of Contents

💾 Installation

📙 Documentation

🎨 Features

:checkered_flag: Quickstart

🐾 Examples Gallery

:blue_book: Publications

📜 Citation

💾 Installation

Open a Julia session and activate the pkg mode (to activate the pkg mode in Julia's REPL, type ], and to leave it, type <backspace>), and enter:

julia pkg> add ReachabilityAnalysis

📙 Documentation

See the Reference Manual for introductory material, examples and API references.

📌 Need help? Have any question, or wish to suggest or ask for a missing feature? Do not hesitate to open an issue or join the JuliaReach Zulip chat: . You can also send an email to the developers.

🎨 Features

The following types of systems are supported (click on the left arrow to display a list of examples):

:checkered_flag: Quickstart

In less than 15 lines of code, we can formulate, solve and visualize the set of states reachable by the Duffing oscillator starting from any initial condition with position in the interval 0.9 .. 1.1 and velocity in -0.1 .. 0.1.

```julia using ReachabilityAnalysis, Plots

const ω = 1.2 const T = 2 * pi / ω

@taylorize function duffing!(du, u, p, t) local α = -1.0 local β = 1.0 local δ = 0.3 local γ = 0.37

x, v = u
f = γ * cos(ω * t)

# write the nonlinear differential equations defining the model
du[1] = u[2]
du[2] = -α*x - δ*v - β*x^3 + f

end

set of initial states

X0 = Hyperrectangle(low=[0.9, -0.1], high=[1.1, 0.1])

formulate the initial-value problem

prob = @ivp(x' = duffing!(x), x(0) ∈ X0, dim=2)

solve using a Taylor model set representation

sol = solve(prob, tspan=(0.0, 20*T), alg=TMJets21a());

plot the flowpipe in state-space

plot(sol, vars=(1, 2), xlab="x", ylab="v", lw=0.5, color=:red) ```

🐾 Examples

| | | |:--------:|:-----:| | Quadrotor altitude control | Lotka-Volterra with tangential guard crossing| | | | | Laub-Loomis model |
Production-Destruction model| | | | | Coupled van der Pol oscillator | Spacecraft rendezvous |

:blue_book: Publications

This library has been applied in a number of scientific works.

📜 How to cite

Research credit and full references to the scientific papers presenting the algorithms implemented in this package can be found in the source code for each algorithm and in the References section of the online documentation.

If you use this package for your research, we kindly ask you to cite the following paper, see CITATION.bib. Moreover, please also cite the appropriate original references to the algorithms used.