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