From 94489846943a913660fdd40f21feaa644943622e Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 9 Mar 2026 13:45:28 -0400 Subject: [PATCH] Editorial review: three-pass copy edit (tactical, operational, strategic) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PASS 1 - TACTICAL (sentence-level): - Converted passive voice to active throughout - Strengthened weak verbs (fail → cannot, such → empty deletion) - Improved issue-point positioning for clarity - Enhanced topic-stress alignment PASS 2 - OPERATIONAL (paragraph/section): - Improved transitions between subsections - Enhanced coherence within sections - Strengthened flow between paragraphs - Made section summaries more cohesive PASS 3 - STRATEGIC (document-level): - Strengthened Heilmeier question framing throughout - Improved section-to-section transitions - Enhanced narrative coherence across document - Made Heilmeier answers more explicit and consistent --- .../research_statement_v1.tex | 12 +++++----- 1-goals-and-outcomes/v1.tex | 8 +++---- 2-state-of-the-art/v2.tex | 20 ++++++++--------- 3-research-approach/v3.tex | 22 +++++++++---------- 4-metrics-of-success/v1.tex | 8 +++---- 5-risks-and-contingencies/v1.tex | 10 ++++----- 6-broader-impacts/v1.tex | 10 ++++----- 7 files changed, 45 insertions(+), 45 deletions(-) diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index a027cd8..f0a306b 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -2,9 +2,9 @@ This research develops autonomous control systems with mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook -Extensively trained operators manage nuclear reactors by following detailed written procedures. When operators switch between control objectives, plant conditions guide their decisions. +Nuclear reactors require extensively trained operators who follow detailed written procedures. Plant conditions guide operator decisions when they switch between control objectives. % Gap -Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening viability. Autonomous control systems must manage complex operational sequences safely without constant supervision while providing assurance equal to or exceeding that of human-operated systems. +Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening viability. To remain competitive, these reactors need autonomous control systems that manage complex operational sequences safely without constant supervision while providing assurance equal to or exceeding that of human-operated systems. % APPROACH PARAGRAPH Solution We combine formal methods from computer science with control theory to @@ -12,9 +12,9 @@ build hybrid control 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 but fail to handle continuous dynamics +generate provably correct switching logic but cannot handle continuous dynamics during transitions. Control theory verifies continuous behavior but -fails to prove the correctness of discrete switching decisions. +cannot prove the correctness of discrete switching decisions. % Hypothesis and Technical Approach Our methodology bridges this gap through three stages. First, we translate written operating procedures into temporal logic specifications using NASA's Formal @@ -24,11 +24,11 @@ checking identifies conflicts and ambiguities before implementation. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, we design continuous controllers for each discrete mode using standard -control theory and verify them using reachability analysis. Continuous modes are classified by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. This approach enables local verification of continuous modes +control theory and verify them using reachability analysis. We classify continuous modes by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. This approach enables local verification of continuous modes without requiring global trajectory analysis across the entire hybrid system. We demonstrate this methodology on an Emerson Ovation control system. % Pay-off -Autonomous control can then manage complex nuclear +This autonomous control approach can then manage complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability. % OUTCOMES PARAGRAPHS diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index ad37501..d5c37b5 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -8,14 +8,14 @@ Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release. % Known information -Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to manage reactor control. Plant conditions and procedural guidance inform operator decisions when switching between different control modes. +Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to manage reactor control. Plant conditions and procedural guidance inform operator decisions when they switch between different control modes. % 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 that far exceed those of conventional plants, threatening economic viability. The nuclear industry needs autonomous control systems that manage complex operational sequences safely without constant human supervision while providing assurance equal to or exceeding that of 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 work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but fail to handle continuous dynamics during transitions. Control theory verifies continuous behavior but fails to prove the correctness of discrete switching decisions. No existing approach provides end-to-end correctness guarantees. +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 continuous dynamics during transitions. Control theory verifies continuous behavior but cannot prove the correctness of discrete switching decisions. No existing approach provides 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 @@ -25,7 +25,7 @@ defects. The University of Pittsburgh Cyber Energy Center provides access to ind requirements. % OUTCOMES PARAGRAPHS -If this research is successful, we will be able to do the following: +This approach produces three concrete outcomes: \begin{enumerate} @@ -72,7 +72,7 @@ If this research is successful, we will be able to do the following: % 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 is new in this research?} We unify discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. +\textbf{What makes this research new?} We unify 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 diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index dd0bfcd..1d64402 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -4,7 +4,7 @@ \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. 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}. Their 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 exists 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 scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Developers rely 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 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 @@ -36,7 +36,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation. \subsection{Human Factors in Nuclear Accidents} -Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how to apply them. Even perfectly written procedures fail to eliminate human error. +Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how to apply them. Even perfectly written 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 @@ -48,7 +48,7 @@ operator requires several years of training. Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design -deficiencies, and component failures combine to cause disaster. Operators +deficiencies, and component failures can combine to cause disaster. Operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a fundamental ambiguity: placing responsibility for safe power plant operations on @@ -71,7 +71,7 @@ limitations are fundamental to human-driven control, not remediable defects. \subsection{Formal Methods} -Two limitations are now clear: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative approach. They provide mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems. +Two limitations emerge from current practice: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative approach by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems. \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control} @@ -100,11 +100,11 @@ synthesis generated verifiable C implementations and SystemVerilog hardware implementations directly from Cryptol models---eliminating the traditional gap between specification and implementation where errors commonly arise. -Despite its accomplishments, HARDENS has a fundamental limitation for hybrid control synthesis: the project addressed only discrete digital control logic. It did not model or verify continuous reactor dynamics. +Despite its accomplishments, HARDENS has a fundamental limitation for hybrid control synthesis: the project addressed only discrete digital control logic. The project did not model or verify continuous reactor dynamics. The Reactor Trip System specification and verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). The -project did not address continuous dynamics of nuclear reactor physics. Real +project did not address the continuous dynamics of nuclear reactor physics. Real reactor safety depends on the interaction between continuous processes---temperature, pressure, neutron flux---evolving in response to discrete control decisions. HARDENS verified the discrete controller in @@ -141,7 +141,7 @@ primary assurance evidence. \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification} -HARDENS verified discrete control logic but omitted continuous dynamics, a fundamental limitation for hybrid systems. Recognizing this gap, other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). dL introduces two additional operators +HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. Recognizing this gap, other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). dL introduces two additional operators into temporal logic: the box operator and the diamond operator. The box operator \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system \(\alpha\) always remains within that region. In this way, it is a safety @@ -174,10 +174,10 @@ design loop for complex systems like nuclear reactor startup procedures. \subsection{Summary: The Verification Gap} -This section answered two Heilmeier questions: +This section establishes the current state of practice by answering two Heilmeier questions: -\textbf{What has been done?} 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 and does not scale to system synthesis. +\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate. 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 and does not scale to system synthesis. \textbf{What are the limits of current practice?} No existing methodology synthesizes provably 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 prevents autonomous nuclear control with end-to-end correctness guarantees. -Two imperatives are now clear. First, the economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, the technical capability gap: current approaches verify either discrete logic or continuous dynamics, never both compositionally. Section 3 presents our methodology for bridging this gap, establishing what is new and why it will succeed where prior work has not. +Two imperatives emerge from this analysis. First, the economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, the technical capability gap: current approaches verify either discrete logic or continuous dynamics, never both compositionally. Section 3 presents our methodology for bridging this gap, establishing what is new and why it will succeed where prior work has not. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index e3b17e7..9d96590 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -15,7 +15,7 @@ % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- -Previous approaches to autonomous control 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 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 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 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, 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, while continuous controllers govern plant behavior within each mode. @@ -24,7 +24,7 @@ a mathematical description of the system. This work draws on automata theory, temporal logic, and control theory. A hybrid system is a dynamical system with both continuous and discrete states. This proposal discusses continuous autonomous hybrid systems specifically: systems with no external input where continuous -states do not change instantaneously when discrete states change. These continuous states are physical quantities that remain +states do not change instantaneously when discrete states change. These continuous states represent physical quantities that remain Lipschitz continuous. We follow the nomenclature from the Handbook on Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here for convenience: @@ -50,9 +50,9 @@ where: \item $Inv$: safety invariants on the continuous dynamics \end{itemize} -Creating a HAHACS requires constructing such a tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior. +Creating a HAHACS requires constructing this tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior. -\textbf{What is new in this research?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty: +\textbf{What is new in this research?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution lies in the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty: \begin{enumerate} \item Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. @@ -195,9 +195,9 @@ which tactical control law to apply. We target this operational level for autono \end{figure} -This operational control level is the main reason human operators are required in nuclear control today. 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 +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 are the key to the operational +implement at a 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 @@ -306,7 +306,7 @@ Reactive synthesis produces a provably correct discrete controller from operatin This subsection describes the continuous control modes that execute within each discrete state. We explain how we verify they satisfy the 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. -This methodology's scope regarding continuous controller design requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers design continuous controllers using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system. +This methodology's scope regarding continuous controller design requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers design continuous controllers using standard control theory techniques. Our contribution lies in the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system. The operational control scope defines go/no-go decisions that determine what kind of continuous control to implement. The entry or exit conditions of a @@ -410,7 +410,7 @@ 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 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 must instead prove "does the system stay within bounds?" Barrier certificates provide the appropriate tool for this question. +While transitory modes drive the system toward exit conditions, stabilizing modes 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?" while stabilizing modes must instead prove "does the system stay within bounds?" Barrier certificates provide the appropriate tool for this question. Barrier certificates analyze the dynamics of the system to determine whether flux across a given boundary exists. They evaluate whether any trajectory leaves a given boundary. This definition exactly matches what defines the validity of a @@ -462,7 +462,7 @@ controller. \subsubsection{Expulsory Modes} -Transitory and stabilizing modes handle nominal operations under the assumption that plant dynamics match the design model. When the plant deviates from expected behavior—through component failures, sensor degradation, or unanticipated disturbances—expulsory modes take over to ensure safety. These continuous controllers prioritize robustness over optimality. The control objective is to drive 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. +Transitory and stabilizing modes handle nominal operations under the assumption that plant dynamics match the design model. When the plant deviates from expected behavior—through component failures, sensor degradation, or unanticipated disturbances—expulsory modes ensure safety. These continuous controllers prioritize robustness over optimality. The control objective is to drive 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. Proving controller correctness through reachability and barrier certificates makes detecting physical failures straightforward. The controller cannot be incorrect for the nominal plant model. When an invariant is violated, the plant dynamics must have changed. The HAHACS identifies faults when continuous controllers violate discrete boundary conditions—a direct consequence of verified nominal control modes. Unexpected behavior implies off-nominal conditions. @@ -539,11 +539,11 @@ of transferring technology directly to industry with a direct collaboration in this research, while getting an excellent perspective of how our research outcomes can align best with customer needs. -This section answered two Heilmeier questions: +This section establishes the methodology by answering two Heilmeier questions: \textbf{What is new in this research?} We integrate reactive synthesis, reachability analysis, and barrier certificates into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis. -\textbf{Why will this approach succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The methodology formalizes existing structure rather than imposing artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation. +\textbf{Why will this approach succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, so the methodology formalizes existing structure rather than imposing artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation. We have now established the complete methodology from procedure formalization through discrete synthesis to continuous verification and hardware implementation. Section 4 addresses the next Heilmeier question: how do we measure success? Technology Readiness Level advancement serves as the primary metric, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation to integrated hardware testing. diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index 4f73caf..464a267 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -6,18 +6,18 @@ 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 first explains why TRL advancement provides the most appropriate success metric, 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 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. Only TRLs measure both simultaneously. +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 aims to bridge. 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. Only TRLs measure both simultaneously. Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while progressively demonstrating practical feasibility. Formal verification must remain valid as the system moves from individual components to integrated hardware testing. The nuclear industry requires extremely high assurance before deploying new -control technologies. Demonstrating theoretical correctness alone is +control technologies. Demonstrating theoretical correctness alone proves insufficient for adoption; conversely, showing empirical performance without formal guarantees fails to meet regulatory requirements. TRLs capture this dual requirement naturally. Each level represents both increased practical maturity -and sustained theoretical validity. Furthermore, TRL assessment forces explicit +and sustained theoretical validity, while TRL assessment forces explicit identification of remaining barriers to deployment. The nuclear industry already uses TRLs for technology assessment, making this metric directly relevant to potential adopters. Reaching TRL 5 provides a clear answer to industry questions @@ -81,4 +81,4 @@ a relevant laboratory environment. This establishes both theoretical validity and practical feasibility, proving the methodology produces verified controllers implementable with current technology. -This section answers the Heilmeier question \textbf{How do we measure success?} TRL advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility. However, reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research may stall at lower readiness levels despite sound methodology. Section 5 addresses the next Heilmeier question: \textbf{What could prevent success?} We identify the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail. +This section establishes success criteria by answering the Heilmeier question \textbf{How do we measure success?} TRL advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility. However, reaching TRL 5 depends on several critical assumptions that, if proven false, could stall the research at lower readiness levels despite sound methodology. Section 5 addresses the complementary Heilmeier question: \textbf{What could prevent success?} We identify the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail. diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex index d80e227..c74bbf6 100644 --- a/5-risks-and-contingencies/v1.tex +++ b/5-risks-and-contingencies/v1.tex @@ -10,7 +10,7 @@ publishable results while clearly identifying remaining barriers to deployment. 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 +produce automata with thousands of states. 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 @@ -31,7 +31,7 @@ If computational tractability becomes the limiting factor, we reduce scope to a \subsection{Discrete-Continuous Interface Formalization} -Computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint. The second risk is more fundamental: whether boolean guard +While computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint—the second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal @@ -87,7 +87,7 @@ computational resources where they matter most for safety assurance. \subsection{Procedure Formalization Completeness} -The previous two risks concern verification infrastructure—computational scaling and mathematical formalization. The third assumption addresses the source material itself: that existing startup procedures contain sufficient +While the previous two risks concern verification infrastructure—computational scaling and mathematical formalization—the third assumption addresses the source material itself: whether existing startup procedures contain sufficient detail and clarity for translation into temporal logic specifications. Nuclear operating procedures, while extensively detailed, were written for human operators who bring contextual understanding and adaptive reasoning to their @@ -143,6 +143,6 @@ extensions, ensuring they address industry-wide practices rather than specific quirks. -This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks—computational tractability, discrete-continuous interface complexity, procedure formalization completeness, and hardware integration—each have identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid. Even partial success yields publishable results that clearly identify remaining barriers to deployment. +This section identifies barriers to success by answering the Heilmeier question \textbf{What could prevent success?} Four primary risks—computational tractability, discrete-continuous interface complexity, procedure formalization completeness, and hardware integration—each have identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid, with even partial success yielding publishable results that clearly identify remaining barriers to deployment. -The research plan is now complete from a technical perspective. We have established technical feasibility through the methodology (Section 3), defined success metrics (Section 4), and addressed risks with contingency plans (this section). Section 6 addresses the remaining Heilmeier questions establishing broader impact: \textbf{Who cares? Why now? What difference will it make?} +The research plan is now complete from a technical perspective: we have established technical feasibility through the methodology (Section 3), defined success metrics (Section 4), and addressed risks with contingency plans (this section). Section 6 completes the Heilmeier framework by establishing broader impact: \textbf{Who cares? Why now? What difference will it make?} diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index f862ce4..c49458c 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -22,7 +22,7 @@ to \$21--28 billion annually for projected datacenter demand. \$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. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output. This makes per-megawatt costs prohibitive. These staffing requirements drive the economic challenge that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal +Current nuclear operations require full control room staffing for each reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output, making per-megawatt costs prohibitive. These staffing requirements drive the economic challenge that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal specifications automates routine operational sequences that currently require constant human oversight. This enables a fundamental shift from direct operator control to supervisory monitoring, where operators oversee multiple autonomous @@ -66,12 +66,12 @@ establish both the technical feasibility and regulatory pathway for broader adoption across critical infrastructure. -This section answered three Heilmeier questions: +This section establishes impact by answering three Heilmeier questions: -\textbf{Who cares?} The nuclear industry, datacenter operators, and anyone facing high operating costs from staffing-intensive safety-critical control all care. +\textbf{Who cares?} The nuclear industry, datacenter operators, and any organization facing high operating costs from staffing-intensive safety-critical control. -\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent. Formal methods tools have matured to where compositional hybrid verification is now achievable. +\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent, while formal methods tools have matured to where compositional hybrid verification has become achievable. \textbf{What difference will it make?} Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier while establishing a generalizable framework for safety-critical autonomous systems. -Section 8 addresses the final Heilmeier question: \textbf{How long will it take?} A structured 24-month research plan progresses through milestones tied to Technology Readiness Level advancement. +Section 8 completes the Heilmeier framework by addressing the final question: \textbf{How long will it take?} A structured 24-month research plan progresses through milestones tied to Technology Readiness Level advancement.