Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Verify Your Favourite Voting Rule

Forschungsthema:Social Choice
Typ: BA / MA
Datum: 2018-10-12
Betreuer: Michael Kirsten
Bearbeiter:
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.

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. Im Rahmen einer Abschlussarbeit wäre es hier interessant, diese Technik auch auf real-eingesetzte komplexere Wahlverfahren anzuwenden und zum Einen zu prüfen inwieweit das Verfahren die behaupteten Eigenschaften erfüllt und zum Anderen die Skalierbarkeit der Verifikationstechniken zu evaluieren und durch geschicktes Ausnutzen von Symmetrien oder anderweitige Optimierungen zu verbessern. Hierbei können Sie sich in Zusammenarbeit mit dem Betreuer selbst ein spannendes Wahlverfahren heraussuchen, das bestimmte social choice Eigenschaften erfüllen soll.

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