diff -r 46709047b260 -r 1da31f35eae3 slides/src/slides.tex
--- a/slides/src/slides.tex	Fri Jul 22 04:33:59 2011 +0200
+++ b/slides/src/slides.tex	Fri Jul 22 15:52:20 2011 +0200
@@ -500,6 +500,32 @@
 \end{frame}
 
 \begin{frame}
+\frametitle{Automata Construction}
+\framesubtitle{Formula automata}
+\begin{center}
+Model $\M_\varphi$ for formula $\varphi$\\
+$\Downarrow$\\
+Closure $CL(\varphi)$ of $\varphi$\\
+$\Downarrow$\\
+Automaton $\A_\varphi$ for $\varphi$\\
+\vspace{20pt}
+\textcolor{red}{On-the-fly methods} \`a la Gerth et al.
+\end{center}
+\end{frame}
+
+\begin{frame}
+\frametitle{Automata Construction}
+\framesubtitle{System automata}
+\begin{center}
+Model $\M_\varphi$ for formula $\varphi$\\
+$\Downarrow$\\
+Closure $CL(\varphi)$ of $\varphi$\\
+$\Downarrow$\\
+Automaton $\A_\varphi$ for $\varphi$
+\end{center}
+\end{frame}
+
+\begin{frame}
 \frametitle{Model Checking}
 \framesubtitle{Definition}
 \begin{thm:model checking}