sawine@55: \documentclass[9pt]{beamer}
sawine@55: \usetheme{Boadilla}
sawine@55: \usecolortheme{seagull}
sawine@55: 
sawine@55: \newcommand{\M}{\mathcal{M}}
sawine@55: \newcommand{\N}{\mathbb{N}_0}
sawine@55: \newcommand{\F}{\mathcal{F}}
sawine@55: \newcommand{\Prop}{\mathcal{P}}
sawine@55: \newcommand{\A}{\mathcal{A}}
sawine@55: \newcommand{\X}{\mathcal{X}}
sawine@55: \newcommand{\U}{\mathcal{U}}
sawine@55: \newcommand{\V}{\mathcal{V}}
sawine@55: \newcommand{\dnf}{\mathsf{dnf}}
sawine@55: \newcommand{\consq}{\mathsf{consq}}
sawine@55: 
sawine@55: \theoremstyle{definition} %plain, definition, remark, proof, corollary
sawine@55: \newtheorem*{def:finite words}{Finite words}
sawine@55: \newtheorem*{def:infinite words}{Infinite words}
sawine@55: \newtheorem*{def:regular languages}{Regular languages}
sawine@55: \newtheorem*{def:regular languages closure}{Regular closure}
sawine@55: \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
sawine@55: \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
sawine@55: \newtheorem*{def:buechi automata}{Automaton}
sawine@55: \newtheorem*{def:automata runs}{Runs}
sawine@55: \newtheorem*{def:automata acceptance}{Acceptance}
sawine@55: \newtheorem*{def:general automata}{Generalised automata}
sawine@55: \newtheorem*{def:general acceptance}{Acceptance}
sawine@55: \newtheorem*{def:vocabulary}{Vocabulary}
sawine@55: \newtheorem*{def:frames}{Frames}
sawine@55: \newtheorem*{def:models}{Models}
sawine@55: \newtheorem*{def:satisfiability}{Satisfiability}
sawine@55: \newtheorem*{def:fs closure}{Closure}
sawine@55: \newtheorem*{def:atoms}{Atoms}
sawine@55: \newtheorem*{def:rep function}{Representation function}
sawine@55: \newtheorem*{def:next}{Next function}
sawine@55: \newtheorem*{def:dnf}{Disjunctive normal form}
sawine@55: \newtheorem*{def:positive formulae}{Positive formulae}
sawine@55: \newtheorem*{def:consq}{Logical consequences}
sawine@55: \newtheorem*{def:partial automata}{Partial automata}
sawine@55: 
sawine@55: \theoremstyle{plain}
sawine@55: \newtheorem{prop:vocabulary sat}{Proposition}[section]
sawine@55: \newtheorem{prop:general equiv}{Proposition}[section]
sawine@55: \newtheorem{prop:computation set=language}{Proposition}[section]
sawine@55: 
sawine@55: \theoremstyle{plain}
sawine@55: \newtheorem{thm:model language}{Theorem}[section]
sawine@55: \newtheorem{cor:mod=model language}{Corollary}[thm:model language]
sawine@55: \newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
sawine@55: \newtheorem{thm:model checking}{Theorem}[section]
sawine@55: \newtheorem{lem:dnf}{Lemma}[section]
sawine@55: \newtheorem{lem:consq}[lem:dnf]{Lemma}
sawine@55: 
sawine@55: \title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}
sawine@55: \author{Eugen Sawin}
sawine@55: \institute[University of Freiburg]
sawine@55: { 
sawine@55:   Research Group for Foundations in Artificial Intelligence\\
sawine@55:   Computer Science Department\\
sawine@55:   University of Freiburg
sawine@55: }
sawine@55: \date[SS 2011]{Seminar: Automata Constructions in Model Checking}
sawine@55: \subject{Model Checking}
sawine@55: 
sawine@55: \begin{document}
sawine@55: \frame{\titlepage}
sawine@55: \begin{frame}
sawine@55: \frametitle{Motivation}
sawine@55: \tableofcontents[currentsection]
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@55: \frametitle{Infinity}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: 
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@55: \frametitle{B\"uchi Automata}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: 
sawine@55: \begin{def:buechi automata}
sawine@55: A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$, with:
sawine@55: \begin{itemize}
sawine@55: \item $\Sigma$ is a finite non-empty \emph{alphabet}
sawine@55: \item $S$ is a finite non-empty set of \emph{states}
sawine@55: \item $S_0 \subseteq S$ is the set of \emph{initial states}
sawine@55: \item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}
sawine@55: \item $F \subseteq S$ is the set of \emph{accepting states} 
sawine@55: \end{itemize}
sawine@55: \end{def:buechi automata}
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@55: \frametitle{Linear Temporal Logic}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: 
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@55: \frametitle{Model Checking}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: 
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@55: \frametitle{On-the-fly Methods}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: 
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}[allowframebreaks]
sawine@55: \frametitle<presentation>{Literature}    
sawine@55: \begin{thebibliography}{10}    
sawine@55: 
sawine@55: \beamertemplatearticlebibitems
sawine@55: \bibitem{ref:ltl&büchi}
sawine@55: Madhavan Mukund.
sawine@55: \newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
sawine@55: \newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
sawine@55:   
sawine@55: \beamertemplatearticlebibitems
sawine@55: \bibitem{ref:alternating verification}
sawine@55: Moshe Y. Vardi.
sawine@55: \newblock {\em Alternating Automata and Program Verification}.
sawine@55: \newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
sawine@55: 
sawine@55: \beamertemplatebookbibitems
sawine@55: \bibitem{ref:handbook}
sawine@55: Patrick Blackburn and Frank Wolter and Johan van Benthem.
sawine@55: \newblock {\em Handbook of Modal Logic}.
sawine@55: \newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.
sawine@55: 
sawine@55: \end{thebibliography}
sawine@55: \end{frame}
sawine@55: 
sawine@55: \end{document}