danesabo/Thesis
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

figures are referenced

Browse Source
This commit is contained in:
Dane Sabo 2026-03-17 20:51:04 -04:00
parent 449256f665
commit c2d1c63bd0
5 changed files with 141 additions and 225 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
2-state-of-the-art/state-of-art.tex
View File

@ -64,9 +64,7 @@ fundamental ambiguity: placing responsibility for safe power plant operations on
the licensee without formal verification that operators can fulfill this the licensee without formal verification that operators can fulfill this
responsibility does not guarantee safety. This tension between operational responsibility does not guarantee safety. This tension between operational
flexibility and safety assurance remains unresolved: the person responsible for flexibility and safety assurance remains unresolved: the person responsible for
reactor safety is often the root cause of failures.\splitnote{``the person reactor safety is often the root cause of failures.
responsible for reactor safety is often the root cause of failures'' —
devastating summary. Very effective.}
Multiple independent analyses converge on a striking statistic: 70--80\% of Multiple independent analyses converge on a striking statistic: 70--80\% of
nuclear power plant events are attributed to human error, versus 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 2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved
active errors, while 92\% were associated with latent active errors, while 92\% were associated with latent
errors---organizational and systemic weaknesses that create conditions for errors---organizational and systemic weaknesses that create conditions for
failure.\splitnote{Strong empirical grounding. The Chinese plant data is a failure.
nice addition — shows this isn't just a Western regulatory perspective.}
\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability
limits that cannot be overcome through training alone.} The persistent human limits that cannot be overcome through training alone.} The persistent human
error contribution despite four decades of improvements demonstrates that error contribution despite four decades of improvements demonstrates that
these limitations are fundamental rather than a remediable part of these limitations are fundamental rather than a remediable part of
human-driven control.\splitnote{Well-stated. The ``four decades'' point human-driven control.
drives it home.}
\subsection{Formal Methods} \subsection{Formal Methods}
\subsubsection{HARDENS} \subsubsection{HARDENS}
@ -174,9 +169,9 @@ operators:
true true
\end{itemize} \end{itemize}
These operators allow specification of safety properties ($\mathbf{G}\neg These operators allow specification of safety properties ($\mathbf{G}\neg
\text{unsafe}$), liveness properties ($\mathbf{F}\text{target}$), and \textit{Unsafe}$), liveness properties ($\mathbf{F}\textit{ Target}$), and
response properties ($\mathbf{G}(\text{trigger} \rightarrow response properties ($\mathbf{G}(\textit{Trigger} \rightarrow
\mathbf{F}\text{response})$). For nuclear control, this expressiveness \mathbf{F}\textit{ Response})$). For nuclear control, this expressiveness
captures exactly the kinds of requirements that matter: the reactor must captures exactly the kinds of requirements that matter: the reactor must
never enter an unsafe configuration, the system must eventually reach never enter an unsafe configuration, the system must eventually reach
operating temperature, and if coolant pressure drops, shutdown must initiate operating temperature, and if coolant pressure drops, shutdown must initiate

330
3-research-approach/approach.tex
View File

