SparsePolynomialZonotope

LazySets.SparsePolynomialZonotopeModule.SparsePolynomialZonotopeType
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.
source

Operations

LazySets.API.centerMethod
center(P::SparsePolynomialZonotope)

Return the center of a sparse polynomial zonotope.

Input

  • P – sparse polynomial zonotope

Output

The center.

source
LazySets.expmatMethod
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.

source
LazySets.genmat_depMethod
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.

source
LazySets.genmat_indepMethod
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.

source
LazySets.SparsePolynomialZonotopeModule.indexvectorMethod
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.

source
LazySets.polynomial_orderMethod
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.

source
Base.randMethod
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.

source
LazySets.remove_redundant_generatorsMethod
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.
source
LazySets.API.linear_mapMethod
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.

source
LazySets.reduce_orderFunction
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.

source
LazySets.API.ρMethod
ρ(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.

source
LazySets.API.translateMethod
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.

source
LazySets.API.cartesian_productMethod
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.

source
LazySets.API.exact_sumMethod
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.

source
LazySets.API.minkowski_sumMethod
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.

source

Inherited from AbstractPolynomialZonotope:

Inherited from AbstractSparsePolynomialZonotope: