System

AbstractAffineApproximationProvider

Supertype of the strategies producing local affine approximations of the dynamics; see build_affine_approximation.

AffineApproximation

Result of build_affine_approximation: the local affine system (MathematicalSystems.NoisyConstrainedAffineControlDiscreteSystem), the lipschitz bounds on the linearization error over the local domain, the Uformat/Wformat matrices consumed by the transition-synthesis LMIs, and a provider-specific summary NamedTuple.

AffineController(map::MathematicalSystems.AffineMap)

Static state feedback u = A·x + c (plain data). Wrap a transition-synthesis result with as_controller to simulate it in a closed loop.

AnalyticAffineApproximationProvider(; A, B, f, lipschitz, nw = 1, E = nothing,
                                    ΔW = zeros(nw), Uformat, Wformat)

Affine approximation from user-supplied derivative information — the same data UGA's LINEARIZED mode asks for, usable without Symbolics:

• A(x̄, ū, w̄), B(x̄, ū, w̄): state and input Jacobians at the linearization point;
• E(x̄, ū, w̄): noise matrix (defaults to a zero nx × nw matrix);
• f(x̄, ū, w̄): the dynamics value, giving the affine offset c = f − A·x̄ − B·ū − E·w̄;
• lipschitz: error bound over the local box — either a constant vector or a callable (x̄, ū, w̄, δx, δu) -> Vector;
• Uformat / Wformat: as in SymbolicAffineApproximationProvider.

AutomatonMemoryController

Finite-memory controller over abstract states, fully table-backed — the serializable alternative to a closure-based DiscreteDynamicController for specification-automaton memory (e.g. co-safe LTL):

• the memory follows the specification automaton: qa′ = step_map[(qa, label)] with label = label_of_state[qs] (default_label for states outside the labeled range);
• the control comes from a controller synthesized on the product automaton, looked up through the product-state table pid[(qs, qa)].

ClosedLoopTrajectory

Result of a closed-loop simulation: the state trajectory x, the input trajectory u, and — for dynamic controllers — the controller-memory trajectory q (nothing for static controllers). Destructures as x_traj, u_traj[, q_traj] = traj.

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::LazySets.AbstractHyperrectangle, 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.

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::LazySets.AbstractHyperrectangle, u::SVector, tstep::Real) -> LazySets.Hyperrectangle This function simulates the image of the center and inflates it using the computed growth bound.

ContinuousTimeGrowthBound(system; jacobian_bound = nothing, ngrowthbound = DEFAULT_NUM_SUBSTEPS)

Build a continuous-time growth-bound overapproximation from a Jacobian bound: the radius dynamics ṙ = jacobian_bound(u) * r are integrated with ngrowthbound RK4 substeps per time step. When jacobian_bound is not provided, it is derived from the system via compute_jacobian_bound (requires an extension providing it).

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::LazySets.AbstractHyperrectangle, u::SVector, tstep::Real) -> LazySets.Hyperrectangle The result is a conservative reachable set from the center using linearization + second-order error correction.

ContinuousTimeOverApproximationMap <: 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(elem::LazySets.LazySet, u::SVector, tstep::Real) -> bounded LazySets.LazySet 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.

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.
• rng: Optional random number generator for reproducible sampling (nothing = global RNG).

Underapproximation Map

Returns a function of the form: f(rect::LazySets.AbstractHyperrectangle, 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.

ContinuousTimeSystemApproximation <: SystemApproximation

Abstract supertype for approximations of continuous-time systems.

ContinuousTimeSystemOverApproximation <: ContinuousTimeSystemApproximation

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

ContinuousTimeSystemUnderApproximation <: ContinuousTimeSystemApproximation

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

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.

ControlTable(nstates::Int)

Plain-data map from an abstract state q ∈ 1:nstates to the list of admissible abstract inputs, the canonical controller_map of a DiscreteStaticController. Callable: table(q) returns the input list; fill with add_control! / set_control!.

ControllerKind

Trait: StaticKind() for a stateless feedback map, DynamicKind() for a controller with internal memory (protocol initial_state/update_state).

DiscreteDynamicController(x0, dom, statemap, outputmap, randomize)

Dynamic feedback on abstract states with memory x starting at x0: statemap(x, y) updates the memory, outputmap(x, y) returns the control (or the list of admissible controls), dom contains the valid (x, y) pairs. Closure-backed and therefore not serializable — prefer AutomatonMemoryController for controllers meant to be saved.

DiscreteStaticController(dom, controller_map, randomize)

Static feedback on abstract states: controller_map(q) returns the admissible inputs of q (e.g. a ControlTable), dom the set of controlled states.

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::LazySets.AbstractHyperrectangle, u::SVector) -> Vector{SVector} which returns a singleton list with the propagated center point.

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::LazySets.AbstractHyperrectangle, u::SVector) -> LazySets.Hyperrectangle This function simulates the image of the center and inflates it using the computed growth bound.

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::LazySets.AbstractHyperrectangle, u::SVector) -> LazySets.Hyperrectangle It evaluates the system at the center, adds linearized spread based on Jacobian, and inflates with the error bound.

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(elem::LazySets.LazySet, u::SVector) -> bounded LazySets.LazySet which returns an overapproximated successor set.

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.
• rng: Optional random number generator for reproducible sampling (nothing = global RNG).

