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. ~11 content slides + title + Q&A. ~1.5–2 min/slide, heavier on slides 1, 9, 10. Buffer ~1 min.

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: procedures → FRET → LTL/AIGER → DRC → continuous gotcha → plant model → reach with stiffness wall → prompt-jump fix (with validity-as-an- invariant) → two sound nonlinear results → seam.

Design principles:

• Plots over bullets. Every result slide anchors on one figure.
• Physical intuition before math. Reactor basics in passing, not as a tutorial.
• Honest limitations 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 + scopes of control (2-frame animation)

Assertion (frame 1): Nuclear reactor operation is dominated by humans following procedures, and the procedures themselves have no formal verification.

Evidence (frame 1): Full-bleed photograph of a control room — analog gauges, paper procedures on the desk, two operators.

Speak (frame 1): Self + advisor + NRC fellowship. The hook: most plants are run by humans following paper procedures. We've been engineering humans out of the loop for forty years by making the procedures more and more prescriptive — but the procedures themselves are written natural language. We rely on humans to follow them faithfully and on tradition to keep them correct. (Soften: "running a nuclear reactor is well-understood" — the procedures are a knowledge-engineering artifact built over decades.)

Assertion (frame 2): Plant control decomposes into three scopes — strategic, operational, tactical — and formal methods most naturally land on the operational scope.

Evidence (frame 2): Photo slides left to make room for a 3-tier pyramid on the right:

            ┌──────────────────┐
            │   STRATEGIC      │  start it up / shut it down (hours-days)
            └──────────────────┘
          ┌──────────────────────┐
          │     OPERATIONAL       │  heat up / run / scram (minutes-hours)
          └──────────────────────┘
        ┌──────────────────────────┐
        │       TACTICAL            │  rod motion, valve actuation (seconds)
        └──────────────────────────┘

Speak (frame 2): Strategic = mission-level decisions, operator authority. Tactical = millisecond-scale rod and valve commands, classical control. The operational middle is where the procedures live — "if cold and ready, heat up; if at temperature and critical, switch to power operation; if any trip condition, scram." This middle is where formal methods can do their best work because the dynamics are slow enough to verify and the logic is discrete enough to specify. The thesis lives here.

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

Figures to make: control-room photo (license-clean source TBD); pyramid diagram (Tikz, simple).

---

Slide 2 — FRET requirements: capture the procedure, find the seam

Assertion: FRET turns natural-language operational procedures into LTL, and reveals the seam where a discrete predicate lands on a continuous state.

Evidence: A two-row figure. Top row: a FRET requirement card.

PWR-2001: 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.

Bottom row: the corresponding LTL, with one of the boolean atoms (t_avg_in_range) circled in red. Side annotation:

t_avg_in_range ≡ |T_c − T_c0| ≤ 2.78 °C (this is a half-space on a continuous state)

Speak: FRET writes requirements like "if A then next B" in a restricted natural-language template. Spot's compiler (FRET → LTL) checks that the requirement set is realizable — there exists a discrete controller that satisfies all requirements. Here's the part that matters for hybrid systems: some of these boolean atoms aren't really boolean. t_avg_in_range is a halfspace on a continuous state vector. The discrete controller treats it as true-or-false; the continuous plant has to actually make it true under whatever dynamics apply. That gap — between the discrete requirement and the continuous truth-maker — is the seam. The whole rest of the talk is about discharging that seam.

Reference: fret-pipeline/pwr_hybrid_3.json, reachability/predicates.json.

Figures to make: FRET-card visual + LTL panel.

---

Slide 3 — From LTL to a synthesized discrete controller

Assertion: Reactive synthesis (Spot/ltlsynt) compiles the LTL into an AIGER circuit — the minimal correct discrete controller — automatically.

Evidence: Pipeline figure. Three boxes left-to-right:

[ FRET requirements ]  →  [ LTL formula ]  →  [ AIGER circuit ]
   (realizability check)    (ltlsynt synthesis)   (.aag file)

Below the third box: a thumbnail of the synthesized DRC state diagram (fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png).

Speak: Two distinct things are happening. FRET's realizability check says "your requirements are mutually consistent and a controller exists." Spot/ltlsynt's reactive synthesis actually builds that controller — it solves a parity game on the LTL formula and emits an AIGER circuit, the minimal-state controller satisfying the spec. We then extract the state diagram from the AIGER. This is well-established machinery in the formal-methods world; our contribution is applying it to reactor operating procedures, which is a formal-methods-free domain historically.

Reference: fret-pipeline/scripts/fret_to_synth.py, circuits/PWR_HYBRID_3_DRC.aag.

---

Slide 4 — The synthesized DRC for PWR_HYBRID_3

