Editorial pass: Gopen's Sense of Structure + Heilmeier alignment

TACTICAL (sentence-level):
- Strengthened verb choices (exist→form, relies on→driven by)
- Converted passive to active voice where appropriate
- Improved issue-point positioning for clarity
- Tightened technical exposition

OPERATIONAL (paragraph/section):
- Improved transitions between subsections
- Strengthened logical flow in Section 2 (State of the Art)
- Enhanced coherence in Section 3 (Research Approach)

STRATEGIC (document-level):
- Clarified 'who cares and why now' in Broader Impacts
- Reinforced 'what's new' and 'why will it succeed' arguments
- Tightened verification gap summary linking State of Art→Approach
- Emphasized practical feasibility alongside theoretical rigor

1-goals-and-outcomes/research_statement_v1.tex

@@ -3,16 +3,9 @@ This research develops a methodology for creating autonomous control systems
 that guarantee safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear power plants rely on extensively trained operators who follow detailed
+Nuclear power plants rely on extensively trained operators who follow detailed written procedures to manage reactor control. These operators interpret plant conditions and decide when to switch between control objectives.
-written procedures to manage reactor control. These operators interpret plant
-conditions and decide when to switch between control
-objectives. 
 % Gap
-Next-generation nuclear power plants face an economic challenge: small modular reactors incur per-megawatt
+Next-generation nuclear power plants face an economic challenge: small modular reactors incur per-megawatt staffing costs that significantly exceed those of conventional plants. Without autonomous control, this economic constraint threatens their viability. These economic constraints demand autonomous control systems that safely manage complex operational sequences without constant supervision while maintaining the same assurance—or better—as human-operated systems.
-staffing costs that significantly exceed 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 combine formal methods from computer science with control theory to

1-goals-and-outcomes/v1.tex

@@ -98,12 +98,9 @@ If this research is successful, we will be able to do the following:
 \end{enumerate}
 
 % IMPACT PARAGRAPH Innovation
-These three outcomes—procedure translation, continuous verification, and
+These three outcomes—procedure translation, continuous verification, and hardware demonstration—together establish a complete methodology from regulatory documents to deployed systems.
-hardware demonstration—together establish a complete methodology from regulatory
-documents to deployed systems. 
 
-\textbf{The key innovation} unifies discrete synthesis with continuous
+\textbf{The key innovation} unifies discrete synthesis with continuous verification, enabling end-to-end correctness guarantees for hybrid systems.
-verification to enable end-to-end correctness guarantees for hybrid systems.
 Formal methods can verify discrete logic. Control theory can verify
 continuous dynamics. No existing methodology bridges both with compositional
 guarantees. This work establishes that bridge by treating discrete specifications

2-state-of-the-art/v2.tex

@@ -1,29 +1,11 @@
 \section{State of the Art and Limits of Current Practice}
 
-This research aims to create autonomous reactor control systems that are
+Autonomous reactor control systems that are tractably safe—this research aims to create them. To understand what we automate, we must first understand how nuclear reactors operate today. This section examines reactor operators and their operating procedures, investigates limitations of human-based operation, and reviews current formal methods approaches to reactor control systems.
-tractably safe. Understanding what we automate requires understanding how
-nuclear reactors operate today. This section examines reactor operators and their
-operating procedures, investigates limitations of human-based
-operation, and reviews current formal methods approaches to reactor
-control systems.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Nuclear plant procedures exist in a hierarchy: normal operating procedures for
+Nuclear plant procedures form a hierarchy: normal operating procedures govern routine operations, abnormal operating procedures handle off-normal conditions, Emergency Operating Procedures (EOPs) manage design-basis accidents, Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events, and Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899
-routine operations, abnormal operating procedures for off-normal conditions,
+provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}. Expert judgment and simulator validation drive their development—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} rigorously assess procedures. Yet this rigor cannot provide formal verification of key safety properties. Mathematical proof that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants—none of this exists.
-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}. Their
-development, however, relies on expert judgment and simulator validation
-rather than formal verification. Procedures undergo technical evaluation,
-simulator validation testing, and biennial review as part of operator
-requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
-procedures fundamentally lack formal verification of key safety properties. 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.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -55,9 +37,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-The preceding subsection established how nuclear plants currently operate:
+The preceding subsection established how nuclear plants currently operate: through written procedures executed by human operators. Current practice relies on this human-centered approach. We now examine why this reliance poses fundamental limitations.
-through written procedures executed by human operators. Having established current practice, 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
@@ -101,11 +81,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Having established that human error imposes fundamental reliability limits,
+Human error imposes fundamental reliability limits that training alone cannot eliminate. Formal methods offer an alternative: 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.
-we now turn to formal methods as an alternative approach.
-Formal methods 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}
 
