sawine@75: Guten Morgen! Mein Name ist Eugen Sawin und ich werde den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking.
sawine@66: 
sawine@75: Meine Präsentation soll einen Überblick über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings geben.
sawine@67: 
sawine@67: ==> 2
sawine@67: 
sawine@75: Modell M erfüllt PHI.
sawine@67: Das ist der Kern unserer Bemühungen. 
sawine@67: Doch was bedeutet das?
sawine@75: Wir übersetzen das in die Problemstellung der Verifikation.
sawine@67: 
sawine@67: ==> 3
sawine@67: 
sawine@72: Gegeben sei ein Programm und dessen Spezifikation, das Problem lautet:
sawine@68: erfüllt jeder Pfad des Programms die Spezifikation?
sawine@67: 
sawine@67: Bevor wir an die Tat schreiten um das Problem zu lösen, 
sawine@67: möchte ich eine andere Frage beantworten.
sawine@67: 
sawine@67: Wieso das Ganze? Was ist der praktische Nutzen der Verifikation?
sawine@67: 
sawine@67: ==> 4
sawine@67: 
sawine@67: Hard- und Softwaresysteme haben alle Bereiche der Industrie und damit auch unseren Alltag durchdrungen.
sawine@67: Sie bilden die Infrastruktur unserer Kommunikation, bieten Sicherheit und retten sogar Leben.
sawine@67: Und sie werden immer komplexer.
sawine@67: Die Industrie investiert viel Zeit und Geld in die Verifikation sicherheitskritischer Systeme und der Kernkomponenten anderer Systeme.
sawine@67: Die automatisierte Verifikation hat bereits in der Chip-Verifikation ihre praktische Anwendbarkeit gezeigt und ist in der Softwareindustrie stark gefragt.
sawine@67: 
sawine@75: ==> 4(2)
sawine@75: 
sawine@76: Hier sind einige promitente Vertreter der Industrie, die Verifikationsmethoden einsetzten.
sawine@75: 
sawine@67: Also fangen wir an.
sawine@67: 
sawine@67: ==> 5
sawine@67: 
sawine@67: Wenn ich sage: "Es ist dunkel." ist es nicht eindeutig, was ich damit ausdrücken möchte.
sawine@67: 
sawine@67: Ich könnte damit meinen "Es ist immer dunkel.", doch das spricht gegen unsere Intuition.
sawine@68: 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).
sawine@67: 
sawine@67: Wenn wir nach draußen schauen, können wir aus Erfahrung behaupten, dass es "notwendigerweise irgendwann dunkel wird."
sawine@67: 
sawine@67: Unsere Sprache erlaubt es uns auch kausale Zusammenhänge zu bilden, wie z.B. "Es ist dunkel, bis Jemand das Licht an macht."
sawine@67: 
sawine@67: Wir sehen, dass die natürliche Sprache nicht eindeutig ist und somit zur formalen Beschreibung ungeeignet.
sawine@67: Wie können wir unsere Sprache zähmen, ohne die Ausdruckskraft zu verlieren.
sawine@67: Nun, als Ersten machen wir das Licht wieder an!
sawine@67: 
sawine@67: ==> 6
sawine@67: 
sawine@67: Nehmen wir den letzten Satz in einer allgemeineren Form als Beispiel.
sawine@67: Dieser Satz sollte allgemeingültig sein. 
sawine@67: Wie können wir die Aussage dieses Satzes formal festhalten?
sawine@67: Wir bedienen uns der Aussagenlogik und erweitern diese um eine weitere Verknüpfung.
sawine@67: 
sawine@67: ==> 6(2)
sawine@67: 
sawine@67: Dabei sind p0 und p1 Elementaraussagen, sog. Atome, die entsprechend für "Es is dunkel" und "Es gibt licht" stehen.
sawine@67: Die neue Verknüpfung nennen wir trivialerweise "until" und notieren sie mit dem kalligraphischen U.
sawine@76: Halten wir die Syntax formal fest.
sawine@67: 
sawine@67: ==> 7
sawine@67: 
sawine@67: Wir definieren die Syntax der linearen temporalen Logik mit Hilfe dieser Produktionen in Backus-Naur-Form.
sawine@67: Somit ist eine LTL-Formel entweder ein aussagenlogisches Atom, eine negierte Formel oder eine Disjunktion zweier Formeln. 
sawine@72: Das kennen wir bereits aus der Aussagenlogik.
sawine@67: Die Erweiterung sind das kalligraphische X, welches für "Next" steht und das "Until" aus dem Beispiel.
sawine@67: Diese Syntaxdefinition bildet das Fundament für weitere abgeleitete Verknüpfungen.
sawine@67: 
sawine@75: ==> 7(2)
sawine@75: 
sawine@75: Schauen wir diese kurz an.
sawine@75: Eine klassische Ableitung für "Wahr" bietet sich durch p oder nicht p an.
sawine@75: Andere Ableitungen folgen analog.
sawine@75: Interessant sind hierbei wieder die modalen Verknüpfungen, Diamand und Box.
sawine@75: Diamant steht für eine Eventualität und Box steht für eine Notwendigkeit.
sawine@75: 
sawine@67: ==> 8
sawine@67: 
sawine@67: Wir interpretieren LTL-Formeln über unendliche Sequenzen von Aussagen. 
sawine@67: Die Sequenz entspricht der zeitlichen Abfolge von Ereignissen in einem vorwärts gerichteteten diskreten Zeitverlauf.
sawine@67: Diese Interpretation heißt die Kripke-Semantik.
sawine@67: Das Kripke-Modell der LTL-Semantik besteht aus einer abzählbaren Menge von Zuständen, verknüpft duch die Erreichbarkeitsrelation und der Bewertungsfunktion V.
sawine@67: Da wir nur lineare Abfolgen betrachten, fällt die Erreichbarkeitsrelation einfach aus.
sawine@67: Von einem beliebigen Zustand ist jeweils nur dessen Nachfolger erreichbar.
sawine@67: Die Bewertungsfunktion liefert uns die Menge aller gültigen Atome für einen bestimmten Zustand.
sawine@67: Intuitiv sagt man, ein Atom p ist wahr zum Zeitpunkt i gdw. p in der Menge V(i) ist.
sawine@67: 
sawine@67: ==> 9
sawine@67: 
sawine@67: Hier ist eine Veranschaulichung eines Beispielmodells.
sawine@67: Man sieht die Zustände s0 bis si und den Zeitverlauf durch die Relation R.
sawine@67: Für jeden Zustand ist die Rückgabe der Bewertungsfunktion als Menge positiver Atome abgebildet.
sawine@68: Wie man sieht, bietet LTL keine gute Grundlage für Science Fiction, weder Zeitreisen noch Parallelwelten sind möglich. 
sawine@68: Luminous Fennell wird in der nächsten Präsentation ein alternatives Modell anbieten, das in dieser Hinsicht etwas interessanter ist und algorithmisch effizienter.
sawine@67: 
sawine@67: ==> 10
sawine@67: 
sawine@67: Die Erfüllbarkeit einer Formel zu einem Zeitpunkt i im Modell M ist folgendermaßen definiert:
sawine@67: - ein Atom p ist erfüllbar gdw. und p in der Menge V(i) ist
sawine@67: - eine negierte Formel PHI ist erfüllbar gdw. PHI nicht erfüllbar ist
sawine@67: - eine Disjunktion von PHI und PSI ist erfüllbar gdw. PHI oder PSI erfüllbar ist
sawine@67: - Next PHI ist erfüllbar gdw. PHI im darauffolgenden Zeitpunkt erfüllbar ist
sawine@67: - PHI Until PSI ist erfüllbar gdw. es einen Zeitpunkt k gibt, ab dem PSI erfüllbar ist und für alle Zeitpunkte vor k PHI erfüllbar ist.
sawine@67: 
sawine@67: Mit Hilfe der linearen temporalen Logik lassen sich Programmeigenschaften und derren zeitliche Abhängigkeiten genau beschreiben.
sawine@67: Als nächstes werden wir uns den Automaten widmen, die auf unendlichen Eingaben operieren.
sawine@67: 
sawine@67: ==> 11
sawine@67: 
sawine@67: Wieso sind unsere Eingaben überhaupt unendlich?
sawine@67: Im Gegensatz zu terminierenden Programmen sind reaktive Systeme fortlaufende Prozesse.
sawine@67: Ein mal initiiert, verbleiben reaktive Systeme in einem aktiven Zustand und reagieren auf nebenläufige Eingaben.
sawine@67: Theoretisch betrachtet, arbeiten solche Systeme somit auf unendlichen Eingabesequenzen.
sawine@67: 
sawine@67: ==> 12
sawine@67: 
sawine@68: Hier ist ein Beispielautomat, der auf unendlichen Eingaben arbeitet.
sawine@68: Sieht jemand auf Anhieb welche Sprache dieser Automat akzeptiert?
sawine@68: w1 ist eine Eingabe, der Überstrich soll eine unendliche periodische Wiederholung der Sequenz darstellen.
sawine@68: Bei dieser Eingabe werden die folgenden Zustände durchlaufen:
sawine@68: - wir starten in q0, lesen zwei b, somit bleiben wir für beide Eingaben in q0
sawine@68: - als nächstes lesen wir ein a, was uns in Zustand q1 versetzt
sawine@68: - danach folgt ein weiteres a, wir bleiben also in q1
sawine@68: - 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
sawine@68:  
sawine@68: w2 bietet ein ähnliches Beispiel, jedoch pendeln wir diesmal zwischen q1 und q2 nach einer kurzen Phase.
sawine@67: 
sawine@68: 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.
sawine@67: 
sawine@68: ==> 13
sawine@67: 
sawine@68: Nun wollen wir das Komplement des Automaten bilden.
sawine@68: Naiverweise gehe ich dabei vor, wie beim endlichen Automaten und kehre einfach die Akzeptanzeigenschaften der Zustände um.
sawine@68: Man sieht sofort, dass dies nicht der korrekte Komplementautomat ist, denn er akzeptiert immer noch Eingaben mit unendlichen Sequenzen von ab.
sawine@67: 
sawine@68: 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.
sawine@68: Wir sehen, dass der Komplement-Automat im Gegensatz zu dem Automaten nicht deterministisch ist.
sawine@68: Die Konstruktion dieser sog. Co-Büchi-Automaten wird Stephanie Embgen im Detail erörtern, deswegen werde ich auch nicht weiter darauf eingehen.
sawine@67: 
sawine@68: ==> 14
sawine@67: 
sawine@68: Halten wir das Ganze formal fest.
sawine@68: Wenn ich von Automaten spreche, meine ich im allgemeinen nicht-deterministische Büchi-Automaten.
sawine@75: Diese bestehen aus: 
sawine@75: - einem endlichen Alphabet, in unserem Beispiel war das die Menge {a,b}.
sawine@68: - einer endlichen Menge von Zuständen
sawine@68: - einer Menge von Startzuständen, in unserem Beispiel war das lediglich der Zustand q0
sawine@68: - der Übergangsrelation Delta
sawine@68: - und einer endlichen Menge an akzeptierenden Zuständen, im Beispiel war das der Zustand q2, bzw q1 und q2 bei dem Co-Automat
sawine@68: 
sawine@68: ==> 15
sawine@68: 
sawine@68: Ein Pfad eines Automaten auf einem Wort w, ist wie wir schon gesehen haben die unendliche Sequenz der dabei durchlaufenen Zustände.
sawine@68: Der erste Zustand muss ein Element der Startzustände sein.
sawine@68: 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.
sawine@68: 
sawine@68: ==> 16
sawine@68: 
sawine@68: 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.
sawine@68: 
sawine@68: Basierend darauf sagen wir:
sawine@68: ein Pfad RHO eines Automaten A ist akzeptierend gdw. ein akzeptierender Zustand unendlich oft in RHO vorkommt.
sawine@68: 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.
sawine@68: 
sawine@68: ==> 17
sawine@68: 
sawine@68: Die akzeptierte Sprache eines Automaten ist einfach die Menge aller akzeptierten Eingaben.
sawine@68: 
sawine@68: ==> 18
sawine@68: 
sawine@68: Es existiert eine verallgemeinerte Form des Büchi-Automaten, welche bei der Automatenkonstruktion Vorteile bietet.
sawine@68: Der Unterschied liegt in der Akzeptanzbedingung.
sawine@68: Der verallgemeinerte Büchi-Automat definiert diese über eine endliche Menge von Mengen von akzeptierenden Zuständen.
sawine@70: Ein Pfad RHO eines solchen Automaten ist akzeptierend gdw. es einen Zustand aus jeder Menge Fi aus dieser Mengenfamilie gibt, der unendlich oft in RHO vorkommt.
sawine@68: 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. 
sawine@68: 
sawine@68: ==> 19
sawine@68: 
sawine@72: Wir kennen nun die Sprache zur Spezifikation von Systemeigenschaften und wir haben Automaten kennengelernt, die auf unendlichen Eingaben arbeiten. 
sawine@75: Für die automaten-theoretische Methode müssen einen Automaten konstruieren anhand einer Systemspezifikation in der linearen temporalen Logik.
sawine@75: In meiner Arbeit geschieht dies über den sog. Fischer-Ladner-Abschluss.
sawine@75: In der Arbeit von Rob Gerth wird eine on-the-fly Konstruktion der Produktautomaten vorgestellt.
sawine@75: Darauf wird Christian Schilling heute Nachmittag genauer eingehen.
sawine@75: 
sawine@75: ==> 20
sawine@75: 
sawine@76: Die Konstruktion des Systemautomaten ist eindeutig einfacher.
sawine@76: 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.
sawine@76: 
sawine@76: Eine Berechnung des Programms ergibt einen Pfad, der aus der Sequenz der Mengen besteht, die die Bewertungsfunktionen für den jeweiligen Zustand zurückgibt.
sawine@76: 
sawine@76: Daraus konstruieren wir den Systemautomaten.
sawine@76: Zu beachten ist, dass die Menge der akzeptierenden Zustände gleich der Menge der Zustände ist, somit ist jeder Pfad des Automaten akzeptierend.
sawine@76: 
sawine@75: ==> 21
sawine@75: 
sawine@76: Daraus folgt direkt folgender Satz: die akzeptierte Sprache eines Systemautomaten ist gleich der Menge aller Pfade des Automaten.
sawine@76: 
sawine@75: ==> 22
sawine@75: 
sawine@72: Erinnern wir uns and die Problembeschreibung vom Anfang.
sawine@75: Übersetzt in die Automatentheorie bedeutet das:
sawine@75: Ein System entspricht der Spezifikation, wenn die akzeptierte Sprache des Systemautomaten in der akzeptierten Sprache des Formelautomaten enthalten ist.
sawine@75: Eine mengentheoretische Umformung gibt uns folgende Form:
sawine@75: 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.
sawine@68: 
sawine@76: Die graphentheoretische Methode erlaubt uns nun die Produktautomaten als Graphen zu interpretieren und das Problem durch die Bildung der Zusammenhangskomponente zu lösen.
sawine@76: Die effiziente on-the-fly Methode sucht stattdessen iterativ nach Zyklen.
sawine@68: 
sawine@76: Wir wissen wie man den Systemautomaten konstruiert und dessen akzeptierte Sprache bestimmt.
sawine@76: Wir wissen wie man Spezifikationen mit Hilfe der linearen temporalen Logik beschreibt.
sawine@76: 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.
sawine@68: 
sawine@76: ==> 23
sawine@76: 
sawine@76: Zum Schluss habe eine kleine Auswahl an Arbeiten vorbereitet.
sawine@76: Meine Arbeit basiert hauptsächlich auf Madhavan Mukund's Veröffentlichung, wobei ich einige Definitionen von Vardi's Paper bevorzugt habe.
sawine@76: Wie bereits erwähnt beschreibt die Arbeit von Rob Gerth und den anderen die on-the-fly Methode.
sawine@76: Das Handbook of Modal Logik kann ich allen empfehlen die sich mehr mit modalen Logiken beschäftigen wollen.
sawine@76: 
sawine@76: ==> 24
sawine@76: 
sawine@76: 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.
sawine@76: 
sawine@76: 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.
sawine@76: 
sawine@76: Vielen Dank!
sawine@76: 
sawine@76: 
sawine@76: