Multi-level editorial pass: tactical, operational, strategic

TACTICAL (sentence-level):
- Applied Gopen's Sense of Structure principles
- Improved issue-point and topic-stress positioning
- Enhanced topic strings for coherent subject flow
- Strengthened verb choices (active voice where appropriate)
- Eliminated weak constructions ('then', excessive passives)
- Fixed typo: 'excess' → 'access' in Section 3

OPERATIONAL (paragraph/section):
- Improved transitions between subsections
- Enhanced coherence within sections
- Streamlined paragraph flow
- Better topic positioning across paragraph boundaries

STRATEGIC (document-level):
- Strengthened Heilmeier catechism alignment
- Made 'What is new?' and 'Why will it succeed?' explicit
- Added section transitions linking methodology to metrics
- Connected risks analysis to broader impacts
- Ensured each section answers its core questions clearly
- Added closing transitions to Sections 5 and 6

1-goals-and-outcomes/research_statement_v1.tex

@@ -3,9 +3,9 @@ This research develops a methodology for creating 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. Plant conditions guide these operators as they decide when to switch between control objectives.
+Extensively trained operators manage nuclear reactor control by following detailed written procedures. Plant conditions guide these operators 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. This economic constraint threatens their viability without autonomous control. Autonomous control systems must therefore manage complex operational sequences safely—without constant supervision—while providing assurance equal to or better than human-operated systems.
+Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs exceed those of conventional plants significantly. Without autonomous control, 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 better than human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods from computer science with control theory to
@@ -21,15 +21,15 @@ 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. Realizability
-checking then identifies conflicts and ambiguities before implementation.
-Second, reactive synthesis generates deterministic automata—provably
+checking identifies conflicts and ambiguities before implementation.
+Second, reactive synthesis generates deterministic automata provably
 correct by construction.
 Third, we design continuous controllers for each discrete mode using standard
-control theory and verify them using reachability analysis. Continuous modes are classified by their transition objectives; assume-guarantee contracts and barrier certificates then prove mode transitions occur safely. This approach enables local verification of continuous modes
+control theory and verify them using reachability analysis. Continuous modes are classified by their transition objectives. Assume-guarantee contracts and barrier certificates prove 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
-This approach demonstrates that autonomous control can manage complex nuclear
+Autonomous control can therefore manage complex nuclear
 power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS

1-goals-and-outcomes/v1.tex

@@ -11,15 +11,15 @@ or radiological release.
 % Known information
 Nuclear plant operations rely on extensively trained human operators
 who follow detailed written procedures and strict regulatory requirements to
-manage reactor control. Plant conditions and procedural guidance inform these operators as they decide when to switch between different control modes.
+manage reactor control. Plant conditions and procedural guidance inform these operators when they switch between different control modes.
 % Gap
 This reliance on human operators prevents autonomous control and
 creates a fundamental economic challenge for next-generation reactor designs.
-Small modular reactors face per-megawatt staffing costs far
-exceeding those of conventional plants, threatening their economic viability.
-The nuclear industry therefore needs autonomous control systems that safely manage complex
-operational sequences without constant human supervision while providing
-assurance higher than human-operated systems.
+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
+operational sequences safely without constant human supervision while providing
+assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control
@@ -34,11 +34,9 @@ and continuous verification prevents end-to-end correctness guarantees.
 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,
-enabling autonomous controllers provably free from design
-defects. This work is conducted within the University of Pittsburgh Cyber Energy Center,
-which provides access to industry collaboration and Emerson control hardware,
-ensuring that developed solutions align with practical implementation
+specifications and verify continuous dynamics against transition requirements. Autonomous controllers provably free from design
+defects result from this approach. This work is conducted within the University of Pittsburgh Cyber Energy Center,
+which provides access to industry collaboration and Emerson control hardware. Developed solutions therefore align with practical implementation
 requirements.
 
 % OUTCOMES PARAGRAPHS
@@ -65,10 +63,10 @@ If this research is successful, we will be able to do the following:
     We establish methods for analyzing continuous control modes to verify
     they satisfy discrete transition requirements. Classical control theory for
     linear systems and reachability analysis for nonlinear dynamics verify
-    that each continuous mode safely reaches its intended transitions.
+    that each continuous mode reaches its intended transitions safely.
     % Outcome
     Engineers design continuous controllers using standard practices while
