Editorial pass: Gopen + Heilmeier alignment

TACTICAL (sentence-level):
- Applied issue-point positioning (old info → new info)
- Strengthened verb choices, reduced nominalizations
- Eliminated unnecessary passive constructions
- Improved topic string coherence across sentences
- Split overly complex sentences for clarity

OPERATIONAL (paragraph-level):
- Strengthened transitions between subsections
- Improved paragraph flow within sections
- Enhanced coherence within related paragraphs
- Clarified relationships between ideas

STRATEGIC (document-level):
- Tightened Heilmeier question alignment
- Improved section-to-section linkages
- Made explicit connections clearer
- Ensured each section clearly answers its Heilmeier questions

Focus: clarity and impact improvements without nitpicking.

1-goals-and-outcomes/research_statement_v1.tex

@@ -4,18 +4,18 @@ This research develops autonomous control systems that provide mathematical guar
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear reactors today require human operators to follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: staffing costs per megawatt far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if safety assurance equals or exceeds that of human operators.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding human operators.
 
 % APPROACH PARAGRAPH Solution
-This research unifies formal methods from computer science with control theory to produce hybrid control systems correct by construction.
+This research unifies formal methods with control theory to produce hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. Both are required for end-to-end correctness.
+Human operators already work this way—they use discrete logic to switch between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. Both are required for end-to-end correctness.
 % Hypothesis and Technical Approach
-Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications, structuring requirements by scope, condition, component, timing, and response. Realizability checking then exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory—satisfy each discrete mode's requirements.
+Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy each discrete mode's requirements. Engineers design these controllers using standard control theory.
 
-Continuous modes classify by control objective into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe. This enables local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
+Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe, enabling local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
 % Pay-off
-This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It directly addresses the economic constraints threatening small modular reactor viability.
+This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It addresses the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS
 This research, if successful, produces three concrete outcomes:

1-goals-and-outcomes/v1.tex

@@ -4,36 +4,36 @@
 This research develops autonomous hybrid control systems that provide mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release.
+Nuclear power plants demand the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release.
 % Known information
-Extensively trained human operators control nuclear plants today. They follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
+Extensively trained human operators control nuclear plants today. They follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
 % Gap
-This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face staffing costs per megawatt that far exceed those of conventional plants, threatening their economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs that far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding human operators.
 
 % APPROACH PARAGRAPH Solution
-This research unifies formal methods with control theory to produce hybrid control systems correct by construction.
+This research unifies formal methods with control theory to produce hybrid control systems that are correct by construction.
 % 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 continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
+Human operators already work this way—they use discrete logic to switch between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify continuous dynamics. 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. This transforms operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers that are 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. These steps transform 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.
+The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware. This ensures solutions align with practical implementation requirements.
 
 % OUTCOMES PARAGRAPHS
-If successful, this approach produces three concrete outcomes:
+Three concrete outcomes define success for this approach:
 
 \begin{enumerate}
 
   % OUTCOME 1 Title
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
-    A methodology converts written operating procedures into formal
+    The methodology converts written operating procedures into formal
-    specifications. Reactive synthesis tools then automatically generate
+    specifications. Reactive synthesis tools then generate
-    discrete control logic from these specifications. Structured intermediate
+    discrete control logic from these specifications automatically. Structured intermediate
     representations bridge natural language procedures and mathematical logic.
     % Outcome
-    Control system engineers can generate verified mode-switching controllers
+    Control engineers generate verified mode-switching controllers
-    directly from regulatory procedures. They need no formal methods expertise.
+    directly from regulatory procedures. Formal methods expertise becomes unnecessary.
     This lowers the barrier to high-assurance control systems.
 
     % OUTCOME 2 Title
@@ -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 shows 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.
+\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. Section 2 shows 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. These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology. It spans 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. 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. 
+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. Such capability is 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. It maintains 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

@@ -2,11 +2,11 @@
 
 \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
 
-No current approach provides end-to-end correctness guarantees for autonomous control. Human-centered operation cannot eliminate reliability limits. Formal methods verify either discrete or continuous behavior—never both. 
+No current approach provides end-to-end correctness guarantees for autonomous control. Human-centered operation cannot eliminate reliability limits. Formal methods verify either discrete or continuous behavior—never both simultaneously. 
 
-Three subsections structure this analysis: reactor operators and their operating procedures, fundamental limitations of human-based operation, and formal methods approaches that verify discrete logic or continuous dynamics but not both together.
+This analysis proceeds through three subsections. The first examines reactor operators and their operating procedures. The second addresses fundamental limitations of human-based operation. The third analyzes formal methods approaches that verify discrete logic or continuous dynamics—but not both together.
 
