PWR-HYBRID-3/presentations/prelim-presentation/outline.md

Preliminary Example Presentation — Assertion-Evidence Outline

Format: Assertion-evidence (Alley). Each slide: one declarative sentence at the top, one piece of visual evidence below. No bullet soup.

Duration: 20 minutes. ~12 slides at ~1.5 min each (60 s typical, up to 2 min for the heavier ones).

Audience: OT-informed cybersecurity experts. Mostly CS, some control-theory familiarity, very little reactor-physics background. Can assume fluency with: LTL, automata, model-checking, reachability (as a concept), SMT/SAT. Must explain: PKE, reactivity, precursors, hybrid systems.

Running thread: FRET natural-language requirement → LTL → synthesized discrete controller → continuous plant → per-mode reach-avoid proof → hybrid correctness by composition.

Design principles:

• Plots over bullets. Every result slide anchors on one figure.
• Physical intuition before math. Reactor basics before PKE.
• Honest limitations boxed on each result slide. Audience are cyber folks — they respect limits more than triumphs.
• CS vocabulary by default, engineering terms defined inline.
• End with the seam, not with a victory lap. The thesis question is "how do discrete proofs and continuous proofs compose?" not "we verified everything."

---

Slide 1 — Title + hook

Assertion: Verified hybrid control for nuclear startup is a real problem with no deployed solution.

Evidence: Title block + a single image showing a control-room board of old-school analog gauges adjacent to a digital SCADA screen. Caption: "The gap we're filling."

Speak: Introduce self + advisor + NRC fellowship context. Name the problem: nuclear reactor operations are 70-80% human-error-driven at severe-accident level (Chernobyl, TMI, Fukushima all primarily human factors). Plants run on paper procedures that have no formal verification. The most advanced work to date (HARDENS, NRC-funded) verified the discrete trip system in isolation and stopped there. This talk: a preliminary example of bridging discrete requirements all the way to continuous-state safety proofs, with the seam between them as the research contribution.

Reference: thesis §2, ¶1-4. Cites Kemeny1979, Hogberg_2013, Kiniry2024.

Figures to make: find or compose the control-room image.

---

Slide 2 — The hybrid-systems gap

Assertion: Existing tools verify either discrete or continuous systems, never the seam between them.

Evidence: Two-column diagram. Left column: discrete (FRET, Spot, SAL, HARDENS, TLA+). Right column: continuous (MATLAB, Modelica, CORA, Flow*, HyTech). A dashed line between them labeled "the bridge problem."

Speak: HARDENS got to TRL 2-3 on the discrete side alone. Continuous-side reach tools exist but assume the discrete controller is given as input. What nobody has done: produce an end-to-end proof where the discrete controller's transitions actually fire in physical time on the modeled plant.

Reference: thesis §2.2 "Formal Methods", §2.2.1 HARDENS, §2.2.2 Temporal Logic. Thesis §2.3 (if exists — continuous methods).

---

Slide 3 — Running example: the PWR_HYBRID_3 controller

Assertion: Our target is a 4-mode hybrid controller that takes a PWR from hot standby to full power and back.

Evidence: The DRC state diagram (from fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png). Four nodes — shutdown, heatup, operation, scram — with labeled transitions.

Speak: One sentence of nuclear physics: a PWR has neutron population (power), coolant temperatures at three locations, and precursor concentrations that determine delayed-neutron generation. Startup is shutdown → heatup → operation; any fault triggers scram. Mode transitions gated by boolean conditions like t_avg_in_range ∧ p_above_crit ∧ inv1_holds.

Four modes means four physical behaviors the plant has to exhibit for the discrete logic to be sound. This example stresses every layer of the bridge we're building.

Evidence path: fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png, fret-pipeline/pwr_hybrid_3.json for one example requirement.

---

Slide 4 — Layer 1: FRET → LTL → synthesized DRC

Assertion: Natural-language requirements become a verified discrete controller automatically.

Evidence: One-panel figure: left half = snippet of FRET natural language ("Upon control_mode = q_heatup ∧ t_avg_in_range ∧ p_above_crit ∧ inv1_holds DRC shall at the next timepoint satisfy control_mode = q_operation"), right half = the corresponding LTL, bottom = arrow labeled ltlsynt pointing to the synthesized state-diagram node.

