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

Formal Verification of Strategic Stability Measures for Scoring Rules Using Iterative Voting

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2021-01-21
Betreuer: Michael Kirsten
Aushang:

Abstract

Iterative Voting is a game form for elections where strategic voting can be analyzed. The question of how untrue or unstable an election result may become when allowing strategic voting can be approached via the measure "Dynamic Price of Anarchy" (DPoA) that was proposed by Branzei et al., 2013. The DPoA assumes that voters act as individuals and respond greedily in best responses to make, according to their own preference, the best possible candidate win. It measures the initial score difference between the truthful winner and the Nash-equilibrium winner at the end of the game with the smallest initial score.
In this thesis, we build a formal model for positional scoring rules and iterative voting games in which we analyze properties of iterative voting games and use it to prove the DPoA of the plurality rule in Isabelle/HOL. We argue for the well-suitedness of this approach to prove upper bounds of the DPoA and indicate challenges for the verification of lower bounds. We furthermore look at other voting rules, e.g., 2-approval and the k-approval family, and analyze their DPoA compared to the Borda rule based on the results by Branzei et al., 2013. Moreover, we investigate how the choice of a tiebreaker may affect the DPoA, and analyze the composition of the plurality rule with a 2-approval-tiebreaker, as well as 2-approval with a plurality and a Borda tiebreaker. Finally, we show that large DPoAs can be reached even with tie-breaking disadvantages of the Nash-equilibrium winners.

Literature