Multi-level editorial pass on thesis proposal

Three-pass editorial review:

TACTICAL (sentence-level):
- Applied Gopen's Sense of Structure principles
- Improved topic-stress positioning (key info at sentence end)
- Strengthened verb choices and tightened passive constructions
- Enhanced topic strings for better flow between related sentences
- Consolidated choppy passages into smoother prose

OPERATIONAL (paragraph/section):
- Improved transitions between subsections
- Enhanced coherence within sections
- Tightened paragraph-level flow
- Reorganized content for clearer logical progression
- Strengthened section endings and beginnings

STRATEGIC (document-level):
- Made Heilmeier questions explicit at section openings
- Improved alignment between section content and assigned questions
- Enhanced summary paragraphs answering Heilmeier questions
- Clarified how sections link to overall proposal structure
- Strengthened transitions between major sections

All changes maintain technical accuracy while improving clarity and impact.

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,20 +2,20 @@
 This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Human operators control today's nuclear reactors through extensive training. They follow detailed written procedures and switch between control objectives based on plant conditions.
+Today's nuclear reactors depend on human operators with extensive training. These operators follow detailed written procedures and switch between control objectives based on plant conditions.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. This threatens their economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only with assurance equal to or exceeding that of human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening their economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only with assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-This research produces hybrid control systems correct by construction. It combines formal methods from computer science with control theory. 
+This research produces hybrid control systems correct by construction, combining formal methods from computer science with control theory. 
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods alone fail—they generate provably correct switching logic but cannot handle continuous dynamics governing transitions. Control theory alone also fails—it 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 alone fail because they generate provably correct switching logic but cannot handle the continuous dynamics governing transitions. Control theory alone also fails because it 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. It 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 each discrete mode imposes. Standard control theory techniques design these continuous controllers.
+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 provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements each discrete mode imposes. Standard control theory techniques design these continuous controllers.
 
-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. This enables local verification without global trajectory analysis. An Emerson Ovation control system will demonstrate the methodology.
+Control objectives classify continuous modes into three types: transitory modes drive the plant between conditions, stabilizing modes maintain operation within regions, and expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove safe mode transitions, enabling local verification without global trajectory analysis. An Emerson Ovation control system will demonstrate the methodology.
 % Pay-off
-This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It directly addresses the economic constraints threatening small modular reactor viability.
+This approach manages complex nuclear power operations autonomously while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS
 This research, if successful, produces three concrete outcomes:

1-goals-and-outcomes/v1.tex

@@ -6,22 +6,21 @@ 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
-Human operators control today's nuclear plants through extensive training. They follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
+Today's nuclear plants depend on human operators with extensive training. These operators follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
 % Gap
-This reliance on human operators prevents autonomous control. 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 their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only with 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 per-megawatt staffing costs far exceeding those of conventional plants, threatening their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only with assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This research produces hybrid control systems correct by construction. It combines formal methods with control theory.
+This research produces hybrid control systems correct by construction, combining 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. They fail, however, when continuous dynamics govern transitions. Control theory verifies continuous behavior. It cannot, however, 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 fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Achieving end-to-end correctness requires both approaches working together.
 % 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. Operating procedures formalize into logical specifications. These specifications 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. Operating procedures formalize 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
+The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation requirements.
-requirements.
 
 % OUTCOMES PARAGRAPHS
-This approach produces three concrete outcomes:
+If successful, this approach produces three concrete outcomes:
 
 \begin{enumerate}
 
@@ -63,7 +62,7 @@ This approach produces three concrete outcomes:
 \end{enumerate}
 
 % IMPACT PARAGRAPH Innovation
-These three outcomes establish a complete methodology from regulatory documents to deployed systems: procedure translation, continuous verification, and hardware demonstration.
+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 to close that gap. The key innovation treats discrete specifications as contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. Section 2 examines why prior work has not achieved this integration. Section 3 details how this integration will be accomplished.
 

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

@@ -1,14 +1,16 @@
 \section{State of the Art and Limits of Current Practice}
 
