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 Symmetry Properties in Distance-Rationalizable Voting Rules

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2023-09-18
Betreuer: Michael Kirsten
Aushang:

Abstract

Voting rules are functions that aggregate multiple single preferences into one result. As such, they model electoral systems. There are certain desirable properties in voting rules that determine their suitability for different use cases. For example, the result of any secret election should be independent of the voters' identities, a property called anonymity. Generally, symmetry properties such as anonymity describe the behaviour of voting rules given a hypothetical change in the votes.
We take a closer look at symmetry properties which can be described with respect to group actions on the sets of elections and election results. We formalize this connection in Isabelle/HOL and use it to show inference rules for the modular construction of distance-rationalizable voting rules. Moreover, some symmetry properties allow the transition to quotients of equivalence relations on the set of elections, offering a geometric perspective to the construction and study of voting rules. We formalize the basics needed to apply such transitions in the modular construction and verification of distance-rationalizable voting rules.

Literature