ReachabilityAnalysis.jl

ReachabilityAnalysis.jl copied to clipboard

ref https://github.com/JuliaReach/ReachabilityAnalysis.jl/pull/258

mforets

Some properties should hold only for some locations; for example, the following function (taken from the spacecraft model, see [this repo](https://github.com/JuliaReach/ARCH2020_AFF_RE)) checks whether the secnd location of the hybrid flowpipe...

mforets

An old ODE/IVP solution approach based on interval arithmetic is outlined in [*Introduction to interval analysis*](https://epubs.siam.org/doi/book/10.1137/1.9780898717716), Section 10.2, or in [*A brief introduction to interval analysis*](https://doi.org/10.1007%2F978-3-319-05311-0_7), p. 191f. The idea...

schillic

Consider the hybrid solve when we check if the newly computed set has already been explored: ```julia # check if this location has already been explored; # if it is...

mforets

Currently `count_jumps` in the hybrid solve loop advances by one for each element in the clustering, https://github.com/JuliaReach/ReachabilityAnalysis.jl/blob/b4f9bef95ea367b7623fb36251e603862d701a45/src/Hybrid/solve.jl#L127 This is not good because the stopping criterion on max jumps now depends...

mforets

Under-approximations

1

Under-approximations for solutions of ODEs, implemented via a generalized mean-value form: https://ieeexplore.ieee.org/abstract/document/9099222 Implemented in https://github.com/cosynus-lix/RINO

dpsanders

mforets

mforets

Backward reachable set: Luc Jaulin

1

The recent paper [101] in this list: https://www.ensta-bretagne.fr/jaulin/publications.html describes an algorithm for constructing backward reachable sets of ODEs. The PDF is here: https://www.ensta-bretagne.fr/jaulin/paper_basin.pdf

dpsanders

not urgent, but there is some nonsense with some combinations of options as i'll collect below. - the idea of `BoxIntersection` is to compute X \cap Y by overapproximating with...

mforets