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)].

AutomatonPath{Q, TT}

A path through a hybrid automaton: a starting mode q_0 and a sequence of discrete transitions. This is a search-space object — the partial candidate grown (via append) by the branch-and-bound solver — not a state/input rollout over time (that is a Trajectory).

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.

FunnelController(kappas, ellipsoids)

Time-indexed funnel-tracking controller, the simulatable form of an ellipsoidal certification chain (E_1, κ_1, …, E_K, κ_K, E_{K+1}): the memory is the step index k, the output at step k is κ_k(x) (an absolute-coordinates MathematicalSystems.AffineMap), and the controller is defined while the measured state lies in the certified ellipsoid E_k. The certificate guarantees that a defined step stays defined: x ∈ E_k ⟹ x⁺ ∈ E_{k+1}. Plain data — serializable.

GuardedResetMap{G, F} <: MathematicalSystems.AbstractMap

The map taken on a hybrid transition: it is enabled on the guard set G and applies the reset F to the state.

MathematicalSystems.stateset returns the guard — which is how HybridSystems stores the enabling condition of a transition — and MathematicalSystems.apply runs the reset. reset defaults to the identity, the common case where switching mode leaves the state untouched.

The state it is applied to is the augmented state of the mode: x for a plain mode, and [x; t] for a clock-lifted one. guard must live in the same space.

# switch enabled on T ≤ 19, leaving the temperature unchanged
GuardedResetMap(LazySets.Hyperrectangle(; low = [17.0], high = [19.0]))

# switch enabled on the target box, resetting x and clamping the clock
GuardedResetMap(target, state -> vcat([0.0], max(1.0, state[end])))

JacobianBoundPrecision

How much of the state and input space a single evaluation of a derived Jacobian bound has to cover at once. Every level is rigorous; they differ in tightness and in how often the bound is recomputed. See compute_jacobian_bound.

• GLOBAL_BOUND — one matrix for all of X and U.
• INPUT_BOUND — over all of X, re-derived per input.
• REGIONWISE_BOUND — over one region of X at a time, per (region, input).

RegionwiseBound(bound, region_of, nregions)

A Jacobian bound that is piecewise constant over the state space: bound(i, u) is the matrix valid throughout region i, and region_of(x) says which region a point falls in.

A bound covering the whole state set must be as large as its worst point. On a nonlinear system that is usually far larger than any one region needs — |-(g/l)cos x₁| is g/l over a full turn but near zero on most slices of it — so splitting the state space buys tightness, and tightness is what decides whether synthesis succeeds at a given grid size.

Crucially the regions are few and fixed, not one per cell: the radius can still be integrated once per (region, input) and hoisted out of the cell loop by input_cache, leaving only an array lookup on the per-cell hot path.

RegionwiseGrowth(radius, region_of, nregions)

The growth-bound map produced by a RegionwiseBound: radius(i, r, u[, tstep]) is the inflated radius for a cell of radius r sitting in region i.

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{S, I, T, M, Q}

A system trajectory stored as parallel channels. The states channel is always present; every other channel is optional and is nothing when absent:

• inputs — applied inputs; nothing for an open-loop / state-only trajectory,
• times — physical time at each step (timed systems),
• modes — active discrete mode at each step (hybrid systems),
• memory — controller memory at each step (dynamic controllers).

So a closed-loop rollout is just a Trajectory that carries inputs, and a plain state trajectory is one with inputs === nothing. Build it with Trajectory(states; inputs = ..., times = ..., modes = ..., memory = ...) and read channels with states, inputs, times, modes, memory.

TransitionResult

Outcome of one transition-synthesis SDP (solve_transition, solve_transition_backward, solve_transition_backward_2step, solve_transition_forward).

• 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 modes only), or nothing;
• target — the synthesized target ellipsoid (forward mode only), or nothing.

Append input u to the admissible inputs of state q.

append(traj::AutomatonPath, t) -> AutomatonPath

Return a copy of traj with the transition t appended — the growth step used by the branch-and-bound search to extend a candidate path.

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.

