Formal Verification of Strategic Stability Measures for Scoring Rules Using Iterative Voting
|Computational Social Choice
Iterative Voting is a game form for elections where strategic voting can be
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
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
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.
- "Automated Verification for Functional and Relational Properties of Voting Rules" in Sixth International Workshop on Computational Social Choice (COMSOC 2016)
- "Verified Construction of Fair Voting Rules" in 29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019)
- "How Bad Is Selfish Voting?" in 17th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS 2018)