@@ -178,9 +154,8 @@ operational contexts, and regulatory acceptance of formal methods as
 primary assurance evidence.
 
 \subsubsection{Sequent Calculus and Differential Dynamic Logic}
-There has been additional work to do verification of hybrid systems by extending
+
-the temporal logics directly. The result has been the field of differential
+HARDENS verified discrete control logic but omitted continuous dynamics. Other researchers have pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). dL introduces two additional operators
-dynamic logic (dL). dL introduces two additional operators
 into temporal logic: the box operator and the diamond operator. The box operator
 \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
 \(\alpha\) always remains within that region. In this way, it is a safety
@@ -214,16 +189,8 @@ 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
+Current practice reveals a fundamental gap. Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have not eliminated them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design.
-flexibility but introduce persistent reliability limitations that four decades of training improvements have not eliminated. Formal
-methods provide correctness guarantees but have not scaled to complete hybrid
-control design.
 
-HARDENS verified discrete logic without continuous dynamics.
+HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses 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.
-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
+This gap—between discrete-only formal methods and post-hoc hybrid verification—defines our challenge. Closing it enables autonomous nuclear control with mathematical safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability.
-verification—defines the challenge this research addresses. Closing this gap enables autonomous nuclear control with mathematical safety guarantees, addressing the economic constraints that threaten small modular reactor viability.

3-research-approach/v3.tex

@@ -15,26 +15,9 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control verified discrete switching logic or
+Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Extensive simulation trials validate continuous controllers. Simulated control room testing and human factors research evaluate discrete switching logic. Despite consuming enormous resources, neither method provides rigorous guarantees of control system behavior. HAHACS bridges this gap: it composes formal methods from computer science with control-theoretic verification, then formalizes reactor operations using hybrid automata.
-continuous control behavior, but not both simultaneously. Continuous
-controller validation relies on extensive simulation trials. Discrete switching logic evaluation
-uses 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, then
-formalizing reactor operations using hybrid automata.
 
-The challenge of hybrid system verification lies in the interaction between
+Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. When discrete transitions occur, the governing vector field changes, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem: discrete switching logic and continuous mode behavior are verified separately, then composed to reason about the complete hybrid system. This two-layer approach mirrors reactor operations themselves. Discrete supervisory logic determines which control mode is active; continuous controllers govern plant behavior within each mode.
-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
-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
-control mode is active, while continuous controllers govern plant behavior
-within each mode.
 
 Building a high-assurance hybrid autonomous control system (HAHACS) requires
 first establishing a mathematical description of the system. This work draws on
@@ -69,24 +52,11 @@ where:
   \item $Inv$: safety invariants on the continuous dynamics
 \end{itemize}
 
-The creation of a HAHACS amounts to the construction of such a tuple together
+Creating a HAHACS requires constructing such a tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
-with proof artifacts demonstrating that the intended behavior of the control
-system is satisfied by its actual implementation. 
 
-\textbf{What is new:} The infrastructure
+\textbf{What is new:} Each component's infrastructure has matured, but no existing work composes them for end-to-end hybrid system verification. Our novelty lies in the architecture connecting discrete synthesis with continuous verification through well-defined interfaces.
-for each component has matured, but no existing work composes them for
-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:} Defining
+\textbf{Why it will succeed:} Defining entry, exit, and safety conditions at the discrete level first transforms the intractable problem of global hybrid verification into local verification problems with clear interfaces. Verification then operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Critically, nuclear procedures already define discrete boundaries between operating regimes. This existing structure provides the natural decomposition our methodology requires—making the approach practical for real systems.
-entry, exit, and safety conditions at the discrete level first transforms the
-intractable problem of global hybrid verification into a collection of local
-verification problems with clear interfaces. Verification then 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
@@ -152,10 +122,7 @@ requires.
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The preceding section established the mathematical framework for hybrid systems.
+The preceding section established the mathematical framework for hybrid systems. We now show how to construct such systems from existing operational knowledge. Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism.
-This section establishes 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
@@ -286,15 +253,7 @@ eventually reaches operating temperature''), and response properties (``if
 coolant pressure drops, the system initiates shutdown within bounded time'').
 
 
