Obsidian/Writing/ERLM/3-research-approach/v5.tex

\section{Research Approach}

This research will overcome the limitations of current practice to build
high-assurance hybrid control systems for critical infrastructure. Building
these systems with formal correctness guarantees requires three main thrusts:

\begin{enumerate}
  \item Translate operating procedures and requirements into temporal logic
    formulae

  \item Create the discrete half of a hybrid controller using reactive synthesis

  \item Develop continuous controllers to operate between modes, and verify
    their correctness

\end{enumerate}

Commercial nuclear power operations remain manually controlled by human
operators, yet the procedures they follow are highly prescriptive and
well-documented. This suggests that human operators may not be entirely
necessary given current technology. Written procedures and requirements are
sufficiently detailed that they may be translatable into logical formulae with
minimal effort. If successful, this approach enables automation of existing
procedures without system reengineering. To formalize these procedures, we will
use temporal logic, which captures system behaviors through temporal relations.

The most efficient path for this translation is NASA's Formal Requirements
Elicitation Tool (FRET). FRET employs a specialized requirements language called
FRETish that restricts requirements to easily understood components while
eliminating ambiguity~\cite{katis_capture_2022}. FRETish bridges natural language
and mathematical specifications through a structured English-like syntax
automatically translatable to temporal logic.

FRET enforces this structure by requiring all requirements to contain six
components: %CITE FRET MANUAL

\begin{enumerate}
  \item Scope: \textit{What modes does this requirement apply to?}
  \item Condition: \textit{Scope plus additional specificity}
  \item Component: \textit{What system element does this requirement affect?}
  \item Shall
  \item Timing: \textit{When does the response occur?}
  \item Response: \textit{What action should be taken?}
\end{enumerate}

FRET provides functionality to check system \textit{realizability}. Realizability
analysis determines whether written requirements are complete by examining the
six structural components. Complete requirements neither conflict with one
another nor leave any behavior undefined. Systems that are not realizable from
their procedure definitions and design requirements present problems beyond
autonomous control implementation. Such systems contain behavioral
inconsistencies---the physical equivalent of software bugs. Using FRET during
autonomous controller development allows systematic identification and
resolution of these errors.

The second category of realizability issues involves undefined behaviors
typically left to human judgment during operations. This ambiguity is
undesirable for high-assurance systems, since even well-trained humans remain
prone to errors. Addressing these specification gaps in FRET during development
yields controllers free from these vulnerabilities.

FRET exports requirements in temporal logic format compatible with reactive
synthesis tools. Linear Temporal Logic (LTL) builds upon modal logic's
foundational operators for necessity ($\Box$, ``box'') and possibility
($\Diamond$, ``diamond''), extending them to reason about temporal
behavior~\cite{baier_principles_2008}. The box operator $\Box$ expresses that a
property holds at all future times (necessarily always), while the diamond
operator $\Diamond$ expresses that a property holds at some future time
(possibly eventually). These are complemented by the next operator ($X$) for the
immediate successor state and the until operator ($U$) for expressing
persistence conditions.

Consider a nuclear reactor SCRAM requirement expressed in natural language:
\textit{``If a high temperature alarm triggers, control rods must immediately
insert and remain inserted until operator reset.''} This plain language
requirement can be translated into a rigorous logical specification:

\begin{equation}
  \Box(HighTemp \rightarrow X(RodsInserted \wedge (\neg
  RodsWithdrawn\ U\ OperatorReset)))
\end{equation}

This specification precisely captures the temporal relationship between the
alarm condition, the required response, and the persistence requirement. The
necessity operator $\Box$ ensures this safety property holds throughout all
possible future system executions, while the next operator $X$ enforces
immediate response. The until operator $U$ maintains the state constraint until
the reset condition occurs. No ambiguity exists in this scenario because all
decisions are represented by discrete variables. Formulating operating rules in
this logic enforces finite, correct operation.

Reactive synthesis is an active research field focused on generating discrete
controllers from temporal logic specifications. The term ``reactive'' indicates
that the system responds to environmental inputs to produce control outputs.
These synthesized systems are finite, with each node representing a unique
discrete state. The connections between nodes, called \textit{state
transitions}, specify the conditions under which the discrete controller moves
from state to state. This complete mapping of possible states and transitions
constitutes a \textit{discrete automaton}. Discrete automata can be represented
graphically as nodes (discrete states) with edges indicating transitions between
them. From the automaton graph, one can fully describe discrete system dynamics
and develop intuitive understanding of system behavior. Hybrid systems naturally
exhibit discrete behavior amenable to formal analysis through these finite state
representations.

