Editorial pass: tactical, operational, and strategic improvements

Three-level editorial revision following Gopen's Sense of Structure and
Heilmeier Catechism alignment:

TACTICAL (sentence-level):
- Improved issue-point positioning (old → new information flow)
- Strengthened topic-stress (key info at sentence end)
- Enhanced verb choice and active voice
- Tightened logical connectives

OPERATIONAL (paragraph/section):
- Improved transitions between subsections
- Enhanced coherence within paragraphs
- Clarified topical flow between ideas

STRATEGIC (document-level):
- Strengthened Heilmeier question framing in each section
- Improved cross-section connections and callbacks
- Enhanced summary paragraphs linking sections together
- Clarified the through-line from gap → innovation → success metrics

1-goals-and-outcomes/v1.tex

@@ -15,7 +15,7 @@ This research unifies formal methods with control theory to produce hybrid contr
 % Rationale
 Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
 % Hypothesis
-Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. Operating procedures transform into logical specifications that constrain continuous dynamics, producing autonomous controllers provably free from design defects. 
+Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This transforms operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers that are provably free from design defects. 
 
 The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation requirements.
 
@@ -62,10 +62,10 @@ If successful, this approach produces three concrete outcomes:
 \end{enumerate}
 
 % IMPACT PARAGRAPH Innovation
-\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. Section 2 will show that prior work verified discrete logic or continuous dynamics—never both compositionally. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. 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?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. Section 2 will show that prior work verified discrete logic or continuous dynamics—never both compositionally. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. Together, these three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology spanning from regulatory documents to deployed systems.
 
 % Outcome Impact
-If successful, control engineers will create autonomous controllers from existing procedures with mathematical proofs of correct behavior, making high-assurance autonomous control practical for safety-critical applications. This capability is essential for the economic viability of next-generation nuclear power. Small modular reactors, in particular, offer a promising solution to growing energy demands, but their success depends on reducing per-megawatt operating costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. 
+If successful, control engineers will create autonomous controllers from existing procedures with mathematical proofs of correct behavior. This makes high-assurance autonomous control practical for safety-critical applications—a capability essential for the economic viability of next-generation nuclear power. Small modular reactors offer a promising solution to growing energy demands. Their success depends on reducing per-megawatt operating costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. 
 
 This proposal follows the Heilmeier Catechism. Each section explicitly answers its assigned questions:
 \begin{itemize}

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

@@ -10,11 +10,11 @@ Section 3 addresses the verification gap these limits establish.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current practice rests on two critical components: procedures and operators. Procedures define what must be done. Operators execute those procedures. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection examines operators—their reliability limits and contribution to accidents.
+Current practice rests on two critical components: procedures and operators. Procedures define what must be done; operators execute those procedures. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The next subsection examines operators—their reliability limits and contribution to accidents.
 
-Nuclear plant procedures form a strict 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. All procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 
+Nuclear plant procedures form a strict 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, while Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. All 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—form the basis for procedure development. Regulations mandate rigorous assessment. Specifically, 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states. No proof confirms that required actions complete within available timeframes. No proof confirms that transitions between procedure sets maintain safety invariants.
+Procedure development rests on expert judgment and simulator validation—not formal verification. Regulations mandate rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms 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.} No proof exists that procedures cover all
@@ -30,9 +30,9 @@ Safety systems already employ extensive automation. Reactor Protection Systems t
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge: even perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
+Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. 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; operators determine when and how to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
+Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. While procedures define what to do, operators determine when and how to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -62,9 +62,9 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The previous subsections established two fundamental limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints—not remediable defects.
+The previous subsections established two fundamental limitations. First, procedures lack formal verification. Second, human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints—not remediable defects.
 
-Formal methods could eliminate both limitations by providing mathematical guarantees of correctness. However, even the most advanced formal methods applications in nuclear control leave a critical verification gap.
+Formal methods could eliminate both limitations by providing mathematical guarantees of correctness. Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap.
 
 This subsection examines two approaches illustrating this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
 
@@ -159,10 +159,10 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 This section addressed two Heilmeier questions: What has been done? What are the limits of current practice?
 
