Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Verify Your Favourite Voting Rule

Forschungsthema:Social Choice
Typ: BA / MA
Datum: 2020-09-30
Betreuer: Michael Kirsten
Aushang: PDF

Beschreibung

Ein Wahlverfahren (engl. voting rule) ist ein Algorithmus, der aus einer Menge an Einzelentscheidungen ein kollektives Ergebnis einer Wahl berechnet. Von solchen Wahlverfahren existieren unzählige verschiedene Arten sowohl im akademischen Bereich als auch im Einsatz bei echten Wahlen bspw. in der Politik. Spätestens seit dem von Kenneth J. Arrow im Jahr 1950 beschriebenen sogenannten Allgemeinen Unmöglichkeitstheorem ist allerdings klar, dass es nicht möglich ist, aus den Wünschen einer Gesellschaft ein Wahlergebnis abzuleiten, ohne zumindest gewisse gewünschte Grundsätze aufzugeben.

Bei real eingesetzten Wahlverfahren wird häufig versucht, relativ viele dieser Grundsätze zu erfüllen, ohne besonders (viele) negative Effekte aufzuweisen. Beispielsweise wurde aufgrund eines entsprechend negativen Effektes das Wahlverfahren zur Bestimmung des deutschen Bundestags im Jahr 2008 als verfassungswidrig verurteilt. Der Grund waren negative Stimmgewichte, die dazu führten, dass manche Stimmen mehr Gewicht hatten als andere. Daraufhin wurde schließlich 2013 das Wahlverfahren geändert.

Zur Veranschaulichung des Themenbereichs empfehlen wir auch dieses Video der Universität von Amsterdam.

Am Lehrstuhl für Anwendungsorientierte Formale Verifikation entwickeln wir Methoden, um Implementierungen von Wahlverfahren auf solche und ähnliche Eigenschaften (allg. als social choice Eigenschaften bezeichnet) hin zu analysieren. Insbesondere mithilfe der Technik Bounded Model Checking lässt sich dies gut automatisieren. Weiterhin wird am Lehrstuhl auch ein auf dem interaktiven Theorembeweiser Isabelle/HOL basierendes Framework entwickelt, um solche Eigenschaften direkt mittels als korrekt bewiesener formaler Konstruktionsregeln modular zu entwickeln. Im Rahmen einer Abschlussarbeit wäre es hier interessant, eine dieser Techniken auch auf weitere entweder real-eingesetzter oder theoretisch-interessanter komplexere Wahlverfahren anzuwenden und die Verifikationsansätze auszubauen und zu prüfen, inwieweit die behaupteten Eigenschaften erfüllt werden. Dabei kann zudem die Skalierbarkeit der Verifikationstechnik evaluiert und durch geschicktes Ausnutzen von Symmetrien oder anderweitiger Optimierungen auch verbessert werden. Hierbei können Sie sich in Zusammenarbeit mit dem Betreuer selbst ein spannendes Wahlverfahren heraussuchen, das bestimmte social choice Eigenschaften erfüllen soll.

Je nach Umfang des untersuchten Wahlverfahrens und der untersuchten Eigenschaften sowie der gewählten Verifikationsansätze kann dieses Thema entweder als Bachelorarbeit oder als Masterarbeit bearbeitet werden.

Voraussetzungen

  • Grundkenntnisse in und Interesse an formalen Methoden, wie sie z. B. in der Vorlesung Formale Methoden vermittelt werden
  • Gründliche Arbeitsweise sowie ein gutes Abstraktionsvermögen

Kontakt

Interesse? Weitergehende Fragen? Dann melden Sie sich unverbindlich bei Michael Kirsten (Raum 228, Geb. 50.34).

Literatur