Reachability is a software for reachability analysis and safety property checking that performs flowpipe computation of dynamical systems given by ordinary differential equations models (ODEs) in continuous or discrete time. Currently this package implements algorithms that can handle:
- flowpipe computation of affine ODEs with nondeterministic inputs
- hybrid dynamical systems (hybrid automata) with nondeterministic affine ODEs in each mode
Reachability is written in Julia, a modern high-performance language
for scientific computing.
Reachability is a software for reach set approximation and safety properties
of affine ordinary differential equations (ODEs) with nondeterministic inputs.
It is written in Julia, a modern high-performance language for scientific computing.
This package requires Julia v0.6 or later. Refer to the official documentation on how to install and run Julia in your system.
The set computations depend on the core library LazySets.jl, which is also part of the JuliaReach framework.
LazySets exploits the principle of lazy (on-demand) evaluation and uses support functions to represent lazy sets.
The latest stable release of LazySets.jl is installed automatically when you install
Reachability.jl, see installation instructions below. You can always install the development version via
Pkg.clone; see the installation section of LazySets.jl for further details.
To install this package, use the following command inside Julia's REPL:
To checkout the latest version, do