Abstractions for Model-Checking Game-Theoretic Properties of Auctions

Emmanuel Mohamed Tadjouddine, Frank Guerin, Wamberto W M P D Vasconcelos

Research output: Chapter in Book/Report/Conference proceedingChapter

8 Citations (Scopus)

Abstract

We are interested in verifying game-theoretic properties such as strategy proofness for auction protocols in open agent systems. Model checking provides an automatic way of carrying out such proofs. However it may suffer from state space explosion for large models. To improve the performance of model checking, abstractions were used along with the SPIN model checker. We applied the technique to the Vickrey auction. Numerical results showed the limits of relying solely on SPIN. To reduce the state space required by SPIN, two property-preserving abstraction methods were applied: firstly the classical program slicing technique, which removes irrelevant variables with respect to the property; the second replaces large data, possibly infinite values of variables, with smaller abstract values. This enabled us to model check the strategy-proofness property of the Vickrey auction for unbounded bid ranges and for any number of agents.
Original languageEnglish
Title of host publicationTitle AAMAS '08 Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems
Place of PublicationRichland, SC
PublisherInternational Foundation for Autonomous Agents and Multiagent Systems
Pages1613-1616
Number of pages4
Volume3
ISBN (Print)978-0-9817381-2-3
Publication statusPublished - 2008
Event7th international joint conference on Autonomous agents and multiagent systems - Estoril, Portugal
Duration: 12 May 200816 May 2008

Conference

Conference7th international joint conference on Autonomous agents and multiagent systems
Country/TerritoryPortugal
CityEstoril
Period12/05/0816/05/08

Fingerprint

Dive into the research topics of 'Abstractions for Model-Checking Game-Theoretic Properties of Auctions'. Together they form a unique fingerprint.

Cite this