We explore techniques from computer-aided verification to construct formal proofs of incentive properties. Because formal proofs can be automatically checked, agents do not need to manually check the properties, or even understand the proof. To demonstrate, we present the verification of a sophisticated mechanism: the generic reduction from Bayesian incentive compatible mechanism design to algorithm design given by Hartline, Kleinberg, and Malekian. This mechanism presents new challenges for formal verification, including essential use of randomness from both the execution of the mechanism and from the prior type distributions.
CITATION STYLE
Barthe, G., Gaboardi, M., Arias, E. J. G., Hsu, J., Roth, A., & Strub, P. Y. (2016). Computer-aided verification for mechanism design. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10123 LNCS, pp. 279–293). Springer Verlag. https://doi.org/10.1007/978-3-662-54110-4_20
Mendeley helps you to discover research relevant for your work.