Editorial pass: tactical (sentence-level), operational (paragraph/section), and strategic (Heilmeier alignment) improvements

- Strengthened topic-stress positioning throughout
- Improved verb choice and active constructions
- Enhanced transitions between paragraphs and sections
- Clarified Heilmeier question alignments
- Reduced redundancy and tightened prose

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,18 +2,18 @@
 My research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors today depend on extensively trained human operators. These operators follow detailed written procedures and switch between control objectives as plant conditions change.
+Extensively trained human operators control nuclear reactors today. They follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
+Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if safety assurance equals or exceeds that of human operators.
 
 % APPROACH PARAGRAPH Solution
-My approach unifies formal methods from computer science with control theory. This produces hybrid control systems that are correct by construction.
+This approach unifies formal methods from computer science with control theory to produce hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
 % Hypothesis and Technical Approach
-Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications. These specifications structure requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory techniques—satisfy each discrete mode's requirements.
+Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications that structure requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory techniques—satisfy each discrete mode's requirements.
 
-Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe. This enables local verification without global trajectory analysis. I demonstrate this methodology on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
+Continuous modes classify by control objective into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe, enabling local verification without global trajectory analysis. This methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
 % Pay-off
 This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It directly addresses the economic constraints threatening small modular reactor viability.
 
@@ -23,11 +23,11 @@ This research, if successful, produces three concrete outcomes:
   % OUTCOME 1 Title
   \item \textit{Synthesize written procedures into verified control logic.} 
     % Strategy
-    A methodology converts written operating procedures into formal specifications.
+    The methodology converts written operating procedures into formal specifications.
     Reactive synthesis tools then generate discrete control logic from these specifications.
     % Outcome
-    Control engineers generate mode-switching controllers directly from regulatory
+    Control engineers can generate mode-switching controllers directly from regulatory
-    procedures with minimal formal methods expertise. This reduces barriers to
+    procedures with minimal formal methods expertise, reducing barriers to
     high-assurance control systems.
 
     % OUTCOME 2 Title

1-goals-and-outcomes/v1.tex

@@ -6,14 +6,14 @@ This research develops autonomous hybrid control systems with mathematical guara
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release.
 % Known information
-Nuclear plants today depend on extensively trained human operators. These operators follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
+Extensively trained human operators control nuclear plants today. They follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
 % Gap
 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 economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This work unifies formal methods with control theory. This produces hybrid control systems that are correct by construction.
+This work unifies formal methods with control theory to produce hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
 % Hypothesis
 Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics—producing autonomous controllers provably free from design defects. 
 

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

@@ -4,17 +4,17 @@
 
 No current approach provides autonomous control with end-to-end correctness guarantees. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior but never both. 
 
-Three subsections structure this analysis. First: reactor operators and their operating procedures. Second: fundamental limitations of human-based operation. Third: formal methods approaches that verify discrete logic or continuous dynamics but not both together.
+Three subsections structure this analysis: reactor operators and their operating procedures; fundamental limitations of human-based operation; and formal methods approaches that verify discrete logic or continuous dynamics but not both together.
 
-Section 3 addresses the verification gap these limits establish.
+These limits establish a verification gap that Section 3 addresses.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current practice rests on two critical components: procedures and operators. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection examines operators—their reliability limits and contribution to accidents.
+Current practice rests on two critical components: procedures and operators. Procedures define what must be done; operators execute those procedures. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection examines operators—their reliability limits and contribution to accidents.
 
 Nuclear plant procedures form a strict 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. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. All procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 
 
-Procedure development relies on expert judgment and simulator validation—not formal verification. Regulations require rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} mandates technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proofs confirm that procedures cover all possible plant states. No proofs verify that required actions complete within available timeframes. No proofs guarantee that transitions between procedure sets maintain safety invariants.
+Expert judgment and simulator validation—not formal verification—form the basis for procedure development. Regulations require rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} mandates technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. Procedures cover all possible plant states without mathematical proof. Required actions complete within available timeframes without proof. Transitions between procedure sets maintain safety invariants without proof.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} No proof exists that procedures cover all
@@ -30,9 +30,9 @@ This division between automated and human-controlled functions reveals the funda
 
 \subsection{Human Factors in Nuclear Accidents}
 
