diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index ee55170..79102d6 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -4,12 +4,12 @@ This research develops autonomous control systems with mathematical guarantees o % INTRODUCTORY PARAGRAPH Hook Nuclear reactors require extensively trained operators who follow detailed written procedures and switch between control objectives based on plant conditions. % Gap -Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control systems can manage complex operational sequences without constant supervision—if they provide assurance equal to or exceeding human-operated systems. +Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening their economic viability. Autonomous control systems can manage complex operational sequences without constant supervision—if they provide assurance equal to or exceeding human-operated systems. % APPROACH PARAGRAPH Solution This research combines formal methods from computer science with control theory to build hybrid control systems 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 but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Neither approach provides end-to-end correctness guarantees for hybrid systems. +Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Neither approach alone provides end-to-end correctness guarantees. % Hypothesis and Technical Approach Three stages bridge this gap. First, written operating procedures translate into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET), which structures requirements into scope, condition, component, timing, and response. Realizability checking identifies conflicts and ambiguities before implementation. Second, reactive synthesis generates deterministic automata—provably correct by construction. Third, standard control theory designs continuous controllers for each discrete mode, which reachability analysis then verifies. Continuous modes classify by transition objectives: transitory modes drive the plant between conditions, stabilizing modes maintain operation within regions, and expulsory modes ensure safety under failures. Assume-guarantee contracts and barrier certificates prove safe mode transitions, enabling local verification without global trajectory analysis. An Emerson Ovation control system demonstrates the methodology. % Pay-off diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index 29ebd22..a4f2f33 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -8,12 +8,12 @@ Nuclear power plants require the highest levels of control system reliability. C % Known information Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements. These operators switch between control modes based on plant conditions and procedural guidance. % Gap -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 economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—if they provide assurance equal to or exceeding human operators. +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. Autonomous control systems could manage complex operational sequences without constant human supervision—if they provide assurance equal to or exceeding that of human operators. % APPROACH PARAGRAPH Solution This research combines formal methods with control theory to build hybrid control systems 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 fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. No existing approach provides end-to-end correctness guarantees for both layers. +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 fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. No existing approach guarantees end-to-end correctness for both layers. % Hypothesis This approach closes the gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between transitions. Operating procedures formalize into logical specifications. Continuous dynamics verify against transition requirements. The result: autonomous controllers provably free from design defects. @@ -68,7 +68,7 @@ This approach produces three concrete outcomes: % IMPACT PARAGRAPH Innovation These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems. -\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. 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, enabling independent verification of each layer while guaranteeing correct composition. +\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. 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, enabling independent verification of each layer while guaranteeing correct composition. Section 2 (State of the Art) examines why prior work has not achieved this integration. Section 3 (Research Approach) details how this integration will be accomplished. % Outcome Impact If successful, control engineers create autonomous controllers from diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index f5243f1..3a008a8 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -1,12 +1,14 @@ \section{State of the Art and Limits of Current Practice} -\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today and why current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. We examine reactor operators and their operating procedures, investigate the fundamental limitations of human-based operation, and review formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap our work addresses. +\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today and why current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis. First, we examine reactor operators and their operating procedures. Second, we investigate the fundamental limitations of human-based operation. Third, we review formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis. \subsection{Current Reactor Procedures and Operation} -Understanding the limits of current practice requires understanding what current practice is. 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. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. +Current practice must be understood before its limits can be identified. This subsection examines the hierarchy of nuclear plant procedures, the role of operators in executing them, and the operational modes that govern reactor control. -Expert judgment and simulator validation drive procedure development—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. Yet this rigor cannot provide formal verification of key safety properties. No mathematical proof confirms that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants. +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. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. + +Procedure development relies on expert judgment and simulator validation—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. Yet this rigor cannot provide formal verification of key safety properties. No mathematical proof confirms that procedures cover all possible plant states, that required actions complete within available timeframes, or that procedure-set transitions maintain safety invariants. \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness and completeness.} Current procedure development relies on expert judgment and @@ -23,7 +25,7 @@ The division between automated and human-controlled functions reveals the fundam \subsection{Human Factors in Nuclear Accidents} -Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Even perfect procedures cannot guarantee safe operation if humans execute them imperfectly. The second pillar of current practice—human operators executing these procedures—introduces reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how. Even perfect procedures cannot eliminate human error. +Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. The other half emerges from procedure execution: even perfect procedures cannot guarantee safe operation when humans execute them imperfectly. The second pillar of current practice—human operators executing these procedures—introduces reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how. Perfect procedures cannot eliminate human error. Current-generation nuclear power plants employ over 3,600 active NRC-licensed reactor operators in the United States~\cite{operator_statistics}. These @@ -60,7 +62,7 @@ limitations are fundamental to human-driven control, not remediable defects. Current practice reveals two critical limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. If training and procedural improvements cannot solve these problems, what can? Formal methods offer an alternative—mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. -Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems. Two approaches illustrate this gap: HARDENS verified discrete logic without continuous dynamics, while differential dynamic logic handles hybrid verification only post-hoc. The following subsections examine each approach and its limitations. +Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems. 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. \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 d35d682..85d46cf 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -15,11 +15,11 @@ % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- -Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees despite consuming enormous resources. +Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees, despite consuming enormous resources. This work bridges the gap by composing formal methods from computer science with control-theoretic verification. Reactor operations formalize as 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 fail to handle this interaction directly. +Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics creates discontinuities in system behavior when discrete transitions change the governing vector field. Traditional verification techniques fail to handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for 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. @@ -140,15 +140,15 @@ This work demonstrates feasibility on production control systems with realistic \subsection{System Requirements, Specifications, and Discrete Controllers} -The hybrid automaton formalism defined above provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. But where do these formal descriptions come from? This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism. +The hybrid automaton formalism defined above provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. But where do these formal descriptions come from? This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. The key insight is that nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism through three control scopes: strategic, operational, and tactical. Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making for the plant. Objectives at this level are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. These decisions span months or years. -The lowest level—the tactical level—controls individual components: pumps, turbines, and chemistry. Nuclear power plants today have already automated tactical control somewhat. Such automation is generally considered ``automatic control.'' These controls are almost always continuous systems with direct impact on the physical state of the plant. Tactical control objectives include maintaining pressurizer level, maintaining core temperature, or adjusting reactivity with a chemical shim. +The lowest level—the tactical level—controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control somewhat through what is generally considered ``automatic control.'' These controls are almost always continuous systems with direct impact on the physical state of the plant. Tactical control objectives include maintaining pressurizer level, maintaining core temperature, and adjusting reactivity with chemical shim. The operational control scope links these two extremes, representing the primary responsibility of human operators today. Operational control takes strategic objectives and implements tactical control sequences to achieve them, bridging high-level goals with low-level execution. -Consider an example: a strategic goal may be to perform refueling at a certain time. The tactical level currently maintains core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this objective. +An example clarifies this three-level structure. Consider a strategic goal to perform refueling at a certain time. The tactical level currently maintains core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this objective. This structure reveals why the operational and tactical levels fundamentally form a hybrid controller. The tactical level represents continuous plant evolution according to control input and control law. The operational level represents discrete state evolution that determines which tactical control law applies. This operational level becomes the target for autonomous control. @@ -186,12 +186,9 @@ This structure reveals why the operational and tactical levels fundamentally for \end{figure} -This operational control level is the main reason nuclear control today requires human operators. The hybrid nature of this control system makes proving controller performance against strategic requirements difficult. Unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature. These operators use prescriptive operating -manuals to perform their control with strict procedures on what control to -implement at a given time. These procedures provide the key to the operational -control scope. +This operational control level is the main reason nuclear control requires human operators. The hybrid nature of this control system makes proving controller performance against strategic requirements difficult. Unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature. These operators follow prescriptive operating manuals with strict procedures governing what control to implement at any given time. These procedures provide the key to the operational control scope. -Constructing a HAHACS leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe the implementation rules before construction. A HAHACS's intended behavior must be completely described before construction begins. Requirements define the behavior of any control system: statements about what +Constructing a HAHACS leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins. A HAHACS's intended behavior must be completely described before construction. Requirements define the behavior of any control system: statements about what the system must do, must not do, and under what conditions. For nuclear systems, these requirements derive from multiple sources including regulatory mandates, design basis analyses, and operating procedures. The challenge is formalizing @@ -241,12 +238,12 @@ coolant pressure drops, the system initiates shutdown within bounded time''). This work uses FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: reducing required expert knowledge makes these tools adoptable by the current nuclear workforce. FRET's key feature is its ability to start with logically imprecise -statements and consecutively refine them into well-posed specifications. We can -use this to our advantage by directly importing operating procedures and design +statements and refine them consecutively into well-posed specifications. We can +leverage this by directly importing operating procedures and design requirements into FRET in natural language, then iteratively refining them into specifications for a HAHACS. This approach provides two distinct benefits. First, it draws a direct link from design documentation to digital system implementation. Second, it clearly demonstrates where natural language documents -are insufficient. Human operators may still use these procedures, making any +fall short. Human operators may still use these procedures, making any room for interpretation a weakness that must be addressed. FRET has been successfully applied to spacecraft control systems, autonomous vehicle requirements, and medical device specifications. NASA used FRET for the Lunar Gateway project, formalizing flight software requirements that were previously specified only in natural language. The Defense Advanced Research Projects Agency (DARPA) employed FRET in the Assured Autonomy program to verify autonomous systems requirements. These applications demonstrate FRET's maturity for safety-critical domains. Nuclear control procedures present an ideal use case: they are already structured, detailed, and written to minimize ambiguity—precisely the characteristics that enable successful formalization. @@ -293,7 +290,7 @@ Reactive synthesis has proven successful in robotics, avionics, and industrial c \subsection{Continuous Control Modes} -Reactive synthesis produces a provably correct discrete controller from operating procedures—an automaton that determines when to switch between modes. But hybrid control requires more than correct mode switching. The continuous dynamics executing within each discrete mode must also be verified to ensure the complete system behaves correctly. +Reactive synthesis produces a provably correct discrete controller from operating procedures—an automaton that determines when to switch between modes. Hybrid control, however, requires more than correct mode switching. The continuous dynamics executing within each discrete mode must also be verified to ensure correct system behavior. This subsection describes the continuous control modes executing within each discrete state and explains how they verify against requirements imposed by the discrete layer. The verification approach depends on control objectives. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. @@ -350,6 +347,8 @@ tools matched to its control objective. Transitory modes drive the plant between \subsubsection{Transitory Modes} +We now examine each of the three continuous controller types in detail, beginning with transitory modes. + Transitory modes move the plant from one discrete operating condition to another. Their purpose is to execute transitions: start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers. We can state the control objective for a transitory mode formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy: @@ -401,7 +400,7 @@ appropriate to the fidelity of the reactor models available. \subsubsection{Stabilizing Modes} -Transitory modes drive the system toward exit conditions. Stabilizing modes do the opposite: they maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach. +Where transitory modes drive the system toward exit conditions, stabilizing modes do the opposite: they maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach. Reachability analysis answers "can the system reach a target?" Stabilizing modes ask instead "does the system stay within bounds?" Barrier certificates provide the appropriate tool. Barrier certificates analyze the dynamics of the system to determine whether @@ -455,7 +454,7 @@ controller. \subsubsection{Expulsory Modes} -Transitory and stabilizing modes handle nominal operations where plant dynamics match the design model. Expulsory modes handle the opposite case: when the plant deviates from expected behavior through component failures, sensor degradation, or unanticipated disturbances. +The first two mode types—transitory and stabilizing—handle nominal operations where plant dynamics match the design model. Expulsory modes handle the opposite case: when the plant deviates from expected behavior through component failures, sensor degradation, or unanticipated disturbances. These continuous controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and controlled depressurization procedures. @@ -536,11 +535,11 @@ outcomes can align best with customer needs. This section establishes the research approach by answering two critical Heilmeier questions: -\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations distinguish this approach: using discrete synthesis to define verification contracts (inverting traditional global analysis), classifying continuous modes by objective to select appropriate verification tools, and leveraging existing procedural structure to avoid intractable state explosion. +\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations distinguish this approach: using discrete synthesis to define verification contracts (inverting traditional global analysis), classifying continuous modes by objective to select appropriate verification tools, and leveraging existing procedural structure to avoid intractable state explosion. Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. This section demonstrates how compositional verification enables what global analysis cannot achieve. \textbf{Why will this approach succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the approach formalizes existing structure rather than imposing artificial abstractions. Second, mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. -The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. Sections 2 and 3 have established what has been done, what is new, and why it will succeed. One critical question remains: \textit{How will success be measured?} Section 4 addresses this through Technology Readiness Level advancement, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation (TRL 3) through integrated simulation (TRL 4) to hardware-in-the-loop testing (TRL 5). +The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. Sections 2 and 3 have established what has been done, what is new, and why it will succeed. Three critical questions remain for the complete research plan. Section 4 addresses \textit{How will success be measured?} through Technology Readiness Level advancement. Section 5 addresses \textit{What could prevent success?} through risk analysis and contingency planning. Section 6 addresses \textit{Who cares? Why now? What difference will it make?} through economic and societal impact analysis. %%% NOTES (Section 5): % - Get specific details on ARCADE interface from Emerson collaboration diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index a055976..fa5bcaa 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -2,7 +2,7 @@ \textbf{How do 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. TRL advancement provides the most appropriate success metric for this work, bridging the gap between academic proof-of-concept and practical deployment. This section explains why, then defines specific criteria for each level from TRL 3 through 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. TRL advancement provides the most appropriate success metric for this work by bridging the gap between academic proof-of-concept and practical deployment. This section explains why, then defines specific criteria for each level from TRL 3 through TRL 5. Technology Readiness Levels provide the ideal success metric by explicitly measuring the gap between academic proof-of-concept and practical deployment—precisely what this work bridges. 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. diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex index 22afe8d..39a14cb 100644 --- a/5-risks-and-contingencies/v1.tex +++ b/5-risks-and-contingencies/v1.tex @@ -4,7 +4,7 @@ \subsection{Computational Tractability of Synthesis} -The first major assumption is that formalized startup procedures will yield automata small enough for efficient synthesis and verification. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states. Such large automata would require synthesis times exceeding days or weeks, preventing demonstration of the complete methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives. +The first major assumption is that formalized startup procedures will yield automata small enough for efficient synthesis and verification. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states, requiring synthesis times that exceed days or weeks and prevent demonstration of the complete methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives. Several indicators would provide early warning of computational tractability problems. Synthesis times exceeding 24 hours for simplified procedure subsets diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 9419ba5..a113968 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -1,6 +1,8 @@ \section{Broader Impacts} -\textbf{Who cares? Why now? What difference will it make?} These three Heilmeier questions connect technical methodology to economic and societal impact. Three stakeholder groups face the same economic constraint: the nuclear industry, datacenter operators, and clean energy advocates. All confront high operating costs driven by staffing requirements. AI infrastructure demands, growing exponentially, have made this constraint urgent. +\textbf{Who cares? Why now? What difference will it make?} These three Heilmeier questions connect technical methodology to economic and societal impact. Sections 2--5 established the technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how success will be measured (Section 4), and what could prevent success (Section 5). This section addresses the remaining Heilmeier questions by connecting the technical methodology to urgent economic and infrastructure challenges. + +Three stakeholder groups face the same economic constraint: the nuclear industry, datacenter operators, and clean energy advocates. All confront high operating costs driven by staffing requirements. AI infrastructure demands, growing exponentially, have made this constraint urgent. Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence infrastructure has renewed focus on small modular reactors (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. Deploying SMRs at datacenter sites minimizes transmission losses and eliminates emissions. However, nuclear power economics at this scale demand careful attention to operating costs.