Multi-level editorial pass: tactical (Gopen), operational (flow), strategic (Heilmeier)

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,18 +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, switching between control objectives based on plant conditions.
+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: 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.
+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.
 
 % APPROACH PARAGRAPH Solution
 Formal methods from computer science combine with control theory to build hybrid control systems correct by construction. 
 % Rationale
-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. 
+Hybrid systems mirror operator decision-making: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when transitions involve continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. 
 % 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 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. 
+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, then reachability analysis verifies them. Continuous modes classify by transition objectives. Assume-guarantee contracts and barrier certificates prove safe mode transitions, enabling local verification of continuous modes without global trajectory analysis across the entire hybrid system. An Emerson Ovation control system demonstrates the methodology. 
 % Pay-off
-This autonomous control approach manages complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
+This autonomous control approach manages complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints that threaten 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

@@ -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
-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.
+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
-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.
+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.
 
 % 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 discrete switching correctness. 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 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.
 % Hypothesis
-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. 
+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. 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.
@@ -82,13 +82,13 @@ 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. The following sections systematically answer the Heilmeier Catechism questions that define this research: 
+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:
 \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 where prior work has not?
+  \item \textbf{Section 3 (Research Approach):} What is new? Why will it succeed where prior work has failed?
   \item \textbf{Section 4 (Metrics for Success):} How do we measure success?
   \item \textbf{Section 5 (Risks and Contingencies):} What could prevent success?
   \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}
-This structure ensures each section explicitly addresses its assigned questions while building toward a complete research plan.
+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

@@ -4,7 +4,7 @@
 
 \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 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 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 +21,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 additional 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. The second pillar of current practice—human operators executing these procedures—introduces additional 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
@@ -33,14 +33,14 @@ operator requires several years of training.
 
 Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile
 Island (TMI) accident demonstrated how personnel error, design
-deficiencies, and component failures can combine to cause disaster. Operators
+deficiencies, and component failures combine to cause disaster. Operators
 misread confusing and contradictory indications, then shut off the emergency water
 system~\cite{Kemeny1979}. The President's Commission on TMI identified a
 fundamental ambiguity: placing responsibility for safe power plant operations on
 the licensee without formally verifying that operators can fulfill this
 responsibility does not guarantee safety. This tension between operational
 flexibility and safety assurance remains unresolved. The person responsible for
-reactor safety often becomes the root cause of failures.
+reactor safety often becomes the root cause of failure.
 
 Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events, compared to approximately 20\% for equipment failures~\cite{WNA2020}. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
 of 190 events at Chinese nuclear power plants from
@@ -58,7 +58,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 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. The following subsections examine why.
+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.
 
 \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control}
 

3-research-approach/v3.tex

@@ -15,7 +15,7 @@
 % ----------------------------------------------------------------------------
 % 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. 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; continuous controllers govern plant behavior within each mode.
 
@@ -52,7 +52,7 @@ where:
 
 Creating a HAHACS requires constructing this tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new in this research?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. This work composes them into a complete methodology for hybrid control synthesis through three key innovations:
+\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. This work composes them into a complete methodology for hybrid control synthesis through three key innovations:
 
 \begin{enumerate}
 \item \textbf{Contract-based decomposition:} Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of global hybrid system verification.
@@ -150,15 +150,14 @@ 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
-perform refueling at a certain time, while the tactical level of the plant is
+perform refueling at a certain time. The tactical level currently maintains core temperature. The operational
-currently focused on maintaining a certain 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
 tactical levels fundamentally form a hybrid controller. The tactical level represents
-continuous plant evolution according to the control input and control
+continuous plant evolution according to control input and control
-law; the operational level represents discrete state evolution that determines
+law. The operational level represents discrete state evolution that determines
 which tactical control law applies. This operational level becomes the target for autonomous control.
 
 
@@ -362,12 +361,12 @@ tools matched to its control objective. Transitory modes drive the plant between
 
 Transitory modes move the plant from one discrete operating condition to another. Their purpose is to execute transitions: start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers.
 
-The control objective for a transitory mode can be stated formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
+We can state the control objective for a transitory mode formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
 \[
 \forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \mathcal{X}_{exit}
 \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
 \]
-That is, from any valid entry state, the trajectory must eventually reach the
+From any valid entry state, the trajectory must eventually reach the
 exit condition without ever leaving the safe region.
 
 Reachability analysis provides the natural verification tool for transitory modes.
@@ -540,13 +539,13 @@ of transferring technology directly to industry with a direct collaboration in
 this research, while getting an excellent perspective of how our research
 outcomes can align best with customer needs.
 
-This section establishes the research methodology by answering two critical Heilmeier questions:
+This section answers two critical Heilmeier questions:
 
 \textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional architecture for hybrid control synthesis. Three innovations distinguish this approach: 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.
 
 \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. 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).
+The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. Sections 2 and 3 have established what has been done, what is new, and why it will succeed. 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

@@ -79,6 +79,6 @@ a relevant laboratory environment. This establishes both theoretical validity
 and practical feasibility, proving the methodology produces verified
 controllers implementable with current technology.
 
-This section establishes success criteria by answering the Heilmeier question \textbf{How do we measure success?} Technology Readiness Level advancement from 2--3 to 5 provides the answer: we measure success by demonstrating both theoretical correctness and practical feasibility through progressively integrated validation. TRL 3 proves component-level correctness, TRL 4 demonstrates system-level integration in simulation, and TRL 5 validates hardware implementation in a relevant environment. Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology.
+This section establishes success criteria by answering the Heilmeier question: \textbf{How do we measure success?} Technology Readiness Level advancement from 2--3 to 5 provides the answer. We measure success by demonstrating both theoretical correctness and practical feasibility through progressively integrated validation. TRL 3 proves component-level correctness. TRL 4 demonstrates system-level integration in simulation. TRL 5 validates hardware implementation in a relevant environment. Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology.
 
-However, reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research could stall at lower readiness levels despite sound methodology. Section 5 addresses the complementary Heilmeier question—\textbf{What could prevent success?}—by identifying primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail.
+However, reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research could stall at lower readiness levels despite sound methodology. Section 5 addresses the complementary Heilmeier question—\textbf{What could prevent success?}—by identifying primary risks, establishing early warning indicators, and defining contingency plans that preserve research value even when core assumptions fail.

6-broader-impacts/v1.tex

@@ -1,6 +1,6 @@
 \section{Broader Impacts}
 
-\textbf{Who cares? Why now? What difference will it make?} 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.
+\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
 economic challenge. Recent interest in powering artificial intelligence