Formal Verification of Diffusion Auctions
Rustam Galimullin, Munyque Mittelmann, Laurent Perrussel
在扩散拍卖中,卖家可以利用底层社交网络来扩大参与,从而增加他们的潜在收入。 具体来说,卖家可以激励参与者通过网络传播有关拍卖的信息。 虽然文献中最近研究了此类拍卖的许多变体,但正式验证和战略推理观点尚未进行调查。 我们的贡献是三倍。 首先,我们引入一种逻辑形式主义,捕捉扩散的动态及其战略维度。 其次,对于这样的逻辑,我们提供模型检查程序,允许一个人验证属性作为纳什均衡,并为检查卖家策略的存在铺平道路。 第三,我们为呈现的算法建立计算复杂性结果。
In diffusion auctions, sellers can leverage an underlying social network to broaden participation, thereby increasing their potential revenue. Specifically, sellers can incentivise participants in their auction to diffuse information about the auction through the network. While numerous variants of such auctions have been recently studied in the literature, the formal verification and strategic reasoning perspectives have not been investigated yet. Our contribution is threefold. First, we introd...