System Representations and Approximations

This module defines tools to represent and manipulate dynamical systems and their approximations.

Concrete Systems

The systems we aim to control are defined using types from external packages such as:

MathematicalSystems.jl for standard (e.g., continuous/discrete-time) control systems.
HybridSystems.jl for hybrid automata.

For example, a continuous-time system might be defined as:

concrete_system = MathematicalSystems.ConstrainedBlackBoxControlContinuousSystem(
    dynamics(),  # system dynamics (function)
    n_X,         # state dimension
    n_U,         # input dimension
    _X_,         # state constraints
    _U_          # input constraints
)

Symbolic/Abstract Systems

Symbolic models (used for abstraction-based control) are constructed separately using the symbolic abstraction module, typically resulting in a SymbolicModelList.

System Approximations

To reason about the system’s behavior during abstraction, we introduce approximations of the system's evolution. These are grouped into:

DiscreteTimeSystemApproximation
ContinuousTimeSystemApproximation

Both are subtypes of SystemApproximation, and can represent either underapproximations or overapproximations of the system dynamics.

Dionysos.System.SystemApproximation — Type

SystemApproximation

Abstract supertype for all system approximation types.

source

Dionysos.System.DiscreteTimeSystemApproximation — Type

DiscreteTimeSystemApproximation <: SystemApproximation

Abstract supertype for approximations of discrete-time systems.

source

Dionysos.System.ContinuousTimeSystemApproximation — Type

ContinuousTimeSystemApproximation <: SystemApproximation

Abstract supertype for approximations of continuous-time systems.

source

The following functions define the SystemApproximation interface:

get_system(approx::SystemApproximation): Returns the underlying concrete system.
is_continuous_time(approx): Returns true if the approximation is continuous-time, i.e., a ContinuousTimeSystemApproximation.
is_over_approximation(approx::SystemApproximation): Return true if approx is a DiscreteTimeSystemOverApproximation or a ContinuousTimeSystemOverApproximation.
discretize(approx::ContinuousTimeSystemApproximation, tstep)::DiscreteTimeSystemApproximation: Returns a DiscreteTimeSystemApproximation with given time step.
get_system_map(approx): Returns the map representing the system's evolution.

Underapproximations

These approximations guarantee that all returned trajectories are feasible under the system dynamics.

Dionysos.System.DiscreteTimeSystemUnderApproximation — Type

DiscreteTimeSystemUnderApproximation <: DiscreteTimeSystemApproximation

An abstract type representing an underapproximation of a discrete-time system.

source

Dionysos.System.ContinuousTimeSystemUnderApproximation — Type

ContinuousTimeSystemUnderApproximation <: ContinuousTimeSystemApproximation

An abstract type representing an underapproximation of a continuous-time system.

source

The following function define the underapproximation interface:

Dionysos.System.get_under_approximation_map — Function

get_under_approximation_map(approx::DiscreteTimeSystemUnderApproximation) -> Function

Returns a function that computes the underapproximation (list of points) of the system's evolution: f(rect::UT.HyperRectangle{N,T}, u::SVector{M,T}) -> SVector{N,T}[]

source

get_under_approximation_map(approx::ContinuousTimeSystemUnderApproximation) -> Function

Returns a function that computes the underapproximation (list of points) of the system's evolution: f(rect::UT.HyperRectangle{N,T}, u::SVector{M,T}, tstep::T) -> SVector{N,T}[]

source

Overapproximations

These approximations guarantee that the true system evolution is contained in the returned set, making them useful for safety and robust control.

Dionysos.System.DiscreteTimeSystemOverApproximation — Type

DiscreteTimeSystemOverApproximation <: DiscreteTimeSystemApproximation

An abstract type representing an overapproximation of a discrete-time system.

source

Dionysos.System.ContinuousTimeSystemOverApproximation — Type

ContinuousTimeSystemOverApproximation <: ContinuousTimeSystemApproximation

An abstract type representing an overapproximation of a continuous-time system.

source

The following function define the overapproximation interface:

Dionysos.System.get_over_approximation_map — Function

get_over_approximation_map(approx::DiscreteTimeSystemOverApproximation) -> Function

Returns a function that computes the overapproximation of the system's evolution: f(rect::UT.HyperRectangle{N,T}, u::SVector{M,T}) -> UT.HyperRectangle{N,T}

source

get_over_approximation_map(overApprox::ContinuousTimeSystemOverApproximation) -> Function

