Representing and reasoning about auctions

The goal of this paper is to propose a framework for representing and reasoning about the rules of auction-based protocols. Such a framework is of interest for building digital marketplaces based on this type of mechanism. Hence the framework should fulfill two requirements: (i) it should enable bidders to express their preferences over combinations of items and (ii) it should allow the mechanism designer to describe the rules governing the market, namely the legality of bids, the allocative choice, and the payment rule. To do so, we define a logical language in the spirit of the Game Description Language, namely Auction Description Language with a set of functions FB\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {F}_{\mathcal {B}}$$\end{document} (ADL[FB]\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$[\mathcal {F}_{\mathcal {B}}]$$\end{document}). ADL[FB]\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$[\mathcal {F}_{\mathcal {B}}]$$\end{document} is the first language for describing auctions in a logical framework. With our approach, each stage in a protocol is seen as an independent direct revelation mechanism. Our contribution is three-fold: first, we illustrate the general dimension by representing different kinds of protocols. Second, we show how this machine-processable language enables reasoning about auction properties, including playability, termination, and classical conditions from mechanism design (e.g., budget-balance and individual rationality). Finally, we develop a model-checking algorithm for ADL[FB]\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$[\mathcal {F}_{\mathcal {B}}]$$\end{document}, with complexity in PTIME when the functions in FB\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {F}_{\mathcal {B}}$$\end{document} can be computed in polynomial time.