Utils

BlackBoxControlFunction{F}

Arbitrary user-supplied state-input function f(x, u); same freedom and serialization caveat as BlackBoxFunction.

BlackBoxFunction{F}

Arbitrary user-supplied state function f(x), in the spirit of MathematicalSystems' BlackBox maps: full modeling freedom, but unlike the structured functions it does not serialize reliably (closures, e.g. to JLD2).

NodeT{S, A}

A node of a Tree: a state of type S, the action of type A that reached it from its parent (nothing for the root), and the cost bookkeeping used by RRT/RRT*.

A defaults to Any (the action type is generally only known lazily while the tree grows); instantiate Tree{S, A} with a concrete A when the action type is known up front.

Piecewise-affine convex function x ↦ max(lower_bound, maxᵢ pieceᵢ(x)) on domain (∞ outside).

Quadratic form x ↦ x'Qx.

QuadraticStateControlFunction{T, MT<:AbstractMatrix{T}}

Quadratic function on state and input defined as x'Qx + u'Ru + 2x'Nu + 2x'q + 2u'r + v

Root of state-input functions f(x, u).

Root of state functions f(x).

SemiLinearSet{T, PT}

A finite union of polytopes: alias of LazySets.UnionSetArray restricted to HPolytope parts, so the whole LazySets API (∈, isempty, dim, intersection, plotting) applies. Build with semilinear_set; the parts live in S.array.

Tree{S, A}

A rooted tree of NodeT{S, A} nodes, tracking its leaves and node count. Built incrementally by add_node!; the search backbone of the RRT-based abstractions.

Basic generic RRT algorihtm
SI : initial state (this will be the root of the tree) ;
SF : target state that we try to reach ;
distance : function that defines a metric between the states ;
rand_state : function that returns a random candidate state ;
new_conf : function that returns a reachable state, with the action and the cost ;
keep : function to filter the node that we want to add during an iteration;
stop_crit : stop criteria ;
RRTstar : boolean to use RRT* ;
compute_transition : to compute transition between to given state (if RRTstar is true).

add_node!(tree, state, parent, action, cost; path_cost = parent.path_cost + cost)

Create a node for state, attach it to parent with the action and edge cost that reached it, and register it as a leaf of tree. Returns the new node.

derivative_bisection(f, df, ddf; interval, δ, verbose, stopIfNegative) -> (f(x⋆), x⋆)

Minimize a convex f by bisecting on the sign of f′: the sub-interval is halved toward where the derivative changes sign. ddf supplies the local curvature bound used by the stopIfNegative early exit.

Semi-axis lengths √λᵢ(Q) of the ellipsoid, longest first.

get_quadratic_form(E::LazySets.Ellipsoid)

Quadratic-form matrix P = Q⁻¹ of the ellipsoid, i.e. the matrix such that E = {x : (x − c)ᵀ P (x − c) ≤ 1}.

Sublevel-set scaling {x : (x−c)ᵀP(x−c) ≤ α}, i.e. Q ← α·Q.

golden_section_search(f; interval, δ, verbose, stopIfNegative) -> (f(x⋆), x⋆)

Golden-section search for the minimum of a unimodal f on interval. Derivative free; brackets the minimum by keeping the golden ratio between four probe points.

grid_step_from_lyapunov(P, ε, γ; state_dim = size(P, 1)) -> η

Largest uniform grid step η for which a center-simulation uniform-grid abstraction of a δ-GAS system is ε-approximately bisimilar to the sampled system, following (Girard et al., 2010).

P is the symmetric positive-definite matrix of a common quadratic Lyapunov function V(x, y) = ‖x - y‖_P, γ ∈ [0, 1) is its per-step contraction (V shrinks by a factor γ each sampling step — for a continuous-time rate κ sampled at τ, γ = e^{-κτ}), and ε is the target precision in the Euclidean (output) norm.

The abstraction relation {(x, x_q) : ‖x - x_q‖_P ≤ √λ_min(P) · ε} is preserved when the per-step quantization error is absorbed by one step of contraction:

