Editorial pass: tactical, operational, and strategic improvements

TACTICAL (sentence-level):
- Improved topic-stress positioning throughout (moved known info to sentence start, new info to stress position)
- Strengthened verb choices (replaced weak verbs with stronger alternatives)
- Fixed awkward passive constructions
- Improved sentence flow and readability

OPERATIONAL (paragraph/section):
- Enhanced transitions between subsections with connecting phrases
- Improved coherence within sections (esp. state-of-the-art formal methods transitions)
- Strengthened logical progression between major subsections

STRATEGIC (document-level):
- Reinforced Heilmeier catechism alignment at section boundaries
- Improved section-to-section linkages (sections 3→4, 4→5, 5→6)
- Made explicit connections between sections and their assigned Heilmeier questions
- Strengthened the narrative arc from methodology through metrics to risks to impact

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,7 +2,7 @@
 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. When operators switch between control objectives, plant conditions guide their decisions.
+Extensively trained operators manage nuclear reactors by following detailed written procedures. Plant conditions guide their decisions when they switch between control objectives.
 % Gap
 Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening 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.
 
@@ -24,11 +24,11 @@ checking identifies conflicts and ambiguities before implementation.
 Second, reactive synthesis generates deterministic automata that are 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 that 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 prove that mode transitions occur safely. Local verification of continuous modes
-without requiring global trajectory analysis across the entire hybrid system. An
+becomes possible without requiring global trajectory analysis across the entire hybrid system. This methodology is demonstrated on an
-Emerson Ovation control system demonstrates this methodology. 
+Emerson Ovation control system. 
 % Pay-off
-Autonomous control manages complex nuclear
+Autonomous control can then manage complex nuclear
 power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS

1-goals-and-outcomes/v1.tex

@@ -11,15 +11,15 @@ 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. When operators switch between different control modes, plant conditions and procedural guidance inform their decisions.
+manage reactor control. Plant conditions and procedural guidance inform their decisions when they switch between different control modes.
 % 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 that far
 exceed those of conventional plants, threatening economic viability.
-The nuclear industry needs autonomous control systems that manage complex
+The nuclear industry needs autonomous control systems that can manage complex
 operational sequences safely without constant human supervision while providing
-assurance equal to or exceeding human-operated systems.
+assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control
@@ -89,7 +89,7 @@ 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. This treatment enables independent
+as contracts that continuous controllers must satisfy, enabling independent
 verification of each layer while guaranteeing correct composition.
 
 % Outcome Impact

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

@@ -22,7 +22,7 @@ adjustment; manual control, where operators directly manipulate the reactor; and
 various intermediate modes. In typical pressurized water reactor operation, the
 reactor control system automatically maintains a floating average temperature
 and compensates for power demand changes through reactivity feedback loops
-alone. Safety systems, by contrast, already employ implemented automation. Reactor
+alone. Safety systems, by contrast, already employ automation. Reactor
 Protection Systems trip automatically on safety signals with millisecond
 response times, and engineered safety features actuate automatically on accident
 signals without requiring operator action.
@@ -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. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations. Procedures define what to do; human operators determine when and how to apply them. Even perfectly written procedures cannot eliminate human error.
+Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations. Procedures define what to do; human operators determine when and how to apply them. Even perfectly written 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
@@ -47,8 +47,8 @@ shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
 and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
 operator requires several years of training.
 
-Despite decades
+Human error persistently contributes to nuclear safety incidents despite decades
-of improvements in training and procedures, human error persistently contributes to nuclear safety incidents. This persistence motivates formal automated control with mathematical safety guarantees.
+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 departing from normal regulations during emergencies. The Three Mile
 Island (TMI) accident demonstrated how personnel error, design
@@ -58,11 +58,11 @@ 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
+flexibility and safety assurance remains unresolved—the person responsible for
 reactor safety often becomes the root cause of failures.
 
 Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of
-nuclear power plant events, versus approximately
+nuclear power plant events, compared to approximately
 20\% for equipment failures~\cite{WNA2020}. More significantly, poor safety management and safety
 culture—primarily human factors—caused
 all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and
@@ -80,7 +80,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Procedures lack formal verification. 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. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
+The limitations are now clear: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative approach: 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: The State of Formal Methods in Nuclear Control}
 
@@ -152,7 +152,7 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-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

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. 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.
+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 to formalize 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 by verifying discrete switching logic and continuous mode behavior separately, then composes them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode.
 
@@ -124,14 +124,14 @@ The eight-tuple hybrid automaton formalism provides a mathematical framework for
 
 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. This level has objectives that are
+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. The time scale at this level is
-long, often spanning months or years. The lowest level is the
+long, often spanning months or years. The lowest level—the
-tactical level: the individual control of pumps, turbines, and
+tactical level—controls individual components: pumps, turbines, and
 chemistry. Nuclear power
-plants today have already automated tactical control somewhat, generally considered ``automatic control'' when autonomous.
+plants today have already automated tactical control somewhat; such automation is generally considered ``automatic control.''
-These controls are almost always continuous systems with a direct impact on the
+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.
@@ -251,15 +251,14 @@ coolant pressure drops, the system initiates shutdown within bounded time'').
 
 We will use FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility is crucial for industrial feasibility: reducing required expert knowledge makes these tools adoptable by the current workforce.
 
-A key feature of FRET is the ability to start with logically imprecise
+FRET's key feature is its ability to start with logically imprecise
 statements and consecutively refine them into well-posed specifications. We can
 use this to our advantage by directly importing operating procedures and design
 requirements into FRET in natural language, then iteratively refining them into
