Editorial pass: tactical/operational/strategic improvements

Three-pass editorial review following Gopen's Sense of Structure:

TACTICAL (sentence-level):
- Improved topic-stress positioning for clearer emphasis
- Tightened topic strings for better paragraph coherence
- Converted passive constructions to active voice
- Strengthened verb choice throughout

OPERATIONAL (paragraph/section):
- Added explicit transitions between major subsections
- Improved flow from state-of-art → research approach
- Clarified relationships between transitory/stabilizing/expulsory modes
- Strengthened section-to-section bridges

STRATEGIC (document-level):
- Made Heilmeier Catechism questions more explicit in Broader Impacts
- Clarified novelty claims in Research Approach (three innovations)
- Strengthened mapping of document structure to Heilmeier questions
- Improved strategic framing of risks as preserving research value

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,9 +2,9 @@
 This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Extensively trained operators manage nuclear reactors by following detailed written procedures. Plant conditions guide their decisions when they switch between control objectives.
+Extensively trained operators manage nuclear reactors by following detailed written procedures. When operators switch between control objectives, plant conditions guide their decisions.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening their viability. Autonomous control systems must 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: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening their viability. To address this challenge, autonomous control systems must manage complex operational sequences safely—without constant supervision—while providing assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods from computer science with control theory to
@@ -16,15 +16,15 @@ generate provably correct switching logic but cannot handle continuous dynamics
 during transitions. Control theory verifies continuous behavior but
 cannot prove discrete switching correctness. 
 % Hypothesis and Technical Approach
-Our methodology bridges this gap through three stages. First, we translate written
+Our methodology bridges this gap in three stages. First, we translate written
 operating procedures 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.
+checking then identifies conflicts and ambiguities before implementation.
 Second, reactive synthesis generates deterministic automata provably
 correct by construction.
 Third, we design continuous controllers for each discrete mode using standard
-control theory and verify them using reachability analysis. Continuous modes are classified by their transition objectives. Assume-guarantee contracts and barrier certificates prove mode transitions occur safely. This approach enables local verification of continuous modes
+control theory and verify them using reachability analysis. We classify continuous modes by their transition objectives. Assume-guarantee contracts and barrier certificates then prove mode transitions occur safely. This approach enables local verification of continuous modes
 without requiring global trajectory analysis across the entire hybrid system. An
 Emerson Ovation control system demonstrates this methodology. 
 % Pay-off

1-goals-and-outcomes/v1.tex

@@ -11,7 +11,7 @@ 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. Plant conditions and procedural guidance inform their decisions when operators switch between different control modes.
+manage reactor control. When operators switch between different control modes, plant conditions and procedural guidance inform their decisions.
 % Gap
 This reliance on human operators prevents autonomous control and
 creates a fundamental economic challenge for next-generation reactor designs.
@@ -90,8 +90,8 @@ These three outcomes—procedure translation, continuous verification, and hardw
 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
+as contracts that continuous controllers must satisfy, enabling independent
-verification of each layer becomes possible while correct composition is guaranteed.
+verification of each layer while guaranteeing correct composition.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from
@@ -105,4 +105,4 @@ costs through increased autonomy. This research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the
 nuclear industry requires.
 
-The following sections answer the Heilmeier Catechism questions that define this research: Section 2 examines the state of the art, establishing what has been done and what remains impossible with current approaches. Section 3 presents our hybrid control synthesis methodology, demonstrating what is new and why it will succeed where prior work has not. Section 4 defines how we measure success through Technology Readiness Level advancement from analytical concepts to hardware demonstration. Section 5 identifies risks that could prevent success and establishes contingencies. Section 6 addresses who cares and why now: the economic imperative driving autonomous nuclear control. Section 7 provides the research schedule and deliverables.
+The following sections systematically answer the Heilmeier Catechism questions that define this research: Section 2 examines the state of the art, establishing what has been done and what remains impossible with current approaches. Section 3 presents our hybrid control synthesis methodology, demonstrating what is new and why it will succeed where prior work has not. Section 4 defines how we measure success through Technology Readiness Level advancement from analytical concepts to hardware demonstration. Section 5 identifies risks that could prevent success and establishes contingencies. Section 6 addresses who cares and why now, examining the economic imperative driving autonomous nuclear control and the broader impact on safety-critical systems. Section 7 provides the research schedule and deliverables, answering how long this work will take.

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

