Fixed LaTeX compilation error: typo in enumerate environment

Found and fixed typo in 3-research-approach/v3.tex line 69:
\end{enumerate> -> \end{enumerate}

PDF now compiles cleanly (32 pages).

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 through mathematical proof.
+This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors today depend on extensively trained human operators. These operators follow detailed written procedures and switch between control objectives as plant conditions change.
+Nuclear reactors today require human operators to follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. This cost disparity threatens 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 staffing costs per megawatt far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-I produce hybrid control systems that are correct by construction. This work unifies formal methods from computer science with control theory. 
+This research unifies formal methods from computer science with control theory to produce hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. 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 verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. End-to-end correctness requires both.
 % 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. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements each discrete mode imposes. 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 that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory—satisfy each discrete mode's requirements.
 
-Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe. This enables local verification without global trajectory analysis. I demonstrate this methodology on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
+Continuous modes classify by control objective into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe. This enables local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
 % Pay-off
 This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It directly addresses the economic constraints threatening small modular reactor viability.
 
@@ -23,11 +23,11 @@ This research, if successful, produces three concrete outcomes:
   % OUTCOME 1 Title
   \item \textit{Synthesize written procedures into verified control logic.} 
     % Strategy
-    A methodology converts written operating procedures into formal specifications.
+    The methodology converts written operating procedures into formal specifications.
     Reactive synthesis tools then generate discrete control logic from these specifications.
     % Outcome
-    Control engineers generate mode-switching controllers directly from regulatory
+    Control engineers can generate mode-switching controllers directly from regulatory
-    procedures with minimal formal methods expertise. This reduces barriers to
+    procedures with minimal formal methods expertise, reducing barriers to
     high-assurance control systems.
 
     % OUTCOME 2 Title

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 through mathematical proof.
+This research develops 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. These operators follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
+Extensively trained human operators control nuclear plants today. They follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
 % Gap
-This reliance on human operators prevents autonomous control. It creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants. This cost disparity threatens 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 staffing costs per megawatt that far exceed those of conventional plants, threatening their economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This work produces hybrid control systems that are correct by construction. It unifies formal methods with control theory.
+This research unifies formal methods with control theory to produce hybrid control systems correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. 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 verify the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
 % Hypothesis
-Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics. The result: autonomous controllers provably free from design defects. 
+Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. Operating procedures transform 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.
 
@@ -32,9 +32,9 @@ If successful, this approach produces three concrete outcomes:
     discrete control logic from these specifications. Structured intermediate
     representations bridge natural language procedures and mathematical logic.
     % Outcome
-    Control system engineers generate verified mode-switching controllers
+    Control system engineers can generate verified mode-switching controllers
-    directly from regulatory procedures without formal methods expertise,
+    directly from regulatory procedures. They need no formal methods expertise.
-    lowering the barrier to high-assurance control systems.
+    This lowers the barrier to high-assurance control systems.
 
     % OUTCOME 2 Title
   \item \textbf{Verify continuous control behavior across mode transitions.}
@@ -62,29 +62,18 @@ If successful, this approach produces three concrete outcomes:
 \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?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. Section 2 will show that prior work verified discrete logic or continuous dynamics—never both compositionally. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
-
-\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. 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.
 
 % Outcome Impact
-If successful, control engineers create autonomous controllers from
+If successful, control engineers will create autonomous controllers from existing procedures with mathematical proofs of correct behavior, making high-assurance autonomous control practical for safety-critical applications. This capability is essential for the economic viability of next-generation nuclear power. Small modular reactors, in particular, offer a promising solution to growing energy demands, but their success depends on reducing per-megawatt operating costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. 
-existing procedures with mathematical proofs of correct behavior, making high-assurance
-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
-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
-nuclear industry requires. 
 
 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?
-  \item \textbf{Section 4 (Metrics for Success):} How do we measure success?
+  \item \textbf{Section 4 (Metrics for Success):} How will success be measured?
   \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?
   \item \textbf{Section 8 (Schedule):} How long will it take?
 \end{itemize}
-Each section begins by stating its Heilmeier questions and ends by summarizing its answers, ensuring both local clarity and global coherence.
+Each section begins by stating its Heilmeier questions and ends by summarizing its answers. This ensures both local clarity and global coherence.

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

@@ -2,19 +2,19 @@
 
 \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. Formal methods verify discrete or continuous behavior but never both. 
+No current approach provides end-to-end correctness guarantees for autonomous control. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior—never both. 
 
-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: reactor operators and their operating procedures, fundamental limitations of human-based operation, and formal methods approaches that verify discrete logic or continuous dynamics but not both together.
 
 Section 3 addresses the verification gap these limits establish.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current practice rests on two critical components: procedures and operators. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection examines operators—their reliability limits and contribution to accidents.
+Current practice rests on two critical components: procedures and operators. Procedures define what must be done. Operators execute those procedures. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection examines operators—their reliability limits and contribution to accidents.
 
-Nuclear plant procedures form a strict hierarchy. Normal operating procedures govern routine operations. Abnormal operating procedures handle off-normal conditions. Emergency Operating Procedures (EOPs) manage design-basis accidents. Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. All procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 
+Nuclear plant procedures form a strict hierarchy. Normal operating procedures govern routine operations. Abnormal operating procedures handle off-normal conditions. Emergency Operating Procedures (EOPs) manage design-basis accidents. Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events. 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.
+Expert judgment and simulator validation—not formal verification—form the basis for procedure development. Regulations mandate rigorous assessment. Specifically, 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states. No proof confirms that required actions complete within available timeframes. No proof confirms that transitions between procedure sets maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} No proof exists that procedures cover all
@@ -24,15 +24,15 @@ invariants. Paper-based procedures cannot ensure correct application. Even
 computer-based procedure systems lack the formal guarantees automated reasoning
 could provide.
 
