Logic for Mechanism Design A Manifesto
Marc Pauly, Michael Wooldridge · 2003
We advance two main claims. The first is that logics --- and in particular, modal strategy logics --- are a powerful formal tool for representing and reasoning about the properties of game theoretic mechanisms. The second is that techniques developed for the formal specification and verification of computer systems (and in particular, the use of logic for specification, and automated verification via model checking) can be usefully applied to mechanism design problems. We begin by reviewing the mechanism design problem, and discussing the issue of how mechanisms might be specified and verified. We then discuss a logic (Alternating-time Temporal Logic --- ATL), which is well suited to representing and reasoning about strategic encounters. We show how ATL can be used to formally specify two social choice mechanisms, and we demonstrate how current model checkers for ATL can be used to verify properties of these mechanisms. We conclude by discussing issues for future research.