1-goals-and-outcomes/research_statement_v1.tex

@@ -1,19 +1,19 @@
 % GOAL PARAGRAPH
-I develop autonomous control systems that guarantee safe and correct behavior mathematically.
+I develop autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 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: 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 if safety assurance equals or exceeds that of human operators.
+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
-I produce hybrid control systems that are correct by construction, unifying formal methods from computer science with control theory. 
+I produce hybrid control systems correct by construction, unifying formal methods from computer science with control theory. 
 % Rationale
-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. Achieving end-to-end correctness requires both approaches working together.
+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, 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 exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements imposed by each discrete mode. Engineers design these continuous controllers using standard control theory techniques.
+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. I demonstrate this methodology on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
+Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove 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 approach manages complex nuclear power operations autonomously while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 

1-goals-and-outcomes/v1.tex

@@ -1,21 +1,21 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops autonomous hybrid control systems that guarantee safe and correct behavior mathematically.
+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 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, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs 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 work produces hybrid control systems that are correct by construction, unifying formal methods with control theory.
+I produce hybrid control systems correct by construction, unifying formal methods with control theory.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Achieving end-to-end correctness requires both approaches working together.
+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
-Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics, producing 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 requirements.
 
@@ -27,7 +27,7 @@ If successful, this approach produces three concrete outcomes:
   % OUTCOME 1 Title
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
-    A methodology converts written operating procedures into formal
+    A methodology converts existing written operating procedures into formal
     specifications. Reactive synthesis tools then automatically generate
     discrete control logic from these specifications. Structured intermediate
     representations bridge natural language procedures and mathematical logic.
@@ -39,12 +39,12 @@ If successful, this approach produces three concrete outcomes:
     % OUTCOME 2 Title
   \item \textbf{Verify continuous control behavior across mode transitions.}
     % Strategy
-    Methods for analyzing continuous control modes verify that they satisfy
+    Methods for analyzing continuous control modes verify they satisfy
     discrete transition requirements. Classical control theory handles linear
-    systems, while reachability analysis handles nonlinear dynamics. Both verify that
+    systems. Reachability analysis handles nonlinear dynamics. Both verify that
     each continuous mode reaches its intended transitions safely.
     % Outcome
-    Engineers design continuous controllers using standard practices while maintaining formal correctness guarantees. Mode transitions occur safely and at the correct times—provably.
+    Engineers design continuous controllers using standard practices. Formal correctness guarantees remain intact. Mode transitions occur safely and at the correct times—provably.
 
     % OUTCOME 3  Title
   \item \textbf{Demonstrate autonomous reactor startup control with safety
@@ -64,7 +64,7 @@ If successful, this approach produces three concrete outcomes:
 % 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?} 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, while control theory verifies continuous dynamics. Section 2 examines why prior work fails at this integration and identifies the limits of current practice. Section 3 details what is new in this approach and why it will succeed.
+\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
@@ -72,7 +72,7 @@ existing procedures with mathematical proofs of correct behavior, making high-as
 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, in particular, offer a promising solution to growing
+nuclear power. Small modular reactors offer a promising solution to growing
 energy demands. Their success depends on reducing per-megawatt operating
 costs through increased autonomy. My research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the

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

@@ -2,22 +2,23 @@
 
 \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
 
-No current approach provides autonomous control with end-to-end correctness guarantees. This section examines why: human-centered operation cannot eliminate reliability limits, and formal methods verify discrete or continuous behavior but never both. 
+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.
+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. 
 
-Section 3 addresses the verification gap these limits establish.
+These limits establish the verification gap that Section 3 addresses.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current practice rests on two critical components: procedures and operators. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection then examines operators—their reliability limits and contribution to accidents.
+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 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. 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 that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets 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.} No proof exists that procedures cover all
+and completeness.} Current procedure development relies on expert judgment and
+simulator validation—not mathematical proof. No proof exists that procedures cover all
 possible plant states, that required actions complete within available
 timeframes, or that transitions between procedure sets maintain safety
 invariants. Paper-based procedures cannot ensure correct application. Even
