Copy edit: Multi-pass editorial improvements

TACTICAL (sentence-level):
- Applied Gopen principles: topic-stress positioning, verb choice
- Removed wordiness and redundant phrases
- Tightened prose for clarity and directness
- Fixed inconsistent punctuation

OPERATIONAL (paragraph-level):
- Improved transitions between subsections
- Enhanced paragraph coherence
- Added strategic paragraph breaks for better flow

STRATEGIC (document-level):
- Verified Heilmeier question alignment
- Strengthened section transitions
- Ensured consistent voice across sections

1-goals-and-outcomes/research_statement_v1.tex

@@ -4,7 +4,7 @@ This research develops autonomous control systems with mathematical guarantees o
 % INTRODUCTORY PARAGRAPH Hook
 Extensively trained operators manage nuclear reactors by following detailed written procedures. When operators switch between control objectives, plant conditions guide their decisions.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening their viability. To address this challenge, autonomous control systems must manage complex operational sequences safely—without constant supervision—while providing assurance equal to or exceeding that of human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening viability. Autonomous control systems must manage complex operational sequences safely—without constant supervision—while providing assurance equal to or exceeding that of 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.
 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
-during transitions. Control theory, conversely, verifies continuous behavior but
+during transitions. Control theory verifies continuous behavior but
 cannot prove the correctness of discrete switching decisions. 
 % Hypothesis and Technical Approach
 Our methodology bridges this gap through three stages. First, we translate written
@@ -24,11 +24,11 @@ checking identifies conflicts and ambiguities before implementation.
 Second, reactive synthesis generates deterministic automata that are 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 by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. This approach enables local verification of continuous modes
+control theory and verify them using reachability analysis. Continuous modes are classified by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. This approach enables local verification of continuous modes
 without requiring global trajectory analysis across the entire hybrid system. An
 Emerson Ovation control system demonstrates this methodology. 
 % Pay-off
-Autonomous control therefore manages complex nuclear
+Autonomous control manages complex nuclear
 power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS

1-goals-and-outcomes/v1.tex

@@ -6,7 +6,7 @@ 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 risk significant economic losses, service interruptions,
+Control system failures risk economic losses, service interruptions,
 or radiological release.
 % Known information
 Nuclear plant operations rely on extensively trained human operators
@@ -16,7 +16,7 @@ manage reactor control. When operators switch between different control modes, p
 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 that far
-exceed those of conventional plants, threatening their economic viability.
+exceed those of conventional plants, threatening economic viability.
 The nuclear industry needs autonomous control systems that manage complex
 operational sequences safely without constant human supervision while providing
 assurance equal to or exceeding human-operated systems.
@@ -27,7 +27,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 handle continuous dynamics during transitions between modes.
+generate provably correct switching logic from written requirements but cannot handle continuous dynamics during transitions.
 Control theory verifies continuous behavior but cannot prove the correctness of discrete switching decisions. This gap prevents end-to-end correctness guarantees.
 % Hypothesis
 Our approach closes this gap by synthesizing discrete mode transitions directly
@@ -85,7 +85,7 @@ If this research is successful, we will be able to do the following:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{What is new:} We unify discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
+\textbf{What is new?} We unify discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
 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

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

@@ -37,7 +37,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Despite rigorous development, procedures lack formal verification. This subsection examines the second pillar of current practice: the human operators who execute these procedures. Procedures define what to do; human operators determine when and how to apply them. This approach introduces fundamental reliability limitations.
+Procedures lack formal verification despite rigorous development. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations. Procedures define what to do; human operators determine when and how to apply them. Even perfectly written procedures cannot eliminate human error.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -80,7 +80,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
+Procedures lack formal verification. Human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
 
 \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control}
 

3-research-approach/v3.tex

@@ -15,9 +15,9 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation; discrete switching logic undergoes simulated control room testing and human factors research. 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, formalizing reactor operations using hybrid automata.
+Previous approaches to autonomous control verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation; discrete switching logic undergoes simulated control room testing and human factors research. 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 by verifying discrete switching logic and continuous mode behavior separately, then composing them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while 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—cannot handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations: 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
 a mathematical description of the system. This work draws on
@@ -52,7 +52,7 @@ where:
 
 Creating a HAHACS requires constructing such a tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty. First, we use discrete synthesis to define entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, we classify continuous modes by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, we leverage existing procedural structure to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
+\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty. First, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, continuous modes are classified by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, existing procedural structure is leveraged to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than impose artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, keeping computational complexity bounded by verifying each mode against local contracts. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We demonstrate feasibility on production control systems with realistic reactor models, not merely prove it in principle.
 
@@ -101,8 +101,8 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac
     
   \end{tikzpicture}
   \caption{Simplified hybrid automaton for reactor startup. Each discrete state 
-    $q_i$ has associated continuous dynamics $f_i$. Guard conditions on 
-    transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous 
+    $q_i$ has associated continuous dynamics $f_i$. Guard conditions 
+    (e.g., $T_{avg} > T_{min}$) are predicates over continuous 
     state. Invariant violations ($\neg Inv_i$) trigger transitions to the 
     SCRAM state. The operational level manages discrete transitions; the 
     tactical level executes continuous control within each mode.}
