Add overapproximate for exponential map for SPZ and Zonotope

[alecarraro]

Implement proposition of LKB23

[schillic]

I tried out a simple example where the SPZ is just a zonotope and the MZ is just a matrix. The overapproximation is not enormously bigger, and it gets quite tight when raising $\kappa$ to 5. This gives some confidence in the correctness.

using LazySets
import IntervalMatrices
N = Float64
P = SparsePolynomialZonotope(zeros(N, 2), zeros(N, 2, 0), N[1 0; 0 1], zeros(Int, 1, 0), [2])
M = N[1 0; 0 1]
EP = exponential_map(M, P)
MZ = MatrixZonotope(M, Vector{Matrix{N}}())
MZE = MatrixZonotopeExp(MZ)
EM = ExponentialMap(MZE, P)
oEP = overapproximate(EM, SparsePolynomialZonotope, 2)  # for value 5 the sets are almost identical

using Plots
plot(oEP)
plot!(EP)

[alecarraro]

I tried out a simple example where the SPZ is just a zonotope and the MZ is just a matrix. The overapproximation is not enormously bigger, and it gets quite tight when raising κ to 5. This gives some confidence in the correctness.

thats very nice!

[schillic]

I tried out a simple example where the SPZ is just a zonotope and the MZ is just a matrix. The overapproximation is not enormously bigger, and it gets quite tight when raising κ to 5. This gives some confidence in the correctness.

With the new code changes, the sets are actually identical already for κ = 2.

I was first surprised because I expected the approximation to get coarser with the fixes. But then I realized that this happens because you now handle this case exactly. So the example above is not a good benchmark anymore 😅

[schillic]

Modifying the example slightly,

MZ = MatrixZonotope(M, [N[0 0; 0 0]])

i.e., adding a zero generator to the MZ, does not trigger the shortcut. So it uses the proper approximation, and I get basically the same results as before.

[schillic]

@alecarraro Is this ready to be merged?

[alecarraro]

@alecarraro Is this ready to be merged?

Yes, I implemented all the feedback from your reviews. I tested the reachability algorithm to test a real use case of these methods and it works .