@ -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 that are always Lipschitz continuous. This nomenclature is borrowed from the
Handbook on Hybrid Systems Control \cite{lunze_handbook_2009}, but is Handbook on Hybrid Systems Control \cite{lunze_handbook_2009}, but is
redefined here for convenience: redefined here for convenience:
%
\begin{equation} \begin{equation}
H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta, H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta,
\mathcal{R}, Inv) \mathcal{R}, Inv)
\end{equation} \end{equation}
%
where: where:
%
\begin{itemize} \begin{itemize}
\item $\mathcal{Q}$: the set of discrete states (modes) of the system \item $\mathcal{Q}$: the set of discrete states (modes) of the system
\item $\mathcal{X} \subseteq \mathbb{R}^n$: the continuous state space \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 HAHACS bridges the gap between discrete and continuous verification by composing
formal methods from computer science with control-theoretic verification, formal methods from computer science with control-theoretic verification,
formalizing reactor operations using the framework of hybrid formalizing reactor operations using the framework of hybrid
automata~\cite{alur_hybrid_1993}. The automata~\cite{alur_hybrid_1993}. The challenge of hybrid system verification
challenge of hybrid system verification lies in the interaction between discrete lies in the interaction between discrete and continuous dynamics. Discrete
and continuous dynamics. Discrete transitions change the active continuous transitions change the active continuous vector field, creating discontinuities
vector field, creating discontinuities in the system's behavior. Traditional in the system's behavior. Traditional verification techniques designed for
verification techniques designed for purely discrete or purely continuous purely discrete or purely continuous systems cannot handle this interaction
systems cannot handle this interaction directly. Our methodology addresses this directly. Our methodology addresses this challenge through decomposition. We
challenge through decomposition. We verify discrete switching logic and verify discrete switching logic and continuous mode behavior separately, then
continuous mode behavior separately, then compose these guarantees to reason compose these guarantees to reason about the complete hybrid system. This
about the complete hybrid system. \addedprose{This compositional strategy follows compositional strategy follows the assume-guarantee paradigm for hybrid systems,
the assume-guarantee paradigm for hybrid systems, where guarantees about where guarantees about individual modes compose into guarantees about the
individual modes compose into guarantees about the overall overall system~\cite{lunze_handbook_2009, alur_hybrid_1993}. This two-layer
system~\cite{lunze_handbook_2009, alur_hybrid_1993}.} This two-layer approach mirrors the structure of reactor approach mirrors the structure of reactor operations themselves: discrete
operations themselves: discrete supervisory logic determines which control mode supervisory logic determines which control mode is active, while continuous
is active, while continuous controllers govern plant behavior within each mode. controllers govern plant behavior within each mode.
The creation of a HAHACS amounts to the construction of such a tuple The creation of a HAHACS amounts to the construction of such a tuple
together with proof artifacts demonstrating that the intended behavior of the 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 verification into a collection of local verification problems with clear
interfaces. Verification is performed per mode rather than on the full interfaces. Verification is performed per mode rather than on the full
hybrid system, keeping the analysis tractable even for complex reactor 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 structure for a simplified reactor startup sequence, showing discrete modes
connected by guard-triggered transitions with continuous dynamics governing connected by guard-triggered transitions with continuous dynamics governing
behavior within each mode.} behavior within each mode.
\begin{figure} \begin{figure}
\centering \centering
@ -132,23 +132,21 @@ behavior within each mode.}
mode.} mode.}
\label{fig:hybrid_automaton} \label{fig:hybrid_automaton}
\end{figure} \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} \subsection{System Requirements, Specifications, and Discrete Controllers}
Human control of nuclear power can be divided into three different scopes: Human control of nuclear power can be divided into three different scopes:
strategic, operational, and tactical. Strategic control is high-level and strategic, operational, and tactical. Strategic control is high-level and
long-term decision making for the plant. This level has objectives that are 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 complex and economic in scale, such as managing labor needs and supply chains to
to optimize scheduled maintenance and downtime. The time scale at this level optimize scheduled maintenance and downtime. The time scale at this level is
is long, often spanning months or years. The lowest level of control is the long, often spanning months or years. The lowest level of control is the
tactical level. This is the individual control of pumps, turbines, and tactical level. This is the individual control of pumps, turbines, and
chemistry. Tactical control has already been somewhat automated in nuclear chemistry. Tactical control has already been somewhat automated in nuclear power
power plants today, and is generally considered ``automatic control'' when plants today, and is generally considered ``automatic control'' when autonomous.
autonomous. These controls are almost always continuous systems with a direct These controls are almost always continuous systems with a direct impact on the
impact on the physical state of the physical state of the plant. Tactical control objectives include, but are not
plant. Tactical control objectives include, but are not limited limited to, maintaining pressurizer level, maintaining core temperature, or
to, maintaining pressurizer level, maintaining core temperature, or
adjusting reactivity with a chemical shim. adjusting reactivity with a chemical shim.
The level of control linking these two extremes is the operational control 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 perform refueling at a certain time, while the tactical level of the plant is
currently focused on maintaining a certain core temperature. The operational currently focused on maintaining a certain core temperature. The operational
level issues the shutdown procedure, using several smaller tactical goals along level issues the shutdown procedure, using several smaller tactical goals along
the way to achieve this strategic the way to achieve this strategic objective. This heiarchal division of control
objective. scope and objectives is illustrated graphically in
figure~\ref{fig:strat_op_tact}.
%Say something about autonomous control systems near here?
\begin{figure} \begin{figure}
\centering \centering
@ -205,9 +201,7 @@ objective.
\label{fig:strat_op_tact} \label{fig:strat_op_tact}
\end{figure} \end{figure}
This operational control level is the main reason for the requirement of human
\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
operators in nuclear control today. The hybrid nature of this control system 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 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 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 Linear temporal logic (LTL) is particularly well-suited for specifying reactive
systems. LTL formulas are built from atomic propositions (our discrete systems. LTL formulas are built from atomic propositions (our discrete
predicates) using Boolean connectives and temporal operators. The key temporal predicates) using Boolean connectives and temporal operators. These operators
operators are: allow us to express safety properties (``the reactor never enters an unsafe
configuration''), liveness properties (``the system eventually reaches operating
\begin{itemize} temperature''), and response properties (``if coolant pressure drops, the system
\item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state initiates shutdown within bounded time''). We note that FRET's realizability
\item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states checking currently supports safety and bounded response properties but not
\item $\mathbf{F}\phi$ (finally): $\phi$ holds in some future state general liveness properties~\cite{katis_realizability_2022}. Liveness
\item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes requirements such as ``eventually reaches operating temperature'' are instead
true verified through the continuous mode analysis described in Section~3.2, where
\end{itemize} reachability analysis can confirm that target states are attained within bounded
time.
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.}
To build these temporal logic statements, an intermediary tool called FRET is To build these temporal logic statements, an intermediary tool called FRET is
planned to be used. FRET stands for Formal Requirements Elicitation Tool, and planned to be used. FRET stands for Formal Requirements Elicitation Tool, and
@ -312,13 +296,12 @@ addressed.
Pressburger and Katis.} Pressburger and Katis.}
Once system requirements are defined as temporal logic specifications, we use Once system requirements are defined as temporal logic specifications, we use
them to build the discrete control system. To do this, reactive synthesis them to build the discrete control system. To do this, reactive synthesis tools
tools are employed. Reactive synthesis is a field in computer science that are employed. Reactive synthesis is a field in computer science that deals with
deals with the automated creation of reactive programs from temporal logic the automated creation of reactive programs from temporal logic specifications.
specifications. A reactive program is one that, for a given state, takes an A reactive program is one that, for a given state, takes an input and produces
input and produces an output~\cite{jacobs_reactive_2024}. Our systems fit an output~\cite{jacobs_reactive_2024}. Our systems fit exactly this mold: the
exactly this mold: the current current discrete state and status of guard conditions are the input, while the
discrete state and status of guard conditions are the input, while the
output is the next discrete state. output is the next discrete state.
Reactive synthesis solves the following problem: given an LTL formula $\varphi$ 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 controller using deterministic algorithms, discrete control decisions become
provably consistent with operating procedures. provably consistent with operating procedures.
\addedprose{The output of reactive synthesis is a finite-state machine that can The output of reactive synthesis is a finite-state machine that can be directly
be directly translated to executable code. Tools such as translated to executable code. Tools such as Strix~\cite{meyer_strix_2018}
Strix~\cite{meyer_strix_2018} accept full LTL specifications and produce accept full LTL specifications and produce Mealy machines via parity game
Mealy machines via parity game solving~\cite{katis_capture_2022}. For solving~\cite{katis_capture_2022}. For specifications within the GR(1)
specifications within the GR(1) fragment---which captures the reactive fragment---which captures the reactive input-output structure typical of
input-output structure typical of supervisory control---synthesis is supervisory control---synthesis is efficient and scales to specifications with
efficient and scales to specifications with thousands of states. Nuclear thousands of states. Nuclear operating procedures are well-suited to this
operating procedures are well-suited to this fragment: environment inputs fragment: environment inputs correspond to plant state measurements and guard
correspond to plant state measurements and guard conditions, while outputs conditions, while outputs are mode transition commands. The synthesized
are mode transition commands. The synthesized automaton provides a automaton provides a correct-by-construction implementation that can be compiled
correct-by-construction implementation that can be compiled to run on to run on industrial control hardware without manual translation of the control
industrial control hardware without manual translation of the control logic.} logic.
\subsection{Continuous Control Modes} \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 with verification in mind. Each continuous control mode has an input set and
output set clearly defined by our discrete transitions \textit{a priori}. output set clearly defined by our discrete transitions \textit{a priori}.
Consider that we define the continuous state space as $\mathcal{X}$. Each Consider that we define the continuous state space as $\mathcal{X}$. Each
discrete mode $q_i$ then provides three key pieces of information for discrete mode $q_i$ then provides three key pieces of information for continuous
continuous controller design: controller design:
%
\begin{enumerate} \begin{enumerate}
\item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq
\mathcal{X}$, the set of possible initial states when entering this mode \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. \mathcal{X}$, the envelope of safe states during operation in this mode.
These are derived from invariants \(Inv\). These are derived from invariants \(Inv\).
\end{enumerate} \end{enumerate}
%
These sets come directly from the discrete controller synthesis and define These sets come directly from the discrete controller synthesis and define
precise objectives for continuous control.\dasnote{This SOUNDS like precise objectives for continuous control.\dasnote{This SOUNDS like
assume-guarantee stuff. Maybe make that connection formal and cite it?} The 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 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 $\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while remaining
remaining within within $\mathcal{X}_{safe,i}$. We classify continuous controllers into three
$\mathcal{X}_{safe,i}$.\splitnote{This compositional approach is formalized types based on their objectives: transitory, stabilizing, and expulsory. Each
in Kapuria 2025 (pp.17-24, Section 2.4): component proofs via differential type has distinct verification requirements that determine which formal methods
cuts reduce state-space (DC rule, p.20), then system proof composes via tools are appropriate.
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.
\dasinline{(1) Add figure showing the relationship between entry/exit/safety \dasinline{(1) Add figure showing the relationship between entry/exit/safety
sets. (2) Mention assume-guarantee compositional stuff and how that fits in 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 entry conditions $\mathcal{X}_{entry}$, exit conditions
$\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and
closed-loop dynamics $\dot{x} = f(x)$, the controller must satisfy: closed-loop dynamics $\dot{x} = f(x)$, the controller must satisfy:
%
\[ \[
\forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \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} \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 That is, from any valid entry state, the trajectory must eventually reach the
exit condition without ever leaving the safe region. exit condition without ever leaving the safe region.
Verification of transitory modes will use reachability analysis. Reachability Verification of transitory modes will use reachability analysis. Reachability
analysis computes the set of all states reachable from a given initial set analysis computes the set of all states reachable from a given initial set under
under the system dynamics~\cite{guernic_reachability_2009, the system dynamics~\cite{guernic_reachability_2009,
mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017}. For a transitory mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017}. For a transitory
mode to be valid, the reachable mode to be valid, the reachable set from $\mathcal{X}_{entry}$ must satisfy two
set from $\mathcal{X}_{entry}$ must satisfy two conditions: conditions:
%
\begin{enumerate} \begin{enumerate}
\item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the \item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the
mode achieves its objective) mode achieves its objective)
\item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is \item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is
maintained throughout the transition) maintained throughout the transition)
\end{enumerate} \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} \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \subseteq \mathcal{X}_{safe}
\land \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \land \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap
\mathcal{X}_{exit} \neq \emptyset \mathcal{X}_{exit} \neq \emptyset
\] \]
%
Because the discrete controller defines clear boundaries in Because the discrete controller defines clear boundaries in
continuous state space, the verification problem for each transitory mode is continuous state space, the verification problem for each transitory mode is
well-posed. We know the possible initial conditions, we know the target 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. all possible starting points.
Several tools exist for computing reachable sets of hybrid systems, including Several tools exist for computing reachable sets of hybrid systems, including
CORA, Flow*, SpaceEx~\cite{frehse_spaceex_2011}, and JuliaReach. The choice CORA, Flow*, SpaceEx~\cite{frehse_spaceex_2011}, and JuliaReach. The choice of
of tool depends on the tool depends on the structure of the continuous dynamics. Linear systems admit
structure of the continuous dynamics. Linear systems admit efficient efficient polyhedral or ellipsoidal reachability computations. Nonlinear systems
polyhedral or ellipsoidal reachability computations. Nonlinear systems
require more conservative over-approximations using techniques such as Taylor require more conservative over-approximations using techniques such as Taylor
models or polynomial zonotopes. For this work, we will select tools models or polynomial zonotopes. For this work, we will select tools appropriate
appropriate to the fidelity of the reactor models to the fidelity of the reactor models available.
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
\subsubsection{Stabilizing Modes} \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. exactly what defines the validity of a stabilizing continuous control mode.
A barrier certificate (or control barrier function) is a scalar function $B: A barrier certificate (or control barrier function) is a scalar function $B:
\mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a safe
safe set. The idea is analogous to Lyapunov functions for set. The idea is analogous to Lyapunov functions for
stability~\cite{branicky_multiple_1998}: rather stability~\cite{branicky_multiple_1998}: rather than computing trajectories
than computing trajectories explicitly, we find a certificate function whose explicitly, we find a certificate function whose properties guarantee the
properties guarantee the desired behavior. For a safe set $\mathcal{C} = desired behavior. For a safe set $\mathcal{C} = \{x : B(x) \geq 0\}$ and
\{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$, dynamics $\dot{x} = f(x,u)$, the\dasinline{Should clarify that the safe set C is
the\dasinline{Should clarify that the safe set C is not the entire not the entire continuous region. It's just the boundary of the region.} barrier
continuous region. It's just the boundary of the region.} barrier certificate certificate condition requires:
condition requires: %
\[ \[
\forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x)) \forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x))
\geq 0 \geq 0
\] \]
%
This condition states that on the boundary of the safe set (where $B(x) = 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 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 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) Finding barrier certificates can be formulated as a sum-of-squares (SOS)
optimization problem for polynomial systems, or solved using satisfiability optimization problem for polynomial systems, or solved using satisfiability
modulo theories (SMT) solvers for broader classes of modulo theories (SMT) solvers for broader classes of
dynamics~\cite{prajna_safety_2004, kapuria_using_2025}. The key dynamics~\cite{prajna_safety_2004, kapuria_using_2025}. The key advantage is
advantage is that the verification is independent of how the controller was that the verification is independent of how the controller was designed.
designed. Standard control techniques can be used to build continuous Standard control techniques can be used to build continuous controllers, and
controllers, and barrier certificates provide a separate check that the barrier certificates provide a separate check that the result satisfies the
result satisfies the required invariants. This also allows for the checking required invariants. This also allows for the checking of control modes with
of control modes with different models than they are designed for. For different models than they are designed for. For example, a lower fidelity model
example, a lower fidelity model can be used for controller design, but a can be used for controller design, but a higher fidelity model can be used for
higher fidelity model can be used for the actual validation of that the actual validation of that stabilizing controller.\splitnote{SOS methods
stabilizing controller.\splitnote{SOS methods proven effective: proven effective: Papachristodoulou 2021 (SOSTOOLS v4, pp.1-2) solves barrier
Papachristodoulou 2021 (SOSTOOLS v4, pp.1-2) solves barrier certificate certificate optimization via SOS constraints---tool integrates with MATLAB.
optimization via SOS constraints---tool integrates with MATLAB. Borrmann Borrmann 2015 (pp.4-8) demonstrates control barrier certificates for
2015 (pp.4-8) demonstrates control barrier certificates for multi-agent multi-agent systems, showing how discrete boundaries (mode guards) can inform
systems, showing how discrete boundaries (mode guards) can inform barrier barrier design. Your claim that discrete specs eliminate barrier search is
design. Your claim that discrete specs eliminate barrier search is novel and novel and well-supported by these foundations.}\splitnote{Hauswirth 2024
well-supported by these foundations.}\splitnote{Hauswirth 2024 (pp.1-3) (pp.1-3) shows optimization-based robust feedback controllers can serve as
shows optimization-based robust feedback controllers can serve as alternative verification method---suggests barrier certificates + reachability
alternative verification method---suggests barrier certificates + provide complementary guarantees for your stabilizing modes.}
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
% ----------------------------------------------------------------------------
\subsubsection{Expulsory 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 conservatively bounded region) rather than a well-defined entry set. The failure
may occur at any point during operation. Second, the dynamics include parametric may occur at any point during operation. Second, the dynamics include parametric
uncertainty representing failure modes: uncertainty representing failure modes:
%
\[ \[
\dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure} \dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure}
\] \]
%
where $\Theta_{failure}$ captures the range of possible degraded plant where $\Theta_{failure}$ captures the range of possible degraded plant
behaviors identified through failure mode and effects analysis (FMEA) or behaviors identified through failure mode and effects analysis (FMEA) or
traditional safety analysis. \addedprose{While tools such as SpaceEx handle traditional safety analysis.
nondeterministic inputs~\cite{frehse_spaceex_2011}, parametric plant
uncertainty requires conservative over-approximation of reachable sets
across the full parameter range.}
We verify expulsory modes using reachability analysis with parametric We verify expulsory modes using reachability analysis with parametric
uncertainty. The verification condition requires that for all parameter uncertainty. While tools such as SpaceEx handle nondeterministic
values within the uncertainty set, trajectories from the expanded entry inputs~\cite{frehse_spaceex_2011}, parametric plant uncertainty requires
region reach the safe shutdown state: 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}: \forall \theta \in \Theta_{failure}:
\text{Reach}(\mathcal{X}_{current}, f_\theta, [0,T]) \subseteq \text{Reach}(\mathcal{X}_{current}, f_\theta, [0,T]) \subseteq
\mathcal{X}_{shutdown} \mathcal{X}_{shutdown}
\] \]
%
This is more conservative than nominal reachability, accounting for the fact This is more conservative than nominal reachability, accounting for the fact
that we cannot know exactly which failure mode is active. 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 mode approach is sound for nuclear failures. Shows safety can be proven even
when controller deviates from nominal (pp.85-107, UCA 1 when controller deviates from nominal (pp.85-107, UCA 1
analysis).} 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} \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 platform are handled correctly. Direct industry collaboration also provides an
immediate pathway for technology transfer and alignment with practical immediate pathway for technology transfer and alignment with practical
deployment requirements. 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

