Editorial pass 1: Tactical improvements (sentence-level clarity, topic-stress, verb choice)

1-goals-and-outcomes/research_statement_v1.tex

@@ -7,13 +7,13 @@ Nuclear reactors today depend on extensively trained human operators who follow
 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 safety assurance equals or exceeds that of human operators.
 
 % APPROACH PARAGRAPH Solution
-I produce hybrid control systems correct by construction by unifying formal methods from computer science with control theory. 
+I produce hybrid control systems that are correct by construction, unifying formal methods from computer science with control theory. 
 % 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. Achieving end-to-end correctness requires both approaches working together.
 % 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, structuring 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 satisfy the requirements each discrete mode imposes. Engineers design these continuous controllers using standard control theory techniques.
+Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications, structuring 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 satisfy the requirements imposed by each discrete mode. Engineers design these continuous controllers using standard control theory techniques.
 
-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 safe mode transitions, enabling local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
+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 safe mode transitions, enabling local verification without global trajectory analysis. I demonstrate this methodology 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, directly addressing the economic constraints threatening small modular reactor viability.
 

1-goals-and-outcomes/v1.tex

@@ -11,7 +11,7 @@ Nuclear plants today depend on extensively trained human operators who follow de
 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 produces hybrid control systems correct by construction by unifying formal methods with control theory.
+This work produces hybrid control systems that are correct by construction, unifying formal methods with control theory.
 % 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. Achieving end-to-end correctness requires both approaches working together.
 % Hypothesis
@@ -27,7 +27,7 @@ If successful, this approach produces three concrete outcomes:
   % OUTCOME 1 Title
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
-    A methodology converts existing written operating procedures into formal
+    A methodology converts written operating procedures into formal
     specifications. Reactive synthesis tools then automatically generate
     discrete control logic from these specifications. Structured intermediate
     representations bridge natural language procedures and mathematical logic.
@@ -39,12 +39,12 @@ If successful, this approach produces three concrete outcomes:
     % OUTCOME 2 Title
   \item \textbf{Verify continuous control behavior across mode transitions.}
     % Strategy
-    Methods for analyzing continuous control modes verify they satisfy
+    Methods for analyzing continuous control modes verify that they satisfy
     discrete transition requirements. Classical control theory handles linear
-    systems. Reachability analysis handles nonlinear dynamics. Both verify that
+    systems, while reachability analysis handles nonlinear dynamics. Both verify that
     each continuous mode reaches its intended transitions safely.
     % Outcome
-    Engineers design continuous controllers using standard practices. Formal correctness guarantees remain intact. Mode transitions occur safely and at the correct times—provably.
+    Engineers design continuous controllers using standard practices while maintaining formal correctness guarantees. Mode transitions occur safely and at the correct times—provably.
 
     % OUTCOME 3  Title
   \item \textbf{Demonstrate autonomous reactor startup control with safety
@@ -64,7 +64,7 @@ If successful, this approach produces three concrete outcomes:
 % 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 makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. Section 2 examines why prior work fails at this integration and identifies the limits of current practice. Section 3 details what is new in this approach and why it will succeed.
+\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic, while control theory verifies continuous dynamics. Section 2 examines why prior work fails at this integration and identifies the limits of current practice. Section 3 details what is new in this approach and why it will succeed.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from
@@ -72,7 +72,7 @@ existing procedures with mathematical proofs of correct behavior, making high-as
 autonomous control 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
+nuclear power. Small modular reactors, in particular, offer a promising solution to growing
 energy demands. Their success depends on reducing per-megawatt operating
 costs through increased autonomy. My research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the

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

@@ -17,8 +17,7 @@ Nuclear plant procedures form a strict hierarchy. Normal operating procedures go
 Procedure development relies on expert judgment and simulator validation—not formal verification. 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through 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, 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
+and completeness.} No proof exists that procedures cover all
-simulator validation—not mathematical proof. No 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. Paper-based procedures cannot ensure correct application. Even
@@ -123,7 +122,7 @@ HARDENS verified discrete control logic without continuous dynamics—leaving ha
 into temporal logic: the box operator and the diamond operator. The box operator
 \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
 \(\alpha\) always remains within that region. In this way, it is a safety
-ivariant being enforced for the system. The second operator, the diamond
+invariant being enforced for the system. The second operator, the diamond
 operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
 one trajectory of \(\alpha\) that enters that region. This is a declaration of a
 liveness property. 
@@ -139,7 +138,7 @@ non-terminating solutions prevent creating system proofs using dL.
 %gyroscopes overloding and needing to dump speed all the time
 Approaches have been made to alleviate
 these issues for nuclear power contexts using contract and decomposition based
