Relation-algebraic and Tool-supported Control of Condorcet Voting

We present a relation-algebraic model of Condorcet voting and, based on it, relation-algebraic solutions of the constructive control problem via the removal of voters. We consider two winning conditions, viz. to be a Condorcet winner and to be in the (Gilles resp. upward) uncovered set. For the first condition the control problem is known to be NP-hard; for the second condition the NP-hardness of the control problem is shown in the paper. All relation-algebraic specifications we will develop in the paper immediately can be translated into the programming language of the BDD-based computer system RelView. Our approach is very flexible and especially appropriate for prototyping and experimentation, and as such very instructive for educational purposes. It can easily be applied to other voting rules and control problems.