1.1 --- a/slides/src/slides.tex	Fri Jul 22 04:33:59 2011 +0200
     1.2 +++ b/slides/src/slides.tex	Fri Jul 22 15:52:20 2011 +0200
     1.3 @@ -500,6 +500,32 @@
     1.4  \end{frame}
     1.5  
     1.6  \begin{frame}
     1.7 +\frametitle{Automata Construction}
     1.8 +\framesubtitle{Formula automata}
     1.9 +\begin{center}
    1.10 +Model $\M_\varphi$ for formula $\varphi$\\
    1.11 +$\Downarrow$\\
    1.12 +Closure $CL(\varphi)$ of $\varphi$\\
    1.13 +$\Downarrow$\\
    1.14 +Automaton $\A_\varphi$ for $\varphi$\\
    1.15 +\vspace{20pt}
    1.16 +\textcolor{red}{On-the-fly methods} \`a la Gerth et al.
    1.17 +\end{center}
    1.18 +\end{frame}
    1.19 +
    1.20 +\begin{frame}
    1.21 +\frametitle{Automata Construction}
    1.22 +\framesubtitle{System automata}
    1.23 +\begin{center}
    1.24 +Model $\M_\varphi$ for formula $\varphi$\\
    1.25 +$\Downarrow$\\
    1.26 +Closure $CL(\varphi)$ of $\varphi$\\
    1.27 +$\Downarrow$\\
    1.28 +Automaton $\A_\varphi$ for $\varphi$
    1.29 +\end{center}
    1.30 +\end{frame}
    1.31 +
    1.32 +\begin{frame}
    1.33  \frametitle{Model Checking}
    1.34  \framesubtitle{Definition}
    1.35  \begin{thm:model checking}