@@ -30,9 +31,9 @@ This division between automated and human-controlled functions reveals the funda
 
 \subsection{Human Factors in Nuclear Accidents}
 
-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.
+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. While procedures define what to do, operators determine when and how to act. This human discretion introduces persistent failure modes that training alone cannot eliminate.
+Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. 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
@@ -42,9 +43,9 @@ 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 the need for 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.
+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.
 
-Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events, while equipment failures account for approximately 20\%~\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
+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 active
 errors appeared in 53\% of events, while latent errors—organizational and
@@ -58,11 +59,11 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The previous two subsections established two fundamental limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints, not remediable defects.
+The previous 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. 
 
-Formal methods could potentially eliminate both limitations by providing mathematical guarantees of correctness. However, even the most advanced formal methods applications in nuclear control leave a critical verification gap.
+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?
 
-This subsection examines two approaches illustrating this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
+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}
 
@@ -118,11 +119,11 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. Other researchers have attacked the problem from the opposite direction by 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
+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
-invariant being enforced for the system. The second operator, the diamond
+ivariant being enforced for the system. The second operator, the diamond
 operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
 one trajectory of \(\alpha\) that enters that region. This is a declaration of a
 liveness property. 
@@ -138,7 +139,7 @@ non-terminating solutions prevent creating system proofs using dL.
 %gyroscopes overloding and needing to dump speed all the time
 Approaches have been made to alleviate
 these issues for nuclear power contexts using contract and decomposition based
-methods, but fall far short of a complete design methodology.
+methods, but are far from a complete methodology to design systems with.
 %source: Manyu's thesis. 
 Instead, these approaches have been used on systems that have been designed a
 priori, and require expert knowledge to create the system proofs. 
@@ -153,16 +154,16 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 This section answered two Heilmeier questions: What has been done? What are the limits of current practice?
 
-\textbf{What has been done?} Three approaches currently exist:
+\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.
+\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.
+\item Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis.
 \end{itemize}
-Each approach has fundamental limitations. None addresses both discrete and continuous verification compositionally.
+No existing approach addresses both discrete and continuous verification compositionally.
 
-\textbf{What are the limits of current practice?} The verification gap emerges clearly: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics but never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
+\textbf{What are the limits of current practice?} 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 forces create urgency. Economic necessity demands solutions: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity enables solutions: formal methods tools have matured to enable compositional hybrid verification.
+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 is new and why the approach will succeed.
+Section 3 closes this verification gap by establishing what makes this approach new and why it will succeed.

3-research-approach/v3.tex

@@ -23,17 +23,15 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified discrete switching logic or continuous control behavior but never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees, and both consume enormous resources.
+Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources.
 
-This approach bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
+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: 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.
 
-This methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active. Continuous controllers govern plant behavior within each mode.
+This methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active; continuous controllers govern plant behavior within each mode.
 
-Hybrid systems require mathematical formalization. This work draws on automata theory, temporal logic, and control theory to provide that description.
+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 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. 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)
@@ -58,23 +56,23 @@ where:
 
 A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new in this research?} Existing approaches verify discrete logic or continuous dynamics but 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 spanning from procedures to verified implementation.
+\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation. Reactive synthesis, reachability analysis, and barrier certificates exist independently. 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:} 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 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:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This existing structure avoids artificial abstractions, 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>
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed.
 
