Reachability using the parallelotope method

[mforets]

See:

• Goldsztejn, A., & Ishii, D. (2016). A parallelotope method for hybrid system simulation. Reliable Computing, 23(1), 163-185.

[dpsanders]

@mforets Do you have an implementation of parallelotopes?

[mforets]

Hi David, A set type specific to parallelotopes is not available yet in LazySets, but we are working on it in LazySets#1632 -- PR which is kind of ready..

Depending on the application that you have in mind, you can use zonotopes, which are a generalization of parallelotopes of order greter than one.

As explained in the notes, there are different approaches for the parallelotope, either in constraint form (as in #1632) on in generator form. Again, depending on the use case, one representation may be preferable than the other.

[dpsanders]

OK great, thanks. I was asking in terms of implementing the algorithms in this and related papers by Goldsztejn.

[mforets]

Alright, I had a look to that paper again, and to get started we would need Theorem 3.1 in page 7, which gives a parallelotopic enclosure of the image set of a parallelotope through a (differentiable) function.

I have to think about it, but perhaps i can add it as an extension in RangeEnclosures.jl.

[mforets]

To mimic the notation in the paper, one can use a LazySets.AffineMap, which can be created with

Parallelotope(A, 𝐮, x̃) = AffineMap(A, 𝐮, x̃)

or equivalently

Parallelotope(A, 𝐮, x̃) = x̃ ⊕ A*𝐮

After looking with some detail Section 3.2, I think there are typos. Since x̃ is a vector, then 𝐲 := 𝛚(x̃) (mind the bold omega, for the interval extension of the discrete map omega) can only possibly be ω(x̃), because by definition of interval extension, ω(x) = 𝛚(x) if x is a scalar. But then 𝐲 - ỹ is identically zero, from Eq. (9). This doesn't make sense. In sum, shouldn't Theorem 3.1 define 𝐲 := 𝛚(□⟨𝐱⟩)?

[mforets]

With such considerations, I tried implementing Theorem 3.1 and the result can be found in this notebook. The final result is at the very end. I'm under the impression that i did something wrong, because the parallelotopic overapproximation is much bigger than the box overapproximation, which can be found in the plot in Out[31].

[dpsanders]

That's a really fantastic notebook, thanks! It illustrates very well a lot of the concepts that you've implemented so nicely in LazySets.jl.

I'll try to think about what's going on.

[dpsanders]

I agree that there is an error as you point out in the paper, and I think your interpretation is correct. I also agree that the result is a huge over-estimation. I think that's because the original parallelotope is so big -- I believe these estimates are supposed to be good for small initial objects?