Editorial pass: tactical (Gopen), operational (flow), and strategic (Heilmeier)

Applied Gopen's Sense of Structure principles throughout:
- Combined short choppy sentences for better flow
- Strengthened topic-stress positioning
- Tightened verb choices and reduced passive voice
- Improved paragraph transitions and coherence
- Enhanced document-level Heilmeier alignment
- Removed redundant content (duplicate paragraph in research approach)

All changes preserve technical accuracy while improving clarity and impact.

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,32 +1,33 @@
 % GOAL PARAGRAPH
-This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
+I develop autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors require extensively trained operators who follow detailed written procedures and switch between control objectives based on plant conditions.
+Nuclear reactors today depend on extensively trained human operators who follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening their economic viability. Autonomous control systems can manage complex operational sequences without constant supervision—if they provide assurance equal to or exceeding human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only with safety assurance equal to or exceeding human operators.
 
 % APPROACH PARAGRAPH Solution
-This research combines formal methods from computer science with control theory to build hybrid control systems correct by construction. 
+I produce hybrid control systems correct by construction, unifying formal methods from computer science with control theory. 
 % Rationale
-Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Neither approach alone provides end-to-end correctness guarantees.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both must work together to achieve end-to-end correctness.
 % Hypothesis and Technical Approach
-Three stages bridge this gap. First, written operating procedures translate into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET), which structures requirements into scope, condition, component, timing, and response. Realizability checking identifies conflicts and ambiguities before implementation. Second, reactive synthesis generates deterministic automata—provably correct by construction. Third, standard control theory designs continuous controllers for each discrete mode, which reachability analysis then verifies. Continuous modes classify by transition objectives: transitory modes drive the plant between conditions, stabilizing modes maintain operation within regions, and expulsory modes ensure safety under failures. Assume-guarantee contracts and barrier certificates prove safe mode transitions, enabling local verification without global trajectory analysis. An Emerson Ovation control system demonstrates the methodology. 
+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 provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements each discrete mode imposes. Engineers design these continuous controllers using standard control theory techniques.
+
+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 safe mode transitions, 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 autonomous control approach manages complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability.
+This approach manages complex nuclear power operations autonomously while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS
-If this research is successful, we will be able to do the following:
+This research, if successful, produces three concrete outcomes:
 \begin{enumerate}
   % OUTCOME 1 Title
   \item \textit{Synthesize written procedures into verified control logic.} 
     % Strategy
-    We develop a methodology for converting written operating procedures
+    A methodology converts written operating procedures into formal specifications.
-    into formal specifications. Reactive synthesis tools then generate
+    Reactive synthesis tools then generate discrete control logic from these specifications.
-    discrete control logic from these specifications.
     % Outcome
-    Control engineers can generate mode-switching controllers from regulatory
+    Control engineers generate mode-switching controllers directly from regulatory
-    procedures with minimal formal methods expertise, reducing barriers to
+    procedures. Minimal formal methods expertise required. This reduces barriers to
     high-assurance control systems.
 
     % OUTCOME 2 Title
@@ -36,15 +37,14 @@ If this research is successful, we will be able to do the following:
     transition requirements. 
     % Outcome
     Engineers design continuous controllers using standard practices while
-    maintaining formal correctness guarantees. Mode transitions provably occur safely and at
+    maintaining formal correctness guarantees. Mode transitions occur safely and at
-    the correct times.
+    the correct times—provably.
 
     % OUTCOME 3  Title
   \item \textit{Demonstrate autonomous reactor startup control with safety
     guarantees.}
     % Strategy
-    A small modular reactor simulation using industry-standard control hardware
+    This methodology demonstrates on a small modular reactor simulation using industry-standard control hardware.
-    implements this methodology.
     % Outcome
     Control engineers implement high-assurance autonomous controls on
     industrial platforms they already use, enabling autonomy without retraining

1-goals-and-outcomes/v1.tex

@@ -1,38 +1,36 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops autonomous hybrid control systems with mathematical guarantees of safe and correct behavior.
+I develop autonomous hybrid control systems with 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.
 % Known information
-Nuclear plant operations rely on extensively trained human operators. These operators follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
+Nuclear plants today depend on extensively trained human operators who follow detailed written procedures and strict regulatory requirements. Operators 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 per-megawatt staffing costs far exceeding those of conventional plants—a gap that threatens their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision, but only if they provide 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 far exceeding those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only with safety assurance equal to or exceeding human operators.
 
 % APPROACH PARAGRAPH Solution
-This research combines formal methods with control theory to build hybrid control systems correct by construction.
+I produce hybrid control systems correct by construction, unifying formal methods with control theory.
 % Rationale
-Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Neither approach alone guarantees end-to-end correctness.
+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 handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both approaches must work together to achieve end-to-end correctness.
 % Hypothesis
-This approach closes the gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between transitions. Operating procedures formalize into logical specifications. Continuous dynamics verify against transition requirements. The result: autonomous controllers provably free from design defects. 
+Two steps close this gap. First, discrete mode transitions synthesize directly from written operating procedures. Second, continuous behavior between transitions verifies against discrete requirements. This formalizes operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers 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
+The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation requirements.
-requirements.
 
 % OUTCOMES PARAGRAPHS
-This approach produces three concrete outcomes:
+If successful, this approach produces three concrete outcomes:
 
 \begin{enumerate}
 
   % OUTCOME 1 Title
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
-    We develop a methodology for converting existing written operating
+    A methodology converts existing written operating procedures into formal
-    procedures into formal specifications. Reactive synthesis tools then
+    specifications. Reactive synthesis tools then automatically generate
-    automatically generate discrete control logic from these specifications.
+    discrete control logic from these specifications. Structured intermediate
-    Structured intermediate representations bridge natural language procedures
+    representations bridge natural language procedures and mathematical logic.
-    and mathematical logic.
     % Outcome
     Control system engineers generate verified mode-switching controllers
     directly from regulatory procedures without formal methods expertise,
