Abstracting and Verifying Strategy-Proofness for Auction Mechanisms

Emmanuel M Tadjouddine, Frank Guerin, Wamberto Vasconcelos

Research output: Chapter in Book/Report/Conference proceedingChapter

5 Citations (Scopus)

Abstract

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 performance of model checking, abstractions were used along with the Spinmodel 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
Title of host publicationDeclarative Agent Languages and Technologies VI
Subtitle of host publication6th International Workshop, DALT 2008, Estoril, Portugal, May 12, 2008, Revised Selected and Invited Papers
EditorsMatteo Baldoni, Tran Cao Son, M. Birna van Riemsdijk, Michael Winikoff
Place of PublicationHeidelberg, Germany
PublisherSpringer-Verlag
Pages197-214
Number of pages18
ISBN (Print)3540939199, 978-3540939191
DOIs
Publication statusPublished - 12 Jan 2009
Event6th International Workshop, DALT 2008 - Estoril, Portugal
Duration: 12 May 200812 May 2008

Publication series

NameLecture Notes in Computer Science
PublisherSpringer-Verlag
Number5397
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference6th International Workshop, DALT 2008
CountryPortugal
CityEstoril
Period12/05/0812/05/08

Fingerprint

Model checking
Network protocols
Explosions

Cite this

Tadjouddine, E. M., Guerin, F., & Vasconcelos, W. (2009). Abstracting and Verifying Strategy-Proofness for Auction Mechanisms. In M. Baldoni, T. C. Son, M. B. van Riemsdijk, & M. Winikoff (Eds.), Declarative Agent Languages and Technologies VI: 6th International Workshop, DALT 2008, Estoril, Portugal, May 12, 2008, Revised Selected and Invited Papers (pp. 197-214). (Lecture Notes in Computer Science; No. 5397). Heidelberg, Germany: Springer-Verlag. https://doi.org/10.1007/978-3-540-93920-7_13

Abstracting and Verifying Strategy-Proofness for Auction Mechanisms. / Tadjouddine, Emmanuel M; Guerin, Frank; Vasconcelos, Wamberto.

Declarative Agent Languages and Technologies VI: 6th International Workshop, DALT 2008, Estoril, Portugal, May 12, 2008, Revised Selected and Invited Papers. ed. / Matteo Baldoni; Tran Cao Son; M. Birna van Riemsdijk; Michael Winikoff. Heidelberg, Germany : Springer-Verlag, 2009. p. 197-214 (Lecture Notes in Computer Science; No. 5397).

Research output: Chapter in Book/Report/Conference proceedingChapter

Tadjouddine, EM, Guerin, F & Vasconcelos, W 2009, Abstracting and Verifying Strategy-Proofness for Auction Mechanisms. in M Baldoni, TC Son, MB van Riemsdijk & M Winikoff (eds), Declarative Agent Languages and Technologies VI: 6th International Workshop, DALT 2008, Estoril, Portugal, May 12, 2008, Revised Selected and Invited Papers. Lecture Notes in Computer Science, no. 5397, Springer-Verlag, Heidelberg, Germany, pp. 197-214, 6th International Workshop, DALT 2008, Estoril, Portugal, 12/05/08. https://doi.org/10.1007/978-3-540-93920-7_13
Tadjouddine EM, Guerin F, Vasconcelos W. Abstracting and Verifying Strategy-Proofness for Auction Mechanisms. In Baldoni M, Son TC, van Riemsdijk MB, Winikoff M, editors, Declarative Agent Languages and Technologies VI: 6th International Workshop, DALT 2008, Estoril, Portugal, May 12, 2008, Revised Selected and Invited Papers. Heidelberg, Germany: Springer-Verlag. 2009. p. 197-214. (Lecture Notes in Computer Science; 5397). https://doi.org/10.1007/978-3-540-93920-7_13
Tadjouddine, Emmanuel M ; Guerin, Frank ; Vasconcelos, Wamberto. / Abstracting and Verifying Strategy-Proofness for Auction Mechanisms. Declarative Agent Languages and Technologies VI: 6th International Workshop, DALT 2008, Estoril, Portugal, May 12, 2008, Revised Selected and Invited Papers. editor / Matteo Baldoni ; Tran Cao Son ; M. Birna van Riemsdijk ; Michael Winikoff. Heidelberg, Germany : Springer-Verlag, 2009. pp. 197-214 (Lecture Notes in Computer Science; 5397).
@inbook{00dd4e4ef87d4c37bf54ead9a5a91e86,
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 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 performance of model checking, abstractions were used along with the Spinmodel 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.",
author = "Tadjouddine, {Emmanuel M} and Frank Guerin and Wamberto Vasconcelos",
year = "2009",
month = "1",
day = "12",
doi = "10.1007/978-3-540-93920-7_13",
language = "English",
isbn = "3540939199",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
number = "5397",
pages = "197--214",
editor = "Matteo Baldoni and Son, {Tran Cao} and {van Riemsdijk}, {M. Birna} and Michael Winikoff",
booktitle = "Declarative Agent Languages and Technologies VI",

}

TY - CHAP

T1 - Abstracting and Verifying Strategy-Proofness for Auction Mechanisms

AU - Tadjouddine, Emmanuel M

AU - Guerin, Frank

AU - Vasconcelos, Wamberto

PY - 2009/1/12

Y1 - 2009/1/12

N2 - 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 performance of model checking, abstractions were used along with the Spinmodel 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 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 performance of model checking, abstractions were used along with the Spinmodel 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.

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

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

M3 - Chapter

SN - 3540939199

SN - 978-3540939191

T3 - Lecture Notes in Computer Science

SP - 197

EP - 214

BT - Declarative Agent Languages and Technologies VI

A2 - Baldoni, Matteo

A2 - Son, Tran Cao

A2 - van Riemsdijk, M. Birna

A2 - Winikoff, Michael

PB - Springer-Verlag

CY - Heidelberg, Germany

ER -