Returns a function that computes the overapproximation of the system's evolution: f(rect::UT.HyperRectangle{N,T}, u::SVector{M,T}, tstep::T) -> UT.HyperRectangle{N,T}

source

Concrete implementations of abstract approximation types

Dionysos.System.DiscreteTimeCenteredSimulation — Type

DiscreteTimeCenteredSimulation <: DiscreteTimeSystemUnderApproximation

A concrete underapproximation that simulates the evolution of the center of the input set under a discrete-time system.

This approximation is very conservative, returning a single propagated point from the center of the input set.

Fields

system: A constrained discrete-time control system (e.g., from MathematicalSystems.jl).

Underapproximation Map

Returns a function of the form: f(rect::HyperRectangle, u::SVector) -> Vector{SVector} which returns a singleton list with the propagated center point.

source

Dionysos.System.ContinuousTimeCenteredSimulation — Type

ContinuousTimeCenteredSimulation <: ContinuousTimeSystemUnderApproximation

A concrete underapproximation of a continuous-time system using center-point simulation.

Simulates only the center of the state set under the system dynamics. Returns a single propagated point after integration over a time step.

Fields

system: A constrained continuous-time control system.

Underapproximation Map

Returns a function of the form: f(rect::HyperRectangle, u::SVector, tstep::Real) -> Vector{SVector} which returns a singleton list with the propagated center point.

Notes

Use discretize to convert this approximation into a discrete-time approximation suitable for use in fixed-step abstraction pipelines.

source

Dionysos.System.DiscreteTimeRandomSimulation — Type

DiscreteTimeRandomSimulation <: DiscreteTimeSystemUnderApproximation

A stochastic underapproximation of a discrete-time system using random sampling.

Propagates multiple randomly sampled points from the input set to provide a discrete underapproximation of reachable states.

Fields

system: The underlying discrete-time control system.
nsamples: Number of samples to draw from the input set.

Underapproximation Map

Returns a function of the form: f(rect::HyperRectangle, u::SVector) -> Vector{SVector} which returns a list of propagated samples.

source

Dionysos.System.ContinuousTimeRandomSimulation — Type

ContinuousTimeRandomSimulation <: ContinuousTimeSystemUnderApproximation

A stochastic underapproximation for continuous-time systems using random point sampling.

Simulates multiple samples from the input set, over a fixed time step.

Fields

system: The underlying continuous-time control system.
nsamples: Number of random samples.

Underapproximation Map

Returns a function of the form: f(rect::HyperRectangle, u::SVector, tstep::Real) -> Vector{SVector} which returns a list of propagated samples.

Notes

Use discretize to convert this approximation into a discrete-time approximation suitable for use in fixed-step abstraction pipelines.

source

Dionysos.System.DiscreteTimeOverApproximationMap — Type

DiscreteTimeOverApproximationMap <: DiscreteTimeSystemOverApproximation

Concrete implementation of a discrete-time overapproximation of a dynamical system.

This type wraps a constrained discrete-time system along with an overapproximation map that, given a set of states and a control input, returns a conservative reachable set.

Fields

system: The underlying ConstrainedBlackBoxControlDiscreteSystem from MathematicalSystems.jl.
over_approximation_map: A function of the form f(rect::HyperRectangle, u::SVector) -> HyperRectangle which returns an overapproximated successor set.

source

Dionysos.System.ContinuousTimeSystemOverApproximationMap — Type

ContinuousTimeSystemOverApproximationMap <: ContinuousTimeSystemOverApproximation

Concrete implementation of a continuous-time overapproximation of a control system.

This type stores a constrained continuous-time system and an overapproximation function that simulates or bounds the system’s behavior over a given time step.

Fields

system: The underlying ConstrainedBlackBoxControlContinuousSystem from MathematicalSystems.jl.
over_approximation_map: A function of the form f(rect::HyperRectangle, u::SVector, tstep::Real) -> HyperRectangle which returns an overapproximated reachable set over the given time interval.

Notes

Use discretize to convert this approximation into a discrete-time overapproximation suitable for use in fixed-step abstraction pipelines.

source

Dionysos.System.DiscreteTimeGrowthBound — Type

DiscreteTimeGrowthBound <: DiscreteTimeSystemOverApproximation

A discrete-time overapproximation based on growth bounds.

Given a system and a growthbound_map, this approximation inflates the center trajectory by a radius that depends on the current state set's size and the input.

Fields

