Module Frama_c_kernel.Lti_system

This module aims to provide overapproximations of the behaviors of linear time-invariant systems, for both the transition and the permanent phases.

A LTI system corresponds to the following recursive equation :

X[t + 1] = AX[t] + Bε[t] + S

where :

• 𝕂 is a field ;
• n is the system's state dimension, or order ;
• m is the system's input space dimension ;
• X[t] ∈ 𝕂^n is the system's state vector at iteration t ;
• μ[t] ∈ 𝕂^m is an input vector at iteration t ;
• A ∈ 𝕂^{n × n} is the state matrix ;
• B ∈ 𝕂^{n × m} is the input matrix ;
• S ∈ 𝕂^n is the system's shift.

Several notes here :

• The only hypothesis on A is that its eigenvalues are all lower than one in absolute value. It is a sufficient condition for the filter to converge. Conversely, there is no hypothesis on B. If the procedure cannot prove easily that this hypothesis is satisfied, it will simply return None.
• All input vectors are supposed belonging to a box in 𝕂^m.
• Most presentations of LTI systems describe them using two equations, a recursive one equivalent to the one presented here and focused on the hidden state vector, and an output non recursive equation focused on transforming the hidden state vector into a usable output. However, as the two equations can be easily combined into one, it is not considered in this module.
• Usually, the shift is not present, as it makes the system kind of affine instead of linear. However, the theory underlying this module can easily take it into account, and thus make it more general.

A complete documentation on the underlying theory will be added in a near future. For an example using this module, one can check its tests, located in ./test/lti_system.