Abstracting and verifying strategy-proofness for auction mechanisms

Emmanuel M Tadjouddine, Frank Guerin, Wamberto Vasconcelos

Research output: Contribution to journalArticle

5 Citations (Scopus)

Abstract

We are interested in finding algorithms which will allow an agent roaming between different electronic auction institutions to antomatically 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 all 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 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 property-preserving abstraction methods were applied: the first is 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 range and number of agents.

Original languageEnglish
Pages (from-to)197-214
Number of pages18
JournalLecture Notes in Computer Science
Volume5397
DOIs
Publication statusPublished - 2009

Keywords

  • model checking

Cite this

Abstracting and verifying strategy-proofness for auction mechanisms. / Tadjouddine, Emmanuel M; Guerin, Frank; Vasconcelos, Wamberto.

In: Lecture Notes in Computer Science, Vol. 5397, 2009, p. 197-214.

Research output: Contribution to journalArticle

@article{12048e6bd30244b8bb311cb2e32f6e5f,
title = "Abstracting and verifying strategy-proofness for auction mechanisms",
abstract = "We are interested in finding algorithms which will allow an agent roaming between different electronic auction institutions to antomatically 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 all 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 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 property-preserving abstraction methods were applied: the first is 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 range and number of agents.",
keywords = "model checking",
author = "Tadjouddine, {Emmanuel M} and Frank Guerin and Wamberto Vasconcelos",
year = "2009",
doi = "10.1007/978-3-540-93920-7_13",
language = "English",
volume = "5397",
pages = "197--214",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Abstracting and verifying strategy-proofness for auction mechanisms

AU - Tadjouddine, Emmanuel M

AU - Guerin, Frank

AU - Vasconcelos, Wamberto

PY - 2009

Y1 - 2009

N2 - We are interested in finding algorithms which will allow an agent roaming between different electronic auction institutions to antomatically 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 all 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 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 property-preserving abstraction methods were applied: the first is 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 range and number of agents.

AB - We are interested in finding algorithms which will allow an agent roaming between different electronic auction institutions to antomatically 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 all 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 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 property-preserving abstraction methods were applied: the first is 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 range and number of agents.

KW - model checking

U2 - 10.1007/978-3-540-93920-7_13

DO - 10.1007/978-3-540-93920-7_13

M3 - Article

VL - 5397

SP - 197

EP - 214

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -