Formal Verification of Diffusion Auctions
Abstract
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 introduce a logical formalism that captures the dynamics of diffusion and its strategic dimension. Second, for such a logic, we provide model-checking procedures that allow one to verify properties as the Nash equilibrium, and that pave the way towards checking the existence of sellers' strategies. Third, we establish computational complexity results for the presented algorithms.
Cite
@article{arxiv.2511.08765,
title = {Formal Verification of Diffusion Auctions},
author = {Rustam Galimullin and Munyque Mittelmann and Laurent Perrussel},
journal= {arXiv preprint arXiv:2511.08765},
year = {2025}
}
Comments
This is an extended version of the paper with the same title that will appear in the proceedings of AAAI 2026. This version contains a technical appendix with proof details that, for space reasons, do not appear in the AAAI 2026 version