Formal Verification of Condorcet Voting Rules Using Composable Modules
|Forschungsthema:||Computational Social Choice|
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
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.
- "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)