Lehr- und Forschungseinheit
Institut
Universität
Lehr- und Forschungseinheit für Theoretische Informatik,
Institut für Informatik der Ludwig-Maximilians-Universität
München
Fixpoint Logic with Chop (FLC) ist eine Erweiterung des modalen μ-Kalküls um einen Operator für sequentielle Komposition (Chop).
Mit Hilfe des Chop-Operators können im Gegensatz zum μ-Kalkül auch kontextfreie und sogar bestimmte kontextsensitive Eigenschaften
ausgedrückt werden.
Während die Semantik eines μ-Kalkül-Ausdrucks als Zustandsmenge eines Transitionssystems definiert ist, nämlich gerade diejenige, deren Elemente
den Ausdruck erfüllen, ist die Semantik eines FLC-Ausdrucks durch eine Funktion von Zustandsmengen in Zustandsmengen gegeben.
Dies erklärt sich dadurch, daß die Bedeutung einer FLC-Teilformel durch den Chop-Operator in Abhängigkeit von den "Resultaten" anderer Teilformeln stehen kann.
Das Model-Checking Problem für FLC ist zwar im Allgemeinen unentscheidbar, jedoch gilt dies nicht für endliche Modelle.
Ein direkter Ansatz zu einem Model-Checking Algorithmus, welcher die Fixpunktiteration global für sämtliche Zustandsmengen durchführt, benötigt im Vergleich zu einem ähnlich arbeitenden μ-Kalkül Model-Checker exponentiell mehr Speicher (in der Anzahl der Zustände), weil stets eine ganze Funktion berechnet werden muß.
Glücklicherweise hat sich herausgestellt, daß es nicht unbedingt notwendig ist, die Fixpunktiteration in allen Argumentstellen durchzuführen, wenn man sich nur für den Wert des Fixpunktes an einer Stelle interessiert.
Die relevanten Argumentstellen lassen sich on-the-fly ermitteln und die Resultate der Fixpunktiteration, eingeschränkt auf diese Stellen, sind korrekt.
Ziel der Diplomarbeit wäre es, einen von Martin Lange entwickelten Algorithmus für dieses sogenannte lokale Model-Checking zu implementieren und in das Tool NuSMV zu integrieren.
Kontakt zu den Verantwortlichen des NuSMV Projektes ist bereits hergestellt, so daß sich hier eine hervorragende Gelegenheit bietet, mit renommierten Wissenschaftlern zusammenzuarbeiten.
Literatur/Material/Links:
Dr. Martin Lange, D1.07, Oettingenstr. 67, Tel.: 089 21809313
Roland Axelsson, D11, Oettingenstr. 67, Tel.: 089 21809139