@@ -5,7 +5,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, and Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage scenarios. 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—not formal verification—form the basis of their development. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. This rigor, however, 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.
+provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Their development relies on expert judgment and simulator validation—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. However, 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
@@ -37,7 +37,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development. This subsection examines the second pillar of current practice: the human operators who execute these procedures. While procedures define what to do, human operators determine when and how to apply them—an approach that introduces fundamental reliability limitations.
+The previous subsection established that procedures lack formal verification despite rigorous development. This subsection examines the second pillar of current practice: the human operators who execute these procedures. While procedures define what to do, human operators determine when and how to apply them—an approach that introduces fundamental reliability limitations.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -61,12 +61,12 @@ responsibility does not guarantee safety. This tension between operational
 flexibility and safety assurance remains unresolved: the person responsible for
 reactor safety is often the root cause of failures.
 
-Multiple independent analyses converge on a striking statistic: 70--80\% of
+Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of
-nuclear power plant events are attributed to human error, versus approximately
+nuclear power plant events, versus approximately
-20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of
+20\% for equipment failures~\cite{WNA2020}. More significantly, poor safety management and safety
-all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and
+culture—primarily human factors—caused
-Fukushima Daiichi---has been identified as poor safety management and safety
+all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and
-culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis
+Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
 of 190 events at Chinese nuclear power plants from
 2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
 errors, while 92\% were associated with latent errors---organizational and
@@ -80,7 +80,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Procedures lack formal verification and human operators introduce persistent reliability issues. Formal methods offer an alternative: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
+The previous two subsections established that procedures lack formal verification and human operators introduce persistent reliability issues. Formal methods offer an alternative: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
 
 \subsubsection{HARDENS}
 
@@ -153,7 +153,7 @@ primary assurance evidence.
 
 \subsubsection{Sequent Calculus and Differential Dynamic Logic}
 
-HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. Other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). dL introduces two additional operators
+HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. Recognizing this gap, other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). dL introduces two additional operators
 into temporal logic: the box operator and the diamond operator. The box operator
 \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
 \(\alpha\) always remains within that region. In this way, it is a safety
@@ -188,6 +188,6 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. 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 does not 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. Closing this gap enables autonomous control that addresses the economic constraints threatening small modular reactor viability while maintaining the safety assurance the nuclear industry requires.
+\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. Closing this gap would enable autonomous control that addresses the economic constraints threatening small modular reactor viability while maintaining the safety assurance the nuclear industry requires.
 
-The next section presents our methodology for bridging this gap through compositional hybrid verification, establishing what is new and why it will succeed.
+Having established what has been done and where current approaches fall short, the next section presents our methodology for bridging this gap through compositional hybrid verification, establishing what is new and why it will succeed.

3-research-approach/v3.tex

@@ -15,7 +15,7 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control 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. Despite consuming enormous resources, neither method provides rigorous guarantees of control system behavior. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations using hybrid automata.
+Previous approaches to autonomous control 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 using 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—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations, where discrete supervisory logic determines which control mode is active and continuous controllers govern plant behavior within each mode.
 
@@ -24,8 +24,8 @@ a mathematical description of the system. This work draws on
 automata theory, temporal logic, and control theory. A hybrid system is a
 dynamical system with both continuous and discrete states. This proposal
 discusses continuous autonomous hybrid systems specifically—systems with no external input where continuous
-states do not change instantaneously when discrete states change. The continuous states are physical quantities that remain
+states do not change instantaneously when discrete states change. These continuous states are physical quantities that remain
-Lipschitz continuous. This nomenclature follows the Handbook on
+Lipschitz continuous. We follow the nomenclature from the Handbook on
 Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here
 for convenience:
 
@@ -50,11 +50,11 @@ where:
   \item $Inv$: safety invariants on the continuous dynamics
 \end{itemize}
 
-Creating a HAHACS requires constructing such a tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
+Creating a HAHACS requires constructing such a tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. The novelty lies in three innovations: (1) using discrete synthesis to define entry/exit/safety contracts that bound continuous verification, (2) classifying continuous modes by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, and (3) leveraging existing procedural structure to avoid global hybrid system analysis. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
+\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. The novelty lies in three innovations: First, we use discrete synthesis to define entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, we classify continuous modes by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, we leverage existing procedural structure to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
 
