chc.reachability

Stability tier: evolving.

Hamilton-Jacobi backward reachable tube under a partially identified control effect.

chc.barrier answers a pointwise question -- at this state, does some admissible action keep d/dt h >= -alpha*h once the effect matrix is only set-identified? That is sufficient for forward invariance but not necessary: a function that fails the barrier condition may still admit a controller that never leaves {h >= 0}, because a barrier certificate demands the safe set be invariant through h itself rather than merely be avoidable. This module computes the question a barrier only approximates,

V(x, T) = max_u min_{Delta_B} min_{s in [0, T]} h(xi(s; x, u, Delta_B)),

so {V(., T) >= 0} is the set from which safety is guaranteed for T more seconds against every effect matrix in the identified ball. V <= h always, and the gap is exactly the price of a finite horizon; the gap against the barrier's own certified set is the price of using h as its own certificate.

The two are not independent. For a control-affine plant with a Euclidean actuation ball and an operator-norm identification radius Delta (the same assumptions chc.barrier needs for its closed form), the upper Hamiltonian is

H(x, p) = max_{||u|| <= U} min_{||Delta_B|| <= Delta} p . (f + (B + Delta_B) u)
        = p . f + U * (||B^T p|| - Delta*||p||)_+,

which is chc.barrier.robust_barrier_margin with p in place of grad h. The reachability solver and the barrier certificate therefore run on the same robust-margin algebra; what differs is that p = grad V is solved for rather than assumed. That also means the §40 zero-action rule reappears here as a property of the Hamiltonian: once Delta*||p|| >= ||B^T p|| the control term vanishes and the tube collapses at the drift's rate.

