SparsePolynomialZonotope

SparsePolynomialZonotope{N, VN<:AbstractVector{N}, MN<:AbstractMatrix{N},
                         MNI<:AbstractMatrix{N},
                         ME<:AbstractMatrix{Int},
                         VI<:AbstractVector{Int}}
    <: AbstractSparsePolynomialZonotope{N}

Type that represents a sparse polynomial zonotope.

A sparse polynomial zonotope $\mathcal{PZ} ⊂ ℝ^n$ is represented by the set

\[\mathcal{PZ} = \left\{x ∈ ℝ^n : x = c + ∑ᵢ₌₁ʰ\left(∏ₖ₌₁ᵖ α_k^{E_{k, i}} \right)Gᵢ+∑ⱼ₌₁^qβⱼGIⱼ,~~ α_k, βⱼ ∈ [-1, 1],~~ ∀ k = 1,…,p, j=1,…,q \right\},\]

where $c ∈ ℝ^n$ is the offset vector (or center), $Gᵢ ∈ ℝ^{n}$ are the dependent generators, $GIⱼ ∈ ℝ^{n}$ are the independent generators, and $E ∈ \mathbb{N}^{p×h}_{≥0}$ is the exponent matrix with matrix elements $E_{k, i}$.

In the implementation, $Gᵢ ∈ ℝ^n$ are arranged as columns of the dependent generator matrix $G ∈ ℝ^{n × h}$, and similarly $GIⱼ ∈ ℝ^{n}$ are arranged as columns of the independent generator matrix $GI ∈ ℝ^{n×q}$.

The shorthand notation $\mathcal{PZ} = ⟨ c, G, GI, E, idx ⟩$ is often used, where $idx ∈ \mathbb{N}^p$ is a list of non-repeated natural numbers storing a unique identifier for each dependent factor $αₖ$.

Fields

• c – offset vector
• G – dependent generator matrix
• GI – independent generator matrix
• E – exponent matrix
• idx – identifier vector of positive integers for the dependent parameters

Notes

Sparse polynomial zonotopes were introduced in [1].

• [1] N. Kochdumper and M. Althoff. Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis. Transactions on Automatic Control, 2021.

center(P::SparsePolynomialZonotope)

Return the center of a sparse polynomial zonotope.

Input

• P – sparse polynomial zonotope

Output

The center.

expmat(P::SparsePolynomialZonotope)

Return the matrix of exponents of the sparse polynomial zonotope.

Input

• P – sparse polynomial zonotope

Output

The matrix of exponents, where each column is a multidegree.

Notes

In the exponent matrix, each row corresponds to a parameter ($αₖ$ in the definition) and each column to a monomial.

genmat_dep(P::SparsePolynomialZonotope)

Return the matrix of dependent generators of a sparse polynomial zonotope.

Input

• P – sparse polynomial zonotope

Output

The matrix of dependent generators.

genmat_indep(P::SparsePolynomialZonotope)

Return the matrix of independent generators of a sparse polynomial zonotope.

Input

• P – sparse polynomial zonotope

Output

The matrix of independent generators.

indexvector(P::SparsePolynomialZonotope)

Return the index vector of a sparse polynomial zonotope.

Input

• P – sparse polynomial zonotope

Output

The index vector.

Notes

The index vector contains positive integers for the dependent parameters.

polynomial_order(P::SPZ)

Return the polynomial order of a sparse polynomial zonotope.

Input

• P – sparse polynomial zonotope

Output

The polynomial order.

Notes

The polynomial order is the maximum sum of all monomials' parameter exponents.

rand(::Type{SparsePolynomialZonotope}; [N]::Type{<:Real}=Float64,
     [dim]::Int=2, [nparams]::Int=2, [maxdeg]::Int=3,
     [num_dependent_generators]::Int=-1,
     [num_independent_generators]::Int=-1, [rng]::AbstractRNG=GLOBAL_RNG,
     [seed]::Union{Int, Nothing}=nothing)

Create a random sparse polynomial zonotope.

Input

• SparsePolynomialZonotope – type for dispatch
• N – (optional, default: Float64) numeric type
• dim – (optional, default: 2) dimension
• nparams – (optional, default: 2) number of parameters
• maxdeg – (optional, default: 3) maximum degree for each parameter
• num_dependent_generators – (optional, default: -1) number of dependent generators (see comment below)
• num_independent_generators – (optional, default: -1) number of independent generators (see comment below)
• rng – (optional, default: GLOBAL_RNG) random number generator
• seed – (optional, default: nothing) seed for reseeding