-\textbf{Why will it succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than imposing artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable. Each mode is verified against local contracts, keeping computational complexity bounded. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We are not proving feasibility in principle—we are demonstrating it on production control systems with realistic reactor models.
+\textbf{Why will it succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than imposing artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, keeping computational complexity bounded by verifying each mode against local contracts. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We are not proving feasibility in principle—we are demonstrating it on production control systems with realistic reactor models.
 
 \begin{figure} 
   \centering
@@ -431,7 +431,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions. Stabilizing modes
+Transitory modes drive the system toward exit conditions. In contrast, stabilizing modes
 maintain the system within a desired operating region indefinitely, keeping it within a safe operating region rather than driving it toward an
 exit condition. Examples
 include steady-state power operation, hot standby, and load-following at
@@ -443,7 +443,7 @@ stabilizing continuous control mode.
 
 Formally, a barrier certificate (or control barrier function) is a
 scalar function $B: \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward
-invariance of a safe set. The idea is analogous to Lyapunov functions for
+invariance of a safe set. The idea parallels Lyapunov functions for
 stability: rather than computing trajectories explicitly, we find a certificate
 function whose properties guarantee the desired behavior. For a safe set
 $\mathcal{C} = \{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$, the
@@ -487,8 +487,8 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations. Expulsory modes
+Transitory and stabilizing modes handle nominal operations. The third mode type, expulsory modes,
-handle off-nominal conditions.
+handles off-nominal conditions.
 
 When the plant deviates from expected behavior, expulsory modes take over. These
 continuous controllers ensure safety when failures occur. They are designed for robustness rather

4-metrics-of-success/v1.tex

@@ -14,7 +14,7 @@ explicitly measure the gap between academic proof-of-concept and practical
 deployment—precisely what this work aims to bridge. Academic metrics like
 papers published or theorems proved cannot capture practical feasibility.
 Empirical metrics like simulation accuracy or computational speed cannot
-demonstrate theoretical rigor. TRLs measure both simultaneously.
+demonstrate theoretical rigor. TRLs alone 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

5-risks-and-contingencies/v1.tex

@@ -16,7 +16,7 @@ automata small enough for efficient synthesis and verification. Reactive
 synthesis scales exponentially with specification complexity, creating the risk that
 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
+synthesis times exceeding days or weeks—preventing us from demonstrating 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
@@ -149,4 +149,4 @@ extensions, ensuring they address industry-wide practices rather than specific
 quirks.
 
 
-These risks and contingencies demonstrate that while the research faces real challenges, each has identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if assumptions prove invalid. With risks addressed, the next section examines broader impacts: who cares about this work and why it matters now.
+These risks and contingencies demonstrate that while the research faces real challenges, each has identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid: partial success yields publishable results that clearly identify remaining barriers to deployment. With risks addressed and contingencies established, the next section examines broader impacts: who cares about this work and why it matters now.

6-broader-impacts/v1.tex

@@ -11,11 +11,11 @@ eliminates emissions from hydrocarbon-based alternatives. Nuclear power
 economics at this scale, however, 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 to cost
+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}. If nuclear power supplied this demand,
+2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would
-the total annual cost of power generation would exceed \$92 billion. Within this
+generate total annual costs exceeding \$92 billion. Within this
 figure, 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
@@ -73,6 +73,12 @@ establish both the technical feasibility and regulatory pathway for broader
 adoption across critical infrastructure.
 
 
-These broader impacts answer the final Heilmeier questions: Who cares? The nuclear industry, datacenter operators, and anyone facing high operating costs from staffing-intensive safety-critical control. Why now? AI infrastructure demands have made nuclear economics urgent, and formal methods tools have matured to the point where compositional hybrid verification is achievable. What difference will it make? Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier while establishing a generalizable framework for safety-critical autonomous systems.
+These broader impacts answer the final Heilmeier questions: 
+
+\textbf{Who cares?} The nuclear industry, datacenter operators, and anyone facing high operating costs from staffing-intensive safety-critical control. 
+
+\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent, and formal methods tools have matured to the point where compositional hybrid verification is achievable. 
+
+\textbf{What difference will it make?} Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier while establishing a generalizable framework for safety-critical autonomous systems.
 
 The next section presents the timeline for achieving these outcomes through a structured 24-month research plan.