Formal Verification of Bayesian Mechanisms

Authors

  • Munyque Mittelmann Università degli Studi di Napoli ``Federico II'', Italy
  • Bastien Maubert Università degli Studi di Napoli ``Federico II'', Italy
  • Aniello Murano Università degli Studi di Napoli ``Federico II'', Italy
  • Laurent Perrussel IRIT - Université Toulouse Capitole, France

DOI:

https://doi.org/10.1609/aaai.v37i10.26373

Keywords:

MAS: Multiagent Systems Under Uncertainty, KRR: Applications, MAS: Mechanism Design

Abstract

In this paper, for the first time, we study the formal verification of Bayesian mechanisms through strategic reasoning. We rely on the framework of Probabilistic Strategy Logic (PSL), which is well-suited for representing and verifying multi-agent systems with incomplete information. We take advantage of the recent results on the decidability of PSL model checking under memoryless strategies, and reduce the problem of formally verifying Bayesian mechanisms to PSL model checking. We show how to encode Bayesian-Nash equilibrium and economical properties, and illustrate our approach with different kinds of mechanisms.
AAAI-23 Proceedings Cover

Downloads

Published

2023-06-26

How to Cite

Mittelmann, M., Maubert, B., Murano, A., & Perrussel, L. (2023). Formal Verification of Bayesian Mechanisms. Proceedings of the AAAI Conference on Artificial Intelligence, 37(10), 11621-11629. https://doi.org/10.1609/aaai.v37i10.26373

Issue

Vol. 37 No. 10: AAAI-23 Technical Tracks 10

Section

AAAI Technical Track on Multiagent Systems