From c2d1c63bd045b74eb05a8903338ea93f083b3dc3 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Tue, 17 Mar 2026 20:51:04 -0400 Subject: [PATCH] figures are referenced --- 2-state-of-the-art/state-of-art.tex | 17 +- 3-research-approach/approach.tex | 330 +++++++++++----------------- 6-broader-impacts/impacts.tex | 4 +- 8-schedule/schedule.tex | 2 +- main.tex | 13 +- 5 files changed, 141 insertions(+), 225 deletions(-) diff --git a/2-state-of-the-art/state-of-art.tex b/2-state-of-the-art/state-of-art.tex index 744a608..cf4aea9 100644 --- a/2-state-of-the-art/state-of-art.tex +++ b/2-state-of-the-art/state-of-art.tex @@ -64,9 +64,7 @@ fundamental ambiguity: placing responsibility for safe power plant operations on the licensee without formal verification that operators can fulfill this responsibility does not guarantee safety. This tension between operational flexibility and safety assurance remains unresolved: the person responsible for -reactor safety is often the root cause of failures.\splitnote{``the person - responsible for reactor safety is often the root cause of failures'' — -devastating summary. Very effective.} +reactor safety is often the root cause of failures. Multiple independent analyses converge on a striking statistic: 70--80\% of nuclear power plant events are attributed to human error, versus @@ -78,16 +76,13 @@ Chinese nuclear power plants from 2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active errors, while 92\% were associated with latent errors---organizational and systemic weaknesses that create conditions for -failure.\splitnote{Strong empirical grounding. The Chinese plant data is a -nice addition — shows this isn't just a Western regulatory perspective.} - +failure. \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits that cannot be overcome through training alone.} The persistent human error contribution despite four decades of improvements demonstrates that these limitations are fundamental rather than a remediable part of -human-driven control.\splitnote{Well-stated. The ``four decades'' point -drives it home.} +human-driven control. \subsection{Formal Methods} \subsubsection{HARDENS} @@ -174,9 +169,9 @@ operators: true \end{itemize} These operators allow specification of safety properties ($\mathbf{G}\neg -\text{unsafe}$), liveness properties ($\mathbf{F}\text{target}$), and -response properties ($\mathbf{G}(\text{trigger} \rightarrow -\mathbf{F}\text{response})$). For nuclear control, this expressiveness +\textit{Unsafe}$), liveness properties ($\mathbf{F}\textit{ Target}$), and +response properties ($\mathbf{G}(\textit{Trigger} \rightarrow +\mathbf{F}\textit{ Response})$). For nuclear control, this expressiveness captures exactly the kinds of requirements that matter: the reactor must never enter an unsafe configuration, the system must eventually reach operating temperature, and if coolant pressure drops, shutdown must initiate diff --git a/3-research-approach/approach.tex b/3-research-approach/approach.tex index bc148ec..7cfcb59 100644 --- a/3-research-approach/approach.tex +++ b/3-research-approach/approach.tex @@ -11,14 +11,14 @@ For our systems of interest, the continuous states are physical quantities that are always Lipschitz continuous. This nomenclature is borrowed from the Handbook on Hybrid Systems Control \cite{lunze_handbook_2009}, but is redefined here for convenience: - +% \begin{equation} H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta, \mathcal{R}, Inv) \end{equation} - +% where: - +% \begin{itemize} \item $\mathcal{Q}$: the set of discrete states (modes) of the system \item $\mathcal{X} \subseteq \mathbb{R}^n$: the continuous state space @@ -39,20 +39,20 @@ where: HAHACS bridges the gap between discrete and continuous verification by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations using the framework of hybrid -automata~\cite{alur_hybrid_1993}. The -challenge of hybrid system verification lies in the interaction between discrete -and continuous dynamics. Discrete transitions change the active continuous -vector field, creating discontinuities in the system's behavior. Traditional -verification techniques designed for purely discrete or purely continuous -systems cannot handle this interaction directly. Our methodology addresses this -challenge through decomposition. We verify discrete switching logic and -continuous mode behavior separately, then compose these guarantees to reason -about the complete hybrid system. \addedprose{This compositional strategy follows -the assume-guarantee paradigm for hybrid systems, where guarantees about -individual modes compose into guarantees about the overall -system~\cite{lunze_handbook_2009, alur_hybrid_1993}.} This two-layer approach mirrors the structure of reactor -operations themselves: discrete supervisory logic determines which control mode -is active, while continuous controllers govern plant behavior within each mode. +automata~\cite{alur_hybrid_1993}. The challenge of hybrid system verification +lies in the interaction between discrete and continuous dynamics. Discrete +transitions change the active continuous vector field, creating discontinuities +in the system's behavior. Traditional verification techniques designed for +purely discrete or purely continuous systems cannot handle this interaction +directly. Our methodology addresses this challenge through decomposition. We +verify discrete switching logic and continuous mode behavior separately, then +compose these guarantees to reason about the complete hybrid system. This +compositional strategy follows the assume-guarantee paradigm for hybrid systems, +where guarantees about individual modes compose into guarantees about the +overall system~\cite{lunze_handbook_2009, alur_hybrid_1993}. This two-layer +approach mirrors the structure of reactor operations themselves: discrete +supervisory logic determines which control mode is active, while continuous +controllers govern plant behavior within each mode. The creation of a HAHACS amounts to the construction of such a tuple together with proof artifacts demonstrating that the intended behavior of the @@ -68,10 +68,10 @@ discrete level first, we transform the intractable problem of global hybrid verification into a collection of local verification problems with clear interfaces. Verification is performed per mode rather than on the full hybrid system, keeping the analysis tractable even for complex reactor -operations. \addedprose{Figure~\ref{fig:hybrid_automaton} illustrates this +operations. Figure~\ref{fig:hybrid_automaton} illustrates this structure for a simplified reactor startup sequence, showing discrete modes connected by guard-triggered transitions with continuous dynamics governing -behavior within each mode.} +behavior within each mode. \begin{figure} \centering @@ -132,23 +132,21 @@ behavior within each mode.} mode.} \label{fig:hybrid_automaton} \end{figure} -\dasnote{There's no reference of this figure in the prose. Perhaps some -explanation could be done in a paragraph to explain the thought process.} \subsection{System Requirements, Specifications, and Discrete Controllers} + Human control of nuclear power can be divided into three different scopes: strategic, operational, and tactical. Strategic control is high-level and long-term decision making for the plant. This level has objectives that are -complex and economic in scale, such as managing labor needs and supply chains -to optimize scheduled maintenance and downtime. The time scale at this level -is long, often spanning months or years. The lowest level of control is the +complex and economic in scale, such as managing labor needs and supply chains to +optimize scheduled maintenance and downtime. The time scale at this level is +long, often spanning months or years. The lowest level of control is the tactical level. This is the individual control of pumps, turbines, and -chemistry. Tactical control has already been somewhat automated in nuclear -power plants today, and is generally considered ``automatic control'' when -autonomous. These controls are almost always continuous systems with a direct -impact on the physical state of the -plant. Tactical control objectives include, but are not limited -to, maintaining pressurizer level, maintaining core temperature, or +chemistry. Tactical control has already been somewhat automated in nuclear power +plants today, and is generally considered ``automatic control'' when autonomous. +These controls are almost always continuous systems with a direct impact on the +physical state of the plant. Tactical control objectives include, but are not +limited to, maintaining pressurizer level, maintaining core temperature, or adjusting reactivity with a chemical shim. The level of control linking these two extremes is the operational control @@ -159,11 +157,9 @@ way, it bridges high-level and low-level goals. A strategic goal may be to perform refueling at a certain time, while the tactical level of the plant is currently focused on maintaining a certain core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along -the way to achieve this strategic -objective. - -%Say something about autonomous control systems near here? - +the way to achieve this strategic objective. This heiarchal division of control +scope and objectives is illustrated graphically in +figure~\ref{fig:strat_op_tact}. \begin{figure} \centering @@ -205,9 +201,7 @@ objective. \label{fig:strat_op_tact} \end{figure} - -\addedprose{As shown in Figure~\ref{fig:strat_op_tact}, nuclear plant control -spans three levels: strategic, operational, and tactical.} This operational control level is the main reason for the requirement of human +This operational control level is the main reason for the requirement of human operators in nuclear control today. The hybrid nature of this control system makes it difficult to prove what the behavior of the combined hybrid system will do across the entire state-space, so human operators have been used as a @@ -264,27 +258,17 @@ what remains to be done. Linear temporal logic (LTL) is particularly well-suited for specifying reactive systems. LTL formulas are built from atomic propositions (our discrete -predicates) using Boolean connectives and temporal operators. The key temporal -operators are: - -\begin{itemize} - \item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state - \item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states - \item $\mathbf{F}\phi$ (finally): $\phi$ holds in some future state - \item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes - true -\end{itemize} - -These operators allow us to express safety properties (``the reactor never -enters an unsafe configuration''), liveness properties (``the system -eventually reaches operating temperature''), and response properties (``if -coolant pressure drops, the system initiates shutdown within bounded -time''). \addedprose{We note that FRET's realizability checking currently -supports safety and bounded response properties but not general liveness -properties~\cite{katis_realizability_2022}. Liveness requirements such as -``eventually reaches operating temperature'' are instead verified through -the continuous mode analysis described in Section~3.2, where reachability -analysis confirms that target states are attained within bounded time.} +predicates) using Boolean connectives and temporal operators. These operators +allow us to express safety properties (``the reactor never enters an unsafe +configuration''), liveness properties (``the system eventually reaches operating +temperature''), and response properties (``if coolant pressure drops, the system +initiates shutdown within bounded time''). We note that FRET's realizability +checking currently supports safety and bounded response properties but not +general liveness properties~\cite{katis_realizability_2022}. Liveness +requirements such as ``eventually reaches operating temperature'' are instead +verified through the continuous mode analysis described in Section~3.2, where +reachability analysis can confirm that target states are attained within bounded +time. To build these temporal logic statements, an intermediary tool called FRET is planned to be used. FRET stands for Formal Requirements Elicitation Tool, and @@ -312,13 +296,12 @@ addressed. Pressburger and Katis.} Once system requirements are defined as temporal logic specifications, we use -them to build the discrete control system. To do this, reactive synthesis -tools are employed. Reactive synthesis is a field in computer science that -deals with the automated creation of reactive programs from temporal logic -specifications. A reactive program is one that, for a given state, takes an -input and produces an output~\cite{jacobs_reactive_2024}. Our systems fit -exactly this mold: the current -discrete state and status of guard conditions are the input, while the +them to build the discrete control system. To do this, reactive synthesis tools +are employed. Reactive synthesis is a field in computer science that deals with +the automated creation of reactive programs from temporal logic specifications. +A reactive program is one that, for a given state, takes an input and produces +an output~\cite{jacobs_reactive_2024}. Our systems fit exactly this mold: the +current discrete state and status of guard conditions are the input, while the output is the next discrete state. Reactive synthesis solves the following problem: given an LTL formula $\varphi$ @@ -346,18 +329,18 @@ Second, by defining system behavior in temporal logic and synthesizing the controller using deterministic algorithms, discrete control decisions become provably consistent with operating procedures. -\addedprose{The output of reactive synthesis is a finite-state machine that can -be directly translated to executable code. Tools such as -Strix~\cite{meyer_strix_2018} accept full LTL specifications and produce -Mealy machines via parity game solving~\cite{katis_capture_2022}. For -specifications within the GR(1) fragment---which captures the reactive -input-output structure typical of supervisory control---synthesis is -efficient and scales to specifications with thousands of states. Nuclear -operating procedures are well-suited to this fragment: environment inputs -correspond to plant state measurements and guard conditions, while outputs -are mode transition commands. The synthesized automaton provides a -correct-by-construction implementation that can be compiled to run on -industrial control hardware without manual translation of the control logic.} +The output of reactive synthesis is a finite-state machine that can be directly +translated to executable code. Tools such as Strix~\cite{meyer_strix_2018} +accept full LTL specifications and produce Mealy machines via parity game +solving~\cite{katis_capture_2022}. For specifications within the GR(1) +fragment---which captures the reactive input-output structure typical of +supervisory control---synthesis is efficient and scales to specifications with +thousands of states. Nuclear operating procedures are well-suited to this +fragment: environment inputs correspond to plant state measurements and guard +conditions, while outputs are mode transition commands. The synthesized +automaton provides a correct-by-construction implementation that can be compiled +to run on industrial control hardware without manual translation of the control +logic. \subsection{Continuous Control Modes} @@ -393,8 +376,9 @@ We circumvent these issues by designing our hybrid system from the bottom up with verification in mind. Each continuous control mode has an input set and output set clearly defined by our discrete transitions \textit{a priori}. Consider that we define the continuous state space as $\mathcal{X}$. Each -discrete mode $q_i$ then provides three key pieces of information for -continuous controller design: +discrete mode $q_i$ then provides three key pieces of information for continuous +controller design: +% \begin{enumerate} \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$, the set of possible initial states when entering this mode @@ -405,23 +389,16 @@ continuous controller design: \mathcal{X}$, the envelope of safe states during operation in this mode. These are derived from invariants \(Inv\). \end{enumerate} +% These sets come directly from the discrete controller synthesis and define precise objectives for continuous control.\dasnote{This SOUNDS like assume-guarantee stuff. Maybe make that connection formal and cite it?} 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}$.\splitnote{This compositional approach is formalized -in Kapuria 2025 (pp.17-24, Section 2.4): component proofs via differential -cuts reduce state-space (DC rule, p.20), then system proof composes via -differential invariants (DI rule, pp.22-24). Kapuria proves SmAHTR safety by -verifying 6 components in isolation then system---your three-mode structure -maps perfectly to this decomposition, reducing verification complexity from -curse of dimensionality.} - -We classify continuous controllers into three types based on their objectives: -transitory, stabilizing, and expulsory. Each type has distinct verification -requirements that determine which formal methods tools are appropriate. +$\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while remaining +within $\mathcal{X}_{safe,i}$. We classify continuous controllers into three +types based on their objectives: transitory, stabilizing, and expulsory. Each +type has distinct verification requirements that determine which formal methods +tools are appropriate. \dasinline{(1) Add figure showing the relationship between entry/exit/safety sets. (2) Mention assume-guarantee compositional stuff and how that fits in @@ -439,33 +416,38 @@ The control objective for a transitory mode can be stated formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x)$, the controller must satisfy: +% \[ \forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \mathcal{X}_{exit} \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe} \] +% That is, from any valid entry state, the trajectory must eventually reach the exit condition without ever leaving the safe region. Verification of transitory modes will use reachability analysis. Reachability -analysis computes the set of all states reachable from a given initial set -under the system dynamics~\cite{guernic_reachability_2009, +analysis computes the set of all states reachable from a given initial set under +the system dynamics~\cite{guernic_reachability_2009, mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017}. For a transitory -mode to be valid, the reachable -set from $\mathcal{X}_{entry}$ must satisfy two conditions: +mode to be valid, the reachable set from $\mathcal{X}_{entry}$ must satisfy two +conditions: +% \begin{enumerate} \item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the mode achieves its objective) \item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is maintained throughout the transition) \end{enumerate} -Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the -states reachable within time horizon $T$: +% +Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the states +reachable within time horizon $T$: +% \[ \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \subseteq \mathcal{X}_{safe} \land \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset \] - +% Because the discrete controller defines clear boundaries in continuous state space, the verification problem for each transitory mode is well-posed. We know the possible initial conditions, we know the target @@ -474,31 +456,12 @@ confirm that the candidate continuous controller achieves the objective from all possible starting points. Several tools exist for computing reachable sets of hybrid systems, including -CORA, Flow*, SpaceEx~\cite{frehse_spaceex_2011}, and JuliaReach. The choice -of tool depends on the -structure of the continuous dynamics. Linear systems admit efficient -polyhedral or ellipsoidal reachability computations. Nonlinear systems +CORA, Flow*, SpaceEx~\cite{frehse_spaceex_2011}, and JuliaReach. The choice of +tool depends on the structure of the continuous dynamics. Linear systems admit +efficient polyhedral or ellipsoidal reachability computations. Nonlinear systems require more conservative over-approximations using techniques such as Taylor -models or polynomial zonotopes. For this work, we will select tools -appropriate to the fidelity of the reactor models -available.\splitnote{Your toolset is well-justified: SpaceEx (Frehse 2011, -pp.3-6) handles hybrid automata via support functions; Flow* (Chen 2013) -uses Taylor models for nonlinear dynamics; JuliaReach (Bogomolov 2019, -pp.1-2) offers flexible set representations (zonotopes, boxes). Kapuria 2025 -(pp.11-12, Section 2.2) uses Flow* successfully for SmAHTR reachability with -reactor models showing state-space constraints (e.g., temp -673--677\textdegree{}C, Figures 6, 16--20). This validates your tool choices -for nuclear systems.}\splitnote{Critical finding from Kapuria 2025: -decomposition-based verification (pp.17-24, Section 2.4) proves component -safety in isolation using reachability, THEN composes to system proof via -differential invariants---your three-mode taxonomy maps cleanly to component -verification, reducing complexity from monolithic analysis.} - -%%% NOTES (Section 4.1): -% - Add timing constraints discussion: what if the transition takes too long? -% - Consider timed reachability for systems with deadline requirements -% - Mention that the Mealy machine perspective unifies this: continuous system -% IS the transition, entry/exit conditions are the discrete states +models or polynomial zonotopes. For this work, we will select tools appropriate +to the fidelity of the reactor models available. \subsubsection{Stabilizing Modes} @@ -515,19 +478,20 @@ evaluate whether any trajectory leaves a given boundary. This definition is exactly what defines the validity of a stabilizing continuous control mode. A barrier certificate (or control barrier function) is a scalar function $B: -\mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a -safe set. The idea is analogous to Lyapunov functions for -stability~\cite{branicky_multiple_1998}: rather -than computing trajectories explicitly, we find a certificate function whose -properties guarantee the desired behavior. For a safe set $\mathcal{C} = -\{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$, -the\dasinline{Should clarify that the safe set C is not the entire -continuous region. It's just the boundary of the region.} barrier certificate -condition requires: +\mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a safe +set. The idea is analogous to Lyapunov functions for +stability~\cite{branicky_multiple_1998}: rather than computing trajectories +explicitly, we find a certificate function whose properties guarantee the +desired behavior. For a safe set $\mathcal{C} = \{x : B(x) \geq 0\}$ and +dynamics $\dot{x} = f(x,u)$, the\dasinline{Should clarify that the safe set C is +not the entire continuous region. It's just the boundary of the region.} barrier +certificate condition requires: +% \[ \forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x)) \geq 0 \] +% This condition states that on the boundary of the safe set (where $B(x) = 0$), the time derivative of $B$ is non-negative. Geometrically, this means the vector field points inward or tangent to the boundary, never outward. If @@ -544,34 +508,23 @@ certificate confirms that the candidate controller achieves this invariance. Finding barrier certificates can be formulated as a sum-of-squares (SOS) optimization problem for polynomial systems, or solved using satisfiability modulo theories (SMT) solvers for broader classes of -dynamics~\cite{prajna_safety_2004, kapuria_using_2025}. The key -advantage is that the verification is independent of how the controller was -designed. Standard control techniques can be used to build continuous -controllers, and barrier certificates provide a separate check that the -result satisfies the required invariants. This also allows for the checking -of control modes with different models than they are designed for. For -example, a lower fidelity model can be used for controller design, but a -higher fidelity model can be used for the actual validation of that -stabilizing controller.\splitnote{SOS methods proven effective: -Papachristodoulou 2021 (SOSTOOLS v4, pp.1-2) solves barrier certificate -optimization via SOS constraints---tool integrates with MATLAB. Borrmann -2015 (pp.4-8) demonstrates control barrier certificates for multi-agent -systems, showing how discrete boundaries (mode guards) can inform barrier -design. Your claim that discrete specs eliminate barrier search is novel and -well-supported by these foundations.}\splitnote{Hauswirth 2024 (pp.1-3) -shows optimization-based robust feedback controllers can serve as -alternative verification method---suggests barrier certificates + -reachability provide complementary guarantees for your stabilizing modes.} - -%%% NOTES (Section 4.2): -% - Clarify relationship between barrier certificates and Lyapunov stability -% - Discuss what happens at mode boundaries: barrier for this mode vs guard -% for transition -% - Mention tools: SOSTOOLS, dReal, barrier function synthesis methods - -% ---------------------------------------------------------------------------- -% 4.3 EXPULSORY MODES -% ---------------------------------------------------------------------------- +dynamics~\cite{prajna_safety_2004, kapuria_using_2025}. The key advantage is +that the verification is independent of how the controller was designed. +Standard control techniques can be used to build continuous controllers, and +barrier certificates provide a separate check that the result satisfies the +required invariants. This also allows for the checking of control modes with +different models than they are designed for. For example, a lower fidelity model +can be used for controller design, but a higher fidelity model can be used for +the actual validation of that stabilizing controller.\splitnote{SOS methods + proven effective: Papachristodoulou 2021 (SOSTOOLS v4, pp.1-2) solves barrier + certificate optimization via SOS constraints---tool integrates with MATLAB. + Borrmann 2015 (pp.4-8) demonstrates control barrier certificates for + multi-agent systems, showing how discrete boundaries (mode guards) can inform + barrier design. Your claim that discrete specs eliminate barrier search is + novel and well-supported by these foundations.}\splitnote{Hauswirth 2024 + (pp.1-3) shows optimization-based robust feedback controllers can serve as +alternative verification method---suggests barrier certificates + reachability +provide complementary guarantees for your stabilizing modes.} \subsubsection{Expulsory Modes} @@ -591,27 +544,29 @@ key ways. First, the entry conditions may be the entire state space (or a large, conservatively bounded region) rather than a well-defined entry set. The failure may occur at any point during operation. Second, the dynamics include parametric uncertainty representing failure modes: - +% \[ \dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure} \] - +% where $\Theta_{failure}$ captures the range of possible degraded plant behaviors identified through failure mode and effects analysis (FMEA) or -traditional safety analysis. \addedprose{While tools such as SpaceEx handle -nondeterministic inputs~\cite{frehse_spaceex_2011}, parametric plant -uncertainty requires conservative over-approximation of reachable sets -across the full parameter range.} +traditional safety analysis. We verify expulsory modes using reachability analysis with parametric -uncertainty. The verification condition requires that for all parameter -values within the uncertainty set, trajectories from the expanded entry -region reach the safe shutdown state: +uncertainty. While tools such as SpaceEx handle nondeterministic +inputs~\cite{frehse_spaceex_2011}, parametric plant uncertainty requires +conservative over-approximation of reachable sets across the full parameter +range. The verification condition requires that for all parameter values within +the uncertainty set, trajectories from the expanded entry region reach the safe +shutdown state: +% \[ \forall \theta \in \Theta_{failure}: \text{Reach}(\mathcal{X}_{current}, f_\theta, [0,T]) \subseteq \mathcal{X}_{shutdown} \] +% This is more conservative than nominal reachability, accounting for the fact that we cannot know exactly which failure mode is active. @@ -629,23 +584,6 @@ $\delta$-SAT) to handle nonlinear uncertainty---demonstrates your expulsory mode approach is sound for nuclear failures. Shows safety can be proven even when controller deviates from nominal (pp.85-107, UCA 1 analysis).} -\addedprose{The construction of $\Theta_{\text{failure}}$ follows a -systematic process: traditional safety analysis techniques (FMEA, -probabilistic risk assessment, design basis accident analysis) identify -credible failure scenarios, which are then mapped to parametric bounds -on the plant dynamics. Kapuria~\cite{kapuria_using_2025} demonstrates -this process for SmAHTR, deriving uncertainty sets from unsafe control -actions identified through STPA.} - -%%% NOTES (Section 4.3): -% - Discuss sensor failures vs actual plant failures -% - Address unmodeled disturbances that aren't failures -% - How much parametric uncertainty is enough? Need methodology for bounds -% - Mention graceful degradation: graded responses vs immediate SCRAM - -% ---------------------------------------------------------------------------- -% 5. INDUSTRIAL IMPLEMENTATION -% ---------------------------------------------------------------------------- \subsection{Industrial Implementation} @@ -673,21 +611,3 @@ system experts at Emerson ensures that implementation details of the Ovation platform are handled correctly. Direct industry collaboration also provides an immediate pathway for technology transfer and alignment with practical deployment requirements. - -\addedprose{A critical integration concern is maintaining formal guarantees -through the implementation pipeline. Pressburger et -al.~\cite{pressburger_using_2023} describe manual integration of -formally specified monitors into executable systems, noting -opportunities for automation to reduce this gap. To mitigate this risk, -the ARCADE interface will support automated code generation from the -synthesized automaton, ensuring that the controller deployed on Ovation -hardware preserves the verified behavior without manual re-implementation -of control logic.} - -%%% NOTES (Section 5): -% - Get specific details on ARCADE interface from Emerson collaboration -% - Mention what startup sequence will be demonstrated (cold shutdown -% $\rightarrow$ criticality $\rightarrow$ low power?) -% - Discuss how off-nominal scenarios will be tested (sensor failures, -% simulated component degradation) -% - Reference Westinghouse relationship if relevant diff --git a/6-broader-impacts/impacts.tex b/6-broader-impacts/impacts.tex index a2d12bb..95c2025 100644 --- a/6-broader-impacts/impacts.tex +++ b/6-broader-impacts/impacts.tex @@ -9,7 +9,7 @@ transmission losses and eliminate emissions from hydrocarbon-based alternatives. However, nuclear power economics at this scale demand careful attention to operating costs. -\addedprose{According to the U.S. Energy Information Administration's Annual +According to the U.S. Energy Information Administration's Annual Energy Outlook 2022, advanced nuclear power entering service in 2027 is projected to cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. In the United States alone, datacenter electricity consumption could reach 560 @@ -22,7 +22,7 @@ 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 the total levelized cost of electricity, translating to \$11--15 billion annually for projected U.S. -datacenter demand alone.} +datacenter demand alone. This research directly addresses the multi-billion-dollar O\&M cost challenge through high-assurance autonomous control. Current nuclear operations require diff --git a/8-schedule/schedule.tex b/8-schedule/schedule.tex index 3b46314..9edd307 100644 --- a/8-schedule/schedule.tex +++ b/8-schedule/schedule.tex @@ -93,4 +93,4 @@ methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical implementability on industrial hardware. This milestone delivers a conference paper submission to NPIC\&HMIT or CDC documenting hardware implementation and experimental validation. M6 (Month 24) completes the dissertation documenting -the entire methodology, experimental results, and research contributions.\splitnote{Clear timeline with publication targets — shows you have a plan.} +the entire methodology, experimental results, and research contributions. diff --git a/main.tex b/main.tex index 9b35bea..3d73208 100644 --- a/main.tex +++ b/main.tex @@ -68,24 +68,25 @@ \pagenumbering{arabic} \input{1-goals-and-outcomes/goals} -\newpage +% \newpage \input{2-state-of-the-art/state-of-art} -\newpage +% \newpage \input{3-research-approach/approach} -\newpage +% \newpage \input{4-metrics-of-success/metrics} -\newpage +% \newpage \input{5-risks-and-contingencies/risks} -\newpage +% \newpage \input{6-broader-impacts/impacts} -\newpage +% \newpage \input{8-schedule/schedule} +\newpage \bibliographystyle{ieeetr} \bibliography{references}