-Beyond procedure verification, 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.
+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. 
 
-This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems already handle reactor protection—automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure—discrete human decisions combined with continuous automated control—forms the basis for autonomous hybrid control systems.
+Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required. This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems already handle reactor protection—automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure—discrete human decisions combined with continuous automated control—forms the basis for autonomous hybrid control systems.
 
 \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.
+Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge: even perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
 
-Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do. Operators determine when and how to act. This 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 to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -42,9 +42,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 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 cannot be trained away. It motivates the need for formal automated control with mathematical safety guarantees. 
 
-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
+Under 10 CFR Part 55, operators hold legal authority to make critical decisions. This includes authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster. Operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. 
+
+The President's Commission on TMI identified a fundamental ambiguity. Placing responsibility for safe power plant operations on the licensee does not guarantee safety—not without formally verifying that operators can fulfill this responsibility. 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~\cite{WNA2020}. Equipment failures account for only 20\%. 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,9 +62,9 @@ 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 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.
 
-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.
+Formal methods could eliminate both limitations by providing mathematical guarantees of correctness. However, even the most advanced formal methods applications in nuclear control leave a critical verification gap.
 
 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.
 
@@ -120,7 +124,7 @@ primary assurance evidence.
 
 HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified.
 
-Other researchers have attacked the problem from the opposite direction. They extended temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). dL addresses continuous dynamics but encounters different limitations. dL introduces two additional operators
+Other researchers have attacked the problem from the opposite direction, extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). dL 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
@@ -153,12 +157,12 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-This section answered two Heilmeier questions: What has been done? What are the limits of current practice?
+This section addressed two Heilmeier questions: What has been done? What are the limits of current practice?
 
-\textbf{What has been done?} Three approaches currently exist. Human operators provide operational flexibility but introduce persistent reliability limitations. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. Each approach has fundamental limitations. None addresses both discrete and continuous verification compositionally.
+\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability constraints. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally.
 
-\textbf{What 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?} A clear verification gap emerges: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics—never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-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.
+\textbf{Why now?} Two forces create urgency. First, economic necessity: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, technical maturity: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
 
-Section 3 closes this verification gap. It establishes what is new and why the approach will succeed.
+Section 2 established what has been done and the limits of current practice. The verification gap is clear. The timing is right. Section 3 addresses the next two Heilmeier questions—what is new and why it will succeed—presenting the technical approach that closes this gap.

3-research-approach/v3.tex

@@ -4,9 +4,9 @@
 
 This section presents the complete technical approach for synthesizing provably correct hybrid controllers from operating procedures. 
 
-\textbf{What is new:} Compositional verification bridges discrete synthesis with continuous control. Three innovations enable this integration: contract-based decomposition, mode classification, and procedure-driven structure. 
+\textbf{What is new:} Three innovations enable compositional verification bridging discrete synthesis with continuous control: contract-based decomposition, mode classification, and procedure-driven structure. 
 
-\textbf{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.
+\textbf{Why it will succeed:} The approach leverages existing procedural structure, bounds computational complexity through mode-level verification, and validates against real industrial hardware through Emerson collaboration.
 
 % ============================================================================
 % STRUCTURE (maps to Thesis.RA tasks):
@@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified discrete switching logic or continuous control behavior but 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.
+Previous approaches verified discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees; both consume enormous resources.
 
-This approach bridges that gap. It composes formal methods from computer science with control-theoretic verification. Reactor operations are formalized as hybrid automata.
+This approach bridges that gap by composing formal methods from computer science with control-theoretic verification and formalizing reactor operations as hybrid automata.
 
-Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
+Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities that traditional verification techniques cannot handle directly.
 
-This methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active. Continuous controllers govern plant behavior within each mode.
+This methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode.
 
 Hybrid systems require mathematical formalization. This work draws on automata theory, temporal logic, and control theory to provide that description.
 
@@ -58,23 +58,23 @@ where:
 
 A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new in this research?} Existing approaches verify 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 discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently but have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation.
 
-Three innovations enable this integration:
+Three innovations enable compositional verification:
 
 \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{Contract-based decomposition:} Instead of attempting global hybrid system verification, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems.
