Obsidian/Writing/ERLM/research-approach/v2.tex

\section{Research Approach}

This research will overcome the limitations of current practice to build 
high-assurance hybrid control systems for critical infrastructure. To achieve 
this goal, 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 using reachability analysis, barrier certificates, and
    assume-guarantee contracts

\end{enumerate}

The following sections discuss how these thrusts will be accomplished.

\subsection{Requirements: $(Procedures \wedge FRET) \rightarrow Temporal Specifications$}

% COMMENT: Consider strengthening this opening with specific examples or 
% statistics about nuclear plant automation levels vs other industries

The motivation behind this work stems from the fact that commercial nuclear 
power operations remain manually controlled by human operators, despite 
significant advances in control systems sophistication. The key insight is that 
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—a significant advantage for 
deployment in existing facilities. The most efficient path to accomplish this 
translation is through automated tools such as NASA's Formal Requirement
Elicitation Tool (FRET).

% COMMENT: Consider adding a brief example of a nuclear procedure that would 
% benefit from this approach

FRET employs a specialized requirements language similar to natural language
called FRETish. FRETish restricts requirements to easily understood components
while eliminating ambiguity. 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}

% COMMENT: The realizability discussion could be clearer - consider defining
% "realizable" more precisely upfront

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.

% COMMENT: This transition could be smoother - consider adding a sentence about
% how the temporal logic output connects to the next section

FRET also provides the capability to export requirements in temporal logic 
format. This export functionality enables progression to the next step of our 
approach: synthesizing discrete mode switching behavior from the formalized 
requirements.

\subsection{Discrete Synthesis: $(TemporalLogic \wedge ReactiveSynthesis) \rightarrow 
DiscreteAutomata$}

This section describes how the discrete component of the hybrid system will be 
constructed. The formal specifications created in FRET will be processed by 
reactive synthesis tools to generate mode switching components. These 
components effectively automate the human decision-making elements of reactor 
operation by implementing the logic typically specified in written procedures. 
By eliminating the human component from control decisions, we remove the 
possibility of human error and advance hybrid system autonomy.

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}. 
From the automaton graph, it becomes possible to fully describe the dynamics 
of the discrete system and develop intuitive understanding of system behavior. 
Once constructed, the automaton can be straightforwardly implemented using 
standard programming control flow constructs.

% COMMENT: The "correct by construction" concept is important - consider 
% expanding this explanation slightly

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

\subsection{$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) 
\rightarrow ContinuousModes$}

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. This section describes how we will develop continuous control 
modes, verify their correctness, and address the unique verification 
challenges of hybrid systems.

% COMMENT: This "glaring problem" phrasing is a bit dramatic - consider toning
% down while maintaining the technical point

First, we must address the limitation left unresolved in the previous section. 
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.

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}

% COMMENT: This paragraph has some word choice issues ("alieviate" -> 
% "alleviate") - fixed in revision

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. Current techniques struggle with this problem because dynamic 
discontinuities complicate verification. 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. 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 ensures each continuous controller is prepared for its 
possible input range, enabling subsequent reachability 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. 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 mode. Combining these three techniques will enable us to prove that 
continuous components of our hybrid controller satisfy discrete requirements.

% 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
% 6. Consider reorganizing the continuous modes classification earlier

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.