Scope: a uniform 2-D grid with the standard Lax-Friedrichs scheme (Osher-Fedkiw; Mitchell's level-set toolbox). Two states because that is where a grid method is honest -- the cost is exponential in the dimension, and this exists to calibrate the barrier certificate on small problems, not to replace it on large ones.

ReachableTube dataclass

V(., T_k) on a grid: the guaranteed-safe value after T_k more seconds.

initial property

V(., 0) = h -- the safe set with no horizon demanded of it.

final property

V(., T) after the full horizon; >= 0 is guaranteed-safe for all of it.

safe_fraction(index=-1)

Fraction of grid points still guaranteed safe at times[index].

interpolate(point, index=-1)

Bilinear value at an arbitrary point, so a plan's states can be scored off-grid.

BarrierReachabilityGap dataclass

What a pointwise §40 check does and does not tell you, measured against the true tube.

The CBF theorem is a statement about a set: if the robust barrier condition holds at every point of {h >= 0}, that set is forward invariant. Checking it at one state -- which is what chc.plan.certify_safety does per step, and what any online safety filter does -- is a strictly weaker thing, and these fields separate the two.

HigherOrderBarrierGap dataclass

The §40 check lifted one derivative, so a relative-degree-2 barrier can see the radius.

At pure relative degree 2 (B^T grad h == 0 on the safe set) the first-order robust condition degenerates: the control term -- which is where the identification radius lives -- vanishes, and barrier_reachability_gap returns the same verdict at every radius while the true tube shrinks. The recorded trap of the honest-scope note, now closed: define psi1 = grad h . f + alpha1 * h (the true hdot + alpha1 h -- control-free exactly because of the degeneracy) and certify the robust margin of psi1 on the working set {h >= 0} & {psi1 >= 0} instead. B^T grad psi1 is generically nonzero, so the radius is back in the verdict.

robust_hamiltonian(p, drift, b_matrix, u_max, radius)

p.f + U*(||B^T p|| - Delta*||p||)_+ -- the §40 margin with a solved-for gradient.

The inner min over ||Delta_B||_op <= radius is attained by aligning Delta_B u with -p, which costs radius*||p||*||u||; the outer max over ||u|| <= u_max then spends the whole budget along B^T p, or nothing once the radius swallows the channel.

backward_reachable_tube(barrier, drift, b_matrix, *, lower, upper, resolution=(81, 81), horizon=1.0, steps=200, u_max=1.0, radius=0.0)

Solve dV/dT = min(0, H(x, grad V)) from V(., 0) = h by Lax-Friedrichs.

Parameters:

Name	Type	Description	Default
barrier	Callable[[Array], Array]	h(x), safe where h >= 0; the same function chc.plan.certify_safety takes, so the two answers are about the same set.	required
drift	Callable[[Array], Array]	f(x), the uncontrolled field. Control-affine is assumed, the control entering through the constant b_matrix -- the assumption chc.barrier's closed form needs anyway, and the reason this module does not accept a general Dynamics.	required
radius	float	the §32 operator-norm identification radius on B. 0 recovers the ordinary (exactly identified) reachable tube.	0.0

Raises:

Type	Description
ValueError	if the step violates the CFL condition, which would let the scheme report a larger safe set than the truth -- the one failure mode a safety tool must not have; on a u_max or radius that is negative or not finite, a horizon that is not positive and finite, a grid axis whose bounds are not finite and increasing, or a barrier, drift or b_matrix that is not finite on the grid.

barrier_reachability_gap(barrier, drift, b_matrix, *, lower, upper, resolution=(81, 81), horizon=1.0, steps=200, u_max=1.0, radius=0.0, alpha=1.0, tolerance=0.02)

Run the §40 condition and the horizon-T tube on one grid and report where they part.

The barrier condition asks ``max_u [grad h . f + - radius||grad h||||u||]

= -alpha*h; the tube asks whether *any* controller holdsh >= 0forhorizonseconds against every effect matrix in the identified ball. The implication runs one way and only with a quantifier: if the condition holds at **every** point of{h >= 0}, that set is invariant and the tube must be all of it -- which is whatokchecks. Pointwise the implication is simply false, andcertified_but_unreachableis how much of the grid it is false on: states where the §40 margin is satisfied right now, yet no controller survives the horizon. Relative degree is the usual reason -- whenB^T grad h == 0`` the condition degenerates into a statement about the drift and stops seeing the actuator at all.

Parameters:

Name	Type	Description	Default
alpha	float	the class-K gain of the barrier condition, matching chc.plan.certify_safety.	1.0
tolerance	float	grid-fraction slack when comparing the tube to {h >= 0}, absorbing the Lax-Friedrichs dissipation that erodes the zero level set by O(dx).	0.02

Raises:

Type	Description
ValueError	as backward_reachable_tube does, and on an alpha that is not finite or a tolerance outside [0, 1].

higher_order_barrier_gap(barrier, drift, b_matrix, *, lower, upper, resolution=(81, 81), horizon=1.0, steps=200, u_max=1.0, radius=0.0, alpha1=1.0, alpha2=1.0, tolerance=0.02)

Second-order (exponential/higher-order CBF) robust condition against the same tube.

The condition asks max_u min_{Delta_B} grad psi1 . (f + (B + Delta_B) u) >= -alpha2 psi1 on the working set {h >= 0} & {psi1 >= 0}, with psi1 = grad h . f + alpha1 h and the same operator-norm identification ball as §40 -- so the margin is robust_hamiltonian with grad psi1 in place of grad h, and the §40 zero-action rule applies to the LIFTED channel: once radius * ||grad psi1|| >= ||B^T grad psi1|| the verdict collapses to the drift's, now visibly rather than silently. If the condition holds everywhere on the working set, that set is forward invariant (Xiao & Belta's HOCBF argument with the worst-case effect substituted), so the tube must contain it -- ok checks exactly that and stays honest under Lax-Friedrichs erosion via tolerance.

Scope: PURE relative degree 2. Where B^T grad h != 0 the true hdot has a control term that psi1 drops, and this condition is a different certificate, not a sharper one -- use barrier_reachability_gap there.

Raises:

Type	Description
ValueError	as backward_reachable_tube does, and on an alpha1 or alpha2 that is not finite or a tolerance outside [0, 1].