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
- "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)