compute_jacobian_bound(system; precision = INPUT_BOUND, nsplit = 4)

Derive a Jacobian bound from the dynamics instead of writing one by hand: the extension traces f symbolically and bounds each entry with interval arithmetic, which is a proof rather than a sample. Requires Symbolics to be loaded.

A hand-written bound is still worth having — it can exploit structure the interval arithmetic cannot see, and costs nothing at runtime — but it is also the single input whose being wrong invalidates every guarantee downstream, silently. This is the alternative.

precision (a JacobianBoundPrecision) trades tightness against work:

GLOBAL_BOUND is enough when the Jacobian barely varies. INPUT_BOUND — the default — is free in the abstraction's hot loop, because the radius map is hoisted out of the cell loop by input_cache. REGIONWISE_BOUND stays hoisted too: the regions are few and fixed, so the radius is integrated once per (region, input) and the per-cell work is a lookup. Reach for it when a bound taken over the whole state space is too conservative for synthesis to succeed — on a pendulum it cut spurious transitions by 5–10% at nsplit ≥ 8.

Note nsplit^n grows with the state dimension n, so lower nsplit above 2–3 states.

denormalize_controller(κ::MathematicalSystems.AffineMap, t) -> AffineMap

A feedback u = K_z·z + b synthesized in the normalized frame, as the physical map u = K_z·D⁻¹·x + b (inputs are frame-invariant).

denormalize_ellipsoid(E, t) -> LazySets.Ellipsoid

An ellipsoid certified in the normalized frame, mapped back to the physical frame: c_x = t .* c_z, Q_x = D·Q_z·D with D = Diagonal(t).

denormalize_funnel(ctrl::FunnelController, t) -> FunnelController

A whole certified funnel controller mapped back to the physical frame — the one-call version of denormalizing every κ_k and every E_k.

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...) -> Trajectory

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"), input_type (element type of the recorded input channel; defaults to the type of the first input — pass Any when inputs are heterogeneous, e.g. continuous inputs mixed with hybrid switching labels), verbose.

get_cost_trajectory(traj::Trajectory, c) -> (cost, total_cost)

Evaluate the stage cost c(state, input) along traj (which must carry an inputs channel). Returns the per-step cost vector and the summed total_cost.

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.

Input channel (vector of applied inputs), or nothing for an open-loop trajectory.

Controller-memory channel, or nothing for static controllers.

Discrete-mode channel, or nothing when the trajectory is non-hybrid.

normalize_box(H, t) -> LazySets.Hyperrectangle

The axis-aligned box H in the normalized frame z = x ./ t.

normalize_trajectory(traj::Trajectory, t) -> Trajectory

The trajectory with every state scaled to the normalized frame z = x ./ t (inputs are frame-invariant).

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 (at least one; a single zero vertex for deterministic dynamics), or a box (LazySets.AbstractHyperrectangle); mapped through the system's noise matrix D when the system has one;
• cost: the PSD cost matrix S of size (nx+nu+1) × (nx+nu+1) bounding [x; u; 1]ᵀ·S·[x; u; 1], or a UT.QuadraticStateControlFunction; the factor the LMIs consume is taken internally (_cost_factor);
• sdp_solver: a JuMP-compatible SDP optimizer (Clarabel, Mosek, …).

Every returned certificate is re-validated numerically at the solver's solution — a transition reported feasible is PSD-certified independently of the solver's termination status.

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,
                          objective = :logdet, remainder_model = :vertices,
                          source_cap = nothing) -> 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 deviations δx + δu — NOTE that δx / δu bound the SQUARED state/input deviations, so maxδx / maxδu are radii at this boundary while the remainder is quadratic in them).

The objective trades the transition-cost bound against the source size (min λ·J − (1−λ)·size): :maximin maximizes the smallest semi-axis (collapse-proof and cone-free — the ellipsoidal certifier's default), :logdet the true volume (this function's default), :trace its stable proxy. remainder_model selects how the linearization error enters the reach blocks: :vertices (exact 2ⁿ corners), :ball (one scalar norm ball), or :john_ball (the box's John ellipsoid — per-axis radii at :ball's block count). u_ref is the reference input the controller stays δu-close to. source_cap (a per-state vector d) additionally confines the source to the axis-aligned slab |xᵢ − c₁ᵢ| ≤ dᵢ — one SOC row per state on the shape factor — so a chain can keep its funnels inside a state domain by construction. Other arguments as in solve_transition. Returns a TransitionResult whose source is the synthesized ellipsoid.

