Editorial pass: three-level copy edit (tactical, operational, strategic)

Tactical (sentence-level):
- Applied Gopen's issue-point structure: sentences now lead with topic
- Improved topic-stress positioning: key info at sentence ends
- Strengthened verb choices and reduced passive voice where appropriate
- Tightened sentence flow and eliminated unnecessary words

Operational (paragraph/section):
- Improved transitions between subsections, especially at critical boundaries
- Strengthened coherence within paragraphs
- Enhanced logical progression through sections
- Clarified connections between arguments

Strategic (document-level):
- Verified Heilmeier catechism alignment in each section
- Strengthened section summaries to explicitly answer assigned questions
- Improved forward/backward references between sections
- Enhanced overall narrative coherence

All changes preserve 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
-Extensively trained human operators control today's nuclear reactors. Based on plant conditions, these operators follow detailed written procedures and switch between control objectives.
+Extensively trained human operators control today's nuclear reactors, following detailed written procedures and switching between control objectives based on plant conditions.
 % Gap
-Small modular reactors face a fundamental economic challenge: 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 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 assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 This research combines formal methods from computer science with control theory to produce hybrid control systems correct by construction. 
 % Rationale
-Operators already work this way: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both approaches must work together to achieve end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic 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 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, standard control theory designs continuous controllers for each discrete mode, while reachability analysis verifies each controller.
+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—designed using standard control theory—satisfy the requirements imposed by each discrete mode.
 
-Continuous modes classify by transition objective: transitory modes drive the plant between conditions, stabilizing modes maintain operation within regions, and expulsory modes ensure safety under failures. Assume-guarantee contracts and barrier certificates prove safe mode transitions, enabling local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system. 
+Continuous modes classify by control objective: 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. The methodology demonstrates on an Emerson Ovation control system. 
 % Pay-off
-This autonomous control approach manages complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability.
+This approach manages complex nuclear power operations autonomously while maintaining safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS
 This research, if successful, produces three concrete outcomes:

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 today's nuclear plants. These operators follow detailed written procedures and strict regulatory requirements while switching between control modes based on plant conditions and procedural guidance.
+Extensively trained human operators control today's nuclear plants, following detailed written procedures and strict regulatory requirements while switching 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: per-megawatt staffing costs for small modular reactors far exceed those of conventional plants, threatening their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only if they provide assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
 This research combines formal methods with control theory to produce hybrid control systems correct by construction.
 % Rationale
-Operators already work this way: discrete logic switches between continuous control modes. Existing formal methods can generate provably correct switching logic from written requirements, but they fail when continuous dynamics govern transitions. Control theory verifies continuous behavior, but it cannot prove discrete switching correctness. Both approaches must work together to achieve end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods can generate provably correct switching logic from written requirements, but they 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
-This approach closes the gap through two steps. First, it synthesizes discrete mode transitions directly from written operating procedures. Second, it verifies continuous behavior between transitions. Operating procedures formalize into logical specifications. Continuous dynamics verify against transition requirements. The result: autonomous controllers provably free from design defects. 
+This approach closes the gap through two steps. First, it synthesizes discrete mode transitions directly from written operating procedures. Second, it verifies continuous behavior between transitions. Operating procedures formalize 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.
@@ -79,7 +79,7 @@ costs through increased autonomy. This research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the
 nuclear industry requires.
 
-These three outcomes establish a complete methodology from regulatory documents to deployed systems. This proposal follows the Heilmeier Catechism, with each section explicitly answering its assigned questions:
+These three outcomes establish a complete methodology from regulatory documents to deployed systems. This proposal follows the Heilmeier Catechism, with each section explicitly answering its assigned questions. Each section begins by stating its Heilmeier questions and ends by summarizing its answers, ensuring both local clarity and global coherence:
 \begin{itemize}
   \item \textbf{Section 2 (State of the Art):} What has been done? What are the limits of current practice?
   \item \textbf{Section 3 (Research Approach):} What is new? Why will it succeed?
