1 1. Guten Morgen! Mein Name ist Eugen Sawin und ich werde jetzt den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking.
3 2. Was ich ihnen erzählen werde, wird die Meisten von euch bei der Bearbeitung des Themas in irgendeiner Form tangiert haben.
5 3. Meine Präsentation soll einen Überblick geben über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings.
9 4. PHI ist erfüllt in Modell M, oder Modell M modelliert PHI.
10 Das ist der Kern unserer Bemühungen.
11 Doch was bedeutet das?
12 Wir übersetzen das in die Problemstellung der Verifikation von Systemen.
16 5. Gegeben sei ein Programm und dessen Spezifikation, das Problem lautet:
17 erfüllt jeder Pfad des Programms die Spezifikation?
19 Bevor wir an die Tat schreiten um das Problem zu lösen,
20 möchte ich eine andere Frage beantworten.
22 Wieso das Ganze? Was ist der praktische Nutzen der Verifikation?
26 Hard- und Softwaresysteme haben alle Bereiche der Industrie und damit auch unseren Alltag durchdrungen.
27 Sie bilden die Infrastruktur unserer Kommunikation, bieten Sicherheit und retten sogar Leben.
28 Und sie werden immer komplexer.
29 Die Industrie investiert viel Zeit und Geld in die Verifikation sicherheitskritischer Systeme und der Kernkomponenten anderer Systeme.
30 Die automatisierte Verifikation hat bereits in der Chip-Verifikation ihre praktische Anwendbarkeit gezeigt und ist in der Softwareindustrie stark gefragt.
36 Wenn ich sage: "Es ist dunkel." ist es nicht eindeutig, was ich damit ausdrücken möchte.
38 Ich könnte damit meinen "Es ist immer dunkel.", doch das spricht gegen unsere Intuition.
39 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).
41 Wenn wir nach draußen schauen, können wir aus Erfahrung behaupten, dass es "notwendigerweise irgendwann dunkel wird."
43 Unsere Sprache erlaubt es uns auch kausale Zusammenhänge zu bilden, wie z.B. "Es ist dunkel, bis Jemand das Licht an macht."
45 Wir sehen, dass die natürliche Sprache nicht eindeutig ist und somit zur formalen Beschreibung ungeeignet.
46 Wie können wir unsere Sprache zähmen, ohne die Ausdruckskraft zu verlieren.
47 Nun, als Ersten machen wir das Licht wieder an!
51 Nehmen wir den letzten Satz in einer allgemeineren Form als Beispiel.
52 Dieser Satz sollte allgemeingültig sein.
53 Wie können wir die Aussage dieses Satzes formal festhalten?
54 Wir bedienen uns der Aussagenlogik und erweitern diese um eine weitere Verknüpfung.
58 Dabei sind p0 und p1 Elementaraussagen, sog. Atome, die entsprechend für "Es is dunkel" und "Es gibt licht" stehen.
59 Die neue Verknüpfung nennen wir trivialerweise "until" und notieren sie mit dem kalligraphischen U.
60 Halten wir das formal fest.
64 Wir definieren die Syntax der linearen temporalen Logik mit Hilfe dieser Produktionen in Backus-Naur-Form.
65 Somit ist eine LTL-Formel entweder ein aussagenlogisches Atom, eine negierte Formel oder eine Disjunktion zweier Formeln.
66 Das kannten wir bereits aus der Aussagenlogik.
67 Die Erweiterung sind das kalligraphische X, welches für "Next" steht und das "Until" aus dem Beispiel.
68 Diese Syntaxdefinition bildet das Fundament für weitere abgeleitete Verknüpfungen.
72 Wir interpretieren LTL-Formeln über unendliche Sequenzen von Aussagen.
73 Die Sequenz entspricht der zeitlichen Abfolge von Ereignissen in einem vorwärts gerichteteten diskreten Zeitverlauf.
74 Diese Interpretation heißt die Kripke-Semantik.
75 Das Kripke-Modell der LTL-Semantik besteht aus einer abzählbaren Menge von Zuständen, verknüpft duch die Erreichbarkeitsrelation und der Bewertungsfunktion V.
76 Da wir nur lineare Abfolgen betrachten, fällt die Erreichbarkeitsrelation einfach aus.
77 Von einem beliebigen Zustand ist jeweils nur dessen Nachfolger erreichbar.
78 Die Bewertungsfunktion liefert uns die Menge aller gültigen Atome für einen bestimmten Zustand.
79 Intuitiv sagt man, ein Atom p ist wahr zum Zeitpunkt i gdw. p in der Menge V(i) ist.
83 Hier ist eine Veranschaulichung eines Beispielmodells.
84 Man sieht die Zustände s0 bis si und den Zeitverlauf durch die Relation R.
85 Für jeden Zustand ist die Rückgabe der Bewertungsfunktion als Menge positiver Atome abgebildet.
86 Wie man sieht, bietet LTL keine gute Grundlage für Science Fiction, weder Zeitreisen noch Parallelwelten sind möglich.
87 Luminous Fennell wird in der nächsten Präsentation ein alternatives Modell anbieten, das in dieser Hinsicht etwas interessanter ist und algorithmisch effizienter.
91 Die Erfüllbarkeit einer Formel zu einem Zeitpunkt i im Modell M ist folgendermaßen definiert:
92 - ein Atom p ist erfüllbar gdw. und p in der Menge V(i) ist
93 - eine negierte Formel PHI ist erfüllbar gdw. PHI nicht erfüllbar ist
94 - eine Disjunktion von PHI und PSI ist erfüllbar gdw. PHI oder PSI erfüllbar ist
95 - Next PHI ist erfüllbar gdw. PHI im darauffolgenden Zeitpunkt erfüllbar ist
96 - 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.
98 Mit Hilfe der linearen temporalen Logik lassen sich Programmeigenschaften und derren zeitliche Abhängigkeiten genau beschreiben.
99 Als nächstes werden wir uns den Automaten widmen, die auf unendlichen Eingaben operieren.
103 Wieso sind unsere Eingaben überhaupt unendlich?
104 Im Gegensatz zu terminierenden Programmen sind reaktive Systeme fortlaufende Prozesse.
105 Ein mal initiiert, verbleiben reaktive Systeme in einem aktiven Zustand und reagieren auf nebenläufige Eingaben.
106 Theoretisch betrachtet, arbeiten solche Systeme somit auf unendlichen Eingabesequenzen.
110 Hier ist ein Beispielautomat, der auf unendlichen Eingaben arbeitet.
111 Sieht jemand auf Anhieb welche Sprache dieser Automat akzeptiert?
112 w1 ist eine Eingabe, der Überstrich soll eine unendliche periodische Wiederholung der Sequenz darstellen.
113 Bei dieser Eingabe werden die folgenden Zustände durchlaufen:
114 - wir starten in q0, lesen zwei b, somit bleiben wir für beide Eingaben in q0
115 - als nächstes lesen wir ein a, was uns in Zustand q1 versetzt
116 - danach folgt ein weiteres a, wir bleiben also in q1
117 - 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
119 w2 bietet ein ähnliches Beispiel, jedoch pendeln wir diesmal zwischen q1 und q2 nach einer kurzen Phase.
121 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.
125 Nun wollen wir das Komplement des Automaten bilden.
126 Naiverweise gehe ich dabei vor, wie beim endlichen Automaten und kehre einfach die Akzeptanzeigenschaften der Zustände um.
127 Man sieht sofort, dass dies nicht der korrekte Komplementautomat ist, denn er akzeptiert immer noch Eingaben mit unendlichen Sequenzen von ab.
129 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.
130 Wir sehen, dass der Komplement-Automat im Gegensatz zu dem Automaten nicht deterministisch ist.
131 Die Konstruktion dieser sog. Co-Büchi-Automaten wird Stephanie Embgen im Detail erörtern, deswegen werde ich auch nicht weiter darauf eingehen.
135 Halten wir das Ganze formal fest.
136 Wenn ich von Automaten spreche, meine ich im allgemeinen nicht-deterministische Büchi-Automaten.
137 Diese bestehen aus : - einem endlichen Alphabet, in unserem Beispiel war das die Menge {a,b}.
138 - einer endlichen Menge von Zuständen
139 - einer Menge von Startzuständen, in unserem Beispiel war das lediglich der Zustand q0
140 - der Übergangsrelation Delta
141 - und einer endlichen Menge an akzeptierenden Zuständen, im Beispiel war das der Zustand q2, bzw q1 und q2 bei dem Co-Automat
145 Ein Pfad eines Automaten auf einem Wort w, ist wie wir schon gesehen haben die unendliche Sequenz der dabei durchlaufenen Zustände.
146 Der erste Zustand muss ein Element der Startzustände sein.
147 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.
151 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.
153 Basierend darauf sagen wir:
154 ein Pfad RHO eines Automaten A ist akzeptierend gdw. ein akzeptierender Zustand unendlich oft in RHO vorkommt.
155 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.
159 Die akzeptierte Sprache eines Automaten ist einfach die Menge aller akzeptierten Eingaben.
163 Es existiert eine verallgemeinerte Form des Büchi-Automaten, welche bei der Automatenkonstruktion Vorteile bietet.
164 Der Unterschied liegt in der Akzeptanzbedingung.
165 Der verallgemeinerte Büchi-Automat definiert diese über eine endliche Menge von Mengen von akzeptierenden Zuständen.
166 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.
167 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.