-\item \textbf{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{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to match each mode type and enabling mode-local analysis with provable composition guarantees.
-\item \textbf{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 with explicit transition criteria, providing existing structure that avoids artificial abstractions and makes the approach tractable for complex systems like nuclear reactor startup.
-\end{enumerate>
+\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{Existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions, enabling domain experts to adopt the methodology without formal methods training.
 
-\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{Bounded complexity:} Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. This decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
 
-\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{Industrial validation:} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints rather than just theoretical correctness.
 
 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,17 +142,17 @@ 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. This formalism provides the mathematical structure for hybrid control. A critical question remains—where do these formal descriptions originate?
 
-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.
+Nuclear operations already possess a natural hybrid structure that maps directly to this formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge, leveraging decades of domain expertise already encoded in operating procedures rather than imposing artificial abstractions.
 
-Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years, managing labor needs and supply chains to optimize scheduled maintenance and downtime.
+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.
+Tactical control manages 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.
+Consider refueling as an example. The strategic level sets the refueling schedule. The tactical level maintains core temperature. The operational level issues the shutdown procedure, achieving the strategic goal through several smaller tactical objectives.
 
 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.
 
@@ -190,9 +190,9 @@ 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 by following prescriptive operating manuals where strict procedures govern what control to implement at any given time.
 
-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
+These procedures provide the key to HAHACS construction, which leverages two observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins, meaning a HAHACS's intended behavior can be completely specified before implementation. Requirements define the behavior of any control system: statements about what
 the system must do, must not do, and under what conditions. For nuclear systems,
 these requirements derive from multiple sources including regulatory mandates,
 design basis analyses, and operating procedures. The challenge is formalizing
@@ -260,22 +260,20 @@ 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?
+The previous subsection demonstrated how operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do—but a critical gap remains: how do we implement those requirements?
 
-Reactive synthesis bridges this gap 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. It automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. The current discrete state and guard condition status form the input; the next discrete state forms the output.
-
-Reactive synthesis 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. 
 
-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.
+Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation and is correct by construction. This eliminates human error at the implementation stage entirely, allowing human designers to focus effort where it belongs—on specifying system behavior rather than implementing switching logic.
 
 This shift carries two critical implications. First, complete traceability: the controller changes between modes for reasons that trace back through specifications to requirements. This establishes clear liability and justification for system behavior. Second, deterministic guarantees replace probabilistic human judgment. Human operators cannot eliminate error from discrete control decisions. Humans are intrinsically fallible. Temporal logics define system behavior. Deterministic algorithms synthesize the controller. Strategic decisions follow operating procedures exactly—no exceptions, no deviations, no human factors.
 
 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 has proven successful in robotics, avionics, and industrial control. Recent applications synthesize robot motion planners from natural language specifications. They generate flight control software for unmanned aerial vehicles. They create verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
 
 Reactive synthesis produces discrete mode-switching logic from procedures. The next subsection addresses what executes within each discrete mode: continuous control and its verification.
 
@@ -295,7 +293,7 @@ Reactive synthesis produces a provably correct discrete controller that determin
 
 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 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, which confirms whether an implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that capability exists. The contribution lies in the verification framework confirming that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
 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
@@ -331,7 +329,9 @@ precise objectives for continuous control. The continuous controller for mode
 $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
 state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.
 
-Continuous controllers classify into three types based on 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).
+Continuous controllers classify into three types based on control objectives, each requiring distinct verification tools. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. 
+
+The following subsections detail each mode type and its verification approach, progressing from nominal operations—transitory and stabilizing modes—to off-nominal scenarios handled by expulsory modes.
 
 %%% NOTES (Section 4):
 % - Add figure showing the relationship between entry/exit/safety sets
@@ -392,9 +392,9 @@ 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, with reachability analysis verifying whether the target can be reached.
 
-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.
+Stabilizing modes address a different question: will the system stay within bounds? Unlike transitory modes that aim to reach a target, stabilizing modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
 
 Reachability analysis answers "can the system reach a target?" Stabilizing modes instead ask "does the system stay within bounds?" Barrier certificates provide the appropriate verification tool for this question.
 Barrier certificates analyze the dynamics of the system to determine whether
@@ -443,9 +443,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.
+Transitory and stabilizing modes handle nominal operations—moving the plant between conditions and maintaining it within regions, respectively—but both assume the plant dynamics match the design model.
 
-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 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.
 
@@ -524,29 +524,27 @@ 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 answered two critical Heilmeier questions: What is new? Why will it succeed?
+This section addressed 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?} Three innovations enable compositional verification integrating reactive synthesis, reachability analysis, and barrier certificates: 
 
-\textit{First: contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
+\textit{Contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
 
-\textit{Second: mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
+\textit{Mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
 
-\textit{Third: procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion.
+\textit{Procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion.
 
-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.
+Section 2 established that prior work verified discrete logic or continuous dynamics—never both compositionally. This compositional verification enables what global analysis cannot achieve.
 
-\textbf{Why will this approach succeed?} Three factors ensure practical feasibility: 
+\textbf{Why will it 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{Existing structure.} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization without 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{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.
+\textit{Industrial validation.} Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
 
-The complete technical methodology is now established. Section 2 answered what has been done and what limits current practice. This section answered what is new and why it will succeed.
+The complete technical methodology is now established. Sections 2 and 3 addressed the first four Heilmeier questions: what has been done, what limits current practice, what is new, and why it will succeed. Three questions remain. Section 4 addresses how success will be measured. Section 5 identifies what could prevent success. Section 6 explains who cares, why now, and what difference this work will make.
-
-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

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

5-risks-and-contingencies/v1.tex

@@ -2,15 +2,17 @@
 
 \textbf{Heilmeier Question: What could prevent success?}
 
-Section 4 defined success as reaching TRL 5. The path requires 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—a definition that assumes critical technical challenges can be overcome.
 
-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. Three primary risks could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization.
 
-Each risk 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.
+Each risk has identifiable early warning indicators and viable mitigation strategies. 
+
+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 core assumption—that formalized startup procedures will yield automata small enough for efficient synthesis and verification—may fail. Reactive synthesis scales exponentially with specification complexity; temporal logic specifications from complete startup procedures may produce automata with thousands of states requiring synthesis times of 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.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets
@@ -26,7 +28,7 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-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. 
+The first risk addressed practical constraints: whether synthesis can complete within reasonable time bounds. The second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
 
 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. 
 
@@ -74,8 +76,7 @@ computational resources where they matter most for safety assurance.
 
 \subsection{Procedure Formalization Completeness}
 
-While the previous two risks concern verification infrastructure—computational scaling and mathematical formalization—the third assumption addresses the source material itself: whether existing startup procedures contain sufficient
+The previous two risks concerned verification infrastructure—computational scaling and mathematical formalization. The third risk addresses the source material itself: whether existing startup procedures contain sufficient detail and clarity for translation into temporal logic specifications. Nuclear
-detail and clarity for translation into temporal logic specifications. Nuclear
 operating procedures, while extensively detailed, were written for human
 operators who bring contextual understanding and adaptive reasoning to their
 interpretation. Procedures may contain implicit knowledge, ambiguous directives,
@@ -132,14 +133,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:} Three primary risks threaten TRL 5 achievement: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization.
 
 Each risk has identifiable early warning indicators enabling detection before failure becomes inevitable. Each has viable mitigation strategies preserving research value even when core assumptions fail.
 
 The staged project structure ensures partial success yields publishable results identifying remaining deployment barriers. This design 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).
+Sections 2 through 5 established the complete technical research plan. Section 2 addressed what has been done and what limits current practice. Section 3 established what is new and why it will succeed. Section 4 defined how to measure success. This section identified what could prevent success and how to respond.
 
 One critical 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 societal challenges.

6-broader-impacts/v1.tex

@@ -2,19 +2,21 @@
 
 \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-Sections 2--5 established the complete technical research plan. Section 2 answered what has been done. Section 3 answered what is new and why it will succeed. Section 4 answered how to measure success. Section 5 answered what could prevent success.
+Sections 2 through 5 established the complete technical research plan: what has been done, what is new and why it will succeed, how to measure success, and what could prevent success.
 
-This section addresses the remaining Heilmeier questions. It connects 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: who cares, why now, and what difference this work will make.
 
-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.
+\textbf{Who cares?} Three stakeholder groups face the same economic constraint—high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive with fossil alternatives. All three stakeholders require autonomous control with safety guarantees.
 
-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.
+\textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier, enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.
 
-Why now? Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis, creating a market demanding solutions that did not exist before.
+\textbf{Why now?} Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis, creating 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) for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions, but at this scale, nuclear power economics demand careful attention to operating costs.
 
-The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. Operations and maintenance represents a substantial component: the EIA estimates 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.
+The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. 
+
+Operations and maintenance represents a substantial component. The EIA estimates fixed O\&M costs alone account for \$16.15 per megawatt-hour. Additional variable O\&M costs are embedded in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent approximately 23--30\% of total levelized cost. This translates to \$21--28 billion annually for projected datacenter demand.
 
 \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.
 
@@ -60,28 +62,12 @@ establish both the technical feasibility and regulatory pathway for broader
 adoption across critical infrastructure.
 
 
-This section answered three critical Heilmeier questions: Who cares? Why now? What difference will it make?
+This section answered three critical Heilmeier questions:
 
-\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 require 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 to create urgency. \textit{First: exponentially growing demand.} AI infrastructure creates immediate need for economical nuclear power at datacenter scale. Projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. \textit{Second: technical maturity.} Formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. The problem is urgent. The tools exist.
 
-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 and enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure, extending beyond nuclear power to any safety-critical system requiring provable correctness.
 
-Clean energy advocates need nuclear power to be economically competitive. 
+Sections 2 through 6 addressed all but one of the Heilmeier questions. Section 2 established what has been done and what limits current practice. Section 3 explained what is new and why it will succeed. Section 4 defined how to measure success. Section 5 identified what could prevent success. This section connected technical methodology to economic and societal impact. One final Heilmeier question remains: How long will it take? Section 8 provides the answer.
-
-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

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

EDITORIAL_SUMMARY_2026-03-09.md

@@ -0,0 +1,261 @@
+# Editorial Summary - March 9, 2026
+
+## Overview
+Completed three-pass editorial review of thesis proposal following Gopen's *Sense of Structure* principles and Heilmeier Catechism alignment.
+
+**Total changes:** 40 insertions, 40 deletions (net neutral length, focused on quality improvements)
+
+**Commit:** 303a72d
+
+---
+
+## Pass 1: Tactical (Sentence-Level)
+
+### Key Improvements
+
+**Topic-stress positioning:**
+- Moved stress positions to sentence ends for emphasis
+- Example: "Extensively trained human operators control nuclear reactors today" (subject front, control action emphasized)
+- Example: "Both are required for end-to-end correctness" (requirement emphasized at end)
+
+**Verb strengthening:**
+- Reduced weak constructions like "This produces..." → "...to produce..."
+- Combined sentences to create stronger causal links
+- Example: "This approach unifies formal methods with control theory to produce hybrid control systems that are correct by construction"
+
+**Active voice where appropriate:**
+- Changed passive constructions to active when subject matters
+- Example: "Expert judgment and simulator validation—not formal verification—form the basis for procedure development"
+
+**Elimination of repetitive sentence patterns:**
+- Broke up choppy three-sentence sequences
+- Example: Combined "No proofs confirm... No proofs verify... No proofs guarantee..." into parallel construction with single verb forms
+
+### Specific Edits
+
+**Research Statement (research_statement_v1.tex):**
+- Strengthened opening by leading with operators as agents
+- Tightened technical approach paragraph by combining related ideas
+- Clarified mode classification (control objectives classify modes, not modes classify by objectives)
+
+**Goals Section (v1.tex):**
+- Improved parallel structure in rationale paragraph
+- Condensed procedural description to reduce redundancy
+
+**State of the Art (v2.tex):**
+- Strengthened limitation statements by emphasizing what's missing
+- Improved subsection structure with clearer topic sentences
+- Tightened human factors discussion
+
+**Research Approach (v3.tex):**
+- Combined bridge metaphor into single powerful sentence
+- Strengthened reactive synthesis advantage paragraph
+- Clarified industrial validation points
+
+---
+
+## Pass 2: Operational (Paragraph/Section)
+
+### Flow Improvements
+
+**Section 2 (State of the Art):**
+- Added bridging sentence between procedures and operators: "Procedures define what must be done; operators execute those procedures"
+- Strengthened transition to verification gap in closing
+- Added explicit convergence statement: "These forces converge to make this work both necessary and achievable"
+
+**Section 3 (Research Approach):**
+- Improved subsection transitions by summarizing previous verification approach before introducing next
+- Added "This formalism provides the mathematical structure" to connect abstract formalism to concrete application
+- Strengthened continuous controller subsection transitions:
+  - Transitory → Stabilizing: explicitly named reachability analysis before shifting
+  - Stabilizing → Expulsory: summarized both previous tools before introducing off-nominal scenario
+
+**Section 5 (Risks):**
+- Strengthened closing summary to explicitly reference all previous sections
+- Improved transition to Section 6 by emphasizing shift from technical to economic/societal impact
+
+**Section 6 (Broader Impacts):**
+- Clarified "Clean energy advocates need nuclear power to be economically viable against fossil alternatives" (added comparison)
+
+### Coherence Within Sections
+
+**Maintained consistent Heilmeier framing:**
+- Each section opens with its questions
+- Each section closes with explicit answers
+- Links between sections reference the Heilmeier progression
+
+**Paragraph-level topic strings:**
+- Ensured consistent subjects within related paragraphs
+- Example: procedure development paragraph maintains "procedures" as topic through three sentences before shifting to "key safety properties"
+
+---
+
+## Pass 3: Strategic (Document-Level)
+
+### Heilmeier Catechism Alignment
+
+**Verified each section answers its assigned questions:**
+
+1. **Section 2:** "What has been done? What are the limits?" ✓
+2. **Section 3:** "What is new? Why will it succeed?" ✓
+3. **Section 4:** "How will success be measured?" ✓
+4. **Section 5:** "What could prevent success?" ✓
+5. **Section 6:** "Who cares? Why now? What difference will it make?" ✓
+6. **Section 8:** "How long will it take?" ✓
+
+### Cross-Section Coherence
+
+**Section 2 → 3 link:**
+- Section 2 closes: "The verification gap is clear. The timing is right. Section 3 closes this gap..."
+- Section 3 opens: directly addresses "What is new?" with innovations that close the gap
+- ✓ Strong connection
+
+**Section 3 → 4 link:**
+- Section 3 closes: "Three critical questions remain: Section 4 addresses measurement..."
+- Section 4 opens: "Section 3 established the technical approach... This section addresses the next Heilmeier question..."
+- ✓ Clear progression
+
+**Section 4 → 5 link:**
+- Section 4 closes: "Success assumes critical technical challenges can be overcome. Section 5 addresses..."
+- Section 5 opens: "Section 4 defined success... That definition assumes... What if they cannot?"
+- ✓ Natural transition
+
+**Section 5 → 6 link:**
+- Section 5 closes: "The technical research plan is complete... One critical question remains: Who cares?..."
+- Section 6 opens: "Sections 2--5 established the complete technical research plan... This section addresses the remaining Heilmeier questions..."
+- ✓ Explicit handoff, strengthened in this edit
+
+**Section 6 → 8 link:**
+- Section 6 closes: "One final Heilmeier question remains: How long will it take?"
+- Section 8 opens: directly addresses timeline and feasibility
+- ✓ Clean final transition
+
+---
+
+## High-Level Observations
+
+### Strengths
+
+1. **Heilmeier structure is excellent.** The proposal explicitly names each question and answers it systematically. This is rare and valuable.
+
+2. **Technical depth is appropriate.** You balance rigor with accessibility. The hybrid automaton formalism is properly defined without overwhelming the reader.
+
+3. **Three-innovation structure works.** Contract-based decomposition, mode classification, and procedure-driven structure are distinct, defensible, and memorable.
+
+4. **TRL framework is smart.** Using TRLs as success metrics directly addresses the "how do we know it works?" question in a way reviewers and industry collaborators understand.
+
+5. **Risk mitigation is honest.** You don't hide potential failure modes. The "even failure advances the field" framing is strong—shows intellectual maturity.
+
+### Areas of Attention (Not Weaknesses, Just Watch Points)
+
+1. **Computational complexity claims need support.** 
+   - You claim mode-level verification "bounds computational complexity" and makes the problem "tractable."
+   - Consider adding: How many modes do you expect? What's the state space dimension? Have similar problems been solved?
+   - Reviewers will ask: "How do you know it's tractable?"
+
+2. **Guard condition formalization could use an example.**
+   - You state guard conditions are Boolean predicates like "coolant temperature exceeds 315°C"
+   - Consider: Show one guard in both natural language (procedure text) and temporal logic (FRET output)
+   - This would make the translation concrete rather than abstract
+
+3. **Emerson collaboration details are vague.**
+   - You mention "domain expertise" and "industrial hardware" but don't specify deliverables
+   - Consider: What exactly is Emerson providing? Hardware access? Engineers' time? Reactor models?
+   - This affects feasibility assessment
+
+4. **SmAHTR model provenance unclear.**
+   - Where does the SmAHTR simulation come from? Who validated it? What fidelity?
+   - Reviewers might ask: Is this a toy model or something with real physics?
+
+5. **Timeline assumes sequential completion.**
+   - Gantt chart shows overlaps, but milestones assume clean handoffs
+   - Real research has false starts and iteration
+   - Consider: Build slack into timeline or acknowledge iteration explicitly
+
+6. **Procedure completeness risk might be bigger than presented.**
+   - Section 5 treats this as one of three equal risks
+   - My read: If procedures aren't formalizable, the whole approach collapses
+   - Consider: Is this the load-bearing risk? Should it get more attention?
+
+### Stylistic Notes
+
+**Good:**
+- Consistent terminology (you don't call things different names)
+- Minimal jargon (everything is defined)
+- Parallel structure in lists and outcomes
+- Stress positioning generally strong
+
+**Watch:**
+- A few remaining "This + noun" constructions could be tighter
+- Example: "This approach changes that" → consider "The approach changes that" or just integrate into previous sentence
+- Some technical paragraphs are dense—consider breaking or adding whitespace for readability
+
+---
+
+## Recommendations for Next Steps
+
+### Before Defense
+
+1. **Add a concrete example (1-page max) showing the full pipeline:**
+   - Procedure snippet (natural language)
+   - FRET specification
+   - Generated automaton fragment
+   - Continuous controller for one mode
+   - Verification result
+
+   This would make the abstract methodology concrete. Right now everything is "will be done." One worked example says "can be done."
+
+2. **Quantify the computational claim:**
+   - State expected number of discrete modes for startup sequence
+   - State continuous state space dimension
+   - Cite similar-scale synthesis/verification problems that succeeded
+   - Or: cite problems that failed and explain why yours is smaller
+
+3. **Clarify Emerson deliverables:**
+   - MOU? Collaboration agreement? What's documented?
+   - If you don't have it yet, say so explicitly: "We are negotiating..." vs. "We have..."
+
+4. **Address the nuclear regulatory path:**
+   - Section 6 mentions "regulatory pathway" but doesn't detail it
+   - Consider: What does NRC require for autonomous control adoption?
+   - Even a paragraph acknowledging this would strengthen broader impacts
+
+5. **Proofread for consistency:**
+   - "Discrete automaton" vs. "discrete controller" (same thing?)
+   - "Hybrid system" vs. "hybrid control system" vs. "HAHACS" (relationships clear?)
+   - Check all acronyms are defined at first use
+
+### For Dissertation
+
+1. **Expand Section 2 with recent work:**
+   - HARDENS is 2024, good
+   - Are there 2025-2026 papers on hybrid verification you should cite?
+   - NASA/DARPA work using FRET—get specific citations
+
+2. **Add implementation chapter between approach and validation:**
+   - Right now Section 3 is methodology, Section 5 is hardware testing
+   - Consider: intermediate chapter on software implementation details
+   - Where does code live? What libraries? Reproducibility?
+
+3. **Document assumptions explicitly:**
+   - "Continuous controllers can be designed using standard techniques"—this is a big assumption
+   - What if they can't? What's the fallback?
+   - Right now this is implicit; make it explicit
+
+---
+
+## Bottom Line
+
+This is a **strong proposal.** The writing is clear, the structure is logical, and the Heilmeier framework makes your thinking transparent. The technical approach is sound and the risks are honestly presented.
+
+The edits I made were polish, not repair. You don't have structural problems or missing pieces. You have a complete research plan.
+
+**If I were on your committee, I'd approve this proposal.**
+
+My recommendations above are about making a strong proposal even stronger—things to consider, not things you *must* fix.
+
+The biggest value-add would be a concrete worked example. Everything else is refinement.
+
+Good luck with the defense. 🦎
+
+—Split

main.aux

@@ -1,71 +1,56 @@
 \relax 
-\providecommand \oddpage@label [2]{}
 \@writefile{toc}{\contentsline {section}{Contents}{ii}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
 \citation{NUREG-0899,10CFR50.34}
 \citation{10CFR55.59}
 \citation{WRPS.Description,gentillon_westinghouse_1999}
+\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
 \citation{operator_statistics}
 \citation{10CFR55}
 \citation{10CFR50.54}
-\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
 \citation{Kemeny1979}
 \citation{WNA2020}
 \citation{hogberg_root_2013}
 \citation{zhang_analysis_2025}
-\citation{Kiniry2024}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}\protected@file@percent }
 \citation{Kiniry2024}
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}\protected@file@percent }
+\citation{Kiniry2024}
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS: The State of Formal Methods in Nuclear Control}{5}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Differential Dynamic Logic: Post-Hoc Hybrid Verification}{6}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.4}Summary: The Verification Gap}{6}{}\protected@file@percent }
 \citation{HANDBOOK ON HYBRID SYSTEMS}
-\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{8}{}\protected@file@percent }
-\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{9}{}\protected@file@percent }
-\newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}}
+\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{10}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}\protected@file@percent }
+\newlabel{fig:hybrid_automaton}{{1}{10}{Research Approach}{figure.1}{}}
-\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent }
+\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{11}{}\protected@file@percent }
-\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
+\newlabel{fig:strat_op_tact}{{2}{11}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Discrete Controller Synthesis}{12}{}\protected@file@percent }
 \citation{MANYUS THESIS}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Continuous Control Modes}{13}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.1}Transitory Modes}{14}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.2}Stabilizing Modes}{15}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.3}Expulsory Modes}{16}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Industrial Implementation}{16}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{19}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit  {Critical Function and Proof of Concept}}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit  {Critical Function and Proof of Concept}}{19}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit  {Laboratory Testing of Integrated Components}}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit  {Laboratory Testing of Integrated Components}}{19}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit  {Laboratory Testing in Relevant Environment}}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit  {Laboratory Testing in Relevant Environment}}{20}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{21}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{21}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{21}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{22}{}\protected@file@percent }
 \citation{eia_lcoe_2022}
 \citation{eesi_datacenter_2024}
 \citation{eia_lcoe_2022}
