Multi-level editorial pass: tactical, operational, and strategic improvements

Applied Gopen's Sense of Structure principles throughout:
- Combined short choppy sentences for better flow
- Strengthened topic-stress positioning
- Tightened verb choices and reduced passive voice
- Improved paragraph transitions and coherence
- Enhanced document-level Heilmeier alignment
- Removed redundant content (duplicate paragraph in research approach)

All changes preserve technical accuracy while improving clarity and impact.

1-goals-and-outcomes/research_statement_v1.tex

@@ -4,14 +4,14 @@ I develop autonomous control systems with mathematical guarantees of safe and co
 % 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.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. This threatens economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only if they provide safety assurance equal to or exceeding human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only if they provide safety assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-I produce hybrid control systems correct by construction. This unifies formal methods from computer science with control theory. 
+I produce hybrid control systems 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 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.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both approaches must work together to achieve 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. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking then 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 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, structuring requirements by scope, condition, component, timing, and response. Realizability checking then 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. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
 % Pay-off

1-goals-and-outcomes/v1.tex

@@ -8,14 +8,14 @@ Nuclear power plants require the highest levels of control system reliability. C
 % Known information
 Nuclear plants today depend on extensively trained human operators who follow detailed written procedures and strict regulatory requirements. These operators switch between control modes based on plant conditions and procedural guidance.
 % Gap
-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 threatens economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only if they provide safety assurance equal to or exceeding human operators.
+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 systems could manage complex operational sequences without constant human supervision—but only if they provide safety assurance equal to or exceeding human operators.
 
 % APPROACH PARAGRAPH Solution
-I produce hybrid control systems correct by construction. This unifies formal methods with control theory.
+I produce hybrid control systems 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. 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. Both approaches must work together to achieve end-to-end correctness.
 % Hypothesis
-Two steps close this gap. First, discrete mode transitions synthesize directly from written operating procedures. Second, continuous behavior between transitions verifies against discrete requirements. This formalizes operating procedures into logical specifications that constrain continuous dynamics. The result: autonomous controllers provably free from design defects. 
+Two steps close this gap. First, discrete mode transitions synthesize directly from written operating procedures. Second, continuous behavior between transitions verifies against discrete requirements. This formalizes operating procedures into logical specifications that constrain continuous dynamics, producing 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.
 
@@ -68,17 +68,15 @@ These three outcomes—procedure translation, continuous verification, and hardw
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from
-existing procedures with mathematical proofs of correct behavior. High-assurance
+existing procedures with mathematical proofs of correct behavior, making high-assurance
-autonomous control becomes practical for safety-critical applications.
+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
 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
-nuclear industry requires.
+nuclear industry requires. 
-
-These three outcomes establish a complete methodology from regulatory documents to deployed systems. 
 
 This proposal follows the Heilmeier Catechism. Each section explicitly answers its assigned questions:
 \begin{itemize}
@@ -89,4 +87,4 @@ This proposal follows the Heilmeier Catechism. Each section explicitly answers i
   \item \textbf{Section 6 (Broader Impacts):} Who cares? Why now? What difference will it make?
   \item \textbf{Section 8 (Schedule):} How long will it take?
 \end{itemize}
-Each section begins by stating its Heilmeier questions. Each section ends by summarizing its answers. This structure ensures both local clarity and global coherence.
+Each section begins by stating its Heilmeier questions and ends by summarizing its answers, ensuring both local clarity and global coherence.

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

@@ -4,7 +4,7 @@
 
 This section examines how nuclear reactors operate today. No current approach provides autonomous control with end-to-end correctness guarantees—neither human-centered operation nor formal methods. 
 
-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. 
 
 These limits establish the verification gap that Section 3 addresses.
 
@@ -14,7 +14,7 @@ Understanding the limits of current practice requires examining how nuclear plan
 
 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. These 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. No proofs confirm that required actions complete within available timeframes. No proofs confirm that transitions between procedure sets maintain safety invariants.
+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
@@ -31,9 +31,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. 
+The previous subsection established that procedures lack formal verification despite rigorous development, representing 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. Procedures define what to do. Human operators determine when and how. This determination 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; human operators determine when and how. This determination 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
@@ -119,9 +119,7 @@ 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 attacked the problem from the opposite direction. They extended temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). 
+HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. Other researchers attacked the problem from the opposite direction, 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
-
-While dL addresses continuous dynamics, it 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

