Strategic Reasoning in Automated Mechanism Design

The tutorial will give an overview of the application of logics for strategic reasoning in Mechanism Design, a central problem in economics that consists of designing new games for aggregating preferences in MAS. The aim is to show how to use extensions of Strategy Logic (SL) for (i) the automated verification of mechanisms in relation to target properties expressed in a high-level logical language, and (ii) the synthesis of mechanisms from a partial or complete logical specification. We will address first the basic background on logics for strategic reasoning in MAS and the relevant decision problems for mechanism design. Next, we recall classical concepts from economics and show how we can capture them with SL. We then explain how to automatically verify and synthesize mechanisms using concurrent game structures and SL specifications. We provide examples of mechanisms and economic properties that can be captured using this approach.