BOX{N, AM, S, D, R} <: AbstractContinuousPost

Implementation of a reachability method for linear systems using box approximations.


  • δ – step-size of the discretization
  • approx_model – (optional, default: Forward) approximation model; see Notes below for possible options
  • static
  • dim – (optional default: missing) ambient dimension
  • recursive – (optional default: false) if true, use the implementation that recursively computes each reach-set; otherwise, use the implementation that unwraps the sequence until the initial set


The type fields are:

  • N – number type of the step-size
  • AM – approximation model
  • S – value type for the static option
  • D – value type for the dimension
  • R – value type for the recursive option

The default approximation model is:

Forward(sih=:concrete, exp=:base, setops=:lazy)

This algorithm solves the set-based recurrence equation $X_{k+1} = ΦX_k ⊕ V_k$ by computing a tight hyperrectangular over-approximation of $X_{k+1}$ at each step $k ∈ \mathbb{N}$. The recursive implementation uses the previously computed set $X_k$ to compute $X_{k+1}$. However, it is known that this method incurs wrapping effects. The non-recursive implementation instead computes $X_{k+1}$ by unwrapping the discrete recurrence until $X_0 = Ω₀$, at the expense of computing powers of the matrix $Φ$. These ideas are discussed in [BFFPSV18].


This algorithm is essentially a non-decomposed version of the method in [BFFPSV18], using hyperrectangles as set representation. For a general introduction we refer to the dissertation [LG09].

Regarding the approximation model, by default we use an adaptation of the method presented in [FRE11].