-\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability constraints. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally.
+\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. First, human operators provide operational flexibility but introduce persistent reliability constraints that training cannot eliminate. Second, HARDENS verified discrete logic but omitted continuous dynamics. Third, differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally.
 
 \textbf{What are the limits of current practice?} A clear verification gap emerges: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics—never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-\textbf{Why now?} Two forces create urgency. First, economic necessity: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, technical maturity: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
+\textbf{Why now?} Two forces create urgency. Economic necessity: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
 
-Section 2 established what has been done and the limits of current practice. The verification gap is clear. The timing is right. Section 3 addresses the next two Heilmeier questions—what is new and why it will succeed—presenting the technical approach that closes this gap.
+This section established what has been done and the limits of current practice. The verification gap is clear: no existing methodology synthesizes provably correct hybrid controllers from operational procedures. The timing is right: economic pressures demand autonomous control while technical maturity enables it. Section 3 addresses the next two Heilmeier questions—what is new and why it will succeed—presenting the technical approach that closes this gap.

3-research-approach/v3.tex

@@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees; both consume enormous resources.
+Previous approaches verified discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources.
 
-This approach bridges that gap by composing formal methods from computer science with control-theoretic verification and formalizing reactor operations as hybrid automata.
+This approach bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
 
 Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities that traditional verification techniques cannot handle directly.
 
-This methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing 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, while continuous controllers govern plant behavior within each mode.
+This 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.
 
 Hybrid systems require mathematical formalization. This work draws on automata theory, temporal logic, and control theory to provide that description.
 
@@ -58,7 +58,7 @@ where:
 
 A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new in this research?} Existing approaches verify discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently but have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation.
+\textbf{What is new in this research?} Existing approaches verify discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently. They have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation.
 
 Three innovations enable compositional verification:
 
@@ -142,9 +142,9 @@ These factors combine to demonstrate feasibility on production control systems w
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The previous subsection established the hybrid automaton formalism: a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. This formalism provides the mathematical structure for hybrid control. A critical question remains—where do these formal descriptions originate?
+The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. This formalism provides the mathematical structure for hybrid control. But a critical question remains: where do these formal descriptions originate?
 
-Nuclear operations already possess a natural hybrid structure that maps directly to this formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge, leveraging decades of domain expertise already encoded in operating procedures rather than imposing artificial abstractions.
+The answer lies in existing practice. Nuclear operations already possess a natural hybrid structure that maps directly to this formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge, leveraging decades of domain expertise already encoded in operating procedures rather than imposing artificial abstractions.
 
 Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years: managing labor needs and supply chains to optimize scheduled maintenance and downtime.
 
@@ -392,9 +392,9 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions, with reachability analysis verifying whether the target can be reached.
+Transitory modes drive the system toward exit conditions. Reachability analysis verifies whether the target can be reached.
 
-Stabilizing modes address a different question: will the system stay within bounds? Unlike transitory modes that aim to reach a target, stabilizing modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
+Stabilizing modes address a different question: will the system stay within bounds? Unlike transitory modes, which aim to reach a target, stabilizing modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
 
 Reachability analysis answers "can the system reach a target?" Stabilizing modes instead ask "does the system stay within bounds?" Barrier certificates provide the appropriate verification tool for this question.
 Barrier certificates analyze the dynamics of the system to determine whether
@@ -443,7 +443,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations—moving the plant between conditions and maintaining it within regions, respectively—but both assume the plant dynamics match the design model.
+Transitory and stabilizing modes handle nominal operations. Transitory modes move the plant between conditions. Stabilizing modes maintain it within regions. Both assume the plant dynamics match the design model.
 
 Expulsory modes address a different scenario: situations where the plant deviates from expected behavior. This deviation may result from component failures, sensor degradation, or unanticipated disturbances. Here, robustness matters more than optimality.
 
@@ -526,15 +526,15 @@ outcomes can align best with customer needs.
 
 This section addressed two critical Heilmeier questions: What is new? Why will it succeed?
 
-\textbf{What is new?} Three innovations enable compositional verification integrating reactive synthesis, reachability analysis, and barrier certificates: 
+\textbf{What is new?} Three innovations enable compositional verification by integrating reactive synthesis, reachability analysis, and barrier certificates: 
 
