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.

mode_matrices(system) -> Vector{Matrix{Float64}}

The linear map of every mode of a discrete switched system, in mode order.

HybridSystems.discreteswitchedsystem stores a mode either as a bare matrix or as a system object carrying one in its A field; both are accepted so a switched system can be built either way. Anything else is an error rather than a silent guess, since the matrices drive the preimages a bisimulation is built from.

It lives here rather than in System because PathCompleteFramework needs it too, and Utils is the only module both can see.

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

build_common_lyapunov(pclf::PCLF; mode = :auto) -> PCLF

The common Lyapunov function induced by pclf, as a one-node PCLF.

mode selects the construction, and the default checks the graph's structure rather than always paying for the subset construction:

:auto prefers :min when both structural tests pass, because a certificate is judged first by what it certifies and the union is the larger region; :max is then available explicitly and is cheaper. On a De Bruijn graph the question does not arise — the primal is complete and not co-complete, the dual the reverse — so each admits exactly one closed form.

The observer fallback is not wrong on the structured graphs, merely wasteful: it recovers the same function (on a complete graph its singletons make min_S max_{i∈S} V_i collapse to min_i V_i) but enumerates redundant subsets on the way. Those are filtered out in every mode.

certify_pclf(pclf, f, optimizer; rtol = 1e-6)
certify_pclf(pclf, A, optimizer; rtol = 1e-6)

Decide the contraction inequality of pclf exactly, for polyhedral pieces.

For a polyhedral piece the value is a gauge, so by homogeneity the rate along an edge (s, s′, m) is

sup { V_{s′}(A_m x) : V_s(x) ≤ 1 },

a maximum of linear functionals over a polytope, hence a linear program per row of G_{s′} and per sign. optimizer is any LP-capable JuMP optimizer.

The return value has the same fields as check_pclf, but the rates are suprema rather than sample maxima: an empty violated here establishes the certificate instead of merely failing to refute it.

check_pclf(pclf, f; nsample = 20_000, rng = nothing, rtol = 1e-6)
check_pclf(pclf, A; nsample = 20_000, rng = nothing, rtol = 1e-6)

Test the contraction inequality that defines the certificate pclf, by sampling.

Along every edge (s, s′, m) of the graph a path-complete Lyapunov function claims

V_{s′}(A_m x) ≤ ρ^d V_s(x)    for all x,

with ρ = pclf.JSRapprox and d the homogeneity degree of the pieces. Both sides are homogeneous, so the claim does not depend on the scale of x and sampling directions covers it.

The mode matrices are taken either from a HybridSystems.HybridSystem or given directly as a vector indexed by mode label.

Returns (; rate, by_edge, violated, certified_rate). rate is the largest rate observed over all edges and by_edge the rate of each, both expressed on the gauge — that is, as (V_{s′}(A_m x) / V_s(x))^(1/d) — so that they are directly comparable with pclf.JSRapprox whatever the piece type. violated lists the edges exceeding it by more than rtol in relative terms.

A sample underestimates a supremum, so this refutes a certificate rather than establishing one: a rate above ρ proves the certificate wrong, a rate below it is evidence and not a proof. When the pieces are polyhedral, certify_pclf decides the question exactly.

rng is the caller's, and nothing uses the default global one; pass a seeded generator when a run has to be reproducible.

See also certify_pclf.

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

enabled_modes(G::LabDigraph) -> Dict{U, Set{Int}}

The modes each node of G may actually emit.

This is the language talking, and it has to be carried forward explicitly rather than rediscovered later from the absence of a transition. Downstream, "node q has no successor under mode m" has two irreconcilable causes: the language forbids m at q, so the environment cannot play it; or m is allowed but its successor left the region the abstraction covers, so a real behaviour was dropped. A universal (∀) answer must ignore the first and pessimistically account for the second, and once the graph is gone the two are indistinguishable. See is_complete for when the distinction is vacuous: on a complete graph every node enables every mode and nothing is ever forbidden.

is_co_complete(G::LabDigraph, modes) -> Bool

Whether every node of G has an incoming edge for every mode in modes.

The mirror of is_complete, and the reason both are worth testing: each licenses a different closed-form common Lyapunov function, and the two are genuinely different objects.

Write the edge condition as V_d(A_m x) ≤ γ V_s(x) for every edge (s, m, d).

• complete ⟹ V_min = min_i V_i is a common Lyapunov function. If the minimum at x is attained at i, completeness supplies an edge (i, m, d), so min_j V_j(A_m x) ≤ V_d(A_m x) ≤ γ V_i(x). Its sublevel set is the union of the pieces' sublevel sets — non-convex, but the larger set.
• co-complete ⟹ V_max = max_i V_i is one. For each target i, co-completeness supplies an edge (s, m, i), so V_i(A_m x) ≤ γ V_s(x) ≤ γ V_max(x). Its sublevel set is the intersection — convex and cheap, but the smaller set.

On De Bruijn graphs exactly one holds: the primal (a node records the last mode played) is complete and not co-complete; the dual (a node commits to the mode played next, and any node may follow) is co-complete and not complete. So the common induced on a dual graph necessarily loses coverage, and the one induced on a primal graph necessarily loses convexity. See build_common_lyapunov.

is_complete(G::LabDigraph, modes) -> Bool

Whether every node of G has an outgoing edge for every mode in modes.

Completeness and path-completeness are different properties and license different uses. A path-complete graph represents every finite mode word by some path, which is what synthesis needs: a co-safe specification is witnessed in finite time, and the witness word has a path to follow. Verification under arbitrary switching needs more — a node missing an outgoing edge for some mode removes a move the real adversary has, so the abstraction can certify a universal property the concrete system does not satisfy. Completeness is exactly what closes that gap.

See also is_deterministic, which bounds the same counts from above rather than below.

is_deterministic(G::LabDigraph, modes) -> Bool

Whether every (node, mode) pair of G has at most one outgoing edge.

When a graph branches, the successor node is not determined by the mode, and something must resolve the choice. A controller that tracks one node resolves it in its own favour; an adversary that resolves it instead removes freedom the concrete system grants. The distinction matters for synthesis guarantees, so it is worth being able to test.

See also is_complete.

restricts_future(G::LabDigraph) -> Bool

Whether the node reached so far changes which modes are available next.

false on a De Bruijn graph, where a node records history only and every node enables every mode, so a result holding at one node holds at all of them. true for a genuine language restriction such as "no two consecutive uses of mode 1", where the node constrains the future — and then results at different nodes are answers to different questions and must not be merged without deciding which node a run may start in.