ReachabilityAnalysis.jl

ReachabilityAnalysis.jl copied to clipboard

Reachability with polynomial zonotopes for nonlinear ODEs (KA19)

1

## Set representations - ~~[PolynomialZonotopes.jl](https://github.com/JuliaReach/PolynomialZonotopes.jl) in JuliaReach~~ Polynomial Zonotope in LazySets - new SparsePolynomialZonotope in LazySets (?) - Representation of Polytopes as Polynomial Zonotopes, https://arxiv.org/pdf/1910.07271.pdf ## Algorithms - [Reachability analysis...

mforets

- example passing a vector of X0 as input

mforets

mforets

example: ```julia @taylorize function _vanderpol!(du, u, params, t) local μ = 1.0 du[1] = u[2] du[2] = (μ * u[2]) * (1 - u[1]^2) - u[1] nothing end u0 =...

mforets

- Optionally apply convex hull - Preallocations - Other ideas from https://nbviewer.jupyter.org/github/mforets/escritoire/blob/master/sets/DiscreteSequence.ipynb

mforets

Reachability for linear systems using vrep

2

https://nbviewer.jupyter.org/github/mforets/escritoire/blob/master/sets/DiscreteSequence.ipynb

mforets

Concrete projection of zontope reach-set with SArray matrix should return a zonotope with SArray center and generators.

mforets

- Concrete projection with `project` Applies to `

mforets

ref notebook: https://github.com/mforets/escritoire/blob/master/2020/Week51/Flat_Zono_Plot.ipynb

mforets

``` TypeError: in typeassert, expected ReachSet{Float64,Union{HPolytope{Float64,LazySets.Arrays.SingleEntryVector{Float64}}, HPolytope{Float64,Array{Float64,1}}}}, got a value of type ReachSet{Float64,HPolytope{Float64,Array{Float64,1}}} Stacktrace: [1] setindex!(::Array{ReachSet{Float64,Union{HPolytope{Float64,LazySets.Arrays.SingleEntryVector{Float64}}, HPolytope{Float64,Array{Float64,1}}}},1}, ::ReachSet{Float64,HPolytope{Float64,Array{Float64,1}}}, ::Int64) at .\array.jl:847 [2] push!(::Array{ReachSet{Float64,Union{HPolytope{Float64,LazySets.Arrays.SingleEntryVector{Float64}}, HPolytope{Float64,Array{Float64,1}}}},1}, ::ReachSet{Float64,HPolytope{Float64,Array{Float64,1}}}) at .\array.jl:936 [3] push!(::Flowpipe{Float64,ReachSet{Float64,Union{HPolytope{Float64,LazySets.Arrays.SingleEntryVector{Float64}}, HPolytope{Float64,Array{Float64,1}}}},Array{ReachSet{Float64,Union{HPolytope{Float64,LazySets.Arrays.SingleEntryVector{Float64}},...

dfcaporale