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

Fortgeschrittenenpraktikum: Visualisierung eines Model Checking Algorithmus

Im Rahmen eines Projektes, in welchem die verschiedenartigsten Problemstellungen in das Model Checking Problem einer sehr ausdrucksstarken temporalen Logik (HFL1) kodiert werden, soll für einen bereits vorhandenen Model Checker ein Tool implementiert werden, welches die sukzessive Verarbeitung der Eingaben graphisch und tabellarisch darstellt.
In diesem Fortgeschrittenenpraktikum geht es weniger um theoretische Aspekte, als vielmehr darum, eine brauchbare Software herzustellen, mit deren Hilfe die Wirkungsweise unseres MC-Algorithmus auf ein gegebenes Problem veranschaulicht werden kann. Dies wiederum dient der Strukturanalyse dieses Problems und ermöglicht die Entwicklung optimierter Algorithmen. So ist es bisher bereits gelungen, einen sehr effektiven Universalitätstest für nichtdeterministische endliche Automaten zu extrahieren.
Die Bearbeitung des Themas beinhaltet optimalerweise folgende Komponenten (die auch auf verschiedene Praktika verteilt werden können):

• Synchrone Darstellung der einzelnen Schritte einer Fixpunktapproximation in Tabellenform und deren Resultate als ausgezeichnete Zustandsmengen im zugrundeliegenden Modell, d.h. in einem Transitionssystem
• Ein Tool, welches komfortabel die Eingabe eines Transitionssystems ermöglicht, d.h. sowohl in einem geeigneten Textformat als auch durch Zusammenklicken graphischer Komponenten, sowie import/export Funktionen von beiden Repräsentationen ineinander und günstigenfalls noch in eine symbolische Repräsentation (Binary Decision Diagrams)

Kontakt

Dr. Martin Lange, D1.07, Oettingenstr. 67, Tel.: 089 21809313

Roland Axelsson, D11, Oettingenstr. 67, Tel.: 089 21809139

Lehr- und Forschungseinheit          Institut          Universität