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

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

Abstract

The field of social choice theory deals with the decision making of a group of people. Specifically, it deals with the different methods that can be used in order to make such a decision and what characteristics they have. The goal is to be able to make a claim about the fairness of an electoral procedure. For the formal investigation of fairness, properties are defined, which a fair election ought to fulfill. One method of examining voting rules for their properties is the composable module approach, which divides an electoral procedure into its basic components. This process is intended to simplify the verification process of properties with regard to election procedures. Instead of considering and evaluating these electoral procedures in their entirety, individual components of an election are examined. We call those components modules. The complexity of the verification is therefore reduced. From the statements we can make about these modules, we infer statements about the entire procedure.
In this thesis, we extend the existing framework for the composable module approach by Diekhoff, Kirsten, and Krämer (2020) for the group of scoring-based voting rules. This group of voting rules awards points to alternatives or candidates, based on their positioning in a ranked ballot. We create an abstract module that is based on the shared characteristics of those scoring-based voting rules. Furthermore, we provide formal proofs for the fairness properties homogeneity and reinforcement for the voting rules we implement. In addition, we make statements on the extent to which the composable module approach is suitable for the the verification of such properties. We implement the voting rules and the proofs regarding the properties in the theorem prover Isabelle using the Isar language. Through the implementation, we show the advantages of the composable module approach for testing properties of voting procedures.

Literature