PWR-HYBRID-3/reachability

Reachability

Continuous-mode verification for the PWR_HYBRID_3 hybrid controller.

Soundness status: APPROXIMATE

The current linear-reach results are not a sound reach tube for the physical plant. They are sound over-approximations of the linearized closed-loop system (A_{\mathrm{cl}} = A - BK around x_{\mathrm{op}}) under bounded disturbance. The linear model is itself an approximation of the nonlinear plant (../code/src/pke_th_rhs.jl), and that approximation error is not currently bounded or inflated into the tube.

Two paths to upgrade to a sound result:

1. Nonlinear reach directly — TMJets (Taylor-model integration) via ReachabilityAnalysis.jl. Currently limited to ~10-second horizons by prompt-neutron stiffness; needs a reduced-order PKE (prompt-jump approximation) to extend to mode-obligation horizons.
2. Linear reach + Taylor-remainder inflation — compute an upper bound on ||f_nl(x, u) - (A x + B u)|| over the reach set and inflate the linear tube by that bound. Cheaper, still rigorous.

Both are thesis-blocking for any safety claim. The current 5-orders-of-margin buffer (reach envelope ~0.03 K against a 5 K safety band on T_c) means linearization error would have to be huge to invalidate the conclusion — but that's vibes, not a proof.

Related open issues

• Saturation semantics. ctrl_heatup.jl uses clamp(u, u_min, u_max). Saturation is formally a 3-mode piecewise-affine system. For heatup reach this must be handled as (a) hybrid locations, or (b) proven dormant via reach on u_unsat. Not modeled in the current artifacts (operation-mode LQR saturation is dormant in practice but the proof is implicit).
• Parametric uncertainty in α_f, α_c. Real plants have α drift with burnup (~20%), boron (α_c ranges 10×), xenon. The feedback-linearization in ctrl_heatup assumes exact α; a robust treatment would make α an interval and propagate parametric reach. Currently idealized.

What's here

Per-mode only. Following the compositionality argument in the thesis: verify each continuous mode separately, let the DRC handle discrete switching.

Files:

• predicates.json — single source of truth for predicate concretizations. Three groups:

  • operational_deadbands — soft bands used by DRC for mode transitions (t_avg_above_min, t_avg_in_range, p_above_crit).
  • safety_limits — hard one-sided halfspaces (fuel centerline, trip setpoints, subcooling, heatup-rate bounds).
  • mode_invariants — inv1_holds, inv2_holds as conjunctions of safety limits.
  • mode_boundaries — per-mode X_{\mathrm{entry}}, X_{\mathrm{safe}}, X_{\mathrm{exit}}, T_{\min}, T_{\max}.

• WALKTHROUGH.md — standalone document explaining the reach-obligation taxonomy, per-mode entry/exit definitions, current results, soundness status. Read this for the full story.

The reach code itself lives in ../code/:

• ../code/src/reach_linear.jl — hand-rolled box reach propagator.
• ../code/src/load_predicates.jl — reads predicates.json.
• ../code/scripts/reach_operation.jl — operation-mode linear reach.
• ../code/scripts/barrier_lyapunov.jl — Lyapunov barrier attempt.
• ../code/scripts/barrier_compare_OL_CL.jl — OL vs CL comparison.
• ../code/scripts/reach_heatup_nonlinear.jl — TMJets nonlinear reach (heatup, saturation-disabled, 10-second horizon cap).

Running

cd code
julia --project=. scripts/reach_operation.jl
julia --project=. scripts/barrier_lyapunov.jl
julia --project=. scripts/barrier_compare_OL_CL.jl
julia --project=. scripts/reach_heatup_nonlinear.jl

Results save here as *.mat (gitignored).

What this does NOT do yet

• Any sound reach tube (see top of this file).
• Nonlinear reach on horizons > 10 s (needs reduced-order PKE).
• Shutdown, scram, initialization reach.
• Hybrid-system level verification (mode switching validity).
• Parametric robustness to α_f, α_c drift.
• Polytopic or SOS barriers — the canonical quadratic Lyapunov barrier fails structurally on this plant (see WALKTHROUGH.md and the OL-vs-CL comparison script).