Editorial pass: tactical, operational, strategic improvements

TACTICAL (sentence-level):
- Applied Gopen's issue-point positioning
- Strengthened verb choices (active over passive where appropriate)
- Reduced wordiness while maintaining technical precision
- Improved topic-stress positioning for better flow
- Tightened long sentences for readability

OPERATIONAL (paragraph/section):
- Smoothed transitions between paragraphs
- Added explicit figure references where needed
- Improved subsection transitions in formal methods section
- Enhanced flow from theoretical to practical sections

STRATEGIC (document-level):
- Ensured each section clearly addresses its Heilmeier question
- Improved consistency of Heilmeier framing across sections
- Strengthened transitions between major sections
- Verified alignment of outcomes with stated research questions

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,32 +2,18 @@
 This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors require extensively trained operators who follow detailed written procedures. Operators switch between control objectives based on plant conditions.
+Nuclear reactors require extensively trained operators who follow detailed written procedures, switching 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, threatening economic viability. To remain competitive, these reactors need autonomous control systems that manage complex operational sequences safely without constant supervision while providing assurance equal to or exceeding that of human-operated systems.
+Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. These reactors need autonomous control systems that manage complex operational sequences safely without constant supervision—systems providing assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-Formal methods from computer science combine with control theory to
+Formal methods from computer science combine with control theory to build hybrid control systems correct by construction. 
-build hybrid control systems correct by construction. 
 % Rationale
-Hybrid systems mirror operator decision-making: discrete
+Hybrid systems mirror operator decision-making: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail during transitions with continuous dynamics. Control theory verifies continuous behavior but fails to prove discrete switching correctness. 
-logic switches between continuous control modes. Existing formal methods
-generate provably correct switching logic but fail during transitions with continuous dynamics. Control theory verifies continuous behavior but
-fails to prove discrete switching correctness. 
 % Hypothesis and Technical Approach
-Three stages bridge this gap. First, written
+Three stages bridge this gap. First, written operating procedures translate into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET), which structures requirements into scope, condition, component, timing, and response elements. Realizability checking identifies conflicts and ambiguities before implementation. 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 them. Continuous modes classify by transition objectives. Assume-guarantee contracts and barrier certificates prove safe mode transitions. This enables local verification of continuous modes without global trajectory analysis across the entire hybrid system. An Emerson Ovation control system demonstrates the methodology. 
-operating procedures translate into temporal logic specifications using NASA's Formal
-Requirements Elicitation Tool (FRET). FRET structures requirements into scope,
-condition, component, timing, and response elements. Realizability
-checking identifies conflicts and ambiguities before implementation.
-Second, reactive synthesis generates deterministic automata—provably
-correct by construction.
-Third, standard control theory designs continuous controllers for each discrete mode; reachability analysis verifies them. Continuous modes classify by their transition objectives. Assume-guarantee contracts and barrier certificates prove safe mode transitions. Local verification of continuous modes
-becomes possible without global trajectory analysis across the entire hybrid system. An
-Emerson Ovation control system demonstrates this methodology. 
 % Pay-off
-This autonomous control approach can then manage complex nuclear
+This autonomous control approach manages complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
-power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS
 If this research is successful, we will be able to do the following:

1-goals-and-outcomes/v1.tex

@@ -4,24 +4,18 @@
 This research develops autonomous hybrid control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear power plants require the highest levels of control system reliability.
+Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release.
-Control system failures risk economic losses, service interruptions,
-or radiological release.
 % Known information
-Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to manage reactor control. Operators switch between different control modes based on plant conditions and procedural guidance.
+Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
 % Gap
-Human operator reliance prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs that far exceed those of conventional plants, threatening their economic viability. The nuclear industry needs autonomous control systems that safely manage complex operational sequences without constant human supervision—systems providing assurance equal to or exceeding that of human operators.
+Human operator reliance prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening economic viability. The nuclear industry needs autonomous control systems that safely manage complex operational sequences without constant human supervision—systems providing assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
 Formal methods combine with control theory to build hybrid control systems correct by construction.
 % Rationale
-Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but fail with continuous dynamics during transitions. Control theory verifies continuous behavior but fails to prove the correctness of discrete switching decisions. No existing approach provides end-to-end correctness guarantees.
+Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but fail with continuous dynamics during transitions. Control theory verifies continuous behavior but fails to prove discrete switching correctness. No existing approach provides end-to-end correctness guarantees.
 % Hypothesis
-This approach closes the gap by synthesizing discrete mode transitions directly
+This approach closes the gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between transitions. Existing procedures formalize into logical specifications while continuous dynamics verify against transition requirements, producing autonomous controllers provably free from design defects. 
-from written operating procedures and verifying continuous behavior between
-transitions. Existing procedures formalize into logical
-specifications; continuous dynamics verify against transition requirements. This produces 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.
@@ -74,12 +68,7 @@ This approach produces three concrete outcomes:
 % IMPACT PARAGRAPH Innovation
 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?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
+\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. Formal methods verify discrete logic; control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. This work establishes that bridge by treating discrete specifications as contracts that continuous controllers must satisfy, enabling independent verification of each layer while guaranteeing correct composition.
-Formal methods verify discrete logic; control theory verifies
-continuous dynamics. No existing methodology bridges both with compositional
-guarantees. This work establishes that bridge by treating discrete specifications
-as contracts that continuous controllers must satisfy. Independent
-verification of each layer becomes possible while guaranteeing correct composition.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from

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

@@ -4,7 +4,7 @@
 
 \subsection{Current Reactor Procedures and Operation}
 
-Nuclear plant procedures form a hierarchy. Normal operating procedures govern routine operations, while 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}. Expert judgment and simulator validation drive development, not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously, yet this rigor cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+Nuclear plant procedures form a 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}. Expert judgment and simulator validation drive development, not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously, yet this rigor cannot provide formal verification of key safety properties. No mathematical proof exists 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
@@ -15,24 +15,9 @@ invariants. Paper-based procedures cannot ensure correct application. Even
 computer-based procedure systems lack the formal guarantees automated reasoning
 could provide.
 
-Nuclear plants operate with multiple control modes: automatic control, where the
+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, and various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature and compensates 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 without requiring operator action.
-reactor control system maintains target parameters through continuous reactivity
-adjustment; manual control, where operators directly manipulate the reactor; and
-various intermediate modes. In typical pressurized water reactor operation, the
-reactor control system automatically maintains a floating average temperature
-and compensates for power demand changes through reactivity feedback loops
-alone. Safety systems, by contrast, already employ automation. Reactor
-Protection Systems trip automatically on safety signals with millisecond
-response times, and engineered safety features actuate automatically on accident
-signals without requiring operator action.
 
-The division between automated and human-controlled functions reveals the
+The division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems 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.
-fundamental challenge of hybrid control. Highly automated systems 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.
 
 \subsection{Human Factors in Nuclear Accidents}
 
@@ -71,9 +56,9 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Current practice reveals two critical limitations: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative path forward—mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. 
+Current practice reveals two critical limitations: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative—mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. 
 
-Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems.
+Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems. The following subsections examine why.
 
 \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control}
 
@@ -81,14 +66,7 @@ The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
 project represents the most advanced application of formal methods to nuclear
 reactor control systems to date~\cite{Kiniry2024}.
 
-HARDENS addressed a fundamental dilemma: existing U.S. nuclear control
+HARDENS addressed a fundamental dilemma: existing U.S. nuclear control rooms rely on analog technologies from the 1950s--60s, which incur significant risk and cost compared to modern control systems. The NRC contracted Galois, a formal methods firm, to demonstrate that Model-Based Systems Engineering and formal methods could design, verify, and implement a complex protection system meeting regulatory criteria at a fraction of typical cost. The project delivered a Reactor Trip System (RTS) implementation with full traceability from NRC Request for Proposals and IEEE standards through formal architecture specifications to verified software.
-rooms rely on analog technologies from the 1950s--60s. This technology incurs significant risk and
-cost compared to modern control systems. The NRC contracted Galois, a formal methods firm, to demonstrate that
-Model-Based Systems Engineering and formal methods could design, verify, and
-implement a complex protection system meeting regulatory criteria at a fraction
-of typical cost. The project delivered a Reactor Trip System (RTS)
-implementation with full traceability from NRC Request for Proposals and IEEE
-standards through formal architecture specifications to verified software.
 
 HARDENS employed formal methods tools and techniques across the verification
 hierarchy. High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
