A Foundational Framework for the Specification and Verification of Mechanism Design - Archive ouverte HAL Accéder directement au contenu
Rapport Année : 2022

A Foundational Framework for the Specification and Verification of Mechanism Design

(1, 2) , (3)
1
2
3

Résumé

We introduce mech.v, a new framework for the specification and verification of mechanisms, implemented using the Coq interactive theorem prover and the Mathematical Components library. We provide a general definition of mechanism, a subclass capturing auctions, and a few examples of auctions including three notions of Vickrey-Clarke-Groves (VCG), proving their main incentive properties such as truthfulness with reasonable verification effort. We define and prove some more lemmas and definitions usually found in the mechanism design (MD) literature such as Pareto-optimality, rationality, dominance and Nash equilibria. We also define a mechanism refinement system, which we use to relate the implementation of an efficient version of the VCG mechanism for an online advertisement auction to the general VCG specification, allowing us to transfer the truthfulness property from the generic proof. We hope that our library can be useful as a formally verified, unambiguous reference with applications ranging from verification of deployed mechanism to education, and that this is a first step to gather interesting results and definitions from the MD literature to eventually provide a comprehensive mechanically formalized reference.
Fichier principal
Vignette du fichier
E-458.pdf (603.64 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03666871 , version 1 (12-05-2022)

Identifiants

  • HAL Id : hal-03666871 , version 1

Citer

Pierre Jouvelot, Emilio Jesús Gallego Arias. A Foundational Framework for the Specification and Verification of Mechanism Design. [Research Report] E-458.PDF, MINES ParisTech - PSL Research University. 2022. ⟨hal-03666871⟩
29 Consultations
14 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More