√λ_max(P) · (η √n / 2) ≤ (1 - γ) · √λ_min(P) · ε,

so

η = 2 (1 - γ) · √(λ_min(P) / λ_max(P)) · ε / √n .

The condition number of P therefore directly controls how fine the grid must be.

Obtain (P, γ) from a common quadratic Lyapunov function, e.g. compute_quadratic_pieces_pclf on the sampled modes. See precision_from_grid_step for the inverse.

Inclusion mode to use for the hole B when discretizing A \ B (soundness inverts it).

is_disjoint(X, Y) -> Bool

Whether X ∩ Y = ∅. Generic sets delegate to LazySets; an exact analytic kernel runs for two LazySets.Ellipsoids (see sets/ellipsoid_intersection.jl).

is_included(X, Y) -> Bool

Whether X ⊆ Y. Generic sets delegate to LazySets; an exact analytic kernel runs for two LazySets.Ellipsoids (see sets/ellipsoid_inclusion.jl) — Dionysos owns this verb because extending Base.issubset on two LazySets-owned types would be piracy.

Hole B of A \ B.

Included region A of A \ B.

newton_method(f, df, ddf; interval, x0, ϵ, verbose, stopIfNegative) -> (f(x⋆), x⋆)

Newton's method for a stationary point of f, iterating x -= f′(x)/f″(x) until |f′(x)| ≤ ϵ or x leaves interval; the result is projected back onto interval.

precision_from_grid_step(P, η, γ; state_dim = size(P, 1)) -> ε

Precision ε (Euclidean norm) of the ε-approximately bisimilar center-simulation abstraction obtained with uniform grid step η; the inverse of grid_step_from_lyapunov:

ε = η √n · √(λ_max(P) / λ_min(P)) / (2 (1 - γ)) .

Project S onto the coordinates dims (identity when dims covers S).

Sample a point of X uniformly (LazySets rejection sampling).

Sample N points of X uniformly (LazySets rejection sampling); pass rng for reproducibility.

semilinear_set(parts) -> SemiLinearSet

The union of the given polyhedral sets, each converted to HPolytope.

set_in_period(rect, periodic_dims, periods, start) -> LazySets.UnionSetArray

Split rect along periodic boundaries and return the union of the wrapped boxes.

set_minus(A, B) -> LazySets.Intersection

The set difference A \ B, represented lazily as A ∩ Bᶜ.

set_union(sets) -> LazySets.UnionSetArray

Lazy union ⋃ᵢ setsᵢ of the given (Dionysos or LazySets) sets.

wrap_coord(x::SVector{N, T}, periodic_dims::SVector{P, Int}, periods::SVector{P, T}; start = zeros(SVector{P, T}))

Wraps the vector x into a periodic domain along dimensions specified in periodic_dims, with period lengths periods and optional offset start.

Arguments

• x: The coordinate vector to wrap.
• periodic_dims: Indices of the periodic dimensions.
• periods: Period lengths for the periodic dimensions.
• start (optional): Starting values of the periodic domains (defaults to 0.0).

Returns

A wrapped SVector where each periodic dimension is mapped to the interval [start[i], start[i] + periods[i]).

Wrap the scalar x into [start, start + period).

struct LabDigraph{T<:Real, U}

Store a graph as an explicit list of edges (u, v, label), preserving parallel edges and arbitrary vertex types.

mutable struct PCLF

Store a path-complete Lyapunov function (i.e. a graph and a collection of Lyapunov pieces) for a linear switched system and the corresponding JSR approximation

Compute a path-complete Lyapunov function (PCLF) with general polyhedral pieces defined over a partition of the state space into cones.

Each node s is associated with a piecewise-linear Lyapunov function:

V_s(x) = max_i |p_{s,i}ᵀ x|,

where the rows of a matrix P_s define the supporting hyperplanes of the polytope.

Method

The method formulates a feasibility linear program (LP) based on:

1. Positivity constraints ensuring V_s(x) ≥ 0 on each cone