@@ -182,4 +160,4 @@ This section establishes the current state of practice by answering two Heilmeie
 
 \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. This gap between discrete-only formal methods and post-hoc hybrid verification prevents autonomous nuclear control with end-to-end correctness guarantees.
 
-Two imperatives emerge from this analysis. The economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. The technical imperative: current approaches verify either discrete logic or continuous dynamics, never both compositionally. These limitations define the research opportunity. Section 3 bridges this gap by establishing what makes this approach new and why it will succeed where prior work has failed.
+Two imperatives emerge. The economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. The technical imperative: current approaches verify either discrete logic or continuous dynamics, never both compositionally. These limitations define the research opportunity. Section 3 bridges this gap by establishing what makes this approach new and why it will succeed where prior work has failed.

3-research-approach/v3.tex

@@ -15,9 +15,9 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified either discrete switching logic or continuous control behavior, never both simultaneously. Continuous controllers rely on extensive simulation trials for validation; discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees of control system behavior despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
+Previous approaches verified either discrete switching logic or continuous control behavior, never both simultaneously. Continuous controllers rely on extensive simulation trials for validation; discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees despite consuming enormous resources. HAHACS bridges this 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: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques fail to handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode.
+Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques fail to handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active; continuous controllers govern plant behavior within each mode.
 
 Building a high-assurance hybrid autonomous control system (HAHACS) requires
 a mathematical description of the system. This work draws on
@@ -70,7 +70,7 @@ No prior work integrates these three techniques into a systematic design methodo
 \item The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility.
 \end{enumerate}
 
-We demonstrate feasibility on production control systems with realistic reactor models, not merely in principle.
+We demonstrate feasibility on production control systems with realistic reactor models, not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates this hybrid structure for a simplified reactor startup sequence.
 
 \begin{figure} 
   \centering
@@ -271,7 +271,7 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 \subsection{Discrete Controller Synthesis}
 
-Temporal logic specifications define what the system must do. Reactive synthesis determines how to implement those requirements. 
+Temporal logic specifications define what the system must do. Reactive synthesis determines how to implement those requirements, automating the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. 
 
 With system requirements defined as temporal logic specifications, reactive synthesis builds the discrete control system. Reactive synthesis automates the creation of reactive programs from temporal logic specifications—programs that take an input for a given state and produce
 an output. Our systems fit this model: the current discrete state and
@@ -305,7 +305,7 @@ Reactive synthesis has proven successful in robotics, avionics, and industrial c
 
 Reactive synthesis produces a provably correct discrete controller from operating procedures—an automaton that determines when to switch between modes. But hybrid control requires more than correct mode switching; the continuous dynamics executing within each discrete mode must also be verified to ensure the complete system behaves correctly.
 
-This subsection describes the continuous control modes that execute within each discrete state and explains how they verify against requirements imposed by the discrete layer. The verification approach depends on control objectives. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
+This subsection describes the continuous control modes executing within each discrete state and explains how they verify against requirements imposed by the discrete layer. The verification approach depends on control objectives. We classify modes 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. Model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers design continuous controllers using standard control theory techniques. Our contribution provides the verification framework confirming that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
@@ -510,7 +510,7 @@ safety margins will matter more than performance during emergency shutdown.
 
 \subsection{Industrial Implementation}
 
