Editorial pass: Gopen sentence structure + paragraph flow + Heilmeier alignment

TACTICAL (sentence-level):
- Improved issue-point positioning and topic-stress
- Shortened compound sentences for clarity
- Strengthened verb choices (active over passive)
- Enhanced topic strings for better flow

OPERATIONAL (paragraph/section):
- Added transition sentences between subsections
- Improved coherence within sections
- Clarified connections between ideas
- Enhanced paragraph-to-paragraph flow

STRATEGIC (document-level):
- Tightened Heilmeier question answers in each section
- Strengthened 'Who cares? Why now?' in Broader Impacts
- Improved global coherence across sections
- Ensured section summaries clearly answer assigned questions

1-goals-and-outcomes/research_statement_v1.tex

@@ -4,12 +4,12 @@ This research develops autonomous control systems with mathematical guarantees o
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear reactors require extensively trained operators who 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, threatening economic viability. These reactors need autonomous control systems that safely manage complex operational sequences without constant supervision—systems that 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 can manage complex operational sequences without constant supervision—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 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 but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. 
+Hybrid systems mirror how operators work: 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. Neither approach provides end-to-end correctness guarantees for hybrid systems.
 % Hypothesis and Technical Approach
 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. 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, which reachability analysis then verifies. Continuous modes classify by transition objectives: 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. An Emerson Ovation control system demonstrates the methodology. 
 % Pay-off

1-goals-and-outcomes/v1.tex

@@ -8,14 +8,14 @@ Nuclear power plants require the highest levels of control system reliability. C
 % Known information
 Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements. These operators switch between control modes based on plant conditions and procedural guidance.
 % Gap
-This reliance on human operators prevents autonomous control 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 that provide assurance equal to or exceeding human operators.
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—if they provide assurance equal to or exceeding human operators.
 
 % APPROACH PARAGRAPH Solution
 This research combines formal methods 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 when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. No existing approach provides end-to-end correctness guarantees for both layers.
 % Hypothesis
-This approach closes the gap by synthesizing discrete mode transitions directly from written operating procedures and verifying 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 by synthesizing discrete mode transitions directly from written operating procedures and verifying 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. 
 
 The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation
 requirements.
@@ -68,7 +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. 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.
+\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.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from

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

@@ -4,7 +4,9 @@
 
 \subsection{Current Reactor Procedures and Operation}
 
-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 confirms that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+Understanding the limits of current practice requires understanding what current practice is. 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 procedure 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 confirms 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
@@ -21,7 +23,7 @@ The division between automated and human-controlled functions reveals the fundam
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development—this represents only half the reliability challenge. The second pillar of current practice—human operators executing these procedures—introduces reliability limitations independent of procedure quality. Procedures define what to do; human operators determine when and how. Even perfect procedures cannot eliminate human error.
+Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Even perfect procedures cannot guarantee safe operation if humans execute them imperfectly. The second pillar of current practice—human operators executing these procedures—introduces reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how. Even perfect procedures cannot eliminate human error.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -56,7 +58,7 @@ 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 that four decades of training improvements have failed to eliminate. Formal methods offer an alternative—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 that four decades of training improvements have failed to eliminate. If training and procedural improvements cannot solve these problems, what can? 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. Two approaches illustrate this gap: HARDENS verified discrete logic without continuous dynamics, while differential dynamic logic handles hybrid verification only post-hoc. The following subsections examine each approach and its limitations.
 
@@ -66,7 +68,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 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.
+HARDENS addressed a fundamental dilemma: existing U.S. nuclear control rooms rely on analog technologies from the 1950s--60s. These technologies 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.
 
 HARDENS employed formal methods tools and techniques across the verification
 hierarchy. High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
@@ -158,6 +160,6 @@ This section establishes the current state of practice by answering two Heilmeie
 
 \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 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.
+\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 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 these limitations. 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 from these limitations. Economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical imperative: current approaches lack compositional verification for hybrid systems. 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,13 @@
 % ----------------------------------------------------------------------------
 % 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 despite consuming enormous resources. This work bridges the 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. 
 
-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.
+This work bridges the gap by composing formal methods from computer science with control-theoretic verification. Reactor operations formalize 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. Continuous controllers govern plant behavior within each mode.
 
 Building a high-assurance hybrid autonomous control system requires
 a mathematical description of the system. This work draws on
@@ -136,29 +140,17 @@ This work demonstrates feasibility on production control systems with realistic
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The hybrid automaton formalism defined above provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism.
+The hybrid automaton formalism defined above provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. But where do these formal descriptions come from? This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism.
 
-Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making for the plant. Objectives at this level are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. These decisions span months or years. The lowest level—the
+Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making for the plant. Objectives at this level are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. These decisions span months or years. 
-tactical level—controls individual components: pumps, turbines, and
+
-chemistry. Nuclear power
+The lowest level—the tactical level—controls individual components: pumps, turbines, and chemistry. Nuclear power plants today have already automated tactical control somewhat. Such automation is generally considered ``automatic control.'' These controls are almost always continuous systems with direct impact on the physical state of the plant. Tactical control objectives include maintaining pressurizer level, maintaining core temperature, or adjusting reactivity with a chemical shim.
-plants today have already automated tactical control somewhat; such automation is generally considered ``automatic control.''
-These controls are almost always continuous systems with direct impact on the
-physical state of the plant. Tactical control objectives include maintaining
-pressurizer level, maintaining core temperature, or adjusting reactivity with a
-chemical shim.
 
 The operational control scope links these two extremes, representing the primary responsibility of human operators today. Operational control takes strategic objectives and implements tactical control sequences to achieve them, bridging high-level goals with low-level execution. 
 
-Consider an example: a strategic goal may be to
+Consider an example: a strategic goal may be 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. 
-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. 
 
-This structure reveals why the operational and
+This structure reveals why the operational and tactical levels fundamentally form a hybrid controller. The tactical level represents continuous plant evolution according to control input and control law. The operational level represents discrete state evolution that determines which tactical control law applies. This operational level becomes the target for autonomous control.
-tactical levels fundamentally form a hybrid controller. The tactical level represents
-continuous plant evolution according to control input and control
-law. The operational level represents discrete state evolution that determines
-which tactical control law applies. This operational level becomes the target for autonomous control.
 
 
 \begin{figure}
@@ -270,7 +262,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, automating the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. 
+Temporal logic specifications define what the system must do. The next question is how to implement those requirements. Reactive synthesis provides the answer, 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
@@ -281,10 +273,9 @@ Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$
 unrealizable specification indicates conflicting or impossible requirements in
 the original procedures, catching errors before implementation. 
 
-Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The resultant automaton is correct by construction, eliminating human error at the implementation stage entirely. Human designers can focus their effort where it belongs: on specifying system behavior rather than implementing switching logic. This shift has two critical implications. First, it provides complete traceability. The reasons the controller
+Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The resultant automaton is correct by construction, eliminating human error at the implementation stage entirely. Human designers can focus their effort where it belongs: on specifying system behavior rather than implementing switching logic. 
-changes between modes trace back through specifications to requirements, establishing clear liability and justification for system
+
-behavior. Second, it replaces probabilistic human judgment with deterministic guarantees. Human operators cannot eliminate error from discrete control decisions; humans are intrinsically fallible. By defining system behavior using temporal logics and synthesizing the controller using deterministic
+This shift has two critical implications. First, it provides complete traceability. The reasons the controller changes between modes trace back through specifications to requirements, establishing clear liability and justification for system behavior. Second, it replaces probabilistic human judgment with deterministic guarantees. Human operators cannot eliminate error from discrete control decisions. Humans are intrinsically fallible. By defining system behavior using temporal logics and synthesizing the controller using deterministic algorithms, strategic decisions always follow operating procedures exactly—no exceptions, no deviations, no human factors.
-algorithms, strategic decisions always follow operating procedures exactly—no exceptions, no deviations, no human factors.
 
 The synthesized automaton translates directly to executable code through standard compilation techniques. Each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees: the implemented code is correct by construction because the automaton it derives from was synthesized to satisfy the temporal logic specifications.
 
@@ -302,7 +293,7 @@ Reactive synthesis has proven successful in robotics, avionics, and industrial c
 
 \subsection{Continuous Control Modes}
 
-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.
+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 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. 
 
@@ -410,9 +401,9 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions. Stabilizing modes do the opposite: they maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. 
+Transitory modes drive the system toward exit conditions. Stabilizing modes do the opposite: they 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. 
 
-This different control objective requires a different verification approach. Reachability analysis answers "can the system reach a target?" Stabilizing modes ask instead "does the system stay within bounds?" Barrier certificates provide the appropriate tool.
+Reachability analysis answers "can the system reach a target?" Stabilizing modes ask instead "does the system stay within bounds?" Barrier certificates provide the appropriate tool.
 Barrier certificates analyze the dynamics of the system to determine whether
 flux across a given boundary exists. They evaluate whether any trajectory leaves
 a given boundary. This definition exactly matches what defines the validity of a
