Thesis/3-research-approach/approach.tex

\section{Research Approach}

To build a high-assurance hybrid autonomous control system (HAHACS), we must
first establish a mathematical description of the system. This work draws on
automata theory, temporal logic, and control theory. A hybrid system is a
dynamical system that has both continuous and discrete states. The specific
type of system discussed in this proposal is a continuous autonomous hybrid
system. This means that the system does not have external input and that
continuous states do not change instantaneously when discrete states change.
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
  \item $\mathbf{f}: \mathcal{Q} \times \mathcal{X} \rightarrow
    \mathbb{R}^n$: vector fields defining the continuous dynamics for each
    discrete mode $q_i$
  \item $Init \subseteq \mathcal{Q} \times \mathcal{X}$: the set of initial
    states
  \item $\mathcal{G}$: guard conditions that define when discrete state
    transitions may occur
  \item $\delta: \mathcal{Q} \times \mathcal{G} \rightarrow \mathcal{Q}$:
    the discrete state transition function
  \item $\mathcal{R}$: reset maps that define any instantaneous changes to
    continuous state upon discrete transitions
  \item $Inv$: safety invariants on the continuous dynamics
\end{itemize}

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.\splitsuggest{Compositional verification claim
  needs citation. See assume-guarantee literature (Henzinger, Alur). None of the
  NEEDS\_REVIEWED papers directly prove tHANDBOOK ON HYBRID SYSTEMShis composition is sound for your
specific approach.} 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
control system is satisfied by its actual
implementation. In concrete terms, this means producing a
discrete automaton whose transitions are provably correct, continuous
controllers whose behavior is verified against transition requirements, and
formal evidence linking the two. This approach is tractable now because the
infrastructure for each component has matured. The novelty is not in the
individual pieces, but in the architecture that connects
them. By defining entry, exit, and safety conditions at the
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.

\begin{figure}
  \centering
  \begin{tikzpicture}[
    state/.style={
      circle, draw=black, thick, minimum size=2.2cm,
      fill=blue!10, align=center, font=\small
    },
    trans/.style={
      ->, thick, >=stealth
    },
    guard/.style={
      font=\scriptsize, align=center, fill=white, inner sep=2pt
    },
    dynamics/.style={
      font=\scriptsize\itshape, text=blue!70!black
    }
  ]
    % States
    \node[state] (q0) at (0,0) {$q_0$\\Cold\\Shutdown};
    \node[state] (q1) at (5,0) {$q_1$\\Heatup};
    \node[state] (q2) at (10,0) {$q_2$\\Power\\Operation};
    \node[state, fill=red!15] (q3) at (5,-3.5) {$q_3$\\SCRAM};

    % Normal transitions
    \draw[trans] (q0) -- node[guard, above]
      {$T_{avg} > T_{min}$} (q1);
    \draw[trans] (q1) -- node[guard, above]
      {$T_{avg} \in [T_{op} \pm \delta]$\\$P > P_{crit}$} (q2);

    % Fault transitions
    \draw[trans, red!70!black] (q1) -- node[guard, left,
      text=red!70!black] {$\neg Inv_1$} (q3);
    \draw[trans, red!70!black] (q2) to[bend left=20] node[guard,
      right, text=red!70!black] {$\neg Inv_2$} (q3);

    % Recovery transition
    \draw[trans, dashed] (q3) to[bend left=30] node[guard, below]
      {Manual reset} (q0);

    % Self-loops indicating staying in mode
    \draw[trans] (q2) to[loop right] node[guard, right] {$Inv_2$}
      (q2);

    % Dynamics labels below states
    \node[dynamics] at (0,-1.4) {$\dot{x} = f_0(x)$};
    \node[dynamics] at (6,-1.2) {$\dot{x} = f_1(x)$};
    \node[dynamics] at (10,-1.4) {$\dot{x} = f_2(x)$};
    \node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$};

  \end{tikzpicture}
  \caption{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.}
  \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
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
adjusting reactivity with a chemical shim.

The level of control linking these two extremes is the operational control
scope. Operational control is the primary responsibility of human operators
today. Operational control takes the current strategic objective and implements
tactical control objectives to drive the plant towards strategic goals. In this
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?


\begin{figure}
  \centering
  \begin{tikzpicture}[scale=0.8]
    % Pyramid layers
    \fill[blue!30!white] (0,4) -- (2,4) -- (1,5.) -- cycle;
    \fill[blue!20!white] (-1.5,2.5) -- (3.5,2.5) -- (2,4) -- (0,4)
      -- cycle;
    \fill[blue!10!white] (-3,1) -- (5,1) -- (3.5,2.5) -- (-1.5,2.5)
      -- cycle;

    % Labels inside pyramid
    \node[font=\small\bfseries] at (1,4.5) {Strategic};
    \node[font=\small\bfseries] at (1,3.1) {Operational};
    \node[font=\small\bfseries] at (1,1.6) {Tactical};

    % Descriptions to the right
    \node[anchor=west, font=\small, text width=8cm] at (5.5,4.6)
      {\textit{Long-term planning:} maintenance scheduling, capacity
      planning, economic dispatch};
    \node[anchor=west, font=\small, text width=8cm] at (5.5,3.1)
      {\textit{Discrete decisions:} startup/shutdown sequences, power
      level changes, mode transitions};
    \node[anchor=west, font=\small, text width=8cm] at (5.5,1.6)
      {\textit{Continuous control:} temperature regulation, pressure
      control, load following};

    % Bracket showing HAHACS scope (simple line with text)
    \draw[thick] (5.0,1.0) -- (-3.5,1) -- (-3.5,4) -- (2.0,4) --
      cycle;
    \node[font=\small, align=center, rotate=90] at (-4.2,2.5)
      {HAHACS scope};
  \end{tikzpicture}
  \caption{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.}
  \label{fig:strat_op_tact}
\end{figure}


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
stop-gap for safety. Humans have been used for this layer because their general
intelligence has been relied upon as a safe way to manage the hybrid nature of
this system---if a failure occured, it has been assumed a human operator can
figure out a solution to maintain plant performance and safety without
exhaustive knowledge of plant behavior. However, human factors research has
sought to minimize the need for general human reasoning by creating extremely
prescriptive operating manuals with strict procedures dictating what control to
implement at a given time. These operating manuals have minimized the role of
human operators today, are the key to the automating the operational control
scope.

The method of constructing a HAHACS in this proposal leverages two key
observations about current practice. First, the operational scope control is
effectively discrete control. Second, the rules for implementing this control
are described in operating procedures prior to their implementation. Instead of
implementing these procudures with a human controller, we rigorize the
instructions as a set of formal requirements. The behavior of any control system
originates in requirements: 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
aforementioned operating procedures. The challenge is formalizing these requirements with
sufficient precision that they can serve as the foundation for autonomous
control system synthesis and verification. We can build these requirements using
temporal logic.

Temporal logic is a powerful set of semantics for building systems with
complex but deterministic behavior. Temporal logic extends classical
propositional logic with operators that express properties over time. Using
temporal logic, we can make statements relating discrete control modes to one
another and define all the requirements of a HAHACS. The guard conditions
$\mathcal{G}$ are defined by determining boundary conditions between discrete
states and specifying their behavior, while continuous mode invariants can
also be expressed as temporal logic statements. These specifications form the
basis of any proofs about a HAHACS and constitute the fundamental truth
statements about what the behavior of the system is designed to be.

Discrete mode transitions include predicates that are Boolean functions over the
continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
\text{false}\}$. These predicates formalize conditions like ``coolant
temperature exceeds 315\textdegree{}C'' or ``pressurizer level is between 30\%
and 60\%.'' Critically, we do not impose this discrete abstraction artificially.
Operating procedures for nuclear systems already define go/no-go conditions as
discrete predicates, but do so in natural language. These thresholds come from
design basis safety analysis and have been validated over decades of operational
experience. Our methodology assumes this domain knowledge exists and provides a
framework to formalize it. This is why the approach is feasible for nuclear
applications specifically: the work of defining safe operating boundaries has
already been done by generations of nuclear engineers. The work of translating
these requirements from interpretable natural language to a formal requirement is
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'').%
\splitsuggest{CAUTION: Katis 2022 (Table 1, p.2) notes FRET realizability
checking does NOT support liveness properties. Your ``eventually reaches
operating temperature'' example may need alternative verification approach.}

To build these temporal logic statements, an intermediary tool called FRET is
planned to be used. FRET stands for Formal Requirements Elicitation Tool, and
was developed by NASA to build high-assurance timed systems. FRET is an
intermediate language between temporal logic and natural language that allows
for rigid definitions of temporal behavior while using a syntax accessible to
engineers without formal methods expertise\cite{katis_realizability_2022}. This
benefit is crucial for the feasibility of this methodology in industry. By
reducing the expert knowledge required to use these tools, their adoption with
the current workforce becomes easier.

A key feature of FRET is the ability to start with logically imprecise
statements and consecutively refine them into well-posed
specifications\cite{katis_realizability_2022, pressburger_using_2023}. We
can use this to our advantage by directly importing operating procedures and
design requirements into FRET in natural language, then iteratively refining
them into specifications for a HAHACS. This has two distinct benefits.
First, it allows us to draw a direct link from design documentation to
digital system implementation. Second, it clearly demonstrates where natural
language documents are insufficient. These procedures may still be used by
human operators, so any room for interpretation is a weakness that must be
addressed.

