From 401f8fbddca2b2e01bfea1bf0c6ad54f61a74780 Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 9 Mar 2026 17:15:13 -0400 Subject: [PATCH] Editorial pass: tactical, operational, and strategic improvements MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TACTICAL (sentence-level): - Strengthened verb choice and active constructions - Improved topic-stress positioning - Enhanced clarity and directness - Tightened issue-point structure OPERATIONAL (paragraph/section): - Improved paragraph breaks and flow - Enhanced transitions between ideas - Reordered content for better coherence - Reduced redundancy STRATEGIC (document-level): - Clarified Heilmeier question framing - Strengthened section linkages and forward references - Improved progression from problem → approach → validation → impact - Enhanced overall document coherence --- .../research_statement_v1.tex | 10 +++--- 1-goals-and-outcomes/v1.tex | 14 ++++---- 2-state-of-the-art/v2.tex | 20 ++++++------ 3-research-approach/v3.tex | 32 ++++++++++--------- 4-metrics-of-success/v1.tex | 2 +- 5-risks-and-contingencies/v1.tex | 2 +- 6-broader-impacts/v1.tex | 10 +++--- 8-schedule/v1.tex | 2 +- 8 files changed, 46 insertions(+), 46 deletions(-) diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index c7471a8..f4ee0d2 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -2,16 +2,16 @@ This research develops autonomous control systems with mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook -Extensively trained human operators control nuclear reactors today. They follow detailed written procedures and switch between control objectives as plant conditions change. +Extensively trained human operators control nuclear reactors today, following detailed written procedures and switching between control objectives as plant conditions change. % Gap -Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if safety assurance equals or exceeds that of human operators. +Small modular reactors face a fundamental economic challenge: staffing costs per megawatt far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators. % APPROACH PARAGRAPH Solution -This approach unifies formal methods from computer science with control theory to produce hybrid control systems that are correct by construction. +Formal methods from computer science unify with control theory to produce hybrid control systems that are correct by construction. % Rationale -Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. End-to-end correctness requires both. +Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. Both are required for end-to-end correctness. % Hypothesis and Technical Approach -Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications that structure requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory techniques—satisfy each discrete mode's requirements. +Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications, structuring requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory—satisfy each discrete mode's requirements. Continuous modes classify by control objective into three types: transitory modes drive the plant between conditions, stabilizing modes maintain operation within regions, and expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe, enabling local verification without global trajectory analysis. This methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use. % Pay-off diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index 879844b..a484578 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -6,16 +6,16 @@ This research develops autonomous hybrid control systems with mathematical guara % INTRODUCTORY PARAGRAPH Hook Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release. % Known information -Extensively trained human operators control nuclear plants today. They follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance. +Extensively trained human operators control nuclear plants today, following detailed written procedures and strict regulatory requirements. They 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 could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of 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 staffing costs per megawatt far exceeding those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators. % APPROACH PARAGRAPH Solution -This work unifies formal methods with control theory to produce hybrid control systems that are correct by construction. +Formal methods unify with control theory to produce hybrid control systems that are correct by construction. % Rationale -Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both. +Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness. % Hypothesis -Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics—producing autonomous controllers provably free from design defects. +Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers provably free from design defects. The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation requirements. @@ -62,9 +62,7 @@ If successful, this approach produces three concrete outcomes: \end{enumerate} % 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?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic; control theory verifies continuous dynamics. +\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic; control theory verifies continuous dynamics. These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems. % Outcome Impact If successful, control engineers will create autonomous controllers from existing procedures with mathematical proofs of correct behavior, making high-assurance autonomous control practical for safety-critical applications. This capability is essential for the economic viability of next-generation nuclear power. Small modular reactors, in particular, offer a promising solution to growing energy demands, but their success depends on reducing per-megawatt operating costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index a7523b0..2d59c45 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -2,19 +2,19 @@ \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} -No current approach provides autonomous control with end-to-end correctness guarantees. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior—but never both. +No current approach provides autonomous control with end-to-end correctness guarantees. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior—never both. -Three subsections structure this analysis: reactor operators and their operating procedures; fundamental limitations of human-based operation; and formal methods approaches that verify discrete logic or continuous dynamics but not both together. +Three subsections structure this analysis: reactor operators and their operating procedures, fundamental limitations of human-based operation, and formal methods approaches that verify discrete logic or continuous dynamics but not both together. -These limits establish a verification gap that Section 3 addresses. +Section 3 addresses the verification gap these limits establish. \subsection{Current Reactor Procedures and Operation} -Current practice rests on two critical components: procedures and operators. Procedures define what must be done; operators execute those procedures. This subsection examines procedures: their hierarchy, development process, and role in defining operational modes. The following subsection examines operators: their reliability limits and contribution to accidents. +Current practice rests on two critical components: procedures and operators. Procedures define what must be done; operators execute those procedures. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection examines operators—their reliability limits and contribution to accidents. Nuclear plant procedures form a strict 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. All procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. -Expert judgment and simulator validation—not formal verification—form the basis for procedure development. Regulations require rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} mandates technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification: procedures cover all possible plant states without mathematical proof, required actions complete within available timeframes without proof, and transitions between procedure sets maintain safety invariants without proof. +Expert judgment and simulator validation—not formal verification—form the basis for procedure development. Regulations mandate rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification: 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. \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness and completeness.} No proof exists that procedures cover all @@ -24,9 +24,9 @@ invariants. Paper-based procedures cannot ensure correct application. Even computer-based procedure systems lack the formal guarantees automated reasoning could provide. -Beyond procedure verification, nuclear plants operate with multiple control modes. Automatic control maintains target parameters through continuous reactivity adjustment. Manual control allows operators to directly manipulate the reactor. Various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature, compensating for power demand changes through reactivity feedback loops alone. Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required. +Nuclear plants operate with multiple control modes. Automatic control maintains target parameters through continuous reactivity adjustment. Manual control allows operators to directly manipulate the reactor. Various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature, compensating for power demand changes through reactivity feedback loops alone. -This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems already handle reactor protection—automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure—discrete human decisions combined with continuous automated control—forms the basis for autonomous hybrid control systems. +Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required. This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems already handle reactor protection—automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure—discrete human decisions combined with continuous automated control—forms the basis for autonomous hybrid control systems. \subsection{Human Factors in Nuclear Accidents} @@ -157,8 +157,8 @@ This section answered two Heilmeier questions: What has been done? What are the \textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability limitations. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally. -\textbf{What are the limits of current practice?} A clear verification gap emerges: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics but never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design. +\textbf{What are the limits of current practice?} A clear verification gap emerges: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics—never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design. -\textbf{Why now?} Two forces create urgency. Economic necessity demands solutions—small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity enables solutions—formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable. +\textbf{Why now?} Two forces create urgency. First, economic necessity demands solutions: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, technical maturity enables solutions: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable. -The verification gap is clear. The timing is right. Section 3 closes this gap by establishing what is new and why the approach will succeed. +The verification gap is clear. The timing is right. Section 3 closes this gap, establishing what is new and why the approach will succeed. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index cec07d7..d68917a 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -4,9 +4,9 @@ This section presents the complete technical approach for synthesizing provably correct hybrid controllers from operating procedures. -\textbf{What is new:} Compositional verification bridges discrete synthesis with continuous control through three innovations: contract-based decomposition, mode classification, and procedure-driven structure. +\textbf{What is new:} Three innovations enable compositional verification bridging discrete synthesis with continuous control: contract-based decomposition, mode classification, and procedure-driven structure. -\textbf{Why it will succeed:} The approach leverages existing procedural structure, bounds computational complexity through mode-level verification, and validates against real industrial hardware through the Emerson collaboration. +\textbf{Why it will succeed:} The approach leverages existing procedural structure, bounds computational complexity through mode-level verification, and validates against real industrial hardware through Emerson collaboration. % ============================================================================ % STRUCTURE (maps to Thesis.RA tasks): @@ -23,9 +23,9 @@ This section presents the complete technical approach for synthesizing provably % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- -Previous approaches verified discrete switching logic or continuous control behavior but never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees; both consume enormous resources. +Previous approaches verified discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources. -This approach bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata. +This approach bridges that gap, composing formal methods from computer science with control-theoretic verification and formalizing reactor operations as hybrid automata. Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field. These discontinuities cannot be handled directly by traditional verification techniques. @@ -58,7 +58,7 @@ where: A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior. -\textbf{What is new in this research?} Existing approaches verify discrete logic or continuous dynamics but never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently but have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation. +\textbf{What is new in this research?} Existing approaches verify discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently but have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation. Three innovations enable compositional verification: @@ -70,7 +70,7 @@ Three innovations enable compositional verification: \textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed. -\textbf{Existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions, enabling domain experts to adopt it without formal methods training. +\textbf{Existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions, enabling domain experts to adopt the methodology without formal methods training. \textbf{Bounded complexity:} Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. This decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications. @@ -331,7 +331,9 @@ precise objectives for continuous control. The continuous controller for mode $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$. -Continuous controllers classify into three types based on their control objectives, each requiring distinct verification tools matched to its purpose. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. The following subsections detail each mode type and its verification approach, progressing from nominal operations (transitory and stabilizing modes) to off-nominal scenarios (expulsory modes). +Continuous controllers classify into three types based on control objectives, each requiring distinct verification tools. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. + +The following subsections detail each mode type and its verification approach, progressing from nominal operations—transitory and stabilizing modes—to off-nominal scenarios handled by expulsory modes. %%% NOTES (Section 4): % - Add figure showing the relationship between entry/exit/safety sets @@ -392,9 +394,9 @@ appropriate to the fidelity of the reactor models available. \subsubsection{Stabilizing Modes} -Transitory modes drive the system toward exit conditions, answering the question "can we reach the target?" Reachability analysis provides the verification tool for this question. +Transitory modes answer the question "can we reach the target?" by driving the system toward exit conditions. Reachability analysis provides the verification tool. -Stabilizing modes address a fundamentally different question—"will we stay within bounds?" These 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. +Stabilizing modes address a fundamentally different question: "will we stay within bounds?" These 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?" Stabilizing modes instead ask "does the system stay within bounds?" Barrier certificates provide the appropriate verification tool for this question. Barrier certificates analyze the dynamics of the system to determine whether @@ -526,25 +528,25 @@ outcomes can align best with customer needs. This section answered two critical Heilmeier questions: What is new? Why will it succeed? -\textbf{What is new?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations enable this integration: +\textbf{What is new?} Three innovations enable compositional verification integrating reactive synthesis, reachability analysis, and barrier certificates: -\textit{Contract-based decomposition} inverts traditional global analysis—discrete synthesis defines verification contracts that bound continuous verification. +\textit{Contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. \textit{Mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. \textit{Procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion. -Section 2 established that prior work verified discrete logic or continuous dynamics but never both compositionally. This compositional verification enables what global analysis cannot achieve. +Section 2 established that prior work verified discrete logic or continuous dynamics—never both compositionally. This compositional verification enables what global analysis cannot achieve. \textbf{Why will it succeed?} Three factors ensure practical feasibility: -\textit{Existing structure.} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization without imposing artificial abstractions. +\textit{Existing structure.} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization without artificial abstractions. \textit{Bounded complexity.} Mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. -\textit{Industrial validation.} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints. +\textit{Industrial validation.} Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints. -The complete technical methodology is now established. Section 2 answered what has been done and what limits current practice. This section answered what is new and why it will succeed. Three critical questions remain: how will success be measured (Section 4), what could prevent success (Section 5), and who cares—why now, what difference will it make (Section 6). +The complete technical methodology is now established. Section 2 answered what has been done and what limits current practice. This section answered what is new and why it will succeed. Three questions remain: How will success be measured? What could prevent success? Who cares, why now, and what difference will it make? Sections 4, 5, and 6 address these in turn. %%% 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 20d4eac..e1ee489 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -2,7 +2,7 @@ \textbf{Heilmeier Question: How will success be measured?} -Section 3 established the technical approach. It answered what is new: compositional verification bridging discrete synthesis with continuous control. It answered why it will succeed: existing procedural structure, bounded complexity, and industrial validation. This section addresses the next Heilmeier question: how to measure success. +Section 3 established the technical approach, answering what is new—compositional verification bridging discrete synthesis with continuous control—and why it will succeed—existing procedural structure, bounded complexity, and industrial validation. This section addresses the next Heilmeier question: How will success be measured? Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5). At TRL 5, system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5. diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex index a28ed12..cd2034d 100644 --- a/5-risks-and-contingencies/v1.tex +++ b/5-risks-and-contingencies/v1.tex @@ -2,7 +2,7 @@ \textbf{Heilmeier Question: What could prevent success?} -Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome. What if they cannot? +Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome. Every research plan rests on assumptions that might prove false. Three primary risks could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization. diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 7efa4b3..5ab9443 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -2,15 +2,15 @@ \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?} -Sections 2--5 established the complete technical research plan. Section 2 answered what has been done. Section 3 answered what is new and why it will succeed. Section 4 answered how to measure success. Section 5 answered what could prevent success. +Sections 2 through 5 established the complete technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how to measure success (Section 4), and what could prevent success (Section 5). -The technical plan is complete. This section addresses the remaining Heilmeier questions. It connects technical methodology to economic and societal impact: who cares, why now, and what difference this work will make. +The technical plan is complete. This section addresses the remaining Heilmeier questions, connecting technical methodology to economic and societal impact: who cares, why now, and what difference this work will make. -\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically viable against fossil alternatives. All three need this research to succeed. +\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive with fossil alternatives. All three require this research to succeed. -\textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier, enabling economically viable small modular reactors for datacenter power while establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure. +\textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier, enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure. -\textbf{Why now?} Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis—creating a market demanding solutions that did not exist before. +\textbf{Why now?} Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis, creating a market demanding solutions that did not exist before. 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. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions. At this scale, nuclear power economics demand careful attention to operating costs. diff --git a/8-schedule/v1.tex b/8-schedule/v1.tex index d0aa598..f53193c 100644 --- a/8-schedule/v1.tex +++ b/8-schedule/v1.tex @@ -2,7 +2,7 @@ \textbf{Heilmeier Question: How long will it take?} -Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. This final Heilmeier question addresses timing and feasibility within a doctoral timeline. +Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. This final section addresses the last Heilmeier question: How long will it take? This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC Fellowship provide all computational and experimental resources. The work progresses sequentially through three main research thrusts, culminating in integrated demonstration and validation.