-\textit{Contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
+First, \textit{contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
 
-\textit{Mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
+Second, \textit{mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
 
-\textit{Procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion.
+Third, \textit{procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion.
 
-Section 2 established that prior work verified discrete logic or continuous dynamics—never both compositionally. This compositional verification enables what global analysis cannot achieve.
+Section 2 established that prior work verified discrete logic or continuous dynamics—never both compositionally. These three innovations enable what global analysis cannot achieve: compositional verification spanning from procedures to verified implementation.
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility: 
 
@@ -544,7 +544,13 @@ Section 2 established that prior work verified discrete logic or continuous dyna
 
 \textit{Industrial validation.} Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
 
-The complete technical methodology is now established. Sections 2 and 3 addressed the first four Heilmeier questions: what has been done, what limits current practice, what is new, and why it will succeed. Three questions remain. Section 4 addresses how success will be measured. Section 5 identifies what could prevent success. Section 6 explains who cares, why now, and what difference this work will make.
+The complete technical methodology is now established. 
+
+Sections 2 and 3 addressed the first four Heilmeier questions. Section 2 established what has been done and what limits current practice. Section 3 explained what is new and why it will succeed. 
+
+Three questions remain. How will success be measured? What could prevent success? Who cares, why now, and what difference will this work make? 
+
+Section 4 addresses the first question: metrics for success. Section 5 identifies what could prevent success. Section 6 explains who cares, why now, and what difference this work will make.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -93,4 +93,6 @@ TRL 5 validates hardware implementation in a relevant environment: the complete
 
 Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology—not merely theoretically sound but practically deployable.
 
-Sections 2 through 4 addressed five Heilmeier questions: what has been done, what limits current practice, what is new, why it will succeed, and how to measure success. Success assumes critical technical challenges can be overcome. Section 5 addresses what could prevent success.
+Sections 2 through 4 addressed five Heilmeier questions. Section 2 established what has been done and what limits current practice. Section 3 explained what is new and why it will succeed. This section defined how to measure success.
+
+But success assumes critical technical challenges can be overcome. Section 5 addresses what could prevent success and how to respond when assumptions fail.

5-risks-and-contingencies/v1.tex

@@ -139,8 +139,10 @@ Each risk has identifiable early warning indicators enabling detection before fa
 
 The staged project structure ensures partial success yields publishable results identifying remaining deployment barriers. This design maintains contribution regardless of which technical obstacles prove insurmountable. Even "failure" advances the field by documenting precisely which barriers remain.
 
-Sections 2 through 5 established the complete technical research plan. Section 2 addressed what has been done and what limits current practice. Section 3 established what is new and why it will succeed. Section 4 defined how to measure success. This section identified what could prevent success and how to respond.
+Sections 2 through 5 established the complete technical research plan. 
+
+Section 2 addressed what has been done and what limits current practice, establishing the verification gap. Section 3 explained what is new and why it will succeed, presenting three innovations that enable compositional verification. Section 4 defined how to measure success through TRL advancement. This section identified what could prevent success and how to respond when assumptions fail.
 
 One critical question remains: Who cares? Why now? What difference will it make?
 
-Section 6 connects this technical methodology to urgent economic and societal challenges.
+Section 6 connects this technical methodology to urgent economic and societal challenges, demonstrating why this work matters now.

6-broader-impacts/v1.tex

@@ -70,4 +70,10 @@ This section answered three critical Heilmeier questions:
 
 \textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier and enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure, extending beyond nuclear power to any safety-critical system requiring provable correctness.
 
-Sections 2 through 6 addressed all but one of the Heilmeier questions. Section 2 established what has been done and what limits current practice. Section 3 explained what is new and why it will succeed. Section 4 defined how to measure success. Section 5 identified what could prevent success. This section connected technical methodology to economic and societal impact. One final Heilmeier question remains: How long will it take? Section 8 provides the answer.
+Sections 2 through 6 addressed all but one of the Heilmeier questions. 
+
+Section 2 established what has been done and what limits current practice, identifying the verification gap. Section 3 explained what is new and why it will succeed, presenting three innovations enabling compositional verification. Section 4 defined how to measure success through TRL advancement from 3 to 5. Section 5 identified what could prevent success and provided contingencies. This section connected technical methodology to economic and societal impact.
+
+One final Heilmeier question remains: How long will it take? 
+
+Section 8 provides the answer, presenting a detailed schedule with milestones and deliverables.