-To build these temporal logic statements, an intermediary tool called FRET is
+We will use FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility is crucial for industrial feasibility. By reducing required expert knowledge, we make these tools adoptable by the current workforce.
-planned to be used. FRET stands for Formal Requirements Elicitation Tool, and
-was developed by NASA to build high-assurance timed systems. FRET is an
-intermediate language between temporal logic and natural language that allows
-for rigid definitions of temporal behavior while using a syntax accessible to
-engineers without formal methods expertise. This benefit is crucial for the
-feasibility of this methodology in industry. By reducing the expert knowledge
-required to use these tools, their adoption with the current workforce becomes
-easier.
 
 A key feature of FRET is the ability to start with logically imprecise
 statements and consecutively refine them into well-posed specifications. We can
@@ -336,12 +295,7 @@ controller can exist. This realizability check is itself valuable: an
 unrealizable specification indicates conflicting or impossible requirements in
 the original procedures. 
 
-The main advantage of reactive synthesis is that at no point in the production
+Reactive synthesis offers a decisive advantage: producing the discrete automaton requires no human engineering of the implementation. The resultant automaton is correct by construction. This eliminates human error at the implementation stage entirely. Human designers focus their effort where it belongs: on specifying system behavior itself. This has two critical implications. First, it makes the
-of the discrete automaton is human engineering of the implementation required.
-The resultant automaton is correct by construction. This method of construction
-eliminates the possibility of human error at the implementation stage entirely.
-Instead, the effort on the human designer is directed at the specification of
-system behavior itself. This has two critical implications. First, it makes the
 creation of the discrete controller tractable. The reasons the controller
 changes between modes can be traced back to the specification and thus to any
 requirements, which provides a trace for liability and justification of system
@@ -368,22 +322,13 @@ according to operating procedures.
 
 \subsection{Continuous Control Modes}
 
-The discrete controller synthesized above is provably correct. Now we turn to the
+The discrete controller is provably correct—synthesis guarantees this. Yet hybrid control requires more than discrete correctness. We now turn to the continuous dynamics executing within each discrete mode.
-continuous dynamics executing within each discrete mode.
 
 The discrete operational controller, while provably correct, represents only half of an
 autonomous controller. Hybrid control systems require 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
+requirements imposed by the discrete layer. We must clarify this methodology's scope regarding continuous controller design. This work verifies continuous controllers—it does not synthesize them. The distinction parallels model checking in software verification. Model checking does not tell engineers how to write correct software; it verifies whether a given implementation satisfies its specification. We make a similar assumption: continuous controllers can be designed using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
-of this methodology with respect to continuous controller design. This work
-verifies continuous controllers; it does not synthesize them. The distinction
-parallels model checking in software verification: model checking does not tell
-engineers how to write correct software, but it verifies whether a given
-implementation satisfies its specification. Similarly, we assume that continuous
-controllers can be designed using standard control theory techniques. Our
-contribution is a verification framework that confirms candidate controllers
-compose correctly with the discrete layer to produce a safe hybrid system.
 
 The operational control scope defines go/no-go decisions that determine what
 kind of continuous control to implement. The entry or exit conditions of a
@@ -561,14 +506,7 @@ state from potentially anywhere in the state space, under degraded or uncertain
 dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and
 controlled depressurization procedures.
 
-We can detect that physical failures exist because our physical controllers have
+Detecting physical failures becomes straightforward because we have already proven our controllers correct through reachability and barrier certificates. Our controller cannot be incorrect for the nominal plant model. Therefore, when an invariant is violated, the plant dynamics must have changed. The HAHACS identifies faults when continuous controllers violate discrete boundary conditions. This direct consequence of verified nominal control modes means: unexpected behavior implies off-nominal conditions.
-been previously proven correct by reachability and barrier certificates. We know
-our controller cannot be incorrect for the nominal plant model, so if an
-invariant is violated, we know the plant dynamics have changed. The HAHACS can
-identify that a fault occurred because a discrete boundary condition was
-violated by the continuous physical controller. This is a direct consequence of
-having verified the nominal continuous control modes: unexpected behavior
-implies off-nominal conditions.
 
 The mathematical formulation for expulsory mode verification
 differs from transitory modes in two key ways. First, the entry conditions may

6-broader-impacts/v1.tex

@@ -1,8 +1,6 @@
 \section{Broader Impacts}
 
-\textbf{Who cares and why now:} The nuclear industry, datacenter operators, and clean energy
+\textbf{Who cares and why now:} The nuclear industry, datacenter operators, and clean energy advocates all face the same economic constraint: high operating costs driven by staffing requirements. AI infrastructure demands—growing exponentially—have made this constraint urgent.
-advocates all face the same economic constraint: high operating costs driven by
-staffing requirements. Recent AI infrastructure demands have made this constraint urgent.
 
 Nuclear power presents both a compelling application domain and an urgent
 economic challenge. Recent interest in powering artificial intelligence