Editorial pass: tactical, operational, and strategic improvements

Pass 1 (Tactical): Sentence-level improvements using Gopen principles
- Strengthened verbs and eliminated wordiness
- Converted passive to active voice where clearer
- Improved topic-stress positioning (old→new info flow)
- Enhanced sentence clarity and directness

Pass 2 (Operational): Paragraph and section flow
- Improved transitions between subsections
- Eliminated redundant transition phrases
- Enhanced coherence within sections
- Streamlined section introductions

Pass 3 (Strategic): Heilmeier catechism alignment
- Clarified 'What is new?' statements
- Strengthened 'What has been done?' / 'What are the limits?' framing
- Ensured proper linkage between sections
- Aligned language with Heilmeier questions throughout

Key improvements:
- Removed unnecessary methodology/approach qualifiers
- Tightened economic argument in Broader Impacts
- Clarified verification gap in State of the Art
- Strengthened success criteria statements
- Enhanced document-level coherence

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,11 +1,10 @@
 % GOAL PARAGRAPH
-This research develops a methodology for creating autonomous control systems
-with mathematical guarantees of safe and correct behavior.
+This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Extensively trained operators manage nuclear reactor control 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: per-megawatt staffing costs significantly exceed those of conventional plants. This economic constraint threatens their viability. Autonomous control systems must therefore 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. 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
@@ -17,7 +16,7 @@ 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 three-stage methodology bridges this gap. First, we translate written
+Our methodology bridges this gap through 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

1-goals-and-outcomes/v1.tex

@@ -1,7 +1,7 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops a methodology for creating autonomous hybrid control
+This research develops autonomous hybrid control
 systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
@@ -11,13 +11,13 @@ 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 operators 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 their economic viability.
-The nuclear industry therefore needs autonomous control systems that manage complex
+The nuclear industry needs autonomous control systems that manage complex
 operational sequences safely without constant human supervision while providing
 assurance equal to or exceeding human-operated systems.
 
@@ -28,8 +28,7 @@ systems correct by construction.
 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 cannot handle continuous dynamics during transitions between modes.
-Control theory verifies continuous behavior but cannot prove correctness of discrete switching decisions. This gap between discrete
-and continuous verification prevents end-to-end correctness guarantees.
+Control theory verifies continuous behavior but cannot prove correctness of discrete switching decisions. This gap prevents end-to-end correctness guarantees.
 % Hypothesis
 Our approach closes this gap by synthesizing discrete mode transitions directly
 from written operating procedures and verifying continuous behavior between
@@ -87,7 +86,7 @@ If this research is successful, we will be able to do the following:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{The key innovation:} We unify discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
+\textbf{What is new:} We unify 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

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}. 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. 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}. 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.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -27,17 +27,17 @@ Protection Systems trip automatically on safety signals with millisecond
 response times, and engineered safety features actuate automatically on accident
 signals without operator action required.
 
-The division between automated and human-controlled functions reveals hybrid control's
-fundamental challenge. Highly automated systems handle reactor
+The division between automated and human-controlled functions reveals the
+fundamental challenge of hybrid control. Highly automated systems handle reactor
 protection---automatic trips on safety parameters, emergency core cooling
 actuation, containment isolation, and basic process
-control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
-however, retain control of strategic decision-making: power level changes,
+control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators
+retain control of strategic decision-making: power level changes,
 startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-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.
+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
@@ -48,7 +48,7 @@ and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
 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.
+of improvements in training and procedures, motivating 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
@@ -80,7 +80,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The previous two subsections identified the limits of current practice: procedures lack formal verification and human operators introduce persistent reliability issues. Formal methods offer an alternative path: 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.
+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}
 
@@ -186,8 +186,8 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-\textbf{What is the state of the art?} Current practice reveals a fundamental gap between capability and need. 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 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{The gap our work addresses:} 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 enables 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.

3-research-approach/v3.tex

@@ -15,12 +15,12 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control verified 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 and 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. 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.
 
-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. Discrete supervisory logic determines which control mode is active. Within each mode, continuous controllers govern plant behavior.
+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.
 
 Building a high-assurance hybrid autonomous control system (HAHACS) requires