@@ -41,51 +39,49 @@ This approach produces three concrete outcomes:
     % OUTCOME 2 Title
   \item \textbf{Verify continuous control behavior across mode transitions.}
     % Strategy
-    We establish methods for analyzing continuous control modes to verify
+    Methods for analyzing continuous control modes verify they satisfy
-    they satisfy discrete transition requirements. Classical control theory for
+    discrete transition requirements. Classical control theory handles linear
-    linear systems and reachability analysis for nonlinear dynamics verify
+    systems. Reachability analysis handles nonlinear dynamics. Both verify that
-    that each continuous mode reaches its intended transitions safely.
+    each continuous mode reaches its intended transitions safely.
     % Outcome
-    Engineers design continuous controllers using standard practices while
+    Engineers design continuous controllers using standard practices. Formal correctness guarantees remain intact. Mode transitions occur safely and at the correct times—provably.
-    maintaining formal correctness guarantees. Mode transitions occur safely and at the correct times, provably.
 
     % OUTCOME 3  Title
   \item \textbf{Demonstrate autonomous reactor startup control with safety
     guarantees.}
     % Strategy
-    We apply this methodology to develop an autonomous controller for
+    This methodology applies to autonomous nuclear reactor startup procedures,
-    nuclear reactor startup procedures, implementing it on a small modular
+    demonstrating on a small modular reactor simulation using industry-standard
-    reactor simulation using industry-standard control hardware. This
+    control hardware. The demonstration proves correctness across multiple
-    demonstration proves correctness across multiple coordinated control
+    coordinated control modes from cold shutdown through criticality to power operation.
-    modes from cold shutdown through criticality to power operation.
     % Outcome
-    We demonstrate that autonomous hybrid control can be realized in the
+    Autonomous hybrid control becomes realizable in the nuclear industry with
-    nuclear industry with current equipment, establishing a path toward reduced
+    current equipment, establishing a path toward reduced operator staffing
-    operator staffing while maintaining safety.
+    while maintaining safety.
 
 \end{enumerate}
 
 % IMPACT PARAGRAPH Innovation
 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?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. This work establishes that bridge by treating discrete specifications as contracts that continuous controllers must satisfy. Independent verification of each layer becomes possible while guaranteeing correct composition. Section 2 (State of the Art) examines why prior work has not achieved this integration. Section 3 (Research Approach) details how this integration will be accomplished.
+\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. 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. Section 2 examines why prior work fails at this integration and what limits current practice. Section 3 details what is new in this approach and why it will succeed.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from
-existing procedures with mathematical proofs of correct behavior. High-assurance
+existing procedures with mathematical proofs of correct behavior, making high-assurance
-autonomous control becomes practical for safety-critical applications.
+autonomous control practical for safety-critical applications.
 % Impact/Pay-off
 This capability is essential for the economic viability of next-generation
 nuclear power. Small modular reactors offer a promising solution to growing
-energy demands, but their success depends on reducing per-megawatt operating
+energy demands. Their success depends on reducing per-megawatt operating
-costs through increased autonomy. This research provides the tools to
+costs through increased autonomy. My research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the
 nuclear industry requires. 
 
-These three outcomes establish a complete methodology from regulatory documents to deployed systems. This proposal follows the Heilmeier Catechism, with each section explicitly answering its assigned questions:
+This proposal follows the Heilmeier Catechism. Each section explicitly answers its assigned questions:
 \begin{itemize}
   \item \textbf{Section 2 (State of the Art):} What has been done? What are the limits of current practice?
-  \item \textbf{Section 3 (Research Approach):} What is new? Why will it succeed where prior work has failed?
+  \item \textbf{Section 3 (Research Approach):} What is new? Why will it succeed?
   \item \textbf{Section 4 (Metrics for Success):} How do we measure success?
   \item \textbf{Section 5 (Risks and Contingencies):} What could prevent success?
   \item \textbf{Section 6 (Broader Impacts):} Who cares? Why now? What difference will it make?

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

@@ -1,14 +1,20 @@
 \section{State of the Art and Limits of Current Practice}
 
-\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today and why current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis. First, we examine reactor operators and their operating procedures. Second, we investigate the fundamental limitations of human-based operation. Third, we review formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis.
+\textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
+
+This section examines how nuclear reactors operate today. No current approach provides autonomous control with end-to-end correctness guarantees—neither human-centered operation nor formal methods. 
+
+Three subsections structure this analysis: first, reactor operators and their operating procedures; second, fundamental limitations of human-based operation; third, formal methods approaches that verify discrete logic or continuous dynamics but not both together. 
+
+These limits establish the verification gap that Section 3 addresses.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current practice must be understood before its limits can be identified. This subsection examines the hierarchy of nuclear plant procedures, the role of operators in executing them, and the operational modes that govern reactor control.
+Understanding the limits of current practice requires examining how nuclear plants operate today. Three aspects structure this analysis: the hierarchy of procedures, the role of operators in executing them, and the operational modes that govern reactor control.
 
-Nuclear plant procedures form a hierarchy. Normal operating procedures govern routine operations. Abnormal operating procedures handle off-normal conditions. Emergency Operating Procedures (EOPs) manage design-basis accidents. Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. These 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. 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 relies on expert judgment and simulator validation—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. Yet this rigor cannot provide formal verification of key safety properties. No mathematical proof confirms that procedures cover all possible plant states. No proof verifies that required actions complete within available timeframes. No proof establishes that procedure-set transitions maintain safety invariants.
+Procedure development relies on expert judgment and simulator validation—not formal verification. 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification: no mathematical proofs confirm procedures cover all possible plant states, required actions complete within available timeframes, or transitions between procedure sets maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -19,13 +25,15 @@ invariants. Paper-based procedures cannot ensure correct application. Even
 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, and various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature and compensates for power demand changes through reactivity feedback loops alone. Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times; engineered safety features actuate automatically on accident signals without requiring operator action.
+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.
 
