1.1 --- a/slides/notes.txt	Fri Jul 22 04:33:59 2011 +0200
     1.2 +++ b/slides/notes.txt	Fri Jul 22 15:52:20 2011 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  ==> 3
     1.5  
     1.6  5. Gegeben sei ein Programm und dessen Spezifikation, das Problem lautet:
     1.7 -erfüllt jeder Durchlauf des Programms die Spezifikation?
     1.8 +erfüllt jeder Pfad des Programms die Spezifikation?
     1.9  
    1.10  Bevor wir an die Tat schreiten um das Problem zu lösen, 
    1.11  möchte ich eine andere Frage beantworten.
    1.12 @@ -36,7 +36,7 @@
    1.13  Wenn ich sage: "Es ist dunkel." ist es nicht eindeutig, was ich damit ausdrücken möchte.
    1.14  
    1.15  Ich könnte damit meinen "Es ist immer dunkel.", doch das spricht gegen unsere Intuition.
    1.16 -Wir denken als Erstes eher an "Es ist im Moment dunkel.", was auch stimmt, wenn ich damit die Folien referenziere (oder das Wetter draußen).
    1.17 +Wir denken als Erstes eher an "Es ist im Moment dunkel.", was auch stimmt, wenn ich damit mich damit auf die Folien beziehe (oder das Wetter draußen).
    1.18  
    1.19  Wenn wir nach draußen schauen, können wir aus Erfahrung behaupten, dass es "notwendigerweise irgendwann dunkel wird."
    1.20  
    1.21 @@ -83,6 +83,8 @@
    1.22  Hier ist eine Veranschaulichung eines Beispielmodells.
    1.23  Man sieht die Zustände s0 bis si und den Zeitverlauf durch die Relation R.
    1.24  Für jeden Zustand ist die Rückgabe der Bewertungsfunktion als Menge positiver Atome abgebildet.
    1.25 +Wie man sieht, bietet LTL keine gute Grundlage für Science Fiction, weder Zeitreisen noch Parallelwelten sind möglich. 
    1.26 +Luminous Fennell wird in der nächsten Präsentation ein alternatives Modell anbieten, das in dieser Hinsicht etwas interessanter ist und algorithmisch effizienter.
    1.27  
    1.28  ==> 10
    1.29  
    1.30 @@ -105,13 +107,67 @@
    1.31  
    1.32  ==> 12
    1.33  
    1.34 -Hier ist ein Beispielautomat, der auf unendlichem Input arbeitet.
    1.35 -Sieht jemand auf Anhieb welche Sprache dieser Automate akzeptiert?
    1.36 -w1 ist eine Eingabe, der Überstrich soll eine periodische Wiederholung der Sequenz darstellen.
    1.37 -....
    1.38 +Hier ist ein Beispielautomat, der auf unendlichen Eingaben arbeitet.
    1.39 +Sieht jemand auf Anhieb welche Sprache dieser Automat akzeptiert?
    1.40 +w1 ist eine Eingabe, der Überstrich soll eine unendliche periodische Wiederholung der Sequenz darstellen.
    1.41 +Bei dieser Eingabe werden die folgenden Zustände durchlaufen:
    1.42 +- wir starten in q0, lesen zwei b, somit bleiben wir für beide Eingaben in q0
    1.43 +- als nächstes lesen wir ein a, was uns in Zustand q1 versetzt
    1.44 +- danach folgt ein weiteres a, wir bleiben also in q1
    1.45 +- nun wiederholt sich die Sequenz, wir lesen zwei b, passieren dabei den akzeptierenden Zustand q2 und landen in q0, wo das Ganze von vorne beginnt
    1.46 + 
    1.47 +w2 bietet ein ähnliches Beispiel, jedoch pendeln wir diesmal zwischen q1 und q2 nach einer kurzen Phase.
    1.48  
    1.49 +Betrachtet man die grün hervorgehobenen Elemente, sieht man, dass der Zustand q2 gd. unendlich mal passiert wird, wenn die Sequenz ab unendlich mal in der Eingabe vorkommt.
    1.50  
    1.51 +==> 13
    1.52  
    1.53 +Nun wollen wir das Komplement des Automaten bilden.
    1.54 +Naiverweise gehe ich dabei vor, wie beim endlichen Automaten und kehre einfach die Akzeptanzeigenschaften der Zustände um.
    1.55 +Man sieht sofort, dass dies nicht der korrekte Komplementautomat ist, denn er akzeptiert immer noch Eingaben mit unendlichen Sequenzen von ab.
    1.56  
    1.57 +Abbildung (b) zeigt die korrekte Version. In Zustand q0 werden beliebige, endliche Sequenzen von as und bs gelesen. Akzeptiert wird ein Wort nur dann, wenn es ab einem bestimmten Zeitpunkt nur noch as oder bs enthält und das natürlich unendlich oft.
    1.58 +Wir sehen, dass der Komplement-Automat im Gegensatz zu dem Automaten nicht deterministisch ist.
    1.59 +Die Konstruktion dieser sog. Co-Büchi-Automaten wird Stephanie Embgen im Detail erörtern, deswegen werde ich auch nicht weiter darauf eingehen.
    1.60  
    1.61 +==> 14
    1.62  
    1.63 +Halten wir das Ganze formal fest.
    1.64 +Wenn ich von Automaten spreche, meine ich im allgemeinen nicht-deterministische Büchi-Automaten.
    1.65 +Diese bestehen aus : - einem endlichen Alphabet, in unserem Beispiel war das die Menge {a,b}.
    1.66 +- einer endlichen Menge von Zuständen
    1.67 +- einer Menge von Startzuständen, in unserem Beispiel war das lediglich der Zustand q0
    1.68 +- der Übergangsrelation Delta
    1.69 +- und einer endlichen Menge an akzeptierenden Zuständen, im Beispiel war das der Zustand q2, bzw q1 und q2 bei dem Co-Automat
    1.70 +
    1.71 +==> 15
    1.72 +
    1.73 +Ein Pfad eines Automaten auf einem Wort w, ist wie wir schon gesehen haben die unendliche Sequenz der dabei durchlaufenen Zustände.
    1.74 +Der erste Zustand muss ein Element der Startzustände sein.
    1.75 +Um bestimmte Elemente der Sequenz zu referenzieren, betrachten wir die Sequenz als Funktion RHO, wobei RHO(i) uns den durchlaufenen Zustand zum Zeitpunkt i zurückgibt.
    1.76 +
    1.77 +==> 16
    1.78 +
    1.79 +Zur Definition der Akzeptanz bedienen wir uns der Funktion inf, die für einen gegebenen Pfad RHO die Menge an Zuständen zurückgibt, die unendlich mal in RHO durchlaufen werden.
    1.80 +
    1.81 +Basierend darauf sagen wir:
    1.82 +ein Pfad RHO eines Automaten A ist akzeptierend gdw. ein akzeptierender Zustand unendlich oft in RHO vorkommt.
    1.83 +Und dann können wir sagen: ein Automat A akzeptiert ein Wort w gdw. es einen Pfad von A auf w gibt, der akzeptierend ist.
    1.84 +
    1.85 +==> 17
    1.86 +
    1.87 +Die akzeptierte Sprache eines Automaten ist einfach die Menge aller akzeptierten Eingaben.
    1.88 +
    1.89 +==> 18
    1.90 +
    1.91 +Es existiert eine verallgemeinerte Form des Büchi-Automaten, welche bei der Automatenkonstruktion Vorteile bietet.
    1.92 +Der Unterschied liegt in der Akzeptanzbedingung.
    1.93 +Der verallgemeinerte Büchi-Automat definiert diese über eine endliche Menge von Mengen von akzeptierenden Zuständen.
    1.94 +Ein Pfad RHO eines solchen Automaten ist akzeptierend gdw. es einen Zustand aus der jeweiligen Menge von akzeptierenden Zuständen gibt, der unendlich oft in RHO vorkommt.
    1.95 +Wenn man sich die Definition anschaut, wird es offensichtlich, dass die akzeptierte Sprache eines verallgemeinerten Automaten equivalent ist zu der Schnittmenge der akzeptierten Sprachen von k Büchi-Automaten. 
    1.96 +
    1.97 +==> 19
    1.98 +
    1.99 +
   1.100 +
   1.101 +

     2.1 --- a/slides/src/slides.tex	Fri Jul 22 04:33:59 2011 +0200
     2.2 +++ b/slides/src/slides.tex	Fri Jul 22 15:52:20 2011 +0200
     2.3 @@ -500,6 +500,32 @@
     2.4  \end{frame}
     2.5  
     2.6  \begin{frame}
     2.7 +\frametitle{Automata Construction}
     2.8 +\framesubtitle{Formula automata}
     2.9 +\begin{center}
    2.10 +Model $\M_\varphi$ for formula $\varphi$\\
    2.11 +$\Downarrow$\\
    2.12 +Closure $CL(\varphi)$ of $\varphi$\\
    2.13 +$\Downarrow$\\
    2.14 +Automaton $\A_\varphi$ for $\varphi$\\
    2.15 +\vspace{20pt}
    2.16 +\textcolor{red}{On-the-fly methods} \`a la Gerth et al.
    2.17 +\end{center}
    2.18 +\end{frame}
    2.19 +
    2.20 +\begin{frame}
    2.21 +\frametitle{Automata Construction}
    2.22 +\framesubtitle{System automata}
    2.23 +\begin{center}
    2.24 +Model $\M_\varphi$ for formula $\varphi$\\
    2.25 +$\Downarrow$\\
    2.26 +Closure $CL(\varphi)$ of $\varphi$\\
    2.27 +$\Downarrow$\\
    2.28 +Automaton $\A_\varphi$ for $\varphi$
    2.29 +\end{center}
    2.30 +\end{frame}
    2.31 +
    2.32 +\begin{frame}
    2.33  \frametitle{Model Checking}
    2.34  \framesubtitle{Definition}
    2.35  \begin{thm:model checking}