1.1 --- a/slides/notes.txt	Fri Jul 22 23:39:42 2011 +0200
     1.2 +++ b/slides/notes.txt	Mon Jul 25 23:56:52 2011 +0200
     1.3 @@ -1,15 +1,13 @@
     1.4 -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 den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking.
     1.6  
     1.7 -Was ich ihnen erzählen werde, wird die Meisten von euch bei der Bearbeitung des Themas in irgendeiner Form tangiert haben. 
     1.8 -
     1.9 -Meine Präsentation soll einen Überblick geben über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings.
    1.10 +Meine Präsentation soll einen Überblick über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings geben.
    1.11  
    1.12  ==> 2
    1.13  
    1.14 -PHI ist erfüllt im Modell M, oder Modell M modelliert PHI.
    1.15 +Modell M erfüllt PHI.
    1.16  Das ist der Kern unserer Bemühungen. 
    1.17  Doch was bedeutet das?
    1.18 -Wir übersetzen das in die Problemstellung der Verifikation von Systemen.
    1.19 +Wir übersetzen das in die Problemstellung der Verifikation.
    1.20  
    1.21  ==> 3
    1.22  
    1.23 @@ -29,6 +27,10 @@
    1.24  Die Industrie investiert viel Zeit und Geld in die Verifikation sicherheitskritischer Systeme und der Kernkomponenten anderer Systeme.
    1.25  Die automatisierte Verifikation hat bereits in der Chip-Verifikation ihre praktische Anwendbarkeit gezeigt und ist in der Softwareindustrie stark gefragt.
    1.26  
    1.27 +==> 4(2)
    1.28 +
    1.29 +Hier sind einige promitente Vertreter der Industry, die Verifikationsmethoden einsetzten.
    1.30 +
    1.31  Also fangen wir an.
    1.32  
    1.33  ==> 5
    1.34 @@ -67,6 +69,14 @@
    1.35  Die Erweiterung sind das kalligraphische X, welches für "Next" steht und das "Until" aus dem Beispiel.
    1.36  Diese Syntaxdefinition bildet das Fundament für weitere abgeleitete Verknüpfungen.
    1.37  
    1.38 +==> 7(2)
    1.39 +
    1.40 +Schauen wir diese kurz an.
    1.41 +Eine klassische Ableitung für "Wahr" bietet sich durch p oder nicht p an.
    1.42 +Andere Ableitungen folgen analog.
    1.43 +Interessant sind hierbei wieder die modalen Verknüpfungen, Diamand und Box.
    1.44 +Diamant steht für eine Eventualität und Box steht für eine Notwendigkeit.
    1.45 +
    1.46  ==> 8
    1.47  
    1.48  Wir interpretieren LTL-Formeln über unendliche Sequenzen von Aussagen. 
    1.49 @@ -134,7 +144,8 @@
    1.50  
    1.51  Halten wir das Ganze formal fest.
    1.52  Wenn ich von Automaten spreche, meine ich im allgemeinen nicht-deterministische Büchi-Automaten.
    1.53 -Diese bestehen aus : - einem endlichen Alphabet, in unserem Beispiel war das die Menge {a,b}.
    1.54 +Diese bestehen aus: 
    1.55 +- einem endlichen Alphabet, in unserem Beispiel war das die Menge {a,b}.
    1.56  - einer endlichen Menge von Zuständen
    1.57  - einer Menge von Startzuständen, in unserem Beispiel war das lediglich der Zustand q0
    1.58  - der Übergangsrelation Delta
    1.59 @@ -169,7 +180,22 @@
    1.60  ==> 19
    1.61  
    1.62  Wir kennen nun die Sprache zur Spezifikation von Systemeigenschaften und wir haben Automaten kennengelernt, die auf unendlichen Eingaben arbeiten. 
    1.63 +Für die automaten-theoretische Methode müssen einen Automaten konstruieren anhand einer Systemspezifikation in der linearen temporalen Logik.
    1.64 +In meiner Arbeit geschieht dies über den sog. Fischer-Ladner-Abschluss.
    1.65 +In der Arbeit von Rob Gerth wird eine on-the-fly Konstruktion der Produktautomaten vorgestellt.
    1.66 +Darauf wird Christian Schilling heute Nachmittag genauer eingehen.
    1.67 +
    1.68 +==> 20
    1.69 +
    1.70 +==> 21
    1.71 +
    1.72 +==> 22
    1.73 +
    1.74  Erinnern wir uns and die Problembeschreibung vom Anfang.
    1.75 +Übersetzt in die Automatentheorie bedeutet das:
    1.76 +Ein System entspricht der Spezifikation, wenn die akzeptierte Sprache des Systemautomaten in der akzeptierten Sprache des Formelautomaten enthalten ist.
    1.77 +Eine mengentheoretische Umformung gibt uns folgende Form:
    1.78 +Ein System entspricht der Spezifikation, wenn der Schnitt der akzeptierten Sprache des Systemautomaten mit der akzeptierten Sprache des Automaten für die negierte Formel gleich der leeren Menge ist.
    1.79  
    1.80  
    1.81