-specifications for a HAHACS. This has two distinct benefits. First, it allows us
+specifications for a HAHACS. This approach provides two distinct benefits. First, it draws a direct link from design documentation to digital system
-to draw a direct link from design documentation to digital system
 implementation. Second, it clearly demonstrates where natural language documents
-are insufficient. These procedures may still be used by human operators, so any
+are insufficient. Human operators may still use these procedures, making any
-room for interpretation is a weakness that must be addressed.
+room for interpretation a weakness that must be addressed.
 
 (Some examples of where FRET has been used and why it will be successful here)
 %%% NOTES (Section 2):
@@ -292,7 +291,7 @@ controller can exist. This realizability check provides immediate value: an
 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 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. 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.
@@ -315,7 +314,7 @@ algorithms, strategic decisions always follow operating procedures exactly—no
 
 Reactive synthesis produces a provably correct discrete controller from operating procedures. This discrete controller determines when to switch between modes—but hybrid control requires more. The continuous dynamics executing within each discrete mode must also be verified to ensure the complete system behaves correctly.
 
-This subsection describes the continuous control modes that execute within each discrete state and explains how we verify they satisfy the requirements imposed by the discrete layer. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification approaches matched to their control objectives. 
+This subsection describes the continuous control modes that execute within each discrete state and explains how we verify they satisfy the requirements imposed by the discrete layer. The verification approach depends on control objectives. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
 
 This methodology's scope regarding continuous controller design requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers can design continuous controllers using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
@@ -433,7 +432,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 parallels Lyapunov functions for
-stability: rather than computing trajectories explicitly, we find a certificate
+stability: rather than computing trajectories explicitly, we seek 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
 barrier certificate condition requires:
@@ -476,7 +475,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations; expulsory modes handle off-nominal conditions. When the plant deviates from expected behavior, expulsory modes take over to ensure safety. These continuous controllers prioritize robustness over optimality. The control objective is to drive the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and controlled depressurization procedures.
+Transitory and stabilizing modes handle nominal operations under the assumption that plant dynamics match the design model. When the plant deviates from expected behavior—through component failures, sensor degradation, or unanticipated disturbances—expulsory modes take over to ensure safety. These continuous controllers prioritize robustness over optimality. The control objective is to drive the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and controlled depressurization procedures.
 
 Proving controller correctness through reachability and barrier certificates makes detecting physical failures straightforward. The controller cannot be incorrect for the nominal plant model. When an invariant is violated, the plant dynamics must have changed. The HAHACS identifies faults when continuous controllers violate discrete boundary conditions—a direct consequence of verified nominal control modes. Unexpected behavior implies off-nominal conditions.
 
@@ -559,7 +558,7 @@ This section answered two Heilmeier questions:
 
 \textbf{Why will it succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the methodology formalizes existing structure rather than imposing artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation.
 
-Having established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—Section 4 addresses the next Heilmeier question: how do we measure success? Technology Readiness Level advancement demonstrates both correctness and practical implementability.
+Having established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—the next question becomes: how do we measure success? Section 4 addresses this question by defining Technology Readiness Level advancement as the primary metric, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation to integrated hardware testing.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -14,7 +14,7 @@ explicitly measuring 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. Only 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
@@ -89,4 +89,4 @@ a relevant laboratory environment. This establishes both theoretical validity
 and practical feasibility, proving the methodology produces verified
 controllers implementable with current technology.
 
-TRL advancement provides clear success criteria, but reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research may stall at lower readiness levels. The next section identifies the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail.
+This section established how we measure success: TRL advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility. However, reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research may stall at lower readiness levels despite sound methodology. Section 5 addresses the Heilmeier question \textbf{What could prevent success?} by identifying the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail.

5-risks-and-contingencies/v1.tex

@@ -36,7 +36,7 @@ minimal viable startup sequence covering only cold shutdown to criticality to lo
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-Computational tractability addresses whether synthesis can complete within practical time bounds. A more fundamental challenge addresses the second critical assumption: whether boolean guard
+Computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint. The second risk is more fundamental: whether boolean guard
 conditions in temporal logic can map cleanly to continuous state boundaries required for mode
 transitions. This interface represents the fundamental challenge of hybrid
 systems: relating discrete switching logic to continuous dynamics. Temporal
@@ -150,4 +150,4 @@ quirks.
 
 This section addressed the Heilmeier question: \textbf{What could prevent success?} Four primary risks—computational tractability, discrete-continuous interface complexity, procedure formalization completeness, and hardware integration—each have 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 technical feasibility established and risks addressed, Section 6 examines the final Heilmeier questions: who cares about this work, why does it matter now, and what difference will it make?
+With technical feasibility established through the methodology (Section 3), success metrics defined (Section 4), and risks addressed with contingency plans (Section 5), the research plan is complete from a technical perspective. Section 6 now addresses the remaining Heilmeier questions that establish broader impact: \textbf{Who cares?} \textbf{Why now?} \textbf{What difference will it make?}

6-broader-impacts/v1.tex

@@ -38,7 +38,7 @@ reactors rather than manually controlling individual units.
 The correct-by-construction methodology is critical for this transition.
 Traditional automation approaches cannot provide sufficient safety guarantees
 for nuclear applications, where regulatory requirements and public safety
-concerns demand the highest levels of assurance. Formally verifying both the
+concerns demand the highest levels of assurance. By formally verifying both the
 discrete mode-switching logic and the continuous control behavior, this research
 will produce controllers with mathematical proofs of correctness. These
 guarantees enable automation to safely handle routine operations---startup