Reach sets

[ga72kud]

Hi, I want to prevent my algorithm with the command project of doing overapproximations. Is there any flag to prevent the overapproximation?

Instead of computing a reach set say for example for [0, 4s] in one step

I want to compute four coupled reach sets

[schillic]

In principle, project should be exact. Do you have a counterexample?
Since you are talking about reach sets, those are defined in ReachabilityAnalysis.jl. It uses this package to represent the sets, but the time information and construction live over there.
I did not exactly understand what you are trying to achieve. You can also join the chatroom in Gitter to explain it.

[ga72kud]

Thank you @schillic, I have joined the chatroom in Gitter. I could explain what I am doing. I tested the LazySets.project function and yes I am using the ReachabilityAnalysis.jl.

I want to use reachability analysis for conservative analysis of dynamic systems. I have a dynamic system with 6 states (2 dimensions for position in x- and y direction). I use the project function from the LazySets to visualize the state evolution of the system. I was wondering that I get bigger areas for the same problem if I use multiple reach sets instead of in a single run.

for the whole time range [0, T]

 prob_set_sysᵦ = @ivp(x' = sys2_A*x + sys2_B*u, x(0) ∈ 𝒳ᵦ, u ∈ 𝒰ᵦ, x ∈ Universe(6))
ℛₐ = ReachabilityAnalysis.solve(prob_set_sysₐ, alg=GLGM06(δ=Ts), T=T);
𝒫ℛₐ=LazySets.project(ℛₐ , [1, 2])

for multiple runs like in a foor loop (in my case I have discrete events) [0, T_1][T_1, T_2]....[T_-1, T])

      ℛ6=take!(reach6_set_channel)      
      #Reachability Analysis as before
      𝒫ℛ=LazySets.project(ℛ , [1, 2])      
      𝒫ℛ=[𝒫ℛ6.Xk[i].X∩𝒫ℛ4.Xk[i].X for i in 1:length(𝒫ℛ4.Xk)]
      𝒫ℛ=intersection.(𝒫ℛ6, 𝒫ℛ4)
      put!(reach6_set_channel, ℛ6.F.Xk[end].X)

t
It might be the problem with reachability Analysis.jl. I can close the Issue and reopen it there. I was guessing that the problem comes from project function

[schillic]

To plot reach sets, there is a keyword argument vars that expects a pair with the dimensions (0 corresponds to time). So for instance plot(R, vars=(1, 2)) plots the first two dimensions. You do not have to manually project.

[ga72kud]

I use a version of
Liu, Stefan B., et al. "Provably safe motion of mobile robots in human environments." 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). IEEE, 2017.
where two parallel reach sets are computed (4 and 6 dimensional)

This does not work, if I project the 6 dimensional reach sets to 4 dimensions

ℛ6=reach.show_reach6(ℛ6, AMAX_VAL)
      ℛ4=reach.show_reach4(ℛ4, VMAX_VAL)
      𝒫ℛ6=LazySets.project(ℛ6 , [1, 2, 3, 4])
      #𝒫ℛ4=LazySets.project(ℛ4 , [1, 2])
      #𝒫ℛ=[ℛ6.Xk[i].X∩ℛ4.Xk[i].X for i in 1:length(𝒫ℛ4.Xk)]
      ℛ=intersection.(𝒫ℛ6, ℛ4)

      display(plot!(ℛ, vars=(1,2), alpha=alpa, color=col, subplot=1, aspect_ratio=:equal))

what works for me, where I get the enlargement (overapproximation) of positions:

ℛ6=reach.show_reach6(ℛ6, AMAX_VAL)
      ℛ4=reach.show_reach4(ℛ4, VMAX_VAL)
      𝒫ℛ6=project(ℛ6 , [1, 2])
      𝒫ℛ4=project(ℛ4 , [1, 2])
      𝒫ℛ=[𝒫ℛ6.Xk[i].X∩𝒫ℛ4.Xk[i].X for i in 1:length(𝒫ℛ4.Xk)]
      𝒫ℛ=intersection.(𝒫ℛ6, 𝒫ℛ4)

      display(plot!(𝒫ℛ, vars=(1,2), alpha=alpa, color=col, subplot=1, aspect_ratio=:equal))

[mforets]

I want to prevent my algorithm with the command project of doing overapproximations.

Do you mean project(X, vars) in this library?

Is there any flag to prevent the overapproximation?

By design, LazySets.project shouldn't perform overapproximations, and if you found a counterexample then it is a bug. But to fix this we would need a way to reproduce the problem. (It doesn't matter if it's your real problem or a modified version of it, so long as there is something we can run.)

For instance,

julia> X = rand(3,3)*rand(Hyperrectangle, dim=3); # some data

julia> project(X, 1:2) # concrete projection, no approximation
Zonotope(...)

julia> overapproximate(Projection(X, 1:2), HPolygon) # approximation of the projection using support functions
HPolygon(...)

[ga72kud]

Thank you for your feedback and information. I will provide an example. I will continue the issue here.

from https://gitter.im/JuliaReach/Lobby?utm_source=notification&utm_medium=email&utm_campaign=unread-notifications

@schillic, as you mentioned, "you mean that you start a new reachability analysis from the last reach set, then yes, it is clear that you get an overapproximation that way." Is there any possibility of setting the overapproximation off? Yes, I want to start multiple reach sets. Is there any possibility to prevent overapproximation in LazySets or ReachabilityAnalysis (I do not know if it is instead a problem for reachability analysis.jl)

I have looked in my code:

ℛ = ReachabilityAnalysis.solve(....);

It seems that the problem does not come from LazySets.jl, but more on ReachabilityAnalysis.jl. Sorry for that. It was not clear to me beforehand.
Is there a possibility to set the overapproximation off?

[mforets]

It is not my intention to sound pedantic, not at all, but without addressing the question

we would need a way to reproduce the problem

I don't even know if this issue is related to a new feature request, or you found a bug, or just ask for feedback regarding the way to use the library for the problem at hand.

For instance, in

ℛ = ReachabilityAnalysis.solve(....);

This is too vague to give you a useful answer for

Is there a possibility to set the overapproximation off?

Which algorithm did you use? Do you refer to the set representation used in the algorithm? Is it in the discretization phase, or in the set propagation phase? etc. Please consider taking the time to frame the question as a small reproducible example that we can start discussing.

[ga72kud]

ok thank you