Multi-level editorial pass: Gopen + Heilmeier alignment

Pass 1 (Tactical): Sentence-level improvements
- Strengthened issue-point positioning (stress at sentence end)
- Improved topic-stress flow (known→new information)
- Converted passive to active voice where appropriate
- Tightened verb choice and eliminated weak constructions
- Fixed pronoun references and reduced unnecessary nominalizations

Pass 2 (Operational): Paragraph and section flow
- Improved transitions between paragraphs and subsections
- Strengthened section-to-section handoffs
- Enhanced coherence within major sections
- Clarified the discrete-continuous interface explanation
- Better signposting for the three controller types

Pass 3 (Strategic): Heilmeier catechism alignment
- Made 'What is new' and 'Why will it succeed' explicit
- Strengthened 'Who cares' and 'What difference' in Broader Impacts
- Clarified 'The exams' in Metrics section
- Added 'How long' statement to Schedule
- Improved overall narrative flow from problem→gap→solution→impact

All changes preserve technical accuracy while improving clarity and impact.

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,41 +1,41 @@
 % GOAL PARAGRAPH
 This research develops a methodology for creating autonomous control systems
-with event-driven control laws that guarantee safe and correct behavior.
+that guarantee safe and correct behavior through event-driven control laws.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear power relies on extensively trained operators who follow detailed
-written procedures to manage reactor control. Operators interpret plant
+Nuclear power plants rely on extensively trained operators who follow detailed
+written procedures to manage reactor control. These operators interpret plant
 conditions and make critical decisions about when to switch between control
 objectives. 
 % Gap
-This reliance on human operators creates an economic challenge for
-next-generation nuclear power plants. Small modular reactors face per-megawatt
-staffing costs that significantly exceed those of conventional plants. These
-economic constraints demand autonomous control systems that safely manage
-complex operational sequences with the same assurance as human-operated systems,
-but without constant supervision.
+Next-generation nuclear power plants face an economic challenge from this
+reliance on human operators. Small modular reactors face per-megawatt
+staffing costs significantly exceeding those of conventional plants. These
+economic constraints demand autonomous control systems that can safely manage
+complex operational sequences without constant supervision while maintaining the
+same assurance as human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-We will combine formal methods from computer science with control theory to
+We combine formal methods from computer science with control theory to
 build hybrid control systems that are correct by construction. 
 % Rationale
-Hybrid systems use discrete logic to switch between continuous control modes,
-mirroring how operators change control strategies. Existing formal methods
+Hybrid systems mirror how operators change control strategies: they use discrete
+logic to switch between continuous control modes. Existing formal methods
 generate provably correct switching logic but cannot handle continuous dynamics
 during transitions. Traditional control theory verifies continuous behavior but
 lacks tools for proving discrete switching correctness. 
 % Hypothesis and Technical Approach
-A three-stage methodology will bridge this gap. First, we translate written
+A three-stage methodology bridges this gap. 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, enabling realizability
 checking that identifies conflicts and ambiguities before implementation.
-Second, we synthesize discrete mode switching logic using reactive synthesis to
-generate deterministic automata that are provably correct by construction.
+Second, reactive synthesis generates deterministic automata that are provably
+correct by construction for discrete mode switching logic.
 Third, we develop continuous controllers for each discrete mode using standard
 control theory and reachability analysis. We classify continuous modes based on
 their transition objectives, then employ assume-guarantee contracts and barrier
-certificates to prove that mode transitions occur safely and as the
+certificates to prove that mode transitions occur safely as the
 deterministic automata specify. Local verification of continuous modes becomes
 possible without global trajectory analysis across the entire hybrid system. An
 Emerson Ovation control system will demonstrate this methodology. 

1-goals-and-outcomes/v1.tex

@@ -2,11 +2,11 @@
 
 % GOAL PARAGRAPH
 This research develops a methodology for creating autonomous hybrid control
-systems with mathematical guarantees of safe and correct behavior.
+systems that provide mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear power plants require the highest levels of control system reliability,
-where failures can result in significant economic losses, service interruptions,
+Nuclear power plants require the highest levels of control system reliability.
+Failures can result in significant economic losses, service interruptions,
 or radiological release.
 % Known information
 Currently, nuclear plant operations rely on extensively trained human operators
@@ -17,34 +17,34 @@ conditions and procedural guidance.
 % Gap
 This reliance on human operators prevents autonomous control capabilities and
 creates a fundamental economic challenge for next-generation reactor designs.
