1.1 --- a/slides/notes.txt	Fri Jul 22 20:49:15 2011 +0200
     1.2 +++ b/slides/notes.txt	Fri Jul 22 23:01:19 2011 +0200
     1.3 @@ -1,19 +1,19 @@
     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 +Guten Morgen! Mein Name ist Eugen Sawin und ich werde jetzt den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking.
     1.6  
     1.7 -2. Was ich ihnen erzählen werde, wird die Meisten von euch bei der Bearbeitung des Themas in irgendeiner Form tangiert haben. 
     1.8 +Was ich ihnen erzählen werde, wird die Meisten von euch bei der Bearbeitung des Themas in irgendeiner Form tangiert haben. 
     1.9  
    1.10 -3. Meine Präsentation soll einen Überblick geben über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings.
    1.11 +Meine Präsentation soll einen Überblick geben über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings.
    1.12  
    1.13  ==> 2
    1.14  
    1.15 -4. PHI ist erfüllt in Modell M, oder Modell M modelliert PHI.
    1.16 +PHI ist erfüllt im Modell M, oder Modell M modelliert PHI.
    1.17  Das ist der Kern unserer Bemühungen. 
    1.18  Doch was bedeutet das?
    1.19  Wir übersetzen das in die Problemstellung der Verifikation von Systemen.
    1.20  
    1.21  ==> 3
    1.22  
    1.23 -5. Gegeben sei ein Programm und dessen Spezifikation, das Problem lautet:
    1.24 +Gegeben sei ein Programm und dessen Spezifikation, das Problem lautet:
    1.25  erfüllt jeder Pfad des Programms die Spezifikation?
    1.26  
    1.27  Bevor wir an die Tat schreiten um das Problem zu lösen, 
    1.28 @@ -63,7 +63,7 @@
    1.29  
    1.30  Wir definieren die Syntax der linearen temporalen Logik mit Hilfe dieser Produktionen in Backus-Naur-Form.
    1.31  Somit ist eine LTL-Formel entweder ein aussagenlogisches Atom, eine negierte Formel oder eine Disjunktion zweier Formeln. 
    1.32 -Das kannten wir bereits aus der Aussagenlogik.
    1.33 +Das kennen wir bereits aus der Aussagenlogik.
    1.34  Die Erweiterung sind das kalligraphische X, welches für "Next" steht und das "Until" aus dem Beispiel.
    1.35  Diese Syntaxdefinition bildet das Fundament für weitere abgeleitete Verknüpfungen.
    1.36  
    1.37 @@ -168,6 +168,8 @@
    1.38  
    1.39  ==> 19
    1.40  
    1.41 +Wir kennen nun die Sprache zur Spezifikation von Systemeigenschaften und wir haben Automaten kennengelernt, die auf unendlichen Eingaben arbeiten. 
    1.42 +Erinnern wir uns and die Problembeschreibung vom Anfang.
    1.43  
    1.44  
    1.45  

     2.1 --- a/slides/src/slides.tex	Fri Jul 22 20:49:15 2011 +0200
     2.2 +++ b/slides/src/slides.tex	Fri Jul 22 23:01:19 2011 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  
     2.5  \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
     2.6  \usepackage{pifont}
     2.7 +\usepackage{multicol}
     2.8  \usepackage{xcolor}
     2.9  \usepackage{ulem}
    2.10  \usepackage{graphics}
    2.11 @@ -45,7 +46,8 @@
    2.12  \newtheorem*{def:general automata}{Generalised automaton}
    2.13  \newtheorem*{def:general acceptance}{Acceptance}
    2.14  \newtheorem*{def:syntax}{Syntax}
    2.15 -
    2.16 +\newtheorem*{def:program}{Program}
    2.17 +\newtheorem*{def:program automaton}{System automaton}
    2.18  
    2.19  \newtheorem*{def:vocabulary}{Vocabulary}
    2.20  \newtheorem*{def:frames}{Frame}
    2.21 @@ -520,58 +522,94 @@
    2.22  $\Downarrow$\\
    2.23  Automaton $\A_\varphi$ for $\varphi$\\
    2.24  \vspace{20pt}
    2.25 -\textcolor{red}{On-the-fly methods} \`a la Gerth et al.
    2.26 +\visible<2>{\textcolor{red}{On-the-fly methods} \`a la Gerth et al.}
    2.27  \end{center}
    2.28  \end{frame}
    2.29  
    2.30  \begin{frame}
    2.31  \frametitle{Automata Construction}
    2.32 -\framesubtitle{System automata}
    2.33 -\begin{center}
    2.34 -Model $\M_\varphi$ for formula $\varphi$\\
    2.35 -$\Downarrow$\\
    2.36 -Closure $CL(\varphi)$ of $\varphi$\\
    2.37 -$\Downarrow$\\
    2.38 -Automaton $\A_\varphi$ for $\varphi$
    2.39 -\end{center}
    2.40 +\framesubtitle{System automata 1/2}
    2.41 +\begin{def:program}
    2.42 +Given a program $P = (S_P, s_0, R, V)$:
    2.43 +\begin{itemize}
    2.44 +\begin{multicols}{2}
    2.45 +\item $S$ is the set of possible states.
    2.46 +\item $s_0$ is the initial state.
    2.47 +\item $R : S \times \Prop \times S$ is the transition relation.
    2.48 +\item $V : S \to 2^\Prop$ is a valuation function.
    2.49 +\end{multicols}
    2.50 +\end{itemize}
    2.51 +A \emph{computation} of $P$ is a run $\rho = (V(s_0), V(s_1), ...)$. 
    2.52 +\end{def:program}
    2.53 +
    2.54 +\begin{def:program automaton}
    2.55 +We construct automaton $\A_P = (\Sigma, S, S_0, \Delta, F)$ for program $P$:
    2.56 +\begin{itemize}
    2.57 +\begin{multicols}{2}
    2.58 +\item $\Sigma = 2^\Prop$
    2.59 +\item $S = S_P$
    2.60 +\item $S_0 = \{s_0\}$
    2.61 +\item $F = S$
    2.62 +\end{multicols}
    2.63 +\vspace{-1.1em}
    2.64 +\item $\Delta = \{(s, V(s), s') \mid \exists{a \in \Prop}: (s, a, s') \in R\}$
    2.65 +\end{itemize}
    2.66 +\end{def:program automaton}
    2.67  \end{frame}
    2.68  
    2.69  \begin{frame}
    2.70 -\frametitle{Model Checking}
    2.71 -\framesubtitle{Definition}
    2.72 -\begin{thm:model checking}
    2.73 -\label{thm:model checking}
    2.74 -Let $\A_P$ be the automaton for program $P$ and let $\A_\varphi$ be the automaton for formula $\varphi$.\\
    2.75 -P satisfies $\varphi$ iff:
    2.76 -\begin{itemize}
    2.77 -\item $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$.
    2.78 -\item $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.
    2.79 -\end{itemize}
    2.80 -\end{thm:model checking}
    2.81 +\frametitle{Automata Construction}
    2.82 +\framesubtitle{System automata 2/2}
    2.83 +\begin{prop:computation set=language}
    2.84 +Let $\A_P = (\Sigma, S, S_0, \Delta, F)$, note that $F = S$, it follows:
    2.85 +\[L_\omega(\A_P) = \{\rho \mid \rho \text{ is a run of } \A_P\}\]
    2.86 +\end{prop:computation set=language}
    2.87 +\end{frame}
    2.88 +
    2.89 +\begin{frame}
    2.90 +\frametitle{Verification}
    2.91 +\begin{center}
    2.92 +Given a program $P$ and specification $\varphi$:\\
    2.93 +\colorbox{black}{\makebox(150,10){\color{white}
    2.94 +\only<1>{does every run of $P$ satisfy $\varphi$?}
    2.95 +\only<2>{$L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$}
    2.96 +\only<3>{$L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$}}}
    2.97 +\end{center}
    2.98  \end{frame}
    2.99  
   2.100  \begin{frame}[allowframebreaks]
   2.101  \frametitle<presentation>{Literature}    
   2.102  \begin{thebibliography}{10}    
   2.103  
   2.104 -\beamertemplatearticlebibitems
   2.105 +%\beamertemplatearticlebibitems
   2.106  \bibitem{ref:ltl&büchi}
   2.107  Madhavan Mukund.
   2.108  \newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
   2.109  \newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
   2.110    
   2.111 -\beamertemplatearticlebibitems
   2.112 +%\beamertemplatearticlebibitems
   2.113  \bibitem{ref:alternating verification}
   2.114  Moshe Y. Vardi.
   2.115  \newblock {\em Alternating Automata and Program Verification}.
   2.116  \newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
   2.117  
   2.118 +\bibitem{ref:on-the-fly verification} 
   2.119 +Rob Gerth, Doron Peled, Moshe Y. Vardi and Pierre Wolper.
   2.120 +\newblock {\em Simple On-the-fly Automatic Verification of Linear Temporal Logic}.
   2.121 +\newblock Proceeding IFIO/WG6.1 Symposium on Protocol Specification, Testing and Verification, Warsaw, 1995.
   2.122 +
   2.123  \beamertemplatebookbibitems
   2.124  \bibitem{ref:handbook}
   2.125 -Patrick Blackburn and Frank Wolter and Johan van Benthem.
   2.126 +Patrick Blackburn, Frank Wolter and Johan van Benthem.
   2.127  \newblock {\em Handbook of Modal Logic}.
   2.128  \newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.
   2.129  
   2.130 +\beamertemplatearticlebibitems
   2.131 +\bibitem{ref:automated verification} 
   2.132 +Moshe Y. Vardi.
   2.133 +\newblock {\em Automated Verification: Graphs, Logic and Automata}.
   2.134 +\newblock Proceeding of the International Joint Conference on Artificial Intelligence, Acapulco, 2003.
   2.135 +
   2.136  \end{thebibliography}
   2.137  \end{frame}
   2.138