Assertion: The discrete controller for our running example has four modes and seven transitions, all driven by predicates on the continuous state.

Evidence: Full-slide DRC state diagram from fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png. Annotated with transition guards, e.g. t_avg_in_range ∧ p_above_crit ∧ inv1_holds on the heatup→operation arrow.

Speak: Cold shutdown, heatup, power operation, scram. Every transition is gated by a conjunction of atomic predicates. Each predicate is a halfspace on the 10-dimensional plant state. So the discrete controller's correctness as a hybrid system depends entirely on whether the continuous plant trajectory makes the right predicates true at the right moments. Which brings us to the gotcha.

Reference: fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png.

---

Slide 5 — The continuous gotcha

Assertion: A correct discrete controller does not imply a correct hybrid system; the continuous-side predicates have to be discharged separately.

Evidence: A simple 2-panel cartoon. Left: DRC state diagram with one transition arrow highlighted. Right: a 2D phase portrait sketch with the trajectory drifting outside the predicate region — controller fires the transition based on logic, but the plant isn't actually where the logic thinks it is.

Speak: The DRC is correct as a discrete object — it satisfies all the LTL requirements given its predicate inputs. But predicates like t_avg_in_range are continuous-state halfspaces. If the plant's actual trajectory leaves that halfspace while the controller still believes it's inside, the discrete proof is meaningless. We need a continuous-side proof that the plant actually inhabits the right halfspaces at the right times. That proof is per-mode and the methodology contribution of the chapter.

---

Slide 6 — The plant model: 10-state PKE + thermal-hydraulics

Assertion: A 10-state point-kinetic + lumped thermal-hydraulics PWR model is the continuous-side surrogate — faithful enough to verify, stiff enough to give us trouble.

Evidence: State-vector coupling diagram showing the chain u (rods) → ρ → n → P → T_f → T_c → T_cold → ρ_feedback, with Q_sg as a bounded disturbance on T_cold.

state x = [ n  C₁..C₆  T_f  T_c  T_cold ]
            └──prompt──┘  └─────thermal─────┘
            (Λ ≈ 10⁻⁴ s)   (τ ≈ 10–100 s)
                 ↑
            stiffness ratio ≈ 10⁵

Speak: Point-kinetic equations for neutron population and six delayed-neutron precursor groups. Three thermal nodes — fuel, average coolant, cold-leg. One control input (rod-induced reactivity). One bounded disturbance (steam-generator heat removal). Stiffness ratio of 10⁵ between prompt-neutron and thermal timescales. Flag this now — it's about to be the cliff.

Reference: code/src/pke_th_rhs.jl, journal entry 2026-04-17.

Figures to make: state-vector coupling diagram (Tikz).

---

Slide 7 — Per-mode reach-avoid obligations

Assertion: Discrete-to-continuous correctness reduces to one reach-avoid obligation per mode — equilibrium modes prove forever-invariance, transition modes prove bounded-time reach-avoid.

Evidence: Compact taxonomy:

Mode	Kind	Obligation
shutdown / operation	equilibrium	stay in safe set forever
heatup / scram	transition	from X_entry, reach X_exit in [T_min, T_max], stay safe

Below the table: a tiny phase-portrait pictogram for each kind — bowl (equilibrium) vs corridor (transition).

Speak: This is the structural insight. If every mode's obligation is discharged, the hybrid system is correct by composition — the discrete controller's transitions fire correctly because the continuous plant actually arrives at each X_exit predicate by the time the transition guard is checked. Two flavors of obligation. Two flavors of proof.

Reference: reachability/WALKTHROUGH.md §1.

---

Slide 8 — First reach attempt: stiffness wall

Assertion: Naive nonlinear reach (TMJets) caps out at ~10 seconds of horizon on the full 10-state model — orders of magnitude short of what the obligations need.

Evidence: A two-panel figure. Left: a graph of horizon achieved vs wall-clock time, asymptoting at ~10 s of plant time. Right: a one-line caption — "T_max(heatup) = 5 hr; T_max(scram) = 60 s. We're 1800× short on heatup and 6× short on scram."

Speak: TMJets is a Taylor-model integrator — produces sound over-approximations of the nonlinear reach set. Beautiful tool. But its step size is bounded by the fastest dynamics in the system, which here is the prompt-neutron timescale Λ ≈ 10⁻⁴ s. Even on a bounded reach horizon, you blow your step budget propagating Taylor models that nobody cares about, because nothing safety-relevant happens on that timescale. The stiffness ratio kills us. We need to remove the fast modes without losing soundness.

Reference: code/scripts/reach/reach_heatup_nonlinear.jl.

---

Slide 9 — Prompt-jump reduction with validity-as-an-invariant

