Ludwig-Maximilians-Universität München, Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik

Diplomarbeit

Lineare schwache alternierende Automaten und das Model Checking Problem

Inhalt

Automatenbasiertes Model Checking ist ein häufig verwendeter Ansatz des Software Model Checkings. Traditionellerweise werden nichtdeterministische Buechi-Automaten verwendet, um die zu checkende temporallogische Formel zu repräsentieren. Diese Automaten weisen i. A. eine exponentielle Grösse bezüglich der repräsentierten LTL-Formel auf. Unser Interesse gilt einer anderen Art von Automaten, den linearen schwachen alternierenden Automaten. Sie weisen eine lineare Anzahl von Zuständen auf und können relativ einfach für eine gegebene LTL-Formel konstruiert werden. Zudem erkenen sie genau die Sprachen, die durch LTL beschrieben werden können. Diese Eigenschaften versuchen wir für Software-Model Checking zu nutzen, wobei wir einen exponentiellen Leerheitstest - bei nichtdeterministischen Büchi-Automaten ist er linear - in Kauf nehmen. Mittels einer Adaption des Tarjan-Algorithmus können wir eine Übersetzung von linearen schwachen alternierenden Automaten in generalisierte Büchi-Automaten mit dem Leerheitstest verbinden. Wir modifizieren den SPIN Model Checker, um den neuen Algorithmus zu verwenden.

Materialien

Bearbeiter: Moritz Hammer
Aufgabensteller: Prof. Dr. Martin Wirsing
Betreuer: Dr. Alexander Knapp Dr. Stephan Merz
Fertigstellung: Sommersemester 2004

Diplomarbeiten und Fortgeschrittenenpraktika

Lehrstuhl

Institut

Universität