model_checking_seminar: slides/src/slides.tex@ba1253cb17a2

     1 \documentclass[9pt]{beamer}

     2 \usetheme{Boadilla}

     3 \usecolortheme{seagull}

     5 \newcommand{\M}{\mathcal{M}}

     6 \newcommand{\N}{\mathbb{N}_0}

     7 \newcommand{\F}{\mathcal{F}}

     8 \newcommand{\Prop}{\mathcal{P}}

     9 \newcommand{\A}{\mathcal{A}}

    10 \newcommand{\X}{\mathcal{X}}

    11 \newcommand{\U}{\mathcal{U}}

    12 \newcommand{\V}{\mathcal{V}}

    13 \newcommand{\dnf}{\mathsf{dnf}}

    14 \newcommand{\consq}{\mathsf{consq}}

    16 \theoremstyle{definition} %plain, definition, remark, proof, corollary

    17 \newtheorem*{def:finite words}{Finite words}

    18 \newtheorem*{def:infinite words}{Infinite words}

    19 \newtheorem*{def:regular languages}{Regular languages}

    20 \newtheorem*{def:regular languages closure}{Regular closure}

    21 \newtheorem*{def:omega regular languages}{$\omega$-regular languages}

    22 \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}

    23 \newtheorem*{def:buechi automata}{Automaton}

    24 \newtheorem*{def:automata runs}{Runs}

    25 \newtheorem*{def:automata acceptance}{Acceptance}

    26 \newtheorem*{def:general automata}{Generalised automata}

    27 \newtheorem*{def:general acceptance}{Acceptance}

    28 \newtheorem*{def:vocabulary}{Vocabulary}

    29 \newtheorem*{def:frames}{Frames}

    30 \newtheorem*{def:models}{Models}

    31 \newtheorem*{def:satisfiability}{Satisfiability}

    32 \newtheorem*{def:fs closure}{Closure}

    33 \newtheorem*{def:atoms}{Atoms}

    34 \newtheorem*{def:rep function}{Representation function}

    35 \newtheorem*{def:next}{Next function}

    36 \newtheorem*{def:dnf}{Disjunctive normal form}

    37 \newtheorem*{def:positive formulae}{Positive formulae}

    38 \newtheorem*{def:consq}{Logical consequences}

    39 \newtheorem*{def:partial automata}{Partial automata}

    41 \theoremstyle{plain}

    42 \newtheorem{prop:vocabulary sat}{Proposition}[section]

    43 \newtheorem{prop:general equiv}{Proposition}[section]

    44 \newtheorem{prop:computation set=language}{Proposition}[section]

    46 \theoremstyle{plain}

    47 \newtheorem{thm:model language}{Theorem}[section]

    48 \newtheorem{cor:mod=model language}{Corollary}[thm:model language]

    49 \newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}

    50 \newtheorem{thm:model checking}{Theorem}[section]

    51 \newtheorem{lem:dnf}{Lemma}[section]

    52 \newtheorem{lem:consq}[lem:dnf]{Lemma}

    54 \title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}

    55 \author{Eugen Sawin}

    56 \institute[University of Freiburg]

    57 {

    58   Research Group for Foundations in Artificial Intelligence\\

    59   Computer Science Department\\

    60   University of Freiburg

    61 }

    62 \date[SS 2011]{Seminar: Automata Constructions in Model Checking}

    63 \subject{Model Checking}

    65 \begin{document}

    66 \frame{\titlepage}

    67 \begin{frame}

    68 \frametitle{Motivation}

    69 \tableofcontents[currentsection]

    70 \end{frame}

    72 \begin{frame}

    73 \frametitle{Infinity}

    74 \framesubtitle{A bit more information about this}

    76 \end{frame}

    78 \begin{frame}

    79 \frametitle{B\"uchi Automata}

    80 \framesubtitle{A bit more information about this}

    82 \begin{def:buechi automata}

    83 A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$, with:

    84 \begin{itemize}

    85 \item $\Sigma$ is a finite non-empty \emph{alphabet}

    86 \item $S$ is a finite non-empty set of \emph{states}

    87 \item $S_0 \subseteq S$ is the set of \emph{initial states}

    88 \item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}

    89 \item $F \subseteq S$ is the set of \emph{accepting states}

    90 \end{itemize}

    91 \end{def:buechi automata}

    92 \end{frame}

    94 \begin{frame}

    95 \frametitle{Linear Temporal Logic}

    96 \framesubtitle{A bit more information about this}

    98 \end{frame}

   100 \begin{frame}

   101 \frametitle{Model Checking}

   102 \framesubtitle{A bit more information about this}

   104 \end{frame}

   106 \begin{frame}

   107 \frametitle{On-the-fly Methods}

   108 \framesubtitle{A bit more information about this}

   110 \end{frame}

   112 \begin{frame}[allowframebreaks]

   113 \frametitle<presentation>{Literature}

   114 \begin{thebibliography}{10}

   116 \beamertemplatearticlebibitems

   117 \bibitem{ref:ltl&büchi}

   118 Madhavan Mukund.

   119 \newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.

   120 \newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.

   122 \beamertemplatearticlebibitems

   123 \bibitem{ref:alternating verification}

   124 Moshe Y. Vardi.

   125 \newblock {\em Alternating Automata and Program Verification}.

   126 \newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.

   128 \beamertemplatebookbibitems

   129 \bibitem{ref:handbook}

   130 Patrick Blackburn and Frank Wolter and Johan van Benthem.

   131 \newblock {\em Handbook of Modal Logic}.

   132 \newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.

   134 \end{thebibliography}

   135 \end{frame}

   137 \end{document}

author	Eugen Sawin <sawine@me73.com>
	Tue, 19 Jul 2011 02:33:21 +0200
changeset 55	ba1253cb17a2
child 56	7190dae7df06
permissions	-rw-r--r--