1.1 --- a/slides/notes.txt	Mon Jul 25 23:56:52 2011 +0200
     1.2 +++ b/slides/notes.txt	Wed Jul 27 11:24:57 2011 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  ==> 4(2)
     1.6  
     1.7 -Hier sind einige promitente Vertreter der Industry, die Verifikationsmethoden einsetzten.
     1.8 +Hier sind einige promitente Vertreter der Industrie, die Verifikationsmethoden einsetzten.
     1.9  
    1.10  Also fangen wir an.
    1.11  
    1.12 @@ -59,7 +59,7 @@
    1.13  
    1.14  Dabei sind p0 und p1 Elementaraussagen, sog. Atome, die entsprechend für "Es is dunkel" und "Es gibt licht" stehen.
    1.15  Die neue Verknüpfung nennen wir trivialerweise "until" und notieren sie mit dem kalligraphischen U.
    1.16 -Halten wir das formal fest.
    1.17 +Halten wir die Syntax formal fest.
    1.18  
    1.19  ==> 7
    1.20  
    1.21 @@ -187,8 +187,18 @@
    1.22  
    1.23  ==> 20
    1.24  
    1.25 +Die Konstruktion des Systemautomaten ist eindeutig einfacher.
    1.26 +Sei das Programm in dieser Form gegeben, mit einer Menger von Zuständen, einer Startzustand, einer Übergangsrelation und der Bewertungsfunktion, welche für jeden Zustand die Menge an gültigen Atomen liefert.
    1.27 +
    1.28 +Eine Berechnung des Programms ergibt einen Pfad, der aus der Sequenz der Mengen besteht, die die Bewertungsfunktionen für den jeweiligen Zustand zurückgibt.
    1.29 +
    1.30 +Daraus konstruieren wir den Systemautomaten.
    1.31 +Zu beachten ist, dass die Menge der akzeptierenden Zustände gleich der Menge der Zustände ist, somit ist jeder Pfad des Automaten akzeptierend.
    1.32 +
    1.33  ==> 21
    1.34  
    1.35 +Daraus folgt direkt folgender Satz: die akzeptierte Sprache eines Systemautomaten ist gleich der Menge aller Pfade des Automaten.
    1.36 +
    1.37  ==> 22
    1.38  
    1.39  Erinnern wir uns and die Problembeschreibung vom Anfang.
    1.40 @@ -197,5 +207,27 @@
    1.41  Eine mengentheoretische Umformung gibt uns folgende Form:
    1.42  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.43  
    1.44 +Die graphentheoretische Methode erlaubt uns nun die Produktautomaten als Graphen zu interpretieren und das Problem durch die Bildung der Zusammenhangskomponente zu lösen.
    1.45 +Die effiziente on-the-fly Methode sucht stattdessen iterativ nach Zyklen.
    1.46  
    1.47 +Wir wissen wie man den Systemautomaten konstruiert und dessen akzeptierte Sprache bestimmt.
    1.48 +Wir wissen wie man Spezifikationen mit Hilfe der linearen temporalen Logik beschreibt.
    1.49 +In den folgenden Vorträgen werden wir u.a. erfahren, wie man den Formelautomaten bildet und effiziente Methoden kennenlernen, wie man die sog. Zustandsexplosion vermeidet.
    1.50  
    1.51 +==> 23
    1.52 +
    1.53 +Zum Schluss habe eine kleine Auswahl an Arbeiten vorbereitet.
    1.54 +Meine Arbeit basiert hauptsächlich auf Madhavan Mukund's Veröffentlichung, wobei ich einige Definitionen von Vardi's Paper bevorzugt habe.
    1.55 +Wie bereits erwähnt beschreibt die Arbeit von Rob Gerth und den anderen die on-the-fly Methode.
    1.56 +Das Handbook of Modal Logik kann ich allen empfehlen die sich mehr mit modalen Logiken beschäftigen wollen.
    1.57 +
    1.58 +==> 24
    1.59 +
    1.60 +Und alle, die eine sehr motivierende, kurze und pregnante Einführung in das präsentierte Thema lesen möchten kann ich nur Vardi's Automated Verification: Graphs, Logic and Automata empfehlen.
    1.61 +
    1.62 +Ich hoffe mein Vortrag hat einen Überblick über die Thematik geboten und freue mich auf die weiteren Vorträge, die von mir hinterlassene Lücken füllen oder ganz andere Aspekte einbringen.
    1.63 +
    1.64 +Vielen Dank!
    1.65 +
    1.66 +
    1.67 +