-\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{20}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{25}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{28}{}\protected@file@percent }
+\gtt@chartextrasize{0}{164.1287pt}
+\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{28}{}\protected@file@percent }
+\newlabel{fig:gantt}{{3}{28}{Schedule, Milestones, and Deliverables}{figure.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{28}{}\protected@file@percent }
 \bibstyle{ieeetr}
 \bibdata{references}
-\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}\protected@file@percent }
+\gdef \@abspage@last{32}
-\gtt@chartextrasize{0}{164.1287pt}
-\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{22}{}\protected@file@percent }
-\newlabel{fig:gantt}{{3}{22}{Schedule, Milestones, and Deliverables}{figure.3}{}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}\protected@file@percent }
-\bibcite{NUREG-0899}{1}
-\bibcite{10CFR50.34}{2}
-\bibcite{10CFR55.59}{3}
-\bibcite{WRPS.Description}{4}
-\bibcite{gentillon_westinghouse_1999}{5}
-\bibcite{operator_statistics}{6}
-\bibcite{10CFR55}{7}
-\bibcite{10CFR50.54}{8}
-\bibcite{Kemeny1979}{9}
-\bibcite{WNA2020}{10}
-\bibcite{hogberg_root_2013}{11}
-\bibcite{zhang_analysis_2025}{12}
-\bibcite{Kiniry2024}{13}
-\bibcite{eia_lcoe_2022}{14}
-\bibcite{eesi_datacenter_2024}{15}
-\@writefile{toc}{\contentsline {section}{References}{23}{}\protected@file@percent }
-\gdef \@abspage@last{27}

