Dynamics

DiscreteTimeStochasticDynamics

Abstract type for discrete-time stochastic dynamicss, i.e. $x_{k+1} = f(x_k, u_k, w_k)$.

dimstate(dyn::DiscreteTimeStochasticDynamics)

Return the dimension of the state space of the dynamics dyn.

diminput(dyn::DiscreteTimeStochasticDynamics)

Return the dimension of the input space of the dynamics dyn.

System{D<:DiscreteTimeStochasticDynamics, I<:LazySet}

A struct representing a system with dynamics and an initial set.

dynamics(sys::System)

Return the dynamics of the system.

initial(sys::System)

Return the initial set of the system.

AdditiveNoiseDynamics

Dynamics with additive noise, i.e. $x_{k+1} = f(x_k, u_k) + w_k$ with some i.i.d. noise structure $w_k$.

nominal

Compute the reachable set under the nominal dynamics of the dynamics dyn over the state region X and control u. The nominal dynamics are given by $\hat{x}_{k+1} = f(x_k, u_k)$, which implies that nominal dynamics are only well-defined for additive noise dynamics. Since for some non-linear dynamics, no analytical formula exists for the one-step reachable set under the nominal dynamics, the function nominal only guarantees that the returned set is a superset of the one-step true reachable set, i.e. an over-approximation.

Note that for NonlinearAdditiveNoiseDynamics, you must first call prepare_nominal before calling nominal. If the method is called with a single state x::Vector{<:Real}, it is not necessary to call prepare_nominal first.

prepare_nominal

The need for this method is a result of using TaylorModels.jl for the over-approximation of the reachable set under non-linear nominal dynamics. This package relies on global variables to store the variables of the Taylor models, which can be problematic when using multi-threading. Furthermore, when setting the variables, it invalidates existing Taylor models. Therefore, before entering the loop of abstraction to compute the transition probability bounds for all regions, we call this method to set up the global state appropriately.

This method is a no-op for dynamics that are not NonlinearAdditiveNoiseDynamics.

Eventually, we hope to remove the need for this method by using a more thread-safe library for Taylor models, e.g. akin to MultivariatePolynomials.jl.

noise

For additive dynamics $x_{k+1} = f(x_k, u_k) + w_k$, return $w_k$ as a struct. See AdditiveNoiseStructure for implementations.

AffineAdditiveNoiseDynamics

A struct representing dynamics with additive noise. That is, $x_{k+1} = A x_k + B u_k + C + w_k$, where $w_k ~ p_w$ and $p_w$ is multivariate probability distribution.

Fields

• A::AbstractMatrix{Float64}: The linear state matrix.
• B::AbstractMatrix{Float64}: The control input matrix.
• C::AbstractMatrix{Float64}: The constant drift vector.
• w::AdditiveNoiseStructure: The additive noise.

Examples

A = [1.0 0.1; 0.0 1.0]
B = [0.0; 1.0]

w_stddev = [0.1, 0.1]
w = AdditiveDiagonalGaussianNoise(w_stddev)

# If no C is provided, it is assumed to be zero.
dyn = AffineAdditiveNoiseDynamics(A, B, w)

NonlinearAdditiveNoiseDynamics

A struct representing continuous non-linear dynamics with additive noise. That is, $x_{k+1} = f(x_k, u_k) + w_k$, where $f(\cdot, u_k)$ is continuously differentiable function for each $u_k \in U$ and $w_k \sim p_w$ and $p_w$ is multivariate probability distribution.

Fields

• f::Function: A function taking x::Vector and u::Vector as input and returns a Vector of the dynamics output.
• nstate::Int: The state dimension.
• ninput::Int: The input dimension.
• w::AdditiveNoiseStructure: The additive noise.

Examples

# Stochastic Van der Pol Oscillator with additive uniform noise, but no inputs.
τ = 0.1
f(x, u) = [x[1] + x[2] * τ, x[2] + (-x[1] + (1 - x[1])^2 * x[2]) * τ]

w_stddev = [0.1, 0.1]
w = AdditiveCentralUniformNoise(w_stddev)

dyn = NonlinearAdditiveNoiseDynamics(f, 2, 0, w)

PiecewiseNonlinearAdditiveNoiseDynamics

A struct representing non-linear dynamics with additive noise. That is, $x_{k+1} = f(x_k, u_k) + w_k$, where $f(\cdot, u_k)$ is piecewise continuously differentiable function for each $u_k \in U$ and $w_k \sim p_w$ and $p_w$ is multivariate probability distribution.

Fields

• regions::Vector{<:NonlinearDynamicsRegion}: A list of NonlinearDynamicsRegion to represent the piecewise dynamics.
• nstate::Int: The state dimension.
• ninput::Int: The input dimension.
• w::AdditiveNoiseStructure: The additive noise.

Examples

τ = 0.1

region1 = Hyperrectangle(low=[-1.0, -1.0], high=[0.0, 1.0])
f(x, u) = [x[1] + x[2] * τ, x[2] + (-x[1] + (1 - x[1])^2 * x[2]) * τ]
dyn_reg1 = NonlinearDynamicsRegion(f, region1)

region2 = Hyperrectangle(low=[0.0, -1.0], high=[1.0, 1.0])
g(x, u) = [x[1] + x[2] * τ, x[2] + (-x[2] + (1 - x[2])^2 * x[1]) * τ]
dyn_reg2 = NonlinearDynamicsRegion(g, region2)

w_stddev = [0.1, 0.1]
w = AdditiveDiagonalGaussianNoise(w_stddev)

dyn = PiecewiseNonlinearAdditiveNoiseDynamics([dyn_reg1, dyn_reg2], 2, 0, w)

NonlinearDynamicsRegion

