Dynamics
General
IntervalMDPAbstractions.DiscreteTimeStochasticDynamics — TypeDiscreteTimeStochasticDynamicsAbstract type for discrete-time stochastic dynamicss, i.e. $x_{k+1} = f(x_k, u_k, w_k)$.
IntervalMDPAbstractions.dimstate — Functiondimstate(dyn::DiscreteTimeStochasticDynamics)Return the dimension of the state space of the dynamics dyn.
IntervalMDPAbstractions.diminput — Functiondiminput(dyn::DiscreteTimeStochasticDynamics)Return the dimension of the input space of the dynamics dyn.
IntervalMDPAbstractions.System — TypeSystem{D<:DiscreteTimeStochasticDynamics, I<:LazySet}A struct representing a system with dynamics and an initial set.
IntervalMDPAbstractions.dynamics — Functiondynamics(sys::System)Return the dynamics of the system.
IntervalMDPAbstractions.initial — Functioninitial(sys::System)Return the initial set of the system.
Additive noise systems
IntervalMDPAbstractions.AdditiveNoiseDynamics — TypeAdditiveNoiseDynamicsDynamics with additive noise, i.e. $x_{k+1} = f(x_k, u_k) + w_k$ with some i.i.d. noise structure $w_k$.
IntervalMDPAbstractions.nominal — FunctionnominalCompute 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.
IntervalMDPAbstractions.prepare_nominal — Functionprepare_nominalThe 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.
IntervalMDPAbstractions.noise — FunctionnoiseFor additive dynamics $x_{k+1} = f(x_k, u_k) + w_k$, return $w_k$ as a struct. See AdditiveNoiseStructure for implementations.
IntervalMDPAbstractions.AffineAdditiveNoiseDynamics — TypeAffineAdditiveNoiseDynamicsA 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)IntervalMDPAbstractions.NonlinearAdditiveNoiseDynamics — TypeNonlinearAdditiveNoiseDynamicsA struct representing dynamics with additive noise. That is, $x_{k+1} = f(x_k, u_k) + w_k$, where $w_k \sim p_w$ and $p_w$ is multivariate probability distribution.
The nominal dynamics of this class are assumed to be infinitely differentiable, i.e. the Taylor expansion of the dynamics function f is well-defined. This is because to over-approximate the one-step reachable set, we rely on Taylor models, which are Taylor expansions + a remainder term. If you are dealing wit a non-differentiable dynamics function, consider using UncertainPWAAdditiveNoiseDynamics instead. To obtain an UncertainPWAAdditiveNoiseDynamics, you can partitoned the state space and use Linear Bound Propagation with each region (see bound_propagation).
Before calling nominal with a LazySet as input, you must call prepare_nominal. This is because the TaylorSeries.jl package modifies its global state. If you are using multi-threading, prepare_nominal must be called before entering the threaded section.
Fields
f::Function: A function takingx::Vectorandu::Vectoras input and returns aVectorof 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 = AdditiveDiagonalUniformNoise(w_stddev)
dyn = NonlinearAdditiveNoiseDynamics(f, 2, 0, w)IntervalMDPAbstractions.UncertainPWAAdditiveNoiseDynamics — TypeUncertainPWAAdditiveNoiseDynamicsA 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) ofUncertainAffineRegionto represent the uncertain PWA dynamics.w::AdditiveNoiseStructure: The additive noise.
IntervalMDPAbstractions.UncertainAffineRegion — TypeUncertainAffineRegionA 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.
Additive noise structures
IntervalMDPAbstractions.AdditiveNoiseStructure — TypeAdditiveNoiseStructureStructure to represent the noise of additive noise dynamics. See AdditiveDiagonalGaussianNoise and AdditiveCentralUniformNoise for concrete types.
IntervalMDPAbstractions.AdditiveDiagonalGaussianNoise — TypeAdditiveDiagonalGaussianNoiseAdditive 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.
IntervalMDPAbstractions.AdditiveCentralUniformNoise — TypeAdditiveCentralUniformNoiseAdditive 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.
Abstracted Gaussian processes
IntervalMDPAbstractions.AbstractedGaussianProcess — TypeAbstractedGaussianProcessA 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) ofAbstractedGaussianProcessRegion`.
IntervalMDPAbstractions.AbstractedGaussianProcessRegion — TypeAbstractedGaussianProcessRegionA 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.
IntervalMDPAbstractions.gp_bounds — Functiongp_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.
IntervalMDPAbstractions.region — Functionregion(abstracted_region::AbstractedGaussianProcessRegion)Return the region over which the Gaussian process bounds are valid.
IntervalMDPAbstractions.mean_lower — Functionmean_lower(abstracted_region::AbstractedGaussianProcessRegion, i)Return the lower bound on the mean of the Gaussian process for axis i.
IntervalMDPAbstractions.mean_upper — Functionmean_upper(abstracted_region::AbstractedGaussianProcessRegion, i)Return the upper bound on the mean of the Gaussian process for axis i.
IntervalMDPAbstractions.stddev_lower — Functionstddev_lower(abstracted_region::AbstractedGaussianProcessRegion, i)Return the lower bound on the stddev of the Gaussian process for axis i.
IntervalMDPAbstractions.stddev_upper — Functionstddev_upper(abstracted_region::AbstractedGaussianProcessRegion, i)Return the upper bound on the stddev of the Gaussian process for axis i.
Stochastic switched systems
IntervalMDPAbstractions.StochasticSwitchedDynamics — TypeStochasticSwitchedDynamicsA 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.