\dasinline{Maybe add more details about FRET case studies here. This would be
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
output is the next discrete state.

Reactive synthesis solves the following problem: given an LTL formula $\varphi$
that specifies 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 called \emph{realizable}. The synthesis algorithm
either produces a correct-by-construction controller or reports that no such
controller can exist. This realizability check is itself valuable: an
unrealizable specification indicates conflicting or impossible requirements in
the original procedures. The current implementation and one of the main uses of
FRET today is for exactly this purpose---multiple case studies have used FRET
for the refinement of unrealizable specifications into realizable systems
\cite{katis_realizability_2022, pressburger_using_2023}. 

The main advantage of reactive synthesis is that at no point in the production
of the discrete automaton is human engineering of the implementation required.
The resultant automaton is correct to the specification by construction. This
method of construction eliminates the possibility of human error at the
implementation stage entirely. The effort shifts entirely to specifying correct
behavior rather than implementing it. This has two critical implications. First,
every mode transition can be traced back through the specification to its
originating requirement, providing a clear liability and justification chain.
Second, by defining system behavior in temporal logic and synthesizing the
controller using deterministic algorithms, discrete control decisions become
provably consistent with operating procedures. 

(Talk about how one would go from a discrete automaton to actual
code)\splitsuggest{Consider citing Strix~\cite{meyer_strix_2018} as an
example reactive synthesis tool, even if you end up using a different one.
Also cite Katis conference version~\cite{katis_capture_2022} alongside the
report if you want both venues represented.}\splitnote{GR(1) fragment (Maoz \& Ringert 2015, pp.1-4) is tractable
LTL subset for synthesis: wins SYNTCOMP competitions (p.13). Luttenberger
2020 (Strix tool, pp.1-3) handles full LTL via parity games, achieving
4000+ state specs efficiently (p.5). Your nuclear procedures should fit
GR(1) since they're reactive (environment inputs = plant state, outputs =
mode transitions). This suggests synthesis will be practical for SmAHTR
scale.}

(Examples of reactive synthesis in the wild)\splitfix{Need to verify your
LTL specs fit GR(1) or full LTL needed---if full LTL required, computational
cost grows but Strix may handle it (confirm scalability claim with specific
spec size estimates for startup/shutdown procedures).}

\subsection{Continuous Control Modes}

The synthesis of the discrete operational controller is only half of an
autonomous controller. These control systems are hybrid, with both discrete and
continuous components. This section describes the continuous control modes that
execute within each discrete state, and how we verify that they satisfy the
requirements imposed by the discrete layer. It is important to clarify the scope
of this methodology with respect to continuous controller design. This work will
verify continuous controllers; it does not synthesize them. The distinction
parallels model checking in software verification: model checking does not tell
engineers how to write correct software, but it verifies whether a given
implementation satisfies its specification. Similarly, we assume that continuous
controllers can be designed using standard control theory techniques, and to
that end, are not prohibitive to create. Our contribution is a verification
framework that confirms 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
discrete state are themselves the guard conditions $\mathcal{G}$ that define
the boundaries for each continuous controller's allowed state-space region.
These continuous controllers all share a common state space, but each
individual continuous control mode operates within its own partition defined
by the discrete state $q_i$ and the associated guard conditions. This partitioning of
the continuous state space among several distinct vector fields has
traditionally been a difficult problem for validation and verification. The
discontinuity of the vector fields at discrete state interfaces makes
reachability analysis computationally expensive, and analytic solutions often
become intractable \cite{kapuria_using_2025, lang_formal_2021}.

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:
\begin{enumerate}
  \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq
    \mathcal{X}$, the set of possible initial states when entering this mode
  \item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq
    \mathcal{X}$, the target states that trigger transition to the next mode,
    or is the region in the state space a stabilizing mode remains within.
  \item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq
    \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.

\dasinline{
  \begin{itemize}
    \item Add figure showing the relationship between entry/exit/safety sets
    \item Mention assume guarantee compositional stuff and how that fits in here
  \end{itemize}
}

\subsubsection{Transitory Modes}

