\section{Goals and Outcomes}

% GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous
hybrid control systems with mathematical guarantees of safe and correct
behavior.

% INTRODUCTORY PARAGRAPH Hook
Nuclear power plants require the highest levels of control system reliability,
where failures can result in significant economic losses, service interruptions,
or radiological release. 
% Known information
Currently, nuclear plant operations rely on extensively trained human operators
who follow detailed written procedures and strict regulatory requirements to
manage reactor control. These operators make critical decisions about when to
switch between different control modes— such as transitioning from startup
heating to power operation—based on their interpretation of plant conditions and
procedural guidance. 
% Gap
However, this reliance on human operators prevents the introduction of
autonomous control capabilities and creates a fundamental economic challenge for
next-generation reactor designs. Emerging technologies like small modular
reactors face significantly higher per-megawatt staffing costs than conventional
plants, threatening their economic viability. 
% Critical Need
What is needed is a way to create autonomous control systems that can safely
manage complex operational sequences with the same level of assurance as
human-operated systems, but without requiring constant human supervision.

% APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods from computer science with
control theory to build hybrid control systems that are correct by construction. 
% Rationale
Hybrid systems use discrete logic to switch between continuous control modes,
similar to how operators change control strategies. Existing formal methods can
generate provably correct switching logic from written requirements, but they
cannot handle the continuous dynamics that occur during transitions between
modes. Meanwhile, traditional control theory can verify continuous behavior but
lacks tools for proving correctness of discrete switching decisions. 
% Hypothesis
By synthesizing discrete mode transitions directly from written operating
procedures and verifying continuous behavior between transitions, we can create
hybrid control systems with end-to-end correctness guarantees. If we can
formalize existing procedures into logical specifications and verify that
continuous dynamics satisfy transition requirements, then we can build
autonomous controllers that are provably free from design defects. 
% Pay-off
This approach will enable autonomous control in nuclear power plants while
maintaining the high safety standards required by the industry. 
% Qualifications
This work is conducted within the University of Pittsburgh Cyber Energy Center,
which provides access to industry collaboration and Emerson control hardware,
ensuring that solutions developed are aligned with practical implementation
requirements.

% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:

\begin{enumerate}

  % OUTCOME 1 Title
  \item \textbf{Translate written procedures into verified control logic.} 
    % Strategy
    We will develop a methodology for converting existing written operating
    procedures into formal specifications that can be automatically synthesized
    into discrete control logic. This process will use structured intermediate
    representations to bridge natural language procedures and mathematical
    logic. 
    % Outcome
    Control system engineers will be able to generate verified mode-switching
    controllers directly from regulatory procedures without requiring expertise
    in formal methods, reducing the barrier to creating high-assurance control
    systems.

    % OUTCOME 2 Title
  \item \textbf{Verify continuous control behavior across mode transitions.} 
    % Strategy
    We will establish methods for analyzing continuous control modes to ensure
    they satisfy the discrete transition requirements. Using a combination of
    classical control theory for linear systems and reachability analysis for
    nonlinear dynamics, we will verify that each continuous mode can safely
    reach its intended transitions. 
    % Outcome
    Engineers will be able to design continuous controllers using standard
    practices while iterating to ensure broader system correctness, proving that
    mode transitions occur safely and at the right times.

    % OUTCOME 3  Title
  \item \textbf{Demonstrate autonomous reactor startup control with safety
    guarantees.} 
    % Strategy
    We will apply this methodology to develop an autonomous controller for
    nuclear reactor startup procedures, implementing it on a small modular
    reactor simulation using industry-standard control hardware. This
    demonstration will prove correctness across multiple coordinated control
    modes from cold shutdown through criticality to power operation. 
    % Outcome
    We will provide evidence that autonomous hybrid control can be realized in
    the nuclear industry with current control equipment, establishing a path
    toward reducing operator staffing requirements while maintaining safety.

\end{enumerate}

% IMPACT PARAGRAPH Innovation
The innovation in this work is the unification of discrete synthesis and
continuous verification to enable end-to-end correctness guarantees for hybrid
systems. 
% Outcome Impact
If successful, control engineers will be able to create autonomous controllers
from existing procedures with mathematical proof of correct behavior, making
high-assurance autonomous control practical for safety-critical applications. 
% Impact/Pay-off
This capability is essential for the economic viability of next-generation
nuclear power. Small modular reactors represent a promising solution to growing
energy demands, but their success depends on reducing per-megawatt operating
costs through increased autonomy. This research will provide the tools to
achieve that autonomy while maintaining the exceptional safety record required
by the nuclear industry.
