\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\_5\_active $\land$}
            \item[] \texttt{k\_eff\_subcritical $\land$}
            \item[] \texttt{zero\_power $\land$}
            \item[] \texttt{temp\_safe $\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!primary] (ltl) {LTL\\Specification};
    \node[draw, rectangle, minimum width=3cm, minimum height=1.5cm, align=center, fill=blue!20!primary, right=of ltl] (game) {Parity\\Game};
    \node[draw, rectangle, minimum width=3cm, minimum height=1.5cm, align=center, fill=blue!20!primary, 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}

  \begin{columns}
    \begin{column}{0.5\textwidth}
      \includegraphics[height=0.7\textheight]{bouncing_ball_hybrid.png}

    \end{column}

    \begin{column}{0.5\textwidth}
      \only<2>{
        \begin{alertblock}{Key Challenge}
          \small
          Verify continuous control behavior across discrete mode transitions
        \end{alertblock}
      }
      \only<3->{
        \begin{block}{Key Challenge}
          \small
          Verify continuous control behavior across discrete mode transitions
        \end{block}
      }

      \vspace{0.3cm}

      \only<3>{
        \begin{alertblock}{Reachable Set}
          \small
          $\mathcal{R}(t) = \{x(t) \mid x(0) \in X_0, \dot{x} = f(x)\}$
        \end{alertblock}
      }
      \only<4->{
        \begin{block}{Reachable Set}
          \small
          $\mathcal{R}(t) = \{x(t) \mid x(0) \in X_0, \dot{x} = f(x)\}$
        \end{block}
      }

      \vspace{0.3cm}

      \only<4>{
        \begin{alertblock}{Barrier Certificate}
          \small
          $B(x) > 0 \land \nabla B \cdot f(x) \leq 0 \implies x \in \text{Safe}$
        \end{alertblock}
      }
    \end{column}
  \end{columns}

\end{frame}

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

  \begin{enumerate}
    \item<1-> \alert<1>{Formalize regulatory procedures into FRET specifications and translate to Linear Temporal Logic (LTL)}

    \item<2-> \alert<2>{Synthesize discrete automata from LTL using reactive synthesis}

    \item<3-> \alert<3>{Design continuous controllers for each discrete mode and verify safety across mode transitions using barrier certificates and reachability analysis}
  \end{enumerate}

  \vspace{1cm}
 
  \onslide<4>{
    \begin{center}
      \large
      \textbf{Result: Complete hybrid autonomous system\\
      with correctness guarantees by construction}
    \end{center}
  }

\end{frame}