system: A ConstrainedBlackBoxControlDiscreteSystem from MathematicalSystems.jl.
growthbound_map: A function f(radius::SVector, u::SVector) -> SVector that computes how uncertainty in state evolves under the system.

Overapproximation Map

Returns a function of the form: f(rect::HyperRectangle, u::SVector) -> HyperRectangle This function simulates the image of the center and inflates it using the computed growth bound.

source

Dionysos.System.ContinuousTimeGrowthBound — Type

ContinuousTimeGrowthBound <: ContinuousTimeSystemOverApproximation

A continuous-time overapproximation based on growth bounds for reachable set propagation.

It estimates how uncertainty evolves through time using a growthbound_map which depends on the radius, input, and time step.

Fields

system: A ConstrainedBlackBoxControlContinuousSystem from MathematicalSystems.jl.
growthbound_map: A function f(radius::SVector, u::SVector, tstep::Real) -> SVector that estimates how uncertainty grows over a time step.

Overapproximation Map

Returns a function of the form: f(rect::HyperRectangle, u::SVector, tstep::Real) -> HyperRectangle This function simulates the image of the center and inflates it using the computed growth bound.

source

Dionysos.System.DiscreteTimeLinearized — Type

DiscreteTimeLinearized <: DiscreteTimeSystemOverApproximation

A discrete-time overapproximation based on linearization of the system dynamics.

This model approximates system behavior by propagating the linearized dynamics around the center of the state set and bounding the resulting error.

Fields

system: A ConstrainedBlackBoxControlDiscreteSystem from MathematicalSystems.jl.
linsys_map: A function (x, dx, u) -> (Fx, DFx) returning the linearized next state Fx and its Jacobian DFx around perturbation dx.
error_map: A function (radius, u) -> Δ returning a bound on the linearization error based on the set radius.

Overapproximation Map

Returns a function of the form: f(rect::HyperRectangle, u::SVector) -> HyperRectangle It evaluates the system at the center, adds linearized spread based on Jacobian, and inflates with the error bound.

source

Dionysos.System.ContinuousTimeLinearized — Type

ContinuousTimeLinearized <: ContinuousTimeSystemOverApproximation

A continuous-time overapproximation based on Runge-Kutta linearization of the system dynamics.

The method propagates both the nominal trajectory and its linearized sensitivity over a time step using a 4th-order Runge-Kutta scheme, while bounding the second-order remainder error.

Fields

system: A ConstrainedBlackBoxControlContinuousSystem from MathematicalSystems.jl.
linsys_map: A function (x, dx, u, tstep) -> (Fx, DFx) simulating a linearized trajectory and its Jacobian.
error_map: A function (r, u, tstep) -> Δ computing a bound on the nonlinearity-induced error over time.

Overapproximation Map

Returns a function of the form: f(rect::HyperRectangle, u::SVector, tstep::Real) -> HyperRectangle The result is a conservative reachable set from the center using linearization + second-order error correction.

source

Controller

So far, the abstraction-based methods that we use define either piecewise-constant or piecewise-affine controllers.

Dionysos.System.ConstantController — Type

ConstantController{T, VT}

encodes a constant state-dependent controller of the κ(x) = c.

source

Dionysos.System.AffineController — Type

AffineController{T, MT, VT1, VT2}

encodes an affine state-dependent controller of the κ(x) = K*(x-c)+ℓ.

source

Trajectories

Dionysos.System.DiscreteTrajectory — Type

DiscreteTrajectory{Q, TT}

q_0 is the starting mode and transitions is a sequence of discrete transitions in the system.

source

Dionysos.System.ContinuousTrajectory — Type

ContinuousTrajectory{T, XVT<:AbstractVector{T}, UVT<:AbstractVector{T}}

x is a sequence of points in the state space and u is a sequence of points in the input space.

source

Dionysos.System.HybridTrajectory — Type

HybridTrajectory{T, TT, XVT <: AbstractVector{T}, UVT <: AbstractVector{T}}

discrete is the discrete trajectory of type DiscreteTrajectory and continuous is a the continuous trajectory of type ContinuousTrajectory.

source

Dionysos.System.Trajectory — Type

Trajectory{T}

provides the sequence of some elements of a trajectory.

source

Dionysos.System.Control_trajectory — Type

Control_trajectory{T1, T2}

provides the sequence of states and inputs of a trajectory.

source

Dionysos.System.Cost_control_trajectory — Type

Cost_control_trajectory{T1, T2, T3}

provides the sequence of states, inputs (via Control_trajectory) and costs of a trajectory.

source