Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
复制标题
拍卖机制的抽象和验证策略证明
DOI：
10.1007/978-3-540-93920-7_13
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
W. Vasconcelos
中科院分区：
文献类型：
--
作者：
E. Tadjouddine;Frank Guerin;W. Vasconcelos
我们感兴趣的是寻找算法，允许代理在不同的电子拍卖机构之间漫游，自动验证以前未见过的拍卖协议的博弈论性质。一个属性可以是协议对共谋或欺骗是健壮的，或者给定的策略是最优的。模型检查提供了一种执行此类证明的自动方法。然而，对于大型车型，它可能会受到状态空间爆炸的影响。为了提高模型检测的性能，抽象与SPIN模型检查器一起被使用。我们考虑了两个案例：Vickrey拍卖和易于处理的组合拍卖。数值结果表明了单纯依靠自旋的局限性。为了减少SPIN所需的状态空间，采用了两种保持属性的抽象方法：第一种是经典的程序切片技术，它去除了与属性无关的变量；第二种是用较小的抽象值替换大数据，可能是无穷大的变量值。这使我们能够对Vickrey拍卖的无限制出价范围和代理人数量进行模型检查。
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 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.