-The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
+Procedures lack formal verification despite rigorous development—this represents only half the reliability challenge. Even perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
 
-Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do; operators determine when and how to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
+Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do. Operators determine when and how to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -159,6 +159,6 @@ This section answered two Heilmeier questions: What has been done? What are the
 
 \textbf{What are the limits of current practice?} A clear verification gap emerges. No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics but never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-\textbf{Why now?} Two forces create urgency. Economic necessity demands solutions: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity enables solutions: formal methods tools have matured sufficiently to enable compositional hybrid verification.
+\textbf{Why now?} Two forces create urgency. Economic necessity demands solutions: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity enables solutions: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
 
-The gap is clear. The timing is right. Section 3 closes this verification gap by establishing what is new and why the approach will succeed.
+The verification gap is clear. The timing is right. Section 3 closes this gap by establishing what is new and why the approach will succeed.

3-research-approach/v3.tex

@@ -23,9 +23,9 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified discrete switching logic or continuous control behavior but never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources. This approach changes that.
+Previous approaches verified discrete switching logic or continuous control behavior but never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources.
 
-This approach bridges that gap. It composes formal methods from computer science with control-theoretic verification. It formalizes reactor operations as hybrid automata.
+This approach bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
 
 Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field. These discontinuities cannot be handled directly by traditional verification techniques.
 
@@ -70,11 +70,11 @@ Three innovations enable compositional verification:
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed.
 