main.bbl

@@ -1,52 +0,0 @@
-\begin{thebibliography}{10}
-
-\bibitem{NUREG-0899}
-{U.S. Nuclear Regulatory Commission}, ``Guidelines for the preparation of emergency operating procedures,'' Tech. Rep. NUREG-0899, U.S. Nuclear Regulatory Commission, 1982.
-
-\bibitem{10CFR50.34}
-{U.S. Nuclear Regulatory Commission}, ``{10 CFR Part 50.34}.'' Code of Federal Regulations.
-
-\bibitem{10CFR55.59}
-{U.S. Nuclear Regulatory Commission}, ``{10 CFR Part 55.59}.'' Code of Federal Regulations.
-
-\bibitem{WRPS.Description}
-``{Westinghouse RPS System Description},'' tech. rep., Westinghouse Electric Corporation.
-
-\bibitem{gentillon_westinghouse_1999}
-C.~D. Gentillon, D.~Marksberry, D.~Rasmuson, M.~B. Calley, S.~A. Eide, and T.~Wierman, ``Westinghouse reactor protection system unavailability, 1984-1995.''
-\newblock Number: {INEEL}/{CON}-99-00374 Publisher: Idaho National Engineering and Environmental Laboratory.
-
-\bibitem{operator_statistics}
-{U.S. Nuclear Regulatory Commission}, ``{Operator Licensing}.'' \url{https://www.nrc.gov/reactors/operator-licensing}.
-
-\bibitem{10CFR55}
-{U.S. Nuclear Regulatory Commission}, ``{Part 55—Operators' Licenses}.'' \url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}.
-
-\bibitem{10CFR50.54}
-{U.S. Nuclear Regulatory Commission}, ``{§ 50.54 Conditions of Licenses}.'' \url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}.
-
-\bibitem{Kemeny1979}
-J.~G. Kemeny {\em et~al.}, ``Report of the president's commission on the accident at three mile island,'' tech. rep., President's Commission on the Accident at Three Mile Island, October 1979.
-
-\bibitem{WNA2020}
-{World Nuclear Association}, ``Safety of nuclear power reactors.'' \url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}, 2020.
-
-\bibitem{hogberg_root_2013}
-L.~Högberg, ``Root causes and impacts of severe accidents at large nuclear power plants,'' vol.~42, no.~3, pp.~267--284.
-
-\bibitem{zhang_analysis_2025}
-M.~Zhang, L.~Dai, W.~Chen, and E.~Pang, ``Analysis of human errors in nuclear power plant event reports,'' vol.~57, no.~10, p.~103687.
-
-\bibitem{Kiniry2024}
-J.~Kiniry, A.~Bakst, S.~Hansen, M.~Podhradsky, and A.~Bivin, ``High assurance rigorous digital engineering for nuclear safety (hardens) final technical report,'' Tech. Rep. TLR-RES-RES/DE-2024-005, Galois, Inc. / U.S. Nuclear Regulatory Commission, 2024.
-\newblock NRC Contract 31310021C0014.
-
-\bibitem{eia_lcoe_2022}
-{U.S. Energy Information Administration}, ``Levelized costs of new generation resources in the annual energy outlook 2022,'' report, U.S. Energy Information Administration, March 2022.
-\newblock See Table 1b, page 9.
-
-\bibitem{eesi_datacenter_2024}
-{Environmental and Energy Study Institute}, ``Data center energy needs are upending power grids and threatening the climate.'' Web article, 2024.
-\newblock Accessed: 2025-09-29.
-
-\end{thebibliography}

