Strategic Reasoning in Automated Mechanism Design @ KR 2023 

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 Multi-Agent Systems (MAS). The aim is to show how to use extensions of Strategy Logic (SL) for: 

1. the automated verification of mechanisms in relation to target properties expressed in a high-level logical language; 

2. 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. 

1. Formal verification (slides)
   
   

   1. Basic concepts of formal verification for monolithic systems (25min)

      • Introduction to closed system verification: Model Checking

      • Linear and Branching-time Temporal Logics: LTL, CTL, and CTL*

      • An automata-theoretic approach to solve model checking
        
        

   2. From one player to multiple players (20min)

      • Introduction to open systems verification: Module checking as a two-player game

      • Logics for strategic reasoning: ATL and ATL*
        
        

2. Strategic Reasoning and Mechanisms Verification and Synthesis
   
   

   1. From ATL to Strategy Logic (25 min, slides)

      • Strategy Logic

      • Fragments

      • Imperfect Information
        
        

   2. Reasoning about Mechanisms with Strategy Logic (40 min, slides)

      • Mechanism Design

      • Verification of Mechanisms

      • Synthesis of Mechanism

The tutorial will assume some basic knowledge of propositional, modal, or temporal logic. The tutorial introduces a bridge between two large scientific communities that participate actively in KR, so the potential audience is wide. In particular, the target audience consists on 

1. AI researchers either specialized in Knowledge Representation, Strategic Reasoning, and/or Multi-Agent Systems; 

2. Economics researchers interested in Algorithmic Game Theory, Social Choice, and Automated Mechanisms Design.

The learning goals are, first, to learn the fundamentals of logics for strategic reasoning and Mechanisms Design. Second, the understanding of how formal reasoning can be applied to social choice problems and to ensure economic properties.

• Alur, R.; Henzinger, T. A.; and Kupferman, O. 2002. Alternating-time temporal logic. Journal of the ACM 49(5):672–713. 

• Berthon, R.; Maubert, B.; Murano, A.; Rubin, S.; and Vardi, M. 2021. Strategy logic with imperfect information. ACM Trans. Comput. Logic 22(1). 

• Bouyer, P.; Kupferman, O.; Markey, N.; Maubert, B.; Murano, A.; and Perelli, G. 2019. Reasoning about quality and fuzziness of strategic behaviours. In Proc. of IJCAI.

• Chatterjee, K.; Henzinger, T. A.; and Piterman, N. 2010. Strategy logic. Information and Computation 208(6):677–693.

• Conitzer, V., and Sandholm, T. 2002. Complexity of mechanism design. In Proc. of the 18th Conf. in Uncertainty in AI, 103–110. Morgan Kaufmann.

• Maubert, B.; Mittelmann, M.; Murano, A.; and Perrussel, L. 2021. Strategic reasoning in automated mechanism design. In Proc. of KR 2021.

• Mittelmann, M.; Maubert, B.; Murano, A.; and Perrussel, L. 2022. Automated synthesis of mechanisms. In IJCAI, 2022.

• Mittelmann, M.; Maubert, B.; Murano, A.; and Perrussel, L. 2023. Formal verification of bayesian mechanisms. In AAAI-23.

• Mogavero, F.; Murano, A.; Perelli, G.; and Vardi, M. 2014. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log. 15(4).

• Nisan, N.; Roughgarden, T.; Tardos,  ́E.; and Vazirani, V. 2007. Algorithmic Game Theory. Cambridge Univ. Press.

• Roughgarden, T. 2010. Algorithmic game theory. Communications of the ACM 53(7):78–86.