Thesis/3-research-approach/v3.tex

\section{Research Approach}

% ============================================================================
% STRUCTURE (maps to Thesis.RA tasks):
%   1. Introduction + Hybrid Systems Definition (Task 34)
%   2. System Requirements and Specifications (Task 35)
%   3. Discrete Controller Synthesis (Task 36)
%   4. Continuous Controllers Overview (Task 37)
%      4.1 Transitory Modes (Task 38)
%      4.2 Stabilizing Modes (Task 39)
%      4.3 Expulsory Modes (Task 40)
%   5. Industrial Implementation (Task 41)
% ============================================================================

% ----------------------------------------------------------------------------
% 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
% ----------------------------------------------------------------------------

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. The nomenclature across
these fields is far from homogeneous, and the reviewer of this proposal is not
expected to be an expert in all of them simultaneously. To present the research
ideas as clearly as possible, the following definitions are provided.

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

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.

\textcolor{blue}{Previous approaches to autonomous control have verified
discrete switching logic or continuous control behavior, but not both
simultaneously. Validation of continuous controllers today consists of
extensive simulation trials. Discrete switching logic for routine operation
has been driven by human operators, whose evaluation includes simulated
control room testing and human factors research. Neither method, despite
being extremely resource intensive, provides rigorous guarantees of control
system behavior. HAHACS bridges this gap by composing formal methods from
computer science with control-theoretic verification, formalizing reactor
operations using the framework of hybrid automata.}

\textcolor{blue}{The challenge of hybrid system verification lies in the
interaction between discrete and continuous dynamics. Discrete transitions
change the governing 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.}

\textcolor{blue}{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 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.}

\textcolor{blue}{This approach is tractable now because the infrastructure for each component
has matured. Reactive synthesis from temporal logic specifications has
progressed from theoretical results to practical tools; solvers like Strix
can synthesize controllers from LTL specifications in seconds. Reachability
analysis and barrier certificates for continuous systems have decades of
theoretical foundation and modern computational tools. 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}[htbp]
  \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 (4,0) {$q_1$\\Heatup};
    \node[state] (q2) at (8,0) {$q_2$\\Power\\Operation};
    \node[state, fill=red!15] (q3) at (4,-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 (4,-1.4) {$\dot{x} = f_1(x,u)$};
    \node[dynamics] at (8,-1.4) {$\dot{x} = f_2(x,u)$};
    \node[dynamics] at (4,-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}

%%% NOTES (Section 1):
% - May want to clarify the "no external input" claim with a footnote about
%   strategic inputs (e.g., remote start/stop commands)
% - The reset map R is often identity for physical systems; clarify if needed

% ----------------------------------------------------------------------------
% 2. SYSTEM REQUIREMENTS AND SPECIFICATIONS
% ----------------------------------------------------------------------------

\subsection{System Requirements and Specifications}

\textcolor{blue}{Before constructing a HAHACS, we must completely describe its
intended behavior. 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 operating
procedures. The challenge is formalizing these requirements with sufficient
precision that they can serve as the foundation for automated controller
synthesis and verification.}

Autonomous control systems are fundamentally different from automatic control
systems. The difference lies in the level at which they operate. Automatic
control systems are purely operational systems that maintain setpoints or track
references. Autonomous control systems make decisions about which operational
objectives to pursue.

\begin{figure}[htbp]
  \centering
  \begin{tikzpicture}[scale=0.8]
    % Pyramid layers
    \fill[blue!60!black] (0,4) -- (2,4) -- (1,5.5) -- cycle;
    \fill[blue!30!white] (-1.5,2.5) -- (3.5,2.5) -- (2,4) -- (0,4) -- cycle;
    \fill[blue!15!white] (-3,1) -- (5,1) -- (3.5,2.5) -- (-1.5,2.5) -- cycle;
    
    % Labels inside pyramid
    \node[font=\small\bfseries, white] 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=6cm] at (5.5,4.5) 
      {\textit{Long-term planning:} maintenance scheduling, capacity planning, economic dispatch};
    \node[anchor=west, font=\small, text width=6cm] at (5.5,3.1) 
      {\textit{Discrete decisions:} startup/shutdown sequences, power level changes, mode transitions};
    \node[anchor=west, font=\small, text width=6cm] at (5.5,1.6) 
      {\textit{Continuous control:} temperature regulation, pressure control, load following};
    
    % Bracket showing HAHACS scope (simple line with text)
    \draw[thick] (-3.3,1) -- (-3.5,1) -- (-3.5,4) -- (-3.3,4);
    \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}

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 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 objective. Thus, the combination of the operational and
tactical levels fundamentally forms a hybrid controller. The tactical level is
the continuous evolution of the plant according to the control input and control
law, while the operational level is a discrete state evolution that determines
which tactical control law to apply.

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 that a controller will perform according to
strategic requirements, as unified infrastructure for building and verifying
hybrid systems does not currently exist. 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. But these operators use prescriptive operating
manuals to perform their control with strict procedures on what control to
implement at a given time. These procedures are the key to 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 prior to their implementation in operating procedures. We can
exploit these facts by formalizing the rules for transitioning between discrete
states using temporal logic.

