Editorial pass: Three-level copy-editing (tactical/operational/strategic)

Pass 1 (Tactical - sentence level):
- Strengthened verb constructions (fail/lack vs cannot/will not)
- Improved topic-stress positioning
- Reduced weak passive voice
- Removed unnecessary future tense (will → present)
- Enhanced issue-point positioning per Gopen

Pass 2 (Operational - paragraph/section):
- Improved transitions between major sections
- Enhanced coherence within subsections
- Smoothed flow between State of Art → Research Approach

Pass 3 (Strategic - document level):
- Sharpened Heilmeier catechism alignment
- Clarified 'what difference it makes' (economic impact)
- Strengthened 'what is new' positioning
- Enhanced 'why it will succeed' specificity
- Improved 'how we measure success' clarity

All changes maintain technical accuracy while improving clarity and impact.

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,11 +1,11 @@
 % GOAL PARAGRAPH
-This research develops a methodology that creates autonomous control systems
+This research develops a methodology for creating autonomous control systems
 with guaranteed safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 Extensively trained operators manage nuclear reactor control by following detailed written procedures. 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 staffing costs that significantly exceed those of conventional plants. This economic constraint threatens their viability without autonomous control. Autonomous control systems must therefore manage complex operational sequences safely, without constant supervision, while maintaining the same assurance—or better—than human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. Without autonomous control, this economic constraint threatens their viability. Autonomous control systems must therefore manage complex operational sequences safely, without constant supervision, while providing assurance equal to—or better than—human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods from computer science with control theory to
@@ -13,26 +13,26 @@ build hybrid control systems that are correct by construction.
 % Rationale
 Hybrid systems mirror operator behavior: discrete
 logic switches between continuous control modes. Existing formal methods
-generate provably correct switching logic but cannot handle continuous dynamics
+generate provably correct switching logic but fail to handle continuous dynamics
 during transitions. Control theory verifies continuous behavior but
-cannot prove discrete switching correctness. 
+lacks tools to prove discrete switching correctness. 
 % Hypothesis and Technical Approach
 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. Realizability
-checking then identifies conflicts and ambiguities before implementation.
-Second, reactive synthesis generates deterministic automata that are provably
+checking identifies conflicts and ambiguities before implementation.
+Second, reactive synthesis generates deterministic automata provably
 correct by construction.
 Third, we design continuous controllers for each discrete mode using standard
 control theory and verify them using reachability analysis. We classify continuous modes based on
 their transition objectives, then employ assume-guarantee contracts and barrier
 certificates to prove mode transitions occur safely. This approach enables local verification of continuous modes
-without global trajectory analysis across the entire hybrid system. An
-Emerson Ovation control system will demonstrate this methodology. 
+without requiring global trajectory analysis across the entire hybrid system. An
+Emerson Ovation control system demonstrates this methodology. 
 % Pay-off
 This approach demonstrates that autonomous control can manage complex nuclear
-power operations while maintaining safety guarantees.
+power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS
 If this research is successful, we will be able to do the following:
@@ -41,21 +41,21 @@ 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. Reactive synthesis tools will then generate
+    into formal specifications. Reactive synthesis tools generate
     discrete control logic from these specifications.
     % Outcome
-    Control engineers will generate mode-switching controllers from regulatory
-    procedures with minimal formal methods expertise. This reduces barriers to
+    Control engineers 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.}
     % Strategy
-    Reachability analysis will verify that continuous control modes satisfy discrete
+    Reachability analysis verifies that continuous control modes satisfy discrete
     transition requirements. 
     % Outcome
-    Engineers will design continuous controllers using standard practices while
-    maintaining formal correctness guarantees. Mode transitions will provably occur safely and at
+    Engineers design continuous controllers using standard practices while
+    maintaining formal correctness guarantees. Mode transitions provably occur safely and at
     the correct times.
 
     % OUTCOME 3  Title
@@ -63,10 +63,10 @@ If this research is successful, we will be able to do the following:
     guarantees.}
     % Strategy
     A small modular reactor simulation using industry-standard control hardware
-    will implement this methodology.
+    implements this methodology.
     % Outcome
-    Control engineers will implement high-assurance autonomous controls on
-    industrial platforms they already use. This enables autonomy without retraining
+    Control engineers implement high-assurance autonomous controls on
+    industrial platforms they already use, enabling autonomy without retraining
     costs or new equipment development.
 
 \end{enumerate}

