Editorial pass: tactical, operational, and strategic improvements

TACTICAL (sentence-level):
- Applied Gopen's Sense of Structure principles
- Improved topic-stress positioning by breaking long sentences
- Strengthened verb choice (active voice where appropriate)
- Enhanced clarity through shorter, more direct sentences

OPERATIONAL (paragraph/section):
- Improved transitions between subsections
- Enhanced flow between related ideas
- Strengthened coherence within sections

STRATEGIC (document-level):
- Verified Heilmeier catechism alignment throughout
- Strengthened section summaries and transitions
- Ensured each section clearly answers its assigned questions
- Improved logical progression between sections

Files edited:
- 1-goals-and-outcomes/research_statement_v1.tex
- 1-goals-and-outcomes/v1.tex
- 2-state-of-the-art/v2.tex
- 3-research-approach/v3.tex
- 4-metrics-of-success/v1.tex
- 5-risks-and-contingencies/v1.tex
- 6-broader-impacts/v1.tex

Focus: clarity, impact, and logical flow without changing technical content.

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,21 +1,21 @@
 % GOAL PARAGRAPH
-I develop autonomous control systems that guarantee safe and correct behavior mathematically.
+I develop autonomous control systems that guarantee safe and correct behavior through mathematical proof.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors today depend on extensively trained human operators who follow detailed written procedures and switch between control objectives as plant conditions change.
+Nuclear reactors today depend on extensively trained human operators. These operators 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 safety assurance equals or exceeds that of human operators.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. This cost disparity threatens 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 that are correct by construction, unifying formal methods from computer science with control theory. 
+I produce hybrid control systems that are correct by construction. This work unifies 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.
+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 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 imposed by each discrete mode. 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. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata 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.
 
-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.
+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.
 % Pay-off
-This approach manages complex nuclear power operations autonomously while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
+This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It directly addresses the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS
 This research, if successful, produces three concrete outcomes:
@@ -27,7 +27,7 @@ This research, if successful, produces three concrete outcomes:
     Reactive synthesis tools then generate discrete control logic from these specifications.
     % Outcome
     Control engineers generate mode-switching controllers directly from regulatory
-    procedures. Minimal formal methods expertise required. This reduces barriers to
+    procedures with minimal formal methods expertise. This reduces barriers to
     high-assurance control systems.
 
     % OUTCOME 2 Title

1-goals-and-outcomes/v1.tex

@@ -1,21 +1,21 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops autonomous hybrid control systems that guarantee safe and correct behavior mathematically.
+This research develops autonomous hybrid control systems that guarantee safe and correct behavior through mathematical proof.
 
 % 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 who follow detailed written procedures and strict regulatory requirements. Operators switch between control modes based on plant conditions and procedural guidance.
+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.
 % 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.
+This reliance on human operators prevents autonomous control. It creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants. This cost disparity threatens 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 that are correct by construction, unifying formal methods with control theory.
+This work produces hybrid control systems that are correct by construction. It unifies 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.
+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 approaches working together.
 % 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. 
+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. The result: autonomous controllers provably free from design defects. 
 
 The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation requirements.
 

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

@@ -2,17 +2,17 @@
 
 \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
 
-No current approach provides autonomous control with end-to-end correctness guarantees. This section examines why: human-centered operation cannot eliminate reliability limits, and formal methods verify discrete or continuous behavior but never both. 
+No current approach provides autonomous control with end-to-end correctness guarantees. This section examines why. 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. 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.
 
 Section 3 addresses the verification gap these limits establish.
 
 \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 then examines operators—their reliability limits and contribution to accidents.
+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.
 
-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}. 
+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. 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.
 
@@ -24,7 +24,7 @@ invariants. Paper-based procedures cannot ensure correct application. Even
 computer-based procedure systems lack the formal guarantees automated reasoning
 could provide.
 
-Nuclear plants operate with multiple control modes. Automatic control maintains target parameters through continuous reactivity adjustment. Manual control allows operators to directly manipulate the reactor. Various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature, compensating for power demand changes through reactivity feedback loops alone. Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required.
+Beyond procedure verification, nuclear plants operate with multiple control modes. Automatic control maintains target parameters through continuous reactivity adjustment. Manual control allows operators to directly manipulate the reactor. Various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature, compensating for power demand changes through reactivity feedback loops alone. Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required.
 
 This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems already 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 retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure—discrete human decisions combined with continuous automated control—forms the basis for autonomous hybrid control systems.
 
