1.1 --- a/paper/src/paper.tex Fri Jul 15 23:39:56 2011 +0200
1.2 +++ b/paper/src/paper.tex Tue Jul 19 02:33:21 2011 +0200
1.3 @@ -1,4 +1,5 @@
1.4 -\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}
1.5 +\documentclass{beamer}
1.6 +%\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}
1.7 \usepackage{graphicx}
1.8 %\usepackage[latin1]{inputenc}
1.9 \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
1.10 @@ -278,7 +279,7 @@
1.11 An LTL-\emph{frame} is a tuple $\F = (S, R)$, where $S = \{s_i \mid i \in \N\}$ is the set of states and $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ the set of accessibility relations. Hence $S$ is an isomorphism of $\N$ and $R$ an isomorphism of the strict linear order $(\N, <)$, which corresponds to the linear progression of discrete time.
1.12 \end{def:frames}
1.13 %
1.14 -\noindent The frame defines the structure of linear time and the flow temporal events. To perfect our structure for temporal reasoning, we need to give those events a formal meaning. We do so by assigning a value to each atomic proposition.
1.15 +\noindent The frame defines the structure of linear time and the temporal flow of events. To perfect our structure for temporal reasoning, we need to give those events a formal meaning. We do so by assigning a value to each atomic proposition.
1.16
1.17 \begin{def:models}
1.18 An LTL-\emph{model} is a tuple $\M = (\F, V)$, where $\F$ is a \emph{frame} and $V: S \to 2^\Prop$ a \emph{valuation function}. Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/slides/makefile Tue Jul 19 02:33:21 2011 +0200
2.3 @@ -0,0 +1,5 @@
2.4 +paper:
2.5 + pdflatex -output-directory=out -aux-directory=out src/slides.tex
2.6 +
2.7 +clean:
2.8 + rm -rf out/*
2.9 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/slides/src/bnf.tex Tue Jul 19 02:33:21 2011 +0200
3.3 @@ -0,0 +1,72 @@
3.4 +%-----cut here with a sharp machete or an 19.95 ginsu knife
3.5 +%************************************************************************
3.6 +%* BNF.tex *
3.7 +%* *
3.8 +%* plain tex macros for formatting grammars *
3.9 +%* *
3.10 +%* Erik Quanstrom *
3.11 +%* 10. November 1990 *
3.12 +%************************************************************************
3.13 +
3.14 +%things to fix:
3.15 +% make configurable
3.16 +% work with texinfo
3.17 +
3.18 +\gdef\actifygrammarchars{%
3.19 + \catcode`\>\active%
3.20 + \catcode`\<\active%
3.21 + \catcode`\:\active%
3.22 + \catcode`\"\active%
3.23 + \catcode`\;\active%
3.24 + \catcode`\.\active%
3.25 + \catcode`\|\active%
3.26 + \catcode`\,\active}
3.27 +
3.28 +\gdef\deactifygrammarchars{%
3.29 + \catcode`\>12%
3.30 + \catcode`\<12%
3.31 + \catcode`\:12%
3.32 + \catcode`\;12%
3.33 + \catcode`\.12%
3.34 + \catcode`\|12%
3.35 + \catcode`\,12}
3.36 +
3.37 +\newif\ifquote
3.38 +\quotefalse
3.39 +
3.40 +\begingroup
3.41 + \actifygrammarchars
3.42 + \gdef>{\/\endgroup$\rangle$\relax}
3.43 + \gdef<{$\langle$\begingroup\sl}
3.44 + \gdef:{$\rightarrow$}
3.45 +
3.46 + \begingroup
3.47 + \catcode`\"\active
3.48 + \gdef"{\ifquote%
3.49 + '\endgroup\quotefalse%
3.50 + \else%
3.51 + \quotetrue\begingroup\deactifygrammarchars\bf`%
3.52 + \fi}%
3.53 + \endgroup
3.54 +
3.55 + \gdef;{\hfill\break}
3.56 + \gdef.{\relax}
3.57 + \gdef|{$\vert$}
3.58 + \gdef,{;\hbox to 1cm{\hfill}}
3.59 +\endgroup
3.60 +
3.61 +\def\begingrammar{%
3.62 + \begingroup
3.63 + \advance\leftskip by 1cm%
3.64 + \parindent=-1cm%
3.65 + \actifygrammarchars%
3.66 + \def\endgrammar{\endgroup}
3.67 + \parskip 1ex%
3.68 + \relax
3.69 +}
3.70 +
3.71 +%
3.72 +%
3.73 +%
3.74 +\def\ul{\lower .2ex\hbox to 1ex{\hrulefill}\relax}%
3.75 +
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/slides/src/bnfexample.tex Tue Jul 19 02:33:21 2011 +0200
4.3 @@ -0,0 +1,106 @@
4.4 +% here's the example
4.5 +\input generic.tex
4.6 +\input bnf.tex
4.7 +
4.8 +\begingrammar
4.9 +%
4.10 +<input>: {$\phi$};
4.11 + <statement>.\par
4.12 +
4.13 +<statement>: "$\{$" <compound> "$\}$" [";"] ;
4.14 + <single> [";"] ;
4.15 + ";".
4.16 +
4.17 +<compound>: <single> ";" <compound> ;
4.18 + <single>.
4.19 +
4.20 +<single>: "if" "(" <expression> ")" <statement> ["else" <statement>];
4.21 + "case" "$\{$" <case-body> "$\}$";
4.22 + "for" "(" <expression> ";" <expression> ";" <expression> ")",
4.23 + <statement>;
4.24 + "while" "(" <expression> ")" <statement>;
4.25 + "do" <expression> "while" "(" <expression> ")";
4.26 + "sum" "(" <expression> ";" <expression> ")" <statment>;
4.27 + "product" "(" <expression> ";" <expression> ")" <statment>;
4.28 + "break";
4.29 + "continue";
4.30 + "return" <expression>;
4.31 + "clear";
4.32 + "load" <expression>;
4.33 + "save" <expression>;
4.34 + "release" <expression>;
4.35 + "show" ["variables" | "functions" | "set" | "all" | <expression>];
4.36 + "set" ["prompt" | "precision"] [<expression>];
4.37 + <equation>.
4.38 +
4.39 +<case-body>: "case" <expression> ":" <compound> <case-body>;
4.40 + "default:" <compound>
4.41 +
4.42 +<equation>: <var> "=" <expression>;
4.43 + <var>"[" <selector> "]" = <expression>;
4.44 + <function> = <input>;
4.45 + <expression>.
4.46 +
4.47 +<selector>: <factor> "," <factor>;
4.48 + <factor> ",";
4.49 + "," <factor>.
4.50 +
4.51 +<expression>: <term> "+" <expression>;
4.52 + <term> "--" <expression>.
4.53 +
4.54 +<term>: <factor> <operator> <term>.
4.55 +
4.56 +<factor> <pre-op> <factor$'$> <post-op>.
4.57 +
4.58 +<factor$'$>: <number>;
4.59 + "+" <number>;
4.60 + "--" <number>;
4.61 + "(" <number> ")";
4.62 + <variable>;
4.63 + <variable>"[" <selector> "]";
4.64 + <string>;
4.65 + <matrix>;
4.66 + <function>.
4.67 +
4.68 +<pre-op>: "++" | "--{\kern 1pt}--" | "$\sim$" | "!".
4.69 +
4.70 +<post-op>: "$\uparrow$" <factor>
4.71 + | "**" <factor>;
4.72 + "++" | "--{\kern 1pt}--" | "!".
4.73 +
4.74 +<matrix>: "[" <row-list> "]".
4.75 +
4.76 +<row-list>: "[" <value-list> "]" [","] <row-list>;
4.77 + "[" <value-list> "]" [","] <row-list>;
4.78 + <value-list>.
4.79 +
4.80 +<value-list>: [ <string> ] <expression> "," <value-list>;
4.81 + [ <string> ] <expression>.
4.82 +
4.83 +<function>: <variable> "(" <arg-list> ")".
4.84 +
4.85 +<arg-list>: $\phi$;
4.86 + <variable> "," <arglist>;
4.87 + "\dots".
4.88 +
4.89 +<string>: " `` " <anything> " '' ".
4.90 +
4.91 +<number>: <real-number>;
4.92 + "$\{$" <real-number> "," <real-number> "$\}$";
4.93 + {$\backslash$}b[01][01]+;
4.94 + {$\backslash$}o[07][07]+;
4.95 + \$[0-9A-Fa-f][0-9A-Fa-f]+.
4.96 +
4.97 +%<real-number>: [\+--]?[0-9][0-9]+[\.[0-9]+]?[[eE][0-9][0-9]+].
4.98 +
4.99 +<operator>: "*" | "/" | "$\backslash$" | "\%";
4.100 + "==" | "!=" | "$>$" | "$<$"
4.101 + | "$<$=" | "$>$=";
4.102 + "\ul =" | "\ul !=" | "\ul $<$" | "\ul $>$"
4.103 + | "\ul$<$=" | "\ul$>$=";
4.104 + "\&" | "$\vert$" | "$\uparrow\uparrow$";
4.105 + "\&\&" | "$\Vert$" | "\ul$\uparrow$".
4.106 +
4.107 +\endgrammar
4.108 +\bye
4.109 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/slides/src/slides.tex Tue Jul 19 02:33:21 2011 +0200
5.3 @@ -0,0 +1,137 @@
5.4 +\documentclass[9pt]{beamer}
5.5 +\usetheme{Boadilla}
5.6 +\usecolortheme{seagull}
5.7 +
5.8 +\newcommand{\M}{\mathcal{M}}
5.9 +\newcommand{\N}{\mathbb{N}_0}
5.10 +\newcommand{\F}{\mathcal{F}}
5.11 +\newcommand{\Prop}{\mathcal{P}}
5.12 +\newcommand{\A}{\mathcal{A}}
5.13 +\newcommand{\X}{\mathcal{X}}
5.14 +\newcommand{\U}{\mathcal{U}}
5.15 +\newcommand{\V}{\mathcal{V}}
5.16 +\newcommand{\dnf}{\mathsf{dnf}}
5.17 +\newcommand{\consq}{\mathsf{consq}}
5.18 +
5.19 +\theoremstyle{definition} %plain, definition, remark, proof, corollary
5.20 +\newtheorem*{def:finite words}{Finite words}
5.21 +\newtheorem*{def:infinite words}{Infinite words}
5.22 +\newtheorem*{def:regular languages}{Regular languages}
5.23 +\newtheorem*{def:regular languages closure}{Regular closure}
5.24 +\newtheorem*{def:omega regular languages}{$\omega$-regular languages}
5.25 +\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
5.26 +\newtheorem*{def:buechi automata}{Automaton}
5.27 +\newtheorem*{def:automata runs}{Runs}
5.28 +\newtheorem*{def:automata acceptance}{Acceptance}
5.29 +\newtheorem*{def:general automata}{Generalised automata}
5.30 +\newtheorem*{def:general acceptance}{Acceptance}
5.31 +\newtheorem*{def:vocabulary}{Vocabulary}
5.32 +\newtheorem*{def:frames}{Frames}
5.33 +\newtheorem*{def:models}{Models}
5.34 +\newtheorem*{def:satisfiability}{Satisfiability}
5.35 +\newtheorem*{def:fs closure}{Closure}
5.36 +\newtheorem*{def:atoms}{Atoms}
5.37 +\newtheorem*{def:rep function}{Representation function}
5.38 +\newtheorem*{def:next}{Next function}
5.39 +\newtheorem*{def:dnf}{Disjunctive normal form}
5.40 +\newtheorem*{def:positive formulae}{Positive formulae}
5.41 +\newtheorem*{def:consq}{Logical consequences}
5.42 +\newtheorem*{def:partial automata}{Partial automata}
5.43 +
5.44 +\theoremstyle{plain}
5.45 +\newtheorem{prop:vocabulary sat}{Proposition}[section]
5.46 +\newtheorem{prop:general equiv}{Proposition}[section]
5.47 +\newtheorem{prop:computation set=language}{Proposition}[section]
5.48 +
5.49 +\theoremstyle{plain}
5.50 +\newtheorem{thm:model language}{Theorem}[section]
5.51 +\newtheorem{cor:mod=model language}{Corollary}[thm:model language]
5.52 +\newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
5.53 +\newtheorem{thm:model checking}{Theorem}[section]
5.54 +\newtheorem{lem:dnf}{Lemma}[section]
5.55 +\newtheorem{lem:consq}[lem:dnf]{Lemma}
5.56 +
5.57 +\title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}
5.58 +\author{Eugen Sawin}
5.59 +\institute[University of Freiburg]
5.60 +{
5.61 + Research Group for Foundations in Artificial Intelligence\\
5.62 + Computer Science Department\\
5.63 + University of Freiburg
5.64 +}
5.65 +\date[SS 2011]{Seminar: Automata Constructions in Model Checking}
5.66 +\subject{Model Checking}
5.67 +
5.68 +\begin{document}
5.69 +\frame{\titlepage}
5.70 +\begin{frame}
5.71 +\frametitle{Motivation}
5.72 +\tableofcontents[currentsection]
5.73 +\end{frame}
5.74 +
5.75 +\begin{frame}
5.76 +\frametitle{Infinity}
5.77 +\framesubtitle{A bit more information about this}
5.78 +
5.79 +\end{frame}
5.80 +
5.81 +\begin{frame}
5.82 +\frametitle{B\"uchi Automata}
5.83 +\framesubtitle{A bit more information about this}
5.84 +
5.85 +\begin{def:buechi automata}
5.86 +A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$, with:
5.87 +\begin{itemize}
5.88 +\item $\Sigma$ is a finite non-empty \emph{alphabet}
5.89 +\item $S$ is a finite non-empty set of \emph{states}
5.90 +\item $S_0 \subseteq S$ is the set of \emph{initial states}
5.91 +\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}
5.92 +\item $F \subseteq S$ is the set of \emph{accepting states}
5.93 +\end{itemize}
5.94 +\end{def:buechi automata}
5.95 +\end{frame}
5.96 +
5.97 +\begin{frame}
5.98 +\frametitle{Linear Temporal Logic}
5.99 +\framesubtitle{A bit more information about this}
5.100 +
5.101 +\end{frame}
5.102 +
5.103 +\begin{frame}
5.104 +\frametitle{Model Checking}
5.105 +\framesubtitle{A bit more information about this}
5.106 +
5.107 +\end{frame}
5.108 +
5.109 +\begin{frame}
5.110 +\frametitle{On-the-fly Methods}
5.111 +\framesubtitle{A bit more information about this}
5.112 +
5.113 +\end{frame}
5.114 +
5.115 +\begin{frame}[allowframebreaks]
5.116 +\frametitle<presentation>{Literature}
5.117 +\begin{thebibliography}{10}
5.118 +
5.119 +\beamertemplatearticlebibitems
5.120 +\bibitem{ref:ltl&büchi}
5.121 +Madhavan Mukund.
5.122 +\newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
5.123 +\newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
5.124 +
5.125 +\beamertemplatearticlebibitems
5.126 +\bibitem{ref:alternating verification}
5.127 +Moshe Y. Vardi.
5.128 +\newblock {\em Alternating Automata and Program Verification}.
5.129 +\newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
5.130 +
5.131 +\beamertemplatebookbibitems
5.132 +\bibitem{ref:handbook}
5.133 +Patrick Blackburn and Frank Wolter and Johan van Benthem.
5.134 +\newblock {\em Handbook of Modal Logic}.
5.135 +\newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.
5.136 +
5.137 +\end{thebibliography}
5.138 +\end{frame}
5.139 +
5.140 +\end{document}