1-goals-and-outcomes/v1.tex

@@ -1,12 +1,12 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops a methodology that creates autonomous hybrid control
+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.
-Control system failures cause significant economic losses, service interruptions,
+Control system failures risk significant economic losses, service interruptions,
 or radiological release.
 % Known information
 Nuclear plant operations rely on extensively trained human operators
@@ -20,8 +20,8 @@ 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 their economic viability.
 The nuclear industry therefore needs autonomous control systems that safely manage complex
-operational sequences without constant human supervision while maintaining
-higher assurance than human-operated systems.
+operational sequences without constant human supervision while providing
+assurance higher than human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control
@@ -29,7 +29,7 @@ systems that are correct by construction.
 % Rationale
 Hybrid systems mirror how operators work: discrete
 logic switches between continuous control modes. Existing formal methods
-generate provably correct switching logic from written requirements but cannot
+generate provably correct switching logic from written requirements but fail to
 handle the continuous dynamics during transitions between modes.
 Control theory verifies continuous behavior but lacks tools for
 proving correctness of discrete switching decisions. This gap between discrete
@@ -53,38 +53,38 @@ If this research is successful, we will be able to do the following:
   % OUTCOME 1 Title
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
-    We will develop a methodology for converting existing written operating
+    We develop a methodology for converting existing written operating
     procedures into formal specifications that can be automatically synthesized
-    into discrete control logic. This process will use structured intermediate
+    into discrete control logic. This process uses structured intermediate
     representations to bridge natural language procedures and mathematical
     logic.
     % Outcome
-    Control system engineers will generate verified mode-switching controllers
+    Control system engineers generate verified mode-switching controllers
     directly from regulatory procedures without formal methods expertise,
     lowering the barrier to high-assurance control systems.
 
     % OUTCOME 2 Title
   \item \textbf{Verify continuous control behavior across mode transitions.}
     % Strategy
-    We will establish methods for analyzing continuous control modes to verify
+    We establish methods for analyzing continuous control modes to verify
     they satisfy discrete transition requirements. Classical control theory for
-    linear systems and reachability analysis for nonlinear dynamics will verify
+    linear systems and reachability analysis for nonlinear dynamics verify
     that each continuous mode safely reaches its intended transitions.
     % Outcome
-    Engineers will design continuous controllers using standard practices while
-    maintaining formal correctness guarantees. Mode transitions will provably occur safely and at the correct times.
+    Engineers design continuous controllers using standard practices while
+    maintaining formal correctness guarantees. Mode transitions provably occur safely and at the correct times.
 
     % OUTCOME 3  Title
   \item \textbf{Demonstrate autonomous reactor startup control with safety
     guarantees.}
     % Strategy
-    We will apply this methodology to develop an autonomous controller for
+    We apply this methodology to develop an autonomous controller for
     nuclear reactor startup procedures, implementing it on a small modular
     reactor simulation using industry-standard control hardware. This
-    demonstration will prove correctness across multiple coordinated control
+    demonstration proves correctness across multiple coordinated control
     modes from cold shutdown through criticality to power operation.
     % Outcome
-    We will demonstrate that autonomous hybrid control can be realized in the
+    We demonstrate that autonomous hybrid control can be realized in the
     nuclear industry with current equipment, establishing a path toward reduced
     operator staffing while maintaining safety.
 
@@ -94,20 +94,20 @@ If this research is successful, we will be able to do the following:
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—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.
-Formal methods can verify discrete logic. Control theory can verify
+Formal methods verify discrete logic. Control theory verifies
 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. This enables independent
+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
+If successful, control engineers create autonomous controllers from
 existing procedures with mathematical proofs of correct behavior. High-assurance
-autonomous control will become practical for safety-critical applications.
+autonomous control becomes practical for safety-critical applications.
 % Impact/Pay-off
 This capability is essential for the economic viability of next-generation
 nuclear power. Small modular reactors offer a promising solution to growing
 energy demands, but their success depends on reducing per-megawatt operating
-costs through increased autonomy. This research will provide the tools to
+costs through increased autonomy. This research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the
 nuclear industry requires.

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

@@ -1,11 +1,11 @@
 \section{State of the Art and Limits of Current Practice}
 
