1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/slides/notes.txt	Fri Jul 22 01:22:59 2011 +0200
     1.3 @@ -0,0 +1,2 @@
     1.4 +1. Guten Morgen! Mein Name ist Eugen Sawin und ich werde jetzt den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking.
     1.5 +

     2.1 --- a/slides/src/slides.tex	Thu Jul 21 14:52:03 2011 +0200
     2.2 +++ b/slides/src/slides.tex	Fri Jul 22 01:22:59 2011 +0200
     2.3 @@ -9,13 +9,13 @@
     2.4  \usepackage{pifont}
     2.5  \usepackage{xcolor}
     2.6  \usepackage{ulem}
     2.7 -\usepackage{graphicx}
     2.8 +\usepackage{graphics}
     2.9  \usepackage{tikz}
    2.10  \usetikzlibrary{automata}
    2.11  \usepackage{subfigure}
    2.12  
    2.13  \renewcommand{\emph}{\textit}
    2.14 -\renewcommand{\em}{\textit}
    2.15 +\renewcommand{\em}{\it}
    2.16  
    2.17  \newcommand{\cross}{\ding{55}}
    2.18  \newcommand{\M}{\mathcal{M}}
    2.19 @@ -86,14 +86,46 @@
    2.20  
    2.21  \begin{document}
    2.22  \frame{\titlepage}
    2.23 +
    2.24  \begin{frame}
    2.25  \frametitle{Motivation}
    2.26 -\tableofcontents[currentsection]
    2.27 +\framesubtitle{Model Checking}
    2.28 +\begin{center}
    2.29 +%\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}
    2.30 +\only<1>{\[\M \models \varphi\]}
    2.31 +\only<2->{Given a program $P$ and specification $\varphi$:\\
    2.32 +\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}}
    2.33 +\end{center}
    2.34 +\end{frame}
    2.35 +
    2.36 +\begin{frame}
    2.37 +\frametitle{Motivation}
    2.38 +\begin{figure}
    2.39 +\centering
    2.40 +\subfigure{\includegraphics[width=100pt,height=70pt]{images/intel.jpg}}
    2.41 +\subfigure{\includegraphics[width=100pt,height=70pt]{images/airbag.jpg}}
    2.42 +\subfigure{\includegraphics[width=100pt,height=70pt]{images/atc.jpg}}
    2.43 +\end{figure}
    2.44  \end{frame}
    2.45  
    2.46  \begin{frame}
    2.47  \frametitle{Infinity}
    2.48 -\framesubtitle{A bit more information about this}
    2.49 +\framesubtitle{Word as function}
    2.50 +\begin{figure}
    2.51 +\centering
    2.52 +\begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth   
    2.53 +    ,accepting/.style={fill, gray!50!black, text=white}]
    2.54 +\node[state, initial, initial text=] (s_0) {$a$};
    2.55 +\node[state] (s_1) [right of= s_0] {$b$};
    2.56 +\node[state] (s_2) [right of= s_1] {$a$};
    2.57 +\node[state] (s_i) [right of= s_2] {$a$};
    2.58 +\path[->] 
    2.59 +(s_0) edge node {} (s_1) 
    2.60 +(s_1) edge node {} (s_2);
    2.61 +\path[dashed,->] 
    2.62 +(s_2) edge node {} (s_i); 
    2.63 +\end{tikzpicture}
    2.64 +\end{figure}
    2.65  \end{frame}
    2.66  
    2.67  \begin{frame}
    2.68 @@ -258,8 +290,7 @@
    2.69              }\\
    2.70  \color{black}  
    2.71  \vspace{20pt}
    2.72 -Accepts all inputs with infinite occurrences of $a$ or $b$.\\
    2.73 -Does \emph{not} accept inputs with infinite occurrences of both $a$ and $b$.
    2.74 +Accepts all inputs with finite many $ab$.
    2.75  }
    2.76  %\caption{Automata from Example \ref{ex:automaton}}
    2.77  \end{figure}
    2.78 @@ -295,6 +326,8 @@
    2.79  \item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$.
    2.80  \end{itemize}
    2.81  \end{def:automata runs}
    2.82 +\visible<2->{\[w_1 = \overline{\textcolor{green}{b}ba\textcolor{green}{a}} \implies \rho_1 = q_0q_0\overline{q_0q_1q_1\textcolor{green}{q_2}}\]
    2.83 +\[w_2 = bb\overline{\textcolor{green}{ab}} \implies \rho_2 = q_0q_0\overline{q_1\textcolor{green}{q_2}}\]}
    2.84  \end{frame}
    2.85  
    2.86  \begin{frame}
    2.87 @@ -379,7 +412,7 @@
    2.88  \color{white}
    2.89  \colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\
    2.90  \visible<2->{
    2.91 -\colorbox{black}{\makebox(50,10){$d$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$l$}}}
    2.92 +\colorbox{black}{\makebox(50,10){$p_0$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$p_1$}}}
    2.93  }
    2.94  \end{center}
    2.95  \end{frame}
    2.96 @@ -460,8 +493,27 @@
    2.97  
    2.98  \begin{frame}
    2.99  \frametitle{Model Checking}
   2.100 -\framesubtitle{A bit more information about this}
   2.101 +\framesubtitle{Definition 1/2}
   2.102 +\begin{center}
   2.103 +%\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}
   2.104 +\only<1>{\[\M \models \varphi\]}
   2.105 +\only<2->{Given a program $P$ and specification $\varphi$:\\
   2.106 +\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}}
   2.107 +\end{center}
   2.108 +\end{frame}
   2.109  
   2.110 +\begin{frame}
   2.111 +\frametitle{Model Checking}
   2.112 +\framesubtitle{Definition 2/2}
   2.113 +\begin{thm:model checking}
   2.114 +\label{thm:model checking}
   2.115 +Let $\A_P$ be the automaton for program $P$ and let $\A_\varphi$ be the automaton for formula $\varphi$.\\
   2.116 +P satisfies $\varphi$ iff:
   2.117 +\begin{itemize}
   2.118 +\item $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$.
   2.119 +\item $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.
   2.120 +\end{itemize}
   2.121 +\end{thm:model checking}
   2.122  \end{frame}
   2.123  
   2.124  \begin{frame}