-The division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems 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 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.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. The other half emerges from procedure execution: 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. Human operators determine when and how. Perfect procedures cannot eliminate human error.
+The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. 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. This 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
@@ -35,18 +43,13 @@ 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 motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including 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. They then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a
+Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including 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}. The President's Commission on TMI identified a fundamental ambiguity—placing responsibility for safe power plant operations on the licensee without formally verifying that operators can fulfill this responsibility guarantees nothing. This tension between operational flexibility and safety assurance remains unresolved: the person responsible for reactor safety often becomes the root cause of failure.
-fundamental ambiguity: placing responsibility for safe power plant operations on
-the licensee without formally verifying that operators can fulfill this
-responsibility does not guarantee safety. This tension between operational
-flexibility and safety assurance remains unresolved. The person responsible for
-reactor safety often becomes the root cause of failure.
 
 Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events, compared to approximately 20\% for equipment failures~\cite{WNA2020}. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
 of 190 events at Chinese nuclear power plants from
-2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
+2007--2020~\cite{zhang_analysis_2025} found that active
-errors, while 92\% were associated with latent errors---organizational and
+errors appeared in 53\% of events, while latent errors—organizational and
-systemic weaknesses that create conditions for failure.
+systemic weaknesses that create conditions for failure—appeared in 92\%.
 
 
 \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
@@ -56,9 +59,11 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Current practice reveals two critical limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. Training and procedural improvements cannot solve these problems. What can? Formal methods offer an alternative—mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. 
+The previous two subsections revealed two critical limitations of current practice. First, procedures lack formal verification despite rigorous development processes. Second, human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. 
 
-Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems. This subsection examines two approaches that illustrate this gap: HARDENS, which verified discrete logic without continuous dynamics, and differential dynamic logic, which handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
+Training and procedural improvements cannot solve these problems. They are fundamental limitations, not remediable defects. Formal methods might offer a solution by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems?
+
+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 my research addresses.
 
 \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control}
 
@@ -80,15 +85,8 @@ synthesis generated verifiable C implementations and SystemVerilog hardware
 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 without modeling or verifying continuous reactor dynamics.
+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
+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.
-transitions (trip/no-trip decisions), digital sensor input processing through
-discrete logic, and discrete actuation outputs (reactor trip commands). The
-project did not address the continuous dynamics of nuclear reactor physics. Real
-reactor safety depends on the interaction between continuous
-processes---temperature, pressure, neutron flux---evolving in response to
-discrete control decisions. HARDENS verified the discrete controller in
-isolation, not the closed-loop hybrid system behavior.
 
 \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
 continuous dynamics or hybrid system verification.} Verifying discrete control
@@ -121,7 +119,7 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic without continuous dynamics. Other researchers attacked the problem from the opposite direction: extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). dL introduces two additional operators
+HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. Other researchers attacked the problem from the opposite direction, extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL), which addresses continuous dynamics but encounters different limitations. dL introduces two additional operators
 into temporal logic: the box operator and the diamond operator. The box operator
 \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
 \(\alpha\) always remains within that region. In this way, it is a safety
@@ -154,10 +152,18 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-This section establishes the current state of practice by answering two Heilmeier questions:
+This section answered two Heilmeier questions: What has been done? What are the limits of current practice?
 
-\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis.
+\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations:
+\begin{itemize}
+\item Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate.
+\item HARDENS verified discrete logic but omitted continuous dynamics.
+\item Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis.
+\end{itemize}
+No existing approach addresses both discrete and continuous verification compositionally.
 
-\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This gap between discrete-only formal methods and post-hoc hybrid verification prevents autonomous nuclear control with end-to-end correctness guarantees.
+\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This verification gap prevents autonomous nuclear control with end-to-end correctness guarantees. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-Two imperatives emerge. Economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical imperative: current approaches lack compositional verification for hybrid systems. These limitations define the research opportunity. Section 3 addresses this gap by establishing what makes this approach new and why it will succeed where prior work has failed.
+Two imperatives converge: economic necessity demands solutions (small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants), and technical opportunity enables solutions (formal methods tools have matured to enable compositional hybrid verification). 
+
+Section 3 closes this verification gap by establishing what makes this approach new and why it will succeed.

3-research-approach/v3.tex

@@ -1,5 +1,13 @@
 \section{Research Approach}
 
+\textbf{Heilmeier Questions: What is new? Why will it succeed?}
+
+This section presents the complete technical approach for synthesizing provably correct hybrid controllers from operating procedures. 
+
+\textbf{What is new:} Compositional verification that bridges discrete synthesis with continuous control. Three innovations enable this integration: contract-based decomposition, mode classification, and procedure-driven structure. 
+
+\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 the Emerson collaboration.
+
 % ============================================================================
 % STRUCTURE (maps to Thesis.RA tasks):
 %   1. Introduction + Hybrid Systems Definition (Task 34)
@@ -15,23 +23,15 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees despite consuming 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 work bridges the gap. It composes formal methods from computer science with control-theoretic verification. Reactor operations formalize as hybrid automata.
+My 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: the interaction between discrete and continuous dynamics creates discontinuities in system behavior when discrete transitions change the governing vector field. Traditional verification techniques fail to handle this interaction directly. 
+Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
 
-Our 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 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.
 
-Building a high-assurance hybrid autonomous control system requires
+A high-assurance hybrid autonomous control system requires a mathematical description. This work draws on automata theory, temporal logic, and control theory to provide that description. A hybrid system is a dynamical system with both continuous and discrete states. This proposal addresses continuous autonomous hybrid systems specifically—systems with no external input where continuous states remain continuous when discrete states change, representing physical quantities that remain Lipschitz continuous. This work follows the nomenclature from the Handbook on Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here for convenience:
-a mathematical description of the system. This work draws on
-automata theory, temporal logic, and control theory to provide that description. A hybrid system is a
-dynamical system with both continuous and discrete states. This proposal
-addresses continuous autonomous hybrid systems specifically: systems with no external input where continuous
-states remain continuous when discrete states change. These continuous states represent physical quantities that remain
-Lipschitz continuous. This work follows the nomenclature from the Handbook on
-Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here
-for convenience:
 
 \begin{equation}
   H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta, \mathcal{R}, Inv)