main.blg

@@ -1,67 +0,0 @@
-This is BibTeX, Version 0.99d (TeX Live 2025)
-Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
-The top-level auxiliary file: main.aux
-White space in argument---line 23 of file main.aux
- : \citation{HANDBOOK
- :                    ON HYBRID SYSTEMS}
-I'm skipping whatever remains of this command
-White space in argument---line 30 of file main.aux
- : \citation{MANYUS
- :                  THESIS}
-I'm skipping whatever remains of this command
-The style file: ieeetr.bst
-Database file #1: references.bib
-Warning--entry type for "gentillon_westinghouse_1999" isn't style-file defined
---line 32 of file references.bib
-Warning--entry type for "operator_statistics" isn't style-file defined
---line 45 of file references.bib
-Warning--entry type for "10CFR50.54" isn't style-file defined
---line 59 of file references.bib
-Warning--empty author in WRPS.Description
-Warning--empty year in WRPS.Description
-Warning--empty journal in hogberg_root_2013
-Warning--empty year in hogberg_root_2013
-Warning--empty journal in zhang_analysis_2025
-Warning--empty year in zhang_analysis_2025
-You've used 15 entries,
-            1876 wiz_defined-function locations,
-            555 strings with 5820 characters,
-and the built_in function-call counts, 2404 in all, are:
-= -- 221
-> -- 100
-< -- 2
-+ -- 42
-- -- 27
-* -- 143
-:= -- 371
-add.period$ -- 18
-call.type$ -- 15
-change.case$ -- 18
-chr.to.int$ -- 0
-cite$ -- 21
-duplicate$ -- 102
-empty$ -- 259
-format.name$ -- 27
-if$ -- 575
-int.to.chr$ -- 0
-int.to.str$ -- 15
-missing$ -- 2
-newline$ -- 52
-num.names$ -- 14
-pop$ -- 64
-preamble$ -- 1
-purify$ -- 0
-quote$ -- 0
-skip$ -- 78
-stack$ -- 0
-substring$ -- 44
-swap$ -- 22
-text.length$ -- 2
-text.prefix$ -- 0
-top$ -- 0
-type$ -- 0
-warning$ -- 6
-while$ -- 18
-width$ -- 17
-write$ -- 128
-(There were 2 error messages)

main.toc

@@ -2,26 +2,27 @@
 \contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}%
 \contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}%
 \contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}%
-\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}%
+\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}%
 \contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}%
-\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}%
+\contentsline {subsubsection}{\numberline {2.3.1}HARDENS: The State of Formal Methods in Nuclear Control}{5}{}%
-\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}%
+\contentsline {subsubsection}{\numberline {2.3.2}Differential Dynamic Logic: Post-Hoc Hybrid Verification}{6}{}%
-\contentsline {section}{\numberline {3}Research Approach}{7}{}%
+\contentsline {subsection}{\numberline {2.4}Summary: The Verification Gap}{6}{}%
-\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}%
+\contentsline {section}{\numberline {3}Research Approach}{8}{}%
-\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}%
+\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{9}{}%
-\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}%
+\contentsline {subsection}{\numberline {3.2}Discrete Controller Synthesis}{12}{}%
-\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}%
+\contentsline {subsection}{\numberline {3.3}Continuous Control Modes}{13}{}%
-\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}%
+\contentsline {subsubsection}{\numberline {3.3.1}Transitory Modes}{14}{}%
-\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}%
+\contentsline {subsubsection}{\numberline {3.3.2}Stabilizing Modes}{15}{}%
-\contentsline {section}{\numberline {4}Metrics for Success}{15}{}%
+\contentsline {subsubsection}{\numberline {3.3.3}Expulsory Modes}{16}{}%
-\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}%
+\contentsline {subsection}{\numberline {3.4}Industrial Implementation}{16}{}%
-\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}%
+\contentsline {section}{\numberline {4}Metrics for Success}{19}{}%
-\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}%
+\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{19}{}%
-\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}%
+\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{19}{}%
-\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}%
+\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{20}{}%
-\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}%
+\contentsline {section}{\numberline {5}Risks and Contingencies}{21}{}%
-\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}%
+\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{21}{}%
-\contentsline {section}{\numberline {6}Broader Impacts}{20}{}%
+\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{21}{}%
-\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}%
+\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{22}{}%
-\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}%
+\contentsline {section}{\numberline {6}Broader Impacts}{25}{}%
-\contentsline {section}{References}{23}{}%
+\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{28}{}%
+\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{28}{}%