Transitory modes are continuous controllers designed to move the plant from one
discrete operating condition to another. Their purpose is to execute
transitions: starting from entry conditions, reach exit conditions, and maintain
safety invariants throughout. Examples include but are not limited to power
ramp-up sequences, cooldown procedures, and load-following maneuvers.

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,
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:
\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$:
\[
\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
conditions, and we know the safety envelope. The verification task is to
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
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

\subsubsection{Stabilizing Modes}

Stabilizing modes are continuous controllers with an objective of maintaining
a particular discrete state indefinitely. Rather than driving the system
toward an exit state, they keep the system within a safe
operating region. Examples include steady-state power operation, hot standby,
and load-following at constant power level. Reachability analysis for
stabilizing modes may not be a suitable approach to validation. Instead, we
plan to use barrier certificates. Barrier certificates analyze the dynamics
of the system to determine whether flux across a given boundary
exists~\cite{prajna_safety_2004}. In other words, they
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:
\[
\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
this condition holds, no trajectory starting inside $\mathcal{C}$ can ever
leave.

Because the design of the discrete controller defines careful boundaries in
continuous state space, the barrier \(\mathcal{C}\) is known prior to designing
the continuous controller. This eliminates the search for an appropriate barrier
and minimizes complication in validating stabilizing continuous control modes.
The discrete specifications tell us what region must be invariant; the barrier
certificate confirms that the candidate controller achieves this invariance.

Finding barrier certificates can be formulated as a sum-of-squares (SOS)
optimization problem for polynomial systems, or solved 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
% ----------------------------------------------------------------------------

\subsubsection{Expulsory Modes}

Expulsory modes are continuous controllers responsible for ensuring safety
when failures occur. They are designed for robustness rather than optimality.
The control objective is to drive 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.

We can detect that physical failures exist because our physical controllers have
been previously proven correct by reachability and barrier certificates. We know
our controller cannot be incorrect for the nominal plant model, so if an
invariant is violated, we know the plant dynamics have changed. The mathematical
formulation for expulsory mode verification differs from transitory modes in two
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%
\splitsuggest{GAP: None of the NEEDS\_REVIEWED papers directly address
reachability with parametric uncertainty for failure mode analysis. SpaceEx
handles nondeterministic inputs (Frehse 2011, p.4) but not parametric plant
uncertainty. Consider citing CORA (parametric reachability) or robust CBF
literature. This may require additional references beyond current
collection.}
behaviors identified through failure mode and effects analysis (FMEA) or
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:
\[
\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.

Traditional safety analysis techniques inform the construction of
$\Theta_{failure}$. Probabilistic risk assessment, FMEA, and design basis
accident analysis identify credible failure scenarios and their effects on
plant dynamics. The expulsory mode must handle the worst-case dynamics within
this envelope. This is where conservative controller design is appropriate as
safety margins will matter more than performance during emergency
shutdown.\splitnote{Parametric uncertainty approach validated: Kapuria 2025
(pp.82-120, Sections 5) verifies SmAHTR resiliency against UCAs with
uncertain dynamics (e.g., PHX secondary flow shutdown, resonating turbine
flow). Uses reachability + Z3 SMT solver (pp.23-24, Section 2.5 on
$\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).}\splitsuggest{Kapuria 2025 reveals practical challenge:
determining $\Theta_{\text{failure}}$ bounds is non-trivial. Recommend
documenting failure mode selection process (FMEA $\rightarrow$ parametric
bounds) to make expulsory mode design repeatable for other reactor
sequences.}

%%% 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}

The methodology described above must be validated on realistic systems using
industrial-grade hardware to demonstrate practical feasibility. This research
will leverage the University of Pittsburgh Cyber Energy Center's partnership
with Emerson to implement and test the HAHACS methodology on production
control equipment. Emerson's Ovation distributed control system is widely
deployed in power generation facilities, including nuclear plants. The
Ovation platform provides a realistic target for demonstrating that formally
synthesized controllers can execute on industrial hardware meeting timing and
reliability requirements. The discrete automaton produced by reactive
synthesis will be compiled to run on Ovation controllers, with verification
that the implemented behavior matches the synthesized specification exactly.

For the continuous dynamics, we will use a small modular reactor simulation. The
SmAHTR (Small modular Advanced High Temperature Reactor) model provides a
relevant testbed for startup and shutdown procedures. The ARCADE (Advanced
Reactor Control Architecture Development Environment) interface will establish
communication between the Emerson Ovation hardware and the reactor simulation,
enabling hardware-in-the-loop testing of the complete hybrid controller.

The Emerson collaboration strengthens this work in two ways. Access to
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.}\splitnote{Kapuria 2025 validates hybrid control on
SmAHTR: formal verification (d$\mathcal{L}$ + reachability, pp.37-70) proved
safe PHX maintenance scenario, then Simulink demo confirmed (pp.70-72). This
two-tier approach (formal proof + simulation validation) strengthens your
Emerson demo plan for credibility.}\splitsuggest{Consider documenting
integration points: ARCADE interface must guarantee formal synthesis outputs
map 1:1 to Ovation code. Pressburger 2023 (pp.22-23) notes manual
integration risks---automate code generation from formal specs to minimize
this gap.}

%%% 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