diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index 2a461fd..3208cf5 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -78,7 +78,9 @@ costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. -These three outcomes establish a complete methodology from regulatory documents to deployed systems. This proposal follows the Heilmeier Catechism, with each section explicitly answering its assigned questions. Each section begins by stating its Heilmeier questions and ends by summarizing its answers, ensuring both local clarity and global coherence: +These three outcomes establish a complete methodology from regulatory documents to deployed systems. + +This proposal follows the Heilmeier Catechism. Each section explicitly answers its assigned questions. Each section begins by stating its Heilmeier questions and ends by summarizing its answers, ensuring both local clarity and global coherence: \begin{itemize} \item \textbf{Section 2 (State of the Art):} What has been done? What are the limits of current practice? \item \textbf{Section 3 (Research Approach):} What is new? Why will it succeed? diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 65dc35f..f0e4784 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -27,9 +27,9 @@ This division between automated and human-controlled functions reveals the funda \subsection{Human Factors in Nuclear Accidents} -Procedures lack formal verification despite rigorous development—but this represents only half the reliability challenge. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly. Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. +Procedures lack formal verification despite rigorous development—but this represents only half the reliability challenge. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly. -Procedures define what to do; human operators determine when and how. This determination introduces persistent failure modes that training alone cannot eliminate. +Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how. This determination introduces persistent failure modes that training alone cannot eliminate. Current-generation nuclear power plants employ over 3,600 active NRC-licensed reactor operators in the United States~\cite{operator_statistics}. These @@ -55,11 +55,11 @@ limitations are fundamental to human-driven control, not remediable defects. \subsection{Formal Methods} -The previous two subsections revealed two critical limitations of current practice: procedures lack formal verification despite rigorous development processes, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. +The previous two subsections revealed two critical limitations of current practice. First: procedures lack formal verification despite rigorous development processes. Second: human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. -Training and procedural improvements cannot solve these problems—they are fundamental limitations, not remediable defects. Formal methods might offer a solution by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems? +Training and procedural improvements cannot solve these problems. They are fundamental limitations, not remediable defects. Formal methods might offer a solution by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems? -Even the most advanced formal methods applications in nuclear control leave a critical verification gap. This subsection examines two approaches that illustrate this gap: HARDENS, which verified discrete logic without continuous dynamics, and differential dynamic logic, which handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses. +Even the most advanced formal methods applications in nuclear control leave a critical verification gap. This subsection examines two approaches that illustrate this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap my research addresses. \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control} diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index f54fe5a..8adb013 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -273,7 +273,7 @@ Reactive synthesis has proven successful in robotics, avionics, and industrial c Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications. -Having established how discrete mode-switching logic synthesizes from procedures, the question becomes: what executes within each discrete mode? The next subsection addresses continuous control modes and their verification. +The discrete mode-switching logic now synthesizes from procedures. But what executes within each discrete mode? The next subsection addresses continuous control modes and their verification. %%% NOTES (Section 3): % - Mention computational complexity of synthesis (doubly exponential worst case) diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index 5027894..813f294 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -10,7 +10,7 @@ Technology Readiness Levels provide the ideal success metric. They explicitly me Academic metrics like papers published or theorems proved fail to capture practical feasibility. Empirical metrics like simulation accuracy or computational speed fail to demonstrate theoretical rigor. TRLs measure both simultaneously. -Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while progressively demonstrating practical feasibility. The system moves from individual components to integrated hardware testing. Formal verification must remain valid throughout this progression. The proofs must compose as the system scales. +Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while progressively demonstrating practical feasibility. The system moves from individual components to integrated hardware testing. Two requirements constrain this progression. First: formal verification must remain valid throughout. Second: the proofs must compose as the system scales. The nuclear industry requires extremely high assurance before deploying new control technologies. Demonstrating theoretical correctness alone proves