Abstracting and Verifying Strategy-Proofness for Auction Mechanisms

ing and Verifying Strategy-proofness for Auction Mechanisms E. M. Tadjouddine, F. Guerin, and W. Vasconcelos Department of Computing Science, King's College, University of Aberdeen, Aberdeen AB24 3UE, Scotland We are interested in finding algorithms which will allow an agent roaming between different electronic auction institutions to automatically verify the game-theoretic properties of a previously unseen auction protocol. A property may be that the protocol is robust to collusion or deception or that a given strategy is optimal. 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 perof model checking, abstractions were used along with the Spin model checker. We considered two case studies: the Vickrey auction and a tractable combinatorial auction. Numerical results showed the limits of relying solely on Spin. To reduce the state space required by Spin, two -preserving abstraction...

• Type: Conference
• Year: 2008
• Where: DALT
• Authors: Emmanuel M. Tadjouddine, Frank Guerin, Wamberto Weber Vasconcelos
• Keywords: Auction, DALT 2008, Intelligent Agents, Model Checking, Vickrey Auction