\section{Research Approach}

\textbf{Heilmeier Questions: What is new? Why will it succeed?}

This section answers these questions by presenting the complete technical approach for synthesizing provably correct hybrid controllers from operating procedures. 

\textbf{What is new:} Compositional verification that bridges discrete synthesis with continuous control. Three key innovations enable this integration: contract-based decomposition, mode classification, and procedure-driven structure. 

\textbf{Why it will succeed:} The approach leverages existing procedural structure, bounds computational complexity through mode-level verification, and validates against real industrial hardware through the Emerson collaboration.

% ============================================================================
% 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
% ----------------------------------------------------------------------------
Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources.

I bridge that gap by composing formal methods from computer science with control-theoretic verification. Reactor operations formalize as hybrid automata.

Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.

This methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode.

A high-assurance hybrid autonomous control system requires a mathematical description. This work draws on automata theory, temporal logic, and control theory to provide that description. A hybrid system is a dynamical system with both continuous and discrete states. This proposal addresses continuous autonomous hybrid systems specifically—systems with no external input where continuous states remain continuous when discrete states change. These continuous states represent physical quantities that remain Lipschitz continuous. This work follows the nomenclature from the Handbook on Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, 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}

A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.

\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Prior work has not integrated them into a systematic design methodology spanning procedures to verified implementation. 

Three innovations enable this integration:

\begin{enumerate}
\item \textbf{Contract-based decomposition:} This approach inverts the traditional structure. Instead of attempting global hybrid system verification, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems.
\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to match each mode type. This classification enables mode-local analysis with provable composition guarantees.
\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases. Leveraging this existing structure avoids imposing artificial abstractions, making the approach tractable for complex systems like nuclear reactor startup.
\end{enumerate>

\textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed.

\textbf{First, existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. I formalize existing structure—I do not impose artificial abstractions. Domain experts without formal methods training can adopt the approach.

\textbf{Second, bounded complexity:} Mode-level verification checks each mode against local contracts. This avoids attempting global hybrid system analysis. The decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.

\textbf{Third, industrial validation:} The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. My solutions address real deployment constraints, not just theoretical correctness.

These factors combine to demonstrate feasibility on production control systems with realistic reactor models—not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence.

\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,u)$};
    \node[dynamics] at (10,-1.4) {$\dot{x} = f_2(x,u)$};
    \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 
    (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, Specifications, and Discrete Controllers}

The previous subsection established the hybrid automaton formalism. This mathematical framework describes discrete modes, continuous dynamics, guards, and invariants. 

A critical question remains: where do these formal descriptions originate? This subsection answers by demonstrating that nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. 

The approach does not impose artificial abstractions. Instead, it constructs formal hybrid systems from existing operational knowledge, leveraging decades of domain expertise encoded in operating procedures.

Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years, managing labor needs and supply chains to optimize scheduled maintenance and downtime.

The tactical level controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems—continuous systems that maintain pressurizer level, core temperature, and reactivity through chemical shim. These systems directly impact the physical state of the plant.

The operational scope links these extremes. It represents the primary responsibility of human operators today. Operators implement tactical control sequences to achieve strategic objectives, bridging high-level goals with low-level execution. 

An example clarifies this three-level structure. Consider a strategic goal to perform refueling at a certain time. The tactical level currently maintains core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this objective.

This structure reveals why the operational and tactical levels fundamentally form a hybrid controller. The tactical level represents continuous plant evolution according to control input and control law. The operational level represents discrete state evolution determining which tactical control law applies. Together, these two levels form the complete hybrid system. This operational level becomes the target for autonomous control because it bridges strategic intent with tactical execution through discrete mode-switching decisions.


\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 explains why nuclear control requires human operators: the hybrid nature of this control system makes proving controller performance against strategic requirements difficult, and no unified infrastructure exists for building and verifying hybrid systems. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature, following prescriptive operating manuals where strict procedures govern what control to implement at any given time. These procedures provide the key to the operational control scope.

A HAHACS construction leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins. A HAHACS's intended behavior must be completely described before construction. Requirements define the behavior of any control system: statements about what
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 autonomous control system synthesis and verification. We can
build these requirements using temporal logic.

