Editorial pass: tactical, operational, and strategic improvements

Pass 1 (Tactical/Sentence-level):
- Improved topic-stress positioning for clearer emphasis
- Shortened complex sentences for better readability
- Strengthened verb choices and reduced passive voice
- Eliminated unnecessary repetition
- Enhanced topic strings (subject consistency)

Pass 2 (Operational/Paragraph-Section):
- Smoothed transitions between paragraphs
- Removed redundant text in subsection openings
- Improved flow within sections

Pass 3 (Strategic/Document-level):
- Strengthened Heilmeier question linkages between sections
- Clarified section-to-section transitions
- Maintained overall argument coherence

Focus: clarity and impact over nitpicking. All edits preserve technical accuracy while improving readability.

1-goals-and-outcomes/v1.tex

@@ -6,14 +6,14 @@ This research develops autonomous hybrid control systems with mathematical guara
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release.
 % Known information
-Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements. These operators switch between control modes based on plant conditions and procedural guidance.
+Nuclear plant operations rely on extensively trained human operators. These operators follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
 % Gap
-This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—if they provide assurance equal to or exceeding that of human operators.
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants—a gap that threatens their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision, but only if they provide assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
 This research combines formal methods with control theory to build hybrid control systems correct by construction.
 % Rationale
-Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. No existing approach guarantees end-to-end correctness for both layers.
+Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Neither approach alone guarantees end-to-end correctness.
 % Hypothesis
 This approach closes the gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between transitions. Operating procedures formalize into logical specifications. Continuous dynamics verify against transition requirements. The result: autonomous controllers provably free from design defects. 
 
@@ -29,10 +29,10 @@ This approach produces three concrete outcomes:
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
     We develop a methodology for converting existing written operating
-    procedures into formal specifications that can be automatically synthesized
-    into discrete control logic. This process uses structured intermediate
-    representations to bridge natural language procedures and mathematical
-    logic.
+    procedures into formal specifications. Reactive synthesis tools then
+    automatically generate discrete control logic from these specifications.
+    Structured intermediate representations bridge natural language procedures
+    and mathematical logic.
     % Outcome
     Control system engineers generate verified mode-switching controllers
     directly from regulatory procedures without formal methods expertise,
@@ -68,7 +68,7 @@ This approach produces three concrete outcomes:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. This work establishes that bridge by treating discrete specifications as contracts that continuous controllers must satisfy, enabling independent verification of each layer while guaranteeing correct composition. Section 2 (State of the Art) examines why prior work has not achieved this integration. Section 3 (Research Approach) details how this integration will be accomplished.
+\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. This work establishes that bridge by treating discrete specifications as contracts that continuous controllers must satisfy. Independent verification of each layer becomes possible while guaranteeing correct composition. Section 2 (State of the Art) examines why prior work has not achieved this integration. Section 3 (Research Approach) details how this integration will be accomplished.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from

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

@@ -8,7 +8,7 @@ Current practice must be understood before its limits can be identified. This su
 
 Nuclear plant procedures form a hierarchy. Normal operating procedures govern routine operations. Abnormal operating procedures handle off-normal conditions. Emergency Operating Procedures (EOPs) manage design-basis accidents. Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 
 
-Procedure 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. Yet this rigor cannot provide formal verification of key safety properties. No mathematical proof confirms that procedures cover all possible plant states, that required actions complete within available timeframes, or that procedure-set transitions maintain safety invariants.
+Procedure 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. Yet this rigor cannot provide formal verification of key safety properties. No mathematical proof confirms that procedures cover all possible plant states. No proof verifies that required actions complete within available timeframes. No proof establishes that procedure-set transitions maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -25,7 +25,7 @@ The division between automated and human-controlled functions reveals the fundam
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. The other half emerges from procedure execution: even perfect procedures cannot guarantee safe operation when humans execute them imperfectly. The second pillar of current practice—human operators executing these procedures—introduces reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how. Perfect procedures cannot eliminate human error.
+Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. The other half emerges from procedure execution: even perfect procedures cannot guarantee safe operation when humans execute them imperfectly. Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how. Perfect procedures cannot eliminate human error.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -35,11 +35,7 @@ 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.
 
-Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile
-Island (TMI) accident demonstrated how personnel error, design
-deficiencies, and component failures combine to cause disaster. Operators
-misread confusing and contradictory indications, then shut off the emergency water
-system~\cite{Kemeny1979}. The President's Commission on TMI identified a
+Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster. Operators misread confusing and contradictory indications. They then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a
 fundamental ambiguity: placing responsibility for safe power plant operations on
 the licensee without formally verifying that operators can fulfill this
 responsibility does not guarantee safety. This tension between operational
