From ab627264ac724d2bda72dba2063b4e914a04979c Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 9 Mar 2026 12:19:07 -0400 Subject: [PATCH] Editorial pass: tactical, operational, and strategic improvements Tactical (sentence-level): - Applied Gopen's principles: improved topic-stress positioning, stronger verbs - Reduced passive voice and unnecessary modifiers - Split long sentences for clarity and emphasis - Tightened redundant phrasing throughout Operational (paragraph/section): - Added explicit transitions between subsections - Improved flow within paragraphs (e.g., control scopes example) - Created parallel structure for related concepts - Enhanced coherence in State of the Art section Strategic (document-level): - Strengthened value proposition (higher vs same assurance) - Improved Heilmeier alignment (why now, what's new, why it will succeed) - Better linkage between State of the Art gap and research goals - Connected economic motivation more explicitly throughout --- .../research_statement_v1.tex | 42 +++++----- 1-goals-and-outcomes/v1.tex | 39 +++++---- 2-state-of-the-art/v2.tex | 34 ++++---- 3-research-approach/v3.tex | 83 +++++++++---------- 4-metrics-of-success/v1.tex | 4 +- 5-risks-and-contingencies/v1.tex | 4 +- 6-broader-impacts/v1.tex | 4 +- 7 files changed, 103 insertions(+), 107 deletions(-) diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index f88a000..93d0ff0 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -1,16 +1,15 @@ % GOAL PARAGRAPH This research develops a methodology for creating autonomous control systems -that guarantee safe and correct behavior through event-driven control laws. +that guarantee safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook Nuclear power plants rely on extensively trained operators who follow detailed written procedures to manage reactor control. These operators interpret plant -conditions and make critical decisions about when to switch between control +conditions and decide when to switch between control objectives. % Gap -Next-generation nuclear power plants face an economic challenge from this -reliance on human operators. Small modular reactors face per-megawatt -staffing costs significantly exceeding those of conventional plants. These +Next-generation nuclear power plants face an economic challenge: small modular reactors incur per-megawatt +staffing costs that significantly exceed those of conventional plants. These economic constraints demand autonomous control systems that can safely manage complex operational sequences without constant supervision while maintaining the same assurance as human-operated systems. @@ -19,25 +18,24 @@ same assurance as human-operated systems. We combine formal methods from computer science with control theory to build hybrid control systems that are correct by construction. % Rationale -Hybrid systems mirror how operators change control strategies: they use discrete -logic to switch between continuous control modes. Existing formal methods +Hybrid systems mirror how operators work: discrete +logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but cannot handle continuous dynamics -during transitions. Traditional control theory verifies continuous behavior but +during transitions. Control theory verifies continuous behavior but lacks tools for proving 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, enabling realizability -checking that identifies conflicts and ambiguities before implementation. +condition, component, timing, and response elements. Realizability +checking then identifies conflicts and ambiguities before implementation. Second, reactive synthesis generates deterministic automata that are provably -correct by construction for discrete mode switching logic. -Third, we develop continuous controllers for each discrete mode using standard -control theory and reachability analysis. We classify continuous modes based on +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 that mode transitions occur safely as the -deterministic automata specify. Local verification of continuous modes becomes -possible without global trajectory analysis across the entire hybrid system. An +certificates to prove that mode transitions occur safely. This enables local verification of continuous modes +without global trajectory analysis across the entire hybrid system. An Emerson Ovation control system will demonstrate this methodology. % Pay-off This approach demonstrates that autonomous control can manage complex nuclear @@ -54,18 +52,18 @@ If this research is successful, we will be able to do the following: discrete control logic from these specifications. % Outcome Control engineers will generate mode-switching controllers from regulatory - procedures with minimal formal methods expertise, reducing barriers to + procedures with minimal formal methods expertise. This reduces barriers to high-assurance control systems. % OUTCOME 2 Title \item \textit{Verify continuous control behavior across mode transitions.} % Strategy - Reachability analysis will ensure continuous control modes satisfy discrete + Reachability analysis will verify that continuous control modes satisfy discrete transition requirements. % Outcome Engineers will design continuous controllers using standard practices while - ensuring system correctness, proving that mode transitions occur safely at - the right times. + maintaining formal correctness guarantees. Mode transitions will provably occur safely and at + the correct times. % OUTCOME 3 Title \item \textit{Demonstrate autonomous reactor startup control with safety @@ -75,7 +73,7 @@ If this research is successful, we will be able to do the following: will implement this methodology. % Outcome Control engineers will implement high-assurance autonomous controls on - industrial platforms they already use, enabling autonomy without retraining - costs or developing new equipment. + industrial platforms they already use. This enables 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 43d8a60..979327d 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -9,38 +9,38 @@ Nuclear power plants require the highest levels of control system reliability. Failures can result in significant economic losses, service interruptions, or radiological release. % Known information -Currently, nuclear plant operations rely on extensively trained human operators +Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to -manage reactor control. These operators make critical decisions about when to +manage reactor control. These operators decide when to switch between different control modes based on their interpretation of plant conditions and procedural guidance. % Gap -This reliance on human operators prevents autonomous control capabilities and +This reliance on human operators prevents autonomous control and 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. % Critical Need The nuclear industry needs autonomous control systems that safely manage complex -operational sequences without constant human supervision while maintaining the -same assurance as human-operated systems. +operational sequences without constant human supervision while maintaining +higher assurance than human-operated systems. % APPROACH PARAGRAPH Solution We combine formal methods with control theory to build hybrid control systems that are correct by construction. % Rationale -Hybrid systems mirror how operators change control strategies: they use discrete -logic to switch between continuous control modes. Existing formal methods +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 -handle the continuous dynamics occurring during transitions between modes. -Traditional control theory verifies continuous behavior but lacks tools for +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 and continuous verification prevents end-to-end correctness guarantees. % Hypothesis Our approach closes this gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between -transitions. If we can formalize existing procedures into logical -specifications and verify continuous dynamics against transition requirements, -we can build autonomous controllers provably free from design +transitions. Formalizing existing procedures into logical +specifications and verifying continuous dynamics against transition requirements +enables us to build autonomous controllers provably free from design defects. % Pay-off This approach enables autonomous control in nuclear power plants while @@ -73,14 +73,13 @@ If this research is successful, we will be able to do the following: % OUTCOME 2 Title \item \textbf{Verify continuous control behavior across mode transitions.} % Strategy - We will establish methods for analyzing continuous control modes to ensure + We will 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 that each continuous mode safely reaches its intended transitions. % Outcome Engineers will design continuous controllers using standard practices while - iterating to ensure broader system correctness, proving that mode - transitions occur safely and at the correct times. + maintaining formal correctness guarantees. Mode transitions will provably occur safely and at the correct times. % OUTCOME 3 Title \item \textbf{Demonstrate autonomous reactor startup control with safety @@ -105,15 +104,15 @@ documents to deployed systems. \textbf{The key innovation} unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. -While formal methods can verify discrete logic and control theory can verify -continuous dynamics, no existing methodology bridges both with compositional -guarantees. This work establishes that bridge. It treats discrete specifications -as contracts that continuous controllers must satisfy, enabling independent +Formal methods can verify discrete logic. Control theory can verify +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 verification of each layer while guaranteeing correct composition. % Outcome Impact If successful, control engineers will create autonomous controllers from -existing procedures with mathematical proof of correct behavior. High-assurance +existing procedures with mathematical proofs of correct behavior. High-assurance autonomous control will become practical for safety-critical applications. % Impact/Pay-off This capability is essential for the economic viability of next-generation diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 2ff9896..2fc9b87 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -2,8 +2,8 @@ This research aims to create 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 the -operating procedures we will leverage, investigates limitations of human-based +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. @@ -15,8 +15,8 @@ Emergency Operating Procedures (EOPs) for design-basis accidents, Severe Accident Management Guidelines (SAMGs) for beyond-design-basis events, and Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899 -provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}, but their -development relies fundamentally on expert judgment and simulator validation +provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}. Their +development, however, relies on expert judgment and simulator validation rather than formal verification. Procedures undergo technical evaluation, simulator validation testing, and biennial review as part of operator requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor, @@ -56,7 +56,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation. \subsection{Human Factors in Nuclear Accidents} The preceding subsection established how nuclear plants currently operate: -through written procedures executed by human operators. This subsection examines +through written procedures executed by human operators. Having established current practice, we now examine why this human-centered approach poses fundamental limitations. Current-generation nuclear power plants employ over 3,600 active NRC-licensed @@ -67,8 +67,8 @@ shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor operator requires several years of training. -Human error persistently plays a role in nuclear safety incidents despite decades -of improvements in training and procedures. This provides the most compelling +Human error persistently contributes to nuclear safety incidents despite decades +of improvements in training and procedures. This provides 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 @@ -95,16 +95,17 @@ systemic weaknesses that create conditions for failure. \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits -that cannot be overcome through training alone.} The persistent human -error contribution despite four decades of improvements demonstrates that these -limitations are fundamental rather than a remediable part of human-driven control. +that training alone cannot overcome.} Four decades of improvements have not eliminated human +error. These +limitations are fundamental to human-driven control, not remediable defects. \subsection{Formal Methods} -The persistent human error problem motivates exploring formal methods to -provide mathematical guarantees of correctness that human-centered approaches +Having established that human error imposes fundamental reliability limits, +we now turn to formal methods as an alternative approach. +Formal methods provide mathematical guarantees of correctness that human-centered approaches cannot achieve. This subsection examines recent formal methods work in nuclear -control and identifies limitations for autonomous hybrid systems. +control and identifies their limitations for autonomous hybrid systems. \subsubsection{HARDENS} @@ -152,7 +153,8 @@ logic alone provides no guarantee that the closed-loop system exhibits desired continuous behavior such as stability, convergence to setpoints, or maintained safety margins. -HARDENS produced a demonstrator system at Technology Readiness Level 2--3 +Beyond the technical limitation of omitting continuous dynamics, HARDENS also faced +deployment maturity constraints. The project produced a demonstrator system at Technology Readiness Level 2--3 (analytical proof of concept with laboratory breadboard validation) rather than a deployment-ready system validated through extended operational testing. The NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is @@ -213,7 +215,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. Formal +flexibility but introduce persistent reliability limitations that four decades of training improvements have not eliminated. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. @@ -224,4 +226,4 @@ correct hybrid controllers from operational procedures with verification integrated into the design process. This gap—between discrete-only formal methods and post-hoc hybrid -verification—defines the challenge this research addresses. +verification—defines the challenge this research addresses. Closing this gap enables autonomous nuclear control with mathematical safety guarantees, addressing the economic constraints that threaten small modular reactor viability. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index e1afe6d..ee5af46 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -16,14 +16,13 @@ % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- Previous approaches to autonomous control verified discrete switching logic or -continuous control behavior, but not both simultaneously. Today's continuous -controller validation consists of extensive simulation trials. Human operators -drive discrete switching logic for routine operation; their evaluation includes -simulated control room testing and human factors research. Neither method +continuous control behavior, but not both simultaneously. Continuous +controller validation relies on extensive simulation trials. Discrete switching logic evaluation +uses simulated control room testing and human factors research. Neither method provides rigorous guarantees of control system behavior despite being extremely resource intensive. HAHACS bridges this gap by composing formal -methods from computer science with control-theoretic verification and -formalizing reactor operations using the framework of hybrid automata. +methods from computer science with control-theoretic verification, then +formalizing reactor operations using hybrid automata. The challenge of hybrid system verification lies in the interaction between discrete and continuous dynamics. Discrete transitions change the governing @@ -74,16 +73,16 @@ The creation of a HAHACS amounts to the construction of such a tuple together with proof artifacts demonstrating that the intended behavior of the control system is satisfied by its actual implementation. -\textbf{What is new:} This approach is tractable now because the infrastructure +\textbf{What is new:} The infrastructure for each component has matured, but no existing work composes them for end-to-end hybrid system verification. The novelty lies in the architecture connecting discrete synthesis with continuous verification through well-defined interfaces. -\textbf{Why it will succeed:} By defining -entry, exit, and safety conditions at the discrete level first, we transform the +\textbf{Why it will succeed:} Defining +entry, exit, and safety conditions at the discrete level first transforms the intractable problem of global hybrid verification into a collection of local -verification problems with clear interfaces. Verification operates per mode +verification problems with clear interfaces. Verification then operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Nuclear procedures already define discrete boundaries between operating regimes, providing the natural decomposition this methodology @@ -153,8 +152,8 @@ requires. \subsection{System Requirements, Specifications, and Discrete Controllers} -The hybrid system mathematical framework defined above provides the foundation. -Now we establish how to construct such systems from existing operational knowledge. +The preceding section established the mathematical framework for hybrid systems. +This section establishes how to construct such systems from existing operational knowledge. The key insight: nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism. @@ -176,17 +175,19 @@ The level of control linking these two extremes is the operational control scope. Operational control is the primary responsibility of human operators today. Operational control takes the current strategic objective and implements tactical control objectives to drive the plant towards strategic goals. In this -way, it bridges high-level and low-level goals. A strategic goal may be to +way, it bridges high-level and low-level goals. + +Consider an example: a strategic goal may be to perform refueling at a certain time, while the tactical level of the plant is currently focused on maintaining a certain core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along -the way to achieve this objective. Thus, the combination of the operational and +the way to achieve this objective. + +This structure reveals why the combination of the operational and tactical levels fundamentally forms a hybrid controller. The tactical level is the continuous evolution of the plant according to the control input and control law, while the operational level is a discrete state evolution that determines -which tactical control law to apply. - -%Say something about autonomous control systems near here? +which tactical control law to apply. This operational level is precisely what we target for autonomous control. \begin{figure} @@ -233,10 +234,10 @@ manuals to perform their control with strict procedures on what control to implement at a given time. These procedures are the key to the operational control scope. -The method of constructing a HAHACS in this proposal leverages two key -observations about current practice. First, the operational scope control is -effectively discrete control. Second, the rules for implementing this control -are described prior to their implementation in operating procedures. Before +Constructing a HAHACS leverages two key +observations about current practice. First, operational scope control is +effectively discrete control. Second, operating procedures describe the rules for implementing this control +before implementation. Before constructing a HAHACS, we must completely describe its intended behavior. The behavior of any control system originates in requirements: statements about what the system must do, must not do, and under what conditions. For nuclear systems, @@ -261,14 +262,13 @@ Discrete mode transitions include predicates that are Boolean functions over the continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true}, \text{false}\}$. These predicates formalize conditions like ``coolant temperature exceeds 315°C'' or ``pressurizer level is between 30\% and 60\%.'' -Critically, we do not impose this discrete abstraction artificially. Operating +We do not impose this discrete abstraction artificially. Operating procedures for nuclear systems already define go/no-go conditions as discrete -predicates. These thresholds come from design basis safety analysis and have -been validated over decades of operational experience. Our methodology assumes -this domain knowledge exists and provides a framework to formalize it. This is -why the approach is feasible for nuclear applications specifically: the hard -work of defining safe operating boundaries has already been done by generations -of nuclear engineers. +predicates. Design basis safety analysis determined these thresholds, and decades of operational experience have +validated them. Our methodology assumes +this domain knowledge exists and provides a framework to formalize it. The approach is feasible for nuclear applications because generations +of nuclear engineers have already done the hard +work of defining safe operating boundaries. Linear temporal logic (LTL) is particularly well-suited for specifying reactive systems. LTL formulas are built from atomic propositions @@ -317,14 +317,14 @@ room for interpretation is a weakness that must be addressed. % 3. DISCRETE CONTROLLER SYNTHESIS % ---------------------------------------------------------------------------- -Once system requirements are defined as temporal logic specifications, we use -them to build the discrete control system. To do this, reactive synthesis tools -are employed. Reactive synthesis is a field in computer science that deals with +Having defined system requirements as temporal logic specifications, we now use +them to build the discrete control system through reactive synthesis. +Reactive synthesis is a field in computer science that deals with the automated creation of reactive programs from temporal logic specifications. -A reactive program is one that, for a given state, takes an input and produces -an output. Our systems fit exactly this mold: the current discrete state and -status of guard conditions are the input, while the output is the next discrete -state. +A reactive program takes an input for a given state and produces +an output. Our systems fit this model: the current discrete state and +status of guard conditions form the input; the next discrete +state is the output. Reactive synthesis solves the following problem: given an LTL formula $\varphi$ that specifies desired system behavior, automatically construct a finite-state @@ -371,8 +371,8 @@ according to operating procedures. The discrete controller synthesized above is provably correct. Now we turn to the continuous dynamics executing within each discrete mode. -Synthesizing the discrete operational controller completes only half of an -autonomous controller. These control systems are hybrid: they have both discrete and +The discrete operational controller, while provably correct, represents only half of an +autonomous controller. Hybrid control systems require both discrete and continuous components. This section describes the continuous control modes that execute within each discrete state, and how we verify that they satisfy the requirements imposed by the discrete layer. It is important to clarify the scope @@ -434,7 +434,7 @@ requirements that determine which formal methods tools are appropriate. \subsubsection{Transitory Modes} -Transitory modes are continuous controllers designed to move +The first mode type, transitory modes, moves the plant from one discrete operating condition to another. Their purpose is to execute transitions: starting from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, @@ -494,11 +494,8 @@ appropriate to the fidelity of the reactor models available. \subsubsection{Stabilizing Modes} -Transitory modes drive the system toward exit conditions. Stabilizing modes, in -contrast, maintain the system within a desired operating region. - -Stabilizing modes are continuous controllers designed to maintain a particular -discrete state indefinitely. Rather than driving the system toward an +Transitory modes drive the system toward exit conditions. Stabilizing modes, the second type, +maintain the system within a desired operating region indefinitely. Rather than driving the system toward an exit condition, they keep the system within a safe operating region. Examples include steady-state power operation, hot standby, and load-following at constant power level. Reachability analysis for stabilizing modes may not be a diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index 90638de..309c211 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -9,9 +9,9 @@ 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 required to achieve TRL 5. -Technology Readiness Levels provide the ideal success metric because they +Technology Readiness Levels provide the ideal success metric: they explicitly measure the gap between academic proof-of-concept and practical -deployment---precisely what this work aims to bridge. Academic metrics like +deployment, precisely what this work aims to bridge. Academic metrics like papers published or theorems proved cannot capture practical feasibility. Empirical metrics like simulation accuracy or computational speed cannot demonstrate theoretical rigor. TRLs measure both dimensions simultaneously. diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex index ea75d0e..6b826ef 100644 --- a/5-risks-and-contingencies/v1.tex +++ b/5-risks-and-contingencies/v1.tex @@ -1,8 +1,8 @@ \section{Risks and Contingencies} This research relies on several critical assumptions that, if invalidated, would -require scope adjustment or methodological revision. The primary risks to -successful completion fall into four categories: computational tractability of +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 diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 5aded3c..b3c93df 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -1,8 +1,8 @@ \section{Broader Impacts} -\textbf{Who cares:} The nuclear industry, datacenter operators, and clean energy +\textbf{Who cares and why now:} The nuclear industry, datacenter operators, and clean energy advocates all face the same economic constraint: high operating costs driven by -staffing requirements. +staffing requirements. Recent AI infrastructure demands have made this constraint urgent. Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence