search

JuliaReach / Reachability.jl

Reachability and Safety of Nondeterministic Dynamical Systems
MIT License
50 stars 4 forks source link

Low-dimensional discrete-post operator #275

Open schillic opened 6 years ago

schillic commented 6 years ago

Terminology: An embedded set is a high-dimensional set that is universal in some dimensions. Let U(m) be the m-dimensional universal set. Then I am talking about a set U(k) × L × U(l) with L being a low-dimensional set. For example, an interval embedded in 2D is a thick vertical or horizontal line, depending on whether it is defined for the dimension x1 or x2.

To take the intersection of two embedded sets, it suffices to take the intersection for the non-universal dimensions and (if not empty) embed again in high dimensions.

Name for embedded sets

What is a good name?

Interface for embedded sets

I think we can assume that the input system is given in full dimensions. Thus we need some way to detect embedded sets in the first place.

After detection, we need to store this information. We can either create a new system (which requires to minimally change the current interface) or have some additional data structure (sounds complicated). For instance, we could have a wrapper Embedding(L::LazySet{N}, n::Int, i0::Int) <: LazySet{N} in LazySets which takes a low-dimensional set L and acts like a high-dimensional set in n dimensions, where i0 is the first index where the set is not universal (i.e., the represented set is U(i0-1) × L × U(n-(i0+dim(L)-1))).

schillic commented 6 years ago

While I still think the above is an interesting approach, for now I will try a straightforward one: For your current location, find all dimensions that are relevant for the guards, and then do the continuous post only in those dimensions (for now: use 1D blocks). Then, for each transition, take a projection of the source invariant and guard in those dimensions. Then we have to compute those reach sets where the invariant intersects in high dimensions again (this will be the most complicated part). We should repeat the invariant intersection to see if we missed something in the first round, but this could be optional. Finally, we apply the assignment and take the intersection with the target invariant, which happens again in high dimensions.