-methods, but are far from a complete methodology to design systems with.
+methods, but fall far short of a complete design methodology.
 %source: Manyu's thesis. 
 Instead, these approaches have been used on systems that have been designed a
 priori, and require expert knowledge to create the system proofs. 

3-research-approach/v3.tex

@@ -25,7 +25,7 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 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, and both consume enormous resources.
 
-This approach bridges that gap by composing formal methods from computer science with control-theoretic verification and formalizing 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, creating discontinuities through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
 

4-metrics-of-success/v1.tex

@@ -4,11 +4,11 @@
 
 Section 3 established the technical approach and answered what is new: compositional verification bridging discrete synthesis with continuous control. It answered why the approach will succeed: existing procedural structure, bounded complexity, and industrial validation. This section addresses the next Heilmeier question: how to measure success. 
 
-Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5) measures success.
+Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
 
 This work begins at TRL 2--3 and targets TRL 5, where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric: 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. They explicitly measure the gap between academic proof-of-concept and practical deployment. This is precisely what my work bridges. 
+Technology Readiness Levels provide the ideal success metric for work that bridges the gap between academic proof-of-concept and practical deployment. 
 
 Academic metrics—papers published or theorems proved—fail to capture practical feasibility. Empirical metrics—simulation accuracy or computational speed—fail to demonstrate theoretical rigor. TRLs measure both.
 

5-risks-and-contingencies/v1.tex

@@ -28,7 +28,7 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 Computational tractability addresses a practical constraint: whether synthesis can complete within reasonable time bounds. The second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
 
-This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction. This would make synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
+This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates, while continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction. This would make synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
 
 The risk extends beyond static interface definition to dynamic behavior across transitions. Barrier certificates may fail to exist for proposed transitions. Continuous modes may be unable to guarantee convergence to discrete transition boundaries.
 

8-schedule/v1.tex

@@ -76,22 +76,16 @@ Figure \ref{fig:gantt} shows the complete project schedule including research th
 
 \subsection{Milestones and Deliverables}
 
-Six major milestones mark critical validation points throughout the research. M1
+Six major milestones mark critical validation points throughout the research:
-(Month 4) confirms that startup procedures have been successfully translated to
+
-temporal logic using FRET with realizability analysis demonstrating consistent
+\textbf{M1 (Month 4):} Confirms that startup procedures have been successfully translated to temporal logic using FRET with realizability analysis demonstrating consistent and complete specifications.
-and complete specifications. M2 (Month 8) validates computational tractability
+
-by demonstrating that Strix can synthesize a complete discrete automaton from
+\textbf{M2 (Month 8):} Validates computational tractability by demonstrating that Strix can synthesize a complete discrete automaton from the formalized specifications. Delivers a conference paper submission to NPIC\&HMIT documenting the procedure-to-specification translation methodology.
-the formalized specifications. This milestone delivers a conference paper
+
-submission to NPIC\&HMIT documenting the procedure-to-specification translation
+\textbf{M3 (Month 12):} Achieves TRL 3 by proving that continuous controllers can be designed and verified to satisfy discrete transition requirements. Delivers an internal technical report demonstrating component-level verification.
-methodology. M3 (Month 12) achieves TRL 3 by proving that continuous controllers
+
-can be designed and verified to satisfy discrete transition requirements. This
+\textbf{M4 (Month 16):} Achieves TRL 4 through integrated simulation demonstrating that component-level correctness composes to system-level correctness. Delivers a journal paper submission to IEEE Transactions on Automatic Control presenting the complete hybrid synthesis methodology.
-milestone delivers an internal technical report demonstrating component-level
+
-verification. M4 (Month 16) achieves TRL 4 through integrated simulation
+\textbf{M5 (Month 20):} Achieves TRL 5 by demonstrating practical implementability on industrial hardware. Delivers a conference paper submission to NPIC\&HMIT or CDC documenting hardware implementation and experimental validation.
-demonstrating that component-level correctness composes to system-level
+
-correctness. This milestone delivers a journal paper submission to IEEE
+\textbf{M6 (Month 24):} Completes the dissertation documenting the entire methodology, experimental results, and research contributions. 
-Transactions on Automatic Control presenting the complete hybrid synthesis
-methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical
-implementability on industrial hardware. This milestone delivers a conference
-paper submission to NPIC\&HMIT or CDC documenting hardware implementation and
-experimental validation. M6 (Month 24) completes the dissertation documenting
-the entire methodology, experimental results, and research contributions.