Speak: FRET compiles natural-language requirements into LTL (Spot ecosystem). ltlsynt turns LTL into an AIGER circuit representing the minimal correct discrete controller. This is well-trodden ground in CS-land; our contribution is using it on reactor operating procedures — so far a formal-methods-free domain.

Evidence path: fret-pipeline/README.md, pwr_hybrid_3.json sample requirement, fret-pipeline/circuits/PWR_HYBRID_3_DRC.aag AIGER circuit.

---

Slide 5 — Layer 2: the plant model

Assertion: A 10-state PKE + thermal-hydraulics model is faithful enough for reach analysis and tractable enough to actually compute with.

Evidence: The state-vector diagram: x = [n, C_1, ..., C_6, T_f, T_c, T_cold] with arrows showing the coupling — neutron balance → fuel heating → coolant transport → feedback to reactivity.

Speak: Point-kinetic equations + three thermal nodes. 10 states, 1 control input (rod worth u), 1 disturbance (steam-generator heat removal Q_sg). Stiff system: prompt-neutron timescale is 10⁻⁴ s, thermal timescales are seconds to minutes. That stiffness becomes critical later — it's what forces the singular-perturbation move.

Five controllers: one per DRC mode (shutdown, heatup, operation under P, under LQR, scram). All Julia, all in code/src/ + code/controllers/.

Evidence path: code/src/pke_th_rhs.jl, journal/journal.pdf entry 2026-04-17 for derivation.

Figures to make: state-vector coupling diagram (can be ASCII → inkscape).

---

Slide 6 — Layer 3: the reach-avoid obligation per mode

Assertion: Discrete correctness transfers to continuous correctness via one reach-avoid obligation per mode.

Evidence: Taxonomy table from reachability/WALKTHROUGH.md:

Mode	Kind	Obligation
shutdown	equilibrium	stay in X_safe forever
heatup	transition	from X_entry, reach X_exit in [T_min, T_max] while maintaining inv1
operation	equilibrium	stay in X_safe forever under bounded Q_sg
scram	transition	from any mode, drive n safely subcritical in T_max

Speak: This is the structural insight. Equilibrium modes → forever-invariance proofs. Transition modes → reach-avoid proofs with time budgets. The DRC transitions fire iff the reach set enters the right exit predicate. If every mode's obligation is discharged, the hybrid system is correct by composition. The methodological contribution of the chapter.

Reference: reachability/WALKTHROUGH.md §1, reachability/predicates.json → mode_boundaries.

---

Slide 7 — Operation mode: discharge all 6 safety halfspaces (the win)

Assertion: Under LQR feedback and ±15% Q_sg variation, the operation-mode reach tube discharges every safety halfspace with orders of magnitude of margin.

Evidence: The two-panel figure docs/figures/reach_operation_tubes.png. Left: temperature tubes (T_c, T_hot, T_cold) overlaid; the near-zero width of T_c visually demonstrates LQR contraction. Right: ΔT_core tube with a right-axis in MW showing the power is tight around nominal.

Per-halfspace margin table (inset or second slide if space allows):

Halfspace	Limit	Reach max	Margin
fuel_centerline	1200 °C	328.9	+871 K
t_avg_high_trip	320 °C	308.4	+11.6 K
n_high_trip	1.15	1.012	+0.14

Speak: LQR contracts the regulated direction (T_c) from 0.1 K to 0.03 K halfwidth. Uncontrolled directions (precursors) expand but don't appear in any safety predicate. Tightest margin is the high-flux trip at 12% headroom.

Limitations box: linear-reach of a nonlinear plant — approximate, not sound yet for the physical plant. That's what the next slides address.

Evidence path: code/scripts/reach/reach_operation.jl, docs/figures/reach_operation_tubes.png.

---

Slide 8 — Quadratic Lyapunov barrier fails structurally

Assertion: The canonical quadratic Lyapunov barrier cannot certify this plant — even with LQR inside the barrier — because of plant anisotropy.

Evidence: Bar chart comparing open-loop vs LQR-closed-loop Lyapunov bound on n_high_trip direction: OL is 27 million × nominal, CL is 1,242 × nominal. Title: "LQR helps 20,000× but both bounds are physically meaningless."

