Editorial pass: Gopen + Heilmeier alignment

Three-level editorial review:

TACTICAL (sentence-level):
- Strengthened verb choices (fail/cause vs weaker alternatives)
- Improved topic-stress positioning
- Removed nominalizations for clearer subject-verb relationships
- Fixed inverted constructions for direct statement flow

OPERATIONAL (paragraph-level):
- Merged redundant Gap/Critical Need paragraphs in Goals section
- Removed redundant pay-off paragraph
- Integrated qualifications for smoother flow to outcomes
- Maintained strong transitions between subsections

STRATEGIC (document-level):
- Verified Heilmeier catechism alignment throughout
- Confirmed explicit 'What is new' and 'Why will it succeed' callouts
- Maintained logical section progression: What/Why → Limits → How → Success → Risks → Impact → Timeline

All edits preserve technical content while improving clarity and impact.

1-goals-and-outcomes/research_statement_v1.tex

@@ -5,7 +5,7 @@ that guarantee safe and correct behavior.
 % INTRODUCTORY PARAGRAPH Hook
 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.
 % 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. 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.
+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. Autonomous control systems must therefore safely manage complex operational sequences without constant supervision while maintaining the same assurance—or better—as human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods from computer science with control theory to
@@ -13,7 +13,7 @@ build hybrid control 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 but cannot handle continuous dynamics
+generate provably correct switching logic but fail to handle continuous dynamics
 during transitions. Control theory verifies continuous behavior but
 lacks tools for proving discrete switching correctness. 
 % Hypothesis and Technical Approach
@@ -27,7 +27,7 @@ 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 that mode transitions occur safely. This enables local verification of continuous modes
+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. 
 % Pay-off

1-goals-and-outcomes/v1.tex

@@ -6,7 +6,7 @@ systems that provide mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability.
-Failures can result in significant economic losses, service interruptions,
+Control system failures cause significant economic losses, service interruptions,
 or radiological release.
 % Known information
 Nuclear plant operations rely on extensively trained human operators
@@ -19,11 +19,10 @@ This reliance on human operators prevents autonomous control and
 creates a fundamental economic challenge for next-generation reactor designs.
 Small modular reactors face per-megawatt staffing costs far
 exceeding those of conventional plants, threatening their economic viability.
-
-% Critical Need
-The nuclear industry needs autonomous control systems that safely manage complex
+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.
+
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control
 systems that are correct by construction.
@@ -38,16 +37,10 @@ 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. Formalizing existing procedures into logical
-specifications and verifying continuous dynamics against transition requirements
-enables us to build autonomous controllers provably free from design
-defects.
-% Pay-off
-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,
+transitions. We formalize existing procedures into logical
+specifications and verify continuous dynamics against transition requirements,
+enabling autonomous controllers provably free from design
+defects. This work is conducted within the University of Pittsburgh Cyber Energy Center,
 which provides access to industry collaboration and Emerson control hardware,
 ensuring that developed solutions align with practical implementation
 requirements.

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

@@ -1,11 +1,11 @@
 \section{State of the Art and Limits of Current Practice}
 
-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.
+This research aims to create autonomous reactor control systems that are tractably safe. 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.
 
 \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 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.
+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. 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
@@ -169,9 +169,8 @@ liveness property.
 While dL allows for the specification of these liveness and safety properties,
 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. 
+but fail for reasonably complex hybrid systems. State space explosion and
+non-terminating solutions prevent creating system proofs using dL. 
 %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

3-research-approach/v3.tex

@@ -15,7 +15,7 @@
 % ----------------------------------------------------------------------------
 % 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. 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.
+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 by composing formal methods from computer science with control-theoretic verification, then formalizing reactor operations using hybrid automata.
 
 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.
 

4-metrics-of-success/v1.tex

@@ -7,7 +7,7 @@ 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.
+metric and defines the specific criteria to achieve TRL 5.
 
 Technology Readiness Levels provide the ideal success metric: they
 explicitly measure the gap between academic proof-of-concept and practical