-Small modular reactors, in particular, face per-megawatt staffing costs far
-exceeding those of conventional plants and threaten their economic viability.
+Small modular reactors face per-megawatt staffing costs far
+exceeding those of conventional plants, threatening their economic viability.
 
 % Critical Need
 The nuclear industry needs autonomous control systems that safely manage complex
-operational sequences with the same assurance as human-operated systems, but
-without constant human supervision.
+operational sequences without constant human supervision while maintaining the
+same assurance as human-operated systems.
 % APPROACH PARAGRAPH Solution
-We will combine formal methods with control theory to build hybrid control
+We combine formal methods with control theory to build hybrid control
 systems that are correct by construction.
 % Rationale
-Hybrid systems use discrete logic to switch between continuous control modes,
-mirroring how operators change control strategies. Existing formal methods
+Hybrid systems mirror how operators change control strategies: they use discrete
+logic to switch between continuous control modes. Existing formal methods
 generate provably correct switching logic from written requirements but cannot
-handle the continuous dynamics that occur during transitions between modes.
+handle the continuous dynamics occurring during transitions between modes.
 Traditional control theory verifies continuous behavior but lacks tools for
 proving correctness of discrete switching decisions. This gap between discrete
 and continuous verification 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. If existing procedures can be formalized into logical
-specifications and continuous dynamics verified against transition requirements,
-then autonomous controllers can be built that are provably free from design
+transitions. If we can formalize existing procedures into logical
+specifications and verify continuous dynamics against transition requirements,
+we can build autonomous controllers provably free from design
 defects.
 % Pay-off
-This approach will enable autonomous control in nuclear power plants while
-maintaining the high safety standards required by the industry.
+This approach enables autonomous control in nuclear power plants while
+maintaining the high safety standards the industry requires.
 
 % Qualifications
 This work is conducted within the University of Pittsburgh Cyber Energy Center,
@@ -107,9 +107,9 @@ documents to deployed systems.
 verification to enable end-to-end correctness guarantees for hybrid systems.
 While formal methods can verify discrete logic and control theory can verify
 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 verification of
-each layer independently while guaranteeing correct composition.
+guarantees. This work establishes that bridge. It treats discrete specifications
+as contracts that continuous controllers must satisfy, enabling independent
+verification of each layer while guaranteeing correct composition.
 
 % Outcome Impact
 If successful, control engineers will create autonomous controllers from

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

@@ -1,10 +1,10 @@
 \section{State of the Art and Limits of Current Practice}
 
 This research aims to create autonomous reactor control systems that are
-tractably safe. Understanding what we automate requires first understanding how
+tractably safe. Understanding what we automate requires understanding how
 nuclear reactors operate today. This section examines reactor operators and the
-operating procedures we leverage, investigates limitations of human-based
-operation, and concludes with current formal methods approaches to reactor
+operating procedures we will leverage, investigates limitations of human-based
+operation, and reviews current formal methods approaches to reactor
 control systems.
 
 \subsection{Current Reactor Procedures and Operation}
@@ -15,7 +15,7 @@ Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
 Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
 Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
 scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899
-provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}, but this
+provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}, but their
 development relies fundamentally on expert judgment and simulator validation
 rather than formal verification. Procedures undergo technical evaluation,
 simulator validation testing, and biennial review as part of operator
@@ -55,19 +55,20 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Having established how nuclear plants currently operate through written
-procedures and human operators, we now examine why this human-centered approach
-poses fundamental limitations. Current-generation nuclear power plants employ
-over 3,600 active NRC-licensed reactor operators in the United
-States~\cite{operator_statistics}. These
+The preceding subsection established how nuclear plants currently operate:
+through written procedures executed by human operators. This subsection examines
+why this human-centered approach poses fundamental limitations.
+
+Current-generation nuclear power plants employ over 3,600 active NRC-licensed
+reactor operators in the United States~\cite{operator_statistics}. These
 operators divide into Reactor Operators (ROs), who manipulate reactor controls,
 and Senior Reactor Operators (SROs), who direct plant operations and serve as
 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.
 
-The persistent role of human error in nuclear safety incidents---despite decades
-of improvements in training and procedures---provides the most compelling
+Human error persistently plays a role in nuclear safety incidents despite decades
+of improvements in training and procedures. This provides the most compelling
 motivation for formal automated control with mathematical safety guarantees.
 Operators hold legal authority under 10 CFR Part 55 to make critical decisions,
 including departing from normal regulations during emergencies. The Three Mile
@@ -100,10 +101,10 @@ limitations are fundamental rather than a remediable part of human-driven contro
 
 \subsection{Formal Methods}
 