Underapproximation Map

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

DiscreteTimeSystemApproximation <: SystemApproximation

Abstract supertype for approximations of discrete-time systems.

DiscreteTimeSystemOverApproximation <: DiscreteTimeSystemApproximation

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

DiscreteTimeSystemUnderApproximation <: DiscreteTimeSystemApproximation

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

DiscreteTrajectory{Q, TT}

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

SymbolicAffineApproximationProvider

Affine approximation from symbolic dynamics fsymbolic(x, u, w): Jacobians are computed symbolically and the Lipschitz constants are bounded over the local domain with interval arithmetic. ΔW is the noise-box radius vector; Uformat / Wformat are the LMI encodings of the input and noise sets (format_input_set / format_noise_set). Requires Symbolics.jl (using Symbolics).

SymbolicSystem

System-definition bundle for solvers that re-linearize the dynamics on the fly (lazy-ellipsoids abstraction): symbolic dynamics (fsymbolic, x, u, w), dimensions, domains X/U/W, local linearization radii ΔX/ΔU/ΔW, forward/backward evaluators, and the LMI formats of U and W. Use get_affine_provider to obtain the corresponding SymbolicAffineApproximationProvider.

SystemApproximation

Abstract supertype for all system approximation types.

Trajectory{T}

provides the sequence of some elements of a trajectory.

TransitionResult

Outcome of one transition-synthesis SDP (solve_transition / solve_transition_backward).

• feasible::Bool — whether a certified controller was found;
• controller — the affine controller as a MathematicalSystems.AffineMap x ↦ Kx + b (with b = ℓ − K·c₁), or nothing if infeasible;
• cost — upper bound on the worst-case transition cost, or nothing;
• source — the synthesized source ellipsoid (backward mode only), or nothing.

Append input u to the admissible inputs of state q.

as_controller(result::TransitionResult) -> Union{Nothing, AffineController}

The synthesized affine controller as a simulatable AffineController, or nothing if the transition was infeasible.

build_affine_approximation(provider, x̄, ū, w̄ = nothing; δx, δu) -> AffineApproximation

Affine approximation of the dynamics around the linearization point (x̄, ū, w̄), valid on the box of radii δx / δu around it (w̄ = nothing linearizes at zero noise). Implemented per provider.

discretize_continuous_system(system::MS.AbstractContinuousSystem, tstep::Float64; num_substeps = 5)

Convert a continuous-time control system to a discrete-time system.

Arguments

• system: Continuous-time AbstractContinuousSystem from MathematicalSystems.jl
• tstep: Fixed time step for Euler discretization
• num_substeps: Number of RK4 substeps per time step

Returns

• A ConstrainedBlackBoxControlDiscreteSystem with the same state/input constraints

format_input_set(U) -> Vector{<:AbstractMatrix}

Convert the input set U (LazySets.AbstractHyperrectangle, LazySets.Ellipsoid, or a LazySets.IntersectionArray of those) into the list of matrices Uᵢ encoding the input constraints |Uᵢ·u| ≤ 1 used by the transition-synthesis LMIs.

format_noise_set(rec::LazySets.AbstractHyperrectangle) -> Matrix

Vertices of the noise polytope rec as an n × 2ⁿ matrix (one vertex per column), the format consumed by the transition-synthesis LMIs.

get_affine_provider(sys::SymbolicSystem) -> SymbolicAffineApproximationProvider

The affine-approximation provider matching the bundle's symbolic dynamics.

get_closed_loop_trajectory(system, controller, x0, nstep; kwargs...) -> ClosedLoopTrajectory

Simulate the closed loop for at most nstep steps and return the visited states/inputs (plus the controller-memory trajectory q for dynamic controllers). The loop stops early when stopping(x) holds, when trajectory_success(x_traj) holds, when the controller returns nothing, or when the successor is nothing/non-finite.