Speak: Plant has prompt timescale 10⁻⁴ s vs thermal timescale ~10 s. Lyapunov matrix P inherits that 10⁴ spread. Resulting ellipsoid stretches obscenely along the fast directions when projected to physical coordinates. No amount of controller tuning fixes this — it's set by the plant's own physics. The ellipsoid geometry cannot match the slab-shaped safe region. This is the motivation for polynomial (SOS) or polytopic barriers.

Reference: code/scripts/barrier/barrier_compare_OL_CL.jl, journal entry 2026-04-20 (evening).

---

Slide 9 — Prompt-jump reduction makes nonlinear reach tractable

Assertion: Singular-perturbation reduction of the fast neutronics gives us 30× more reach horizon and a rigorous O(Λ) error bound via Tikhonov.

Evidence: Side-by-side: left panel = validate_pj_heatup.png (empirical: PJ and full-state trajectories overlay perfectly over 50 minutes). Right panel = the Tikhonov bound written out mathematically:

|x(t) - x_{\mathrm{PJ}}(t)| \leq C \cdot \Lambda = \mathcal{O}(10^{-4})

Speak: Setting dn/dt = 0 and solving algebraically for n gives us n = Λ·Σλᵢ·Cᵢ / (β - ρ). State drops from 10 to 9, removes the Λ⁻¹ stiffness. Reach tool (TMJets) can take steps on thermal timescale instead of prompt timescale.

The magic: we prove the PJ approximation's validity condition (β - ρ > 0 with margin) as part of the same reach obligation via the prompt_critical_margin_heatup halfspace in inv1_holds. No hand-waving — the reach machinery proves both the safety claim and the approximation's soundness together.

Evidence path: code/src/pke_th_rhs_pj.jl, code/scripts/sim/validate_pj.jl, journal/ entry 2026-04-21 "Tikhonov bound".

---

Slide 10 — First sound nonlinear heatup reach (the second win)

Assertion: With PJ + a tightened entry box, nonlinear Taylor-model reach discharges all 6 inv1_holds safety halfspaces over the first 300 s of heatup.

Evidence: The four-panel reach_heatup_pj_tubes.png: temperature tubes overlaid, ΔT_core, ρ in dollars (stays between -0.25 and -0.05 — sub-prompt-critical), n decaying.

Speak: TMJets Taylor-model integration. 12,932 reach-sets, 200 s wall time. Tube stable — T_c envelope [281.05, 291.0] identical at 60 s and 300 s, meaning the controller holds the state inside the tube indefinitely. This is the first sound (modulo O(Λ) PJ error) nonlinear reach-avoid artifact for this plant.

Limitations box: 300 s of a 5-hour T_max. Step budget caps horizon; entry refinement (Blanchini-style) is the path to hours.

Evidence path: code/scripts/reach/reach_heatup_pj.jl configs/heatup/tight.toml, docs/figures/reach_heatup_pj_tubes.png.

---

Slide 11 — Degree-4 SOS polynomial barrier, a working proof of concept

Assertion: A degree-4 polynomial barrier certificate — the structure that quadratic Lyapunov cannot provide — works on the operation-mode projection.

Evidence: Equation block showing the symbolic polynomial (abbreviated — the actual 13-term polynomial from code/scripts/barrier/barrier_sos_2d.jl). Side caption: "CSDP returned OPTIMAL. Solve: ~3 seconds."

Speak: Polynomials of degree 4 can localize to slab-shaped safety regions in a way degree-2 (quadratic) cannot. The Prajna-Jadbabaie formulation: find B(x) such that B ≤ 0 on entry, B ≥ 0 on unsafe, and ∇B·f ≤ 0 on {B=0}. Sum-of-squares programming reduces this to an SDP. 2D projection proof of concept; scaling to full 10-state requires bigger solver (Mosek or SCS).

Reference: code/scripts/barrier/barrier_sos_2d.jl, journal entry 2026-04-21.

---

Slide 12 — The hybrid correctness story, assembled

Assertion: All four pieces — FRET/synthesis, plant model, reach tubes, SOS/polytopic barriers — compose into a hybrid system correctness argument.

Evidence: The composition picture. DRC state diagram at center; each DRC node has an arrow to a "per-mode obligation box" labeled with its proof artifact (tube or barrier or certificate). Arrows between nodes = transitions, labeled with the predicate polytope. Outer dashed box: "hybrid system closed-loop safety."

