\documentclass[9pt]{beamer}
\usetheme{Boadilla}
\usecolortheme{seagull}

\newcommand{\M}{\mathcal{M}}
\newcommand{\N}{\mathbb{N}_0}
\newcommand{\F}{\mathcal{F}}
\newcommand{\Prop}{\mathcal{P}}
\newcommand{\A}{\mathcal{A}}
\newcommand{\X}{\mathcal{X}}
\newcommand{\U}{\mathcal{U}}
\newcommand{\V}{\mathcal{V}}
\newcommand{\dnf}{\mathsf{dnf}}
\newcommand{\consq}{\mathsf{consq}}

\theoremstyle{definition} %plain, definition, remark, proof, corollary
\newtheorem*{def:finite words}{Finite words}
\newtheorem*{def:infinite words}{Infinite words}
\newtheorem*{def:regular languages}{Regular languages}
\newtheorem*{def:regular languages closure}{Regular closure}
\newtheorem*{def:omega regular languages}{$\omega$-regular languages}
\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
\newtheorem*{def:buechi automata}{Automaton}
\newtheorem*{def:automata runs}{Runs}
\newtheorem*{def:automata acceptance}{Acceptance}
\newtheorem*{def:general automata}{Generalised automata}
\newtheorem*{def:general acceptance}{Acceptance}
\newtheorem*{def:vocabulary}{Vocabulary}
\newtheorem*{def:frames}{Frames}
\newtheorem*{def:models}{Models}
\newtheorem*{def:satisfiability}{Satisfiability}
\newtheorem*{def:fs closure}{Closure}
\newtheorem*{def:atoms}{Atoms}
\newtheorem*{def:rep function}{Representation function}
\newtheorem*{def:next}{Next function}
\newtheorem*{def:dnf}{Disjunctive normal form}
\newtheorem*{def:positive formulae}{Positive formulae}
\newtheorem*{def:consq}{Logical consequences}
\newtheorem*{def:partial automata}{Partial automata}

\theoremstyle{plain}
\newtheorem{prop:vocabulary sat}{Proposition}[section]
\newtheorem{prop:general equiv}{Proposition}[section]
\newtheorem{prop:computation set=language}{Proposition}[section]

\theoremstyle{plain}
\newtheorem{thm:model language}{Theorem}[section]
\newtheorem{cor:mod=model language}{Corollary}[thm:model language]
\newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
\newtheorem{thm:model checking}{Theorem}[section]
\newtheorem{lem:dnf}{Lemma}[section]
\newtheorem{lem:consq}[lem:dnf]{Lemma}

\title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}
\author{Eugen Sawin}
\institute[University of Freiburg]
{ 
  Research Group for Foundations in Artificial Intelligence\\
  Computer Science Department\\
  University of Freiburg
}
\date[SS 2011]{Seminar: Automata Constructions in Model Checking}
\subject{Model Checking}

\begin{document}
\frame{\titlepage}
\begin{frame}
\frametitle{Motivation}
\tableofcontents[currentsection]
\end{frame}

\begin{frame}
\frametitle{Infinity}
\framesubtitle{A bit more information about this}

\end{frame}

\begin{frame}
\frametitle{B\"uchi Automata}
\framesubtitle{A bit more information about this}

\begin{def:buechi automata}
A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$, with:
\begin{itemize}
\item $\Sigma$ is a finite non-empty \emph{alphabet}
\item $S$ is a finite non-empty set of \emph{states}
\item $S_0 \subseteq S$ is the set of \emph{initial states}
\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}
\item $F \subseteq S$ is the set of \emph{accepting states} 
\end{itemize}
\end{def:buechi automata}
\end{frame}

\begin{frame}
\frametitle{Linear Temporal Logic}
\framesubtitle{A bit more information about this}

\end{frame}

\begin{frame}
\frametitle{Model Checking}
\framesubtitle{A bit more information about this}

\end{frame}

\begin{frame}
\frametitle{On-the-fly Methods}
\framesubtitle{A bit more information about this}

\end{frame}

\begin{frame}[allowframebreaks]
\frametitle<presentation>{Literature}    
\begin{thebibliography}{10}    

\beamertemplatearticlebibitems
\bibitem{ref:ltl&büchi}
Madhavan Mukund.
\newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
\newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
  
\beamertemplatearticlebibitems
\bibitem{ref:alternating verification}
Moshe Y. Vardi.
\newblock {\em Alternating Automata and Program Verification}.
\newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.

\beamertemplatebookbibitems
\bibitem{ref:handbook}
Patrick Blackburn and Frank Wolter and Johan van Benthem.
\newblock {\em Handbook of Modal Logic}.
\newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.

\end{thebibliography}
\end{frame}

\end{document}
