Add support for singular state matrix in ExactDiscretizationAlgorithm

[ueliwechsler]

https://github.com/JuliaReach/MathematicalSystems.jl/pull/122#issuecomment-570776436

The current implementation #122 of the exact discretization of an affine system does throw an error if the state matrix is singular.

Here is an algorithm for this special case: https://math.stackexchange.com/questions/658276/integral-of-matrix-exponential

The implementation consists of computing the Jordan form of a matrix (see, e.g. https://discourse.julialang.org/t/jordan-form-of-a-matrix/7123/6) and the computation of the integral where B is a strictly upper triangular matrix

[ueliwechsler]

@mforets did you figure out how to best compute the Jordan form?

[mforets]

We were interested in floating-point computations and discarded using the Jordan normal form because it is ill-advised (ref. to the comments in that thread).

However, to compute that integral for non-invertible A I would suggest to use a series expansion of the "shifted" matrix exponential of A. For the theory, see page 8 in SpaceEx: Scalable verification of hybrid systems. We have written a Julia implementation of Φ1(A, δ) and Φ2(A, δ) in Reachability/src/discretize.jl.

[ueliwechsler]

Thanks for the information! I will have a look.