Speak: What's been built, what's been proven, what's next. Transition correctness between modes is the next thesis-blocking piece — each mode's X_exit has to be inside the next mode's X_entry (with margin). That's an inclusion check, not a reach — but it's the final structural piece.

---

Slide 13 — Limitations and next steps

Assertion: This is a preliminary example, not a deployable system.

Evidence: A two-column list:

What's proven	What's next
Operation mode safe under ±15% load (approximate, via linear reach)	Nonlinear operation reach (tight SOS barrier, LOCA disturbance)
Heatup PJ reach discharges all 6 safety halfspaces for 300 s	Extend to full 5-hr T_max; model steam-dump disturbance
Scram PJ n-decay monotone over 60 s	Expand X_entry(scram) to union of all mode tubes + LOCA
Degree-4 SOS barrier on 2D projection	Full 10-state SOS barrier
PJ error rigorously bounded by Tikhonov	Parametric α uncertainty; DNBR correlation

Speak: The gap from prelim example to deployable system is well-defined: more states, tighter bounds, real tech-spec numbers, hardware-in-the-loop. None of these is a research novelty unto itself — they're engineering. The research contribution is the composition framework, demonstrated end-to-end on a nontrivial running example. Phase 2 of the thesis is filling in the gaps and expanding to multiple plants.

---

Slide 14 — Questions / acknowledgements

Assertion: (none — backup slide)

Evidence: Thanks to advisor, committee, NRC fellowship. Links to: repo (gitea), journal PDF, thesis in progress.

Speak: Open for questions. Expect questions on:

• "Why not Stateflow/Simulink?" → (have answer prepared; HARDENS used Cryptol for a reason — formal tool integration matters)
• "What's the relationship to LTLMoP / DragonFly?" → (survey answer)
• "How would this interact with ML components?" → (out of scope for now, the whole pitch is no ML in safety-critical loop)
• "What's your threat model for cybersecurity?" → (tie back to OT audience — formal methods guarantee the controller's logic; they do not protect the comms layer or implementation-level vulns. Mention HARDENS' focus on "correctness of implementation" vs our focus on "correctness of specification")

---

Presentation construction notes

What to build in Beamer later

• Assertion-evidence template (one sentence at top, centered figure below).
• Consistent color coding: green for "discharged" / "proved", red for "limitation" / "gap", blue for "discrete-layer", amber for "continuous-layer".
• The composition diagram on slide 12 — this will take the most Tikz work.

Figures that need to be created or dressed up for the talk

• Slide 1: control-room visual.
• Slide 2: discrete/continuous tools comparison.
• Slide 3: use fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png.
• Slide 4: FRET → LTL → AIGER panel.
• Slide 5: 10-state coupling diagram.
• Slide 7, 10: reuse docs/figures/reach_*_tubes.png.
• Slide 8: bar chart (new, easy matplotlib).
• Slide 9: reuse validate_pj_heatup.png.
• Slide 11: latex-typeset polynomial + CSDP log snippet.
• Slide 12: composition diagram (Tikz, will take time).

Cybersecurity angle to emphasize

• The point the OT audience will care about: this kind of verification constrains what the controller can physically do. Even if an attacker gets past authentication and can inject arbitrary commands, the DRC-plus- reach-certified envelope limits how bad things can get within the physical plant. That's a different assurance axis than the usual comms-security one and complements it.
• Formal methods as defense-in-depth: they catch bugs before deployment, which reduces attack surface more than any runtime defense.
• The PJ reduction + Tikhonov approach might be of interest for other safety-critical stiff systems (power grid, aerospace).

Things to NOT do

• Don't get lost in reactor-physics detail. One sentence per physical concept; get them to the CS content fast.
• Don't show code unless it's a slide about why the code structure matters. Code screenshots are terrible evidence.
• Don't oversell. Honest limitations at every stage builds trust with a skeptical audience.
• Don't use more than 2 bullet points on any slide. Alley rules.

Timing checkpoints

• Slide 6 (mode-obligation taxonomy) by minute 8.
• Slide 10 (first nonlinear reach result) by minute 13.
• Slide 12 (composition story) by minute 17.
• Slide 13 (limitations) by minute 19.