Systems

normalize(system::AbstractSystem)

Transform a mathematical system to a normalized (or canonical) form.

Input

• system – system; it can be discrete or continuous

Output

Either the same system if it already conforms to a canonical form, or a new system otherwise.

Notes

The normalization procedure consists of transforming a given system type into a "canonical" format that is used internally. More details are given below.

Algorithm

The implementation of normalize exploits MathematicalSystems's' types, which carry information about the problem as a type parameter.

Homogeneous ODEs of the form $x' = Ax, x ∈ \mathcal{X}$ are canonical if the associated problem is a ConstrainedLinearContinuousSystem and A is a matrix. This type does not handle non-deterministic inputs.

Note that a LinearContinuousSystem does not consider constraints on the state-space (such as an invariant); to specify state constraints, use a ConstrainedLinearContinuousSystem. If the passed system is a LinearContinuousSystem (i.e. no constraints) then the normalization fixes a universal set (Universe) as the constraint set.

The generalization to canonical systems with constraints and possibly time-varying non-deterministic inputs is considered next. These systems are of the form $x' = Ax + u, u ∈ \mathcal{U}, x ∈ \mathcal{X}$. The system type is ConstrainedLinearControlContinuousSystem, where A is a matrix, X is a set and U is an input, that is, any concrete subtype of AbstractInput.

If U is not given as an input, normalization accepts either a LazySet, or a vector of LazySets. In these cases, the sets are wrapped around an appropriate concrete input type.

If the system does not conform to a canonical form, the implementation tries to make the transformation; otherwise an error is thrown. In particular, ODEs of the form $x' = Ax + Bu$ are mapped into $x' = Ax + u, u ∈ B\mathcal{U}$, where now $u$ has the same dimensions as $x$.

The transformations described above are analogous in the discrete case, i.e. $x_{k+1} = A x_k$ and $x_{k+1} = Ax_{k} + u_k, u_k ∈ \mathcal{U}, x_k ∈ \mathcal{X}$ for the linear and affine cases respectively.

normalize(ivp::InitialValueProblem)

Transform an initial-value problem into a normalized (or canonical) form.

Input

• ivp – initial-value problem

Output

Either the same initial-value problem if it already conforms to a canonical form, or a new one otherwise.

Notes

This function extends normalize for initial-value problems.

add_dimension(A::AbstractMatrix, m=1)

Append one or more zero rows and columns to a matrix.

Input

• A – matrix
• m – (optional, default: 1) the number of extra dimensions

Examples

julia> using ReachabilityAnalysis: add_dimension

julia> A = [0.4 0.25; 0.46 -0.67]
2×2 Matrix{Float64}:
 0.4    0.25
 0.46  -0.67

julia> add_dimension(A)
3×3 Matrix{Float64}:
 0.4    0.25  0.0
 0.46  -0.67  0.0
 0.0    0.0   0.0

To append more than one zero row-column, use the second argument m:

julia> add_dimension(A, 2)
4×4 Matrix{Float64}:
 0.4    0.25  0.0  0.0
 0.46  -0.67  0.0  0.0
 0.0    0.0   0.0  0.0
 0.0    0.0   0.0  0.0

add_dimension(X::LazySet, m=1)

Adds an extra dimension to a LazySet through a Cartesian product.

Input

• X – a lazy set
• m – (optional, default: 1) the number of extra dimensions

Examples

julia> using ReachabilityAnalysis: add_dimension

julia> X = BallInf(ones(9), 0.5);

julia> dim(X)
9

julia> Xext = add_dimension(X);

julia> dim(Xext)
10

julia> X = ZeroSet(4);

julia> dim(add_dimension(X))
5

julia> typeof(X)
ZeroSet{Float64}

More than one dimension can be added passing the second argument:

julia> Xext = add_dimension(BallInf(zeros(10), 0.1), 4);

julia> dim(Xext)
14

Notes

In the special case that the given set is a zero set, instead of cartesian product a new zero set with extended dimensions is returned.

add_dimension(ivp::IVP, m=1)

Adds an extra dimension to a initial-value system.

Input

• ivp – initial-value system
• m – (optional, default: 1) the number of extra dimensions

Examples

julia> using MathematicalSystems, SparseArrays

julia> using ReachabilityAnalysis: add_dimension

julia> A = sprandn(3, 3, 0.5);

julia> X0 = BallInf(zeros(3), 1.0);

julia> s = InitialValueProblem(LinearContinuousSystem(A), X0);

julia> sext = add_dimension(s);

julia> statedim(sext)
4

If there is an input set, it is also extended:

julia> using LinearAlgebra

julia> using ReachabilityAnalysis.DiscretizationModule: next_set

julia> U = ConstantInput(Ball2(ones(3), 0.1));

julia> s = InitialValueProblem(ConstrainedLinearControlContinuousSystem(A, Matrix(1.0I, size(A)), nothing, U), X0);