-The persistent human error problem motivates exploration of formal methods to
+The persistent human error problem motivates exploring formal methods to
 provide mathematical guarantees of correctness that human-centered approaches
 cannot achieve. This subsection examines recent formal methods work in nuclear
-control and identifies their limitations for autonomous hybrid systems.
+control and identifies limitations for autonomous hybrid systems.
 
 \subsubsection{HARDENS}
 
@@ -211,13 +212,16 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-Current practice reveals a fundamental gap: human operators provide operational
-flexibility but introduce persistent reliability limitations, while formal
+Current practice reveals a fundamental gap. Human operators provide operational
+flexibility but introduce persistent reliability limitations. Formal
 methods provide correctness guarantees but have not scaled to complete hybrid
-control design. HARDENS verified discrete logic without continuous dynamics.
+control design.
+
+HARDENS verified discrete logic without continuous dynamics.
 Differential dynamic logic can express hybrid properties but requires
 post-design expert analysis. 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—defines the challenge this research
-addresses.
+integrated into the design process.
+
+This gap—between discrete-only formal methods and post-hoc hybrid
+verification—defines the challenge this research addresses.

3-research-approach/v3.tex

@@ -20,17 +20,17 @@ continuous control behavior, but not both simultaneously. Today's continuous
 controller validation consists of extensive simulation trials. Human operators
 drive discrete switching logic for routine operation; their evaluation includes
 simulated control room testing and human factors research. Neither method
-provides rigorous guarantees of control system behavior, despite being
+provides rigorous guarantees of control system behavior despite being
 extremely resource intensive. HAHACS bridges this gap by composing formal
-methods from computer science with control-theoretic verification, formalizing
-reactor operations using the framework of hybrid automata.
+methods from computer science with control-theoretic verification and
+formalizing reactor operations using the framework of hybrid automata.
 
 The challenge of hybrid system verification lies in the interaction between
 discrete and continuous dynamics. Discrete transitions change the governing
 vector field, creating discontinuities in the system's behavior. Traditional
 verification techniques designed for purely discrete or purely continuous
 systems cannot handle this interaction directly. Our methodology addresses this
-challenge through decomposition. We verify discrete switching logic and
+challenge through decomposition: we verify discrete switching logic and
 continuous mode behavior separately, then compose these guarantees to reason
 about the complete hybrid system. This two-layer approach mirrors the structure
 of reactor operations themselves: discrete supervisory logic determines which
@@ -76,14 +76,18 @@ system is satisfied by its actual implementation.
 
 \textbf{What is new:} This approach is tractable now because the infrastructure
 for each component has matured, but no existing work composes them for
-end-to-end hybrid system verification. The novelty lies in the architecture that
-connects discrete synthesis with continuous verification through well-defined
-interfaces. By defining
+end-to-end hybrid system verification. The novelty lies in the architecture
+connecting discrete synthesis with continuous verification through well-defined
+interfaces.
+
+\textbf{Why it will succeed:} By defining
 entry, exit, and safety conditions at the discrete level first, we transform the
 intractable problem of global hybrid verification into a collection of local
-verification problems with clear interfaces. Verification is performed per mode
-rather than on the full hybrid system, keeping the analysis tractable even for
-complex reactor operations.
+verification problems with clear interfaces. Verification operates per mode
+rather than on the full hybrid system, keeping analysis tractable even for
+complex reactor operations. Nuclear procedures already define discrete boundaries
+between operating regimes, providing the natural decomposition this methodology
+requires.
 
 \begin{figure} 
   \centering
@@ -149,10 +153,10 @@ complex reactor operations.
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-Having defined the hybrid system mathematical framework, we now establish how to
-construct such systems from existing operational knowledge. The key insight is
-that nuclear operations already have a natural hybrid structure that maps
-directly to the automaton formalism.
+The hybrid system mathematical framework defined above provides the foundation.
+Now we establish how to construct such systems from existing operational knowledge.
+The key insight: nuclear operations already possess a natural hybrid structure
+that maps directly to the automaton formalism.
 
 Human control of nuclear power divides into three scopes: strategic,
 operational, and tactical. Strategic control is high-level and
@@ -364,9 +368,11 @@ according to operating procedures.
 
 \subsection{Continuous Control Modes}
 