Assertion: Singular-perturbation reduction eliminates the prompt neutronics, gives us 30× more reach horizon — and, critically, the reduction's validity condition becomes part of the safety obligation itself, not a separate hand-wave.

Evidence: Two stacked panels.

Top: the algebraic substitution.

\frac{dn}{dt} = 0 \implies n = \frac{\Lambda \sum_i \lambda_i C_i}{\beta - \rho(x)}

State drops from 10 to 9. Stiffness gone. Reach steps now bounded by thermal timescale, not prompt timescale.

Bottom: the validity condition + Tikhonov bound.

• Validity: β − ρ(x) > δ > 0 over the reach set — this is a half-space in the same vocabulary as every other safety predicate.
• Error: |x(t) − x_PJ(t)| ≤ C·Λ = O(10⁻⁴) (Tikhonov).

Speak: The trick that makes this thesis-shaped: we don't assume the prompt-jump reduction is valid — we prove it as part of the same reach obligation. The halfspace prompt_critical_margin_holds is in the per-mode invariant set right alongside the safety halfspaces. If reach discharges the invariant, it discharges both safety and the approximation's soundness. No separate validity argument. This is the formal-methods-shaped move I want the audience to take home.

Reference: code/src/pke_th_rhs_pj.jl, journal entry 2026-04-21 "Tikhonov bound", reachability/predicates.json::prompt_critical_margin_*.

---

Slide 10 — Two sound nonlinear reach proofs

Assertion: With prompt-jump, both transition modes — heatup and scram — discharge their full safety invariants over their relevant horizons.

Evidence: Side-by-side, two panels.

Left panel — heatup: tube plot from docs/figures/reach_heatup_pj_tubes.png. Caption: "300 s, all 6 inv1_holds halfspaces discharged, T_c stable at [281.05, 291.0] °C."

Right panel — scram: shutdown-margin discharge from results/reach_scram_pj_fat.mat. A bar chart of |ρ| vs the 1% Δk/k floor at T = 10, 30, 60 s. Caption: "Fat entry polytope (union of all mode envelopes). |ρ| ≈ 5%. 5× the requirement at 60 s."

Speak: Heatup: 12,932 reach-sets, 200 s wall, tube stable — T_c envelope identical at 60 s and 300 s, meaning the controller holds the state inside the tube indefinitely. Scram: from the fat entry polytope (any state the plant could be in across all modes plus LOCA), the shutdown-margin halfspace discharges at 10, 30, and 60 s with five times the NRC tech-spec margin. Both are sound for the prompt-jump-reduced plant; both inherit the O(Λ) Tikhonov error to the full plant. Two transition modes formally verified end-to-end. This is the headline result.

Limitations box: 300 s of a 5-hour T_max on heatup. Step budget is the wall; entry refinement is the path to hours.

Evidence path: code/scripts/reach/reach_heatup_pj.jl, code/scripts/reach/reach_scram_pj_fat.jl, docs/figures/reach_heatup_pj_tubes.png, results/reach_scram_pj_fat.mat.

---

Slide 11 — Composition + impact + the open seam

Assertion: Two transition modes verified, two equilibrium modes are the next step — the composition story holds, the open question is well-defined.

Evidence: Two-column layout.

Left column — what's proven (with a green check):

Mode	Status
Heatup	Sound nonlinear reach, 300 s, all 6 safety halfspaces
Scram	Sound nonlinear reach, 60 s, shutdown margin, 5× tech-spec
FRET → AIGER	Sound discrete controller, realizability checked
PJ validity	Discharged inside the same reach obligation

Right column — what's next (amber):

Open	Path
Operation mode forever-invariance	Polynomial barrier certificate (SOS) on PJ dynamics
Hot-standby forever-invariance	Same machinery, different equilibrium
Full 5-hr heatup horizon	Entry refinement (Blanchini-style)
Hardware integration	Ovation DCS, scheduled

Speak: Where this lands. Two transition modes, formally verified end-to-end — discrete controller from FRET, continuous trajectory bounded by sound nonlinear reach, validity of the reduction proven inside the same obligation. The open piece is stability proofs for the equilibrium modes — operation and hot-standby. We've started on barrier certificates to discharge those, and the machinery works on a 2D linearization, but the sound treatment on the full nonlinear plant is the next thrust. That's the work for the next several months. The composition framework holds; we're filling in cells in the matrix.

Cyber angle close: Formal verification of operational procedures is defense-in-depth for OT. Even if an attacker bypasses the comms layer and injects commands, a verified DRC plus a discharged reach-avoid envelope constrains what the physical plant can be made to do. That's an assurance axis comms-security alone can't reach.

---

