Umfang

Dieses Thema kann im Rahmen einer Bachelorarbeit bearbeitet werden.

Problemstellung

Einleitung

In vorangegangener Arbeit wurde mittels Deep Learning ein Classifier trainiert, welcher für ein gegebenes B Prädikat das beste Backend des ProB Model Checkers zum Lösen des Prädikats bestimmt. Für weitere Arbeit in dem Bereich ist das Ziel eine generellere Prädikatendatenbank zu erstellen.

Ein Problem, welches sich hierbei ergibt, ist die Detektion von syntaxgleichen Expressions, z.B.

a + b = 2*b+1 & a > b

b + a = 2*a+1 & a < b

Obige Ausdrücke sind äquivalent, jedoch nutzen sie andere Operatoren (> vs. <) und vertauschte Variablennamen. Solche Duplikate zu erkennen würde erlauben eine Prädikatendatenbank zu erstellen, in welcher alle Prädikate syntaktisch einzigartig sind.

Zielsetzung

Ziel der Arbeit ist es, eine semi-kanonische Form für Prädikate zu erarbeiten, welche, bei Gleichheit für zwei Prädikate, die syntaktische Gleichheit der beiden Prädikate impliziert.

Eine Äquivalenzbeziehung wäre zwar wünschenswerter, jedoch vermutlich nicht erreichbar.

Hierfür wird die Repräsentation der Prädikate in einem Abstract Syntax Tree (AST) gegeben, welcher in die kanonische Form manipuliert/modifiziert werden kann.

Empfohlene Vorkenntnisse

Java- und OOP-Kenntnisse.

Wissen über B ist nicht erforderlich, obgleich hilfreich. Ebenso ist wissen über SableCC und ASTs hilfreich, aber nicht erforderlich.

Minimalanforderungen

  • Entwicklung verschiedener kanonischer Formen
  • Auswertung und Vergleich der Formen
    • Angabe problematischer Prädikate
  • Anwendung auf Prädikatendatenbank

Variationen

  • Vergleich welche Art von Duplikaten (unterschiedliche Struktur, Variablennamen, etc.) für welchen Machine Learning Ansatz akzeptabel sein könnte

Kontakt

Jannik Dunkelau
Raum 25.12.02.52 · jannik.dunkelau@hhu.de