-Section 3 addresses the verification gap these limits establish.
+Section 3 addresses the verification gap these limits create.
 
 \subsection{Current Reactor Procedures and Operation}
 
@@ -14,25 +14,26 @@ Current practice rests on two critical components: procedures and operators. Pro
 
 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}. 
 
-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 time, or 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. No proof verifies that required actions complete within available time. No proof guarantees 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
-possible plant states, that required actions complete within available
+possible plant states. No proof confirms that required actions complete within available
-timeframes, or that transitions between procedure sets maintain safety
+timeframes. No proof guarantees that transitions between procedure sets maintain safety
-invariants. Paper-based procedures cannot ensure correct application. Even
+invariants. Paper-based procedures cannot ensure correct application. Computer-based procedure systems similarly lack the formal guarantees that automated reasoning
-computer-based procedure systems lack the formal guarantees automated reasoning
 could provide.
 
 Nuclear plants operate with multiple control modes. Automatic control maintains target parameters through continuous reactivity adjustment. Manual control allows operators to directly manipulate the reactor. Various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature, compensating for power demand changes through reactivity feedback loops alone. 
 
-Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required. This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems already handle reactor protection—automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure—discrete human decisions combined with continuous automated control—forms the basis for autonomous hybrid control systems.
+Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required. This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. 
+
+Highly automated systems already handle reactor protection: automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators retain control of strategic decision-making—power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure forms the basis for autonomous hybrid control systems. It combines discrete human decisions with continuous automated control.
 
 \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 executed imperfectly.
+The previous subsection established that procedures lack formal verification despite rigorous development. 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 cannot eliminate.
+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 cannot eliminate.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -42,7 +43,7 @@ shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
 and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
 operator requires several years of training.
 
-Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence cannot be trained away. It motivates the need for formal automated control with mathematical safety guarantees. 
+Human error persistently contributes to nuclear safety incidents despite decades of training and procedure improvements. Training cannot eliminate this persistence. This motivates formal automated control with mathematical safety guarantees. 
 
 Under 10 CFR Part 55, operators hold legal authority to make critical decisions. This includes authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster. Operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. 
 
@@ -62,19 +63,19 @@ 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 these 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.
+This subsection examines two approaches that illustrate 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. Each reveals the verification gap this research addresses.
 
-\subsubsection{HARDENS: The State of Formal Methods in Nuclear Control}
+\subsubsection{HARDENS: Formal Methods in Nuclear Control}
 
 The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
 project represents the most advanced application of formal methods to nuclear
 reactor control systems to date~\cite{Kiniry2024}.
 
-HARDENS addressed a fundamental dilemma: existing U.S. nuclear control rooms rely on analog technologies from the 1950s--60s. These technologies incur significant risk and cost compared to modern control systems. The NRC contracted Galois, a formal methods firm, to demonstrate that Model-Based Systems Engineering and formal methods could design, verify, and implement a complex protection system meeting regulatory criteria at a fraction of typical cost. The project delivered a Reactor Trip System (RTS) implementation with full traceability from NRC Request for Proposals and IEEE standards through formal architecture specifications to verified software.
+HARDENS addressed a fundamental dilemma: existing U.S. nuclear control rooms rely on analog technologies from the 1950s--60s. These technologies incur significant risk and cost compared to modern control systems. The NRC contracted Galois, a formal methods firm, to demonstrate that Model-Based Systems Engineering and formal methods could design, verify, and implement a complex protection system meeting regulatory criteria at a fraction of typical cost. The project delivered a Reactor Trip System (RTS) implementation with full traceability. This traceability spans from NRC Request for Proposals and IEEE standards through formal architecture specifications to verified software.
 
 HARDENS employed formal methods tools and techniques across the verification
 hierarchy. High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
@@ -89,7 +90,7 @@ implementations directly from Cryptol models---eliminating the traditional gap
 between specification and implementation where errors commonly arise.
 
 Despite its accomplishments, HARDENS has a fundamental limitation for hybrid control synthesis: the project addressed only discrete digital control logic. Continuous reactor dynamics remained unmodeled and unverified.