@@ -325,14 +325,16 @@ discrete state are the guard conditions $\mathcal{G}$ that define the
 boundaries for each continuous controller's allowed state-space region. These
 continuous controllers all share a common state space, but each individual
 continuous control mode operates within its own partition—defined by the
-discrete state $q_i$ and the associated guards. This partitioning of the
+discrete state $q_i$ and the associated guards. 
+
+This partitioning of the
 continuous state space among several discrete vector fields has traditionally
 posed a difficult problem for validation and verification. The discontinuity of
 the vector fields at discrete state interfaces makes reachability analysis
 computationally expensive, and analytic solutions often become intractable
 \cite{MANYUS THESIS}.
 
-We circumvent these issues by designing our hybrid system from the bottom up
+These issues are circumvented by designing the hybrid system from the bottom up
 with verification in mind. The discrete transitions define each continuous
 control mode's input and output sets clearly \textit{a priori}.
 
@@ -553,11 +555,11 @@ outcomes can align best with customer needs.
 
 This section answered two Heilmeier questions:
 
-\textbf{What is new?} We integrate reactive synthesis, reachability analysis, and barrier certificates into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis.
+\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates are integrated into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis.
 
-\textbf{Why will it succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than impose artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation.
+\textbf{Why will it succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the methodology formalizes existing structure rather than imposing artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation.
 
-Having established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—Section 4 addresses the next Heilmeier question: how do we measure success? Not through theoretical contributions alone, but through Technology Readiness Level advancement that demonstrates both correctness and practical implementability.
+Having established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—Section 4 addresses the next Heilmeier question: how do we measure success? Technology Readiness Level advancement demonstrates both correctness and practical implementability.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -82,7 +82,7 @@ development status indicates progress toward TRL 3. Synthesis results and
 verification coverage indicate progress toward TRL 4. Simulation performance
 metrics and hardware integration milestones indicate progress toward TRL 5. The
 research plan will be revised only when new data invalidates fundamental
-assumptions. This research succeeds if it achieves TRL 5 by demonstrating a
+assumptions. This research succeeds by achieving TRL 5: demonstrating a
 complete autonomous hybrid controller with formal correctness guarantees
 operating on industrial control hardware through hardware-in-the-loop testing in
 a relevant laboratory environment. This establishes both theoretical validity

5-risks-and-contingencies/v1.tex

@@ -13,14 +13,13 @@ publishable results while clearly identifying remaining barriers to deployment.
 
 The first major assumption is that formalized startup procedures will yield
 automata small enough for efficient synthesis and verification. Reactive
-synthesis scales exponentially with specification complexity. This scaling creates the risk that
-temporal logic specifications derived from complete startup procedures may
+synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may
 produce automata with thousands of states. Such large automata would require
 synthesis times exceeding days or weeks, preventing demonstration of the
 complete methodology within project timelines. Reachability analysis for
 continuous modes with high-dimensional state spaces may similarly prove
 computationally intractable. Either barrier would constitute a fundamental
-obstacle to achieving our research objectives.
+obstacle to achieving research objectives.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets

6-broader-impacts/v1.tex

@@ -7,7 +7,7 @@ economic challenge. Recent interest in powering artificial intelligence
 infrastructure has renewed focus on small modular reactors (SMRs), particularly
 for hyperscale datacenters requiring hundreds of megawatts of continuous power.
 Deploying SMRs at datacenter sites minimizes transmission losses and
-eliminates emissions from hydrocarbon-based alternatives. However, nuclear power
+eliminates emissions. However, nuclear power
 economics at this scale demand careful attention to operating costs.
 
 The U.S. Energy Information Administration's Annual Energy Outlook
@@ -28,11 +28,11 @@ to \$21--28 billion annually for projected datacenter demand.
 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. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output, making the per-megawatt cost prohibitive. These staffing requirements drive the economic challenge
+reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output, making per-megawatt costs prohibitive. These staffing requirements drive the economic challenge
 that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal
 specifications automates routine operational sequences that currently require
-constant human oversight. A fundamental shift from direct operator
-control to supervisory monitoring becomes possible, where operators oversee multiple autonomous
+constant human oversight. This enables a fundamental shift from direct operator
+control to supervisory monitoring, where operators oversee multiple autonomous
 reactors rather than manually controlling individual units.
 
 The correct-by-construction methodology is critical for this transition.

8-schedule/v1.tex

@@ -4,7 +4,7 @@
 trimesters (24 months) of full-time effort following the proposal defense in
 Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC
 Fellowship provide all computational and experimental resources. The work progresses
-sequentially through three main research thrusts before culminating in
+sequentially through three main research thrusts, culminating in
 integrated demonstration and validation.
 
 The first semester (Spring 2026) focuses on Thrust 1, translating startup