-\textbf{First, existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This approach formalizes that existing structure without imposing artificial abstractions. Domain experts can adopt it without formal methods training.
+\textbf{First, existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions, enabling domain experts to adopt it without formal methods training.
 
-\textbf{Second, bounded complexity:} Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. The decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
+\textbf{Second, bounded complexity:} Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. This decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
 
-\textbf{Third, industrial validation:} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. Solutions address real deployment constraints, not just theoretical correctness.
+\textbf{Third, industrial validation:} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints rather than just theoretical correctness.
 
 These factors combine to demonstrate feasibility on production control systems with realistic reactor models—not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence.
 
@@ -142,9 +142,9 @@ These factors combine to demonstrate feasibility on production control systems w
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. A critical question remains: where do these formal descriptions originate?
+The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. This formalism provides the mathematical structure for hybrid control. A critical question remains: where do these formal descriptions originate?
 
-Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge—leveraging decades of domain expertise already encoded in operating procedures—rather than imposing artificial abstractions.
+Nuclear operations already possess a natural hybrid structure that maps directly to this formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge—leveraging decades of domain expertise already encoded in operating procedures—rather than imposing artificial abstractions.
 
 Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years, managing labor needs and supply chains to optimize scheduled maintenance and downtime.
 
@@ -262,14 +262,14 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 The previous subsection demonstrated how operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do. A critical gap remains: how do we implement those requirements?
 
-Reactive synthesis bridges this gap. It automatically constructs controllers guaranteed to satisfy temporal logic specifications.
+Reactive synthesis bridges this gap by automatically constructing controllers guaranteed to satisfy temporal logic specifications.
 
-Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. Temporal logic specifications enable reactive synthesis to construct the discrete control system automatically. The current discrete state and status of guard conditions form the input; the next discrete state forms the output.
+Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. The current discrete state and status of guard conditions form the input; the next discrete state forms the output.
 
 Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ specifying desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller exists. Unrealizable specifications indicate conflicting or impossible requirements in
 the original procedures—this realizability check catches errors before implementation. 
 
-Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The automaton is correct by construction. This eliminates human error at the implementation stage entirely. Human designers focus effort where it belongs—on specifying system behavior, not implementing switching logic.
+Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation and is correct by construction. This eliminates human error at the implementation stage entirely, allowing human designers to focus effort where it belongs—on specifying system behavior rather than implementing switching logic.
 
 This shift carries two critical implications. First, complete traceability: the controller changes between modes for reasons that trace back through specifications to requirements. This establishes clear liability and justification for system behavior. Second, deterministic guarantees replace probabilistic human judgment. Human operators cannot eliminate error from discrete control decisions. Humans are intrinsically fallible. Temporal logics define system behavior. Deterministic algorithms synthesize the controller. Strategic decisions follow operating procedures exactly—no exceptions, no deviations, no human factors.
 
@@ -392,7 +392,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions, answering the question: "can we reach the target?"
+Transitory modes drive the system toward exit conditions, answering the question: "can we reach the target?" Reachability analysis provides the verification tool for this question.
 
 Stabilizing modes address a fundamentally different question: "will we stay within bounds?" These modes maintain the system within a desired operating region indefinitely—examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
 
@@ -443,7 +443,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-The first two mode types handle nominal operations: transitory modes move the plant between conditions, while stabilizing modes maintain the plant within regions. Both assume the plant dynamics match the design model.
+The first two mode types handle nominal operations: transitory modes move the plant between conditions using reachability analysis, while stabilizing modes maintain the plant within regions using barrier certificates. Both assume the plant dynamics match the design model.
 
 Expulsory modes address a fundamentally different scenario—situations where the plant deviates from expected behavior. This deviation may result from component failures, sensor degradation, or unanticipated disturbances. Here, robustness matters more than optimality.
 
@@ -526,7 +526,7 @@ outcomes can align best with customer needs.
 
 This section answered two critical Heilmeier questions: What is new? Why will it succeed?
 
-\textbf{What is new?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis through three innovations: 
+\textbf{What is new?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations enable this integration: 
 
 \textit{Contract-based decomposition} inverts traditional global analysis—discrete synthesis defines verification contracts that bound continuous verification. 
 

4-metrics-of-success/v1.tex

@@ -4,7 +4,7 @@
 
 Section 3 established the technical approach. It answered what is new: compositional verification bridging discrete synthesis with continuous control. It answered why it will succeed: existing procedural structure, bounded complexity, and industrial validation. This section addresses the next Heilmeier question: how to measure success. 
 
-Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5), where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
+Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5) measures success. At TRL 5, system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
 
 Technology Readiness Levels provide the ideal success metric for work bridging academic proof-of-concept and practical deployment. 
 

5-risks-and-contingencies/v1.tex

@@ -4,9 +4,9 @@
 
 Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome. What if they cannot?
 
-Every research plan rests on assumptions that might prove false. This section identifies three primary risks that could prevent reaching TRL 5. These are: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization. 
+Every research plan rests on assumptions that might prove false. Three primary risks could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization. 
 
-Each risk carries associated early warning indicators and contingency plans that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results and clearly identifies remaining barriers to deployment even when full success proves elusive.
+Each risk carries associated early warning indicators and contingency plans that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results and clearly identifies remaining barriers to deployment, even when full success proves elusive.
 
 \subsection{Computational Tractability of Synthesis}
 
@@ -131,14 +131,14 @@ quirks.
 
 This section answered the Heilmeier question: What could prevent success?
 
-\textbf{Answer:} Three primary risks threaten TRL 5 achievement. First: computational tractability of synthesis and verification. Second: complexity of the discrete-continuous interface. Third: completeness of procedure formalization.
+\textbf{Answer:} Three primary risks threaten TRL 5 achievement: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization.
 
 Each risk has identifiable early warning indicators enabling detection before failure becomes inevitable. Each has viable mitigation strategies preserving research value even when core assumptions fail.
 
 The staged project structure ensures partial success yields publishable results identifying remaining deployment barriers. This design maintains contribution regardless of which technical obstacles prove insurmountable. Even "failure" advances the field by documenting precisely which barriers remain.
 
-The technical research plan is complete: what will be done and why it will succeed (Section 3), how to measure success (Section 4), what might prevent success (this section).
+The technical research plan is complete. Section 3 established what will be done and why it will succeed. Section 4 defined how to measure success. This section identified what might prevent success and how to respond.
 
 One critical question remains: Who cares? Why now? What difference will it make?
 
-Section 6 connects this technical methodology to urgent economic challenges.
+Section 6 connects this technical methodology to urgent economic and societal challenges.

6-broader-impacts/v1.tex

@@ -6,7 +6,7 @@ Sections 2--5 established the complete technical research plan. Section 2 answer
 
 The technical plan is complete. This section addresses the remaining Heilmeier questions. It connects technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
 
-\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically viable. All three need this research to succeed.
+\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically viable against fossil alternatives. All three need this research to succeed.
 
 \textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier, enabling economically viable small modular reactors for datacenter power while establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.