Multi-pass editorial review: tactical, operational, strategic

TACTICAL (sentence-level):
- Applied Gopen's topic-stress positioning (old→new info flow)
- Strengthened verb choices and active voice
- Eliminated unnecessary hedging and wordiness
- Improved clause positioning for clarity

OPERATIONAL (paragraph/section):
- Streamlined transitions between subsections
- Removed redundant transition phrases
- Improved paragraph coherence and flow
- Tightened connections between related ideas

STRATEGIC (document-level):
- Fixed section reference (Section 8, not Section 7)
- Verified Heilmeier catechism alignment across sections
- Strengthened signposting between major sections
- Ensured each section delivers on its stated purpose

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,33 +2,33 @@
 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 their viability. To address this challenge, autonomous control systems must manage complex operational sequences safely—without constant supervision—while providing assurance equal to or exceeding that of human-operated systems.
+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
-build hybrid control systems correct by construction. 
+build hybrid control systems that are 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 but cannot handle continuous dynamics
 during transitions. Control theory verifies continuous behavior but
-cannot prove discrete switching correctness. 
+cannot prove the correctness of discrete switching decisions. 
 % Hypothesis and Technical Approach
 Our methodology bridges this gap in three stages. First, we translate written
 operating procedures into temporal logic specifications using NASA's Formal
 Requirements Elicitation Tool (FRET). FRET structures requirements into scope,
 condition, component, timing, and response elements. Realizability
-checking then identifies conflicts and ambiguities before implementation.
+checking identifies conflicts and ambiguities before implementation.
-Second, reactive synthesis generates deterministic automata provably
+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. We classify continuous modes by their transition objectives. Assume-guarantee contracts and barrier certificates then prove mode transitions occur safely. This approach enables local verification of continuous modes
+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. This approach enables local verification of continuous modes
 without requiring global trajectory analysis across the entire hybrid system. An
 Emerson Ovation control system demonstrates this methodology. 
 % Pay-off
-Autonomous control can therefore manage complex nuclear
+Autonomous control therefore manages 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,7 +11,7 @@ or radiological release.
 % Known information
 Nuclear plant operations rely on extensively trained human operators
 who follow detailed written procedures and strict regulatory requirements to
-manage reactor control. 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.
@@ -23,19 +23,19 @@ assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control
-systems correct by construction.
+systems that are 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 cannot handle continuous dynamics during transitions between modes.
-Control theory verifies continuous behavior but cannot prove correctness of discrete switching decisions. This gap prevents end-to-end correctness guarantees.
+Control theory verifies continuous behavior but cannot prove the 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
 transitions. We formalize existing procedures into logical
-specifications and verify continuous dynamics against transition requirements. This approach produces autonomous controllers provably free from design
+specifications and verify continuous dynamics against transition requirements. This approach produces autonomous controllers that are provably free from design
 defects. We conduct this work within the University of Pittsburgh Cyber Energy Center,
-which provides access to industry collaboration and Emerson control hardware. Solutions developed here therefore align with practical implementation
+which provides access to industry collaboration and Emerson control hardware. Solutions developed here align with practical implementation
 requirements.
 
 % OUTCOMES PARAGRAPHS
@@ -105,4 +105,4 @@ costs through increased autonomy. This research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the
 nuclear industry requires.
 
-The following sections systematically answer the Heilmeier Catechism questions that define this research: Section 2 examines the state of the art, establishing what has been done and what remains impossible with current approaches. Section 3 presents our hybrid control synthesis methodology, demonstrating what is new and why it will succeed where prior work has not. Section 4 defines how we measure success through Technology Readiness Level advancement from analytical concepts to hardware demonstration. Section 5 identifies risks that could prevent success and establishes contingencies. Section 6 addresses who cares and why now, examining the economic imperative driving autonomous nuclear control and the broader impact on safety-critical systems. Section 7 provides the research schedule and deliverables, answering how long this work will take.
+The following sections systematically answer the Heilmeier Catechism questions that define this research: Section 2 examines the state of the art, establishing what has been done and what remains impossible with current approaches. Section 3 presents our hybrid control synthesis methodology, demonstrating what is new and why it will succeed where prior work has not. Section 4 defines how we measure success through Technology Readiness Level advancement from analytical concepts to hardware demonstration. Section 5 identifies risks that could prevent success and establishes contingencies. Section 6 addresses who cares and why now, examining the economic imperative driving autonomous nuclear control and the broader impact on safety-critical systems. Section 8 provides the research schedule and deliverables, answering how long this work will take.

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

@@ -22,10 +22,10 @@ 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, operate with implemented automation. Reactor
+alone. Safety systems, by contrast, already employ implemented automation. Reactor
 Protection Systems trip automatically on safety signals with millisecond
 response times, and engineered safety features actuate automatically on accident
-signals without operator action required.
+signals without requiring operator action.
 
 The division between automated and human-controlled functions reveals the
 fundamental challenge of hybrid control. Highly automated systems handle reactor
@@ -37,7 +37,7 @@ 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. Procedures define what to do; human operators determine when and how to apply them. This approach 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
@@ -56,10 +56,10 @@ deficiencies, and component failures combined to cause partial meltdown. Operato
 misread confusing and contradictory indications, then shut off the emergency water
 system~\cite{Kemeny1979}. The President's Commission on TMI identified a
 fundamental ambiguity: placing responsibility for safe power plant operations on
-the licensee without formal verification that operators can fulfill this
+the licensee without formally verifying that operators can fulfill this
 responsibility does not guarantee safety. This tension between operational
 flexibility and safety assurance remains unresolved: the person responsible for