solve_transition_backward_2step(affsys1, affsys2, κ1, target, source_center,
                                u_ref0, U, W1, W2, cost, lipschitz1,
                                e2_halfwidths, sdp_solver;
                                maxδx = 100.0, maxδu = 20.0, λ = 0.01,
                                objective = :maximin,
                                remainder_model = :vertices,
                                source_cap = nothing)
    -> TransitionResult

Synthesize a first-step controller κ₀ and the largest source ellipsoid centered at source_center that reaches target in TWO steps: one step of affsys1 under κ₀, then one step of affsys2 under the fixed controller κ1 (a MathematicalSystems.AffineMap, u₁ = K₁x₁ + b₁). No containment is required at the intermediate state — the lever against per-step chain bottlenecks on underactuated plants (the certificate gains the two-step coupling channel).

lipschitz1 bounds step 1's linearization error (scaled by the synthesized δx + δu — SQUARED deviations, as in solve_transition_backward); e2_halfwidths is the CONSTANT per-axis half-width vector of step 2's remainder box — the caller fixes step 2's linearization box in advance, scales e2_halfwidths with the SQUARED box radii, and must verify a posteriori that the realized intermediate excursion stays inside the box. Both steps currently require a single noise vertex, and only remainder_model = :vertices is supported (the combined two-box remainder has no ball form yet — the kwarg exists so callers passing another model fail loudly instead of being silently downgraded). The transition-cost bound covers (x₀, u₀) only. Returns a TransitionResult whose controller is κ₀ and whose source is the synthesized two-step funnel entry.

solve_transition_forward(affsys, source, target_center, u_ref, U, W, cost,
                         lipschitz, sdp_solver;
                         target_shape = nothing, maxδu = 20.0, λ = 0.01,
                         q_min = 1e-9, q_max = 1e9,
                         remainder_model = :vertices) -> TransitionResult

Synthesize an affine controller and the smallest target ellipsoid centered at target_center that the controller certifiably reaches from the given source ellipsoid in one step of affsys, robustly to the disturbance vertices and to the linearization error bounded by lipschitz — whose state deviation is the known λ_max(Q₁) of the source (a SQUARED semi-axis: the same squared-radius convention as the backward kernels' δx), so the remainder is fixed data (no adaptive boxes).

Target modes: with target_shape (a LazySets shape matrix Q̂) only the scale α is free (min λ·J + (1−λ)·α — α is the per-step contraction number); without it the shape Q₂ itself is a decision variable (min λ·J + (1−λ)·tr(Q₂)) inside the conditioning sandwich q_min·I ⪯ Q₂ ⪯ q_max·I. Both are single convex SDPs — the target enters the reach blocks linearly. remainder_model accepts :vertices or :ball (:john_ball is backward-only and errors here). Certificates are validated at the returned solution as in solve_transition. Returns a TransitionResult whose target 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⁻¹). On an unsuccessful solve the result is (false, nothing, nothing, nothing) — no values are extracted from a failed model.

State channel (vector of visited states) of a trajectory.

Physical-time channel, or nothing when the trajectory is untimed.

unwrap_trajectory(traj::Trajectory, periodic_dims, periods) -> Trajectory

Lift a trajectory with wrapped periodic coordinates to its continuous cover: each periodic dimension follows the increment closest to the previous state, so the ±period jumps at the seam disappear. The certifiers linearize in ℝⁿ and cannot represent a seam jump — certify the unwrapped trajectory, wrap only for plotting/replay.

AffineSys

Union of the affine discrete-time system types the transition-synthesis kernels accept: (Noisy)ConstrainedAffineControlDiscreteSystem and ConstrainedAffineControlMap.

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