-\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today. Current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis: reactor operators and their operating procedures, the fundamental limitations of human-based operation, and formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis.
+\textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
+
+This section answers these questions by examining how nuclear reactors operate today. Current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis: reactor operators and their operating procedures, the fundamental limitations of human-based operation, and formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis.
 
 \subsection{Current Reactor Procedures and Operation}
 
 Understanding the limits of current practice requires first examining how nuclear plants operate today. Three aspects structure this analysis: the hierarchy of procedures, the role of operators in executing them, and the operational modes that govern reactor control.
 
-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}. 
+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, and 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. Key safety properties, however, escape formal verification. No mathematical proofs confirm that procedures cover all possible plant states. No proofs verify that required actions complete within available timeframes. No proofs ensure that transitions between procedure sets maintain safety invariants.
+Procedure development relies on expert judgment and simulator validation—not formal verification. While 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review, 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
@@ -25,9 +27,9 @@ This division between automated and human-controlled functions reveals the funda
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development. The previous subsection established this. 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.
+Procedures lack formal verification despite rigorous development—but 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.
 
-Procedures define what to do. Human operators determine when and how. This determination introduces persistent failure modes. Training alone cannot eliminate them.
+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
@@ -37,12 +39,7 @@ shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
 and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
 operator requires several years of training.
 
-Despite decades of improvements in training and procedures, human error persistently contributes to nuclear safety incidents—a persistence that motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster: operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a
+Despite decades of improvements in training and procedures, human error persistently contributes to nuclear safety incidents—a persistence that motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster: operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a fundamental ambiguity: placing responsibility for safe power plant operations on the licensee without formally verifying that operators can fulfill this responsibility guarantees nothing. This tension between operational flexibility and safety assurance remains unresolved—the person responsible for reactor safety often becomes the root cause of failure.
-fundamental ambiguity: placing responsibility for safe power plant operations on
-the licensee without formally verifying that operators can fulfill this
-responsibility guarantees nothing. This tension between operational
-flexibility and safety assurance remains unresolved. The person responsible for
-reactor safety often becomes the root cause of failure.
 
 Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events, compared to approximately 20\% for equipment failures~\cite{WNA2020}. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
 of 190 events at Chinese nuclear power plants from
@@ -58,11 +55,11 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The previous two subsections revealed two critical limitations of current practice. First, procedures lack formal verification despite rigorous development processes. Second, human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. 
+The previous two subsections revealed two critical limitations of current practice: procedures lack formal verification despite rigorous development processes, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. 
 
-Training and procedural improvements cannot solve these problems. They are fundamental limitations, not remediable defects. Formal methods might offer a solution. They could provide mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems?
+Training and procedural improvements cannot solve these problems—they are fundamental limitations, not remediable defects. Formal methods might offer a solution by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems?
 
-Even the most advanced formal methods applications in nuclear control leave a critical verification gap. This subsection examines two approaches that illustrate this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
+Even the most advanced formal methods applications in nuclear control leave a critical verification gap. This subsection examines two approaches that illustrate this gap: HARDENS, which verified discrete logic without continuous dynamics, and differential dynamic logic, which handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
 
 \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control}
 
@@ -120,7 +117,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: extending 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 by extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). 
 
 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
@@ -155,12 +152,18 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-This section answered two Heilmeier questions assigned to the State of the Art analysis.
+This section answered the two Heilmeier questions assigned to the State of the Art analysis.
 
-\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability limitations. Four decades of training improvements have failed to eliminate these limitations. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis. No existing approach addresses both discrete and continuous verification compositionally.
+\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations:
+\begin{itemize}
+\item Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate.
+\item HARDENS verified discrete logic but omitted continuous dynamics.
+\item Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis.
+\end{itemize}
+No existing approach addresses both discrete and continuous verification compositionally.
 