-The Reactor Trip System specification and verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). Continuous reactor physics remained unaddressed. Real reactor safety depends on interactions between continuous processes—temperature, pressure, neutron flux—evolving in response to discrete control decisions. HARDENS verified the discrete controller in isolation. The closed-loop hybrid system behavior remained unverified.
+The Reactor Trip System specification and verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). Continuous reactor physics remained unaddressed. Real reactor safety depends on interactions between continuous processes—temperature, pressure, neutron flux—evolving in response to discrete control decisions. HARDENS verified the discrete controller in isolation, leaving the closed-loop hybrid system behavior unverified.
 
 \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
 continuous dynamics or hybrid system verification.} Verifying discrete control
@@ -161,10 +162,8 @@ This section addressed two Heilmeier questions: What has been done? What are the
 
 \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{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: economic necessity and technical maturity. Small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants, while formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
+This verification gap is both clear and consequential. Economic pressures demand autonomous control. Technical maturity now enables it. 
 
-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? Why will it succeed?—by presenting the technical approach that closes this gap.
-
-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

@@ -4,9 +4,9 @@
 
 This section presents the complete technical approach for synthesizing provably correct hybrid controllers from operating procedures. 
 
-\textbf{What is new:} Three innovations enable compositional verification bridging discrete synthesis with continuous control: contract-based decomposition, mode classification, and procedure-driven structure. 
+\textbf{What is new:} Three innovations enable compositional verification. They bridge discrete synthesis with continuous control: contract-based decomposition, mode classification, and procedure-driven structure. 
 
-\textbf{Why it will succeed:} The approach leverages existing procedural structure, bounds computational complexity through mode-level verification, and validates against real industrial hardware through Emerson collaboration.
+\textbf{Why it will succeed:} The approach leverages existing procedural structure. It bounds computational complexity through mode-level verification. It validates against real industrial hardware through Emerson collaboration.
 
 % ============================================================================
 % STRUCTURE (maps to Thesis.RA tasks):
@@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified either 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, and both consume enormous resources.
+Previous approaches verified either 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, formalizing reactor operations as hybrid automata.
+This approach bridges that gap by composing formal methods with control-theoretic verification and 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. 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.
+This methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately, then composes them to guarantee correctness 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,23 +58,23 @@ 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 either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently and 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 either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation. Reactive synthesis, reachability analysis, and barrier certificates exist independently. No one has integrated them into a systematic design methodology spanning from procedures to verified implementation.
 
 Three innovations enable compositional verification:
 
 \begin{enumerate}
-\item \textbf{Contract-based decomposition:} Instead of attempting global hybrid system verification, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems.
+\item \textbf{Contract-based decomposition:} Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems and replacing traditional global hybrid system verification.
-\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to match each mode type and enabling mode-local analysis with provable composition guarantees.
+\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory. This classification matches appropriate verification tools to each mode type and enables mode-local analysis with provable composition guarantees.
-\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, providing existing structure that avoids artificial abstractions and makes the approach tractable for complex systems like nuclear reactor startup.
+\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This existing structure avoids artificial abstractions and makes the approach tractable for complex systems like nuclear reactor startup.
 \end{enumerate}
 
-\textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed.
+\textbf{Why will it succeed?} Three factors ensure practical feasibility.
 
-\textbf{Existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions, enabling domain experts to adopt the methodology without formal methods training.
+First, \textit{existing structure}: Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions. Domain experts can adopt the methodology without formal methods training.
 
-\textbf{Bounded complexity:} Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. This decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
+Second, \textit{bounded complexity}: Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. This decomposition bounds computational complexity. It transforms an intractable global problem into tractable local verifications.
 
-\textbf{Industrial validation:} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints rather than just theoretical correctness.
+Third, \textit{industrial validation}: The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. This ensures solutions address real deployment constraints—not just theoretical correctness.
 
 These factors combine to demonstrate feasibility on production control systems with realistic reactor models—not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence.
 
@@ -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. But 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 provides the mathematical structure for hybrid control, but a critical question remains: where do these formal descriptions originate?
 
-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.
+The answer lies in existing practice: nuclear operations already possess a natural hybrid structure that maps directly to the formalism through three control scopes: strategic, operational, and tactical. The approach constructs formal hybrid systems from existing operational knowledge, leveraging decades of domain expertise already encoded in operating procedures without 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.
 
@@ -190,7 +190,7 @@ This structure reveals why the operational and tactical levels fundamentally for
 \end{figure}
 
 
-This operational control level explains why nuclear control requires human operators: the hybrid nature of this control system makes proving controller performance against strategic requirements difficult, and no unified infrastructure exists for building and verifying hybrid systems. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature by following prescriptive operating manuals where strict procedures govern what control to implement at any given time.
+This operational control level explains why nuclear control requires human operators. The hybrid nature makes proving controller performance against strategic requirements difficult. No unified infrastructure exists for building and verifying hybrid systems. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature. They follow prescriptive operating manuals where strict procedures govern what control to implement at any given time.
 
 These procedures provide the key to HAHACS construction, which leverages two observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins, meaning a HAHACS's intended behavior can be completely specified before implementation. Requirements define the behavior of any control system: statements about what
 the system must do, must not do, and under what conditions. For nuclear systems,
@@ -236,7 +236,7 @@ eventually reaches operating temperature''), and response properties (``if
 coolant pressure drops, the system initiates shutdown within bounded time'').
 
 
-I use FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language. It enables rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: the current nuclear workforce can adopt these tools without extensive formal methods training.
+This methodology uses FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language. It enables rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: the current nuclear workforce can adopt these tools without extensive formal methods training.
 
 FRET's key feature is its ability to start with logically imprecise
 statements and refine them consecutively into well-posed specifications. We
@@ -260,14 +260,14 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 \subsection{Discrete Controller Synthesis}
 
-The previous subsection demonstrated how operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do—but a critical gap remains: how do we implement those requirements?
+The previous subsection demonstrated how operating procedures translate into temporal logic specifications using FRET, defining what the system must do. A critical gap remains: how do we implement those requirements?
 
-Reactive synthesis bridges this gap by automatically constructing controllers guaranteed to satisfy temporal logic specifications. It automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. The current discrete state and guard condition status form the input; the next discrete state forms the output.
+Reactive synthesis bridges this gap by automatically constructing controllers guaranteed to satisfy temporal logic specifications. It automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output, where the current discrete state and guard condition status form the input and the next discrete state forms the output.
 
 Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ specifying desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller exists. Unrealizable specifications indicate conflicting or impossible requirements in
 the original procedures—this realizability check catches errors before implementation. 
 
-Reactive synthesis offers a decisive advantage: the discrete automaton is correct by construction and requires no human engineering of its implementation. This eliminates human error at the implementation stage entirely, allowing designers to focus on specifying system behavior rather than implementing switching logic.
+Reactive synthesis offers a decisive advantage. The discrete automaton is correct by construction. It requires no human engineering of its implementation. This eliminates human error at the implementation stage entirely. Designers focus on specifying system behavior rather than implementing switching logic.
 
 This shift carries two critical implications. First, complete traceability: the controller changes between modes for reasons that trace back through specifications to requirements. This establishes clear liability and justification for system behavior. Second, deterministic guarantees replace probabilistic human judgment. Human operators cannot eliminate error from discrete control decisions. Humans are intrinsically fallible. Temporal logics define system behavior. Deterministic algorithms synthesize the controller. Strategic decisions follow operating procedures exactly—no exceptions, no deviations, no human factors.
 
@@ -275,7 +275,7 @@ The synthesized automaton translates directly to executable code through standar
 
 Reactive synthesis has proven successful in robotics, avionics, and industrial control. Recent applications synthesize robot motion planners from natural language specifications. They generate flight control software for unmanned aerial vehicles. They create verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
 
-Reactive synthesis produces discrete mode-switching logic from procedures. The next subsection addresses what executes within each discrete mode: continuous control and its verification.
+Reactive synthesis produces discrete mode-switching logic from procedures. This solves half the hybrid control problem: determining when to switch modes. The next subsection addresses the other half: what executes within each discrete mode and how to verify it.
 
 %%% NOTES (Section 3):
 % - Mention computational complexity of synthesis (doubly exponential worst case)
@@ -289,11 +289,11 @@ Reactive synthesis produces discrete mode-switching logic from procedures. The n
 
 \subsection{Continuous Control Modes}
 
-Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. However, hybrid control requires more than correct mode switching—the continuous dynamics executing within each discrete mode must also verify against requirements.
+Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. This solves half the hybrid control problem. The other half remains: the continuous dynamics executing within each discrete mode must also verify against requirements.
 
-Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to its distinct purpose. This subsection describes each type and its verification method. 
+Control objectives determine the verification approach. This work classifies modes into three types: transitory, stabilizing, and expulsory. Each type requires different verification tools matched to its distinct purpose. This subsection describes each type and its verification method. 
 
-This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification, which confirms whether an implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that capability exists. The contribution lies in the verification framework confirming that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
+This methodology's scope requires clarification. This work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking confirms whether an implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques. This work assumes that capability exists. The contribution lies in the verification framework. It confirms that 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
@@ -310,7 +310,7 @@ the vector fields at discrete state interfaces makes reachability analysis
 computationally expensive, and analytic solutions often become intractable
 \cite{MANYUS THESIS}.
 
-I circumvent these issues by designing the hybrid system from the bottom up with verification in mind. The discrete transitions define each continuous control mode's input and output sets clearly \textit{a priori}.
+This methodology circumvents these issues by designing the hybrid system from the bottom up with verification in mind. The discrete transitions define each continuous control mode's input and output sets clearly \textit{a priori}.
 
 Each discrete mode $q_i$ provides
 three key pieces of information for continuous controller design:
@@ -329,9 +329,9 @@ precise objectives for continuous control. The continuous controller for mode
 $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
 state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.
 
-Continuous controllers classify into three types based on control objectives, each requiring distinct verification tools. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. 
+Continuous controllers classify into three types based on control objectives. Each type requires distinct verification tools. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. 
 
-The following subsections detail each mode type and its verification approach, progressing from nominal operations—transitory and stabilizing modes—to off-nominal scenarios handled by expulsory modes.
+The following subsections detail each mode type and its verification approach. We progress from nominal operations—transitory and stabilizing modes—to off-nominal scenarios handled by expulsory modes.
 
 %%% NOTES (Section 4):
 % - Add figure showing the relationship between entry/exit/safety sets
@@ -344,7 +344,7 @@ The following subsections detail each mode type and its verification approach, p
 
 \subsubsection{Transitory Modes}
 
-Transitory modes—the first of three continuous controller types—execute transitions between operating conditions. Their purpose is to move the plant from one discrete operating condition to another. They start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers.
+Transitory modes—the first of three continuous controller types—execute transitions between operating conditions, moving the plant from one discrete operating condition to another. They 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 has a formal statement. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
 \[
@@ -377,7 +377,7 @@ systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool
 depends on the structure of the continuous dynamics. Linear systems admit
 efficient polyhedral or ellipsoidal reachability computations. Nonlinear
 systems require more conservative over-approximations using techniques such as
-Taylor models or polynomial zonotopes. For this work, we will select tools
+Taylor models or polynomial zonotopes. This work will select tools
 appropriate to the fidelity of the reactor models available.
 
 %%% NOTES (Section 4.1):
@@ -392,11 +392,9 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions, and reachability analysis verifies whether the target can be reached.
+While transitory modes drive the system toward exit conditions using reachability analysis to verify whether the target can be reached, stabilizing modes address a different question: rather than "can the system reach a target?" they ask "will the system stay within bounds?" 
 
-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.
+Transitory modes 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: barrier certificates.
-
-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
 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
@@ -445,9 +443,9 @@ controller.
 
 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.
+Real systems deviate from design models. Component failures occur. Sensors degrade. Unanticipated disturbances arise. Expulsory modes address these off-nominal scenarios.
 
-Expulsory controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and controlled depressurization procedures.
+For expulsory modes, robustness matters more than optimality. The control objective shifts from reaching targets or maintaining regions to driving the plant to a safe shutdown state. This must succeed 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.
 
@@ -505,7 +503,7 @@ requirements. The discrete automaton produced by reactive synthesis will be
 compiled to run on Ovation controllers, with verification that the implemented
 behavior matches the synthesized specification exactly.
 
-For the continuous dynamics, we will use a small modular
+For the continuous dynamics, this work will use a small modular
 reactor simulation. The SmAHTR (Small modular Advanced High Temperature
 Reactor) model provides a relevant testbed for startup and shutdown procedures.
 The ARCADE (Advanced Reactor Control Architecture Development Environment)
@@ -513,44 +511,41 @@ interface will establish communication between the Emerson Ovation hardware and
 the reactor simulation, enabling hardware-in-the-loop testing of the complete
 hybrid controller.
 
-Working with Emerson on such an implementation is an incredible advantage for
+Working with Emerson on such an implementation provides an incredible advantage for
-the success and impact of this work. We will directly address the gap of
+the success and impact of this work. The collaboration directly addresses the gap in
-verification and validation methods for these systems and industry adoption by
+verification and validation methods for these systems and industry adoption. It
-forming a two-way exchange of knowledge between the laboratory and commercial
+forms a two-way exchange of knowledge between the laboratory and commercial
-environments. This work stands to be successful with Emerson implementation
+environments. This work stands to succeed with Emerson implementation
-because we will have access to system experts at Emerson to help with the fine
+because it will have access to system experts at Emerson. These experts can help with the fine
-details of using the Ovation system. At the same time, we will have the benefit
+details of using the Ovation system. At the same time, the collaboration will
-of transferring technology directly to industry with a direct collaboration in
+transfer technology directly to industry through direct research participation. This provides an excellent perspective on how research
-this research, while getting an excellent perspective of how our research
+outcomes can best align with customer needs.
-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 by 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. 
 
 First, \textit{contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
 
-Second, \textit{mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
+Second, \textit{mode classification} matches continuous modes to appropriate verification tools. This enables mode-local analysis with provable composition guarantees. 
 
-Third, \textit{procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion.
+Third, \textit{procedure-driven structure} leverages existing procedural decomposition to avoid intractable state explosion.
 
-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.
+Section 2 established that prior work verified discrete logic or continuous dynamics—never both compositionally. These three innovations enable what global analysis cannot: compositional verification spanning from procedures to verified implementation.
 
-\textbf{Why will it succeed?} Three factors ensure practical feasibility: 
+\textbf{Why will it succeed?} Three factors ensure practical feasibility. 
 
-\textit{Existing structure.} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization without artificial abstractions. 
+\textit{Existing structure}: Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This allows formalization without artificial abstractions. 
 
-\textit{Bounded complexity.} Mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. 
+\textit{Bounded complexity}: Mode-level verification bounds each problem locally. This avoids the state explosion that makes global hybrid system analysis intractable. 
 
-\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.
+\textit{Industrial validation}: Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. This ensures solutions address real deployment constraints.
 
-The complete technical methodology is now established. 
+With the complete technical methodology established, Sections 2 and 3 have addressed the first four Heilmeier questions: what has been done, what limits current practice, what is new, and why it will succeed. 
 
-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 and what difference will this work make? 
 
-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 metrics for success. Section 5 identifies what could prevent success. Section 6 explains who cares and what difference this work will 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

@@ -2,13 +2,17 @@
 
 \textbf{Heilmeier Question: How will success be measured?}
 
-Section 3 established the technical approach: compositional verification bridges discrete synthesis with continuous control. It will succeed because it leverages existing procedural structure, bounds computational complexity, and validates against industrial hardware. This section addresses the next Heilmeier question: How will success be measured? 
+Section 3 established the technical approach: compositional verification bridges discrete synthesis with continuous control. It will succeed because it leverages existing procedural structure, bounds computational complexity, and validates against industrial hardware. 
 
-Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5), where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
+This section addresses the next Heilmeier question: How will success be measured? 
+
+Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5). At TRL 5, system components operate successfully in a relevant laboratory environment. 
+
+TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section first explains why TRLs appropriately measure success. It then defines specific criteria for each level from TRL 3 through TRL 5.
 
 Technology Readiness Levels provide the ideal success metric for work bridging academic proof-of-concept and practical deployment. 
 
-Academic metrics—papers published or theorems proved—fail to capture practical feasibility. Empirical metrics—simulation accuracy or computational speed—fail to demonstrate theoretical rigor. TRLs measure both.
+Academic metrics—papers published or theorems proved—fail to capture practical feasibility. Empirical metrics—simulation accuracy or computational speed—fail to demonstrate theoretical rigor. TRLs measure both simultaneously.
 
 Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while progressively demonstrating practical feasibility. The system moves from individual components to integrated hardware testing. Two requirements constrain this progression. First: formal verification must remain valid throughout. Second: the proofs must compose as the system scales.
 
@@ -83,16 +87,16 @@ controllers implementable with current technology.
 
 This section answered the Heilmeier question: How will success be measured?
 
-\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5. Each level demonstrates both theoretical correctness and practical feasibility through progressively integrated validation.
+\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5, where each level demonstrates both theoretical correctness and practical feasibility through progressively integrated validation:
 
-TRL 3 proves component-level correctness: each methodology element works independently.
+TRL 3 proves component-level correctness—each methodology element works independently.
 
-TRL 4 demonstrates system-level integration in simulation: components compose correctly.
+TRL 4 demonstrates system-level integration in simulation—components compose correctly.
 
-TRL 5 validates hardware implementation in a relevant environment: the complete system operates on industrial control hardware.
+TRL 5 validates hardware implementation in a relevant environment—the complete system operates on industrial control hardware.
 
 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. 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.
+Sections 2 through 4 have addressed five Heilmeier questions: what has been done, what limits current practice, what is new, why it will succeed, and how success will be measured.
 
-But success assumes critical technical challenges can be overcome. Section 5 addresses what could prevent success and how to respond when assumptions fail.
+Success, however, assumes critical technical challenges can be overcome. Section 5 addresses what could prevent success and explains how to respond when assumptions fail.

5-risks-and-contingencies/v1.tex

@@ -2,13 +2,11 @@
 
 \textbf{Heilmeier Question: What could prevent success?}
 
-Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. This definition assumes critical technical challenges can be overcome.
+Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. This assumes critical technical challenges can be overcome.
 
-Every research plan rests on assumptions that might prove false. Three primary risks could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization.
+Every research plan rests on assumptions that might prove false. Three primary risks could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization. Each risk has identifiable early warning indicators. Each has viable mitigation strategies. Each has contingency plans that preserve research value even when core assumptions fail. 
 
-Each risk has identifiable early warning indicators and viable mitigation strategies. 
+The staged project structure ensures partial success yields publishable results. It clearly identifies remaining barriers to deployment—even when full success proves elusive.
-
-Each risk carries associated early warning indicators and contingency plans that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results and clearly identifies remaining barriers to deployment, even when full success proves elusive.
 
 \subsection{Computational Tractability of Synthesis}
 
@@ -28,9 +26,9 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-The first risk addressed practical constraints: whether synthesis can complete within reasonable time bounds. The second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
+The first risk addressed practical constraints: whether synthesis can complete within reasonable time bounds. The second risk proves more fundamental. Can boolean guard conditions in temporal logic map cleanly 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 reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction. This would make synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
+This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction, making synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
 
 The risk extends beyond static interface definition to dynamic behavior across transitions. Barrier certificates may fail to exist for proposed transitions. Continuous modes may be unable to guarantee convergence to discrete transition boundaries.
 
@@ -133,15 +131,11 @@ quirks.
 
 This section answered the Heilmeier question: What could prevent success?
 
-\textbf{Answer:} Three primary risks threaten TRL 5 achievement: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization.
+\textbf{Answer:} Three primary risks threaten TRL 5 achievement: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization. Each risk has identifiable early warning indicators enabling detection before failure becomes inevitable, viable mitigation strategies preserving research value even when core assumptions fail, and contingency plans that maintain contribution regardless of which technical obstacles prove insurmountable.
 
-Each risk has identifiable early warning indicators enabling detection before failure becomes inevitable. Each has viable mitigation strategies preserving research value even when core assumptions fail.
+The staged project structure ensures partial success yields publishable results identifying remaining deployment barriers. Even failure advances the field by documenting precisely which barriers remain.
 
-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 have established the complete technical research plan: 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. This section identified what could prevent success and explained how to respond when assumptions fail.
-
-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?
 

6-broader-impacts/v1.tex

@@ -2,41 +2,40 @@
 
 \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-Sections 2 through 5 established the complete technical research plan: what has been done, what is new and why it will succeed, how to measure success, and what could prevent success.
+Sections 2 through 5 established the complete technical research plan. They addressed what has been done, what is new and why it will succeed, how to measure success, and what could prevent success.
 
-This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
+This section addresses the remaining Heilmeier questions. It connects technical methodology to economic and societal impact.
 
-\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive with fossil alternatives. All three require autonomous control with safety guarantees.
+\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to compete economically with fossil alternatives. All three require autonomous control with safety guarantees.
 
-\textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier, enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.
+\textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier. It enables economically viable small modular reactors for datacenter power. It establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure.
 
-\textbf{Why now?} Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis, creating a market demanding solutions that did not exist before.
+\textbf{Why now?} Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis. A market now demands solutions that did not exist before.
 
 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) for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions, but at this scale, nuclear power economics demand careful attention to operating costs.
 
 The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. 
 
-Operations and maintenance represents a substantial component. The EIA estimates fixed O\&M costs alone account for \$16.15 per megawatt-hour. Additional variable O\&M costs are embedded in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent approximately 23--30\% of total levelized cost. This translates to \$21--28 billion annually for projected datacenter demand.
+Operations and maintenance represents a substantial component. The EIA estimates fixed O\&M costs alone account for \$16.15 per megawatt-hour. Variable O\&M costs are embedded in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent approximately 23--30\% of total levelized cost. For projected datacenter demand, this translates to \$21--28 billion annually.
 
 \textbf{What difference will it make?} This research directly addresses the \$21--28 billion annual O\&M cost barrier. High-assurance autonomous control makes small modular reactors economically viable for datacenter power while maintaining nuclear safety standards. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure.
 
 Current nuclear operations require full control room staffing for each reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output. This makes per-megawatt costs prohibitive. These staffing requirements drive the economic challenge threatening SMR deployment for datacenter applications.
 
-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. Operators oversee multiple autonomous reactors rather than manually controlling individual units.
+Synthesizing provably correct hybrid controllers from formal specifications automates routine operational sequences currently requiring 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.
 
 The correct-by-construction methodology proves critical for this transition.
 Traditional automation approaches cannot provide sufficient safety guarantees
-for nuclear applications, where regulatory requirements and public safety
+for nuclear applications. Regulatory requirements and public safety
-concerns demand the highest levels of assurance. By formally verifying both the
+concerns demand the highest levels of assurance. This research formally verifies both the
-discrete mode-switching logic and the continuous control behavior, this research
+discrete mode-switching logic and the continuous control behavior. It
 produces controllers with mathematical proofs of correctness. These
-guarantees enable automation to safely handle routine operations---startup
+guarantees enable automation to safely handle routine operations: startup
-sequences, power level changes, and normal operational transitions---that
+sequences, power level changes, and normal operational transitions. These operations
 currently require human operators to follow written procedures. Operators will
 remain in supervisory roles to handle off-normal conditions and provide
-authorization for major operational changes, but the routine cognitive burden of
+authorization for major operational changes. The routine cognitive burden of
-procedure execution shifts to provably correct automated systems that are much
+procedure execution shifts to provably correct automated systems that cost far less to operate.
-cheaper to operate.
 
 SMRs represent an ideal deployment target for this technology. Nuclear
 Regulatory Commission certification requires extensive documentation of control
@@ -49,31 +48,29 @@ continuous control modes. The infrastructure of requirements and specifications
 already exists as part of the licensing process, creating a direct pathway from
 existing regulatory documentation to formally verified autonomous controllers.
 
-Beyond reducing operating costs for new reactors, this research will establish a
+Beyond reducing operating costs for new reactors, this research establishes a
 generalizable framework for autonomous control of safety-critical systems. The
-methodology of translating operational procedures into formal specifications,
+methodology translates operational procedures into formal specifications. It
-synthesizing discrete switching logic, and verifying continuous mode behavior
+synthesizes discrete switching logic. It verifies continuous mode behavior. This methodology
 applies to any hybrid system with documented operational requirements. Potential
 applications include chemical process control, aerospace systems, and autonomous
-transportation, where similar economic and safety considerations favor increased
+transportation. Similar economic and safety considerations favor increased
-autonomy with provable correctness guarantees. Demonstrating this approach in
+autonomy with provable correctness guarantees in these domains. Demonstrating this approach in
-nuclear power---one of the most regulated and safety-critical domains---will
+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.
 
 
 This section answered three critical Heilmeier questions:
 
-\textbf{Who cares?} Three stakeholder groups face the same constraint. The nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive. All three require autonomous control with safety guarantees.
+\textbf{Who cares?} Three stakeholder groups face the same constraint: the nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs, datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure, and clean energy advocates need nuclear power to be economically competitive. All three require autonomous control with safety guarantees.
 
-\textbf{Why now?} Two forces converge to create urgency. \textit{First: exponentially growing demand.} AI infrastructure creates immediate need for economical nuclear power at datacenter scale. Projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. \textit{Second: technical maturity.} Formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. The problem is urgent. The tools exist.
+\textbf{Why now?} Two forces converge to create urgency. First, \textit{exponentially growing demand}: AI infrastructure creates immediate need for economical nuclear power at datacenter scale, with projections showing datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. Second, \textit{technical maturity}: formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. The problem is urgent and the tools exist.
 
-\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.
+\textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier by enabling 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. 
+Sections 2 through 6 have addressed all but one Heilmeier question: 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.
-
-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.
+Section 8 provides the answer with a detailed schedule of milestones and deliverables.

8-schedule/v1.tex

@@ -2,9 +2,11 @@
 
 \textbf{Heilmeier Question: How long will it take?}
 
-Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. This final section addresses the last Heilmeier question: How long will it take?
+Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. 
 
-This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC Fellowship provide all computational and experimental resources, with work progressing sequentially through three main research thrusts and culminating in integrated demonstration and validation.
+This final section addresses the last Heilmeier question: How long will it take?
+
+This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026, with all computational and experimental resources provided by the University of Pittsburgh Cyber Energy Center and NRC Fellowship. Work progresses sequentially through three main research thrusts, culminating in integrated demonstration and validation.
 
 The first semester (Spring 2026) focuses on Thrust 1, translating startup
 procedures into formal temporal logic specifications using FRET. This