-This research creates autonomous reactor control systems that are 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.
+This research creates tractably safe autonomous reactor control systems. 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 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
-provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Expert judgment and simulator validation—not formal verification—drive their development. 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. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Expert judgment and simulator validation—not formal verification—drive their development. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} rigorously assess procedures. Yet this rigor fails to provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -27,8 +27,8 @@ Protection Systems trip automatically on safety signals with millisecond
 response times, and engineered safety features actuate automatically on accident
 signals without operator action required.
 
-The division between automated and human-controlled functions reveals the
-fundamental challenge of hybrid control. Highly automated systems handle reactor
+The division between automated and human-controlled functions reveals hybrid control's
+fundamental challenge. Highly automated systems handle reactor
 protection---automatic trips on safety parameters, emergency core cooling
 actuation, containment isolation, and basic process
 control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
@@ -48,7 +48,7 @@ and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
 operator requires several years of training.
 
 Human error persistently contributes to nuclear safety incidents despite decades
-of improvements in training and procedures. This provides compelling
+of improvements in training and procedures, providing 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
@@ -75,13 +75,13 @@ systemic weaknesses that create conditions for failure.
 
 
 \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
-that training alone cannot overcome.} Four decades of improvements have not eliminated human
+that training alone cannot overcome.} Four decades of improvements have failed to eliminate human
 error. These
 limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Training alone cannot eliminate the fundamental reliability limits imposed by human error. 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.
+Training alone fails to eliminate the fundamental reliability limits imposed by human error. 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.
 
 \subsubsection{HARDENS}
 
@@ -188,7 +188,7 @@ 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—four decades of training improvements have not eliminated them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design.
+Current practice reveals a fundamental gap. Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design.
 
 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.
 

3-research-approach/v3.tex

@@ -15,9 +15,9 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-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. Neither method provides rigorous guarantees of control system behavior, despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification to formalize reactor operations using hybrid automata.
+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. Neither method provides rigorous guarantees of control system behavior, despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations using hybrid automata.
 
-Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, 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: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about 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.
+Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—fail to handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about 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.
 
 Building a high-assurance hybrid autonomous control system (HAHACS) requires
 establishing a mathematical description of the system. This work draws on
@@ -53,9 +53,9 @@ where:
 
 Creating a HAHACS requires constructing such a tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
 
-\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 that connects discrete synthesis with continuous verification through well-defined interfaces.
+\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—specifically, mode-level verification that avoids global hybrid system analysis.
 
-\textbf{Why it will succeed:} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and 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.
+\textbf{Why it will succeed:} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into tractable local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and 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.
 
 \begin{figure} 
   \centering

4-metrics-of-success/v1.tex

@@ -1,13 +1,13 @@
 \section{Metrics for Success}
 
-\textbf{The exams:} This research will be measured by advancement through
-Technology Readiness Levels, progressing from fundamental concepts to validated
-prototype demonstration.
+\textbf{How we measure success:} This research advances through
+Technology Readiness Levels, progressing from fundamental concepts (TRL 2--3) to validated
+prototype demonstration (TRL 5).
 
 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 to achieve TRL 5.
+metric and defines specific criteria for achieving TRL 5.
 
 Technology Readiness Levels provide the ideal success metric: they
 explicitly measure the gap between academic proof-of-concept and practical

5-risks-and-contingencies/v1.tex

@@ -1,12 +1,12 @@
 \section{Risks and Contingencies}
 
-This research relies on several critical assumptions that, if invalidated, would
-require scope adjustment or methodological revision. Four primary risks could prevent
+This research relies on several critical assumptions that, if invalidated, require
+scope adjustment or methodological revision. Four primary risks could prevent
 successful completion: computational tractability of
 synthesis and verification, complexity of the discrete-continuous interface,
 completeness of procedure formalization, and hardware-in-the-loop integration
 challenges. Each risk has associated indicators for early detection and
-contingency plans that preserve research value even if core assumptions prove
+contingency plans preserving research value even if core assumptions prove
 false. The staged project structure ensures that partial success yields
 publishable results and clear identification of remaining barriers to
 deployment.

6-broader-impacts/v1.tex

@@ -24,8 +24,8 @@ approximately 23--30\% of the total levelized cost of electricity, translating
 to \$21--28 billion annually for projected datacenter demand.
 
 \textbf{What difference it makes:} This research directly addresses the
-multi-billion-dollar O\&M cost challenge through high-assurance autonomous
-control.
+\$21--28 billion annual O\&M cost challenge through high-assurance autonomous
+control, making small modular reactors economically viable for datacenter power.
 
 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