We will employ state-of-the-art reactive synthesis tools, particularly Strix,
which has demonstrated superior performance in the Reactive Synthesis
Competition (SYNTCOMP) through efficient parity game solving
algorithms~\cite{meyer_strix_2018,jacobs_reactive_2024}. Strix translates linear
temporal logic specifications into deterministic automata automatically while
maximizing generated automata quality. Once constructed, the automaton can be
implemented using standard programming control flow constructs. The graphical
representation enables inspection and facilitates communication with controls
programmers who lack formal methods expertise.

We will use discrete automata to represent the switching behavior of our hybrid
system. This approach yields an important theoretical guarantee: because the
discrete automaton is synthesized entirely through automated tools from design
requirements and operating procedures, the automaton---and therefore our hybrid
switching behavior---is \textit{correct by construction}. Correctness of the
switching controller is paramount. Mode switching represents the primary
responsibility of human operators in control rooms today. Human operators
possess the advantage of real-time judgment: when mistakes occur, they can
correct them dynamically with capabilities extending beyond written procedures.
Autonomous control lacks this adaptive advantage. Instead, autonomous
controllers replacing human operators must not make switching errors between
continuous modes. Synthesizing controllers from logical specifications with
guaranteed correctness eliminates the possibility of switching errors.

While discrete system components will be synthesized with correctness
guarantees, they represent only half of the complete system. Autonomous
controllers like those we are developing exhibit continuous dynamics within
discrete states. These systems, called hybrid systems, combine continuous
dynamics (flows) with discrete transitions (jumps). These dynamics can be
formally expressed as~\cite{branicky_multiple_1998}:

\begin{equation}
\dot{x}(t) = f(x(t),q(t),u(t))
\end{equation}

\begin{equation}
q(k+1) = \nu(x(k),q(k),u(k))
\end{equation}

Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs
discrete transitions. The continuous states $x$, discrete state $q$, and
control input $u$ interact to produce hybrid behavior. The discrete state $q$
defines which continuous dynamics mode is currently active. Our focus centers
on continuous autonomous hybrid systems, where continuous states remain
unchanged during jumps---a property naturally exhibited by physical systems. For
example, a nuclear reactor switching from warm-up to load-following control
cannot instantaneously change its temperature or control rod position, but can
instantaneously change control laws.

The approach described for producing discrete automata yields physics-agnostic
specifications representing only half of a complete hybrid autonomous
controller. These automata alone cannot define the full behavior of the control
systems we aim to construct. The continuous modes will be developed after
discrete automaton construction, leveraging the automaton structure and
transitions to design multiple smaller, specialized continuous controllers.

Notably, translation into linear temporal logic creates barriers between
different control modes. Switching from one mode to another becomes a discrete
boolean variable. \(RodsInserted\) or \(HighTemp\) in the temporal
specifications are booleans, but in the real system they represent physical
features in the state space. These features mark where continuous control modes
end and begin; their definition is critical for determining which control mode
is active at any given time. Information about where in the state space these
conditions exist will be preserved from the original requirements and included
in continuous control mode development, but will not appear as numeric values in
discrete mode switching synthesis.

The discrete automaton transitions are key to the supervisory behavior of the
autonomous controller. These transitions mark decision points for switching
between continuous control modes and define their strategic objectives. We
will classify three types of high-level continuous controller objectives based
on discrete mode transitions:

\begin{enumerate}
  \item \textbf{Stabilizing:} A stabilizing control mode has one primary
    objective: maintaining the hybrid system within its current discrete mode.
    This corresponds to steady-state normal operating modes, such as a
    full-power load-following controller in a nuclear power plant. Stabilizing
    modes can be identified from discrete automata as nodes with only incoming
    transitions.

  \item \textbf{Transitory:} A transitory control mode has the primary goal of
    transitioning the hybrid system from one discrete state to another. In
    nuclear applications, this might represent a controlled warm-up procedure.
    Transitory modes ultimately drive the system toward a stabilizing
    steady-state mode. These modes may have secondary objectives within a
    discrete state, such as maintaining specific temperature ramp rates before
    reaching full-power operation.

  \item \textbf{Expulsory:} An expulsory mode is a specialized transitory mode
    with additional safety constraints. Expulsory modes ensure the system is
    directed to a safe stabilizing mode during failure conditions. For example,
    if a transitory mode fails to achieve its intended transition, the
    expulsory mode activates to immediately and irreversibly guide the system
    toward a globally safe state. A reactor SCRAM exemplifies an expulsory
    continuous mode: when initiated, it must reliably terminate the nuclear
    reaction and direct the reactor toward stabilizing decay heat removal.