-With the discrete controller synthesized and provably correct, we turn to the
-continuous dynamics that execute within each discrete mode. The synthesis of the
-discrete operational controller is only half of an autonomous controller. These control systems are hybrid, with both discrete and
+The discrete controller synthesized above is provably correct. Now we turn to the
+continuous dynamics executing within each discrete mode.
+
+Synthesizing the discrete operational controller completes only half of an
+autonomous controller. These control systems are hybrid: they have both discrete and
 continuous components. This section describes the continuous control modes that
 execute within each discrete state, and how we verify that they satisfy the
 requirements imposed by the discrete layer. It is important to clarify the scope
@@ -393,11 +399,11 @@ computationally expensive, and analytic solutions often become intractable
 \cite{MANYUS THESIS}.
 
 We circumvent these issues by designing our hybrid system from the bottom up
-with verification in mind. Each continuous control mode has an input set and
-output set clearly defined by our discrete transitions \textit{a priori}.
-Consider that we define the continuous state space as $\mathcal{X}$.  Each
-discrete mode $q_i$ then provides three key pieces of information for continuous
-controller design:
+with verification in mind. The discrete transitions define each continuous
+control mode's input set and output set clearly \textit{a priori}.
+
+The continuous state space is $\mathcal{X}$. Each discrete mode $q_i$ provides
+three key pieces of information for continuous controller design:
 \begin{enumerate}
   \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$,
     the set of possible initial states when entering this mode
@@ -488,9 +494,10 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-While transitory modes drive the system toward exit conditions, stabilizing
-modes maintain the system within a desired operating region. Stabilizing modes
-are continuous controllers with an objective of maintaining a particular
+Transitory modes drive the system toward exit conditions. Stabilizing modes, in
+contrast, maintain the system within a desired operating region.
+
+Stabilizing modes are continuous controllers designed to maintain a particular
 discrete state indefinitely. Rather than driving the system toward an
 exit condition, they keep the system within a safe operating region. Examples
 include steady-state power operation, hot standby, and load-following at
@@ -547,9 +554,11 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations. When the plant
-deviates from expected behavior, expulsory modes take over. Expulsory modes are
-continuous controllers responsible for ensuring safety when failures occur. They are designed for robustness rather
+Transitory and stabilizing modes handle nominal operations. Expulsory modes
+handle 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

4-metrics-of-success/v1.tex

@@ -1,8 +1,10 @@
 \section{Metrics for Success}
 
-This research will be measured by advancement through Technology Readiness
-Levels, progressing from fundamental concepts to validated prototype
-demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where
+\textbf{The exams:} This research will be measured by advancement through
+Technology Readiness Levels, progressing from fundamental concepts to validated
+prototype demonstration.
+
+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 the specific criteria required to achieve TRL 5.

6-broader-impacts/v1.tex

@@ -1,5 +1,9 @@
 \section{Broader Impacts}
 
+\textbf{Who cares:} The nuclear industry, datacenter operators, and clean energy
+advocates all face the same economic constraint: high operating costs driven by
+staffing requirements.
+
 Nuclear power presents both a compelling application domain and an urgent
 economic challenge. Recent interest in powering artificial intelligence
 infrastructure has renewed focus on small modular reactors (SMRs), particularly
@@ -21,14 +25,16 @@ 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.
 
-This research directly addresses the multi-billion-dollar O\&M cost challenge
-through the high-assurance autonomous control methodology developed in this
-work. Current nuclear operations require full control room staffing for each
+\textbf{What difference it makes:} This research directly addresses the
+multi-billion-dollar O\&M cost challenge through high-assurance autonomous
+control.
+
+Current nuclear operations require full control room staffing for each
 reactor, whether large conventional units or small modular designs. These staffing requirements drive the high O\&M costs
 that make nuclear power economically challenging, particularly for smaller
 reactor designs where the same staffing overhead must be spread across lower
 power output. Synthesizing provably correct hybrid controllers from formal
-specifications can automate routine operational sequences that currently require
+specifications automates routine operational sequences that currently require
 constant human oversight. This enables a fundamental shift from direct operator
 control to supervisory monitoring, where operators oversee multiple autonomous
 reactors rather than manually controlling individual units.

8-schedule/v1.tex

@@ -1,7 +1,10 @@
 \section{Schedule, Milestones, and Deliverables}
 
-This research will be conducted over six trimesters (24 months) of full-time
-effort following the proposal defense in Spring 2026. The work progresses
+\textbf{How long it will take:} This research will be conducted over six
+trimesters (24 months) of full-time effort following the proposal defense in
+Spring 2026. All work uses existing computational and experimental resources
+available through the University of Pittsburgh Cyber Energy Center and NRC
+Fellowship funding. The work progresses
 sequentially through three main research thrusts before culminating in
 integrated demonstration and validation.