4
6-broader-impacts/impacts.tex
View File

@ -9,7 +9,7 @@ transmission losses and eliminate emissions from hydrocarbon-based
alternatives. However, nuclear power economics at this scale demand careful alternatives. However, nuclear power economics at this scale demand careful
attention to operating costs. 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 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 projected to cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. In the
United States alone, datacenter electricity consumption could reach 560 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 in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related
costs represent approximately 23--30\% of the total levelized cost of costs represent approximately 23--30\% of the total levelized cost of
electricity, translating to \$11--15 billion annually for projected U.S. 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 This research directly addresses the multi-billion-dollar O\&M cost challenge
through high-assurance autonomous control. Current nuclear operations require through high-assurance autonomous control. Current nuclear operations require

2
8-schedule/schedule.tex
View File

@ -93,4 +93,4 @@ methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical
implementability on industrial hardware. This milestone delivers a conference implementability on industrial hardware. This milestone delivers a conference
paper submission to NPIC\&HMIT or CDC documenting hardware implementation and paper submission to NPIC\&HMIT or CDC documenting hardware implementation and
experimental validation. M6 (Month 24) completes the dissertation documenting 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.

13
main.tex
View File

@ -68,24 +68,25 @@
\pagenumbering{arabic} \pagenumbering{arabic}
\input{1-goals-and-outcomes/goals} \input{1-goals-and-outcomes/goals}
\newpage % \newpage
\input{2-state-of-the-art/state-of-art} \input{2-state-of-the-art/state-of-art}
\newpage % \newpage
\input{3-research-approach/approach} \input{3-research-approach/approach}
\newpage % \newpage
\input{4-metrics-of-success/metrics} \input{4-metrics-of-success/metrics}
\newpage % \newpage
\input{5-risks-and-contingencies/risks} \input{5-risks-and-contingencies/risks}
\newpage % \newpage
\input{6-broader-impacts/impacts} \input{6-broader-impacts/impacts}
\newpage % \newpage
\input{8-schedule/schedule} \input{8-schedule/schedule}
\newpage
\bibliographystyle{ieeetr} \bibliographystyle{ieeetr}
\bibliography{references} \bibliography{references}