% GOAL PARAGRAPH
This research develops autonomous control systems that provide mathematical guarantees of safe and correct behavior.

% INTRODUCTORY PARAGRAPH Hook
Human operators control nuclear reactors today by following detailed written procedures and switching between control objectives as plant conditions change.
% Gap
Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs far exceed those of conventional plants, threatening their economic viability. Autonomous control offers a solution—managing complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.

% APPROACH PARAGRAPH Solution
This research unifies formal methods from computer science with control theory to produce hybrid control systems correct by construction.
% Rationale
Human operators already work this way: they use discrete logic to switch between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. Both are required for end-to-end correctness.
% Hypothesis and Technical Approach
Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications, structuring requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory—satisfy each discrete mode's requirements.

Continuous modes classify by control objective into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe, enabling local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
% Pay-off
This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It directly addresses the economic constraints that threaten small modular reactor viability.

% OUTCOMES PARAGRAPHS
This research, if successful, produces three concrete outcomes:
\begin{enumerate}
  % OUTCOME 1 Title
  \item \textit{Synthesize written procedures into verified control logic.} 
    % Strategy
    The methodology converts written operating procedures into formal specifications.
    Reactive synthesis tools then generate discrete control logic from these specifications.
    % Outcome
    Control engineers can generate mode-switching controllers directly from regulatory
    procedures with minimal formal methods expertise, reducing barriers to
    high-assurance control systems.

    % OUTCOME 2 Title
  \item \textit{Verify continuous control behavior across mode transitions.}
    % Strategy
    Reachability analysis verifies that continuous control modes satisfy discrete
    transition requirements. 
    % Outcome
    Engineers design continuous controllers using standard practices while
    maintaining formal correctness guarantees. Mode transitions occur safely and at
    the correct times—provably.

    % OUTCOME 3  Title
  \item \textit{Demonstrate autonomous reactor startup control with safety
    guarantees.}
    % Strategy
    This methodology demonstrates on a small modular reactor simulation using industry-standard control hardware.
    % Outcome
    Control engineers implement high-assurance autonomous controls on
    industrial platforms they already use, enabling autonomy without retraining
    costs or new equipment development.

\end{enumerate}