# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1311035601 -7200
# Node ID ba1253cb17a2831760be0a94bea9e75662e98128
# Parent  352ab4bd22f308ade00470fd62c0c9e0d5aff036
Initial slides.

diff -r 352ab4bd22f3 -r ba1253cb17a2 paper/src/paper.tex
--- a/paper/src/paper.tex	Fri Jul 15 23:39:56 2011 +0200
+++ b/paper/src/paper.tex	Tue Jul 19 02:33:21 2011 +0200
@@ -1,4 +1,5 @@
-\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
+\documentclass{beamer}
+%\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
 \usepackage{graphicx}
 %\usepackage[latin1]{inputenc}
 \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
@@ -278,7 +279,7 @@
 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. 
 \end{def:frames}
 %
-\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.
+\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.
 
 \begin{def:models}
 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)$. 
diff -r 352ab4bd22f3 -r ba1253cb17a2 slides/makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/makefile	Tue Jul 19 02:33:21 2011 +0200
@@ -0,0 +1,5 @@
+paper: 
+	pdflatex -output-directory=out -aux-directory=out src/slides.tex
+
+clean:
+	rm -rf out/*
\ No newline at end of file
diff -r 352ab4bd22f3 -r ba1253cb17a2 slides/src/bnf.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/src/bnf.tex	Tue Jul 19 02:33:21 2011 +0200
@@ -0,0 +1,72 @@
+%-----cut here with a sharp machete or an 19.95 ginsu knife
+%************************************************************************
+%* BNF.tex								*
+%* 									*
+%* plain tex macros for formatting grammars				*
+%*									*
+%* Erik Quanstrom 							*
+%* 10. November 1990							*
+%************************************************************************
+
+%things to fix:
+%	make configurable
+%	work with texinfo
+
+\gdef\actifygrammarchars{%
+	\catcode`\>\active%
+	\catcode`\<\active%
+	\catcode`\:\active%
+	\catcode`\"\active%
+	\catcode`\;\active%
+	\catcode`\.\active%
+	\catcode`\|\active%
+	\catcode`\,\active}
+
+\gdef\deactifygrammarchars{%
+	\catcode`\>12%
+	\catcode`\<12%
+	\catcode`\:12%
+	\catcode`\;12%
+	\catcode`\.12%
+	\catcode`\|12%
+	\catcode`\,12}
+
+\newif\ifquote
+\quotefalse
+
+\begingroup
+   \actifygrammarchars
+   \gdef>{\/\endgroup$\rangle$\relax}
+   \gdef<{$\langle$\begingroup\sl}
+   \gdef:{$\rightarrow$}
+
+   \begingroup
+	\catcode`\"\active
+	\gdef"{\ifquote%
+		'\endgroup\quotefalse%
+	   \else%
+		\quotetrue\begingroup\deactifygrammarchars\bf`%
+	\fi}%
+   \endgroup
+
+   \gdef;{\hfill\break}
+   \gdef.{\relax}
+   \gdef|{$\vert$}
+   \gdef,{;\hbox to 1cm{\hfill}}
+\endgroup
+
+\def\begingrammar{%
+	\begingroup
+	\advance\leftskip by 1cm%
+	\parindent=-1cm%
+	\actifygrammarchars%
+	\def\endgrammar{\endgroup}
+	\parskip 1ex%
+	\relax
+}
+
+%
+%
+%
+\def\ul{\lower .2ex\hbox to 1ex{\hrulefill}\relax}%
+
diff -r 352ab4bd22f3 -r ba1253cb17a2 slides/src/bnfexample.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/src/bnfexample.tex	Tue Jul 19 02:33:21 2011 +0200
@@ -0,0 +1,106 @@
+% here's the example
+\input generic.tex
+\input bnf.tex
+
+\begingrammar
+%		
+<input>:	{$\phi$};
+		<statement>.\par
+
+<statement>:	"$\{$" <compound> "$\}$" [";"] ;
+		<single> [";"] ;
+		";".
+
+<compound>:	<single> ";" <compound> ;
+		<single>.
+
+<single>:	"if" "(" <expression> ")" <statement> ["else" <statement>];
+		"case" "$\{$" <case-body> "$\}$";
+		"for" "(" <expression> ";" <expression> ";" <expression> ")",
+			<statement>;
+		"while" "(" <expression> ")" <statement>;
+		"do" <expression> "while" "(" <expression> ")";
+		"sum" "(" <expression> ";" <expression> ")" <statment>;
+		"product" "(" <expression> ";" <expression> ")" <statment>;
+		"break";
+		"continue";
+		"return" <expression>;
+		"clear";
+		"load" <expression>;
+		"save" <expression>;
+		"release" <expression>;
+		"show" ["variables" | "functions" | "set" | "all" | <expression>];
+		"set"  ["prompt" | "precision"] [<expression>];
+		<equation>.
+
+<case-body>:	"case" <expression> ":" <compound> <case-body>;
+		 "default:" <compound>
+
+<equation>:	<var> "=" <expression>;
+		<var>"[" <selector> "]" = <expression>;
+		<function> = <input>;
+		<expression>.
+
+<selector>:	<factor> "," <factor>;
+		<factor> ",";
+		"," <factor>.
+
+<expression>:	<term> "+" <expression>;
+		<term> "--" <expression>.		
+
+<term>:		<factor> <operator> <term>.
+
+<factor>	<pre-op> <factor$'$> <post-op>.
+
+<factor$'$>:	<number>;
+		"+" <number>;
+		"--" <number>;
+		"(" <number> ")";
+		<variable>;
+		<variable>"[" <selector> "]";
+		<string>;
+		<matrix>;
+		<function>.
+
+<pre-op>:	"++" | "--{\kern 1pt}--" | "$\sim$" | "!".
+
+<post-op>:	"$\uparrow$" <factor> 
+		| "**" <factor>;
+		"++" | "--{\kern 1pt}--" | "!".		
+
+<matrix>:	"[" <row-list> "]".
+
+<row-list>:	"[" <value-list> "]" [","] <row-list>;
+		"[" <value-list> "]" [","] <row-list>;
+		<value-list>.
+
+<value-list>:	[ <string> ] <expression> "," <value-list>;
+		[ <string> ] <expression>.
+
+<function>:	<variable> "(" <arg-list> ")".
+
+<arg-list>:	$\phi$;
+		<variable> "," <arglist>;
+		"\dots".
+
+<string>:	" `` "  <anything> " '' ".
+
+<number>:	<real-number>;
+		"$\{$" <real-number> "," <real-number> "$\}$";
+		{$\backslash$}b[01][01]+;
+		{$\backslash$}o[07][07]+;
+		\$[0-9A-Fa-f][0-9A-Fa-f]+.
+
+%<real-number>:	[\+--]?[0-9][0-9]+[\.[0-9]+]?[[eE][0-9][0-9]+].
+
+<operator>:	"*" |	 "/"	|     "$\backslash$"	| "\%";
+		"==" |	 "!="	|     "$>$" 		| "$<$"  
+		| "$<$=" | "$>$=";
+		"\ul ="	| "\ul !=" |  "\ul $<$" | "\ul $>$" 
+		| "\ul$<$=" | "\ul$>$=";
+		"\&"	 | "$\vert$"  | "$\uparrow\uparrow$";
+		"\&\&"	| "$\Vert$"  | "\ul$\uparrow$".
+		
+\endgrammar
+\bye
+
diff -r 352ab4bd22f3 -r ba1253cb17a2 slides/src/slides.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/src/slides.tex	Tue Jul 19 02:33:21 2011 +0200
@@ -0,0 +1,137 @@
+\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}