A struct representing a non-linear dynamics, valid over a region.

UncertainPWAAdditiveNoiseDynamics

A struct representing uncertain PWA dynamics with additive noise. That is, $x_{k+1} = A_{iu}(\alpha) x_k + C_{iu}(\alpha) + w_k$, where $x_k \in X_i$ is the state, $A_{iu}(\alpha) = \alpha \underline{A}_{iu} + (1 - \alpha) \overline{A}_{iu}$ and $C_{iu}(\alpha) = \alpha \underline{C}_{iu} + (1 - \alpha) \overline{C}_{iu}$ with $\alpha \in [0, 1]$ is the dynamics for region $X_i$ under control action $u$, and $w_k \sim p_w$ is the additive noise where $p_w$ is multivariate probability distribution.

Fields

• dimstate::Int: The dimension of the state space.
• dynregions::Vector{Vector{<:UncertainAffineRegion}: A list (action) of lists (regions) of UncertainAffineRegion to represent the uncertain PWA dynamics.
• w::AdditiveNoiseStructure: The additive noise.

UncertainAffineRegion

A struct representing an uncertain affine transition, valid over a region. That is, $A(\alpha) x + C(\alpha)$ where $A(\alpha) = \alpha \underline{A} + (1 - \alpha) \overline{A}$ and $C(\alpha) = \alpha \underline{C} + (1 - \alpha) \overline{C}$ for $\alpha \in [0, 1]$, valid over a region $X$.

Fields

• region::LazySet{Float64}: The region over which the affine transition is valid.
• Alower::AbstractMatrix{Float64}: The linear lower bound matrix.
• Clower::AbstractVector{Float64}: The constant lower bound vector.
• Aupper::AbstractMatrix{Float64}: The linear upper bound matrix.
• Cupper::AbstractVector{Float64}: The constant upper bound vector.

AdditiveNoiseStructure

Structure to represent the noise of additive noise dynamics. See AdditiveDiagonalGaussianNoise and AdditiveCentralUniformNoise for concrete types.

AdditiveDiagonalGaussianNoise

Additive diagonal Gaussian noise structure with zero mean, i.e. $w_k \sim \mathcal{N}(0, \mathrm{diag}(\sigma))$. Zero mean is without loss of generality, since the mean can be absorbed into the nominal dynamics.

AdditiveGaussianNoise

Additive Gaussian noise structure with zero mean, i.e. $w_k \sim \mathcal{N}(0, \mathrm{diag}(\sigma))$. Zero mean is without loss of generality, since the mean can be absorbed into the nominal dynamics.

AdditiveCentralUniformNoise

Additive diagonal uniform noise structure, i.e. $w_k \sim \mathcal{U}(-r, r)$. This is without loss of generality, since the mean can be absorbed into the nominal dynamics. That is, $w_k \sim \mathcal{U}(a, b)$ is equivalent to $c + w_k$ where $w_k \sim \mathcal{U}(-r, r)$ with $c = (a + b) / 2$ and $r = (b - a) / 2$, such that $c$ can be absorbed into the nominal dynamics.

AbstractedGaussianProcess

A struct representing bounds on the mean and stddev of a Gaussian process for each region over a partitioned space.

Fields

• dyn::Vector{Vector{<:AbstractedGaussianProcessRegion}}: A list (action) of lists (regions) of AbstractedGaussianProcessRegion`.

AbstractedGaussianProcessRegion

A struct representing an bounds on the mean and stddev of a Gaussian process over a region $X_i$. That is, $\underline{\mu}_{i} \leq \mu(x) \leq \overline{\mu}_{i}$ and $\underline{\Sigma}_{i,ll} \leq \Sigma(x)_{i,ll} \leq \overline{\Sigma}_{i,ll}$ for all $x \in X_i$ and each axis $l$.

Fields

• region::LazySet{Float64}: The region over which the affine transition is valid.
• mean_lower::AbstractVector{Float64}: The linear lower bound vector.
• mean_upper::AbstractVector{Float64}: The constant lower bound vector.
• stddev_lower::AbstractVector{Float64}: The linear upper bound vector.
• stddev_upper::AbstractVector{Float64}: The constant upper bound vector.

gp_bounds(dyn::AbstractedGaussianProcess, X::LazySet, input::Int)

Return the bounds on the mean and stddev of the Gaussian process for a given state region X and control action input. The return type is an AbstractedGaussianProcessRegion.

If the state region is not in the domain of the dynamics, an ArgumentError is thrown.

gp_bounds(dyn::AbstractedGaussianProcess, x::Vector{<:Real}, input::Int)

Return the bounds on the mean and stddev of the Gaussian process for a given state x and control action input. The return type is an AbstractedGaussianProcessRegion.

If the state is not in the domain of the dynamics, an ArgumentError is thrown.

region(abstracted_region::AbstractedGaussianProcessRegion)

Return the region over which the Gaussian process bounds are valid.

mean_lower(abstracted_region::AbstractedGaussianProcessRegion, i)

Return the lower bound on the mean of the Gaussian process for axis i.

mean_upper(abstracted_region::AbstractedGaussianProcessRegion, i)

Return the upper bound on the mean of the Gaussian process for axis i.

stddev_lower(abstracted_region::AbstractedGaussianProcessRegion, i)

Return the lower bound on the stddev of the Gaussian process for axis i.

stddev_upper(abstracted_region::AbstractedGaussianProcessRegion, i)

Return the upper bound on the stddev of the Gaussian process for axis i.

StochasticSwitchedDynamics

A type that represents dynamics with a stochastic transition between the modes. When abstracting stochastic switched dynamics, the transition probability bounds are computed individually for each mode and then combined using the weights.