\section{Schedule, Milestones, and Deliverables}

This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026. The work progresses sequentially through three main research thrusts before culminating in integrated demonstration and validation.

The first semester (Spring 2026) focuses on Thrust 1, translating SmAHTR startup procedures into formal temporal logic specifications using FRET. This establishes the foundation for automated synthesis by converting natural language procedures into machine-readable requirements. The second semester (Summer 2026) addresses Thrust 2, using Strix to synthesize the discrete automaton that defines mode-switching behavior. With the discrete structure established, the third semester (Fall 2026) develops the continuous controllers for each operational mode through Thrust 3, employing reachability analysis and barrier certificates to verify that each mode satisfies its transition requirements.

Integration and validation occupy the remaining three semesters. Spring 2027 integrates the verified hybrid controller into high-fidelity Simulink simulation, achieving TRL 4 through extensive testing across the operational envelope. Summer 2027 implements the controller on Emerson Ovation hardware with ARCADE providing the hardware-in-the-loop interface, demonstrating TRL 5 with actual industrial control equipment. The final semester (Fall 2027) completes validation testing, addresses any remaining issues discovered during hardware testing, and finalizes the dissertation.

Figure \ref{fig:gantt} shows the complete project schedule including research thrusts, major milestones, and planned publications.

\begin{figure}[htbp]
    \centering
    \begin{ganttchart}[
        hgrid,
        vgrid={*{4}{draw=none}, dotted},
        x unit=0.5cm,
        y unit title=0.8cm,
        y unit chart=0.6cm,
        title/.append style={fill=gray!30},
        title height=1,
        bar/.append style={fill=blue!50},
        bar height=0.5,
        bar label font=\small,
        milestone/.append style={fill=red, shape=diamond},
        milestone height=0.5,
        milestone width=0.6
    ]{1}{24}
    
    % Timeline headers
    \gantttitle{2026}{12}
    \gantttitle{2027}{12} \\
    \gantttitle{Spring}{4}
    \gantttitle{Summer}{4}
    \gantttitle{Fall}{4}
    \gantttitle{Spring}{4}
    \gantttitle{Summer}{4}
    \gantttitle{Fall}{4} \\
    
    % Major thrusts
    \ganttbar{Thrust 1: Procedure Translation}{1}{5} \\
    \ganttbar{Thrust 2: Discrete Synthesis}{4}{10} \\
    \ganttbar{Thrust 3: Continuous Control}{9}{15} \\
    \ganttbar{Integration \& Simulation (TRL 4)}{13}{17} \\
    \ganttbar{Hardware-in-Loop Testing (TRL 5)}{16}{21} \\
    \ganttbar{Dissertation Writing}{18}{24} \\[grid]
    
    % Milestones row
    \ganttbar[bar/.append style={fill=orange!50}]{Milestones}{1}{24}
    \ganttmilestone{}{4}
    \ganttmilestone{}{8}
    \ganttmilestone{}{12}
    \ganttmilestone{}{16}
    \ganttmilestone{}{20}
    \ganttmilestone{}{24} \\
    
    % Publications row
    \ganttbar[bar/.append style={fill=green!50}]{Publications}{1}{24}
    \ganttmilestone{}{8}
    \ganttmilestone{}{16}
    \ganttmilestone{}{20}
    
    \end{ganttchart}
    \caption{Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}
    \label{fig:gantt}
\end{figure}

\subsection{Milestones and Deliverables}

Six major milestones mark critical validation points throughout the research. M1
(Month 4) confirms that SmAHTR startup procedures have been successfully
translated to temporal logic using FRET with realizability analysis
demonstrating consistent and complete specifications. Domain expert review
validates that formalized specifications accurately capture procedural intent.
This milestone delivers an internal technical report documenting the t ranslation methodology and complete specification set.

M2 (Month 8) validates computational tractability by demonstrating that Strix
can synthesize a complete discrete automaton from the formalized specifications.
Success requires an automaton with fewer than 1,000 states generated within 48
hours of computation time, with all operational modes present and interpretable
structure. This milestone delivers a conference paper submission to NPIC\&HMIT
documenting the procedure-to-specification translation methodology.

M3 (Month 12) achieves TRL 3 by proving that continuous controllers can be
designed and verified to satisfy discrete transition requirements. At least one
complete operational sequence must have continuous controllers for all required
modes, with reachability analysis confirming satisfaction of transition
requirements and barrier certificates proving safety constraints. This milestone
delivers an internal technical report demonstrating component-level verification.

M4 (Month 16) achieves TRL 4 through integrated simulation demonstrating that
component-level correctness composes to system-level correctness. The complete
hybrid controller must execute autonomous startup sequences in high-fidelity
Simulink simulation with zero safety violations across 100 consecutive runs with
varied initial conditions. Discrete behavior must match synthesized
specifications exactly while continuous trajectories remain within verified
reachable sets. This milestone delivers a journal paper submission to IEEE
Transactions on Automatic Control presenting the complete hybrid synthesis
methodology.

M5 (Month 20) achieves TRL 5 by demonstrating practical implementability on
industrial hardware. The discrete automaton must be implemented on Emerson
Ovation distributed control system with ARCADE providing stable real-time
communication at required control rates. Complete autonomous startup sequences
must execute successfully via hardware-in-the-loop, including correct responses
to off-nominal scenarios such as sensor failures and loss of cooling events.
This milestone delivers a conference paper submission to NPIC\&HMIT or CDC
documenting hardware implementation and experimental validation.

M6 (Month 24) completes the dissertation documenting the entire methodology,
experimental results, and research contributions. All verification artifacts
including specifications, automata, reachable sets, and barrier functions are
publicly released along with implementation code for both simulation and
hardware integration. This enables independent replication and provides the
nuclear industry with practical tools for developing autonomous control systems.

The publication strategy targets both the nuclear instrumentation community and
the broader control systems research community. The first conference paper
(Summer 2026) presents the procedure formalization methodology to NPIC\&HMIT,
building on a previous best student paper award received at that conference.
This paper addresses the practical challenge of translating natural language
procedures into formal specifications, presenting a taxonomy of procedural
ambiguities and systematic resolution strategies that will be valuable to the
nuclear I\&C community.

The journal paper (Spring 2027) targets IEEE Transactions on Automatic Control
to establish theoretical rigor and reach the broader control systems community.
This paper presents the complete hybrid synthesis methodology as a contribution
to control theory, demonstrating how reactive synthesis and continuous
verification can be unified to address continuous autonomous hybrid systems. The
three-mode classification and compositional verification framework have
applications beyond nuclear systems to any safety-critical domain with
documented operational procedures.

The final conference paper (Summer 2027) documents hardware implementation and
experimental validation, demonstrating that the methodology produces controllers
compatible with existing industrial control infrastructure. Venue selection
between NPIC\&HMIT and IEEE Conference on Decision and Control depends on
whether emphasis is placed on nuclear industry adoption or experimental
validation of theoretical control methods. This decision will be made based on
results from preliminary hardware testing and feedback from the TRL 4 milestone
review. Additional dissemination includes release of all software tools and
verification artifacts.