@@ -32,7 +32,7 @@ This division between automated and human-controlled functions reveals the funda
 
 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.
 
-Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. While procedures define what to do, operators determine when and how to act. This human 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 human 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
@@ -118,7 +118,9 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. Other researchers have attacked the problem from the opposite direction by extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL), which addresses continuous dynamics but encounters different limitations. dL introduces two additional operators
+HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. 
+
+Other researchers have attacked the problem from the opposite direction. They extended temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). dL addresses continuous dynamics but encounters different limitations. dL introduces two additional operators
 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
@@ -153,16 +155,10 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 This section answered two Heilmeier questions: What has been done? What are the limits of current practice?
 
-\textbf{What has been done?} Three approaches currently exist:
+\textbf{What has been done?} Three approaches currently exist. Human operators provide operational flexibility but introduce persistent reliability limitations. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. Each approach has fundamental limitations. None addresses both discrete and continuous verification compositionally.
-\begin{itemize}
-\item Human operators provide operational flexibility but introduce persistent reliability limitations.
-\item HARDENS verified discrete logic but omitted continuous dynamics.
-\item Differential dynamic logic expresses hybrid properties but requires post-design expert analysis.
-\end{itemize}
-Each approach has fundamental limitations. None addresses both discrete and continuous verification compositionally.
 
-\textbf{What are the limits of current practice?} The verification gap emerges clearly: 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{What are the limits of current practice?} The verification gap emerges clearly. 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.
 
 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 to enable compositional hybrid verification.
 
-Section 3 closes this verification gap by establishing what is new and why the approach will succeed.
+Section 3 closes this verification gap. It establishes what is new and why the approach will succeed.

3-research-approach/v3.tex

@@ -4,7 +4,7 @@
 
 This section presents the complete technical approach for synthesizing provably correct hybrid controllers from operating procedures. 
 
-\textbf{What is new:} Compositional verification that bridges discrete synthesis with continuous control. Three innovations enable this integration: contract-based decomposition, mode classification, and procedure-driven structure. 
+\textbf{What is new:} Compositional verification bridges discrete synthesis with continuous control. Three innovations enable this integration: contract-based decomposition, mode classification, and procedure-driven structure. 
 
 \textbf{Why it will succeed:} The approach leverages existing procedural structure. It bounds computational complexity through mode-level verification. It validates against real industrial hardware through the Emerson collaboration.
 
@@ -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 and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees, and both consume enormous resources.
+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 bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
+This approach bridges that gap. It composes formal methods from computer science with control-theoretic verification. Reactor operations are formalized 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

@@ -2,11 +2,11 @@
 
 \textbf{Heilmeier Question: How do we measure success?}
 
-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. 
+Section 3 established the technical approach. It 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. 
 
-Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
+Success is measured by Technology Readiness Level advancement. The work advances 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.
+This work begins at TRL 2--3 and targets TRL 5. At TRL 5, 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 for work that bridges the gap between academic proof-of-concept and practical deployment. 
 

5-risks-and-contingencies/v1.tex

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Question: What could prevent success?}
 
-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.
+Section 4 defined success as reaching TRL 5. The path requires component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome.
 
 Every research plan rests on assumptions that might prove false. This section identifies three primary risks that could prevent reaching TRL 5. First: computational tractability of synthesis and verification. Second: complexity of the discrete-continuous interface. Third: completeness of procedure formalization. 
 

6-broader-impacts/v1.tex

@@ -2,11 +2,11 @@
 
 \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-Sections 2--5 established the complete technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how to measure success (Section 4), and what could prevent success (Section 5).
+Sections 2--5 established the complete technical research plan. Section 2 answered what has been done. Section 3 answered what is new and why it will succeed. Section 4 answered how to measure success. Section 5 answered what could prevent success.
 
-This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
+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.
 
-Three stakeholder groups converge on one 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.
+Three stakeholder groups converge on one 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.
 
 This research directly addresses a \$21--28 billion annual cost barrier by enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.