-reactor safety is often the root cause of failures.
+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
@@ -80,7 +80,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The previous two subsections established that procedures lack formal verification and human operators introduce persistent reliability issues. Formal methods offer an alternative: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
+Procedures lack formal verification, and human operators introduce persistent reliability issues. Formal methods offer an alternative: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
 
 \subsubsection{HARDENS}
 
@@ -153,7 +153,7 @@ primary assurance evidence.
 
 \subsubsection{Sequent Calculus and Differential Dynamic Logic}
 
-HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. 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
+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
 into temporal logic: the box operator and the diamond operator. The box operator
 \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
 \(\alpha\) always remains within that region. In this way, it is a safety
@@ -188,6 +188,6 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and does not scale to system synthesis.
 
-\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. This gap—between discrete-only formal methods and post-hoc hybrid verification—prevents autonomous nuclear control with end-to-end correctness guarantees. Closing this gap would enable 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.
 
-Having established what has been done and where current approaches fall short, the next section presents our methodology for bridging this gap through compositional hybrid verification, establishing what is new and why it will succeed.
+Section 3 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,9 +15,9 @@
 % ----------------------------------------------------------------------------
 % 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, formalizing reactor operations using hybrid automata.
 
-Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations, where discrete supervisory logic determines which control mode is active and continuous controllers govern plant behavior within each mode.
+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
 a mathematical description of the system. This work draws on
@@ -52,9 +52,9 @@ where:
 
 Creating a HAHACS requires constructing such a tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. The novelty lies in three innovations: First, we use discrete synthesis to define entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, we classify continuous modes by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, we leverage existing procedural structure to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
+\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. The novelty lies in three innovations. First, we use discrete synthesis to define entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, we classify continuous modes by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, we leverage existing procedural structure to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
 
-\textbf{Why will it succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than imposing artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, keeping computational complexity bounded by verifying each mode against local contracts. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We are not proving feasibility in principle—we are demonstrating it on production control systems with realistic reactor models.
+\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 impose artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, keeping computational complexity bounded by verifying each mode against local contracts. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We demonstrate feasibility on production control systems with realistic reactor models, not merely prove it in principle.
 
 \begin{figure} 
   \centering
@@ -320,7 +320,7 @@ Reactive synthesis produces a provably correct discrete controller from operatin
 
 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 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.
+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 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.
 
 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
@@ -371,11 +371,7 @@ requirements that determine which formal methods tools are appropriate. The foll
 
 \subsubsection{Transitory Modes}
 
-Transitory modes, the first mode type, move
+Transitory modes move the plant from one discrete operating condition to another. Their purpose is to execute transitions: start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers.
-the plant from one discrete operating condition to another. Their purpose is to
-execute transitions: start from entry conditions, reach exit conditions,
-and maintain safety invariants throughout. Examples include power ramp-up sequences,
-cooldown procedures, and load-following maneuvers.
 
 The control objective for a transitory mode can be stated
 formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions
@@ -431,11 +427,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions. In contrast, stabilizing modes
+Transitory modes drive the system toward exit conditions. Stabilizing modes, in contrast, maintain the system within a desired operating region indefinitely rather than drive 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 use barrier certificates.
-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.
 Barrier certificates analyze the dynamics of the system to determine whether
 flux across a given boundary exists. They evaluate whether any trajectory leaves
 a given boundary. This definition exactly matches what defines the validity of a
@@ -487,15 +479,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations. The third mode type, 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 are designed for robustness rather than 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.
-handles off-nominal conditions.
-
-When the plant deviates from expected behavior, expulsory modes take over. These
-continuous controllers ensure safety when failures occur. They are designed for robustness rather
-than 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.
 
@@ -572,7 +556,7 @@ of transferring technology directly to industry with a direct collaboration in
 this research, while getting an excellent perspective of how our research
 outcomes can align best with customer needs.
 
-This methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—establishes the complete research approach. We have shown what is new (compositional hybrid verification integrated into the design process) and why it will succeed (leveraging existing procedural structure, mode-level analysis, and industrial collaboration). The next section defines how we measure success: not through theoretical contributions alone, but through Technology Readiness Level advancement that demonstrates both correctness and practical implementability.
+This methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—establishes the complete research approach. We have shown what is new (compositional hybrid verification integrated into the design process) and why it will succeed (leveraging existing procedural structure, mode-level analysis, and industrial collaboration). Section 4 defines how we measure success: not through theoretical contributions alone, but through Technology Readiness Level advancement that demonstrates both correctness and practical implementability.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

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

5-risks-and-contingencies/v1.tex

@@ -20,7 +20,7 @@ synthesis times exceeding days or weeks—preventing us from demonstrating the
 complete methodology within project timelines. Reachability analysis for
 continuous modes with high-dimensional state spaces may similarly prove
 computationally intractable. Either barrier would constitute a fundamental
-obstacle to achieving the research objectives.
+obstacle to achieving our research objectives.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets

6-broader-impacts/v1.tex

@@ -1,6 +1,6 @@
 \section{Broader Impacts}
 
-\textbf{Who cares and why now:} The nuclear industry, datacenter operators, and clean energy advocates all face the same economic constraint: high operating costs driven by staffing requirements. AI infrastructure demands—growing exponentially—have made this constraint urgent.
+\textbf{Who cares? Why now?} The nuclear industry, datacenter operators, and clean energy advocates all face the same economic constraint: high operating costs driven by staffing requirements. AI infrastructure demands—growing exponentially—have made this constraint urgent.
 
 Nuclear power presents both a compelling application domain and an urgent
 economic challenge. Recent interest in powering artificial intelligence