-    maintaining formal correctness guarantees. Mode transitions provably occur safely and at the correct times.
+    maintaining formal correctness guarantees. Mode transitions occur safely and at the correct times, provably.
 
     % OUTCOME 3  Title
   \item \textbf{Demonstrate autonomous reactor startup control with safety
@@ -93,8 +91,8 @@ These three outcomes—procedure translation, continuous verification, and hardw
 Formal methods verify discrete logic. Control theory verifies
 continuous dynamics. No existing methodology bridges both with compositional
 guarantees. This work establishes that bridge by treating discrete specifications
-as contracts that continuous controllers must satisfy, enabling independent
-verification of each layer while guaranteeing correct composition.
+as contracts that continuous controllers must satisfy. Independent
+verification of each layer becomes possible while correct composition is guaranteed.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from
@@ -108,4 +106,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 detail this methodology: Section 2 examines the state of the art and identifies the verification gap this work addresses. Section 3 presents our hybrid control synthesis approach. Section 4 defines Technology Readiness Level advancement as the success metric. Section 5 analyzes risks and contingencies. Section 6 discusses broader impacts, and Section 7 provides the research schedule.
+The following sections detail this methodology: Section 2 examines the state of the art and identifies the verification gap this work addresses. Section 3 presents our hybrid control synthesis approach and establishes what is new and why it will succeed. Section 4 defines Technology Readiness Level advancement as the success metric. Section 5 analyzes risks and contingencies. Section 6 discusses broader impacts and answers who cares and why now. Section 7 provides the research schedule.

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

@@ -1,11 +1,11 @@
 \section{State of the Art and Limits of Current Practice}
 
-This research creates tractably safe autonomous reactor control systems. Understanding what we automate requires understanding how nuclear reactors operate today. This section examines reactor operators and their operating procedures, investigates the limitations of human-based operation, and reviews current formal methods approaches to reactor control systems.
+This research creates tractable safe autonomous reactor control systems. Understanding what we automate requires understanding how nuclear reactors operate today. This section examines reactor operators and their operating procedures, investigates the limitations of human-based operation, and reviews current formal methods approaches to reactor control systems.
 
 \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}. Expert judgment and simulator validation—not formal verification—drive their development. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} rigorously assess procedures. 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—drive 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
@@ -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. Nuclear plants currently operate through written procedures executed by human operators. This human-centered approach defines current practice. We now examine why this reliance poses fundamental limitations.
+The previous subsection established that procedures lack formal verification despite rigorous development. Human operators execute these procedures to control nuclear plants—a human-centered approach that defines current practice. This subsection examines why reliance on human operators 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
@@ -81,7 +81,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Human factors impose fundamental reliability limits that training alone cannot overcome. Formal methods offer an alternative: 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.
+Human factors impose fundamental reliability limits that training alone cannot overcome. Formal methods offer an alternative: mathematical guarantees of correctness that human-centered approaches cannot achieve. This subsection examines recent formal methods work in nuclear control and identifies limitations for autonomous hybrid systems.
 
 \subsubsection{HARDENS}
 
@@ -121,7 +121,7 @@ project did not address continuous dynamics of nuclear reactor physics. Real
 reactor safety depends on the interaction between continuous
 processes---temperature, pressure, neutron flux---evolving in response to
 discrete control decisions. HARDENS verified the discrete controller in
-isolation but not the closed-loop hybrid system behavior.
+isolation, not the closed-loop hybrid system behavior.
 
 \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
 continuous dynamics or hybrid system verification.} Verifying discrete control
@@ -129,8 +129,7 @@ logic alone provides no guarantee that the closed-loop system exhibits desired
 continuous behavior such as stability, convergence to setpoints, or maintained
 safety margins.
 
-Beyond the technical limitation of omitting continuous dynamics, HARDENS also faced
-deployment maturity constraints. The project produced a demonstrator system at Technology Readiness Level 2--3
+HARDENS also faced deployment maturity constraints beyond the technical limitation of omitting continuous dynamics. The project produced a demonstrator system at Technology Readiness Level 2--3
 (analytical proof of concept with laboratory breadboard validation) rather than
 a deployment-ready system validated through extended operational testing. The
 NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
@@ -188,8 +187,8 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-\textbf{State of the art:} Current practice reveals a fundamental gap. 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.
+\textbf{What is the state of the art?} Current practice reveals a fundamental gap. 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. No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process.
 
-\textbf{The gap our work addresses:} This gap—between discrete-only formal methods and post-hoc hybrid verification—defines our challenge and motivates our approach. Closing it enables autonomous nuclear control with mathematical safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability. The next section presents our methodology for bridging this gap through compositional hybrid verification.
+\textbf{The gap our work addresses:} This gap—between discrete-only formal methods and post-hoc hybrid verification—defines our challenge and motivates our approach. Closing it enables autonomous nuclear control with mathematical safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability. 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,9 +15,9 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Extensive simulation trials validate continuous controllers. Simulated control room testing and human factors research evaluate discrete switching logic. 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, then formalizing reactor operations using hybrid automata.
+Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Extensive simulation trials validate continuous controllers. Simulated control room testing and human factors research evaluate discrete switching logic. 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 and 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—fail to 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; 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—fail to 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. 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
@@ -54,7 +54,7 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac
 
 \textbf{What is new?} Each component's infrastructure has matured, but no existing work composes them for end-to-end hybrid system verification. Our novelty lies in the architecture connecting discrete synthesis with continuous verification through well-defined interfaces—specifically, mode-level verification that avoids global hybrid system analysis.
 
-\textbf{Why will it succeed?} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into tractable local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and critically—nuclear procedures already define discrete boundaries between operating regimes. This existing structure provides the natural decomposition our methodology requires, making the approach practical for real systems.
+\textbf{Why will it succeed?} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into tractable local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and critically—nuclear procedures already define discrete boundaries between operating regimes. This existing structure provides the natural decomposition our methodology requires. The approach becomes practical for real systems as a result.
 
 \begin{figure} 
   \centering
