From 00c14339e0963e6580607b8f2527bf50eb3d2f83 Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 9 Mar 2026 12:12:33 -0400 Subject: [PATCH] Multi-level editorial pass: Gopen + Heilmeier alignment MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pass 1 (Tactical): Sentence-level improvements - Strengthened issue-point positioning (stress at sentence end) - Improved topic-stress flow (known→new information) - Converted passive to active voice where appropriate - Tightened verb choice and eliminated weak constructions - Fixed pronoun references and reduced unnecessary nominalizations Pass 2 (Operational): Paragraph and section flow - Improved transitions between paragraphs and subsections - Strengthened section-to-section handoffs - Enhanced coherence within major sections - Clarified the discrete-continuous interface explanation - Better signposting for the three controller types Pass 3 (Strategic): Heilmeier catechism alignment - Made 'What is new' and 'Why will it succeed' explicit - Strengthened 'Who cares' and 'What difference' in Broader Impacts - Clarified 'The exams' in Metrics section - Added 'How long' statement to Schedule - Improved overall narrative flow from problem→gap→solution→impact All changes preserve technical accuracy while improving clarity and impact. --- .../research_statement_v1.tex | 32 ++++----- 1-goals-and-outcomes/v1.tex | 38 +++++------ 2-state-of-the-art/v2.tex | 42 ++++++------ 3-research-approach/v3.tex | 65 +++++++++++-------- 4-metrics-of-success/v1.tex | 8 ++- 6-broader-impacts/v1.tex | 14 ++-- 8-schedule/v1.tex | 7 +- 7 files changed, 115 insertions(+), 91 deletions(-) diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index a6399ed..f88a000 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -1,41 +1,41 @@ % GOAL PARAGRAPH This research develops a methodology for creating autonomous control systems -with event-driven control laws that guarantee safe and correct behavior. +that guarantee safe and correct behavior through event-driven control laws. % INTRODUCTORY PARAGRAPH Hook -Nuclear power relies on extensively trained operators who follow detailed -written procedures to manage reactor control. Operators interpret plant +Nuclear power plants rely on extensively trained operators who follow detailed +written procedures to manage reactor control. These operators interpret plant conditions and make critical decisions about when to switch between control objectives. % Gap -This reliance on human operators creates an economic challenge for -next-generation nuclear power plants. Small modular reactors face per-megawatt -staffing costs that significantly exceed those of conventional plants. These -economic constraints demand autonomous control systems that safely manage -complex operational sequences with the same assurance as human-operated systems, -but without constant supervision. +Next-generation nuclear power plants face an economic challenge from this +reliance on human operators. Small modular reactors face per-megawatt +staffing costs significantly exceeding those of conventional plants. These +economic constraints demand autonomous control systems that can safely manage +complex operational sequences without constant supervision while maintaining the +same assurance as human-operated systems. % APPROACH PARAGRAPH Solution -We will combine formal methods from computer science with control theory to +We combine formal methods from computer science with control theory to build hybrid control systems that are correct by construction. % Rationale -Hybrid systems use discrete logic to switch between continuous control modes, -mirroring how operators change control strategies. Existing formal methods +Hybrid systems mirror how operators change control strategies: they use discrete +logic to switch between continuous control modes. Existing formal methods generate provably correct switching logic but cannot handle continuous dynamics during transitions. Traditional control theory verifies continuous behavior but lacks tools for proving discrete switching correctness. % Hypothesis and Technical Approach -A three-stage methodology will bridge this gap. First, we translate written +A three-stage methodology bridges this gap. First, we translate written operating procedures into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET). FRET structures requirements into scope, condition, component, timing, and response elements, enabling realizability checking that identifies conflicts and ambiguities before implementation. -Second, we synthesize discrete mode switching logic using reactive synthesis to -generate deterministic automata that are provably correct by construction. +Second, reactive synthesis generates deterministic automata that are provably +correct by construction for discrete mode switching logic. Third, we develop continuous controllers for each discrete mode using standard control theory and reachability analysis. We classify continuous modes based on their transition objectives, then employ assume-guarantee contracts and barrier -certificates to prove that mode transitions occur safely and as the +certificates to prove that mode transitions occur safely as the deterministic automata specify. Local verification of continuous modes becomes possible without global trajectory analysis across the entire hybrid system. An Emerson Ovation control system will demonstrate this methodology. diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index d0d03fe..43d8a60 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -2,11 +2,11 @@ % GOAL PARAGRAPH This research develops a methodology for creating autonomous hybrid control -systems with mathematical guarantees of safe and correct behavior. +systems that provide mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook -Nuclear power plants require the highest levels of control system reliability, -where failures can result in significant economic losses, service interruptions, +Nuclear power plants require the highest levels of control system reliability. +Failures can result in significant economic losses, service interruptions, or radiological release. % Known information Currently, nuclear plant operations rely on extensively trained human operators @@ -17,34 +17,34 @@ conditions and procedural guidance. % Gap This reliance on human operators prevents autonomous control capabilities and creates a fundamental economic challenge for next-generation reactor designs. -Small modular reactors, in particular, face per-megawatt staffing costs far -exceeding those of conventional plants and threaten their economic viability. +Small modular reactors face per-megawatt staffing costs far +exceeding those of conventional plants, threatening their economic viability. % Critical Need The nuclear industry needs autonomous control systems that safely manage complex -operational sequences with the same assurance as human-operated systems, but -without constant human supervision. +operational sequences without constant human supervision while maintaining the +same assurance as human-operated systems. % APPROACH PARAGRAPH Solution -We will combine formal methods with control theory to build hybrid control +We combine formal methods with control theory to build hybrid control systems that are correct by construction. % Rationale -Hybrid systems use discrete logic to switch between continuous control modes, -mirroring how operators change control strategies. Existing formal methods +Hybrid systems mirror how operators change control strategies: they use discrete +logic to switch between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but cannot -handle the continuous dynamics that occur during transitions between modes. +handle the continuous dynamics occurring during transitions between modes. Traditional control theory verifies continuous behavior but lacks tools for proving correctness of discrete switching decisions. This gap between discrete and continuous verification prevents end-to-end correctness guarantees. % Hypothesis Our approach closes this gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between -transitions. If existing procedures can be formalized into logical -specifications and continuous dynamics verified against transition requirements, -then autonomous controllers can be built that are provably free from design +transitions. If we can formalize existing procedures into logical +specifications and verify continuous dynamics against transition requirements, +we can build autonomous controllers provably free from design defects. % Pay-off -This approach will enable autonomous control in nuclear power plants while -maintaining the high safety standards required by the industry. +This approach enables autonomous control in nuclear power plants while +maintaining the high safety standards the industry requires. % Qualifications This work is conducted within the University of Pittsburgh Cyber Energy Center, @@ -107,9 +107,9 @@ documents to deployed systems. verification to enable end-to-end correctness guarantees for hybrid systems. While formal methods can verify discrete logic and control theory can verify continuous dynamics, no existing methodology bridges both with compositional -guarantees. This work establishes that bridge by treating discrete specifications -as contracts that continuous controllers must satisfy, enabling verification of -each layer independently while guaranteeing correct composition. +guarantees. This work establishes that bridge. It treats discrete specifications +as contracts that continuous controllers must satisfy, enabling independent +verification of each layer while guaranteeing correct composition. % Outcome Impact If successful, control engineers will create autonomous controllers from diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 5da74c8..2ff9896 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -1,10 +1,10 @@ \section{State of the Art and Limits of Current Practice} This research aims to create autonomous reactor control systems that are -tractably safe. Understanding what we automate requires first understanding how +tractably safe. Understanding what we automate requires understanding how nuclear reactors operate today. This section examines reactor operators and the -operating procedures we leverage, investigates limitations of human-based -operation, and concludes with current formal methods approaches to reactor +operating procedures we will leverage, investigates limitations of human-based +operation, and reviews current formal methods approaches to reactor control systems. \subsection{Current Reactor Procedures and Operation} @@ -15,7 +15,7 @@ Emergency Operating Procedures (EOPs) for design-basis accidents, Severe Accident Management Guidelines (SAMGs) for beyond-design-basis events, and Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899 -provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}, but this +provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}, but their development relies fundamentally on expert judgment and simulator validation rather than formal verification. Procedures undergo technical evaluation, simulator validation testing, and biennial review as part of operator @@ -55,19 +55,20 @@ startup/shutdown sequences, mode transitions, and procedure implementation. \subsection{Human Factors in Nuclear Accidents} -Having established how nuclear plants currently operate through written -procedures and human operators, we now examine why this human-centered approach -poses fundamental limitations. Current-generation nuclear power plants employ -over 3,600 active NRC-licensed reactor operators in the United -States~\cite{operator_statistics}. These +The preceding subsection established how nuclear plants currently operate: +through written procedures executed by human operators. This subsection examines +why this human-centered approach poses fundamental limitations. + +Current-generation nuclear power plants employ over 3,600 active NRC-licensed +reactor operators in the United States~\cite{operator_statistics}. These operators divide into Reactor Operators (ROs), who manipulate reactor controls, and Senior Reactor Operators (SROs), who direct plant operations and serve as shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor operator requires several years of training. -The persistent role of human error in nuclear safety incidents---despite decades -of improvements in training and procedures---provides the most compelling +Human error persistently plays a role in nuclear safety incidents despite decades +of improvements in training and procedures. This provides the most compelling motivation for formal automated control with mathematical safety guarantees. Operators hold legal authority under 10 CFR Part 55 to make critical decisions, including departing from normal regulations during emergencies. The Three Mile @@ -100,10 +101,10 @@ limitations are fundamental rather than a remediable part of human-driven contro \subsection{Formal Methods} -The persistent human error problem motivates exploration of formal methods to +The persistent human error problem motivates exploring formal methods to provide mathematical guarantees of correctness that human-centered approaches cannot achieve. This subsection examines recent formal methods work in nuclear -control and identifies their limitations for autonomous hybrid systems. +control and identifies limitations for autonomous hybrid systems. \subsubsection{HARDENS} @@ -211,13 +212,16 @@ design loop for complex systems like nuclear reactor startup procedures. \subsection{Summary: The Verification Gap} -Current practice reveals a fundamental gap: human operators provide operational -flexibility but introduce persistent reliability limitations, while formal +Current practice reveals a fundamental gap. Human operators provide operational +flexibility but introduce persistent reliability limitations. Formal methods provide correctness guarantees but have not scaled to complete hybrid -control design. HARDENS verified discrete logic without continuous dynamics. +control design. + +HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic can express hybrid properties but requires post-design expert analysis. 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—defines the challenge this research -addresses. +integrated into the design process. + +This gap—between discrete-only formal methods and post-hoc hybrid +verification—defines the challenge this research addresses. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index 4f4104f..e1afe6d 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -20,17 +20,17 @@ continuous control behavior, but not both simultaneously. Today's continuous controller validation consists of extensive simulation trials. Human operators drive discrete switching logic for routine operation; their evaluation includes simulated control room testing and human factors research. Neither method -provides rigorous guarantees of control system behavior, despite being +provides rigorous guarantees of control system behavior despite being extremely resource intensive. HAHACS bridges this gap by composing formal -methods from computer science with control-theoretic verification, formalizing -reactor operations using the framework of hybrid automata. +methods from computer science with control-theoretic verification and +formalizing reactor operations using the framework of hybrid automata. The challenge of hybrid system verification lies in the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in the system's behavior. Traditional verification techniques designed for purely discrete or purely continuous systems cannot handle this interaction directly. Our methodology addresses this -challenge through decomposition. We verify discrete switching logic and +challenge through decomposition: we verify discrete switching logic and continuous mode behavior separately, then compose these guarantees to reason about the complete hybrid system. This two-layer approach mirrors the structure of reactor operations themselves: discrete supervisory logic determines which @@ -76,14 +76,18 @@ system is satisfied by its actual implementation. \textbf{What is new:} This approach is tractable now because the infrastructure for each component has matured, but no existing work composes them for -end-to-end hybrid system verification. The novelty lies in the architecture that -connects discrete synthesis with continuous verification through well-defined -interfaces. By defining +end-to-end hybrid system verification. The novelty lies in the architecture +connecting discrete synthesis with continuous verification through well-defined +interfaces. + +\textbf{Why it will succeed:} By defining entry, exit, and safety conditions at the discrete level first, we transform the intractable problem of global hybrid verification into a collection of local -verification problems with clear interfaces. Verification is performed per mode -rather than on the full hybrid system, keeping the analysis tractable even for -complex reactor operations. +verification problems with clear interfaces. Verification operates per mode +rather than on the full hybrid system, keeping analysis tractable even for +complex reactor operations. Nuclear procedures already define discrete boundaries +between operating regimes, providing the natural decomposition this methodology +requires. \begin{figure} \centering @@ -149,10 +153,10 @@ complex reactor operations. \subsection{System Requirements, Specifications, and Discrete Controllers} -Having defined the hybrid system mathematical framework, we now establish how to -construct such systems from existing operational knowledge. The key insight is -that nuclear operations already have a natural hybrid structure that maps -directly to the automaton formalism. +The hybrid system mathematical framework defined above provides the foundation. +Now we establish how to construct such systems from existing operational knowledge. +The key insight: nuclear operations already possess a natural hybrid structure +that maps directly to the automaton formalism. Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control is high-level and @@ -364,9 +368,11 @@ according to operating procedures. \subsection{Continuous Control Modes} -With the discrete controller synthesized and provably correct, we turn to the -continuous dynamics that execute within each discrete mode. The synthesis of the -discrete operational controller is only half of an autonomous controller. These control systems are hybrid, with both discrete and +The discrete controller synthesized above is provably correct. Now we turn to the +continuous dynamics executing within each discrete mode. + +Synthesizing the discrete operational controller completes only half of an +autonomous controller. These control systems are hybrid: they have both discrete and continuous components. This section describes the continuous control modes that execute within each discrete state, and how we verify that they satisfy the requirements imposed by the discrete layer. It is important to clarify the scope @@ -393,11 +399,11 @@ computationally expensive, and analytic solutions often become intractable \cite{MANYUS THESIS}. We circumvent these issues by designing our hybrid system from the bottom up -with verification in mind. Each continuous control mode has an input set and -output set clearly defined by our discrete transitions \textit{a priori}. -Consider that we define the continuous state space as $\mathcal{X}$. Each -discrete mode $q_i$ then provides three key pieces of information for continuous -controller design: +with verification in mind. The discrete transitions define each continuous +control mode's input set and output set clearly \textit{a priori}. + +The continuous state space is $\mathcal{X}$. Each discrete mode $q_i$ provides +three key pieces of information for continuous controller design: \begin{enumerate} \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$, the set of possible initial states when entering this mode @@ -488,9 +494,10 @@ appropriate to the fidelity of the reactor models available. \subsubsection{Stabilizing Modes} -While transitory modes drive the system toward exit conditions, stabilizing -modes maintain the system within a desired operating region. Stabilizing modes -are continuous controllers with an objective of maintaining a particular +Transitory modes drive the system toward exit conditions. Stabilizing modes, in +contrast, maintain the system within a desired operating region. + +Stabilizing modes are continuous controllers designed to maintain a particular discrete state indefinitely. Rather than driving the system toward an exit condition, they keep the system within a safe operating region. Examples include steady-state power operation, hot standby, and load-following at @@ -547,9 +554,11 @@ controller. \subsubsection{Expulsory Modes} -Transitory and stabilizing modes handle nominal operations. When the plant -deviates from expected behavior, expulsory modes take over. Expulsory modes are -continuous controllers responsible for ensuring safety when failures occur. They are designed for robustness rather +Transitory and stabilizing modes handle nominal operations. Expulsory modes +handle off-nominal conditions. + +When the plant deviates from expected behavior, expulsory modes take over. These +continuous controllers ensure safety when failures occur. They are designed for robustness rather than 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 diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index 74956ce..90638de 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -1,8 +1,10 @@ \section{Metrics for Success} -This research will be measured by advancement through Technology Readiness -Levels, progressing from fundamental concepts to validated prototype -demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where +\textbf{The exams:} This research will be measured by advancement through +Technology Readiness Levels, progressing from fundamental concepts to validated +prototype demonstration. + +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 explains why TRL advancement provides the most appropriate success metric and defines the specific criteria required to achieve TRL 5. diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 3dcd003..5aded3c 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -1,5 +1,9 @@ \section{Broader Impacts} +\textbf{Who cares:} The nuclear industry, datacenter operators, and clean energy +advocates all face the same economic constraint: high operating costs driven by +staffing requirements. + 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 @@ -21,14 +25,16 @@ expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent approximately 23--30\% of the total levelized cost of electricity, translating to \$21--28 billion annually for projected datacenter demand. -This research directly addresses the multi-billion-dollar O\&M cost challenge -through the high-assurance autonomous control methodology developed in this -work. Current nuclear operations require full control room staffing for each +\textbf{What difference it makes:} This research directly addresses the +multi-billion-dollar O\&M cost challenge through high-assurance autonomous +control. + +Current nuclear operations require full control room staffing for each reactor, whether large conventional units or small modular designs. These staffing requirements drive the high O\&M costs that make nuclear power economically challenging, particularly for smaller reactor designs where the same staffing overhead must be spread across lower power output. Synthesizing provably correct hybrid controllers from formal -specifications can automate routine operational sequences that currently require +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 reactors rather than manually controlling individual units. diff --git a/8-schedule/v1.tex b/8-schedule/v1.tex index 415f6e8..c5a9991 100644 --- a/8-schedule/v1.tex +++ b/8-schedule/v1.tex @@ -1,7 +1,10 @@ \section{Schedule, Milestones, and Deliverables} -This research will be conducted over six trimesters (24 months) of full-time -effort following the proposal defense in Spring 2026. The work progresses +\textbf{How long it will take:} This research will be conducted over six +trimesters (24 months) of full-time effort following the proposal defense in +Spring 2026. All work uses existing computational and experimental resources +available through the University of Pittsburgh Cyber Energy Center and NRC +Fellowship funding. The work progresses sequentially through three main research thrusts before culminating in integrated demonstration and validation.