-\textbf{First, existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions. Domain experts without formal methods training can adopt it.
+\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.
 
 \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.
 
-\textbf{Third, industrial validation:} The Emerson collaboration provides domain expertise to validate procedure formalization. It provides industrial hardware to demonstrate implementation feasibility. Solutions address real deployment constraints, not just theoretical correctness.
+\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.
 
@@ -142,9 +140,11 @@ These factors combine to demonstrate feasibility on production control systems w
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. A critical question remains: where do these formal descriptions originate?
+The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. 
 
-The answer lies in existing practice. Nuclear operations already possess a natural hybrid structure. This structure maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. 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.
+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. 
+
+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.
 
 Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years, managing labor needs and supply chains to optimize scheduled maintenance and downtime.
 
@@ -190,7 +190,7 @@ This structure reveals why the operational and tactical levels fundamentally for
 \end{figure}
 
 
-This operational control level explains why nuclear control requires human operators: the hybrid nature of this control system makes proving controller performance against strategic requirements difficult, and no unified infrastructure exists for building and verifying hybrid systems. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature by following prescriptive operating manuals where strict procedures govern what control to implement at any given time. 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.
 
 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,
@@ -260,11 +260,9 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 \subsection{Discrete Controller Synthesis}
 
-Operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do, but a critical gap remains: how do we implement those requirements?
+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 bridges this gap 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. 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 automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. Temporal logic specifications enable reactive synthesis to construct the discrete control system automatically. The current discrete state and status of guard conditions form the input; the next discrete state forms the output.
 
 Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ specifying desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller exists. Unrealizable specifications indicate conflicting or impossible requirements in
 the original procedures—this realizability check catches errors before implementation. 
@@ -291,11 +289,11 @@ Reactive synthesis produces discrete mode-switching logic from procedures. The n
 
 \subsection{Continuous Control Modes}
 
-Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. However, hybrid control requires more than correct mode switching—the continuous dynamics executing within each discrete mode must also verify against requirements.
+Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. 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.
 
-Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to its distinct purpose. This subsection describes each type and its verification method. 
+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 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 that confirms 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
@@ -344,7 +342,7 @@ Continuous controllers classify into three types based on their control objectiv
 
 \subsubsection{Transitory Modes}
 
-Transitory modes—the first of three continuous controller types—execute transitions between operating conditions. Their purpose is to move the plant from one discrete operating condition to another. They start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers.
+Transitory modes—the first of three continuous controller types—execute transitions between operating conditions. 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.
 
 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:
 \[
@@ -392,7 +390,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions and answer one question: "can we reach the target?"
+Transitory modes drive the system toward exit conditions. They answer: "can we reach the target?"
 
 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.
 
@@ -443,9 +441,9 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-The first two mode types handle nominal operations. Transitory modes move the plant between conditions, while stabilizing modes maintain the plant within regions. Both assume the plant dynamics match the design model and that the plant behaves as expected.
+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 by handling 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 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.
 
@@ -526,27 +524,15 @@ outcomes can align best with customer needs.
 
 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 through three innovations: 
+\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.
 
-\textit{First: contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
+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.
 
-\textit{Second: mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
+\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.
 
-\textit{Third: procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion.
+The complete methodology encompasses procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. 
 
-Section 2 established that prior work verified discrete logic or continuous dynamics but never both compositionally. This compositional verification enables what global analysis cannot achieve.
+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?}
-
-\textbf{Why will this approach succeed?} Three factors ensure practical feasibility: 
-
-\textit{First: existing structure.} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization of existing structure without imposing artificial abstractions. 
-
-\textit{Second: bounded complexity.} Mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. 
-
-\textit{Third: industrial validation.} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
-
-The complete technical methodology is now established. Section 2 answered what has been done and what limits current practice. This section answered what is new and why it will succeed.
-
-Three critical questions remain. Section 4 addresses measurement: \textit{How will success be measured?} Section 5 addresses risks: \textit{What could prevent success?} Section 6 addresses impact: \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

@@ -2,15 +2,15 @@
 
 \textbf{Heilmeier Question: How do we measure success?}
 
-Section 3 established the technical approach and answered what is new: compositional verification bridging discrete synthesis with continuous control. It answered why the approach will succeed: existing procedural structure, bounded complexity, and industrial validation. This section addresses the next Heilmeier question: how to measure success. 
+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. 
 
-Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
+The answer: Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
 
-This work begins at TRL 2--3 and targets TRL 5, where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric: it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
+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 for work that bridges the gap between academic proof-of-concept and practical deployment. 
+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—papers published or theorems proved—fail to capture practical feasibility. Empirical metrics—simulation accuracy or computational speed—fail to demonstrate theoretical rigor. TRLs measure both.
+Academic metrics 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.
 
@@ -85,14 +85,6 @@ controllers implementable with current technology.
 
 This section answered the Heilmeier question: How do we measure success?
 
-\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5. Each level demonstrates both theoretical correctness and practical feasibility through progressively integrated validation.
+\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5 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.
 
-TRL 3 proves component-level correctness. Each methodology element works independently.
+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?
-
-TRL 4 demonstrates system-level integration in simulation. Components compose correctly.
-
-TRL 5 validates hardware implementation in a relevant environment. The complete system operates on industrial control hardware.
-
-Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology—not merely theoretically sound but practically deployable.
-
-Success assumes critical technical challenges can be overcome. Section 5 addresses the complementary question: What could prevent success?

5-risks-and-contingencies/v1.tex

@@ -2,15 +2,15 @@
 
 \textbf{Heilmeier Question: What could prevent success?}
 
-Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome.
+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 three primary risks that could prevent reaching TRL 5. First: computational tractability of synthesis and verification. Second: complexity of the discrete-continuous interface. Third: completeness of procedure formalization. 
+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}
 
-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.
+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
@@ -28,7 +28,7 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 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, while continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction. This would make synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
+This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction. 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.
 
@@ -132,14 +132,14 @@ quirks.
 
 This section answered the Heilmeier question: What could prevent success?
 
-\textbf{Answer:} Three primary risks threaten TRL 5 achievement. First: computational tractability of synthesis and verification. Second: complexity of the discrete-continuous interface. Third: completeness of procedure formalization.
+\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 has viable mitigation strategies preserving research value even when core assumptions fail.
+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 identifying remaining deployment barriers. This design maintains contribution regardless of which technical obstacles prove insurmountable. Even "failure" advances the field by documenting precisely which barriers remain.
+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: what will be done and why it will succeed (Section 3), how to measure success (Section 4), what might prevent success (this section).
+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 question remains: Who cares? Why now? What difference will it make?
+One critical Heilmeier question remains: Who cares? Why now? What difference will it make? 
 
-Section 6 connects this technical methodology to urgent economic challenges.
+Section 6 connects this technical methodology to urgent economic and infrastructure challenges.

6-broader-impacts/v1.tex

@@ -2,23 +2,23 @@
 
 \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-Sections 2--5 established the complete technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how to measure success (Section 4), and what could prevent success (Section 5).
+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.
 
-This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
+This section addresses the remaining Heilmeier questions 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, creating a market demanding solutions that did not exist before.
+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, nuclear power economics demand careful attention to operating costs.
+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 barrier. High-assurance autonomous control makes small modular reactors economically viable for datacenter power while maintaining nuclear safety standards. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure.
+\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. This makes per-megawatt costs prohibitive. These staffing requirements drive the economic challenge threatening SMR deployment for datacenter applications.
+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.
 
 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.
 
@@ -62,26 +62,12 @@ adoption across critical infrastructure.
 
 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: 
+\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.
 
-The nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs. 
+\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.
 
-Datacenter operators need hundreds of megawatts of continuous clean power for AI 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.
 
-Clean energy advocates need nuclear power to be economically competitive. 
+The complete research plan spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains: How long will it take? 
-
-All three groups require autonomous control with safety guarantees.
-
-\textbf{Why now?} Two forces converge to create urgency: 
-
-\textit{First: exponentially growing demand.} 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. 
-
-\textit{Second: technical maturity.} Formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. 
-
-The problem is urgent. The tools exist.
-
-\textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier and enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure. Impact extends beyond nuclear power to any safety-critical system requiring provable correctness.
-
-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

@@ -76,16 +76,22 @@ Figure \ref{fig:gantt} shows the complete project schedule including research th
 
 \subsection{Milestones and Deliverables}
 
-Six major milestones mark critical validation points throughout the research:
+Six major milestones mark critical validation points throughout the research. M1
-
+(Month 4) confirms that startup procedures have been successfully translated to
-\textbf{M1 (Month 4):} Confirms that startup procedures have been successfully translated to temporal logic using FRET with realizability analysis demonstrating consistent and complete specifications.
+temporal logic using FRET with realizability analysis demonstrating consistent
-
+and complete specifications. M2 (Month 8) validates computational tractability
-\textbf{M2 (Month 8):} Validates computational tractability by demonstrating that Strix can synthesize a complete discrete automaton from the formalized specifications. Delivers a conference paper submission to NPIC\&HMIT documenting the procedure-to-specification translation methodology.
+by demonstrating that Strix can synthesize a complete discrete automaton from
-
+the formalized specifications. This milestone delivers a conference paper
-\textbf{M3 (Month 12):} Achieves TRL 3 by proving that continuous controllers can be designed and verified to satisfy discrete transition requirements. Delivers an internal technical report demonstrating component-level verification.
+submission to NPIC\&HMIT documenting the procedure-to-specification translation
-
+methodology. M3 (Month 12) achieves TRL 3 by proving that continuous controllers
-\textbf{M4 (Month 16):} Achieves TRL 4 through integrated simulation demonstrating that component-level correctness composes to system-level correctness. Delivers a journal paper submission to IEEE Transactions on Automatic Control presenting the complete hybrid synthesis methodology.
+can be designed and verified to satisfy discrete transition requirements. This
-
+milestone delivers an internal technical report demonstrating component-level
-\textbf{M5 (Month 20):} Achieves TRL 5 by demonstrating practical implementability on industrial hardware. Delivers a conference paper submission to NPIC\&HMIT or CDC documenting hardware implementation and experimental validation.
+verification. M4 (Month 16) achieves TRL 4 through integrated simulation
-
+demonstrating that component-level correctness composes to system-level
-\textbf{M6 (Month 24):} Completes the dissertation documenting the entire methodology, experimental results, and research contributions. 
+correctness. This milestone delivers a journal paper submission to IEEE
+Transactions on Automatic Control presenting the complete hybrid synthesis
+methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical
+implementability on industrial hardware. This milestone delivers a conference
+paper submission to NPIC\&HMIT or CDC documenting hardware implementation and
+experimental validation. M6 (Month 24) completes the dissertation documenting
+the entire methodology, experimental results, and research contributions. 

EDITORIAL_SUMMARY.md

@@ -1,90 +0,0 @@
-# Editorial Pass Summary - Thesis Proposal
-**Date:** March 9, 2026
-**Editor:** Split 🦎
-
-## Overview
-Completed multi-level editorial pass on thesis proposal following Gopen's *Sense of Structure* principles and Heilmeier Catechism alignment.
-
-## Changes Made
-
-### Research Statement (research_statement_v1.tex)
-**Tactical improvements:**
-- Fixed awkward phrasing "correct by construction by" → "that are correct by construction, unifying..."
-- Improved stress position: "requirements each discrete mode imposes" → "requirements imposed by each discrete mode"
-- Strengthened voice: "The methodology demonstrates on" → "I demonstrate this methodology on"
-
-### Section 1: Goals and Outcomes (v1.tex)
-**Tactical improvements:**
-- Fixed parallel phrasing: "correct by construction by" → "that are correct by construction, unifying..."
-- Removed redundant "existing" in "existing written operating procedures"
-- Combined choppy sentences for better flow:
-  - "Classical control theory handles linear systems. Reachability analysis handles nonlinear dynamics." → "...while reachability analysis..."
-  - "Engineers design continuous controllers using standard practices. Formal correctness guarantees remain intact." → "...while maintaining formal correctness guarantees."
-  - Similar fix for "Formal methods verify discrete logic. Control theory verifies continuous dynamics."
-- Added transition word for better paragraph flow: "Small modular reactors offer..." → "Small modular reactors, in particular, offer..."
-
-### Section 2: State of the Art (v2.tex)
-**Tactical improvements:**
-- Removed redundant sentence in LIMITATION box (repeated "expert judgment and simulator validation")
-- Fixed typo: "ivariant" → "invariant"
-- Improved ending: "far from a complete methodology to design systems with" → "fall far short of a complete design methodology"
-
-### Section 3: Research Approach (v3.tex)
-**Tactical improvements:**
-- Fixed conjunction: "by composing formal methods from computer science with control-theoretic verification and formalizing" → "...verification, formalizing..." (cleaner parallel structure)
-
-### Section 4: Metrics for Success (v1.tex)
-**Tactical improvements:**
-- Strengthened opening: "Technology Readiness Level advancement...measures success" → "Success is measured by Technology Readiness Level advancement..."
-- Condensed repetitive opening: Combined three short sentences about TRLs into one tighter statement
-
-### Section 5: Risks and Contingencies (v1.tex)
-**Tactical improvements:**
-- Combined choppy sentences: "Temporal logic operates on boolean predicates. Continuous control requires reasoning..." → "...predicates, while continuous control requires..."
-
-### Section 6: Broader Impacts (v1.tex)
-**No changes needed** - This section was already strong with excellent argument flow and stress positions.
-
-### Section 8: Schedule (v1.tex)
-**Operational improvement:**
-- Reformatted dense milestone paragraph into structured list with bold headings (M1-M6) for much better readability
-- Each milestone now has clear deliverable and achievement statement
-
-## High-Level Observations
-
-### Strengths
-1. **Strategic alignment is excellent**: Every section clearly states its Heilmeier questions at the beginning and summarizes answers at the end
-2. **Argument flow is strong**: Sections build logically from problem → approach → metrics → risks → impact → timeline
-3. **Technical depth is appropriate**: Balance between rigor and readability is well-maintained
-4. **Stress positions are generally good**: Important information lands at sentence/paragraph ends effectively
-
-### Areas of Excellence (No Changes Needed)
-- Section 6 (Broader Impacts): Excellent argument structure and economic framing
-- Section summaries: Crisp, direct answers to Heilmeier questions
-- Technical subsection organization: Clear progression through methodology
-- Use of examples: TMI accident, HARDENS project, concrete statistics strengthen arguments
-
-### Minor Opportunities for Future Consideration
-1. **Paragraph length**: Some sections (especially 2, 5, 6) contain very long paragraphs (6-7 sentences). Consider breaking these up for better visual flow, though content is strong.
-2. **Citation placement**: Generally good, a few places could add citations for recent SMR economics claims
-3. **Technical notes**: Several `%%% NOTES` sections at end of Section 3 indicate potential areas for expansion
-
-## Summary Statistics
-- Files edited: 7
-- Insertions: 30 lines
-- Deletions: 37 lines
-- Net change: Tighter, clearer writing with improved flow
-- Commit hash: db0d891
-
-## Overall Assessment
-**This is a strong proposal.** The Heilmeier structure provides excellent scaffolding. The technical argument is sound and well-presented. The edits focus on polish—improving clarity, flow, and readability without changing substance.
-
-The proposal successfully:
-- Establishes clear research gap (discrete OR continuous, never both compositionally)
-- Presents novel approach (contract-based decomposition, mode classification, procedure-driven)
-- Justifies feasibility (existing structure, bounded complexity, industrial validation)
-- Defines success metrics (TRL advancement 2-3 → 5)
-- Addresses risks with viable contingencies
-- Connects to urgent economic need ($21-28B annual O&M costs)
-
-**Bottom line:** Ready for committee review. The editorial pass improved clarity and flow without needing major structural changes.