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