3-research-approach/v3.tex

@@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified either discrete switching logic or continuous control behavior—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.
+Previous approaches verified either discrete switching logic or continuous control behavior—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.
 
-My approach bridges that gap. It composes formal methods from computer science with control-theoretic verification. It formalizes reactor operations as hybrid automata.
+My approach bridges that gap, composing formal methods from computer science with control-theoretic verification and formalizing reactor operations as hybrid automata.
 
-Hybrid system verification faces a fundamental challenge. Discrete transitions change the governing vector field. This creates discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
+Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
 
-This methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active. Continuous controllers govern plant behavior within each mode.
+This methodology decomposes the problem, verifying discrete switching logic and continuous mode behavior separately, then composing them to establish guarantees for 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.
 
 A high-assurance hybrid autonomous control system requires a mathematical description. This work draws on automata theory, temporal logic, and control theory to provide that description. A hybrid system is a dynamical system with both continuous and discrete states. This proposal addresses continuous autonomous hybrid systems specifically—systems with no external input where continuous states remain continuous when discrete states change, representing physical quantities that remain Lipschitz continuous. This work follows the nomenclature from the Handbook on Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here for convenience:
 
@@ -206,8 +206,8 @@ operators that express properties over time. Temporal logic relates discrete
 control modes to one another and defines all HAHACS requirements. Boundary
 conditions between discrete states determine guard conditions $\mathcal{G}$ and
 specify their behavior. Continuous mode invariants similarly express as temporal
-logic statements. These specifications form the basis of any proofs about a
+logic statements, forming the basis of any proofs about a
-HAHACS, constituting fundamental truth statements about designed system behavior.
+HAHACS and constituting fundamental truth statements about designed system behavior.
 
 Discrete mode transitions include predicates—Boolean functions over the
 continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
@@ -275,8 +275,6 @@ The synthesized automaton translates directly to executable code through standar
 
 Reactive synthesis has proven successful in robotics, avionics, and industrial control. Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
 
-Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
-
 Reactive synthesis produces discrete mode-switching logic from procedures. The next subsection addresses what executes within each discrete mode: continuous control and its verification.
 
 %%% NOTES (Section 3):

4-metrics-of-success/v1.tex

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Question: How do we measure success?}
 
-Section 3 established the technical approach. It answered what is new (compositional verification bridging discrete synthesis with continuous control) and why it will succeed (existing procedural structure, bounded complexity, industrial validation). This section addresses the next Heilmeier question: how to measure success. 
+Section 3 established the technical approach, answering what is new (compositional verification bridging discrete synthesis with continuous control) and why it will succeed (existing procedural structure, bounded complexity, industrial validation). This section addresses the next Heilmeier question: how to measure success. 
 
 The answer: Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
 
@@ -85,12 +85,6 @@ controllers implementable with current technology.
 
 This section answered the Heilmeier question: How do we measure success?
 
-\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility through progressively integrated validation. 
+\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility through progressively integrated validation. TRL 3 proves component-level correctness: each part works independently. TRL 4 demonstrates system-level integration in simulation: the parts compose correctly. TRL 5 validates hardware implementation in a relevant environment: the complete system works on real control hardware. Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology.
 
-TRL 3 proves component-level correctness: each part works independently. TRL 4 demonstrates system-level integration in simulation: the parts compose correctly. TRL 5 validates hardware implementation in a relevant environment: the complete system works on real control hardware. 
+Success, however, depends on several critical assumptions. If these assumptions prove false, research could stall at lower readiness levels despite sound methodology. Section 5 addresses the complementary question: What could prevent success?
-
-Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology.
-
-Success, however, depends on several critical assumptions. If these assumptions prove false, research could stall at lower readiness levels despite sound methodology. 
-
-Section 5 addresses the complementary question: What could prevent success?

5-risks-and-contingencies/v1.tex

@@ -6,7 +6,7 @@ Section 4 defined success as reaching TRL 5 through component validation, system
 
 Every research plan rests on assumptions that might prove false. This section identifies four primary risks that could prevent successful completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration. 
 
-Each risk carries associated early warning indicators. Each has contingency plans that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results. It 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}
 

6-broader-impacts/v1.tex

@@ -6,7 +6,7 @@ Sections 2--5 established the complete technical research plan. Section 2 answer
 
 This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact.
 
-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, and 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, and 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.