From 0c035111746b58d1c90aff8dddd0dd069985de28 Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 9 Mar 2026 16:03:26 -0400 Subject: [PATCH] Editorial pass: Tactical, operational, and strategic improvements TACTICAL (sentence-level): - Applied Gopen's Sense of Structure principles - Broke long sentences into shorter, punchier statements - Strengthened verb choices and reduced passive voice - Improved topic-stress positioning - Created better rhythm and clarity OPERATIONAL (paragraph/section): - Added backward references between subsections - Strengthened transitions between major sections - Improved coherence within sections - Made topic strings more consistent STRATEGIC (document-level): - Enhanced Heilmeier question alignment - Strengthened section-to-section connections - Made 'what is new' clearer throughout - Ensured each section explicitly addresses its assigned questions - Improved overall narrative flow Focus: Clarity and impact over nitpicking. Changes maintain technical precision while improving readability. --- 1-goals-and-outcomes/research_statement_v1.tex | 10 +++++----- 1-goals-and-outcomes/v1.tex | 12 ++++++------ 2-state-of-the-art/v2.tex | 18 +++++++++--------- 3-research-approach/v3.tex | 18 +++++++++--------- 4-metrics-of-success/v1.tex | 4 +++- 6-broader-impacts/v1.tex | 2 +- 8-schedule/v1.tex | 2 ++ 7 files changed, 35 insertions(+), 31 deletions(-) diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index 301b013..60fdc06 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -2,16 +2,16 @@ I develop autonomous control systems with mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook -Nuclear reactors today depend on extensively trained human operators. Operators follow detailed written procedures and switch between control objectives as plant conditions change. +Nuclear reactors today depend on extensively trained human operators who follow detailed written procedures and switch 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 systems could manage complex operational sequences without constant supervision—but only if they provide safety assurance equal to or exceeding human-operated systems. +Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. This threatens economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only if they provide safety assurance equal to or exceeding human-operated systems. % APPROACH PARAGRAPH Solution -I produce hybrid control systems correct by construction, unifying formal methods from computer science with control theory. +I produce hybrid control systems correct by construction. This unifies formal methods from computer science with control theory. % Rationale -Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together. +Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together. % 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. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking then exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy requirements imposed by each discrete mode. Engineers design these continuous controllers using standard control theory techniques. +Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking then exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements imposed by each discrete mode. Engineers design these continuous controllers using standard control theory techniques. Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove safe mode transitions, enabling local verification without global trajectory analysis. The 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 12dcf16..f501280 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -6,16 +6,16 @@ I develop autonomous hybrid control systems with mathematical guarantees of safe % 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 -Nuclear plants today depend on extensively trained human operators. Operators follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance. +Nuclear plants today depend 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—but only if they provide safety assurance equal to or exceeding human operators. +This reliance on human operators prevents autonomous control. It creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants. This threatens economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only if they provide safety assurance equal to or exceeding human operators. % APPROACH PARAGRAPH Solution -I produce hybrid control systems correct by construction, unifying formal methods with control theory. +I produce hybrid control systems correct by construction. This unifies formal methods with control theory. % 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 handle continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together. +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 handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together. % Hypothesis -Two steps close this gap. First, discrete mode transitions synthesize directly from written operating procedures. Second, continuous behavior between transitions verifies against discrete requirements. This approach formalizes operating procedures into logical specifications that constrain continuous dynamics. The result: autonomous controllers provably free from design defects. +Two steps close this gap. First, discrete mode transitions synthesize directly from written operating procedures. Second, continuous behavior between transitions verifies against discrete requirements. This formalizes operating procedures into logical specifications that constrain continuous dynamics. The result: 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. @@ -64,7 +64,7 @@ If successful, 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?} 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. Section 2 examines why prior work fails at this integration. Section 3 details how this approach succeeds. +\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. Section 2 examines why prior work fails at this integration and what limits current practice. Section 3 details what is new in this approach and why it will succeed. % 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 6600ab7..342f162 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -2,9 +2,9 @@ \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} -This section examines how nuclear reactors operate today. No current approach—whether human-centered or formal methods—provides autonomous control with end-to-end correctness guarantees. +This section examines how nuclear reactors operate today. No current approach provides autonomous control with end-to-end correctness guarantees—neither human-centered operation nor formal methods. -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. First, reactor operators and their operating procedures. Second, fundamental limitations of human-based operation. Third, formal methods approaches that verify discrete logic or continuous dynamics but not both together. These limits establish the verification gap that Section 3 addresses. @@ -12,9 +12,9 @@ These limits establish the verification gap that Section 3 addresses. Understanding the limits of current practice requires examining how nuclear plants operate today. Three aspects structure this analysis: the hierarchy of procedures, the role of operators in executing them, and the operational modes that govern reactor control. -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, and 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}. +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. 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. 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification: no mathematical proofs confirm that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants. +Procedure development relies on expert judgment and simulator validation—not formal verification. 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proofs confirm that procedures cover all possible plant states. No proofs confirm that required actions complete within available timeframes. No proofs confirm 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 @@ -31,9 +31,9 @@ This division between automated and human-controlled functions reveals the funda \subsection{Human Factors in Nuclear Accidents} -Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly. +The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly. -Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how. This determination introduces persistent failure modes. Training alone cannot eliminate these modes. +Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how. This determination introduces persistent failure modes that training alone cannot eliminate. Current-generation nuclear power plants employ over 3,600 active NRC-licensed reactor operators in the United States~\cite{operator_statistics}. These @@ -59,11 +59,11 @@ limitations are fundamental to human-driven control, not remediable defects. \subsection{Formal Methods} -The previous two subsections revealed two critical limitations of current practice. First: procedures lack formal verification despite rigorous development processes. Second: human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. +The previous two subsections revealed two critical limitations of current practice. First, procedures lack formal verification despite rigorous development processes. Second, human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. -Training and procedural improvements cannot solve these problems. They are fundamental limitations, not remediable defects. Formal methods might offer a solution by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems? +Training and procedural improvements cannot solve these problems—they are fundamental limitations, not remediable defects. Formal methods might offer a solution by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems? -Even the most advanced formal methods applications in nuclear control leave a critical verification gap. This subsection examines two approaches that illustrate this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap my research addresses. +Even the most advanced formal methods applications in nuclear control leave a critical verification gap. This subsection examines two approaches that illustrate this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each approach demonstrates the current state of formal methods while revealing the verification gap my 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 16bc7c3..1068b7e 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- -Previous approaches verified either discrete switching logic or continuous control behavior—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 either 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. -My approach bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata. +My approach bridges that gap. It composes formal methods from computer science with control-theoretic verification. It formalizes reactor operations as hybrid automata. -Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly. +Hybrid system verification faces a fundamental challenge. Discrete transitions change the governing vector field. This creates discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly. -This methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing 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. +This methodology decomposes the problem. It verifies 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. A high-assurance hybrid autonomous control system requires a mathematical description. This work draws on automata theory, temporal logic, and control theory to provide that description. A hybrid system is a dynamical system with both continuous and discrete states. This proposal addresses continuous autonomous hybrid systems specifically—systems with no external input where continuous states remain continuous when discrete states change, representing physical quantities that remain Lipschitz continuous. This work follows the nomenclature from the Handbook on Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here for convenience: @@ -56,7 +56,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 either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Prior work has not integrated them into a systematic design methodology spanning procedures to verified implementation. +\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Prior work has not integrated them into a systematic design methodology. No prior work spans procedures to verified implementation. Three innovations enable this integration: @@ -140,11 +140,11 @@ These factors combine to demonstrate feasibility on production control systems w \subsection{System Requirements, Specifications, and Discrete Controllers} -The previous subsection established the hybrid automaton formalism. This mathematical framework describes discrete modes, continuous dynamics, guards, and invariants. +The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. -Where do these formal descriptions originate? Nuclear operations already possess a natural hybrid structure. This structure maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. +Where do these formal descriptions originate? Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. -The approach does not impose artificial abstractions. It constructs formal hybrid systems from existing operational knowledge. This leverages decades of domain expertise encoded in operating procedures. +The approach constructs formal hybrid systems from existing operational knowledge rather than imposing artificial abstractions. This leverages decades of domain expertise already encoded in operating procedures. Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years, managing labor needs and supply chains to optimize scheduled maintenance and downtime. @@ -392,7 +392,7 @@ appropriate to the fidelity of the reactor models available. \subsubsection{Stabilizing Modes} -Transitory modes drive the system toward exit conditions. They answer the question: "can we reach the target?" +The previous subsection addressed transitory modes—modes that drive the system toward exit conditions. They answer the question: "can we reach the target?" 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. diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index 344e594..e0e55a9 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -2,7 +2,9 @@ \textbf{Heilmeier Question: How do we measure success?} -Section 3 established the technical approach—what I will do and why it will work. This section addresses how to measure success: Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5). +Section 3 established the technical approach. It answered what is new (compositional verification bridging discrete synthesis with continuous control) and why it will succeed (existing procedural structure, bounded complexity, industrial validation). This section addresses the next Heilmeier question: how to measure success. + +The answer: Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5). My 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 because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5. diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 28c5188..8cf6fe7 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -2,7 +2,7 @@ \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?} -Sections 2--5 established the complete technical research plan: what has been done and its limits (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). +Sections 2--5 established the complete technical research plan. Section 2 answered what has been done and identified the limits of current practice. Section 3 answered what is new and why it will succeed. Section 4 answered how success will be measured through TRL advancement. Section 5 answered what could prevent success and provided mitigation strategies for each risk. This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact. diff --git a/8-schedule/v1.tex b/8-schedule/v1.tex index a282130..a2a60cf 100644 --- a/8-schedule/v1.tex +++ b/8-schedule/v1.tex @@ -2,6 +2,8 @@ \textbf{Heilmeier Question: How long will it take?} +The complete research plan is now established. Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. The final Heilmeier question addresses timing and feasibility within a doctoral timeline. + 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. The first semester (Spring 2026) focuses on Thrust 1, translating startup