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

\section{Research Approach}

This research will overcome the limitations of current practice to build 
high-assurance hybrid control systems for critical infrastructure. To build these systems with formal correctness guarantees, we must accomplish 
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}

The motivation behind this work stems from the fact that commercial nuclear
power operations remain manually controlled by human operators, but procedures
performed by human operators are highly prescriptive and well-documented. This
suggests that human operators in nuclear power plants may not be entirely
necessary given today's available technology. Written procedures and
requirements in nuclear power are sufficiently detailed that we may be able to
translate them into logical formulae with minimal effort. If successful, this
approach would enable automation of existing procedures without requiring system
reengineering. To formalize these procedures, we will use temporal logic, which
captures system behaviors through temporal relations.

The most efficient path to accomplish this translation is through 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 that is 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 the \textit{realizability} of a system. 
Realizability analysis determines whether written requirements are complete by 
examining the six structural components. Complete requirements are those that 
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 that represent the physical 
equivalent of software bugs. Using FRET during autonomous controller 
development allows us to identify and resolve these errors systematically.

The second category of realizability issues involves undefined behaviors that 
are typically left to human judgment during control operations. This 
ambiguity is undesirable for high-assurance systems, since even well-trained 
humans remain prone to errors. By addressing these specification gaps in FRET 
during autonomous controller development, we can deliver controllers free from 
these vulnerabilities.

FRET provides the capability to export 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. There is no ambiguity on the control in this
scenario because all decisions are represented by discrete variables.
Formulating operating rules using this logic enforces a finite and correct way
of operating.



Reactive synthesis is an active research field in computer science 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 in size, where
each node represents 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 a series of nodes that are discrete
states, with traces indicating transitions between states. From the automaton
graph, it becomes possible to fully describe the dynamics of the discrete system
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 autom\cite
automatically while maximizing generated automata quality. Once constructed, the
automaton can be straightforwardly implemented using standard programming
control flow constructs. The graphical representation provided by the automaton
enables inspection and facilitates communication with controls programmers who
may not have 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, we can prove that the automaton—and
therefore our hybrid switching behavior—is \textit{correct by construction}.
Correctness of the switching controller is paramount to this work. 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 that extend
beyond written procedures. Autonomous control lacks this adaptive advantage.
Instead, we must ensure that autonomous controllers replacing human operators
will not make switching errors between continuous modes. By synthesizing
controllers from logical specifications with guaranteed correctness, we
eliminate 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 that represent 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.

Of note is the fact that the translation into this linear temporal logic does
something to create barriers between different control modes. Switching from one
mode to another mode becomes a discrete, boolean variable. \(RodsInserted\) or
\(HighTemp\) in the temporal specifications are booleans, but in the real system
can represent a physical feature in the state space. These features are where
continuous control modes end and begin, and their definition is critical in
defining which control mode is active at any given time. This information of
where in the state space these conditions represent will be preserved from the
original requirements by including them in the development of the continuous
control modes, but will not be considered as numeric values in the synthesis of
the discrete mode switching portion of the autonomous controller.

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. By decomposing continuous modes according to their required
behavior at transition points, we avoid solving trajectories through the entire
hybrid system. Instead, we can use local behavior information at transition
boundaries. To ensure continuous modes satisfy their requirements, we will
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 will use
reachability to define continuous state ranges at discrete transition boundaries
and verify that requirements are satisfied within continuous modes.
Assume-guarantee contracts will be employed 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 subsequent reachability analysis without
requiring global system analysis. Finally, we will use barrier certificates to
prove that mode transitions are satisfied. Barrier certificates ensure that
continuous modes on either side of a transition behave appropriately by ensuring
no system trajectories cross a given barrier. Control barrier functions provide
a method to 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 research
approach breaks down the autonomous controller design into smaller chunks. For
designers of future autonomous control systems, the barrier to entry is small,
while milestones in design are clear by the procedural nature of this research
plan. Second, the ability to measure design progress also enables the
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 component of this development plan
enables incremental refinement between control system layers. For example,
difficulty in developing a continuous mode may reflect a discrete automata that
is too restrictive, which in turn may result in refinement of system design
requirements. This synthesis between levels will promote 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, which is 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, providing assessment
of computational performance, real-time execution constraints, and communication
latency effects. By demonstrating autonomous startup control on this
representative platform, we 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. By translating existing nuclear procedures into temporal logic,
synthesizing provably correct discrete switching logic, and developing verified
continuous controllers, we create 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.

% COMMENTS FOR FUTURE REVISION:
% 1. Add concrete examples throughout (specific nuclear procedures, requirements)
% 2. Include a figure showing the overall workflow/methodology
% 3. Consider adding a subsection on validation approach
% 4. Strengthen the connections between subsections
% 5. Add discussion of limitations and assumptions