Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 67 additions & 0 deletions src/Approximations/overapproximate.jl
Original file line number Diff line number Diff line change
Expand Up @@ -810,3 +810,70 @@ function overapproximate(cap::Intersection{N,<:AbstractPolyhedron,<:AbstractPoly
dirs::AbstractDirections; kwargs...) where {N}
return overapproximate_cap_helper(second(cap), first(cap), dirs; kwargs...)
end


"""
overapproximate(lm::LinearMap{N,S,NM,MAT},
::Type{<:SparsePolynomialZonotope}) where {N,
S<:SparsePolynomialZonotope{N},
NM,MAT<:MatrixZonotope{NM}}

Overapproximate the linear map of a sparse polynomial zonotope through a matrix zonotope,
following Proposition 2 in [HuangLBS2025](@citet).

### Input

- `lm` -- a linear map of a sparse polynomial zonotope through a matrix zonotope

### Output

A sparse polynomial zonotope overapproximating the linear map

"""
function overapproximate(lm::LinearMap{N,S,NM,MAT},
::Type{<:SparsePolynomialZonotope}) where {N,
S<:SparsePolynomialZonotope{N},
NM,MAT<:MatrixZonotope{NM}}
P = set(lm)
MZ = matrix(lm)
n = dim(P)
T = promote_type(N, NM)

SP = SparsePolynomialZonotope(center(P), genmat_dep(P), zeros(N, n, 0), expmat(P), indexvector(P))
Pd = linear_map(MZ, SP)

if ngens_indep(P) == 0
return Pd # fallback to linear_map
end

Z = Zonotope(zeros(T, n), genmat_indep(P))
Zi = overapproximate(MZ * Z, Zonotope)

return SparsePolynomialZonotope(center(Pd), genmat_dep(Pd), genmat(Zi), expmat(Pd), indexvector(Pd))
end

"""
overapproximate(lm::LinearMap{N,S,NM,MAT},
::Type{<:SparsePolynomialZonotope}) where {N,S<:SparsePolynomialZonotope{N},NM,
MAT<:MatrixZonotopeProduct{NM}}

Overapproximate the linear map of a sparse polynomial zonotope through a product of matrix zonotopes,
by recursively applying the overapproximation rule from the inside out.

### Input

- `lm` -- a linear map of a sparse polynomial zonotope through a `MatrixZonotopeProduct`
- `SparsePolynomialZonotope` -- target type

### Output

An overapproximation of the linear map as a sparse polynomial zonotope.
"""
function overapproximate(lm::LinearMap{N,S,NM,MAT},
T::Type{<:SparsePolynomialZonotope}) where {N,S<:SparsePolynomialZonotope{N},NM,
MAT<:MatrixZonotopeProduct{NM}}
MZs = factors(matrix(lm))
P = set(lm)
reduced = foldr((A, acc) -> overapproximate(A * acc, T), MZs; init=P)
return reduced
end
33 changes: 33 additions & 0 deletions test/Approximations/overapproximate.jl
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,39 @@ for N in @tN([Float64, Float32, Rational{Int}])
MZP = MZ2 * MZ
res2 = overapproximate(MZP * Z, Zonotope)
@test res2 == overapproximate(MZ2 * res, Zonotope)

# overapproximate the lm of a matrix zonotope with a SPZ
P = SparsePolynomialZonotope(N[1, -1], N[1 1; 0 -1], hcat(N[0, 1]), [2 1; 0 1; 1 0], [1, 2, 3])
res = overapproximate(MZ * P, SparsePolynomialZonotope)
@test center(res) == [0, -2]
@test genmat_dep(res) == hcat(N[1 0; -1 -2], N[1, -1], N[1 1; 1 -1])
@test genmat_indep(res) == hcat(N[1, 1], N[0, 2], N[0, 0])
@test expmat(res) == hcat([2 1; 0 1; 1 0], [1; 0; 0], [3 2; 0 1; 1 0])

# case: 0 gens matrix zonotope
MZ = MatrixZonotope(N[1 1; -1 1], Vector{Matrix{N}}())
res = overapproximate(MZ * P, SparsePolynomialZonotope)
@test res == linear_map(N[1 1; -1 1], P)

#case: id_mz ≠ id_spz
MZ = MatrixZonotope(N[1 1; -1 1], [N[1 0; 1 2]], [4])
res = overapproximate(MZ * P, SparsePolynomialZonotope)
@test center(res) == [0, -2]
@test genmat_dep(res) == hcat(N[1 0; -1 -2], N[1, -1], N[1 1; 1 -1])
@test genmat_indep(res) == hcat(N[1, 1], N[0, 2], N[0, 0])
@test expmat(res) == hcat([2 1; 0 1; 1 0; 0 0], [0, 0, 0, 1], [2 1; 0 1; 1 0; 1 1])

#case: matrix zonotope product
MZ2 = MatrixZonotope(N[1.1 0.9; -1.1 1.1], [N[1.1 -0.1; 0.9 2.1]])
res = overapproximate(MZ * MZ2 * P, SparsePolynomialZonotope)
P_in = overapproximate(MZ2 * P, SparsePolynomialZonotope)
@test res == overapproximate(MZ * P_in, SparsePolynomialZonotope)

#case: no ind generators
P = SparsePolynomialZonotope(N[1, -1], N[1 1; 0 -1], Matrix{N}(undef, 2, 0), [2 1; 0 1; 1 0],
[1, 2, 3])
res = overapproximate(MZ * P, SparsePolynomialZonotope)
@test res == linear_map(MZ, P) #test fallback
end

# tests that do not work with Rational{Int}
Expand Down
Loading