\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}[c]
    \begin{column}{0.7\textwidth}
      \includegraphics[
        width=1.0\textwidth,
        trim={1cm 22cm 1cm 0cm},
        clip
      ]
      {images/4_research_approach/procedure.png}
      \scriptsize{
      Westinghouse Technology Systems Manual, Section 19.0 - Plant Operations
    }
    \end{column}

    \begin{column}{0.3\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}
      }

      \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 reactive synthesis to convert the logical formulae to generate discrete
  automata}

  \begin{columns}
    \begin{column}{0.5\textwidth}
      \begin{tikzpicture}
        \node (chess) at (0cm,0cm){\includegraphics[width=0.4\textwidth]{images/4_research_approach/strategy.png}};
        \node[draw=textcolor, fill=secondary, left=0.1cm of chess, yshift=-0.8cm] {Plant};
        \node[draw=textcolor, fill=primary!30!red, right=0.1cm of chess, yshift=0.4cm] {Controller};
      \end{tikzpicture}
    \end{column}
    \begin{column}{0.5\textwidth}
      \pause
      \begin{tikzpicture}[
        state/.style={circle, draw=textcolor, fill=secondary, minimum size=1.2cm},
        transition/.style={->, >=stealth, thick}
      ]
        
        % States arranged vertically
        \coordinate (start) at (0,1.5);
        \node[state] (s0) at (0,0) {\scriptsize MODE 5};
        \node[state] (s1) at (0,-2) {\scriptsize MODE 4};
        \node[state] (s2) at (1,-4) {\scriptsize MODE 3};
        \node[state] (s3) at (3,-5.) {\scriptsize MODE 2};
        \node[state] (s4) at (5,-6) {\scriptsize MODE 1};
        \node[state] (s5) at (3,-1.5) {\scriptsize SCRAM};

        % Transitions
      \draw[transition] (start) -- node[midway, right] {\scriptsize Start} (s0);
        \draw[transition] (s0) -- (s1);
        \draw[transition] (s1) -- (s2);
        \draw[transition] (s2) -- (s3);
        \draw[transition] (s3) -- (s4);
        \draw[transition] (s2) to[bend right] (s5);
        \draw[transition] (s1) to[bend right] (s5);
        \draw[transition] (s3) to[bend right] (s5);
        \draw[transition] (s4) to[bend right] (s5);

        \draw[transition] (s0) to[loop left] (s0);
        \draw[transition] (s1) to[loop left] (s1);
        \draw[transition] (s2) to[loop left] (s2);
        \draw[transition] (s3) to[loop below] (s3);
        \draw[transition] (s4) to[loop below] (s4);

      \end{tikzpicture}
    \end{column}
  \end{columns}
  
\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}