@@ -54,27 +54,27 @@ where:
   \item $Inv$: safety invariants on the continuous dynamics
 \end{itemize}
 
-Creating a HAHACS requires constructing this tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
+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?} Section 2 established that existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. This work composes them into a complete methodology for hybrid control synthesis through three key innovations:
+\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. Prior work has not integrated them into a systematic design methodology. No prior work spans from procedures to verified implementation. 
+
+Three innovations enable this integration:
 
 \begin{enumerate}
-\item \textbf{Contract-based decomposition:} Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of global hybrid system verification.
+\item \textbf{Contract-based decomposition:} This approach inverts the traditional structure. 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{Mode classification:} Continuous modes classify by objective (transitory, stabilizing, expulsory), which selects appropriate verification tools and enables mode-local analysis with provable composition.
+\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to match each mode type. This classification enables mode-local analysis with provable composition guarantees.
-\item \textbf{Procedure-driven structure:} Existing procedural structure avoids global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup.
+\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases. Leveraging this existing structure avoids imposing artificial abstractions, making the approach tractable for complex systems like nuclear reactor startup.
-\end{enumerate}
+\end{enumerate>
 
-No prior work integrates these three techniques into a systematic design methodology that spans procedures to verified implementation.
+\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{First, existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes existing structure without imposing artificial abstractions. Domain experts without formal methods training can adopt it.
 
-\begin{enumerate}
+\textbf{Second, bounded complexity:} Mode-level verification checks each mode against local contracts. This avoids global hybrid system analysis. The decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
-\item Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—this work formalizes existing structure rather than imposing artificial abstractions.
-\item Mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, bounding computational complexity by verifying each mode against local contracts.
-\item The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility.
-\end{enumerate}
 
-This work demonstrates 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.
+\textbf{Third, industrial validation:} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. 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.
 
 \begin{figure} 
   \centering
@@ -140,17 +140,21 @@ This work demonstrates feasibility on production control systems with realistic
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The hybrid automaton formalism provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. But where do these formal descriptions come from? This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure. This structure maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical.
+The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. 
 
-Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making for the plant. Objectives at this level are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. These decisions span months or years. 
+But where do these formal descriptions originate? Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. 
 
-The lowest level—the tactical level—controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control somewhat through what is generally considered ``automatic control.'' These controls are almost always continuous systems with direct impact on the physical state of the plant. Tactical control objectives include maintaining pressurizer level, maintaining core temperature, and adjusting reactivity with chemical shim.
+This approach constructs formal hybrid systems from existing operational knowledge rather than imposing artificial abstractions. It leverages decades of domain expertise already encoded in operating procedures.
 
-The operational control scope links these two extremes, representing the primary responsibility of human operators today. Operational control takes strategic objectives and implements tactical control sequences to achieve them, bridging high-level goals with low-level execution. 
+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.
+
+The tactical level controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems—continuous systems that maintain pressurizer level, core temperature, and reactivity through chemical shim. These systems directly impact the physical state of the plant.
+
+The operational scope links these extremes. It represents the primary responsibility of human operators today. Operators implement tactical control sequences to achieve strategic objectives, bridging high-level goals with low-level execution. 
 
 An example clarifies this three-level structure. Consider a strategic goal to perform refueling at a certain time. The tactical level currently maintains core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this objective.
 
-This structure reveals why the operational and tactical levels fundamentally form a hybrid controller. The tactical level represents continuous plant evolution according to control input and control law. The operational level represents discrete state evolution that determines which tactical control law applies. This operational level becomes the target for autonomous control.
+This structure reveals why the operational and tactical levels fundamentally form a hybrid controller. The tactical level represents continuous plant evolution according to control input and control law. The operational level represents discrete state evolution determining which tactical control law applies. Together, these two levels form the complete hybrid system. This operational level becomes the target for autonomous control because it bridges strategic intent with tactical execution through discrete mode-switching decisions.
 
 
 \begin{figure}
@@ -186,9 +190,9 @@ This structure reveals why the operational and tactical levels fundamentally for
 \end{figure}
 
 
-This operational control level is the main reason nuclear control requires human operators. The hybrid nature of this control system makes proving controller performance against strategic requirements difficult. Unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature. These operators follow prescriptive operating manuals. Strict procedures govern what control to implement at any given time. These procedures provide the key to the operational control scope.
+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, following prescriptive operating manuals where strict procedures govern what control to implement at any given time. These procedures provide the key to the operational control scope.
 
-Constructing a HAHACS leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins. A HAHACS's intended behavior must be completely described before construction. Requirements define the behavior of any control system: statements about what
+A HAHACS construction leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins. A HAHACS's intended behavior must be completely described before construction. 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,
 these requirements derive from multiple sources including regulatory mandates,
 design basis analyses, and operating procedures. The challenge is formalizing
@@ -197,26 +201,23 @@ foundation for autonomous control system synthesis and verification. We can
 build these requirements using temporal logic.
 
 Temporal logic provides powerful semantics for building systems with complex
-but deterministic behavior. It extends classical propositional logic
+but deterministic behavior, extending classical propositional logic with
-with operators that express properties over time. Using temporal logic, we can
+operators that express properties over time. Temporal logic relates discrete
-relate discrete control modes to one another and define all
+control modes to one another and defines all HAHACS requirements. Boundary
-the requirements of a HAHACS. The guard conditions $\mathcal{G}$ are defined by
+conditions between discrete states determine guard conditions $\mathcal{G}$ and
-determining boundary conditions between discrete states and specifying their
+specify their behavior. Continuous mode invariants similarly express as temporal
-behavior. Continuous mode invariants can also be expressed as temporal
+logic statements, forming the basis of any proofs about a
-logic statements. These specifications form the basis of any proofs about a
+HAHACS and constituting fundamental truth statements about designed system behavior.
-HAHACS and constitute the fundamental truth statements about what the behavior
-of the system is designed to be.
 
 Discrete mode transitions include predicates—Boolean functions over the
 continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
 \text{false}\}$. These predicates formalize conditions like ``coolant
 temperature exceeds 315°C'' or ``pressurizer level is between 30\% and 60\%.''
-We do not impose this discrete abstraction artificially. Operating
+This discrete abstraction is not imposed artificially—operating
 procedures for nuclear systems already define go/no-go conditions as discrete
-predicates. Design basis safety analysis determined these thresholds. Decades of operational experience have
+predicates. Design basis safety analysis determined these thresholds; decades of operational experience validated them. Our methodology assumes
-validated them. Our methodology assumes
+this domain knowledge exists and provides a framework to formalize it. The approach proves feasible for nuclear applications because generations
-this domain knowledge exists and provides a framework to formalize it. The approach is feasible for nuclear applications because generations
+of nuclear engineers already completed the hard
-of nuclear engineers have already completed the hard
 work of defining safe operating boundaries. 
 
 Linear temporal logic (LTL) is particularly well-suited for
@@ -235,16 +236,16 @@ eventually reaches operating temperature''), and response properties (``if
 coolant pressure drops, the system initiates shutdown within bounded time'').
 
 