@@ -513,7 +504,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—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).
+The complete methodology—procedure formalization, discrete synthesis, and continuous verification across three mode types—provides a theoretical framework for hybrid control synthesis. Theory alone, however, does not demonstrate practical feasibility. Validation on realistic systems using industrial-grade hardware is required, 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

4-metrics-of-success/v1.tex

@@ -4,7 +4,7 @@
 
 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. TRLs measure both simultaneously.
+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. TRLs measure both simultaneously.
 
 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.
 

5-risks-and-contingencies/v1.tex

@@ -4,15 +4,7 @@
 
 \subsection{Computational Tractability of Synthesis}
 
-The first major assumption is that formalized startup procedures will yield
+The first major assumption is that formalized startup procedures will yield automata small enough for efficient synthesis and verification. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states. Such large automata would require synthesis times exceeding days or weeks, preventing demonstration of the complete methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives.
-automata small enough for efficient synthesis and verification. Reactive
-synthesis scales exponentially with specification complexity, which means temporal logic specifications derived from complete startup procedures may
-produce automata with thousands of states. Such large automata would require
-synthesis times exceeding days or weeks, preventing demonstration of the
-complete methodology within project timelines. Reachability analysis for
-continuous modes with high-dimensional state spaces may similarly prove
-computationally intractable. Either barrier would constitute a fundamental
-obstacle to achieving research objectives.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets
@@ -28,19 +20,9 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-While computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint—the second risk proves more fundamental: whether boolean guard
+While computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint—the second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
-conditions in temporal logic can map cleanly to continuous state boundaries required for mode
+
-transitions. This interface represents the fundamental challenge of hybrid
+This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction, making synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. The risk extends beyond static interface definition to dynamic behavior across transitions. Barrier certificates may fail to exist for proposed transitions. Continuous modes may be unable to guarantee convergence to discrete transition boundaries.
-systems: relating discrete switching logic to continuous dynamics. Temporal
-logic operates on boolean predicates, while continuous control requires
-reasoning about differential equations and reachable sets. Guard conditions
-requiring complex nonlinear predicates may resist boolean abstraction, making
-synthesis intractable. Continuous safety regions that cannot be expressed as
-conjunctions of verifiable constraints would similarly create insurmountable
-verification challenges. The risk extends beyond static interface definition to
-dynamic behavior across transitions: barrier certificates may fail to exist for
-proposed transitions, or continuous modes may be unable to guarantee convergence
-to discrete transition boundaries.
 
 Early indicators of interface formalization problems would appear during both
 synthesis and verification phases. Guard conditions requiring complex nonlinear

6-broader-impacts/v1.tex

@@ -2,13 +2,7 @@
 
 \textbf{Who cares? Why now? What difference will it make?} These three Heilmeier questions connect technical methodology to economic and societal impact. Three stakeholder groups face the same economic constraint: the nuclear industry, datacenter operators, and clean energy advocates. All confront high operating costs driven by staffing requirements. AI infrastructure demands, growing exponentially, have made this constraint urgent.
 
-Nuclear power presents both a compelling application domain and an urgent
+Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence infrastructure has renewed focus on small modular reactors (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. Deploying SMRs at datacenter sites minimizes transmission losses and eliminates emissions. However, nuclear power economics at this scale demand careful attention to operating costs.
-economic challenge. Recent interest in powering artificial intelligence
-infrastructure has renewed focus on small modular reactors (SMRs), particularly
-for hyperscale datacenters requiring hundreds of megawatts of continuous power.
-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: 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 total levelized cost, translating to \$21--28 billion annually for projected datacenter demand.
 
@@ -60,9 +54,9 @@ adoption across critical infrastructure.
 
 This section establishes impact by answering three critical Heilmeier questions:
 
-\textbf{Who cares?} The nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Any organization operating staffing-intensive safety-critical systems faces similar economic pressures.
+\textbf{Who cares?} Three stakeholder groups face the same constraint. The nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive. All three groups need autonomous control with safety guarantees.
 
-\textbf{Why now?} Two forces converge to make this research urgent. First, exponentially growing AI infrastructure demands have created immediate need for economical nuclear power at datacenter scale. Second, formal methods tools have matured to where compositional hybrid verification has become computationally achievable—what was theoretically possible but practically intractable a decade ago is now feasible.
+\textbf{Why now?} Two forces converge to make this research urgent. First, exponentially growing AI infrastructure demands have created immediate need for economical nuclear power at datacenter scale. Projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. Second, formal methods tools have matured to where compositional hybrid verification has become computationally achievable—what was theoretically possible but practically intractable a decade ago is now feasible.
 
 \textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier by enabling autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure.