Reasoning about Social Choice and Games in Monadic Fixed-Point Logic

TL;DR

This paper proposes using monadic fixed-point logic with counting as a natural language to specify and analyze properties of improvement graphs in social choice and game theory, enabling efficient model checking.

Contribution

It introduces a novel application of monadic fixed-point logic with counting to model and verify properties of improvement graphs across social choice and game-theoretic domains.

Findings

Logic can specify properties of improvement graphs

Model checking is efficient in graph size

Applicable to various social choice and game scenarios

Abstract

Whether it be in normal form games, or in fair allocations, or in voter preferences in voting systems, a certain pattern of reasoning is common. From a particular profile, an agent or a group of agents may have an incentive to shift to a new one. This induces a natural graph structure that we call the improvement graph on the strategy space of these systems. We suggest that the monadic fixed-point logic with counting, an extension of monadic first-order logic on graphs with fixed-point and counting quantifiers, is a natural specification language on improvement graphs, and thus for a class of properties that can be interpreted across these domains. The logic has an efficient model checking algorithm (in the size of the improvement graph).