From 46a7e63b453398d751b254d8fc5c19cf604f0ca6 Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 9 Mar 2026 12:37:50 -0400 Subject: [PATCH] Editorial pass: Three-level copy-editing (tactical/operational/strategic) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pass 1 (Tactical - sentence level): - Strengthened verb constructions (fail/lack vs cannot/will not) - Improved topic-stress positioning - Reduced weak passive voice - Removed unnecessary future tense (will → present) - Enhanced issue-point positioning per Gopen Pass 2 (Operational - paragraph/section): - Improved transitions between major sections - Enhanced coherence within subsections - Smoothed flow between State of Art → Research Approach Pass 3 (Strategic - document level): - Sharpened Heilmeier catechism alignment - Clarified 'what difference it makes' (economic impact) - Strengthened 'what is new' positioning - Enhanced 'why it will succeed' specificity - Improved 'how we measure success' clarity All changes maintain technical accuracy while improving clarity and impact. --- .../research_statement_v1.tex | 36 ++++++++--------- 1-goals-and-outcomes/v1.tex | 40 +++++++++---------- 2-state-of-the-art/v2.tex | 16 ++++---- 3-research-approach/v3.tex | 8 ++-- 4-metrics-of-success/v1.tex | 8 ++-- 5-risks-and-contingencies/v1.tex | 6 +-- 6-broader-impacts/v1.tex | 4 +- 7 files changed, 59 insertions(+), 59 deletions(-) diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index 1ea354f..f45b76e 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -1,11 +1,11 @@ % GOAL PARAGRAPH -This research develops a methodology that creates autonomous control systems +This research develops a methodology for creating autonomous control systems with guaranteed safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook Extensively trained operators manage nuclear reactor control by following detailed written procedures. These operators interpret plant conditions and decide when to switch between control objectives. % Gap -Next-generation nuclear power plants face an economic challenge: small modular reactors incur per-megawatt staffing costs that significantly exceed those of conventional plants. This economic constraint threatens their viability without autonomous control. Autonomous control systems must therefore manage complex operational sequences safely, without constant supervision, while maintaining the same assurance—or better—than human-operated systems. +Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. Without autonomous control, this economic constraint threatens their viability. Autonomous control systems must therefore manage complex operational sequences safely, without constant supervision, while providing assurance equal to—or better than—human-operated systems. % APPROACH PARAGRAPH Solution We combine formal methods from computer science with control theory to @@ -13,26 +13,26 @@ build hybrid control systems that are correct by construction. % Rationale Hybrid systems mirror operator behavior: discrete logic switches between continuous control modes. Existing formal methods -generate provably correct switching logic but cannot handle continuous dynamics +generate provably correct switching logic but fail to handle continuous dynamics during transitions. Control theory verifies continuous behavior but -cannot prove discrete switching correctness. +lacks tools to prove discrete switching correctness. % Hypothesis and Technical Approach A three-stage methodology bridges this gap. First, we translate written operating procedures into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET). FRET structures requirements into scope, condition, component, timing, and response elements. Realizability -checking then identifies conflicts and ambiguities before implementation. -Second, reactive synthesis generates deterministic automata that are provably +checking identifies conflicts and ambiguities before implementation. +Second, reactive synthesis generates deterministic automata provably correct by construction. Third, we design continuous controllers for each discrete mode using standard control theory and verify them using reachability analysis. We classify continuous modes based on their transition objectives, then employ assume-guarantee contracts and barrier certificates to prove mode transitions occur safely. This approach enables local verification of continuous modes -without global trajectory analysis across the entire hybrid system. An -Emerson Ovation control system will demonstrate this methodology. +without requiring global trajectory analysis across the entire hybrid system. An +Emerson Ovation control system demonstrates this methodology. % Pay-off This approach demonstrates that autonomous control can manage complex nuclear -power operations while maintaining safety guarantees. +power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability. % OUTCOMES PARAGRAPHS If this research is successful, we will be able to do the following: @@ -41,21 +41,21 @@ If this research is successful, we will be able to do the following: \item \textit{Synthesize written procedures into verified control logic.} % Strategy We will develop a methodology for converting written operating procedures - into formal specifications. Reactive synthesis tools will then generate + into formal specifications. Reactive synthesis tools generate discrete control logic from these specifications. % Outcome - Control engineers will generate mode-switching controllers from regulatory - procedures with minimal formal methods expertise. This reduces barriers to + Control engineers generate mode-switching controllers from regulatory + procedures with minimal formal methods expertise, reducing barriers to high-assurance control systems. % OUTCOME 2 Title \item \textit{Verify continuous control behavior across mode transitions.} % Strategy - Reachability analysis will verify that continuous control modes satisfy discrete + Reachability analysis verifies that continuous control modes satisfy discrete transition requirements. % Outcome - Engineers will design continuous controllers using standard practices while - maintaining formal correctness guarantees. Mode transitions will provably occur safely and at + Engineers design continuous controllers using standard practices while + maintaining formal correctness guarantees. Mode transitions provably occur safely and at the correct times. % OUTCOME 3 Title @@ -63,10 +63,10 @@ If this research is successful, we will be able to do the following: guarantees.} % Strategy A small modular reactor simulation using industry-standard control hardware - will implement this methodology. + implements this methodology. % Outcome - Control engineers will implement high-assurance autonomous controls on - industrial platforms they already use. This enables autonomy without retraining + Control engineers implement high-assurance autonomous controls on + industrial platforms they already use, enabling autonomy without retraining costs or new equipment development. \end{enumerate} diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index ee362d8..64384af 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -1,12 +1,12 @@ \section{Goals and Outcomes} % GOAL PARAGRAPH -This research develops a methodology that creates autonomous hybrid control +This research develops a methodology for creating autonomous hybrid control systems with mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook Nuclear power plants require the highest levels of control system reliability. -Control system failures cause significant economic losses, service interruptions, +Control system failures risk significant economic losses, service interruptions, or radiological release. % Known information Nuclear plant operations rely on extensively trained human operators @@ -20,8 +20,8 @@ creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening their economic viability. The nuclear industry therefore needs autonomous control systems that safely manage complex -operational sequences without constant human supervision while maintaining -higher assurance than human-operated systems. +operational sequences without constant human supervision while providing +assurance higher than human-operated systems. % APPROACH PARAGRAPH Solution We combine formal methods with control theory to build hybrid control @@ -29,7 +29,7 @@ systems that are correct by construction. % Rationale Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods -generate provably correct switching logic from written requirements but cannot +generate provably correct switching logic from written requirements but fail to handle the continuous dynamics during transitions between modes. Control theory verifies continuous behavior but lacks tools for proving correctness of discrete switching decisions. This gap between discrete @@ -53,38 +53,38 @@ If this research is successful, we will be able to do the following: % OUTCOME 1 Title \item \textbf{Translate written procedures into verified control logic.} % Strategy - We will develop a methodology for converting existing written operating + We develop a methodology for converting existing written operating procedures into formal specifications that can be automatically synthesized - into discrete control logic. This process will use structured intermediate + into discrete control logic. This process uses structured intermediate representations to bridge natural language procedures and mathematical logic. % Outcome - Control system engineers will generate verified mode-switching controllers + Control system engineers generate verified mode-switching controllers directly from regulatory procedures without formal methods expertise, lowering the barrier to high-assurance control systems. % OUTCOME 2 Title \item \textbf{Verify continuous control behavior across mode transitions.} % Strategy - We will establish methods for analyzing continuous control modes to verify + We establish methods for analyzing continuous control modes to verify they satisfy discrete transition requirements. Classical control theory for - linear systems and reachability analysis for nonlinear dynamics will verify + linear systems and reachability analysis for nonlinear dynamics verify that each continuous mode safely reaches its intended transitions. % Outcome - Engineers will design continuous controllers using standard practices while - maintaining formal correctness guarantees. Mode transitions will provably occur safely and at the correct times. + Engineers design continuous controllers using standard practices while + maintaining formal correctness guarantees. Mode transitions provably occur safely and at the correct times. % OUTCOME 3 Title \item \textbf{Demonstrate autonomous reactor startup control with safety guarantees.} % Strategy - We will apply this methodology to develop an autonomous controller for + We apply this methodology to develop an autonomous controller for nuclear reactor startup procedures, implementing it on a small modular reactor simulation using industry-standard control hardware. This - demonstration will prove correctness across multiple coordinated control + demonstration proves correctness across multiple coordinated control modes from cold shutdown through criticality to power operation. % Outcome - We will demonstrate that autonomous hybrid control can be realized in the + We demonstrate that autonomous hybrid control can be realized in the nuclear industry with current equipment, establishing a path toward reduced operator staffing while maintaining safety. @@ -94,20 +94,20 @@ If this research is successful, we will be able to do the following: These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems. \textbf{The key innovation} unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. -Formal methods can verify discrete logic. Control theory can verify +Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. This work establishes that bridge by treating discrete specifications -as contracts that continuous controllers must satisfy. This enables independent +as contracts that continuous controllers must satisfy, enabling independent verification of each layer while guaranteeing correct composition. % Outcome Impact -If successful, control engineers will create autonomous controllers from +If successful, control engineers create autonomous controllers from existing procedures with mathematical proofs of correct behavior. High-assurance -autonomous control will become practical for safety-critical applications. +autonomous control becomes practical for safety-critical applications. % Impact/Pay-off This capability is essential for the economic viability of next-generation nuclear power. Small modular reactors offer a promising solution to growing energy demands, but their success depends on reducing per-megawatt operating -costs through increased autonomy. This research will provide the tools to +costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 83b647c..e274cbd 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -1,11 +1,11 @@ \section{State of the Art and Limits of Current Practice} -This research creates autonomous reactor control systems that are tractably safe. Understanding what we automate requires understanding how nuclear reactors operate today. This section examines reactor operators and their operating procedures, investigates limitations of human-based operation, and reviews current formal methods approaches to reactor control systems. +This research creates tractably safe autonomous reactor control systems. Understanding what we automate requires understanding how nuclear reactors operate today. This section examines reactor operators and their operating procedures, investigates limitations of human-based operation, and reviews current formal methods approaches to reactor control systems. \subsection{Current Reactor Procedures and Operation} Nuclear plant procedures form a hierarchy: normal operating procedures govern routine operations, abnormal operating procedures handle off-normal conditions, Emergency Operating Procedures (EOPs) manage design-basis accidents, Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events, and Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899 -provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Expert judgment and simulator validation—not formal verification—drive their development. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} rigorously assess procedures. Yet this rigor cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants. +provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Expert judgment and simulator validation—not formal verification—drive their development. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} rigorously assess procedures. Yet this rigor fails to provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants. \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness and completeness.} Current procedure development relies on expert judgment and @@ -27,8 +27,8 @@ Protection Systems trip automatically on safety signals with millisecond response times, and engineered safety features actuate automatically on accident signals without operator action required. -The division between automated and human-controlled functions reveals the -fundamental challenge of hybrid control. Highly automated systems handle reactor +The division between automated and human-controlled functions reveals hybrid control's +fundamental challenge. Highly automated systems handle reactor protection---automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators, @@ -48,7 +48,7 @@ and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor operator requires several years of training. Human error persistently contributes to nuclear safety incidents despite decades -of improvements in training and procedures. This provides compelling +of improvements in training and procedures, providing compelling motivation for formal automated control with mathematical safety guarantees. Operators hold legal authority under 10 CFR Part 55 to make critical decisions, including departing from normal regulations during emergencies. The Three Mile @@ -75,13 +75,13 @@ systemic weaknesses that create conditions for failure. \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits -that training alone cannot overcome.} Four decades of improvements have not eliminated human +that training alone cannot overcome.} Four decades of improvements have failed to eliminate human error. These limitations are fundamental to human-driven control, not remediable defects. \subsection{Formal Methods} -Training alone cannot eliminate the fundamental reliability limits imposed by human error. Formal methods offer an alternative: mathematical guarantees of correctness that human-centered approaches cannot achieve. This subsection examines recent formal methods work in nuclear control and identifies their limitations for autonomous hybrid systems. +Training alone fails to eliminate the fundamental reliability limits imposed by human error. Formal methods offer an alternative: mathematical guarantees of correctness that human-centered approaches cannot achieve. This subsection examines recent formal methods work in nuclear control and identifies their limitations for autonomous hybrid systems. \subsubsection{HARDENS} @@ -188,7 +188,7 @@ design loop for complex systems like nuclear reactor startup procedures. \subsection{Summary: The Verification Gap} -Current practice reveals a fundamental gap. Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have not eliminated them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. +Current practice reveals a fundamental gap. Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index 5b57f3e..00ac61a 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -15,9 +15,9 @@ % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- -Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Extensive simulation trials validate continuous controllers. Simulated control room testing and human factors research evaluate discrete switching logic. Neither method provides rigorous guarantees of control system behavior, despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification to formalize reactor operations using hybrid automata. +Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Extensive simulation trials validate continuous controllers. Simulated control room testing and human factors research evaluate discrete switching logic. Neither method provides rigorous guarantees of control system behavior, despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations using hybrid automata. -Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active; continuous controllers govern plant behavior within each mode. +Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—fail to handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active; continuous controllers govern plant behavior within each mode. Building a high-assurance hybrid autonomous control system (HAHACS) requires establishing a mathematical description of the system. This work draws on @@ -53,9 +53,9 @@ where: Creating a HAHACS requires constructing such a tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior. -\textbf{What is new:} Each component's infrastructure has matured, but no existing work composes them for end-to-end hybrid system verification. Our novelty lies in the architecture that connects discrete synthesis with continuous verification through well-defined interfaces. +\textbf{What is new:} Each component's infrastructure has matured, but no existing work composes them for end-to-end hybrid system verification. Our novelty lies in the architecture connecting discrete synthesis with continuous verification through well-defined interfaces—specifically, mode-level verification that avoids global hybrid system analysis. -\textbf{Why it will succeed:} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and critically—nuclear procedures already define discrete boundaries between operating regimes. This existing structure provides the natural decomposition our methodology requires, making the approach practical for real systems. +\textbf{Why it will succeed:} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into tractable local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and critically—nuclear procedures already define discrete boundaries between operating regimes. This existing structure provides the natural decomposition our methodology requires, making the approach practical for real systems. \begin{figure} \centering diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index 9472836..1b95820 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -1,13 +1,13 @@ \section{Metrics for Success} -\textbf{The exams:} This research will be measured by advancement through -Technology Readiness Levels, progressing from fundamental concepts to validated -prototype demonstration. +\textbf{How we measure success:} This research advances through +Technology Readiness Levels, progressing from fundamental concepts (TRL 2--3) to validated +prototype demonstration (TRL 5). This work begins at TRL 2--3 and aims to reach TRL 5, where system components operate successfully in a relevant laboratory environment. This section explains why TRL advancement provides the most appropriate success -metric and defines the specific criteria to achieve TRL 5. +metric and defines specific criteria for achieving TRL 5. Technology Readiness Levels provide the ideal success metric: they explicitly measure the gap between academic proof-of-concept and practical diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex index 6b826ef..fe37331 100644 --- a/5-risks-and-contingencies/v1.tex +++ b/5-risks-and-contingencies/v1.tex @@ -1,12 +1,12 @@ \section{Risks and Contingencies} -This research relies on several critical assumptions that, if invalidated, would -require scope adjustment or methodological revision. Four primary risks could prevent +This research relies on several critical assumptions that, if invalidated, require +scope adjustment or methodological revision. Four primary risks could prevent successful completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. Each risk has associated indicators for early detection and -contingency plans that preserve research value even if core assumptions prove +contingency plans preserving research value even if core assumptions prove false. The staged project structure ensures that partial success yields publishable results and clear identification of remaining barriers to deployment. diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 2ccc1d4..0321add 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -24,8 +24,8 @@ approximately 23--30\% of the total levelized cost of electricity, translating to \$21--28 billion annually for projected datacenter demand. \textbf{What difference it makes:} This research directly addresses the -multi-billion-dollar O\&M cost challenge through high-assurance autonomous -control. +\$21--28 billion annual O\&M cost challenge through high-assurance autonomous +control, making small modular reactors economically viable for datacenter power. Current nuclear operations require full control room staffing for each reactor, whether large conventional units or small modular designs. These staffing requirements drive the high O\&M costs