Temporal logic provides powerful semantics for building systems with complex
but deterministic behavior, extending classical propositional logic with
operators that express properties over time. Temporal logic relates discrete
control modes to one another and defines all HAHACS requirements. Boundary
conditions between discrete states determine guard conditions $\mathcal{G}$ and
specify their behavior. Continuous mode invariants similarly express as temporal
logic statements. These specifications form the basis of any proofs about a
HAHACS, constituting fundamental truth statements about designed system behavior.

Discrete mode transitions include predicates—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\%.''
This discrete abstraction is not imposed artificially—operating
procedures for nuclear systems already define go/no-go conditions as discrete
predicates. Design basis safety analysis determined these thresholds; decades of operational experience validated them. Our methodology assumes
this domain knowledge exists and provides a framework to formalize it. The approach proves feasible for nuclear applications because generations
of nuclear engineers already completed the hard
work of defining safe operating boundaries. 

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


I use FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language. It enables rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: the current nuclear workforce can adopt these tools without extensive formal methods training.

FRET's key feature is its ability to start with logically imprecise
statements and refine them consecutively into well-posed specifications. We
leverage this by directly importing operating procedures and design
requirements into FRET in natural language, then iteratively refining them into
specifications for a HAHACS. This approach provides two distinct benefits: first, it draws a direct link from design documentation to digital system
implementation; second, it clearly demonstrates where natural language documents
fall short. Human operators may still use these procedures, making any
room for interpretation a weakness requiring correction.

FRET has been successfully applied to spacecraft control systems, autonomous vehicle requirements, and medical device specifications. NASA used FRET for the Lunar Gateway project, formalizing flight software requirements that were previously specified only in natural language. The Defense Advanced Research Projects Agency (DARPA) employed FRET in the Assured Autonomy program to verify autonomous systems requirements. These applications demonstrate FRET's maturity for safety-critical domains. Nuclear control procedures present an ideal use case: they are already structured, detailed, and written to minimize ambiguity—precisely the characteristics that enable successful formalization.
%%% 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}

Operating procedures translate into temporal logic specifications using FRET—these specifications define what the system must do. But how do we implement those requirements? Reactive synthesis provides the answer by automatically constructing controllers guaranteed to satisfy temporal logic specifications.

Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. System requirements defined as temporal logic specifications enable reactive synthesis to build the discrete control system. Our systems fit this model: the current discrete state and status of guard conditions form the input, while the next discrete state forms the output.

Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ specifying desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller exists. Unrealizable specifications indicate conflicting or impossible requirements in
the original procedures—this realizability check catches errors before implementation. 

Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The resultant automaton is correct by construction. This eliminates human error at the implementation stage entirely. Human designers focus their effort where it belongs—on specifying system behavior, not implementing switching logic.

This shift carries two critical implications. First, complete traceability: the controller changes between modes for reasons that trace back through specifications to requirements. This establishes clear liability and justification for system behavior. Second, deterministic guarantees replace probabilistic human judgment. Human operators cannot eliminate error from discrete control decisions. Humans are intrinsically fallible. Temporal logics define system behavior. Deterministic algorithms synthesize the controller. Strategic decisions always follow operating procedures exactly—no exceptions, no deviations, no human factors.

The synthesized automaton translates directly to executable code through standard compilation techniques. Each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees by ensuring the implemented code is correct by construction—the automaton from which it derives was synthesized to satisfy the temporal logic specifications.

Reactive synthesis has proven successful in robotics, avionics, and industrial control. Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.

Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.

The discrete mode-switching logic now synthesizes from procedures. But what executes within each discrete mode? The next subsection addresses continuous control modes and their verification.

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

The previous subsection established that reactive synthesis produces a provably correct discrete controller. This controller is an automaton synthesized from operating procedures. It determines when to switch between modes.

Hybrid control, however, requires more than correct mode switching. The continuous dynamics executing within each discrete mode must also verify against requirements. Without this continuous verification, the discrete controller cannot guarantee correct system behavior.

This subsection describes the continuous control modes executing within each discrete state. It explains how they verify against requirements imposed by the discrete layer. Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory. Each type requires different verification tools matched to its distinct purpose. 

This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking confirms whether a given implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that design capability exists. The contribution lies in the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.

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

This partitioning of the
continuous state space among several discrete vector fields has traditionally
posed 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{MANYUS THESIS}.