-This work uses FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: reducing required expert knowledge makes these tools adoptable by the current nuclear workforce.
+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.
 
 FRET's key feature is its ability to start with logically imprecise
-statements and refine them consecutively into well-posed specifications. We can
+statements and refine them consecutively into well-posed specifications. We
 leverage this by directly importing operating procedures and design
 requirements into FRET in natural language, then iteratively refining them into
-specifications for a HAHACS. This approach provides two distinct benefits. First, it draws a direct link from design documentation to digital system
+specifications for a HAHACS. This approach provides two distinct benefits: first, it draws a direct link from design documentation to digital system
-implementation. Second, it clearly demonstrates where natural language documents
+implementation; second, it clearly demonstrates where natural language documents
 fall short. Human operators may still use these procedures, making any
-room for interpretation a weakness that must be addressed.
+room for interpretation a weakness requiring correction.
 
 FRET has been successfully applied to spacecraft control systems, autonomous vehicle requirements, and medical device specifications. NASA used FRET for the Lunar Gateway project, formalizing flight software requirements that were previously specified only in natural language. The Defense Advanced Research Projects Agency (DARPA) employed FRET in the Assured Autonomy program to verify autonomous systems requirements. These applications demonstrate FRET's maturity for safety-critical domains. Nuclear control procedures present an ideal use case: they are already structured, detailed, and written to minimize ambiguity—precisely the characteristics that enable successful formalization.
 %%% NOTES (Section 2):
@@ -259,22 +260,23 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 \subsection{Discrete Controller Synthesis}
 
-Temporal logic specifications define what the system must do. The next question is how to implement those requirements. Reactive synthesis provides the answer.
+Operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do, but how do we implement those requirements? Reactive synthesis provides the answer by automatically constructing controllers guaranteed to satisfy temporal logic specifications.
 
-Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. With system requirements defined as temporal logic specifications, reactive synthesis builds the discrete control system. Our systems fit this model: the current discrete state and status of guard conditions form the input, while the next discrete state forms the output. 
+Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. System requirements defined as temporal logic specifications enable reactive synthesis to build the discrete control system. Our systems fit this model: the current discrete state and status of guard conditions form the input, while 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. This realizability check provides immediate value: an
+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
-unrealizable specification indicates conflicting or impossible requirements in
+the original procedures—this realizability check catches errors before implementation. 
-the original procedures, catching errors before implementation. 
 
-Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The resultant automaton is correct by construction. This eliminates human error at the implementation stage entirely. Human designers can focus their effort where it belongs: on specifying system behavior rather than implementing switching logic. 
+Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The automaton is correct by construction. This eliminates human error at the implementation stage entirely. Human designers focus effort where it belongs—on specifying system behavior, not implementing switching logic.
 
-This shift has two critical implications. First, it provides complete traceability. The reasons the controller changes between modes trace back through specifications to requirements, establishing clear liability and justification for system behavior. Second, it replaces probabilistic human judgment with deterministic guarantees. Human operators cannot eliminate error from discrete control decisions. Humans are intrinsically fallible. By defining system behavior using temporal logics and synthesizing the controller using deterministic algorithms, strategic decisions always follow operating procedures exactly—no exceptions, no deviations, no human factors.
+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.
 
-The synthesized automaton translates directly to executable code through standard compilation techniques. Each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees: the implemented code is correct by construction because the automaton it derives from was synthesized to satisfy the temporal logic specifications.
+The synthesized automaton translates directly to executable code through standard compilation techniques. Each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees by ensuring the implemented code is correct by construction—the automaton from which it derives was synthesized to satisfy the temporal logic specifications.
 
 Reactive synthesis has proven successful in robotics, avionics, and industrial control. Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating 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.
+
 %%% NOTES (Section 3):
 % - Mention computational complexity of synthesis (doubly exponential worst case)
 % - Discuss how specification structure affects synthesis tractability
@@ -287,11 +289,11 @@ Reactive synthesis has proven successful in robotics, avionics, and industrial c
 
 \subsection{Continuous Control Modes}
 
-Reactive synthesis produces a provably correct discrete controller from operating procedures—an automaton that determines when to switch between modes. Hybrid control, however, requires more than correct mode switching. The continuous dynamics executing within each discrete mode must also be verified to ensure correct system behavior.
+Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. But hybrid control requires more than correct mode switching. Continuous dynamics executing within each discrete mode must also verify against requirements. Without this continuous verification, the discrete controller cannot guarantee correct system behavior.
 