julia> sext = add_dimension(s);

julia> statedim(sext)
4

julia> dim(next_set(inputset(sext)))
4

Extending a system with a varying input set:

If there is an input set, it is also extended:

julia> U = VaryingInput([Ball2(ones(3), 0.1 * i) for i in 1:3]);

julia> s = InitialValueProblem(ConstrainedLinearControlContinuousSystem(A, Matrix(1.0I, size(A)), nothing, U), X0);

julia> sext = add_dimension(s);

julia> statedim(sext)
4

julia> dim(next_set(inputset(sext), 1))
4

Extending a varying input set with more than one extra dimension:

julia> sext = add_dimension(s, 7);

julia> statedim(sext)
10

julia> dim(next_set(inputset(sext), 1))
10

homogenize(ivp::IVP{CLCCS{N,MT,IdentityMultiple{N},XT,ConstantInput{SI}},ST}) where {N, MT<:AbstractMatrix{N}, XT<:LazySet{N}, SI<:Singleton{N}, ST<:LazySet{N}}

Transform an inhomogeneous linear initial-value problem into an homogeneous one by introducing auxiliary state variables.

Input

• ivp – initial-value problem

Output

Homogeneous initial-value problem.

Notes

This function transforms the canonical initial-value problem $x' = Ax + u$, $x ∈ X$ with $u(0) ∈ U = {u}$ (a singleton) into an homogeneous problem without inputs $y' = Â * y$, $y ∈ Y$.

homogenize(sys::SOACS)

Transform an inhomogeneous second order system into an homogeneous one by introducing auxiliary state variables.

Input

• sys – second order system

Output

First-order homogeneous system.

Notes

This function transforms the second-order system $Mx'' + Cx' + Kx = b$ into a first-order, homogeneous one, $y' = Â * y$. It is assumed that the matrix $M$ is invertible.

HACLD1{T<:AbstractSystem, MT, N, J} <: AHACLD

Single-mode hybrid automaton with clocked linear dynamics.

Fields

• sys – system
• rmap – reset map
• Tsample – sampling time
• ζ – jitter
• switching – (optional) value that

Notes

This type is parametric in:

• T – system type
• MT – type of the reset map
• N – numeric type, applies to the sampling time and jitter
• J – type associated to the jitter

The type associated to the jitter, J, can be one of the following:

• Missing – no jitter, i.e. switchings are deterministic
• Number – symmetric jitter, i.e. non-deterministic switchings occur in the intervals [Tsample - ζ, Tsample + ζ]
• IA.Interval – non-symmetric jitter, i.e. non-deterministic switchings occur in the intervals [Tsample + inf(ζ), Tsample + sup(ζ)]; note that the infimum is expected to be negative for most use cases, i.e. when the jitter interval is centered at zero

The following getter functions are available:

• initial_state – initial state of the continuous mode
• jitter – return the jitter
• reset_map – return the reset map
• sampling_time – return the sampling time
• statedim – dimension of the state-space
• system – return the continuous mode
• switching – return the type of switching

Non-deterministic switching:

tstart Ts-ζ⁻ tend [––––––-|––––––-]

In the following, suppose that the continuous post-operator has fixed step-size δ > 0. If F denotes the flowpipe, then

F[1] F[2] F[3] F[4] F[5] F[k] [–––][–––][–––][–––][–––] ⋅ ⋅ ⋅ ⋅ ⋅ ⋅ ⋅ ⋅ [–––]

R = array(F) denote the array of reach-sets time-span for reach reach-set is of the form:

Similarly we compute tstart and tend for the supremum part Ts-ζ⁺

DiscreteTransition{RT, GT, IT⁻, IT⁺, WT} <: AbstractTransition

Type that encodes a discrete transition with an affine assignment of the form:

\[ post_d(X) = (R(X ∩ G ∩ I⁻) ⊕ W) ∩ I⁺\]

where $I⁻$ and $I⁺$ are invariants at the source and the target locations respectively, $G ⊆ \mathbb{R}^n$ is the guard set of the transition, the assignment is of the form $x^+ := Rx + w$, $w ∈ W$, $x^+ ∈ \mathbb{R}^m$ are the values after the transition, $R ∈ \mathbb{R}^{m\times n}$ is the assignment map (or reset map) and $W ⊆ \mathbb{R}^m$ is a closed and bounded convex set of non-deterministic inputs.

Fields

• R – assignment map
• W – non-deterministic inputs
• G – guard set of the transition from the source location to the target location
• I⁻ – invariant at the source location
• I⁺ – invariant at the target location

constrained_dimensions(HS::HybridSystem)::Dict{Int,Vector{Int}}

For each location, compute all dimensions that are constrained in the invariant or the guard of any outgoing transition.

Input

• HS – hybrid system

Output

A dictionary mapping (::Dict{Int,Vector{Int}}) the index of each location $ℓ$ to the dimension indices that are constrained in $ℓ$.