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

Verified Construction of the Split Cycle Voting Rule

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2023-04-28
Betreuer: Michael Kirsten
Aushang:

Abstract

A voting rule is an algorithm that uses a set of votes to determine the winner or multiple winners out of a set of alternatives. In order to study these rules more closely, Diekhoff, Kirsten, and Krämer (2019) created a framework to assist in the construction of voting rules and the formal verification of social choice properties that these rules might exhibit using composable modules. A social choice property is herein a formalization of a commonly desirable characteristic of a voting rule.

In this thesis, we implement the split cycle voting rule into this framework. The split cycle voting rule is a relatively new voting rule which fulfills several highly sought-after social choice properties. We implement the rule both by using existing modules in the framework and by creating new modules, which can in turn be used for constructing other voting rules. We also prove that the split cycle voting rule fulfills the two social choice properties Condorcet consistency and monotonicity.

A voting rule is Condorcet consistent whenever if an alternative is pairwise preferred to every other alternative, said alternative will be the sole winner of the election. Furthermore, a voting rule is monotone whenever if an alternative wins the election and the election is held again, with said alternative being equally or more preferred to every other alternative than in the previous round, said alternative will still win the election. Overall, we construct the split cycle voting rule and formally verify said properties by using and creating composable modules.

Literature