-This subsection describes the continuous control modes executing within each discrete state and explains how they verify against requirements imposed by the discrete layer. The verification approach depends on control objectives. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
+This subsection describes continuous control modes and their verification. 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 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 verifies whether a given implementation satisfies its specification without prescribing how to write the software. This work assumes engineers design continuous controllers using standard control theory techniques. The contribution provides 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 confirming 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
@@ -308,9 +310,7 @@ the vector fields at discrete state interfaces makes reachability analysis
 computationally expensive, and analytic solutions often become intractable
 \cite{MANYUS THESIS}.
 
-These issues are circumvented by designing the hybrid system from the bottom up
+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}.
-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,7 @@ 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}$.
 
-We classify continuous controllers into three types based on their objectives:
+Continuous controllers classify into three types based on their control objectives, each requiring distinct verification tools matched to its purpose. 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 (expulsory modes).
-transitory, stabilizing, and expulsory. Each type requires distinct verification
-tools matched to its control objective. 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.
 
 %%% NOTES (Section 4):
 % - Add figure showing the relationship between entry/exit/safety sets
@@ -344,27 +342,24 @@ tools matched to its control objective. Transitory modes drive the plant between
 
 \subsubsection{Transitory Modes}
 
-We now examine each of the three continuous controller types in detail, beginning with 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: 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 move the plant from one discrete operating condition to another. Their purpose is to execute transitions: start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers.
+The 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:
-
-We can state the control objective for a transitory mode formally. 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:
 \[
 \forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \mathcal{X}_{exit}
 \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
 \]
-From any valid entry state, the trajectory must eventually reach the
+This requirement is straightforward: from any valid entry state, the trajectory must eventually reach the exit condition without ever leaving the safe region.
-exit condition without ever leaving the safe region.
 
 Reachability analysis provides the natural verification tool for transitory modes.
-Reachability analysis computes the set of all states reachable from a given
+It computes the set of all states reachable from a given
 initial set under the system dynamics. For a transitory mode to be valid, the
 reachable set from $\mathcal{X}_{entry}$ must satisfy two conditions:
 \begin{enumerate}
-  \item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the mode
+  \item The reachable set eventually intersects $\mathcal{X}_{exit}$—the mode
-    achieves its objective)
+    achieves its objective
-  \item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is maintained
+  \item The reachable set never leaves $\mathcal{X}_{safe}$—safety is maintained
-    throughout the transition)
+    throughout the transition
 \end{enumerate}
 Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the states
 reachable within time horizon $T$:
@@ -373,9 +368,7 @@ reachable within time horizon $T$:
 \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset
 \]
 
-The discrete controller defines clear boundaries in continuous state
+The discrete controller defines clear boundaries in continuous state space. This makes the verification problem for each transitory mode well-posed. The possible initial conditions, target conditions, and safety envelope are all known before verification begins. The verification task then confirms that the candidate continuous controller achieves the objective from all possible starting points.
-space, making the verification problem for each transitory mode well-posed. The possible initial conditions, target conditions, and safety envelope are all known. The verification task then confirms that the candidate
-continuous controller achieves the objective from all possible starting points.
 
 Several tools exist for computing reachable sets of hybrid
 systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool
@@ -397,9 +390,11 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Where transitory modes drive the system toward exit conditions, stabilizing modes do the opposite: they 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 drive the system toward exit conditions. They answer: "can we reach the target?"
 
-Reachability analysis answers "can the system reach a target?" Stabilizing modes ask instead "does the system stay within bounds?" Barrier certificates provide the appropriate tool.
+Stabilizing modes address a fundamentally different question: "will we stay within bounds?" These 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
 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
@@ -420,12 +415,7 @@ the time derivative of $B$ is non-negative. Geometrically, this means the
 vector field points inward or tangent to the boundary, never outward. If this
 condition holds, no trajectory starting inside $\mathcal{C}$ can ever leave.
 
-Because the design of the discrete controller defines careful boundaries in
+The discrete controller design defines careful boundaries in continuous state space. Therefore, the barrier is known prior to designing the continuous controller. This eliminates the search for an appropriate barrier. It minimizes complication in validating stabilizing continuous control modes. The discrete specifications tell us what region must be invariant. The barrier certificate then confirms that the candidate controller achieves this invariance.
-continuous state space, the barrier is known prior to designing the continuous
-controller. This eliminates the search for an appropriate barrier and minimizes
-complication in validating stabilizing continuous control modes. The discrete
-specifications tell us what region must be invariant; the barrier certificate
-confirms that the candidate controller achieves this invariance.
 
 Finding barrier certificates can be formulated as a
 sum-of-squares (SOS) optimization problem for polynomial systems, or solved
@@ -451,7 +441,9 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-The first two mode types—transitory and stabilizing—handle nominal operations where plant dynamics match the design model. Expulsory modes handle the opposite case: when the plant deviates from expected behavior. Component failures, sensor degradation, or unanticipated disturbances cause this deviation.
+The first two mode types handle nominal operations. Transitory modes move the plant between conditions. Stabilizing modes maintain the plant within regions. Both assume plant dynamics match the design model. Both assume the plant behaves as expected.
+
+Expulsory modes address a fundamentally 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.
 
 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.
 
@@ -500,7 +492,7 @@ safety margins will matter more than performance during emergency shutdown.
 
 \subsection{Industrial Implementation}
 
-The complete methodology—procedure formalization, discrete synthesis, and continuous verification across three mode types—provides a theoretical framework for hybrid control synthesis. Theory alone, however, does not demonstrate practical feasibility. Validation on realistic systems using industrial-grade hardware is required, advancing from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5).
+The complete methodology—procedure formalization, discrete synthesis, and continuous verification across three mode types—provides a theoretical framework for hybrid control synthesis. But theory alone does not demonstrate practical feasibility. Advancing from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5) requires validation on realistic systems using industrial-grade hardware.
 This research will leverage the University of Pittsburgh Cyber Energy Center's
 partnership with Emerson to implement and test the HAHACS methodology on
 production control equipment. Emerson's Ovation distributed control system is widely deployed
@@ -530,13 +522,17 @@ of transferring technology directly to industry with a direct collaboration in
 this research, while getting an excellent perspective of how our research
 outcomes can align best with customer needs.
 
