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 language | English |
---|---|
Title of host publication | Title AAMAS '08 Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems |
Place of Publication | Richland, SC |
Publisher | International Foundation for Autonomous Agents and Multiagent Systems |
Pages | 1613-1616 |
Number of pages | 4 |
Volume | 3 |
ISBN (Print) | 978-0-9817381-2-3 |
Publication status | Published - 2008 |
Event | 7th international joint conference on Autonomous agents and multiagent systems - Estoril, Portugal Duration: 12 May 2008 → 16 May 2008 |
Conference
Conference | 7th international joint conference on Autonomous agents and multiagent systems |
---|---|
Country/Territory | Portugal |
City | Estoril |
Period | 12/05/08 → 16/05/08 |