\end{enumerate}

Building continuous modes after constructing discrete automata enables local
controller design focused on satisfying discrete transitions. The primary
challenge in hybrid system verification is ensuring global stability across
transitions~\cite{branicky_multiple_1998}. Current techniques struggle with this
problem because dynamic discontinuities complicate
verification~\cite{bansal_hamilton-jacobi_2017,guernic_reachability_2009}. This
work alleviates these problems by designing continuous controllers specifically
with transitions in mind. Decomposing continuous modes according to their
required behavior at transition points avoids solving trajectories through the
entire hybrid system. Instead, local behavior information at transition
boundaries suffices. To ensure continuous modes satisfy their requirements, we
employ three main techniques: reachability analysis, assume-guarantee contracts,
and barrier certificates.

Reachability analysis computes the reachable set of states for a given input
set. While trivial for linear continuous systems, recent advances have extended
reachability to complex nonlinear
systems~\cite{frehse_spaceex_2011,mitchell_time-dependent_2005}. We use
reachability to define continuous state ranges at discrete transition boundaries
and verify that requirements are satisfied within continuous modes.
Assume-guarantee contracts apply when continuous state boundaries are not
explicitly defined. For any given mode, the input range for reachability
analysis is defined by the output ranges of discrete modes that transition to
it. This compositional approach ensures each continuous controller is prepared
for its possible input range, enabling reachability analysis without global
system analysis. Finally, barrier certificates prove that mode transitions are
satisfied. Barrier certificates ensure that continuous modes on either side of a
transition behave appropriately by preventing system trajectories from crossing
a given barrier. Control barrier functions certify safety by establishing
differential inequality conditions that guarantee forward invariance of safe
sets~\cite{prajna_safety_2004}. For example, a barrier certificate can guarantee
that a transitory mode transferring control to a stabilizing mode will always
move away from the transition boundary, rather than destabilizing the target
stabilizing mode.

This compositional approach has several advantages. First, this approach breaks
down autonomous controller design into smaller pieces. For designers of future
autonomous control systems, the barrier to entry is low, and design milestones
are clear due to the procedural nature of this research plan. Second, measurable
design progress also enables measurement of regulatory adherence. Each step in
this development procedure generates an artifact that can be independently
evaluated as proof of safety and performance. Finally, the compositional nature
of this development plan enables incremental refinement between control system
layers. For example, difficulty developing a continuous mode may reflect a
discrete automaton that is too restrictive, prompting refinement of system
design requirements. This synthesis between levels promotes broader
understanding of the autonomous controller.

To demonstrate this methodology, we will develop an autonomous startup
controller for a Small Modular Advanced High Temperature Reactor (SmAHTR). We
have already developed a high-fidelity SmAHTR model in Simulink that captures
the thermal-hydraulic and neutron kinetics behavior essential for verifying
continuous controller performance under realistic plant dynamics. The
synthesized hybrid controller will be implemented on an Emerson Ovation control
system platform, representative of industry-standard control hardware deployed
in modern nuclear facilities. The Advanced Reactor Cyber Analysis and
Development Environment (ARCADE) suite will serve as the integration layer,
managing real-time communication between the Simulink simulation and the Ovation
controller. This hardware-in-the-loop configuration enables validation of the
controller implementation on actual industrial control equipment interfacing
with a realistic reactor simulation, assessing computational performance,
real-time execution constraints, and communication latency effects.
Demonstrating autonomous startup control on this representative platform will
establish both the theoretical validity and practical feasibility of the
synthesis methodology for deployment in actual small modular reactor systems.

This unified approach addresses a fundamental gap in hybrid system design by
bridging formal methods and control theory through a systematic, tool-supported
methodology. Translating existing nuclear procedures into temporal logic,
synthesizing provably correct discrete switching logic, and developing verified
continuous controllers creates a complete framework for autonomous hybrid
control with mathematical guarantees. The result is an autonomous controller
that not only replicates human operator decision-making but does so with formal
assurance that switching logic is correct by construction and continuous
behavior satisfies safety requirements. This methodology transforms nuclear
reactor control from a manually intensive operation requiring constant human
oversight into a fully autonomous system with higher reliability than
human-operated alternatives. More broadly, this approach establishes a
replicable framework for developing high-assurance autonomous controllers in any
domain where operating procedures are well-documented and safety is paramount.