-This section establishes the research approach by answering two critical Heilmeier questions:
+This section answered two critical Heilmeier questions: What is new? Why will it succeed?
 
-\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations distinguish this approach: using discrete synthesis to define verification contracts (inverting traditional global analysis), classifying continuous modes by objective to select appropriate verification tools, and leveraging existing procedural structure to avoid intractable state explosion. Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. This section demonstrates how compositional verification enables what global analysis cannot achieve.
+\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis through three innovations. First, contract-based decomposition inverts traditional global analysis—discrete synthesis defines verification contracts that bound continuous verification. Second, mode classification enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. Third, procedure-driven structure leverages existing procedural decomposition to avoid intractable state explosion.
 
-\textbf{Why will this approach succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the approach formalizes existing structure rather than imposing artificial abstractions. Second, mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility.
+Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. This compositional verification enables what global analysis cannot achieve.
 
-The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. Sections 2 and 3 have established what has been done, what is new, and why it will succeed. Three critical questions remain for the complete research plan. Section 4 addresses \textit{How will success be measured?} through Technology Readiness Level advancement. Section 5 addresses \textit{What could prevent success?} through risk analysis and contingency planning. Section 6 addresses \textit{Who cares? Why now? What difference will it make?} through economic and societal impact analysis.
+\textbf{Why will this approach succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization of existing structure without imposing artificial abstractions. Second, mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
+
+The complete methodology encompasses procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. 
+
+Three operational questions remain: Section 4 addresses \textit{How will success be measured?} Section 5 addresses \textit{What could prevent success?} Section 6 addresses \textit{Who cares? Why now? What difference will it make?}
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -1,12 +1,18 @@
 \section{Metrics for Success}
 
-\textbf{How do we measure success?} This research advances through Technology Readiness Levels, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
+\textbf{Heilmeier Question: How do we measure success?}
 
-This work begins at TRL 2--3 and aims to reach TRL 5, where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric for this work by bridging the gap between academic proof-of-concept and practical deployment. This section explains why, then defines specific criteria for each level from TRL 3 through TRL 5.
+Section 3 established the technical approach, answering what is new (compositional verification bridging discrete synthesis with continuous control) and why it will succeed (existing procedural structure, bounded complexity, industrial validation). This section addresses the next Heilmeier question: how to measure success. 
 
-Technology Readiness Levels provide the ideal success metric by explicitly measuring the gap between academic proof-of-concept and practical deployment—precisely what this work bridges. Academic metrics like papers published or theorems proved fail to capture practical feasibility. Empirical metrics like simulation accuracy or computational speed fail to demonstrate theoretical rigor. TRLs measure both simultaneously.
+The answer: Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
 
-Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while progressively demonstrating practical feasibility. Formal verification must remain valid as the system moves from individual components to integrated hardware testing.
+My work begins at TRL 2--3 and aims to reach 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 are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5.
+
+Technology Readiness Levels provide the ideal success metric. They explicitly measure the gap between academic proof-of-concept and practical deployment. This is precisely what my work bridges. 
+
+Academic metrics like papers published or theorems proved fail to capture practical feasibility. Empirical metrics like simulation accuracy or computational speed fail to demonstrate theoretical rigor. TRLs measure both.
+
+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.
 
 The nuclear industry requires extremely high assurance before deploying new
 control technologies. Demonstrating theoretical correctness alone proves
@@ -77,6 +83,8 @@ a relevant laboratory environment. This establishes both theoretical validity
 and practical feasibility, proving the methodology produces verified
 controllers implementable with current technology.
 
-This section establishes success criteria by answering the Heilmeier question: \textbf{How do we measure success?} Technology Readiness Level advancement from 2--3 to 5 provides the answer. We measure success by demonstrating both theoretical correctness and practical feasibility through progressively integrated validation. TRL 3 proves component-level correctness. TRL 4 demonstrates system-level integration in simulation. TRL 5 validates hardware implementation in a relevant environment. Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology.
+This section answered the Heilmeier question: How do we measure success?
 
-Reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research could stall at lower readiness levels despite sound methodology. Section 5 addresses the complementary Heilmeier question—\textbf{What could prevent success?}—by identifying primary risks, establishing early warning indicators, and defining contingency plans that preserve research value even when core assumptions fail.
+\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility through progressively integrated validation. TRL 3 proves component-level correctness: each part works independently. TRL 4 demonstrates system-level integration in simulation: the parts compose correctly. TRL 5 validates hardware implementation in a relevant environment: the complete system works on real control hardware. Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology.
+
+Success, however, depends on several critical assumptions. If these assumptions prove false, research could stall at lower readiness levels despite sound methodology. Section 5 addresses the complementary question: What could prevent success?

5-risks-and-contingencies/v1.tex

@@ -1,10 +1,16 @@
 \section{Risks and Contingencies}
 
-\textbf{What could prevent success?} Every research plan rests on assumptions. When those assumptions prove false, research must adapt. Four primary risks could prevent successful completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration. Each risk carries associated early warning indicators and contingency plans that preserve research value even when core assumptions prove false. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment.
+\textbf{Heilmeier Question: What could prevent success?}
+
+Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration.
+
+Every research plan rests on assumptions that might prove false. This section identifies four primary risks that could prevent successful completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. 
+
+Each risk 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}
 
-The first major assumption is that formalized startup procedures will yield automata small enough for efficient synthesis and verification. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states, requiring synthesis times that exceed days or weeks and prevent demonstration of the complete methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives.
+Computational tractability represents the first major risk. The assumption: formalized startup procedures will yield automata small enough for efficient synthesis and verification. This assumption may fail. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications from complete startup procedures may produce automata with thousands of states. Synthesis times may exceed days or weeks, preventing completion within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets
@@ -20,9 +26,11 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-While computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint—the second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
+Computational tractability addresses a practical constraint: 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. 
 
-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.
+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. This would make 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.
 
 Early indicators of interface formalization problems would appear during both
 synthesis and verification phases. Guard conditions requiring complex nonlinear
@@ -122,6 +130,16 @@ extensions, ensuring they address industry-wide practices rather than specific
 quirks.
 
 
-This section identifies barriers to success by answering the Heilmeier question \textbf{What could prevent success?} Four primary risks threaten project completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment—even when core assumptions prove invalid, the research produces valuable contributions that advance the field.
+This section answered the Heilmeier question: What could prevent success?
 
-The technical research plan is now complete. What will be done (Section 3), how success will be measured (Section 4), and what might prevent it (this section) have been established. One critical Heilmeier question remains: \textbf{Who cares? Why now? What difference will it make?} Section 6 answers by connecting this technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector.
+\textbf{Answer:} Four primary risks threaten project completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. 
+
+Each risk has identifiable early warning indicators enabling detection before failure becomes inevitable. Each risk has viable mitigation strategies preserving research value even when core assumptions fail. 
+
+The staged project structure ensures partial success yields publishable results. It identifies remaining barriers to deployment. This design feature maintains contribution regardless of which technical obstacles prove insurmountable. Even "failure" advances the field by documenting precisely which barriers remain.
+
+The technical research plan is complete. Section 3 established what will be done and why it will succeed. Section 4 established how to measure success. This section established what might prevent success and how to mitigate risks. 
+
+One critical Heilmeier question remains: Who cares? Why now? What difference will it make? 
+
+Section 6 connects this technical methodology to urgent economic and infrastructure challenges.

6-broader-impacts/v1.tex

@@ -1,27 +1,33 @@
 \section{Broader Impacts}
 
-\textbf{Who cares? Why now? What difference will it make?} These three Heilmeier questions connect technical methodology to economic and societal impact. Sections 2--5 established the technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how success will be measured (Section 4), and what could prevent success (Section 5). This section addresses the remaining Heilmeier questions by connecting the technical methodology to urgent economic and infrastructure challenges.
+\textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-Three stakeholder groups face the same economic constraint: the nuclear industry, datacenter operators, and clean energy advocates. All confront high operating costs driven by staffing requirements. AI infrastructure demands, growing exponentially, have made this constraint urgent.
+Sections 2--5 established the complete technical research plan. Section 2 answered what has been done and identified the limits of current practice. Section 3 answered what is new and why it will succeed. Section 4 answered how success will be measured through TRL advancement. Section 5 answered what could prevent success and provided mitigation strategies for each risk.
 
-Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence infrastructure has renewed focus on small modular reactors (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. Deploying SMRs at datacenter sites minimizes transmission losses and eliminates emissions. However, nuclear power economics at this scale demand careful attention to operating costs.
+This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact.
+
+Three stakeholder groups converge on one 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 viable.
+
+This research directly addresses a \$21--28 billion annual cost barrier by enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.
+
+Why now? Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis. This creates a market demanding 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), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions. At this scale, however, 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 that fixed O\&M costs alone account for \$16.15 per megawatt-hour, with additional variable O\&M costs embedded in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent approximately 23--30\% of total levelized cost, translating to \$21--28 billion annually for projected datacenter demand.
 
 \textbf{What difference will it make?} This research directly addresses the \$21--28 billion annual O\&M cost challenge. High-assurance autonomous control makes small modular reactors economically viable for datacenter power while maintaining nuclear safety standards.
 
-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, which makes per-megawatt costs prohibitive. These staffing requirements drive the economic challenge that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal
+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 that threatens SMR deployment for datacenter applications.
-specifications automates routine operational sequences that currently require
-constant human oversight. This enables a fundamental shift from direct operator
-control to supervisory monitoring, where operators oversee multiple autonomous
-reactors rather than manually controlling individual units.
 
-The correct-by-construction methodology is critical for this transition.
+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.
+
+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
 concerns demand the highest levels of assurance. By formally verifying both the
 discrete mode-switching logic and the continuous control behavior, this research
-will produce controllers with mathematical proofs of correctness. These
+produces controllers with mathematical proofs of correctness. These
 guarantees enable automation to safely handle routine operations---startup
 sequences, power level changes, and normal operational transitions---that
 currently require human operators to follow written procedures. Operators will
@@ -54,12 +60,14 @@ establish both the technical feasibility and regulatory pathway for broader
 adoption across critical infrastructure.
 
 
-This section establishes impact by answering three critical Heilmeier questions:
+This section answered three critical Heilmeier questions: Who cares? Why now? What difference will it make?
 
 \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 groups need autonomous control with safety guarantees.
 
-\textbf{Why now?} Two forces converge to make this research urgent. First, exponentially growing AI infrastructure demands have created immediate need for economical nuclear power at datacenter scale. Projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. Second, formal methods tools have matured to where compositional hybrid verification has become computationally achievable—what was theoretically possible but practically intractable a decade ago is now feasible.
+\textbf{Why now?} Two forces converge. First, exponentially growing AI infrastructure demands create immediate need for economical nuclear power at datacenter scale. Projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. Second, 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{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.
+\textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier. It 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. Impact extends beyond nuclear power to any safety-critical system requiring provable correctness.
 
-The complete research plan now spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains: \textbf{How long will it take?} Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement, demonstrating the proposed work is achievable within a doctoral timeline.
+The complete research plan spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains: How long will it take? 
+
+Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement, demonstrating the proposed work is achievable within a doctoral timeline.

8-schedule/v1.tex

@@ -1,6 +1,10 @@
 \section{Schedule, Milestones, and Deliverables}
 
-\textbf{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. The University of Pittsburgh Cyber Energy Center and NRC Fellowship provide all computational and experimental resources. The work progresses sequentially through three main research thrusts, culminating in integrated demonstration and validation.
+\textbf{Heilmeier Question: How long will it take?}
+
+The complete research plan is now established. Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. The final Heilmeier question addresses timing and feasibility within a doctoral timeline.
+
+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. The 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