I circumvent these issues by designing the hybrid system from the bottom up with verification in mind. The discrete transitions define each continuous control mode's input and output sets clearly \textit{a priori}.

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, 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. The continuous controller for mode
$q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.

Continuous controllers classify into three types based on their control objectives, each requiring distinct verification tools matched to its purpose. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. The following subsections detail each mode type and its verification approach, progressing from nominal operations (transitory and stabilizing modes) to off-nominal scenarios (expulsory modes).

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

Transitory modes—the first of three continuous controller types—execute transitions between operating conditions. Their purpose is to move the plant from one discrete operating condition to another: start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers.

The control objective for a transitory mode has a formal statement. 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}
\]
This requirement is straightforward: from any valid entry state, the trajectory must eventually reach the exit condition without ever leaving the safe region.

Reachability analysis provides the natural verification tool for transitory modes.
It 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_i, [0,T]) \subseteq \mathcal{X}_{safe} \land
\text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset
\]

The discrete controller defines clear boundaries in continuous state space. This makes the verification problem for each transitory mode well-posed. The possible initial conditions, target conditions, and safety envelope are all known before verification begins. The verification task then confirms 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, 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.

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

Transitory modes drive the system toward exit conditions. They answer the question: "can we reach the target?"

Stabilizing modes address a fundamentally different question: "will we stay within bounds?" These modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.

Reachability analysis answers "can the system reach a target?" Stabilizing modes instead ask "does the system stay within bounds?" Barrier certificates provide the appropriate verification tool for this question.
Barrier certificates analyze the dynamics of the system to determine whether
flux across a given boundary exists. They evaluate whether any trajectory leaves
a given boundary. This definition exactly matches what defines the validity of a
stabilizing continuous control mode.

Formally, 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 parallels Lyapunov functions for
stability: rather than computing trajectories explicitly, we seek 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.

The discrete controller design defines careful boundaries in continuous state space. Therefore, the barrier is known prior to designing the continuous controller. This eliminates the search for an appropriate barrier. It minimizes complication in validating stabilizing continuous control modes. The discrete specifications tell us what region must be invariant. The barrier certificate then 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. 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.

%%% 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 first two mode types handle nominal operations. Transitory modes move the plant between conditions. Stabilizing modes maintain the plant within regions. Both assume that plant dynamics match the design model. Both assume the plant behaves as expected.

Expulsory modes address a fundamentally different scenario. They handle situations where the plant deviates from expected behavior. This deviation may result from component failures, sensor degradation, or unanticipated disturbances. Here, robustness matters more than optimality.

Expulsory controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and controlled depressurization procedures.

Proving controller correctness through reachability and barrier certificates makes detecting physical failures straightforward. The controller cannot be incorrect for the nominal plant model. When an invariant is violated, the plant dynamics must have changed. The HAHACS identifies faults when continuous controllers violate discrete boundary conditions—a direct consequence of verified nominal control modes. Unexpected behavior implies off-nominal conditions.

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.

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.

%%% 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 complete methodology—procedure formalization, discrete synthesis, and continuous verification across three mode types—provides a theoretical framework for hybrid control synthesis. But theory alone does not demonstrate practical feasibility. Advancing from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5) requires validation on realistic systems using industrial-grade hardware.
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.

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

This section answered two critical Heilmeier questions.

\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations enable this integration. 

First, contract-based decomposition uses discrete synthesis to define verification contracts that bound continuous verification. This inverts traditional global analysis. Second, mode classification classifies continuous modes by control objective to select appropriate verification tools. This enables mode-local analysis with provable composition guarantees. Third, procedure-driven structure leverages existing procedural structure to avoid intractable state explosion.

Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. Compositional verification enables what global analysis cannot achieve.

\textbf{Why will this approach succeed?} Three factors ensure practical feasibility. 

First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes existing structure. It does not impose artificial abstractions. Second, mode-level verification bounds each verification problem locally. This avoids the state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. Solutions address real deployment constraints, not just theoretical correctness.

The methodology is now complete. It encompasses procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. 

Operational questions about executing this research plan remain. Section 4 addresses \textit{How will success be measured?} through Technology Readiness Level advancement. Section 5 addresses \textit{What could prevent success?} through risk analysis and contingency planning. Section 6 addresses \textit{Who cares? Why now? What difference will it make?} through economic and societal impact analysis.

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

