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 Condorcet Voting Rules Using Composable Modules

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2019-11-18
Betreuer: Michael Kirsten
Aushang:

Abstract

In this thesis, we analyze an approach to formally construct verified voting rules using formal composable modules and composition rules such that they fulfill given formal fairness criteria. A voting rule is a function that maps several single voters’ election decisions to a collective election decision. Moreover, the formal fairness criteria are so-called social choice properties which are formalizations of commonly desirable characteristics for voting rules. Instead of considering such a voting rule entirely as a black box, the composable module approach by Diekhoff, Kirsten, and Krämer (2019) understands voting rules as compositions of separate modules and various compositional structures.
The findings in this thesis support the hypothesis that the approach is well-suited for the formal analysis of voting rules, particularly the construction of voting rules and the formal verification of social-choice properties of these voting rules. We apply the approach to the family of Condorcet voting rules, which --if existing-- always elect a so-called Condorcet winner, i.e., the alternative that wins the majority of the pairwise comparisons against all other alternatives.
We implement a new elimination module that uses shared characteristics in the construction to prove properties on an abstract layer such that properties of concrete voting rules follow directly from construction.
The construction pays particular attention to modular design and software-technical standards such as reusability, abstraction, and generalizability. Our case study exemplarily applies the new module on eight Condorcet voting rules and the two properties of Condorcet consistency and homogeneity. The implementations and most of the proofs are conducted in Isabelle/HOL for future reusability.

Literature