Three-element overapproximation of the Minkowski sum of an intersection

[mforets]

Given sets X, Y and Z three subsets of R^n, the following holds:

    (X∩Y)⊕Z ⊆ (X⊕Z)∩(Y⊕Z).

The inclusion is strict, in general.

Ref: Prop. 7.1. in Le Guernic's thesis.

[schillic]

I do not see the benefit here. The expression on the right looks more complicated to me.

[mforets]

It can be used for the overapproximation of the exact solution of the recurrence equation that appears in the discretization of x'(t) = Ax(t) + Bu(t) where u(t) is nondeterministic, u(t)∈ U, and the state is constrained to an invariant, x(t) ∈ I. The discrete equation is:

N_{i+1} = (ΦN_i ⊕ V) ∩ I,

since we have to intersect with the invariant.

Now the closed form of N_i is quite complicated. Instead one can overapproximate its solution with that of two other sequences which do not have intersection (they are of the form X_{k_1} = A X_k ⊕ V as shown below, see Corollary 7.1 in Le Guernic's thesis). The intersection part is shifted on top of calculating each new N_i.

Indeed,

N_{i+1} ⊆ Ω_i ∩ (⋂_{j=0}^{i-1} I_j),

where Ω_i and I_j are the solutions of the linear sequences Ω_{k+1} = Φ Ω_k ⊕ V and I_{k+1} = Φ I_k ⊕ V respectively. What is interesting here is that one can use efficient methods for finding Ω_i and I_j. The difficult part is ⋂_{j=0}^{i-1} I_j which can be again overapproximated using support functions, by taking the minimum value for instance, since it holds in general that ρ_{X∩Y}(ℓ) ≦ min(ρ_X(ℓ), ρ_Y(ℓ)).