Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add quadratic map for sspz #2990

Merged
merged 5 commits into from
Jul 15, 2022
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
1 change: 1 addition & 0 deletions docs/src/lib/sets/SimpleSparsePolynomialZonotope.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,4 +20,5 @@ cartesian_product(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZono
linear_combination(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
convex_hull(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
convex_hull(::SimpleSparsePolynomialZonotope)
quadratic_map(::Vector{MT}, ::SimpleSparsePolynomialZonotope) where {N, MT<:AbstractMatrix{N}}
```
54 changes: 53 additions & 1 deletion src/Sets/SimpleSparsePolynomialZonotope.jl
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
export SimpleSparsePolynomialZonotope, PolynomialZonotope, expmat, nparams,
linear_map
linear_map, quadratic_map

"""
SimpleSparsePolynomialZonotope{N, VN<:AbstractVector{N}, MN<:AbstractMatrix{N}, ME<:AbstractMatrix{<:Integer}} <: AbstractPolynomialZonotope{N}
Expand Down Expand Up @@ -152,3 +152,55 @@ The set resulting from applying the linear map `M` to `P`.
function linear_map(M::AbstractMatrix, P::SSPZ)
return SimpleSparsePolynomialZonotope(M * center(P), M * genmat(P), expmat(P))
end

"""
quadratic_map(Q::Vector{MT}, S::SimpleSparsePolynomialZonotope) where {N, MT<:AbstractMatrix{N}}

Return an overapproximation of the quadratic map of the given zonotope.
schillic marked this conversation as resolved.
Show resolved Hide resolved

### Input

- `Q` -- vector of square matrices
- `S` -- simple sparse polynomial zonotope

### Output

The quadratic map of the given zonotope represented as a polynomial zonotope.

### Algorithm

This method implements Proposition 12 in [1].
See also Proposition 3.1.30 in [2].

[1] N. Kochdumper, M. Althoff. *Sparse polynomial zonotopes: A novel set
representation for reachability analysis*. 2021
[2] N. Kochdumper. *Extensions of polynomial zonotopes and their application to
verification of cyber-physical systems*. 2021.
"""
function quadratic_map(Q::Vector{MT}, S::SimpleSparsePolynomialZonotope) where {N, MT<:AbstractMatrix{N}}
m = length(Q)
c = center(S)
h = ngens(S)
G = genmat(S)
E = expmat(S)

cnew = similar(c, m)
Gnew = similar(G, m, h^2 + h)
QiG = similar(Q)
@inbounds for (i, Qi) in enumerate(Q)
cnew[i] = dot(c, Qi, c)
Gnew[i, 1:h] = c' * (Qi + Qi') * G
QiG[i] = Qi * G
end

Enew = repeat(E, 1, h + 1)
@inbounds for i in 1:h
idxstart = h * i + 1
idxend = (i + 1) * h
Enew[:, idxstart:idxend] .+= E[:, i]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

E[:, i] and in other places it allocates, we could optimize but i think it's fine for now.

for j in eachindex(QiG)
Gnew[j, idxstart:idxend] = G[:, i]' * QiG[j]
end
end
return SimpleSparsePolynomialZonotope(cnew, Gnew, Enew)
end
12 changes: 12 additions & 0 deletions test/Sets/SimpleSparsePolynomialZonotope.jl
Original file line number Diff line number Diff line change
Expand Up @@ -53,4 +53,16 @@ for N in [Float64, Float32, Rational{Int}]
@test center(CH1) == _c
@test genmat(CH1) == _g
@test expmat(CH1) == _e

S2 = SimpleSparsePolynomialZonotope(N[0.2, -0.6], N[1 0;0 0.4], [1 0;0 1])
Q = [[0. 1;1 0], [-3.2 1.2;1.2 0]]

q1 = quadratic_map(Q, S2)

@test center(q1) ≈ [-0.24, -0.416]
@test genmat(q1) ≈ [-1.2 0.16 0.0 0.4 0.4 0.0;
-2.72 0.192 -3.2 0.48 0.48 0.0]

@test expmat(q1) == [ 1 0 2 1 1 0;
0 1 0 1 1 2]
end