Reach-sets

Abstract interface

ReachabilityAnalysis.AbstractReachSetType
AbstractReachSet{N}

Abstract type for all reach-sets types.

Notes

A reach-set is a set representation X associated to a given time span Δt.

In its simplest form, we represent reach-sets with a struct that wraps the tuple (X, Δt), where X corresponds to a geometric set, eg. a polytope, and Δt is the interval with the time span associated to this reach-set.

This type is parametric in N. The parameter N represents for the type of numerical coefficient used in the representation (typically, N = Float64).

Although concrete subtypes of AbstractReachSet may represent the set X in different ways, or carry additional information as an extra type field, they should all implement the AbstractReachSet interface to enable shared functionality for reach-set types. In particular, each concrete subtype should implement the following methods:

  • set – return the geometric set
  • setrep – return the type of the set representation
  • tspan – return the time interval span
  • tstart – return the initial time
  • tend – return the final time
  • dim – return ambient dimension of the reach-set
source

The functions are available at the interface level.

ReachabilityAnalysis.basetypeMethod
basetype(T::Type{<:AbstractReachSet})

Return the base type of the given reach-set type (i.e., without type parameters).

Input

  • T – reach-set type, used for dispatch

Output

The base type of T.

source
LazySets.setMethod
set(R::AbstractReachSet)

Return the geometric set represented by this reach-set.

Input

  • R – reach-set

Output

The set wrapped by the given reach-set.

source
ReachabilityAnalysis.setrepMethod
setrep(R::AbstractReachSet)

Return the type of the set representation of this reach-set.

Input

  • R – reach-set

Output

Type of the set representation of the given reach-set.

source
ReachabilityAnalysis.tspanMethod
tspan(R::AbstractReachSet)

Return time span of this reach-set.

Input

  • R – reach-set

Output

The interval representing the time span of the given reach-set.

source
ReachabilityAnalysis.tstartMethod
tstart(R::AbstractReachSet)

Return the initial time of this reach-set.

Input

  • R – reach-set

Output

A float representing the initial time of the given reach-set.

source
ReachabilityAnalysis.tendMethod
tend(R::AbstractReachSet)

Return the final time of this reach-set.

Input

  • R – reach-set

Output

A float representing the final time of the given reach-set.

source
LazySets.dimMethod
dim(R::AbstractReachSet)

Return the ambient dimension of the reach-set.

Input

  • R – reach-set

Output

An integer corresponding to the ambient dimension of the given reach-set.

source
Base.copyMethod
copy(R::AbstractReachSet)

Return a copy of the given reach-set.

Input

  • R – reach-set

Output

A new reach-set of the sam type and the same field values as R.

source
ReachabilityAnalysis.shiftMethod
shift(fp::Flowpipe{N, <:AbstractReachSet}, t0::Number) where {N}

Return the time-shifted flowpipe by the given number.

Input

  • fp – flowpipe
  • t0 – time shift

Output

A new flowpipe such that the time-span of each constituent reach-set has been shifted by t0.

source
ReachabilityAnalysis.AbstractLazyReachSetType
AbstractLazyReachSet{N} <: AbstractReachSet{N}

Abstract type for all reach-set types that use a LazySet for the underlying set representation.

Notes

An AbstractLazyReachSet is the interface for reach-sets such that the geometric set is represented by any subtype of LazySet.

This types implements the LazySets interface, namely support function (ρ), support vector (σ) and ambient dimension (dim) functions. Hence, these functions directly apply to concrete subtypes of an AbstractLazyReachSet. The set wrapped by this type is obtained through set(R).

The following functions should be implemented by any concrete subtype:

  • reconstruct – create a new instance of the given reach-set with a different set representation but sharing the other fields, i.e. the same time span (and the same for other fields, if applicable)

In addition to the functions inherited from AbstractReachSet, the following are available:

  • linear_map – concrete linear map of a reach-set
  • project – projection of a reach-set
  • shift – time-shift of a reach-set
  • vars – tuple of integers associated to the variables of the given reach-set
source
LazySets.projectMethod
project(R::AbstractLazyReachSet, variables::NTuple{D,Int};
        check_vars::Bool=true) where {D}

Projects a reach-set onto the subspace spanned by the given variables.