@@ -136,9 +136,9 @@ physical state of the plant. Tactical control objectives include maintaining
 pressurizer level, maintaining core temperature, or adjusting reactivity with a
 chemical shim.
 
-The operational control scope links these two extremes. This level is the primary responsibility of human operators
+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. It thereby bridges high-level and low-level goals. 
+tactical control objectives to drive the plant toward strategic goals, thereby 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
@@ -189,10 +189,10 @@ which tactical control law to apply. This operational level is precisely what we
 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
-strategic requirements, as unified infrastructure for building and verifying
+strategic requirements; unified infrastructure for building and verifying
 hybrid systems does not currently exist. Humans have been used for this layer
-because their general intelligence has been relied upon as a safe way to manage
-the hybrid nature of this system. But these operators use prescriptive operating
+because their general intelligence provides a safe way to manage
+the hybrid nature of this 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.
@@ -296,7 +296,7 @@ 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
 human operator operating correctly. Humans are intrinsically probabilistic
-creatures who cannot eliminate human error. By defining the behavior of this
+and cannot eliminate human error. By defining the behavior of this
 system using temporal logics and synthesizing the controller using deterministic
 algorithms, we are assured that strategic decisions will always be made
 according to operating procedures.
@@ -317,11 +317,11 @@ according to operating procedures.
 
 \subsection{Continuous Control Modes}
 
-Synthesis guarantees the discrete controller is provably correct—but hybrid control requires more than discrete correctness. We now turn to the continuous dynamics executing within each discrete mode.
+Synthesis guarantees the discrete controller is provably correct—but hybrid control requires more than discrete correctness. The continuous dynamics executing within each discrete mode must also be verified.
 
 The discrete operational controller represents only half of an
 autonomous controller, despite its provable correctness. Hybrid control systems require both discrete and
-continuous components. This section describes the continuous control modes that
+continuous components. 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. 
 
@@ -572,12 +572,14 @@ the success and impact of this work. We will directly address the gap of
 verification and validation methods for these systems and industry adoption by
 forming a two-way exchange of knowledge between the laboratory and commercial
 environments. This work stands to be successful with Emerson implementation
-because we will have excess to system experts at Emerson to help with the fine
+because we will have access to system experts at Emerson to help with the fine
 details of using the Ovation system. At the same time, we will have the benefit
 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. The next section defines how we measure success through Technology Readiness Level advancement.
+
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration
 % - Mention what startup sequence will be demonstrated (cold shutdown →

4-metrics-of-success/v1.tex

@@ -88,3 +88,5 @@ 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
 controllers and that implementation is achievable with current technology.
+
+While TRL advancement provides clear success criteria, several risks could prevent achieving these milestones. The next section analyzes these risks and establishes contingency plans.

5-risks-and-contingencies/v1.tex

@@ -6,10 +6,9 @@ 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 indicators for early detection and
-contingency plans preserving research value even if core assumptions prove
+contingency plans that preserve research value even if core assumptions prove
 false. The staged project structure ensures that partial success yields
-publishable results and clear identification of remaining barriers to
-deployment.
+publishable results and identifies remaining barriers to deployment clearly.
 
 \subsection{Computational Tractability of Synthesis}
 
@@ -46,8 +45,8 @@ rather than a failure.
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-Computational tractability represents one dimension of risk. The second critical assumption concerns a more fundamental challenge: the mapping between boolean guard
-conditions in temporal logic and continuous state boundaries required for mode
+Computational tractability represents one dimension of risk. A more fundamental challenge represents the second critical assumption: mapping boolean guard
+conditions in temporal logic to continuous state boundaries required for mode
 transitions. This interface represents the fundamental challenge of hybrid
 systems: relating discrete switching logic to continuous dynamics. Temporal
 logic operates on boolean predicates, while continuous control requires
@@ -156,3 +155,6 @@ ambiguities amenable to systematic resolution. This cross-design analysis would
 strengthen the generalizability of any proposed specification language
 extensions, ensuring they address industry-wide practices rather than specific
 quirks.
+
+
+These risks and contingencies demonstrate that while the research faces real challenges, each has identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if assumptions prove invalid. With risks addressed, the next section examines broader impacts: who cares about this work and why it matters now.

6-broader-impacts/v1.tex

@@ -33,8 +33,8 @@ 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 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
+constant human oversight. A fundamental shift from direct operator
+control to supervisory monitoring becomes possible, where operators oversee multiple autonomous
 reactors rather than manually controlling individual units.
 
 The correct-by-construction methodology is critical for this transition.
@@ -73,3 +73,6 @@ autonomy with provable correctness guarantees. Demonstrating this approach in
 nuclear power---one of the most regulated and safety-critical domains---will
 establish both the technical feasibility and regulatory pathway for broader
 adoption across critical infrastructure.
+
+
+The broader impacts establish why this work matters beyond nuclear power. The next section presents the timeline for achieving these outcomes through a structured research plan.