Auf der AAAI-Konferenz 2010 wurde eine Arbeit von Umberto Grandi und Ulle Endriss vorgestellt, in der es um die Frage geht, ob sich bei Wahlverfahren bestimmte Rationalitätseigenschaften der einzelnen Wähler auf die gesamte Wählerschaft übertragen lassen. Es ist nämlich bekannt, dass Wahlverfahren grundsätzlich nicht perfekt sein können, und deshalb ist die Entwicklung von Wahlverfahren und die Erforschung ihrer Eigenschaften ein wichtiges Gebiet. In der Master-Arbeit soll es darum gehen, die Ergebnisse obiger Arbeit im Theorembeweiser Isabelle umzusetzen, d.h., die Theoreme dieser Arbeit maschinell zu beweisen.

Bei der Modellprüfung wird untersucht, ob ein gegebenes System eine gegebene Spezifikation erfüllt. Ist dies nicht der Fall, wird ein Gegenbeispiel erzeugt, das zeigt, warum die Spezifikation verletzt ist. NuSMV ist ein symbolischer Modellprüfer für Spezifikationen in den Logiken CTL und LTL. Es enthält SAT- und BDD-basierte Algorithmen zur LTL-Modellprüfung, wobei der SAT-basierte Algorithmus in vielen Fällen ineffizienter als der BDD-basierte ist.

Ziel dieser Arbeit ist die Implementierung einer vorgegebenen Modifikation des SAT-basierten Algorithmus in NuSMV (parallele statt nur sequentieller Transitionen), in der Hoffnung, dadurch eine merkliche Effizienzsteigerung zu erzielen. Abschließend soll die Implementierung anhand vorhandener Benchmarks im Vergleich zu anderen Verfahren evaluiert werden.

Voraussetzungen:

1. Gute C-Programmierkenntnisse
2. Hilfreich: Grundlagen über Planen durch Erfüllbarkeitstests und über Modal- bzw. Temporallogiken

Die Arbeit behandelt einen Teilaspekt des Suchens nach starken und starken zyklischen Plänen für nichtdeterministische Planungsprobleme mit dem Ansatz des Planens durch heuristische Suche unter Verwendung des (L)AO*-Algorithmus und domänenunabhängiger Heuristiken, genauer die Verwendung sogenannter Merge-and-Shrink-Heuristiken (M&S). Starke bzw. starke zyklische Pläne garantieren das Erreichen eines Zielzustands bzw. das Vermeiden von Sackgassen unabhängig vom Ausgang des Nichtdeterminismus. Der Fokus dieser Arbeit liegt auf der automatischen Erzeugung geeigneter Heuristiken zur Steuerung der Suche. Dabei bedienen wir uns des Merge-and-Shrink-Ansatzes von Helmert, Haslum und Hoffmann (2007).

Ein linearer pseudo-Boolescher Constraint (LPB) ist ein Ausdruck der Form a_1 l_1+...+a_m l_m ≥ d. Hierbei ist jedes l_i ein Literal der Form x_i or ¯x_i=1-x_i, d.h., x_i wird 0 wenn x_i falsch ist und 1 wenn x_i wahr ist, und umgekehrt für ¯x_i. Des weiteren sind a_1,...,a_m,d natürliche Zahlen. LPBs sind eine Verallgemeinerung von aussagenlogischen Klauseln. Boolesche Funktionen können mittels LPBs oft kompakter dargestellt werden als mittels konjunktiver oder disjunktiver Normalformen. Z.B. entspricht die LPB 2x_1+¯x_2+x_3+x_4≥2 der DNF x_1\/(¬ x_2/\ x_3)\/(¬ x_2/\ x_4)\/(x_3/\ x_4). Daher gibt es in der Literatur mehrere Ansätze, die Techniken aus dem SAT Solving (aussagenlogische Erfüllbarkeit) auf LPBs zu verallgemeinern. In diesen Arbeiten wird immer davon ausgegangen, dass sich die LPBs aus der Kodierung innerhalb der Problemdomäne natürlich ergeben.

Man kann allerding fragen: könnte es nicht auch interessant sein, beliebige aussagenlogische Formeln in eine äquivalente LPB-Menge zu transformieren, um dann beim Entscheiden der Erfüllbarkeit von der kompakteren Darstellung zu profitieren? Es gibt einen Algorithmus, der dieses Problem teilweise löst: gegeben eine aussagenlogische Formel, die sich als eine einzige LPB darstellen lässt, findet der Algorithmus diese LPB.

Gegenstand der Bachelor-Arbeit ist es, diesen Algorithmus zu implementieren, und einige Experimente zu machen, um abzuschätzen, wie aufwändig die Transformation in der Praxis ist.

Domänenkontrollwissen kann verwendet werden, um die möglichen Pläne einer Planungsaufgabe einzuschränken. Dadurch wird der Suchraum verkleinert und es ist so möglich, Planungsaufgaben zu lösen, die zu schwierig für ein domänenunabhängiges Planungssystem wären. Eine Möglichkeit, solches Domänenwissen zu definieren, ist, die möglichen Pläne abstrakt mit Hilfe einer prozeduralen (Golog-ähnlichen) Sprache zu beschreiben. Baier hat solch eine Sprache vorgestellt und gezeigt, wie man dieses Domänenwissen in die ursprüngliche PDDL-Beschreibung kompilieren kann und es so für beliebige klassische Planungssysteme nutzbar machen kann.

Ziel dieser Diplomarbeit ist es, diese Methode für temporales Planen weiterzuentwickeln. Die prozedurale Beschreibungssprache muss hierzu um geeignet gewählte temporale Konstrukte mit einer klar definierten Semantik erweitert werden. Im nächsten Schritt soll dann eine Kompilierung angegeben werden, die das Domänenkontrollwissen in die gegebene temporale PDDL-Beschreibung integriert. Eine Implementierung dieser Kompilation und eine experimentelle Evaluation runden die Arbeit ab.