Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Verified Construction of Approval-Based Committee Voting Rules

Forschungsthema:Computational Social Choice
Typ: PdF
Datum: 2025-04-11
Betreuer: Michael Kirsten
Aushang:

Abstract

Decision-making processes like the collective scheduling of a meeting, range design in a store or political elections concern the aggregation of preferences, but may have widely different requirements on a potential outcome. This has led to the formulation and study of a variety of voting rules, which formally describe such collective decision-making processes. Approval-based committee (ABC) voting rules are one important class of voting rules.

In this work, I introduce the concept of aggregate profiles as a means of abstracting similarities in preference aggregation between voting rules. An aggregate profile intuitively limits the information on voters' ballots and possible election outcomes that are used by a given voting rule. I illustrate how aggregate profiles can be used to structure proofs on properties of voting rules. Furthermore, I report on my work of implementing aggregate profiles in the theorem prover Isabelle/HOL and the connected case study of proving three established properties, anonymity, neutrality and continuity, for a subset of approval-based committee voting rules.

Literature