Formal Verification of Diffusion Auctions

Fuente: arXiv
Salvato in:
Dettagli Bibliografici
Autori principali: Galimullin, Rustam, Mittelmann, Munyque, Perrussel, Laurent
Natura: Preprint
Pubblicazione: 2025
Soggetti:
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866908647174438912
author Galimullin, Rustam
Mittelmann, Munyque
Perrussel, Laurent
author_facet Galimullin, Rustam
Mittelmann, Munyque
Perrussel, Laurent
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2511_08765
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Formal Verification of Diffusion Auctions
Galimullin, Rustam
Mittelmann, Munyque
Perrussel, Laurent
Computer Science and Game Theory
Logic in Computer Science
F.4.1; I.2.4
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.
title Formal Verification of Diffusion Auctions
topic Computer Science and Game Theory
Logic in Computer Science
F.4.1; I.2.4
url https://arxiv.org/abs/2511.08765