danesabo/Thesis
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Editorial pass: tactical sentence improvements (Gopen), operational flow, Heilmeier alignment

Browse Source
This commit is contained in:
Split 2026-03-09 17:29:33 -04:00
parent fa4936cb28
commit 4fbca0899a
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
1-goals-and-outcomes/v1.tex
View File

@ -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. 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 % 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 % 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. 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 % Hypothesis

2
2-state-of-the-art/v2.tex
View File

@ -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? 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. \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.