From 4fbca0899a4407bd560934261cdedae19ad6019b Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 9 Mar 2026 17:29:33 -0400 Subject: [PATCH] Editorial pass: tactical sentence improvements (Gopen), operational flow, Heilmeier alignment --- 1-goals-and-outcomes/v1.tex | 2 +- 2-state-of-the-art/v2.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index 9d88147..135268c 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -11,7 +11,7 @@ Extensively trained human operators control nuclear plants today. They follow de This reliance on human operators prevents autonomous control. It creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face staffing costs per megawatt far exceeding those of conventional plants. This threatens economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators. % APPROACH PARAGRAPH Solution -Formal methods unify with control theory to produce hybrid control systems that are correct by construction. +This research unifies formal methods with control theory to produce hybrid control systems correct by construction. % Rationale Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements. However, they cannot verify the continuous dynamics governing transitions. Control theory verifies continuous behavior. However, it cannot prove discrete switching correctness. Both are required for end-to-end correctness. % Hypothesis diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 75c6201..ac12638 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -159,7 +159,7 @@ design loop for complex systems like nuclear reactor startup procedures. This section addressed two Heilmeier questions: What has been done? What are the limits of current practice? -\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability limitations. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally. +\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability constraints. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally. \textbf{What are the limits of current practice?} A clear verification gap emerges: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics—never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.