\textcolor{blue}{The discrete predicates that trigger mode transitions 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°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. 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 hard work of defining
safe operating boundaries has already been done by generations of nuclear
engineers. We are formalizing existing practice, not inventing new
abstractions.}

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.

\textcolor{blue}{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'').}

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

%%% NOTES (Section 2):
% - Add concrete FRET example showing requirement → FRETish → LTL
% - Discuss hysteresis and how to prevent mode chattering near boundaries
% - Address sensor noise and measurement uncertainty in threshold definitions
% - Consider numerical precision issues when creating discrete automata

% ----------------------------------------------------------------------------
% 3. DISCRETE CONTROLLER SYNTHESIS
% ----------------------------------------------------------------------------

\subsection{Discrete Controller Synthesis}

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. 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. The output of a reactive synthesis algorithm is a discrete automaton.

\textcolor{blue}{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 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 by construction. This method of construction
eliminates the possibility of human error at the implementation stage entirely.
Instead, the effort on the human designer is directed at the specification of
system behavior itself.

This has two critical implications. First, it makes the creation of the
controller tractable. The reasons the controller changes between modes can be
traced back to the specification and thus to any requirements, which provides a
trace for liability and justification of system behavior. Second, discrete
control decisions made by humans are reliant on the human operator operating
correctly. Humans are intrinsically probabilistic creatures who cannot eliminate
human error. By defining the behavior of this system using temporal logics and
synthesizing the controller using deterministic algorithms, we are assured that
strategic decisions will always be made according to operating procedures.

\textcolor{blue}{FRET can export specifications directly to formats compatible
with reactive synthesis solvers such as Strix, a state-of-the-art LTL
synthesis tool. The synthesis pipeline proceeds as follows:
\begin{enumerate}
  \item Operating procedures are formalized in FRET's structured English
  \item FRET translates requirements to past-time or future-time LTL
  \item Realizability analysis checks for specification conflicts
  \item If realizable, synthesis produces a Mealy machine implementing the
    discrete controller
  \item The Mealy machine is compiled to executable code for the target
    platform
\end{enumerate}
This pipeline provides complete traceability from natural language procedures
to verified implementation, with each step producing artifacts that can be
independently reviewed and validated.}

%%% NOTES (Section 3):
% - Mention computational complexity of synthesis (doubly exponential worst case)
% - Discuss how specification structure affects synthesis tractability
% - Reference GR(1) fragment as a tractable subset commonly used in practice
% - May want to include an example automaton figure

% ----------------------------------------------------------------------------
% 4. CONTINUOUS CONTROLLERS
% ----------------------------------------------------------------------------

\subsection{Continuous Controllers}

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.

\textcolor{blue}{It is important to clarify the scope of this methodology with
respect to continuous controller design. This work verifies 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. 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. 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
guards. This partitioning of the continuous state space among several discrete
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.

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}$. Whenever we
create guard conditions from our design requirements, we are effectively
creating subsets $\mathcal{X}_{entry,i}$ and $\mathcal{X}_{exit,i}$ for each
discrete mode $q_i$. These subsets define when state transitions occur between
discrete modes. More importantly, when building continuous control modes, they
become control objectives.

\textcolor{blue}{Mathematically, each discrete mode $q_i$ 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
  \item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq \mathcal{X}$,
    the envelope of safe states during operation in this mode
\end{enumerate}
These sets come directly from the discrete controller synthesis and define
precise objectives for continuous control. The continuous controller for mode
$q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.}

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.

%%% NOTES (Section 4):
% - Add figure showing the relationship between entry/exit/safety sets
% - Discuss how standard control techniques (LQR, MPC, PID) fit into this framework
% - Mention assume-guarantee reasoning for compositional verification

% ----------------------------------------------------------------------------
% 4.1 TRANSITORY MODES
% ----------------------------------------------------------------------------

\subsubsection{Transitory Modes}

\textcolor{blue}{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, reaching exit conditions,
while maintaining safety throughout. Examples include power ramp-up sequences,
cooldown procedures, and load-following maneuvers.}

\textcolor{blue}{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, u(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.}

\textcolor{blue}{Verification of transitory modes uses reachability analysis.
Reachability analysis computes the set of all states reachable from a given
initial set under the system dynamics. 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, [0,T]) \subseteq \mathcal{X}_{safe} \land
\text{Reach}(\mathcal{X}_{entry}, f, [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.

\textcolor{blue}{Several tools exist for computing reachable sets of hybrid
systems, including CORA, Flow*, SpaceEx, 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 through the
Emerson partnership.}

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

% ----------------------------------------------------------------------------
% 4.2 STABILIZING MODES
% ----------------------------------------------------------------------------

\subsubsection{Stabilizing Modes}

\textcolor{blue}{Stabilizing modes are continuous controllers with an objective
of maintaining a particular discrete state indefinitely. Rather than driving
the system toward an exit condition, 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 the most prudent approach
to validation. Instead, barrier certificates must be used. Barrier certificates
analyze the dynamics of the system to determine whether flux across a given
boundary exists. They evaluate whether any trajectory leaves a given boundary.
This definition is exactly what defines the validity of a stabilizing continuous
control mode.

\textcolor{blue}{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: 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
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 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.

\textcolor{blue}{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. 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.}

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

The validation of transitory and stabilizing modes hinges on an assumption of
correct plant models. In the case of a mechanical failure, the model will almost
certainly be invalidated. For this reason, we must also build safe shutdown
modes, since a human will not be in the loop to handle failures.

\textcolor{blue}{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 HAHACS can
identify that a fault occurred because a discrete boundary condition was
violated by the continuous physical controller. This is a direct consequence of
having verified the nominal continuous control modes: unexpected behavior
implies off-nominal conditions.

\textcolor{blue}{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
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.

\textcolor{blue}{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:
safety margins matter more than performance during emergency shutdown.}

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

\textcolor{blue}{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.}

\textcolor{blue}{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.}

\textcolor{blue}{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.}

\textcolor{blue}{The demonstration will proceed through stages aligned with
Technology Readiness Levels:
\begin{enumerate}
  \item \textbf{TRL 3:} Individual components validated in isolation (synthesized
    automaton, verified continuous modes)
  \item \textbf{TRL 4:} Integrated hybrid controller executing complete sequences
    in pure simulation
  \item \textbf{TRL 5:} Hardware-in-the-loop testing with Ovation executing the
    discrete controller and simulation providing plant response
\end{enumerate}
Success at TRL 5 demonstrates that the methodology produces deployable
controllers, not merely theoretical constructs.}

Working with Emerson on such an implementation is an incredible advantage for
the success and impact of this work. We will directly address the gap of
verification and validation methods for these systems and industry adoption by
forming a two-way exchange of knowledge between the laboratory and commercial
environments. This work stands to be successful with Emerson implementation
because we will have excess to system experts at Emerson to help with the fine
details of using the Ovation system. At the same time, we will have the benefit
of transferring technology directly to industry with a direct collaboration in
this research, while getting an excellent perspective of how our research
outcomes can align best with customer needs.

%%% NOTES (Section 5):
% - Get specific details on ARCADE interface from Emerson collaboration
% - Mention what startup sequence will be demonstrated (cold shutdown →
%   criticality → low power?)
% - Discuss how off-nominal scenarios will be tested (sensor failures,
%   simulated component degradation)
% - Reference Westinghouse relationship if relevant