-\textbf{What are the limits of current practice?} The answer is clear: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This verification gap prevents autonomous nuclear control with end-to-end correctness guarantees. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
+\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This verification gap prevents autonomous nuclear control with end-to-end correctness guarantees. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-Two imperatives converge to make closing this gap urgent. First, economic necessity: small modular reactors cannot compete economically with per-megawatt staffing costs matching large conventional plants. Second, technical opportunity: formal methods tools have matured sufficiently to enable compositional hybrid verification. 
+Two imperatives converge to make closing this gap urgent: economic necessity (small modular reactors cannot compete economically with per-megawatt staffing costs matching large conventional plants) and technical opportunity (formal methods tools have matured sufficiently to enable compositional hybrid verification). 
 
-Section 3 addresses this verification gap. It establishes what makes the proposed approach new and why it will succeed.
+Section 3 addresses this verification gap by establishing what makes the proposed approach new and why it will succeed.

3-research-approach/v3.tex

@@ -1,5 +1,9 @@
 \section{Research Approach}
 
+\textbf{Heilmeier Questions: What is new? Why will it succeed?}
+
+This section answers these questions by presenting the complete technical approach for synthesizing provably correct hybrid controllers from operating procedures. The innovation lies in compositional verification that bridges discrete synthesis with continuous control—three key innovations (contract-based decomposition, mode classification, and procedure-driven structure) enable this integration. The approach will succeed because it leverages existing procedural structure, bounds computational complexity through mode-level verification, and validates against real industrial hardware through the Emerson collaboration.
+
 % ============================================================================
 % STRUCTURE (maps to Thesis.RA tasks):
 %   1. Introduction + Hybrid Systems Definition (Task 34)
@@ -15,13 +19,13 @@
 % ----------------------------------------------------------------------------
 % 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; both consume enormous resources.
 
-This work bridges that gap. It composes formal methods from computer science with control-theoretic verification. It formalizes reactor operations as hybrid automata.
+This work 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 in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
 
-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; 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.
 
 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. These continuous states represent 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:
 
@@ -132,15 +136,15 @@ These factors combine to demonstrate feasibility on production control systems w
 
 The previous subsection established the hybrid automaton formalism. This mathematical framework describes discrete modes, continuous dynamics, guards, and invariants. 
 
-A critical question remains: where do these formal descriptions originate? This subsection answers by demonstrating that nuclear operations already possess a natural hybrid structure. This structure maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. 
+A critical question remains: where do these formal descriptions originate? This subsection answers by demonstrating that nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. 
 
-The approach does not impose artificial abstractions. Instead, it constructs formal hybrid systems from existing operational knowledge. It leverages decades of domain expertise encoded in operating procedures.
+The approach does not impose artificial abstractions. Instead, it constructs formal hybrid systems from existing operational knowledge, leveraging decades of domain expertise encoded in operating procedures.
 
-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. It manages labor needs and supply chains to optimize scheduled maintenance and downtime.
+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.
 
-The tactical level controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems. These continuous systems directly impact the physical state of the plant. They maintain pressurizer level, core temperature, and reactivity through chemical shim.
+The tactical level controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems—continuous systems that directly impact the physical state of the plant by maintaining pressurizer level, core temperature, and reactivity through chemical shim.
 
-The operational scope links these extremes. It represents the primary responsibility of human operators today. Operators implement tactical control sequences to achieve strategic objectives, bridging high-level goals with low-level execution. 
+The operational scope links these extremes and represents the primary responsibility of human operators today. Operators implement tactical control sequences to achieve strategic objectives, bridging high-level goals with low-level execution. 
 
 An example clarifies this three-level structure. Consider a strategic goal to perform refueling at a certain time. The tactical level currently maintains core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this objective.
 
@@ -250,9 +254,9 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 \subsection{Discrete Controller Synthesis}
 
-The previous subsection showed how operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do. But how do we implement those requirements? Reactive synthesis provides the answer—this technique automatically constructs controllers guaranteed to satisfy temporal logic specifications.
+Operating procedures translate into temporal logic specifications using FRET—these specifications define what the system must do. But how do we implement those requirements? Reactive synthesis provides the answer by automatically constructing controllers guaranteed to satisfy temporal logic specifications.
 
-Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. System requirements defined as temporal logic specifications enable reactive synthesis to build the discrete control system. Our systems fit this model: the current discrete state and status of guard conditions form the input; the next discrete state forms the output.
+Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. System requirements defined as temporal logic specifications enable reactive synthesis to build the discrete control system. Our systems fit this model: the current discrete state and status of guard conditions form the input, while the next discrete state forms the output.
 
 Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ specifying desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller exists. Unrealizable specifications indicate conflicting or impossible requirements in
 the original procedures—this realizability check catches errors before implementation. 
@@ -265,7 +269,9 @@ 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.
 
-Having established how discrete mode-switching logic synthesizes from procedures, the question becomes: what executes within each discrete mode? The next subsection addresses continuous control modes and their verification. 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.
+
+Having established how discrete mode-switching logic synthesizes from procedures, the question becomes: what executes within each discrete mode? The next subsection addresses continuous control modes and their verification.
 
 %%% NOTES (Section 3):
 % - Mention computational complexity of synthesis (doubly exponential worst case)

4-metrics-of-success/v1.tex

@@ -1,6 +1,8 @@
 \section{Metrics for Success}
 
-\textbf{How do we measure success?} Section 3 established the technical approach—what will be done and why it will work. This section addresses how we measure whether it actually succeeds. The answer: Technology Readiness Level advancement, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
+\textbf{Heilmeier Question: How do we measure success?}
+
+Section 3 established the technical approach—what will be done and why it will work. This section addresses how we measure whether it actually succeeds. The answer: Technology Readiness Level advancement, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
 
 This work begins at TRL 2--3 and aims to reach 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 are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5.
 

5-risks-and-contingencies/v1.tex

@@ -1,8 +1,10 @@
 \section{Risks and Contingencies}
 
-\textbf{What could prevent success?} Section 4 defined success as reaching TRL 5. This requires component validation, system integration, and hardware demonstration.
+\textbf{Heilmeier Question: What could prevent success?}
 
-Every research plan, however, rests on assumptions that might prove false. This section identifies four primary risks that could prevent successful completion. These risks are: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration. 
+Section 4 defined success as reaching TRL 5, requiring component validation, system integration, and hardware demonstration.
+
+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.
 

6-broader-impacts/v1.tex

@@ -1,8 +1,10 @@
 \section{Broader Impacts}
 
-\textbf{Who cares? Why now? What difference will it make?} Sections 2--5 established the complete technical research plan. Section 2 examined what has been done and its limits. Section 3 detailed what is new and why it will succeed. Section 4 explained how success will be measured. Section 5 identified what could prevent success and how to mitigate those risks.
+\textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-This section addresses the remaining Heilmeier questions. It connects technical methodology to economic and societal impact. The answer: this research directly addresses a \$21--28 billion annual cost barrier. It establishes a generalizable framework for safety-critical autonomous systems.
+Sections 2--5 established the complete technical research plan: what has been done and its limits (Section 2), what is new and why it will succeed (Section 3), how success will be measured (Section 4), and what could prevent success with mitigation strategies (Section 5).
+
+This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact. The answer: this research directly addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems.
 
 The technical approach enables compositional hybrid verification. This capability did not exist before. But why does this matter beyond academic contribution? 
 

8-schedule/v1.tex

@@ -1,6 +1,8 @@
 \section{Schedule, Milestones, and Deliverables}
 
-\textbf{How long will it take?} This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC Fellowship provide all computational and experimental resources. The work progresses sequentially through three main research thrusts, culminating in integrated demonstration and validation.
+\textbf{Heilmeier Question: How long will it take?}
+
+This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC Fellowship provide all computational and experimental resources. The work progresses sequentially through three main research thrusts, culminating in integrated demonstration and validation.
 
 The first semester (Spring 2026) focuses on Thrust 1, translating startup
 procedures into formal temporal logic specifications using FRET. This