-establishing a mathematical description of the system. This work draws on
+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
@@ -52,7 +52,7 @@ where:
 
 Creating a HAHACS requires constructing such a tuple together with proof artifacts demonstrating that 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 specific 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 entirely. 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: (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{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.
 
@@ -120,17 +120,17 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The preceding section established the mathematical framework for hybrid systems: the eight-tuple definition that formalizes discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism.
+The eight-tuple definition formalizes discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge. 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 is high-level and
+operational, and tactical. Strategic control represents high-level,
 long-term decision making for the plant. This level has objectives that 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 of control is the
-tactical level. This is the individual control of pumps, turbines, and
-chemistry. Tactical control has already been somewhat automated in nuclear power
-plants today, and is generally considered ``automatic control'' when autonomous.
+long, often spanning months or years. The lowest level is the
+tactical level: the individual control of pumps, turbines, and
+chemistry. Nuclear power
+plants today have already automated tactical control somewhat, generally considered ``automatic control'' when autonomous.
 These controls are almost always continuous systems with a direct impact on the
 physical state of the plant. Tactical control objectives include maintaining
 pressurizer level, maintaining core temperature, or adjusting reactivity with a
@@ -138,7 +138,7 @@ chemical shim.
 
 The operational control scope links these two extremes and represents the primary responsibility of human operators
 today. Operational control takes the current strategic objective and implements
-tactical control objectives to drive the plant toward strategic goals, thereby bridging high-level and low-level goals. 
+tactical control objectives to drive the plant toward strategic goals, bridging high-level and low-level goals. 
 
 Consider an example: a strategic goal may be to
 perform refueling at a certain time, while the tactical level of the plant is
@@ -146,11 +146,11 @@ 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 combination of the operational and
-tactical levels fundamentally forms a hybrid controller. The tactical level is
-the continuous evolution of the plant according to the control input and control
-law, while the operational level is a discrete state evolution that determines
-which tactical control law to apply. This operational level is precisely what we target for autonomous control.
+This structure reveals why the operational and
+tactical levels fundamentally form a hybrid controller. The tactical level represents
+continuous evolution of the plant according to the control input and control
+law, while the operational level represents discrete state evolution that determines
+which tactical control law to apply. We target this operational level for autonomous control.
 
 
 \begin{figure}
@@ -186,13 +186,13 @@ which tactical control law to apply. This operational level is precisely what we
 \end{figure}
 
 
-This operational control level is the main reason for the requirement of human
-operators in nuclear control today. The hybrid nature of this control system
-makes it difficult to prove that a controller will perform according to
+This operational control level is the main reason human
+operators are required in nuclear control today. The hybrid nature of this control system
+makes it difficult to prove a controller will perform according to
 strategic requirements; unified infrastructure for building and verifying
-hybrid systems does not currently exist. Humans have been used for this layer
+hybrid systems does not currently exist. Humans fill this layer
 because their general intelligence provides a safe way to manage
-the hybrid nature of this system. These operators use prescriptive operating
+the hybrid nature of the system. These operators use prescriptive operating
 manuals to perform their control with strict procedures on what control to
 implement at a given time. These procedures are the key to the operational
 control scope.
@@ -200,8 +200,8 @@ control scope.
 Constructing a HAHACS leverages two key
 observations about current practice. First, operational scope control is
 effectively discrete control. Second, operating procedures describe the rules for implementing this control
-before implementation. Before
-constructing a HAHACS, we must completely describe its intended behavior. The
+before implementation. We must completely describe a HAHACS's intended behavior before
+constructing it. The
 behavior of any control system originates in requirements: statements about what
 the system must do, must not do, and under what conditions. For nuclear systems,
 these requirements derive from multiple sources including regulatory mandates,
@@ -249,7 +249,7 @@ eventually reaches operating temperature''), and response properties (``if
 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: by reducing required expert knowledge, we make these tools adoptable by the current workforce.
+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
 statements and consecutively refine them into well-posed specifications. We can
@@ -272,14 +272,13 @@ room for interpretation is a weakness that must be addressed.
 % 3. DISCRETE CONTROLLER SYNTHESIS
 % ----------------------------------------------------------------------------
 
-Having defined system requirements as temporal logic specifications, we now use
-them to build the discrete control system through reactive synthesis.
-Reactive synthesis is a field in computer science that deals with
-the automated creation of reactive programs from temporal logic specifications.
+With system requirements defined as temporal logic specifications, we now build
+the discrete control system through reactive synthesis.
+Reactive synthesis automates the creation of reactive programs from temporal logic specifications.
 A reactive program takes an input for a given state and produces
 an output. Our systems fit this model: the current discrete state and
 status of guard conditions form the input; the next discrete
-state is the output. 
+state forms the output. 
 
 Reactive synthesis solves the following problem: given an LTL formula $\varphi$
 that specifies desired system behavior, automatically construct a finite-state
@@ -291,7 +290,7 @@ controller can exist. This realizability check is itself valuable: an
 unrealizable specification indicates conflicting or impossible requirements in
 the original procedures. 
 
-Reactive synthesis offers a decisive advantage: producing the discrete automaton requires no human engineering of the 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 itself. This has two critical implications. First, it makes discrete controller creation tractable. 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 focus their effort where it belongs: on specifying system behavior. This has two critical implications. First, it makes discrete controller creation tractable. The reasons the controller
 changes between modes can be traced back to the specification and thus to any
 requirements, providing a trace for liability and justification of system
 behavior. Second, discrete control decisions made by humans depend on the
@@ -317,11 +316,11 @@ according to operating procedures.
 
 \subsection{Continuous Control Modes}
 
-The previous subsection showed how to synthesize a provably correct discrete controller from operating procedures using reactive synthesis. This discrete controller determines when to switch between modes—but hybrid control requires more than discrete correctness. 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. 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. Three mode types—transitory, stabilizing, and expulsory—require different verification approaches. 
 
-This methodology's scope regarding continuous controller design requires clarification. This work verifies continuous controllers—it 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 make a similar assumption: continuous controllers can be designed 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.
+This methodology's scope regarding continuous controller design requires clarification. This work verifies continuous controllers—it 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 continuous controllers can be designed 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.
 
 The operational control scope defines go/no-go decisions that determine what
 kind of continuous control to implement. The entry or exit conditions of a
@@ -432,8 +431,8 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions. Stabilizing modes, the second type,
-maintain the system within a desired operating region indefinitely. They keep the system within a safe operating region rather than driving it toward an
+Transitory modes drive the system toward exit conditions. 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
 constant power level. Reachability analysis may not suit validation of stabilizing modes. Instead, we will use barrier certificates.
@@ -543,7 +542,7 @@ safety margins will matter more than performance during emergency shutdown.
 
 \subsection{Industrial Implementation}
 
-The previous subsections established the complete methodology: procedure formalization, discrete synthesis, and continuous verification across three mode types. This methodology must now be validated on realistic systems using industrial-grade hardware to demonstrate practical feasibility and advance from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5).
+The complete methodology—procedure formalization, discrete synthesis, and continuous verification across three mode types—must now be validated on realistic systems using industrial-grade hardware to demonstrate practical feasibility and advance from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5).
 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