@@ -60,7 +56,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Current practice reveals two critical limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. If training and procedural improvements cannot solve these problems, what can? Formal methods offer an alternative—mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. 
+Current practice reveals two critical limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. Training and procedural improvements cannot solve these problems. What can? Formal methods offer an alternative—mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. 
 
 Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems. This subsection examines two approaches that illustrate this gap: HARDENS, which verified discrete logic without continuous dynamics, and differential dynamic logic, which handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
 
@@ -164,4 +160,4 @@ This section establishes the current state of practice by answering two Heilmeie
 
 \textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This gap between discrete-only formal methods and post-hoc hybrid verification prevents autonomous nuclear control with end-to-end correctness guarantees.
 
-Two imperatives emerge from these limitations. Economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical imperative: current approaches lack compositional verification for hybrid systems. These limitations define the research opportunity. Section 3 bridges this gap by establishing what makes this approach new and why it will succeed where prior work has failed.
+Two imperatives emerge. Economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical imperative: current approaches lack compositional verification for hybrid systems. These limitations define the research opportunity. Section 3 addresses this gap by establishing what makes this approach new and why it will succeed where prior work has failed.

3-research-approach/v3.tex

@@ -15,13 +15,13 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees, despite consuming enormous resources. 
+Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees despite consuming enormous resources. 
 
-This work bridges the gap by composing formal methods from computer science with control-theoretic verification. Reactor operations formalize as hybrid automata.
+This work bridges the gap. It composes formal methods from computer science with control-theoretic verification. Reactor operations formalize as hybrid automata.
 
 Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics creates discontinuities in system behavior when discrete transitions change the governing vector field. Traditional verification techniques fail to handle this interaction directly. 
 
-Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active. Continuous controllers govern plant behavior within each mode.
+Our methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active. Continuous controllers govern plant behavior within each mode.
 
 Building a high-assurance hybrid autonomous control system requires
 a mathematical description of the system. This work draws on
@@ -140,7 +140,7 @@ This work demonstrates feasibility on production control systems with realistic
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The hybrid automaton formalism defined above provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. But where do these formal descriptions come from? This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. The key insight is that nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism through three control scopes: strategic, operational, and tactical.
+The hybrid automaton formalism provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. But where do these formal descriptions come from? This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure. This structure maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical.
 
 Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making for the plant. Objectives at this level are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. These decisions span months or years. 
 
@@ -186,7 +186,7 @@ This structure reveals why the operational and tactical levels fundamentally for
 \end{figure}
 
 
-This operational control level is the main reason nuclear control requires human operators. The hybrid nature of this control system makes proving controller performance against strategic requirements difficult. Unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature. These operators follow prescriptive operating manuals with strict procedures governing what control to implement at any given time. These procedures provide the key to the operational control scope.
+This operational control level is the main reason nuclear control requires human operators. The hybrid nature of this control system makes proving controller performance against strategic requirements difficult. Unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature. These operators follow prescriptive operating manuals. Strict procedures govern what control to implement at any given time. These procedures provide the key to the operational control scope.
 
 Constructing a HAHACS leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins. A HAHACS's intended behavior must be completely described before construction. Requirements define the behavior of any control system: statements about what
 the system must do, must not do, and under what conditions. For nuclear systems,
@@ -259,18 +259,15 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 \subsection{Discrete Controller Synthesis}
 
-Temporal logic specifications define what the system must do. The next question is how to implement those requirements. Reactive synthesis provides the answer, automating the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. 
+Temporal logic specifications define what the system must do. The next question is how to implement those requirements. Reactive synthesis provides the answer.
 
-With system requirements defined as temporal logic specifications, reactive synthesis builds the discrete control system. Reactive synthesis automates the creation of reactive programs from temporal logic specifications—programs that take an input for a given state and produce
-an output. Our systems fit this model: the current discrete state and
-status of guard conditions form the input, while the next discrete
-state forms the output. 
+Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. With system requirements defined as temporal logic specifications, reactive synthesis builds the discrete control system. Our systems fit this model: the current discrete state and status of guard conditions form the input, while the next discrete state forms the output. 
 
 Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ specifying desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller exists. 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 can focus their effort where it belongs: on specifying system behavior rather than implementing switching logic. 
+Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The resultant automaton is correct by construction. This eliminates 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.
 
@@ -454,9 +451,9 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-The first two mode types—transitory and stabilizing—handle nominal operations where plant dynamics match the design model. Expulsory modes handle the opposite case: when the plant deviates from expected behavior through component failures, sensor degradation, or unanticipated disturbances. 
+The first two mode types—transitory and stabilizing—handle nominal operations where plant dynamics match the design model. Expulsory modes handle the opposite case: when the plant deviates from expected behavior. Component failures, sensor degradation, or unanticipated disturbances cause this deviation.
 
-These continuous controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving 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.
+Expulsory controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving 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.
 

4-metrics-of-success/v1.tex

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