Output

A random sparse polynomial zonotope.

Algorithm

All numbers are normally distributed with mean 0 and standard deviation 1.

The number of generators can be controlled with the arguments num_dependent_generators and num_dependent_generators. For a negative value we choose a random number in the range dim:2*dim (except if dim == 1, in which case we only create a single generator). Note that the final number of generators may be lower if redundant monomials are generated.

remove_redundant_generators(S::SparsePolynomialZonotope)

Remove redundant generators from S.

Input

• S – sparse polynomial zonotope

Output

A new sparse polynomial zonotope where redundant generators have been removed.

Notes

The result uses dense arrays irrespective of the array type of S.

Algorithm

Let G be the dependent generator matrix, E the exponent matrix, and GI the independent generator matrix of S. We perform the following simplifications:

• Remove zero columns in G and the corresponding columns in E.
• Remove Zero columns in GI.
• For zero columns in E, add the corresponding column in G to the center.
• Group repeated columns in E together by summing the corresponding columns in G.

uniqueID(n::Int)

Return a collection of n unique identifiers (integers 1, …, n).

Input

• n – number of variables

Output

1:n.

linear_map(M::AbstractMatrix, P::SparsePolynomialZonotope)

Apply a linear map to a sparse polynomial zonotope.

Input

• M – square matrix with size(M) == dim(P)
• P – sparse polynomial zonotope

Output

The sparse polynomial zonotope resulting from applying the linear map.

reduce_order(P::SparsePolynomialZonotope, r::Real,
             [method]::AbstractReductionMethod=GIR05())

Overapproximate the sparse polynomial zonotope by another sparse polynomial zonotope with order at most r.

Input

• P – sparse polynomial zonotope
• r – maximum order of the resulting sparse polynomial zonotope (≥ 1)
• method – (optional default GIR05) algorithm used internally for the order reduction of a (normal) zonotope

Output

A sparse polynomial zonotope with order at most r.

Notes

This method implements the algorithm described in Proposition 3.1.39 of [1].

[1] Kochdumper, Niklas. Extensions of polynomial zonotopes and their application to verification of cyber-physical systems. PhD diss., Technische Universität München, 2022.

ρ(d::AbstractVector, P::SparsePolynomialZonotope; [enclosure_method]=nothing)

Bound the support function of $P$ in the direction $d$.

Input

• d – direction
• P – sparse polynomial zonotope
• enclosure_method – (optional; default: nothing) method to use for enclosure; an AbstractEnclosureAlgorithm from the Rangeenclosures.jl package

Output

An overapproximation of the support function in the given direction.

Algorithm

This method implements Proposition 3.1.16 in [1].

[1] Kochdumper, Niklas. Extensions of polynomial zonotopes and their application to verification of cyber-physical systems. PhD diss., Technische Universität München, 2022.

translate(S::SparsePolynomialZonotope, v::AbstractVector)

Translate (i.e., shift) a sparse polynomial zonotope by a given vector.

Input

• S – sparse polynomial zonotope
• v – translation vector

Output

A translated sparse polynomial zonotope.

cartesian_product(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)

Compute the Cartesian product of two sparse polynomial zonotopes.

Input

• P1 – sparse polynomial zonotope
• P2 – sparse polynomial zonotope

Output

The Cartesian product of P1 and P2.

Algorithm

This method implements Proposition 3.1.22 in [1].

[1] Kochdumper, Niklas. Extensions of polynomial zonotopes and their application to verification of cyber-physical systems. PhD diss., Technische Universität München, 2022.

exact_sum(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)

Compute the exact sum of sparse polyomial zonotopes $P₁$ and $P₂$.

Input

• P1 – sparse polynomial zonotope
• P2 – sparse polynomial zonotope

Output

A SparsePolynomialZonotope representing the exact sum $P₁ ⊞ P₂$.

Algorithm

This method implements Proposition 3.1.20 in [1].

[1] Kochdumper, Niklas. Extensions of polynomial zonotopes and their application to verification of cyber-physical systems. PhD diss., Technische Universität München, 2022.

minkowski_sum(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)

Compute the Minkowski sum of two sparse polyomial zonotopes.

Input

• P1 – sparse polynomial zonotope
• P2 – sparse polynomial zonotope

Output

The Minkowski sum of P1 and P2.

Algorithm

See Proposition 3.1.19 in [1].

[1] Kochdumper. Extensions of polynomial zonotopes and their application to verification of cyber-physical systems. PhD diss., TU Munich, 2022.