ReachabilityAnalysis.jl

Reachability Analysis is concerned with computing rigorous approximations of the set of states reachable by a dynamical system. The scope of the package are systems modeled by ordinary differential equations (ODEs) with uncertain initial states, uncertain parameters or non-deterministic inputs.

Resources

• Reference manual
• Citation

Features

The following types of systems are supported:

• Continuous ODEs with linear dynamics
• Continuous ODEs with non-linear dynamics
• Hybrid systems with piecweise-affine dynamics
• Hybrid systems with non-linear dynamics

References to the scientific papers presenting the algorithms implemented in this package can be found in the source code and in the online documentation.

Installation

Once you have installed Julia in your system, open a Julia session, activate the pkg mode (remember that to activate the pkg mode in Julia's REPL, you need to type ], and to leave it, type <backspace>), and enter:

pkg> add ReachabilityAnalysis

📖 This package is still a work-in-progress. It grew out of the package JuliaReach/Reachability.jl. If you are interested to know more about the project, feel free to open an issue or join the chat room JuliaReach gitter channel.

!! NOTE: currently using mforets/dev branch in LazySets.jl.

Examples

We suggest to explore the Examples section of the online documentation for examples illustrating how to use the library.

Linear

using ReachabilityAnalysis, Plots

prob = @ivp(x' = 1.01x, x(0) ∈ 0 .. 1)
sol = solve(prob, tspan=(0.0, 1.0))

plot(sol, vars=(0, 1))

Higher-order linear

(motor or a problem from the problem library)

using ReachabilityAnalysis, Plots

A = [1 0; 0 -1]
B = [1, 1]
X = Universe(n)
U = Interval(-0.1, 0.1)
X0 = ...
prob = @ivp(x' = Ax + Bu, x ∈ X, u ∈ U, x(0) ∈ X0)
sol = solve(prob, T=1.0, GLGM06())

plot(sol, vars=(1, 2))

Nonlinear

(van der pol?)

using ReachabilityAnalysis, Plots

A = [1 0; 0 -1]
B = [1, 1]
X = Universe(n)
U = Interval(-0.1, 0.1)
X0 = ...
prob = @ivp(x' = Ax + Bu, x ∈ X, u ∈ U, x(0) ∈ X0)
sol = solve(prob, T=1.0, GLGM06())

plot(sol, vars=(1, 2))

Hybrid

(bouncing ball?)

using ReachabilityAnalysis, Plots

A = [1 0; 0 -1]
B = [1, 1]
X = Universe(n)
U = Interval(-0.1, 0.1)
X0 = ...
prob = @ivp(x' = Ax + Bu, x ∈ X, u ∈ U, x(0) ∈ X0)
sol = solve(prob, T=1.0, GLGM06())

plot(sol, vars=(1, 2))

Citation

If you use this package for your research, we kindly ask you to consider citing the following paper.

@inproceedings{bogomolov2019juliareach,
  title={JuliaReach: a toolbox for set-based reachability},
  author={Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
  booktitle={Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control},
  pages={39--44},
  year={2019}
}