2. Dominance constraints ensuring correct piecewise structure

3. Decrease conditions along edges:

   V_v(A_σ x) ≤ ρ V_u(x)

These constraints are enforced on the extreme rays of the cones in partitions.

A bisection on ρ is used to approximate the joint spectral radius (JSR).

Arguments

• f: hybrid system containing the system matrices A_σ
• D: labeled directed graph defining the PCLF structure
• optimizer: JuMP optimizer
• partitions: dictionary mapping each node to a list of cones (matrices of rays)

Keyword arguments

• tol: tolerance for bisection on ρ
• maxiter: maximum number of iterations
• MLF: if true, extracts the Lyapunov pieces
• verbose: enable solver output
• min_c: lower bound on auxiliary scalar variables

Returns

• PCLF: structure containing the graph, Lyapunov pieces, and JSR approximation

Notes

• This method allows for more general polyhedral Lyapunov functions than the symmetric 2n-face construction.
• The number of faces depends on the number of rows of P_s.
• Less conservative but computationally more expensive.
• The quality depends on the chosen cone partition.

Compute a path-complete Lyapunov function (PCLF) with quadratic (ellipsoidal) pieces for a switched linear system.

Each node s of the graph is associated with a quadratic Lyapunov function:

V_s(x) = xᵀ P_s x,

where P_s is a symmetric positive definite matrix. The corresponding sublevel sets are ellipsoids.

Method

The method formulates a semidefinite feasibility problem (SDP) and performs a bisection on γ. For each edge (u → v, σ), it enforces the Lyapunov inequality:

A_σᵀ P_v A_σ ≤ γ² P_u,

implemented via linear matrix inequalities (LMIs):

γ² P_u - A_σᵀ P_v A_σ - I ≽ 0.

Additional constraints ensure positive definiteness and boundedness of the matrices P_s.

Arguments

• f: hybrid system containing the system matrices A_σ
• G: labeled directed graph defining the PCLF structure
• optimizer: JuMP-compatible SDP solver

Keyword arguments

• tol: tolerance for bisection on γ
• maxiter: maximum number of iterations
• MLF: if true, extracts the Lyapunov matrices P_s

Returns

• PCLF: structure containing the graph, Lyapunov pieces (ellipsoids), and JSR approximation

Notes

• This method searches for a quadratic (ellipsoidal) Lyapunov function on each node.
• It relies on semidefinite programming (SDP), which is more expensive than LP-based polyhedral methods but often less conservative.
• The resulting Lyapunov function is smooth and globally defined on each node.

Compute a path-complete Lyapunov function (PCLF) with symmetric polyhedral pieces having 2n faces for a switched linear system.

Each node s of the graph is associated with a polyhedral Lyapunov function of the form:

V_s(x) = max_i |(G_s x)_i| / w_s[i]

whose sublevel sets are polytopes:

{ x : -γ w_s ≤ G_s x ≤ γ w_s }.

Method

The method constructs and solves a feasibility linear program (LP) using bisection on γ. For each edge (u → v, σ), it enforces:

|G_v A_σ G_u^{-1}| * w_u ≤ γ w_v,

where the absolute value is taken elementwise.

Arguments

• f: hybrid system containing the system matrices A_σ
• D: labeled directed graph defining the PCLF structure
• optimizer: JuMP optimizer

Keyword arguments

• Gmats: choice of matrices G_s (identity, Dict, or Vector)
• tol: tolerance for bisection on γ
• maxiter: maximum number of bisection iterations
• MLF: if true, extracts the Lyapunov pieces
• verbose: enable solver output
• min_w: lower bound to enforce strict positivity of w

Returns

• PCLF: structure containing the graph, Lyapunov pieces, and JSR approximation

Notes

• The resulting Lyapunov functions are structured and correspond to weighted ∞-norms in transformed coordinates.
• This approach is computationally efficient but may be conservative.

Reference

This symmetric 2n-face construction of polyhedral path-complete Lyapunov functions follows (Athanasopoulos and Jungers, 2019).