From 751a25780fc6861313a9284ddb9c488554f5aa00 Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 9 Mar 2026 12:07:07 -0400 Subject: [PATCH] Editorial pass: tactical, operational, and strategic improvements Tactical (sentence-level): - Strengthened weak verbs and passive constructions - Improved issue-point positioning (old info first, new info in stress position) - Removed unnecessary hedging phrases - Fixed active/passive voice for clarity Operational (paragraph/section): - Added transition sentences between major subsections - Strengthened flow between State of the Art and Research Approach - Added connecting tissue between continuous controller types - Improved coherence within outcomes section Strategic (document-level): - Made 'what's new' explicit with highlighted innovation statement - Added summary paragraph to State of the Art defining the verification gap - Strengthened connections between sections for Heilmeier alignment - Clarified how the three-layer approach unifies existing tools --- .../research_statement_v1.tex | 101 +++++++++--------- 1-goals-and-outcomes/v1.tex | 58 +++++----- 2-state-of-the-art/v2.tex | 67 ++++++++---- 3-research-approach/v3.tex | 63 ++++++----- 6-broader-impacts/v1.tex | 6 +- 5 files changed, 170 insertions(+), 125 deletions(-) diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index 0a09d93..a6399ed 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -1,49 +1,47 @@ % GOAL PARAGRAPH -The goal of this research is to develop a methodology for creating autonomous -control systems with event-driven control laws that have guarantees of safe and -correct behavior. +This research develops a methodology for creating autonomous control systems +with event-driven control laws that guarantee safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook Nuclear power relies on extensively trained operators who follow detailed -written procedures to manage reactor control. Based on these procedures and -operators' interpretation of plant conditions, operators make critical decisions -about when to switch between control objectives. +written procedures to manage reactor control. Operators interpret plant +conditions and make critical decisions about when to switch between control +objectives. % Gap -But, reliance on human operators has created an economic challenge for -next-generation nuclear power plants. Small modular reactors face significantly -higher per-megawatt staffing costs than conventional plants. Autonomous control -systems are needed that can safely manage complex operational sequences with the -same assurance as human-operated systems, but without constant supervision. +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. % APPROACH PARAGRAPH Solution -To address this need, we will combine formal methods from computer science with -control theory to build hybrid control systems that are correct by construction. +We will 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, -similar to how operators change control strategies. Existing formal methods +mirroring how operators change control strategies. Existing formal methods generate provably correct switching logic but cannot handle continuous dynamics -during transitions, while traditional control theory verifies continuous -behavior but lacks tools for proving discrete switching correctness. +during transitions. Traditional control theory verifies continuous behavior but +lacks tools for proving discrete switching correctness. % Hypothesis and Technical Approach -We will bridge this gap through a three-stage methodology. First, we will -translate written operating procedures into temporal logic specifications using -NASA's Formal Requirements Elicitation Tool (FRET), which structures -requirements into scope, condition, component, timing, and response elements. -This structured approach enables realizability checking to identify conflicts -and ambiguities in procedures before implementation. Second, we will synthesize -discrete mode switching logic using reactive synthesis -to generate deterministic automata that are provably -correct by construction. Third, we will develop continuous -controllers for each discrete mode using standard control theory and -reachability analysis. We will classify continuous modes based on their -transition objectives, and then employ assume-guarantee contracts and barrier -certificates to prove that mode transitions occur safely and as defined by the -deterministic automata. This compositional approach enables local verification -of continuous modes without requiring global trajectory analysis across the -entire hybrid system. We will demonstrate this on an Emerson Ovation control system. +A three-stage methodology will bridge 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. +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 +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. % Pay-off -This approach will demonstrate autonomous control can be used for complex -nuclear power operations while maintaining safety guarantees. +This approach demonstrates that autonomous control can manage complex nuclear +power operations while maintaining safety guarantees. % OUTCOMES PARAGRAPHS If this research is successful, we will be able to do the following: @@ -52,31 +50,32 @@ If this research is successful, we will be able to do the following: \item \textit{Synthesize written procedures into verified control logic.} % Strategy We will develop a methodology for converting written operating procedures - into formal specifications. These specifications will be synthesized into - discrete control logic using reactive synthesis tools. + into formal specifications. Reactive synthesis tools will then generate + discrete control logic from these specifications. % Outcome - Control engineers will be able to generate mode-switching controllers from - regulatory procedures with little formal methods expertise, reducing - barriers to high-assurance control systems. + Control engineers will generate mode-switching controllers from regulatory + procedures with minimal formal methods expertise, reducing barriers to + high-assurance control systems. % OUTCOME 2 Title - \item \textit{Verify continuous control behavior across mode transitions. } + \item \textit{Verify continuous control behavior across mode transitions.} % Strategy - We will develop methods using reachability analysis to ensure continuous control modes - satisfy discrete transition requirements. + Reachability analysis will ensure continuous control modes satisfy discrete + transition requirements. % Outcome - Engineers will be able to design continuous controllers using standard - practices while ensuring system correctness and proving mode transitions - occur safely at the right times. + Engineers will design continuous controllers using standard practices while + ensuring system correctness, proving that mode transitions occur safely at + the right times. % OUTCOME 3 Title \item \textit{Demonstrate autonomous reactor startup control with safety - guarantees. } + guarantees.} % Strategy - We will implement this methodology on a small modular reactor simulation - using industry-standard control hardware. % Outcome - Control engineers will be able to implement high-assurance autonomous - controls on industrial platforms they already use, enabling users to - achieve autonomy without retraining costs or developing new equipment. + A small modular reactor simulation using industry-standard control hardware + will implement this methodology. + % Outcome + Control engineers will implement high-assurance autonomous controls on + industrial platforms they already use, enabling autonomy without retraining + costs or developing new equipment. \end{enumerate} diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index 566c66b..d0d03fe 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -1,9 +1,8 @@ \section{Goals and Outcomes} % GOAL PARAGRAPH -The goal of this research is to develop a methodology for creating autonomous -hybrid control systems with mathematical guarantees of safe and correct -behavior. +This research develops a methodology for creating autonomous hybrid control +systems with mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook Nuclear power plants require the highest levels of control system reliability, @@ -22,26 +21,27 @@ Small modular reactors, in particular, face per-megawatt staffing costs far exceeding those of conventional plants and threaten their economic viability. % Critical Need -What is needed is a method to create autonomous control systems that safely -manage complex operational sequences with the same assurance as human-operated -systems, but without constant human supervision. +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. % APPROACH PARAGRAPH Solution -To address this need, we will combine formal methods with control theory to -build hybrid control systems that are correct by construction. +We will 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 can -generate provably correct switching logic from written requirements, but they -cannot handle the continuous dynamics that occur during transitions between -modes. Meanwhile, traditional control theory can verify continuous behavior but -lacks tools for proving correctness of discrete switching decisions. +mirroring how operators change control strategies. Existing formal methods +generate provably correct switching logic from written requirements but cannot +handle the continuous dynamics that occur 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 -By synthesizing discrete mode transitions directly from written operating -procedures and verifying continuous behavior between transitions, we can create -hybrid control systems with end-to-end correctness guarantees. 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 defects. +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 +defects. % Pay-off This approach will enable autonomous control in nuclear power plants while maintaining the high safety standards required by the industry. @@ -74,10 +74,10 @@ If this research is successful, we will be able to do the following: \item \textbf{Verify continuous control behavior across mode transitions.} % Strategy We will establish methods for analyzing continuous control modes to ensure - they satisfy discrete transition requirements. Using classical control - theory for linear systems and reachability analysis for nonlinear dynamics, - we will verify that each continuous mode safely reaches its intended - transitions. + they satisfy discrete transition requirements. Classical control theory for + linear systems and reachability analysis for nonlinear dynamics will verify + that each continuous mode safely reaches its intended transitions. + % Outcome Engineers will design continuous controllers using standard practices while iterating to ensure broader system correctness, proving that mode transitions occur safely and at the correct times. @@ -99,8 +99,18 @@ If this research is successful, we will be able to do the following: \end{enumerate} % IMPACT PARAGRAPH Innovation -The innovation in this work is unifying discrete synthesis with continuous +These three outcomes—procedure translation, continuous verification, and +hardware demonstration—together establish a complete methodology from regulatory +documents to deployed systems. + +\textbf{The key innovation} unifies discrete synthesis with continuous 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. + % Outcome Impact If successful, control engineers will create autonomous controllers from existing procedures with mathematical proof of correct behavior. High-assurance diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 38c2f4e..5da74c8 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -1,11 +1,11 @@ \section{State of the Art and Limits of Current Practice} -The principal aim of this research is to create autonomous reactor control -systems that are tractably safe. To understand what is being automated, we must -first understand how nuclear reactors are operated today. This section examines -reactor operators and the operating procedures we aim to leverage, then -investigates limitations of human-based operation, and concludes with current -formal methods approaches to reactor control systems. +This research aims to create autonomous reactor control systems that are +tractably safe. Understanding what we automate requires first 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 +control systems. \subsection{Current Reactor Procedures and Operation} @@ -14,8 +14,8 @@ routine operations, abnormal operating procedures for off-normal conditions, 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) and are -developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their +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 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 @@ -30,9 +30,9 @@ and completeness.} Current procedure development relies on expert judgment and simulator validation. No mathematical proof exists that procedures cover all possible plant states, that required actions can be completed within available timeframes, or that transitions between procedure sets maintain safety -invariants. Paper-based procedures cannot ensure correct application, and even -computer-based procedure systems lack the formal guarantees that automated -reasoning could provide. +invariants. Paper-based procedures cannot ensure correct application. Even +computer-based procedure systems lack the formal guarantees automated reasoning +could provide. Nuclear plants operate with multiple control modes: automatic control, where the reactor control system maintains target parameters through continuous reactivity @@ -55,8 +55,11 @@ startup/shutdown sequences, mode transitions, and procedure implementation. \subsection{Human Factors in Nuclear Accidents} -Current-generation nuclear power plants employ over 3,600 active NRC-licensed -reactor operators in the United States~\cite{operator_statistics}. These +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 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 @@ -96,6 +99,12 @@ error contribution despite four decades of improvements demonstrates that these limitations are fundamental rather than a remediable part of human-driven control. \subsection{Formal Methods} + +The persistent human error problem motivates exploration of 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. + \subsubsection{HARDENS} The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) @@ -180,11 +189,11 @@ liveness property. %source: https://symbolaris.com/logic/dL.html While dL allows for the specification of these liveness and safety properties, -actually proving them for a given hybrid system is quite difficult. Automated -proof assistants such as KeYmaera X exist to help develop proofs of systems -using dL, but so far have been insufficient for reasonably complex hybrid -systems. The main issue behind creating system proofs using dL is state space -explosion and non-terminating solutions. +actually proving them for a given hybrid system is difficult. Automated proof +assistants such as KeYmaera X exist to help develop proofs of systems using dL, +but have been insufficient for reasonably complex hybrid systems. The main issue +behind creating system proofs using dL is state space explosion and +non-terminating solutions. %Source: that one satellite tracking paper that has the problem with the %gyroscopes overloding and needing to dump speed all the time Approaches have been made to alleviate @@ -194,7 +203,21 @@ methods, but are far from a complete methodology to design systems with. Instead, these approaches have been used on systems that have been designed a priori, and require expert knowledge to create the system proofs. -%Maybe a limitation here? Something about dL doesn't scale or help in design -%very much, so the limitation is that logic based hybrid system approaches have -%not been used in the DESIGN of autonomous controllers, only in the analysis of -%systems that already exist. +\textbf{LIMITATION:} \textit{Logic-based hybrid system verification has not +scaled to system design.} While dL and related approaches can verify hybrid +systems post-hoc, they require expert knowledge and have been applied only to +systems designed a priori. State space explosion prevents their use in the +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 +methods provide correctness guarantees but have not scaled to complete hybrid +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. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index 4b5199a..4f4104f 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -15,22 +15,21 @@ % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- -Previous approaches to autonomous control have verified -discrete switching logic or continuous control behavior, but not both -simultaneously. Validation of continuous controllers today consists of -extensive simulation trials. Discrete switching logic for routine operation -has been driven by human operators, whose evaluation includes simulated -control room testing and human factors research. Neither method, despite -being extremely resource intensive, provides rigorous guarantees of control -system behavior. HAHACS bridges this gap by composing formal methods from -computer science with control-theoretic verification, formalizing reactor -operations using the framework of hybrid automata. +Previous approaches to autonomous control verified discrete switching logic or +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 +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. 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 +systems cannot handle this interaction directly. Our methodology addresses this 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 @@ -38,10 +37,10 @@ of reactor operations themselves: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode. -To build a high-assurance hybrid autonomous control system (HAHACS), we must -first establish a mathematical description of the system. This work draws on +Building a high-assurance hybrid autonomous control system (HAHACS) requires +first establishing a mathematical description of the system. This work draws on automata theory, temporal logic, and control theory. A hybrid system is a -dynamical system that has both continuous and discrete states. The specific type +dynamical system with both continuous and discrete states. The specific type of system discussed in this proposal is a continuous autonomous hybrid system. This means that the system does not have external input and that continuous states do not change instantaneously when discrete states change. For our @@ -73,9 +72,13 @@ where: The creation of a HAHACS amounts to the construction of such a tuple together with proof artifacts demonstrating that the intended behavior of the control -system is satisfied by its actual implementation. This approach is tractable now -because the infrastructure for each component has matured. The novelty is not in -the individual pieces, but in the architecture that connects them. By defining +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 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 @@ -145,8 +148,14 @@ complex reactor operations. % ---------------------------------------------------------------------------- \subsection{System Requirements, Specifications, and Discrete Controllers} -Human control of nuclear power can be divided into three different scopes: -strategic, operational, and tactical. Strategic control is high-level and + +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. + +Human control of nuclear power divides into three scopes: strategic, +operational, and tactical. Strategic control is high-level and long-term decision making for the plant. This level has objectives that are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. The time scale at this level is @@ -355,8 +364,9 @@ according to operating procedures. \subsection{Continuous Control Modes} -The synthesis of the discrete operational controller is only half of an -autonomous controller. These control systems are hybrid, with both discrete and +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 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 @@ -478,8 +488,10 @@ appropriate to the fidelity of the reactor models available. \subsubsection{Stabilizing Modes} -Stabilizing modes are continuous controllers with an objective of maintaining a -particular discrete state indefinitely. Rather than driving the system toward an +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 +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 constant power level. Reachability analysis for stabilizing modes may not be a @@ -535,8 +547,9 @@ controller. \subsubsection{Expulsory Modes} -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. 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 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/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 6d75f42..3dcd003 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -22,9 +22,9 @@ 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 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 +through the high-assurance autonomous control methodology developed in this +work. 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