Keyword arguments: meas (measurement map, default identity), stopping, trajectory_success, wrap (state normalization, e.g. periodic wrapping), update_on_next (feed the next measurement to update_state), f_map_override (replace MathematicalSystems.mapping(system) as the step function; may return nothing for "no successor"), verbose.

get_over_approximation_map(overApprox::ContinuousTimeSystemOverApproximation) -> Function

Returns a function that computes the overapproximation of the system's evolution: f(elem::LazySets.LazySet, u::SVector{M,T}, tstep::T) -> bounded LazySets.LazySet

get_over_approximation_map(approx::DiscreteTimeSystemOverApproximation) -> Function

Returns a function that computes the overapproximation of the system's evolution: f(elem::LazySets.LazySet, u::SVector{M,T}) -> bounded LazySets.LazySet

get_under_approximation_map(approx::ContinuousTimeSystemUnderApproximation) -> Function

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

get_under_approximation_map(approx::DiscreteTimeSystemUnderApproximation) -> Function

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

input_cache(approx::DiscreteTimeSystemOverApproximation, r, u)

Data the approximation can hoist out of the per-cell loop: whatever depends only on the input u and the (uniform) cell radius r, computed once per input and reused by reach_set across all cells. Defaults to nothing.

reach_set(approx::DiscreteTimeSystemOverApproximation, elem, u, cache) -> LazySets.LazySet

Over-approximation of the successor set of the cell elem under input u, using the per-input cache produced by input_cache. Concrete approximations override both functions as a pair; the fallback ignores the cache and calls the generic over-approximation map.

runge_kutta4(dynamics, x, u, tstep, num_substeps::Int)

Perform one step of 4th-order Runge-Kutta time integration.

Arguments

• dynamics: Function f(x, u) for the continuous dynamics
• x: Current state
• u: Control input
• tstep: Total time step
• num_substeps: Number of substeps for integration

Returns

• Updated state after time tstep

Make u the unique admissible input of state q.

solve_transition(affsys, source, target, U, W, cost, sdp_solver) -> TransitionResult

Synthesize an affine controller u(x) = K(x − c₁) + ℓ certifying that every state of the source ellipsoid reaches the target ellipsoid in one step of the affine system affsys (x⁺ = Ax + Bu + c (+ Dw)), for every disturbance vertex, while minimizing an upper bound on the worst-case transition cost ‖cost · [x; u; 1]‖².

Arguments

• affsys: an affine system ((Noisy)ConstrainedAffineControlDiscreteSystem or ConstrainedAffineControlMap);
• source, target: LazySets.Ellipsoids;
• U: input constraints — a set (LazySets.AbstractHyperrectangle, LazySets.Ellipsoid, LazySets.IntersectionArray) or a preformatted list (format_input_set);
• W: disturbance vertices — one per column, or a box (LazySets.AbstractHyperrectangle); mapped through the system's noise matrix D when the system has one;
• cost: the cost factor matrix Λ of size (nx+nu+1) × (nx+nu+1), or a UT.QuadraticStateControlFunction;
• sdp_solver: a JuMP-compatible SDP optimizer (Clarabel, Mosek, …).

solve_transition_backward(affsys, target, source_center, u_ref, U, W, cost,
                          lipschitz, sdp_solver;
                          maxδx = 100.0, maxδu = 20.0, λ = 0.01,
                          use_log_det = true) -> TransitionResult

Synthesize an affine controller and the largest source ellipsoid centered at source_center that the controller certifiably drives into the target ellipsoid in one step of affsys, robustly to the disturbance vertices W and to the linearization error bounded by lipschitz (the Lipschitz radii of [x; u; 1], scaled by the synthesized state/input deviations δx + δu).

The objective trades the transition-cost bound against the source volume: min λ·J − (1−λ)·logdet(L) (a trace proxy when use_log_det = false). u_ref is the reference input the controller stays δu-close to; maxδx / maxδu cap the synthesized deviations. Other arguments as in solve_transition. Returns a TransitionResult whose source is the synthesized ellipsoid.

stabilizing_feedback(subsys, sdp_solver) -> (feasible, K, P, γ)

For a stabilizable affine system, find the state-feedback gain K and the matrix P satisfying the discrete-time Lyapunov inequality (A+BK)'P(A+BK) − P ≺ 0, minimizing the condition number of P (γ is the attained smallest eigenvalue of P⁻¹).

Default number of RK4 substeps per time step, shared by every discretize path.