PSE – Gruppe II

Hintergrund

Ein Wahlverfahren oder auch Wahlauszählverfahren ist eine Methode, individuelle Präferenzen zu einer aggregierten Wahlentscheidung zu kombinieren. Häufig ist ein solches Verfahren Teil des grundsätzlichen demokratischen Verfahrens und stellt einen wichtigen Faktor für die Glaubwürdigkeit der gesamten Wahl dar. Es ist also unerlässlich, dass Wahlverfahren wie vorgesehen funktionieren, also beispielsweise den in einer rechtlich verbindlichen Verfassung spezifizierten Anforderungen genügen. Existierende Wahlverfahren haben ungewollte und manchmal überraschende Eigenschaften aufgewiesen (z. B. negative Stimmgewichte bei den Bundestagswahlen in Deutschland). Für kompliziertere, neu-designte Wahlverfahren, die mithilfe der Unterstützung von Computern im Stimmauszählverfahren ermöglicht werden, ist es wahrscheinlich, dass sich solche Sachverhalte ebenso abzeichnen.

Im Rahmen von Forschungskollaborationen innerhalb der COST Action IC1205 "Computational Social Choice" entwickelt unsere Forschungsgruppe logik-basierte Verfahren, um Wahlverfahren auf formale Eigenschaften zu prüfen, sowie die Durchführung konkreter Wahlen mittels logik-basierter Methoden zu unterstützen.

Aufgabenbeschreibung

Ziel dieses Projekts ist die Planung und Implementierung eines Wahl-Analyse-Tools, das für unterschiedliche Algorithmen zur Berechnung eines Wahlergebnisses verwendbar ist. Für einen Benutzer soll es dabei möglich sein, ein solches Wahlverfahren auf verschiedene Aspekte hin zu analysieren. Das Tool soll es erlauben, Annahmen und Aussagen als C-Ausdrücke bezüglich Ein- und Ausgabe sowie auch zwischen verschiedenen Ein- und Ausgaben (sogenannte relationale Eigenschaften) zu spezifizieren, die im Hintergrund von einem Verifikationswerkzeug geprüft werden.

Dieses Werkzeug wird als Black-Box verwendet, wobei es das zu schreibende Wahl-Analyse-Tool sowohl erlaubt, selbst-geschriebene Formeln in geeigneter Form an das Verifikationswerkzeug weiterzugeben, als auch die Ausgabe des Werkzeugs (entweder ein Gegenbeispiel oder eine Erfolgsnachricht) an das Analyse-Tool weiterzuleiten. Weiterhin soll es möglich sein, das Verifikationswerkzeug für eine Liste von Eingaben im Stapelverarbeitungs-Modus anzusteuern und abzufragen.

Das Tool soll es außerdem erlauben, entsprechende Wahlverfahren selbst in der Programmiersprache C zu schreiben, auf die geeignete Form zu prüfen und an das Verifikationswerkzeug weiterzugeben. Insbesondere sollen vom Verifikationswerkzeug ausgegebene Gegenbeispiele anschaulich dargestellt werden, wobei auch relationale Eigenschaften berücksichtigt werden sollen, in denen zwei oder mehr Läufe gegenübergestellt werden. Zusätzlich soll es das Analyse-Tool erlauben, das Wahlverfahren mit konkreten Eingabedaten auszuführen.