% 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.}
\dasinline{Title needs updated to High Assurance Hybrid
Control Systems. Maybe removal of `formal'?}

% INTRODUCTORY PARAGRAPH Hook
Nuclear power relies on extensively trained operators who follow detailed
written procedures to manage reactor control.\dasinline{Why is there any
hyphenation at all? Why not full justification?} Based on these procedures and
\oldt{operators'} \newt{their} interpretation of plant conditions, \oldt{operators} \newt{they} 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
\oldt{But, reliance} \newt{This 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...''}
\dasinline{Or just straight up ``this reliance''.
Right to the topic.}
Small modular reactors face significantly higher per-megawatt staffing costs 
than conventional 
plants.\dasinline{Obvious but source required.} Autonomous control systems \oldt{are
needed that can} \newt{must} 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.}\dasinline{Add
``and leverage existing domain knowledge'' or similar.
Industry knowledge can be reused here --- less like
starting from scratch.}
% 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.\dasinline{Had to read this twice.} Second, we will synthesize
discrete mode switching logic using reactive 
synthesis\dasinline{Also had to read this twice. A lot of
jargon. Check topic stress.}
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\dasinline{I don't think
I ever mention this phrase again specifically. Might be a
dogwhistle to other work unintentionally. Must be
careful.} 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.\dasinline{Where did this come from? Needs context.}
\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 \oldt{will demonstrate autonomous control can be used for} \newt{enables autonomous management of} 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,\dasinline{This may not be true, and perhaps
    does not belong.} 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 \oldt{implement high-assurance autonomous
    controls on industrial platforms they already use, enabling users to
    achieve autonomy without retraining costs or developing new 
    equipment.} \newt{achieve autonomy without retraining costs or developing new equipment by implementing high-assurance autonomous controls on industrial platforms they already use.}\splitnote{Strong industrial grounding --- the ``platforms they 
    already use'' point is compelling for 
    adoption.}\dasinline{Flip the clauses. Put retraining
    and new equipment before the comma, end with building
    HAHACs with control hardware they already use.
    That's the more important part.}

\end{enumerate}