Strategic edits: strengthened Heilmeier alignment and document coherence

- Improved cross-references between sections
- Strengthened transitions emphasizing Heilmeier structure
- Made explicit connections showing how each section answers its questions
- Enhanced narrative thread through the document

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,14 +2,14 @@
 This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Human operators control nuclear reactors today. They follow detailed written procedures and switch between control objectives as plant conditions change.
+Nuclear reactors today require 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 staffing costs per megawatt far exceed those of conventional plants. This 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.
+Small modular reactors face a fundamental economic challenge: staffing costs per megawatt far 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
 This research unifies formal methods from computer science with control theory to produce hybrid control systems 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 verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic 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 verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic 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. 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 each discrete mode's requirements. Engineers design these controllers using standard control theory.
 

1-goals-and-outcomes/v1.tex

@@ -6,16 +6,16 @@ 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
-Extensively trained human operators control nuclear plants today. They 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, following 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. It creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face staffing costs per megawatt far exceeding those of conventional plants. This 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.
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face staffing costs per megawatt far exceeding 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
 This research unifies formal methods with control theory to produce hybrid control systems 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. However, they cannot verify the continuous dynamics governing transitions. Control theory verifies continuous behavior. However, it cannot prove discrete switching correctness. Both are required for end-to-end correctness.
+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 verify 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. These specifications 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. Operating procedures transform 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.
 
@@ -62,7 +62,7 @@ If successful, this approach produces three concrete outcomes:
 \end{enumerate}
 
 % IMPACT PARAGRAPH Innovation
-\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. 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. Section 2 will show that prior work verified discrete logic or continuous dynamics—never both compositionally. 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. These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
 % Outcome Impact
 If successful, control engineers will create autonomous controllers from existing procedures with mathematical proofs of correct behavior, making high-assurance autonomous control practical for safety-critical applications. This capability is essential for the economic viability of next-generation nuclear power. Small modular reactors, in particular, offer a promising solution to growing energy demands, but their success depends on reducing per-megawatt operating costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. 

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

@@ -12,7 +12,7 @@ Section 3 addresses the verification gap these limits establish.
 
 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}. 
+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}. 
 
 Expert judgment and simulator validation—not formal verification—form the basis for procedure development. Regulations mandate rigorous assessment. Specifically, 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states. No proof confirms that required actions complete within available timeframes. No proof confirms that transitions between procedure sets maintain safety invariants.
 
@@ -165,4 +165,4 @@ This section addressed two Heilmeier questions: What has been done? What are the
 
 \textbf{Why now?} Two forces create urgency. First, economic necessity: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, technical maturity: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
 
-The verification gap is clear. The timing is right. Section 3 addresses this gap, establishing what is new and why the approach will succeed.
+Section 2 established what has been done and the limits of current practice. The verification gap is clear. The timing is right. Section 3 addresses the next two Heilmeier questions—what is new and why it will succeed—presenting the technical approach that closes this gap.

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 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 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; 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 and 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.
+Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities that traditional verification techniques cannot handle directly.
 
-This methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately. It 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 by 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.
 
 Hybrid systems require mathematical formalization. This work draws on automata theory, temporal logic, and control theory to provide that description.
 
@@ -63,9 +63,9 @@ A HAHACS requires this tuple together with proof artifacts demonstrating that th
 Three innovations enable compositional verification:
 
 \begin{enumerate}
-\item \textbf{Contract-based decomposition:} This approach inverts the traditional structure. Instead of attempting global hybrid system verification, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems.
+\item \textbf{Contract-based decomposition:} Instead of attempting global hybrid system verification, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems.
-\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to match each mode type. This classification enables mode-local analysis with provable composition guarantees.
+\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to match each mode type and enabling mode-local analysis with provable composition guarantees.
-\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This existing structure avoids artificial abstractions, making the approach tractable for complex systems like nuclear reactor startup.
+\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, providing existing structure that avoids artificial abstractions and makes the approach tractable for complex systems like nuclear reactor startup.
 \end{enumerate>
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed.
@@ -144,7 +144,7 @@ These factors combine to demonstrate feasibility on production control systems w
 
 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 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.
+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.
 
@@ -546,7 +546,7 @@ Section 2 established that prior work verified discrete logic or continuous dyna
 
 \textit{Industrial validation.} Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
 
-The complete technical methodology is now established. Section 2 answered what has been done and what limits current practice. This section answered what is new and why it will succeed. Three questions remain: How will success be measured? What could prevent success? Who cares, why now, and what difference will it make? Sections 4, 5, and 6 address these in turn.
+The complete technical methodology is now established. Sections 2 and 3 addressed the first four Heilmeier questions: what has been done, what limits current practice, what is new, and why it will succeed. Three questions remain. Section 4 addresses how success will be measured. Section 5 identifies what could prevent success. Section 6 explains who cares, why now, and what difference this work will make.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -81,7 +81,7 @@ a relevant laboratory environment. This establishes both theoretical validity
 and practical feasibility, proving the methodology produces verified
 controllers implementable with current technology.
 
-This section answered the Heilmeier question—how do we measure success?
+This section answered the Heilmeier question: How will success be measured?
 
 \textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5. Each level demonstrates both theoretical correctness and practical feasibility through progressively integrated validation.
 
@@ -93,4 +93,4 @@ TRL 5 validates hardware implementation in a relevant environment: the complete
 
 Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology—not merely theoretically sound but practically deployable.
 
-Success assumes critical technical challenges can be overcome. Section 5 addresses the complementary question—what could prevent success?
+Sections 2 through 4 addressed five Heilmeier questions: what has been done, what limits current practice, what is new, why it will succeed, and how to measure success. Success assumes critical technical challenges can be overcome. Section 5 addresses what could prevent success.

5-risks-and-contingencies/v1.tex

@@ -139,7 +139,7 @@ Each risk has identifiable early warning indicators enabling detection before fa
 
 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. 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.
+Sections 2 through 5 established the complete technical research plan. Section 2 addressed what has been done and what limits current practice. Section 3 established what is new and why it will succeed. Section 4 defined how to measure success. This section identified what could prevent success and how to respond.
 
 One critical question remains: Who cares? Why now? What difference will it make?
 

6-broader-impacts/v1.tex

@@ -70,4 +70,4 @@ This section answered three critical Heilmeier questions:
 
 \textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier and enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure, extending beyond nuclear power to any safety-critical system requiring provable correctness.
 
-The complete research plan now spans technical approach (Section 3), success metrics (Section 4), risk mitigation (Section 5), and broader impact (this section). One final Heilmeier question remains—how long will it take? Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement, demonstrating the proposed work is achievable within a doctoral timeline.
+Sections 2 through 6 addressed all but one of the Heilmeier questions. Section 2 established what has been done and what limits current practice. Section 3 explained what is new and why it will succeed. Section 4 defined how to measure success. Section 5 identified what could prevent success. This section connected technical methodology to economic and societal impact. One final Heilmeier question remains: How long will it take? Section 8 provides the answer.