Frequently Asked Questions (FAQ)

General questions

What are good introductory papers on the subject?

An elementary introduction to the principles of set-based numerical integration can be found in Oded Maler's article Computing Reachable Sets: An Introduction. For an introduction to hybrid systems reachability we recommend the lecture notes of Prof. Goran Frehse, Formal Verification of Piecewise Affine Hybrid Systems (DigiCosme Spring School, Paris, May 2016). Most up-to-date material related to reachability analysis can be found in journals, conference articles or in PhD theses. For a comprehensive review of different set propagation techniques for linear, nonlinear and hybrid systems see [AFG20]. The article also contains a discussion of successful applications of reachability analysis to real-world problems. We refer to the References section of this manual for further links to the relevant literature.

Are there other tools that perform reachability analysis?

The wiki Related Tools contains an extensive list of pointers related to reachability analysis tools for dynamical systems. Languages and tools for hybrid systems design are described in the review article [CPPSV06] (a bit outdated with respect to the tools since it is of 2006).

A subset of such tools has participated in recent editions of the Friendly Competition for Applied Reachability of Continuous and Hybrid Systems, ARCH-COMP. In alphabetic order: Ariadne, CORA, C2E2, DynIbex, Flow*, HyDRA, Hylaa, Isabelle/HOL-ODE-Numerics, SpaceEx and XSpeed. A paragraph describing each tool's main characteristics can be found in the ARCH-COMP articles for each category (AFF for linear and NLN for nonlinear).

The IEEE Control Systems Society (CSS) has a Technical Committee on Hybrid Systems that is dedicated to providing informational forums, meetings for technical discussion, and information over the web to researchers in the IEEE CSS who are interested in the field of hybrid systems and its applications. A list of actively-maintained tools for the analysis and synthesis of hybrid systems, compiled by members of such committee, can be found here.

Why did you choose Julia to write this library?

The language choice when programming for research purposes usually depends on the developers' background knowledge which directly impacts convenience during development and output performance in the final product. On the one hand, compiled languages such as C++ offer high performance, but the compilation overhead is inconvenient for prototyping. On the other hand, interpreted languages such as Python offer an interactive session for convenient prototyping, but these languages fall behind in performance or need to extend the code to work with another lower-layer program such as Numba or Cython (known as the two-language problem). A compromise between the two worlds are just-in-time (JIT) compiled languages such as MATLAB. Last but not least, the ecosystem of libraries available and the user base is also an important consideration.

In our case, we began to develop the JuliaReach stack in 2017 and quickly adopted the language when it was at its v0.5 [v1]. Julia is a general-purpose programming language but it was conceived with high-performance scientific computing in mind, and it reconciles the two advantages of compiled and interpreted languages described above, as it comes with an interactive read-evaluate-print loop (REPL) front-end, but is JIT compiled to achieve performance that is competitive with compiled languages such as C [BEKS17]. A distinctive feature of Julia is multiple dispatch (i.e., the function to execute is chosen based on each argument type), which allows to write efficient machine code based on a given type, e.g., of the set. As additional features, Julia is platform independent, has an efficient interface to C and FORTRAN, is supported in Jupyter notebooks (the "Ju" in Jupyter is for Julia) and well-suited for parallel computing. Julia has a determined and quickly-growing community, especially for scientific tools (see the JuliaLang Community webpage). All this makes Julia an interesting programming language for writing a library for reachability analysis.

What is the wrapping effect?

Quoting a famous paper by R. E. Moore [M65]:

Under the flow itself a box is carried after certain time into a set of points which will in general not remain a box excepted for a few simple flows.

The wrapping effect is associated to error propagation that arises from the inability of a set representation to accurately abstract some properties of system under study. Wrapping-free methods only exist for linear systems. Nonlinear reachability methods control, but do not totally elimitate, the wrapping effect in different ways.

As a simple illustration of the wrapping effect, consider the image of a box through a rotation in discrete time-steps. Box enclosures (full line) introduce a strong wrapping effect. On the other hand, had we represented the sequence using zonotopes (dashed lines), the result would be exact, i.e. without wrapping, since the image of a hyperrectangular set under an affine map is a zonotope.

using LazySets, Plots

R(θ) = [cos(θ) -sin(θ); sin(θ) cos(θ)]

B = BallInf(ones(2), 0.1)
B′ = R(π/4) * B
B′′ = R(π/2) * B

□B = box_approximation(B)
□B′ = box_approximation(B′)
□B′′ = box_approximation(R(π/4) * □B′)

plot(B, ratio=1, lw=2.0, style=:dash)
plot!(B′, lw=2.0, style=:dash)
plot!(B′′, lw=2.0, style=:dash)

plot!(□B, lw=2.0, style=:solid)
plot!(□B′, lw=2.0, style=:solid)
plot!(□B′′, lw=2.0, style=:solid)

Does reachability solve for the vertices of the set?

What happens if you consider a chaotic system?

Can reachability analysis be used to solve large problems?

Solving capabilities

How can I visualize trajectories?

It is often necessary to plot a "bunch" of trajectories starting from a set of initial conditions. The parallel ensemble simulations capabilities from the Julia DifferentialEquations.jl suite can be used to numerically simulate a given number of trajectories and it counts with state-of-the-art algorithms for stiff and non-stiff ODEs as well as many other advanced features, such as distributed computing, multi-threading and GPU support. See EnsembleAlgorithms for details.

As a simple example consider the scalar ODE $x'(t) = 1.01x(t)$ with initial condition on the interval $x(0) \in [0, 0.5]$. To solve it using ensemble simulations, pass the ensemble=true keyword argument to the solve function (if the library DifferentialEquations was not loaded in your current session, an error is triggered). The number of trajectories can be specified with the trajectories keyword argument.

using ReachabilityAnalysis, DifferentialEquations

# formulate initial-value problem
prob = @ivp(x' = 1.01x, x(0) ∈ 0 .. 0.5)

# solve the flowpipe using a default algorithm, and also compute trajectories
sol = solve(prob, tspan=(0.0, 1.0), ensemble=true, trajectories=250)

# plot flowpipe and the ensemble solution
using Plots

plot(sol, vars=(0, 1), linewidth=0.2, xlab="t", ylab="x(t)")
plot!(ensemble(sol), vars=(0, 1), linealpha=1.0)