-The complete methodology—procedure formalization, discrete synthesis, and continuous verification across three mode types—must now be validated on realistic systems using industrial-grade hardware to demonstrate practical feasibility and advance from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5).
+The complete methodology—procedure formalization, discrete synthesis, and continuous verification across three mode types—provides a theoretical framework for hybrid control synthesis. Demonstrating practical feasibility requires validation on realistic systems using industrial-grade hardware, advancing from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5).
 This research will leverage the University of Pittsburgh Cyber Energy Center's
 partnership with Emerson to implement and test the HAHACS methodology on
 production control equipment. Emerson's Ovation distributed control system is widely deployed
@@ -546,7 +546,7 @@ This section establishes the research methodology by answering two critical Heil
 
 \textbf{Why will this approach succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the approach formalizes existing structure rather than imposing artificial abstractions. Second, mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility.
 
-The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. Establishing what will be done and why it will work leaves one critical question unanswered: \textit{how will success be measured?} Section 4 addresses this through Technology Readiness Level advancement, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation (TRL 3) through integrated simulation (TRL 4) to hardware-in-the-loop testing (TRL 5).
+The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. What will be done and why it will work have been established. One critical question remains: \textit{how will success be measured?} Section 4 addresses this through Technology Readiness Level advancement, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation (TRL 3) through integrated simulation (TRL 4) to hardware-in-the-loop testing (TRL 5).
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -1,10 +1,8 @@
 \section{Metrics for Success}
 
-\textbf{How do we measure success?} This research advances through
+\textbf{How do we measure success?} This research advances through Technology Readiness Levels, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
-Technology Readiness Levels, 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. This section first explains why TRL advancement provides the most appropriate success metric, then defines specific criteria for each level from TRL 3 through 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 for this work, bridging the gap between academic proof-of-concept and practical deployment. This section explains why, then defines specific criteria for each level from TRL 3 through TRL 5.
 
 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. Only TRLs measure both simultaneously.
 Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while

5-risks-and-contingencies/v1.tex

@@ -1,9 +1,6 @@
 \section{Risks and Contingencies}
 
-Every research plan rests on assumptions. When those assumptions prove false, research must adapt. Four primary risks 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 and
+\textbf{What could prevent success?} Every research plan rests on assumptions. When those assumptions prove false, research must adapt. Four primary risks 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 and contingency plans that preserve research value even when core assumptions prove false. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment.
-contingency plans that preserve research value even when core assumptions prove
-false. The staged project structure ensures that partial success yields
-publishable results while clearly identifying remaining barriers to deployment.
 
 \subsection{Computational Tractability of Synthesis}
 

6-broader-impacts/v1.tex

@@ -10,16 +10,9 @@ Deploying SMRs at datacenter sites minimizes transmission losses and
 eliminates emissions. However, nuclear power
 economics at this scale demand careful attention to operating costs.
 
-The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. Operations and maintenance represents a substantial component of this figure. The EIA
+The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. Operations and maintenance represents a substantial component. The EIA estimates that fixed O\&M costs alone account for \$16.15 per megawatt-hour, with additional variable O\&M costs embedded in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent approximately 23--30\% of the total levelized cost of electricity, translating to \$21--28 billion annually for projected datacenter demand.
-estimates that fixed O\&M costs alone account for \$16.15 per megawatt-hour,
-with additional variable O\&M costs embedded in fuel and operating
-expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent
-approximately 23--30\% of the total levelized cost of electricity, translating
-to \$21--28 billion annually for projected datacenter demand.
 
-\textbf{What difference will it make?} This research directly addresses the
+\textbf{What difference will it make?} This research directly addresses the \$21--28 billion annual O\&M cost challenge through high-assurance autonomous control, making small modular reactors economically viable for datacenter power.
-\$21--28 billion annual O\&M cost challenge through high-assurance autonomous
-control, making small modular reactors economically viable for datacenter power.
 
 Current nuclear operations require full control room staffing for each reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output, which makes per-megawatt costs prohibitive. These staffing requirements drive the economic challenge that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal
 specifications automates routine operational sequences that currently require

8-schedule/v1.tex

@@ -1,11 +1,6 @@
 \section{Schedule, Milestones, and Deliverables}
 
-\textbf{How long will it take?} This research will be conducted over six
+\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.
-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