Input

  • R – reach-set
  • vars – tuple of variables for the projection
  • check_vars – (optional, default: true) if true, check that the given variable indices vars are a subset of the variables of R

Output

A SparseReachSet whose variable indices are given by vars.

The type of the new reach-set depends on the type of the reach-set R:

  • If R contains a hyperrectangular set, the output is a hyperrectangle.
  • If R contains a zonotopic set, the output is a zonotope.
  • Otherwise, the return type is a polytope either in constraint representation or in vertex representation, depending on the dimension and the properties of M. For details, see LazySets.project.

Notes

This function can be used to project a reach-set onto a lower-dimensional sub-space. The projection is concrete, and it consists of mapping the reach-set X = set(R) to a new reach-set through to MX, where M is the projection matrix associated with the given variables vars.

To project onto the time variable, use the index 0. For instance, (0, 1) projects onto the time variable and the first variable in R.

source

Reachable set

ReachabilityAnalysis.ReachSetType
ReachSet{N, ST<:LazySet{N}} <: AbstractLazyReachSet{N}

Type that wraps a reach-set using a LazySet as underlying representation.

Fields

  • X – set
  • Δt – time interval

Notes

A ReachSet is a struct representing (an approximation of) the reachable states for a given time interval. The type of the representation is ST, which may be any subtype LazySet. For efficiency reasons, ST should be concretely typed.

By assumption the coordinates in this reach-set are associated to the integers 1, …, n. The function vars returns such tuple.

source

Sparse reachable set

ReachabilityAnalysis.SparseReachSetType
SparseReachSet{N, ST<:LazySet{N}, D} <: AbstractReachSet{N}

Type that wraps a reach-set using a LazySet as underlying representation, together with a tuple of variables associated to this reach-set.

Fields

  • X – set
  • Δt – time interval
  • vars – tuple of variable indices represented by the set X

Notes

A SparseReachSet is a struct representing (an approximation of) the reachable states for a given time interval. The type of the representation is ST, which may be any subtype of LazySet (ideally, concrete). Moreover, this type also stores information about the variables (also named coordinates, or by abuse of notation, dimensions) corresponding to the set X.

For instance in the ambient space n=5, one may have a SparseReachSet whose variables tuple is vars = (4, 5, 6), i.e. representing a three-dimensional projection of the full-dimensional reach-set. In consequence, the dimension of X doesn't match the length of vars, in general

In this type, the parameter N represents the numerical type of the LazySet (typically, Float64), the type ST represents the set representation used, and D denotes the dimension of this sparse reach set. Note that, in contrast to ReachSet, for SparseReachSet the number of dimensions is part of the type information.

source

Taylor model reach-sets

ReachabilityAnalysis.TaylorModelReachSetType
TaylorModelReachSet{N, S} <: AbstractTaylorModelReachSet{N}

Reach-set representation consisting of a vector of taylor models in one variable (the "time" variable) whose coefficients are multivariate polynomials (the "space" variables).

Notes

The parameters N and S refer to the numerical type of the representation (used for the Taylor model in time and Taylor series polynomials respectively). The space variables are assumed to be normalized to the interval [-1, 1]. It is assumed that the time domain is the same for all components.

source

Template reach-sets

ReachabilityAnalysis.TemplateReachSetType
TemplateReachSet{N, VN, TN<:AbstractDirections{N, VN}, SN<:AbstractVector{N}} <: AbstractLazyReachSet{N}

Reach set that stores the support function of a set at a give set of directions.

Notes

The struct has the following parameters:

  • N – refers to the numerical type of the representation.
  • VN – refers to the vector type of the template
  • TN – refers to the template type
  • SN – vector type that holds the support function evaluations

Concrete subtypes of AbstractDirections are defined in the LazySets library.

This reach-set implicitly represents a set by a set of directions and support functions. set(R::TemplateReachSet) returns a polyhedron in half-space representation.

Apart from the getter functions inherited from the AbstractReachSet interface, the following methods are available:

  • directions(R) – return the set of directions normal to the faces of this reach-set
  • support_functions(R) – return the vector of support function evaluations
  • support_functions(R, i) – return the i-th coordinate of the vector of support function evaluatons
source