@@ -88,4 +88,3 @@ These three outcomes establish a complete methodology from regulatory documents
   \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 and ends by summarizing its answers, ensuring both local clarity and global coherence.

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

@@ -8,7 +8,7 @@ Understanding the limits of current practice requires first examining how nuclea
 
 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. Yet key safety properties escape formal verification. Mathematical proofs confirming that procedures cover all possible plant states, that required actions complete within available timeframes, or that safety invariants hold across procedure-set transitions do not exist.
+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: mathematical proofs confirming that procedures cover all possible plant states, that required actions complete within available timeframes, or that safety invariants hold across procedure-set transitions do not exist.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -21,11 +21,11 @@ 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.
 
-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, meanwhile, 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.
+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.
 
 \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. Even 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, human operators determine when and how—introducing persistent failure modes.
+The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Even 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—introducing 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
@@ -45,7 +45,7 @@ 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
 2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
-errors, while 92\% were associated with latent errors---organizational and
+errors, while 92\% were associated with latent errors—organizational and
 systemic weaknesses that create conditions for failure.
 
 
@@ -116,7 +116,7 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic without continuous dynamics. 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). dL introduces two additional operators
+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
 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
@@ -151,8 +151,8 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 This section answered two Heilmeier questions about current practice:
 
-\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate. 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.
+\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate. 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 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.
+\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 this gap urgent: economic necessity (small modular reactors cannot compete 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 by establishing what makes the proposed approach new and why it will succeed.

3-research-approach/v3.tex

@@ -15,11 +15,11 @@
 % ----------------------------------------------------------------------------
 % 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 and test discrete switching logic through simulated control room testing and human factors research. Despite consuming enormous resources, neither method provides rigorous guarantees.
+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. Despite consuming enormous resources, neither method provides rigorous guarantees.
 
 This work bridges the 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. This creates discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques fail to 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 fail to handle this interaction directly.
 
 Our methodology decomposes this 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.
 
@@ -51,17 +51,17 @@ Creating a HAHACS requires constructing this tuple together with proof artifacts
 \textbf{What is new in this research?} Section 2 established that existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Prior work has not integrated them into a systematic design methodology spanning procedures to verified implementation. Three innovations enable this integration:
 
 \begin{enumerate}
-\item \textbf{Contract-based decomposition:} Instead of attempting global hybrid system verification, this approach inverts the traditional structure. 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:} 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{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to be selected for 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. This classification enables mode-local analysis with provable composition guarantees.
-\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases. Leveraging this existing structure avoids imposing artificial abstractions and makes the approach tractable for complex systems like nuclear reactor startup.
+\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases. Leveraging this existing structure avoids imposing artificial abstractions, making the approach tractable for complex systems like nuclear reactor startup.
-\end{enumerate}
+\end{enumerate>
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed:
 
 \begin{enumerate}
-\item \textbf{Leverage existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This work formalizes existing structure rather than imposing artificial abstractions. This makes adoption tractable for domain experts without formal methods training.
+\item \textbf{Leverage existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This work formalizes existing structure rather than imposing artificial abstractions, making adoption tractable for domain experts without formal methods training.
-\item \textbf{Avoid state explosion:} Mode-level verification checks each mode against local contracts rather than attempting global hybrid system analysis. This decomposition bounds computational complexity. It transforms an intractable global problem into tractable local verifications.
+\item \textbf{Avoid state explosion:} Mode-level verification checks each mode against local contracts rather than attempting global hybrid system analysis. This decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
-\item \textbf{Industrial validation:} The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. This ensures solutions address real deployment constraints, not just theoretical correctness.
+\item \textbf{Industrial validation:} The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints, not just theoretical correctness.
 \end{enumerate}
 
 These factors combine to demonstrate feasibility on production control systems with realistic reactor models—not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence.
@@ -130,7 +130,7 @@ These factors combine to demonstrate feasibility on production control systems w
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The previous subsection established the hybrid automaton formalism—a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. Where do these formal descriptions originate? This subsection demonstrates that nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. Rather than imposing artificial abstractions, this approach constructs formal hybrid systems from existing operational knowledge.
+The previous subsection established the hybrid automaton formalism—a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. Where do these formal descriptions originate? This subsection demonstrates that nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. Rather than imposing artificial abstractions, this approach 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.
 
@@ -279,7 +279,7 @@ The previous subsection established that reactive synthesis produces a provably
 
 This subsection describes the continuous control modes executing within each discrete state and explains how they verify against requirements imposed by the discrete layer. Control objectives determine the verification approach: modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
 
-This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification, where verification confirms whether a given implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that design capability exists. The contribution is the verification framework confirming that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
+This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification, where verification confirms whether a given implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that design capability exists. The contribution lies in the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
 The operational control scope defines go/no-go decisions that determine what
 kind of continuous control to implement. The entry or exit conditions of a
@@ -317,9 +317,7 @@ precise objectives for continuous control. The continuous controller for mode
 $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
 state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.
 
-We classify continuous controllers into three types based on their objectives:
+Continuous controllers classify into three types based on their control objectives, each requiring distinct verification tools matched to its purpose. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. The following subsections detail each mode type and its verification approach, progressing from nominal operations (transitory and stabilizing modes) to off-nominal scenarios (expulsory modes).
-transitory, stabilizing, and expulsory. Each type requires distinct verification
-tools matched to its control objective. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. The following subsections detail each mode type and its verification approach.
 
 %%% NOTES (Section 4):
 % - Add figure showing the relationship between entry/exit/safety sets
@@ -383,7 +381,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-While transitory modes drive the system toward exit conditions, stabilizing modes maintain the system within a desired operating region indefinitely—examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
+Transitory modes drive the system toward exit conditions—answering "can we reach the target?" Stabilizing modes address a fundamentally different question: "will we stay within bounds?" These modes maintain the system within a desired operating region indefinitely—examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
 
 Where reachability analysis answers "can the system reach a target?", stabilizing modes ask "does the system stay within bounds?" Barrier certificates provide the appropriate tool.
 Barrier certificates analyze the dynamics of the system to determine whether
@@ -437,7 +435,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-The first two mode types—transitory modes that move the plant between conditions and stabilizing modes that maintain the plant within regions—handle nominal operations under the assumption that plant dynamics match the design model. Expulsory modes handle the opposite case: situations where the plant deviates from expected behavior due to component failures, sensor degradation, or unanticipated disturbances.
+The first two mode types—transitory modes that move the plant between conditions and stabilizing modes that maintain the plant within regions—handle nominal operations under the assumption that plant dynamics match the design model. Both assume the plant behaves as expected. Expulsory modes address a fundamentally different scenario: situations where the plant deviates from expected behavior due to component failures, sensor degradation, or unanticipated disturbances. Here, robustness matters more than optimality.
 
 Expulsory controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and controlled depressurization procedures.
 
@@ -518,9 +516,9 @@ outcomes can align best with customer needs.
 
 This section answered two critical Heilmeier questions about the research approach:
 
-\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations enable this integration: using discrete synthesis to define verification contracts (inverting traditional global analysis), classifying continuous modes by objective to select appropriate verification tools, and leveraging existing procedural structure to avoid intractable state explosion. Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. Compositional verification enables what global analysis cannot achieve.
+\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations enable this integration: contract-based decomposition (using discrete synthesis to define verification contracts that bound continuous verification, inverting traditional global analysis), mode classification (classifying continuous modes by objective to select appropriate verification tools, enabling mode-local analysis with provable composition guarantees), and procedure-driven structure (leveraging existing procedural structure to avoid intractable state explosion). Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. Compositional verification enables what global analysis cannot achieve.
 
-\textbf{Why will this approach succeed?} Three factors ensure practical feasibility: nuclear procedures already decompose operations into discrete phases with explicit transition criteria (allowing the approach to formalize existing structure rather than impose artificial abstractions), mode-level verification bounds each verification problem locally (avoiding the state explosion that makes global hybrid system analysis intractable), and the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility.
+\textbf{Why will this approach succeed?} Three factors ensure practical feasibility: nuclear procedures already decompose operations into discrete phases with explicit transition criteria (allowing the approach to formalize existing structure rather than impose artificial abstractions), mode-level verification bounds each verification problem locally (avoiding the state explosion that makes global hybrid system analysis intractable), and the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility—ensuring solutions address real deployment constraints, not just theoretical correctness.
 
 The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. What remains are operational questions about executing this research plan. Section 4 addresses \textit{How will success be measured?} through Technology Readiness Level advancement. Section 5 addresses \textit{What could prevent success?} through risk analysis and contingency planning. Section 6 addresses \textit{Who cares? Why now? What difference will it make?} through economic and societal impact analysis.
 

4-metrics-of-success/v1.tex

@@ -6,7 +6,7 @@ This work begins at TRL 2--3 and aims to reach TRL 5, where system components op
 
 Technology Readiness Levels provide the ideal success metric by explicitly measuring the gap between academic proof-of-concept and practical deployment—precisely what this work bridges. Academic metrics like papers published or theorems proved fail to capture practical feasibility. Empirical metrics like simulation accuracy or computational speed fail to demonstrate theoretical rigor. Both measure simultaneously through TRLs.
 
-Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while progressively demonstrating practical feasibility. Formal verification must remain valid as the system moves from individual components to integrated hardware testing.
+Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while progressively demonstrating practical feasibility. Formal verification must remain valid as the system moves from individual components to integrated hardware testing—the proofs must compose as the system scales.
 
 The nuclear industry requires extremely high assurance before deploying new
 control technologies. Demonstrating theoretical correctness alone proves

5-risks-and-contingencies/v1.tex

@@ -122,6 +122,6 @@ extensions, ensuring they address industry-wide practices rather than specific
 quirks.
 
 
-This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks threaten project completion. First: computational tractability of synthesis and verification. Second: complexity of the discrete-continuous interface. Third: completeness of procedure formalization. Fourth: hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment. This critical design feature maintains contribution to the field regardless of which technical obstacles prove insurmountable.
+This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks threaten project completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment. This critical design feature maintains contribution to the field regardless of which technical obstacles prove insurmountable—even "failure" advances the field by documenting precisely which barriers remain.
 
-The technical research plan is now complete. Section 3 established what will be done. Section 4 established how success will be measured. This section established what might prevent it. One critical Heilmeier question remains: \textbf{Who cares? Why now? What difference will it make?} Section 6 answers by connecting this technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector.
+The technical research plan is now complete. Section 3 established what will be done and why it will succeed. Section 4 established how success will be measured. This section established what might prevent it and how to mitigate those risks. One critical Heilmeier question remains: \textbf{Who cares? Why now? What difference will it make?} Section 6 answers by connecting this technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector.

6-broader-impacts/v1.tex

@@ -1,6 +1,6 @@
 \section{Broader Impacts}
 
-\textbf{Who cares? Why now? What difference will it make?} 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 (Section 5). This section addresses the remaining Heilmeier questions, connecting technical methodology to economic and societal impact.
+\textbf{Who cares? Why now? What difference will it make?} 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 (Section 5). This section addresses the remaining Heilmeier questions, connecting technical methodology to economic and societal impact. The answer: this research directly addresses a \$21--28 billion annual cost barrier while establishing a generalizable framework for safety-critical autonomous systems.
 
 The technical approach enables compositional hybrid verification—a capability that did not exist before. But why does this matter beyond academic contribution? Three stakeholder groups converge on the same economic constraint: high operating costs driven by staffing requirements.