Thesis/1-goals-and-outcomes/research-statement.tex

% GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous
control systems with event-driven control laws that have guarantees of safe and
correct behavior.\splitnote{Strong, direct opening. Sets scope immediately.}

% INTRODUCTORY PARAGRAPH Hook
Nuclear power relies on extensively trained operators who follow detailed
written procedures to manage reactor control. Based on these procedures and
operators' interpretation of plant conditions, operators make critical decisions
about when to switch between control objectives.
\splitinline{Consider: ``operators'' appears 3x in two sentences. Maybe: 
``Based on these procedures and their interpretation of plant conditions, 
they make critical decisions...''}
% Gap
But, reliance on human operators has created an economic challenge for
next-generation nuclear power plants.
\splitinline{``But, reliance'' — the comma after ``But'' is unusual. Either 
drop it or restructure: ``However, this reliance...'' or ``This reliance, 
however, has created...''}
Small modular reactors face significantly higher per-megawatt staffing costs 
than conventional 
plants. Autonomous control systems are needed that can safely manage complex 
operational sequences with the same assurance as human-operated systems, but 
without constant supervision.
\splitinline{``are needed that can'' — passive. Try: ``Autonomous control 
systems must safely manage...''}

% 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.\splitnote{Clear statement of approach.}
% Rationale
Hybrid systems use discrete logic to switch between continuous control modes,
similar to how operators change control strategies. Existing formal methods
generate provably correct switching logic but cannot handle continuous dynamics
during transitions, while traditional control theory verifies continuous
behavior but lacks tools for proving discrete switching 
correctness.\splitnote{Nice parallel structure showing the gap.}
% Hypothesis and Technical Approach
We will bridge this gap through a three-stage methodology. First, we will
translate written operating procedures into temporal logic specifications using
NASA's Formal Requirements Elicitation Tool (FRET), which structures
requirements into scope, condition, component, timing, and response elements.
This structured approach enables realizability checking to identify conflicts
and ambiguities in procedures before implementation. Second, we will synthesize
discrete mode switching logic using reactive synthesis
to generate deterministic automata that are provably
correct by construction. Third, we will develop continuous
controllers for each discrete mode using standard control theory and
reachability analysis. We will classify continuous modes based on their
transition objectives, and then employ assume-guarantee contracts and barrier
certificates to prove that mode transitions occur safely and as defined by the
deterministic automata. This compositional approach enables local verification
of continuous modes without requiring global trajectory analysis across the
entire hybrid system. We will demonstrate this on an Emerson Ovation control 
system.
\splitinline{This paragraph is dense. Consider breaking after the three 
stages, then a new paragraph for the compositional verification point and 
Emerson demo.}
% Pay-off
This approach will demonstrate autonomous control can be used for complex
nuclear power operations while maintaining safety 
guarantees.
\splitinline{``can be used for'' — weak. Try: ``...will demonstrate that 
autonomous control can manage complex nuclear power operations while 
maintaining safety guarantees.'' Or even stronger: ``...enables autonomous 
management of complex nuclear power operations with safety guarantees.''}

% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:
\begin{enumerate}
  % OUTCOME 1 Title
  \item \textit{Synthesize written procedures into verified control logic.} 
    % Strategy
    We will develop a methodology for converting written operating procedures
    into formal specifications. These specifications will be synthesized into
    discrete control logic using reactive synthesis tools.     
    % Outcome
    Control engineers will be able to generate mode-switching controllers from
    regulatory procedures with little formal methods expertise, reducing
    barriers to high-assurance control 
    systems.\splitnote{Good practical framing — emphasizes accessibility.}

    % OUTCOME 2 Title
  \item \textit{Verify continuous control behavior across mode transitions. }
    % Strategy
    We will develop methods using reachability analysis to ensure continuous 
    control modes satisfy discrete transition requirements. 
    % Outcome
    Engineers will be able to design continuous controllers using standard
    practices while ensuring system correctness and proving mode transitions
    occur safely at the right times.

    % OUTCOME 3  Title
  \item \textit{Demonstrate autonomous reactor startup control with safety
    guarantees. }
    % Strategy
    We will implement this methodology on a small modular reactor simulation
    using industry-standard control hardware.     % Outcome
    Control engineers will be able to implement high-assurance autonomous
    controls on industrial platforms they already use, enabling users to
    achieve autonomy without retraining costs or developing new 
    equipment.\splitnote{Strong industrial grounding — the ``platforms they 
    already use'' point is compelling for adoption.}

\end{enumerate}