@@ -7,14 +7,14 @@ prototype demonstration (TRL 5).
 This work begins at TRL 2--3 and aims to reach TRL 5—where
 system components operate successfully in a relevant laboratory environment.
 This section explains why TRL advancement provides the most appropriate success
-metric and defines specific criteria for achieving TRL 5.
+metric and defines specific criteria for TRL 5.
 
 Technology Readiness Levels provide the ideal success metric: they
 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 dimensions simultaneously.
+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
@@ -86,7 +86,7 @@ assumptions. This research succeeds if it achieves TRL 5 by demonstrating a
 complete autonomous hybrid controller with formal correctness guarantees
 operating on industrial control hardware through hardware-in-the-loop testing in
 a relevant laboratory environment. This establishes both theoretical validity
-and practical feasibility, proving that the methodology produces verified
+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.

5-risks-and-contingencies/v1.tex

@@ -4,8 +4,7 @@ This research relies on several critical assumptions that, if invalidated, requi
 scope adjustment or methodological revision. Four primary risks could prevent
 successful completion: computational tractability of
 synthesis and verification, complexity of the discrete-continuous interface,
-completeness of procedure formalization, and hardware-in-the-loop integration
-challenges. Each risk has associated early warning indicators and
+completeness of procedure formalization, and hardware-in-the-loop integration. Each risk has associated early warning indicators and
 contingency plans that preserve research value even if core assumptions prove
 false. The staged project structure ensures that partial success yields
 publishable results while clearly identifying remaining barriers to deployment.

6-broader-impacts/v1.tex

@@ -10,11 +10,11 @@ Deploying SMRs at datacenter sites minimizes transmission losses and
 eliminates emissions from hydrocarbon-based alternatives. Nuclear power
 economics at this scale, however, demand careful attention to operating costs.
 
-According to the U.S. Energy Information Administration's Annual Energy Outlook
-2022, advanced nuclear power entering service in 2027 is projected to cost
+The U.S. Energy Information Administration's Annual Energy Outlook
+2022 projects advanced nuclear power entering service in 2027 to 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 this demand were supplied by nuclear power,
+2030~\cite{eesi_datacenter_2024}. If nuclear power supplied this demand,
 the total annual cost of power generation would exceed \$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,
@@ -23,7 +23,7 @@ expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent
 approximately 23--30\% of the total levelized cost of electricity, translating
 to \$21--28 billion annually for projected datacenter demand.
 
-\textbf{What difference does it make?} This research directly addresses the
+\textbf{What difference will it make?} This research directly addresses the
 \$21--28 billion annual O\&M cost challenge through high-assurance autonomous
 control, making small modular reactors economically viable for datacenter power.