Slide 12 — Q&A / acknowledgements (backup)

Assertion: (none — backup slide)

Evidence: Acknowledgements. Advisor (Cole), committee, NRC fellowship. Repo (gitea), journal PDF, thesis in progress.

Anticipated questions:

• "Why not Stateflow/Simulink?" → tool-integration story; HARDENS used Cryptol for the same reason.
• "How does this interact with ML components?" → out of scope; the pitch is no ML in the safety-critical loop.
• "What's the threat model?" → tie back to OT audience: formal methods guarantee the controller's logic and the physical plant's behavior; they do not protect comms or implementation. Defense in depth.
• "Why not just do nonlinear-SOS directly?" → the thrust starts there in the next phase; the linearized 2D version was the proof-of-concept.

---

Presentation construction notes

Slide-count vs. time budget

11 content slides + title + Q&A. Average 1.6 min/slide. Allocation:

Slide	Min	Reason
1 (anim)	2.5	Hook needs riff room
2 (FRET seam)	2.0	Audience unfamiliar; this is the central insight
3	1.5	Pipeline diagram
4	1.5	DRC walkthrough
5	1.0	Transition slide, short
6	1.5	Plant + stiffness flag
7	1.0	Taxonomy, short
8	1.5	Wall problem
9	2.0	Methodology contribution; slowest
10	2.0	Headline result
11	1.5	Closing seam
Total	18.0	+ 2 min buffer

What to build in Beamer

• Assertion-evidence template — one declarative sentence at top, centered figure below, optional 2-line speaker note in footer.
• Color coding: green = sound/proven, amber = approximate/open, red = limitation, blue = discrete-layer, purple = continuous-layer.
• 2-frame animation on slide 1 (overlay specs in Beamer).
• Inset boxes on result slides for limitations (slide 10).

Figures that need to be created or dressed up

Slide	Figure	Source / status
1	Control-room photo	License-clean source TBD
1	Strategic/operational/tactical pyramid	Tikz, fresh
2	FRET-card + LTL panel	Inkscape, fresh
3	FRET → LTL → AIGER pipeline	Tikz, fresh
4	DRC state diagram	fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png, dress up
5	DRC + drifted-trajectory cartoon	Inkscape, fresh
6	State-vector coupling diagram	Tikz, fresh
7	Equilibrium/transition pictograms	Tikz, simple
8	Horizon-vs-walltime stiffness graph	Matplotlib, fresh
9	PJ algebraic substitution + Tikhonov	LaTeX math + label
10	Heatup tubes	docs/figures/reach_heatup_pj_tubes.png, dress up
10	Scram shutdown-margin bars	Matplotlib, fresh, from reach_scram_pj_fat.mat
11	Two-column matrix	Beamer table

Cybersecurity angle to emphasize (one sentence each, distributed across slides)

• Slide 1: procedures are the OT-side analog of code; both deserve formal verification.
• Slide 2: discrete-only verification (HARDENS) leaves the seam unaddressed.
• Slide 11 close: verified physical-plant envelope is an assurance axis comms security alone cannot reach.

Things to NOT do

• Don't get lost in reactor-physics detail. One sentence per physical concept; keep the audience moving.
• Don't show code unless code structure is the point. Code screenshots are weak evidence.
• Don't oversell. Honest limitations build trust with skeptical audiences.
• Don't use more than 2 bullet points on any slide. Alley rules.
• Don't try to fit SOS barriers as their own slide. They live in slide 11 as one closing line about what's next. Cutting them out of the talk was a deliberate choice — say it once, move on.

Timing checkpoints

• Slide 4 (DRC) by minute 6.
• Slide 7 (taxonomy) by minute 9.
• Slide 9 (PJ) by minute 13.
• Slide 10 (results) by minute 16.
• Slide 11 (close) by minute 19.

Cuts made vs. April-21 outline (for reference)

• Slide 7 "Operation reach (the win)" — cut. Linear reach is a gut-check, not a headline. Demoted to one bullet on slide 11.
• Slide 8 "Quadratic Lyapunov fails" — cut. Side-quest in this arc.
• Slide 11 "Degree-4 SOS barrier" — cut as standalone slide. Folded into slide 11 "next steps" as one line.
• Slide 6 mode-taxonomy table — folded into slide 7 informally; modes appear as concrete examples (heatup, scram) when verified, not as upfront enumeration.
• Lyapunov bar-chart, per-halfspace margin table, tools-comparison diagram — all cut for time.
• Added: scopes-of-control framing on slide 1.
• Added: continuous-gotcha transition (slide 5) explicitly calling out the seam.
• Added: scram reach as headline result on slide 10 (was a follow-up bullet on April-21 limitations slide).