\begin{frame}{The goal of this research is to create verified autonomous control
  systems}

  \textbf{\underline{
    If this research is successful, we will be able to do the following:
  }}
  \pause

  \begin{enumerate}

    \item \alert<2>{Translate written procedures into discrete control logic}
      \pause

    \item \alert<3>{Verify continuous control behavior across discrete mode
      transitions}
      \pause

    \item \alert<4>{Demonstrate autonomous reactor startup with verifiable safety
      guarantees}

  \end{enumerate}
\end{frame}

\begin{frame}{First, we will formalize written procedures into logical
  statements}

  \begin{columns}
    \begin{column}{0.33\textwidth}
      \includegraphics[width=\textwidth]{images/4_research_approach/procedure.png}
    \end{column}

    \begin{column}{0.33\textwidth}
      \only<2>{
        \begin{alertblock}{FRET Specification}
        \scriptsize
        \texttt{INITIAL\_CONDITIONS shall satisfy:}
        \begin{itemize}
          \item[] \texttt{mode = MODE\_5}
          \item[] \texttt{k\_eff < 0.99}
          \item[] \texttt{power = 0}
          \item[] \texttt{t\_avg < 200}
          \item[] \texttt{...}
        \end{itemize}
      \end{alertblock}
      }

      \only<3->{
        \begin{block}{FRET Specification}
        \scriptsize
        \texttt{INITIAL\_CONDITIONS shall satisfy:}
        \begin{itemize}
          \item[] \texttt{mode = MODE\_5}
          \item[] \texttt{k\_eff < 0.99}
          \item[] \texttt{power = 0}
          \item[] \texttt{t\_avg < 200}
          \item[] \texttt{...}
        \end{itemize}
      \end{block}
      }
    \end{column}

    \begin{column}{0.33\textwidth}
      \only<3>{
        \begin{alertblock}{LTL Formula}
          \scriptsize
          \texttt{$\Box$ (initial $\rightarrow$ (}
          \begin{itemize}
            \item[] \texttt{mode = MODE\_5 $\land$}
            \item[] \texttt{k\_eff < 0.99 $\land$}
            \item[] \texttt{power = 0 $\land$}
            \item[] \texttt{t\_avg < 200 $\land$}
            \item[] \texttt{...))}
          \end{itemize}
        \end{alertblock}
      }
    \end{column}
  \end{columns}

\end{frame}

\begin{frame}{Second, we will use the logical formulae to generate discrete
  automata}

  \centering
  \begin{tikzpicture}[node distance=2cm]
    % Blocks
    \node[draw, rectangle, minimum width=3cm, minimum height=1.5cm, align=center, fill=blue!20] (ltl) {LTL\\Specification};
    \node[draw, rectangle, minimum width=3cm, minimum height=1.5cm, align=center, fill=blue!20, right=of ltl] (game) {Game\\Graph};
    \node[draw, rectangle, minimum width=3cm, minimum height=1.5cm, align=center, fill=blue!20, right=of game] (automata) {Discrete\\Automata};

    % Arrows
    \draw[->, thick] (ltl) -- (game);
    \draw[->, thick] (game) -- (automata);

    % Curly bracket
    \draw[decorate, decoration={brace, amplitude=10pt, mirror}, thick]
      ([yshift=-1cm]ltl.south west) -- ([yshift=-1cm]automata.south east)
      node[midway, below=0.5cm] {\textbf{Reactive Synthesis}};
  \end{tikzpicture}

\end{frame}

\begin{frame}{Finally, we will build continuous controllers to move between
  discrete states}

\end{frame}

\begin{frame}{Verified autonomous controllers can be created by building this
chain of proof of correctness}

\end{frame}