Université de Toulouse - IRIT Toulouse, France Université Grenoble Alpes - LIG
Grenoble, France Université de Toulouse - IRIT Toulouse, France

#  A General Framework for the Logical Representation of Combinatorial
Exchange Protocols

Munyque Mittelmann<EMAIL_ADDRESS>,  Sylvain Bouveret
<EMAIL_ADDRESS>and  Laurent Perrussel<EMAIL_ADDRESS>
###### Abstract.

The goal of this paper is to propose a framework for representing and
reasoning about the rules governing a combinatorial exchange. Such a framework
is at first interest as long as we want to build up digital marketplaces based
on auction, a widely used mechanism for automated transactions. Combinatorial
exchange is the most general case of auctions, mixing the double and
combinatorial variants: agents bid to trade bundles of goods. Hence the
framework should fulfill two requirements: (i) it should enable bidders to
express their bids on combinations of goods and (ii) it should allow
describing the rules governing some market, namely the legal bids, the
allocation and payment rules. To do so, we define a logical language in the
spirit of the Game Description Language: the Combinatorial Exchange
Description Language is the first language for describing combinatorial
exchange in a logical framework. The contribution is two-fold: first, we
illustrate the general dimension by representing different kinds of protocols,
and second, we show how to reason about auction properties in this machine-
processable language.

###### Key words and phrases:

Logics for Multi-agents, Game Description Language, Auction-based Markets

##  1\. Introduction

Auction-based markets are widely used for automated business transactions.
There are numerous variants whether we consider single or multiple goods,
single or multiple units, single or double-side Klemperer (1999); Krishna
(2009). For a fixed set of parameters, the auction protocol, i.e., the
bidding, allocation, and payment rules, may also differ. Building intelligent
agents that can switch between different auctions and process their rules is a
key issue for building automated auction-based marketplaces. To do so,
auctioneers should at first describe the rules governing an auction and second
allow bidders to express complex bids. The aim of this paper is to propose
such language with clear semantics enabling us to derive properties.
Hereafter, we consider _combinatorial exchanges_ which are the most general
case for auctions, mixing double and combinatorial variants Lubin et al.
(2008).

More precisely, such _Combinatorial Exchange Description Language_ should
address the following dimensions:

Agent:

(i) one seller and multiple buyers, or vice-versa (single-side auctions); (ii)
multiple sellers and buyers (double-side auctions); (iii) multiple bidders
that can be both sellers and buyers (i.e., agents are traders);

Unit:

(i) single-unit or (ii) multi-unit auction;

Good type:

(i) single-good or (ii) multiple-goods; for that latter case a bid can
consider units and operators such as “1 table _and_ 4 chairs”.

Bidding protocol:

the auction protocol may be (i) one-shot (e.g., sealed-bid auction) or (ii)
iterative (e.g., ascending and descending auctions);

Allocation and payment:

the protocol should (i) detail how the winners are determined Xia et al.
(2005), (ii) quantify the money transfer (e.g., first price or
Vickrey–Clarke–Groves payment Parkes et al. (2005)).

In the spirit of the _General Game Playing_ Genesereth and Thielscher (2014)
where games are described with the help of a logical language, namely the
_Game Description Language_ (GDL), we propose the _Combinatorial Exchange
Description Language_ (CEDL) which is based on the Auction Description
Language (ADL) Mittelmann and Perrussel (2020). CEDL includes a bidding
language that can represent a wide range of auctions from a single-side,
single-unit and good auction (as a single-unit Vickrey Auction) to Iterative
Combinatorial Exchange Parkes et al. (2005). As for GDL and ADL, we propose a
precise semantics based on state-transition models, that gives a clear meaning
to the properties describing an auction. CEDL embeds the Tree-Based Bidding
Language Parkes et al. (2005), which generalizes known languages such as
XOR/OR Nisan (2000) to combinatorial exchange, where agents should be able to
express preferences for both buying and selling goods. To the best of our
knowledge, CEDL is the first framework offering a unified perspective on an
auction mechanism: (i) representation on how to bid and (ii) representation of
the protocol including allocation and payment. Such a framework offers two
benefits: (i) with this language, one can represent many kinds of auctions in
a compact way and (ii) the precise state-transition semantics can be used to
derive key properties.

CEDL extends ADL in numerous ways: ADL only focuses on one-side auctions and
can not represent double auctions; next, ADL is also unable to consider the
multiple-good dimension. These two dimensions are now considered in CEDL and
thus allow (i) to handle the problem of re-allocating goods, as in an
exchange, and (ii) to embed a bidding language to address combinatorial
markets.

The paper is organized as follows: in Section 2 we review the key components
for describing auctions; we next detail in Section 3 the bidding language that
will be embedded in CEDL and exhibit its key properties. Section 4 details
CEDL: semantics and syntax. Section 5 specifies two auction protocols with the
help of CEDL: a one-shot combinatorial exchange and a variant of ascending
combinatorial auction. We conclude by discussing related work and future work
for going further.

##  2\. Preliminaries

To describe a combinatorial exchange, we first define an auction signature,
that specifies the auction participants (the agents), the goods involved in
the auction and the propositions and variables describing each state of the
auction:

######  Definition 0.

An _auction signature_ $\mathcal{S}$ is a tuple $(N,G,\mathcal{A},\Phi,Y,I)$,
where: (i) $N=\\{1,2,\dots,n\\}$ is a nonempty finite set of agents (or
bidders); (ii) $G=\\{1,\dots,m\\}$ is a nonempty set of good types; (iii)
$\mathcal{A}$ is a nonempty finite set of actions or bid-trees; (iv)
$\Phi=\\{P,Q,\dots\\}$ is a finite set of atomic propositions specifying
individual features of a state; (v) $Y=\\{y_{1},y_{2},\dots\\}$ is a finite
set of numerical variables specifying numerical features in a state; (vi)
$I=\\{z:z_{min}\leq z\leq z_{max}$ & $z\in\mathbb{Z}\\}$ is a finite subset of
integer numbers, denoting the value range for any countable component of the
framework, for some arbitrary bounds $z_{min}\leq z_{max}$. We denote
$I_{+}=I\cap\mathbb{N}$ and $I_{-}=(I\setminus I_{+})\cup\\{0\\}$ as the non-
negative and non-positive subsets of $I$, respectively.

We will fix an auction signature $\mathcal{S}$ and all concepts will be based
on this signature, except if stated otherwise. Note that $z_{min}$ and
$z_{max}$, in the definition of $I$, should be large enough to represent the
total supply of goods being traded, _i.e._ , as we shall see below,
$\sum_{i\in N}\sum_{j\in G}x_{i,j}$, as well as the cumulative available money
among agents. Through the rest of this paper, we assume that is the case.111In
practice, we could have different bounds for each framework component (e.g.,
payment, trade). For notation simplicity, we assume a unique value range $I$.

A joint allocation is a tuple $X=(x_{1},\dots,x_{n})$, where
$x_{i}=(x_{i,1},\dots$, $x_{i,m})$ is an individual allocation for agent $i\in
N$ and $x_{i,j}\in I_{+}$ denotes the number of units $j\in G$ held by $i$. A
joint trade is a tuple $\Lambda=(\lambda_{1},\dots,\lambda_{n})$, where
$\lambda_{i}=(\lambda_{i,1},\dots,\lambda_{i,m})$ is an individual trade for
agent $i\in N$ and $\lambda_{i,j}\in I$ denotes the number of units $j\in G$
being traded by agent $i$. A trade can be seen as a change over an agent’s
initial allocation, resulting in a new one. A positive trade expresses how
many units of a good type were purchased and a negative trade represents how
many units were sold.

Given an auction signature, we now define a bidding language allowing agents
to express the combination of goods they are willing to buy (or sell) and the
value they intend to pay (or receive).

##  3\. Tree-Based Bidding Language

The Tree-Based Bidding Language (TBBL) Parkes et al. (2005); Lubin et al.
(2008) is a language designed for Combinatorial Exchange. It allows to
represent buyers and sellers demands in the same structure. We adopt TBBL as
it is a highly expressive and compact language for combinatorial bids as
stressed out by Cavallo _et al._ Cavallo et al. (2005) who compare TBBL to
alternative languages such as the OR language Boutilier and Hoos (2001).

Our bidding language $\mathcal{L}_{TBBL}$ only differs from the original
definition of TBBL in the fact that we assume all language components and
related optimization problems are bounded by $I$.

######  Definition 0.

A formula in $\mathcal{L}_{TBBL}$ is called a _bid-tree_ (or simply a bid) and
is generated by the following BNF:

$\beta::=\langle z,j,z\rangle\mid IC_{x}^{y}(\bar{\beta},z)$

where $\bar{\beta}::=\bar{\beta},\beta\mid\beta$ is a nonempty bid list, $j\in
G$, $z\in I$, and $x,y\in I_{+}$.

A bid in the form $\langle q,j,v\rangle$ is called a leaf and represents that
the agent is willing to buy (or sell) $q$ units of the good $j$ and pay (or
receive) $v$. The interval-choose (IC) operator defines a range on the number
of child nodes that must be satisfied. Thus, a bid $IC_{x}^{y}(\bar{\beta},v)$
indicates the agent is willing to pay (or receive) $v$ for the satisfaction of
at least $x$ and at most $y$ of his children nodes $\bar{\beta}$. The IC
operator can express logical connectors. For instance,
$IC^{1}_{1}(\bar{\beta},v)$ is equivalent to an $XOR$ operator between the
bids in the list $\bar{\beta}$. Let $s=|\bar{\beta}|$ (_i.e._ , the list
size), $IC^{s}_{s}(\bar{\beta},v)$ is equivalent to an AND operator and
$IC^{1}_{s}(\bar{\beta},v)$ is equivalent to an OR operator. For simplicity,
we denote $XOR(\bar{\beta},v)$, (resp. $AND(\bar{\beta},v)$,
$OR(\bar{\beta},v)$) as a shortcut for $IC^{1}_{1}(\bar{\beta},v)$ (resp.
$IC^{s}_{s}(\bar{\beta},v)$, $IC_{1}^{s}(\bar{\beta},v)$).

For instance, in Figure 1, agent $r1$ bids to buy $1$ or $2$ units of
$\mathsf{a}$ paying $2$ for each or to sell one unit of $\mathsf{b}$ receiving
$3$. Agent $r2$ bids an exclusive disjunction for either (i) to sell one unit
of $\mathsf{a}$ and receive $3$; or (ii) to sell $2$ units of $\mathsf{a}$
receiving $4$ and to buy one unit of $\mathsf{b}$ paying $2$. The node
representing (ii) has an additional value of $1$.

Figure 1. Examples of tree-bids for agents $r1$ and $r2$

Hereafter, we introduce some extra notations to characterize solutions and
winners. Let $T_{i}\in\mathcal{L}_{TBBL}$ be a bid-tree from bidder $i$, the
set $Node(T_{i})$ denotes all nodes in the tree, that is, all its inner bids,
including $T_{i}$ itself. Formally, if $T_{i}$ is in the form $\langle
q,j,v\rangle$, then $Node(T_{i})=\\{T_{i}\\}$. Otherwise, $T_{i}$ is in the
form $IC_{x}^{y}(\bar{\beta},v^{\prime})$ and $Node(T_{i})=\\{T_{i}\\}\cup
Node(\bar{\beta}_{1})\cup\cdots\cup Node(\bar{\beta}_{s})$, where
$s=|\bar{\beta}|$.

Let $\beta\in Node(T_{i})$, the set $Child(\beta)\subset Node(T_{i})$ denotes
the children of node $\beta$. If $\beta$ is in the form
$IC_{x}^{y}(\bar{\beta},v)$, then
$Child(\beta)=\\{\bar{\beta}_{1},\dots,\bar{\beta}_{s}\\}$, where
$s=|\bar{\beta}|$. Otherwise, $Child(\beta)=\\{\\}$. The leaves of a bid-tree
$T_{i}$ are denoted by $Leaf(T_{i})=\\{\langle q,j,v\rangle\in
Node(T_{i}):q\in I,v\in I$ & $j\in G\\}$. The value specified at node $\beta$
is denoted by $v_{i}(\beta)\in I$. If $\beta$ is in the form $\langle
q,j,v\rangle$, then $v_{i}(\beta)=v$. Otherwise, $\beta$ is in the form
$IC_{x}^{y}(\bar{\beta},v^{\prime})$ and $v_{i}(\beta)=v^{\prime}$. Finally,
the quantity of units of the good $j$ specified at a leaf $\beta=\langle
q,j,v\rangle$ is denoted $q_{i}(\beta,j)=q$. For any other $j^{\prime}\neq
j\in G$, $q_{i}(\beta,j^{\prime})=0$. For any node $\beta\not\in Leaf(T_{i})$
and $j\in G$, $q_{i}(\beta,j)=0$.

If $\beta$ is not a leaf (_i.e._ , $\beta\in Node(T_{i})\setminus
Leaf(T_{i})$), then it is in the form $IC_{x}^{y}(\bar{\beta})$ and we denote
by $\mathrm{x}_{\beta}$ and $\mathrm{y}_{\beta}$ the interval-choose
constraints $x$ and $y$, respectively.

###  3.1. Trade value and valid solutions

Given a tree $T_{i}$ from agent $i$, the value of a trade $\lambda_{i}\in
I^{m}$ is defined as the sum of the values in all satisfied nodes, where the
set of satisfied nodes is chosen to provide the maximal total value. Let
$sat_{i}(\beta)\in\\{0,1\\}$ denote whether a node $\beta\in Node(T_{i})$ is
satisfied and $sat_{i}=\\{\beta:sat_{i}(\beta)=1,$ for all $\beta\in
Node(T_{i})\\}$ denote the nodes satisfied in a solution.

A solution $sat_{i}$ is valid for a tree $T_{i}$ and trade $\lambda_{i}$,
written $sat_{i}\in valid(T_{i},\lambda_{i})$ if Rules 3.1 and R2 hold Lubin
et al. (2008):

$\displaystyle\mathrm{x}_{\beta}sat_{i}(\beta)\leq\sum_{\beta^{\prime}\in
Child(\beta)}sat_{i}(\beta^{\prime})\leq\mathrm{y}_{\beta}sat_{i}(\beta)$
$\displaystyle\forall\beta\in Node(T_{i})\setminus Leaf(T_{i})$
$\displaystyle\sum_{\beta\in
Leaf(T_{i})}q_{i}(\beta,j)sat_{i}(\beta)\leq\lambda_{i,j},\forall j\in G$ (R2)

Rule 3.1 ensures that no more and no less than the appropriate number of
children are satisfied for any node that is satisfied. Rule R2 requires that
the total increase in quantity of each item across all satisfied leaves is no
greater than the total number of units traded.

The total value of a trade $\lambda_{i}$, given a bid-tree $T_{i}$, is defined
as the solution to the following problem:

$\displaystyle
v_{i}(T_{i},\lambda_{i})=\mathop{\operatorname{argmax}}_{sat_{i}}\sum_{\beta\in
Node(T_{i})}v_{i}(\beta)sat_{i}(\beta)$ $\displaystyle\text{s.t.
}\ref{rule:R1},\ref{rule:R2}\text{ hold}$

###  3.2. Winner Determination

Given an auction signature, the bid-trees $T=(T_{1},\dots,T_{n})$ and a joint
allocation $X=(x_{1},\dots,x_{n})$, where $T_{i}\in\mathcal{L}_{TBBL}$ denotes
the bid-tree from agent $i\in N$, $x_{i}=(x_{i,1},\dots,x_{i,m})$ is the
individual allocation for $i$ and $x_{i,j}\in I_{+}$ for each good $j\in G$.

The Winner Determination (WD) defines a pair $(\Lambda,sat)$ obtained by the
solution to the following mixed-integer program Lubin et al. (2008):

$\displaystyle WD(T,X):\mathop{\operatorname{argmax}}_{\Lambda,sat}\sum_{i\in
N}\sum_{\beta\in Node(T_{i})}v_{i}(\beta)sat_{i}(\beta)$
$\displaystyle\text{s.t. }\lambda_{i,j}+x_{i,j}\geq 0,\forall i\in N,j\in G$
(C1) $\displaystyle\sum_{i\in N}\lambda_{i,j}=0,\forall j\in G$ (C2)
$\displaystyle sat_{i}\in valid(T_{i},\lambda_{i}),\forall i\in N$ (C3)
$\displaystyle sat_{i}(\beta)\in\\{0,1\\},\lambda_{i,j}\in I$ (C4)

where $sat=(sat_{1},\dots,sat_{n})$. Constraint C1 ensures that the joint
trade $\Lambda$ is feasible given $X$, that is no agent sells more items then
she initially hold. Constraint C2 imposes strict balance in the supply and
demand of goods. Constraint C3 ensures that each individual trade for an agent
$i$ is valid given her bid-tree. Constraint C4 defines the range for trades
and node satisfaction. We denote by $\Lambda(T,X)$ the joint trade $\Lambda$
in the solution $WD(T,X)=(\Lambda,sat)$, where $\lambda_{i}(T,X)$ denotes the
individual trade for agent $i$ and $\lambda_{i,j}(T,X)$ denotes the units of
good $j$ traded by agent $i$.

If there are two or more solutions for $WD(T,X)$, the trade $\Lambda(T,X)$
will be chosen w.r.t. some total order among the elements of $I^{mn}$. This
tie-breaking order is omitted to avoid overloading the notation. In the
examples, we assume this order is defined such as it is compatible with the
Pareto dominance relation Voorneveld (2003).

##### Bid-tree Equivalence

To ensure the finiteness of the framework, we define a maximal subset of TBBL,
such that there is no pair of bid-trees representing the exact same value for
every trade.

######  Definition 0.

Given the bid-trees $T_{i},T_{i}^{\prime}\in\mathcal{L}_{TBBL}$ from agent
$i\in N$, we say $T_{i}$ and $T_{i}^{\prime}$ are equivalent bid-trees,
denoted $T_{i}\approx_{tree}T_{i}^{\prime}$, if for all $\lambda_{i}\in
I^{m}$, $v_{i}(T_{i},\lambda_{i})=v_{i}(T_{i}^{\prime},\lambda_{i})$.

Notice that $\approx_{tree}$ is reflexive, symmetric and transitive.

######  Proposition 0.

Given $\mathcal{L}_{TBBL}^{\prime}\subset\mathcal{L}_{TBBL}$, if for all bid-
trees $\beta,\beta^{\prime}\in\mathcal{L}_{TBBL}^{\prime}$ where
$\beta\neq\beta^{\prime}$, $\beta\not\approx_{tree}\beta^{\prime}$ then
$\mathcal{L}_{TBBL}^{\prime}$ is finite.

###### Proof.

Let $i\in N$ be an agent and $s=|I|$ denote the size of $I$. Assume
$\mathcal{L}_{TBBL}^{\prime}\subset\mathcal{L}_{TBBL}$ such that for all
$\beta_{i},\beta_{i}^{\prime}\in\mathcal{L}_{TBBL}$, where
$\beta_{i}\neq\beta_{i}^{\prime}$, we have
$\beta_{i}\not\approx_{tree}\beta_{i}^{\prime}$. That is,
$v_{i}(\beta_{i},\lambda_{i})\neq v_{i}(\beta_{i}^{\prime},\lambda_{i})$ for
some $\lambda_{i}\in I^{m}$.

For each trade $\lambda_{i}\in I^{m}$, there are $s$ possibilities of distinct
values $v_{i}(\beta_{i},\lambda_{i})$. Furthermore, there are $s^{m}$ distinct
trades. Thus, there may be at most $s^{s^{m}}$ non equivalent bids-tree in
$\mathcal{L}_{TBBL^{\prime}}$ and $\mathcal{L}_{TBBL^{\prime}}$ is finite. ∎

Let $\mathcal{L}_{TBBLf}$ be a maximal subset of $\mathcal{L}_{TBBL}$ such
that $\beta\not\approx_{tree}\beta^{\prime}$, for all
$\beta,\beta^{\prime}\in\mathcal{L}_{TBBL}$, where $\beta\neq\beta^{\prime}$.

######  Corollary 0.

$\mathcal{L}_{TBBLf}$ is finite and $|\mathcal{L}_{TBBLf}|=|I|^{|I|^{m}}$.

A maximal subset of TBBL without equivalent bids is finite, but its size grows
exponentially over the size of $I$ and the quantity $m$ of goods in the
auction.

##  4\. Combinatorial Exchange Description Language

The _Combinatorial Exchange Description Language_ (CEDL) is a framework for
specification of auction-based markets and it is composed by a State-
Transition Model and a logical language. Next, we present the model, the
common legality constraints and the language’s syntax and semantics.

###  4.1. State-Transition Model

Given an auction signature and the bidding language, we define the auction
protocol through a state-transition model. It allows us to represent the key
aspects of an auction, at first the legal bids and how to update the auction
state.

Let $\mathcal{A}\subset\mathcal{L}_{TBBL}$ be a finite set of actions. It is
not a limitation to assume $\mathcal{A}$ finite since a maximal subset of TBBL
without equivalent bid-trees is finite. We denote $noop=_{def}\langle
0,g,0\rangle$ as the action of not bidding for any good, for some arbitrary
$g\in M$.

######  Definition 0.

A state-transition ST-model $M$ is a tuple $(W,\bar{w},T,L$,
$U,\pi_{\Phi},\pi_{Y})$, where: (i) $W$ is a nonempty set of states; (ii)
$\bar{w}\in W$ is the initial state; (iii) $T\subseteq W$ is a set of terminal
states; (iv) $L\subseteq W\times N\times\mathcal{A}$ is a legality relation,
describing the legal actions at each state, let
$L(w,i)=\\{a\in\mathcal{A}\mid(w,i,a)\in L\\}$ be the set of all legal actions
for agent $i$ at state $w$; (v) $U:W\times\mathcal{A}^{n}\rightarrow W$ is an
update function, given $d\in\mathcal{A}^{n}$, let $d(i)$ be the individual
action for agent $i$ in the joint action $d$; (vi) $\pi_{\Phi}:W\to 2^{\Phi}$
is the valuation function for the state propositions; (vii) $\pi_{Y}:W\times
Y\to\mathbb{Z}$, is the valuation function for the numerical variables.

######  Definition 0.

Given an ST-model $M=(W,\bar{w},T,L,U,$ $\pi_{\Phi},\pi_{Y})$, a path is a
sequence of states and joint actions
$\bar{w}\accentset{d_{1}}{\to}w_{1}\accentset{d_{2}}{\to}\dots\accentset{d_{t}}{\to}w_{t}\accentset{d_{t+1}}{\to}\dots$
such that for any $t\geq 1$: (i) $w_{0}=\bar{w}$; (ii) $w_{t}\neq w_{0}$;
(iii) $d_{t}(i)\in L(w_{t-1})$ for any $i\in N$, (iv)
$w_{t}=U(w_{t-1},d_{t})$; and (v) if $w_{t-1}\in T$, then $w_{t-1}=w_{t}$.

Let $\delta[t]$ denote the $t$-th reachable state of $\delta$,
$\theta(\delta,t)$ denote the joint action performed at stage $t$ of $\delta$;
and $\theta_{i}(\delta,t)$ denote the action of agent $i$ performed at stage
$t$ of $\delta$, and $\delta[0,t]$ denote the finite prefix
$\bar{w}\accentset{d_{1}}{\to}w_{1}\accentset{d_{2}}{\to}\dots\accentset{d_{t}}{\to}w_{t}$.
A path $\delta$ is complete if $\delta[e]\in T$, for some $e>0$. After
reaching a terminal state $\delta[e]$, for any $e^{\prime}>e$,
$\delta[e^{\prime}]=\delta[e]$.

###  4.2. Language Syntax

Each payment, allocation and trade should be represented as a numerical
variable $y\in Y$. We assume the predefined variables set
$\\{payment_{i},alloc_{i,j},trade_{i,j}:i\in N,j\in G\\}\subseteq Y$. Let
$z\in\mathcal{L}_{z}$ be a numerical term defined as follows:

$\displaystyle z::=z^{\prime}\mid add(z,z)\mid sub(z,z)\mid min(z,z)\mid
max(z,z)\mid times(z,z)\mid$ $\displaystyle y\mid
win_{i,j}(\bar{\beta},\bar{Z})\mid value_{i}(\beta)\mid
value_{i}(\beta,\bar{z})\mid qtd_{i}(\beta,j)$

where $z^{\prime}\in I,y\in Y$, $i\in N$, $j\in G$, $\beta\in\mathcal{A}$,
$\bar{\beta}\in\mathcal{A}^{n}$ $\bar{z}\in\mathcal{L}_{z}^{m}$, and
$\bar{Z}\in\mathcal{L}_{z}^{mn}$.

The terms $add(z_{1},z_{2})$, $sub(z_{1},z_{2})$, $times(z_{1}$, $z_{2})$,
$min(z_{1},z_{2})$ and $max(z_{1},z_{2})$ specify the corresponding
mathematical operation or function. For agent $i$ and good $j$, the value of a
bid $\beta$, the value of $\beta$ given a trade $\bar{z}$, the quantity of $j$
in bid $\beta$ and the trade $\lambda_{i,j}(\bar{\beta},\bar{Z})$ are denoted
$value_{i}(\beta)$, $value_{i}(\beta,\bar{z})$, $qtd_{i}(\beta,j)$ and
$win_{i,j}$, resp.

The Combinatorial Exchange Description language is denoted by
$\mathcal{L}_{CEDL}$ and a formula $\varphi$ in $\mathcal{L}_{CEDL}$ is
defined by the following BNF grammar:

$\displaystyle\varphi::=p\mid initial\mid terminal\mid legal_{i}(\beta)\mid
does_{i}(\beta)\mid$
$\displaystyle\neg\varphi\mid\varphi\land\varphi\mid\bigcirc\varphi\mid
z<z\mid z>z\mid z=z\mid rest_{i}(res,\beta)$

where $p\in\Phi$, $i\in N$, $res\in\\{buyer,seller,good,unit\\}$,
$\beta\in\mathcal{A}$ and $z\in\mathcal{L}_{z}$.

Intuitively, $initial$ and $terminal$ specify the initial terminal states,
resp.; $legal_{i}(\beta)$ asserts that agent $i$ is allowed to take action
$\beta$ at the current state and $does_{i}(\beta)$ asserts that agent $i$
takes action $\beta$ at the current state. The formula $\bigcirc\varphi$ means
“$\varphi$ holds at the next state”. The formulas $z_{1}>z_{2}$,
$z_{1}<z_{2}$, $z_{1}=z_{2}$ mean that a numerical term $z_{1}$ is greater,
less and equal to a numerical term $z_{2}$, resp. The formula
$rest_{i}(res,\beta)$ specifies whether the bid $\beta$ from agent $i$
respects the restriction $res\in\\{buyer,seller,good,unit\\}$. The restriction
$buyer$ specifies that $\beta$ cannot have negative quantities or prices.
Similarly, the restriction $seller$ specifies that $\beta$ cannot have
positive quantities or prices. The restriction $good$ states that $\beta$
should be a leaf node. Finally, the restriction $unit$ says any leaf node in
$\beta$ can only demand a single unit from a good type.

Other connectives $\lor,\to,\leftrightarrow,\top$ and $\bot$ are defined by
$\neg$ and $\land$ in the standard way. The comparison operators $\leq$,
$\geq$ and $\neq$ are defined by $\lor,>,<$ and $=$. The extension of the
comparison operators $>,<,=$, $\leq$, $\geq$, $\neq$ and numerical terms
$max(z_{1},z_{2}),min(z_{1},z_{2})$, $add(z_{1},z_{2})$, $sub(z_{1},z_{2})$,
$times(z_{1},z_{2})$ to multiple arguments is straightforward.

We define $trade_{i}$ such that it denotes the list of numerical terms
representing $i$’s trades as follows:
$trade_{i}=_{def}trade_{i,1},\dots,trade_{i,m}$. The list $alloc^{i}$ is
defined in a similar way. Note that $trade_{i}$, $alloc_{i}$
$\in\mathcal{L}_{z}^{m}$. Given a joint allocation $X$ and a list of bids $T$,
we write $trade_{i}=win_{i}(X,T)$ to denote the formula $\bigwedge_{j\in
G}trade_{i,j}=win_{i,j}(X,T)$. Assume the bids $T=(T_{1},\dots,T_{n})$, where
$T_{i}\in\mathcal{A}$ is a bid associated to the agent $i\in N$. The formula
$does(T)=_{def}\bigwedge_{i\in N}does_{i}(T_{i})$ represents that the agents
perform the joint action $T$.

###  4.3. Language Semantics

The semantics for the CEDL language is given in two steps. First, we define
Function $f$ to compute the meaning of numerical terms $z\in\mathcal{L}_{z}$
in some specific state. Next, a formula $\varphi\in\mathcal{L}_{CEDL}$ is
interpreted with respect to a step in a path.

######  Definition 0.

Given an ST-model $M$, define Function $f:\mathcal{L}_{z}\times
W\rightarrow\mathbb{Z}$, assigning any $z\in\mathcal{L}_{z}$ and state $w\in
W$ to a number in $\mathbb{Z}$:

If $z$ is in the form $add(z^{\prime},z^{\prime\prime})$,
$sub(z^{\prime},z^{\prime\prime})$, $min(z^{\prime},z^{\prime\prime})$,
$max(z^{\prime},z^{\prime\prime})$, or $times(z^{\prime},z^{\prime\prime})$,
then $f(z,w)$ is defined through the application of the corresponding
mathematical operators and functions over $f(z^{\prime},w)$ and
$f(z^{\prime\prime},w)$. Otherwise, $f(z,w)$ is defined as follows:

$f(z,w)=\begin{dcases}z\text{ if }z\in\mathbb{Z}\\\ \pi_{Y}(w,z)\text{ if
}z\in Y\\\ \lambda_{i,j}(T,X)\text{ if }\\\ \quad
z=win_{i,j}(T,X)\end{dcases}f(z,w)=\begin{dcases}v_{i}(T_{i})\text{ if
}z=value_{i}(T_{i})\\\ v_{i}(T_{i},\bar{z})\text{ if
}z=value_{i}(T_{i},\bar{z})\\\ q_{i}(T_{i},j)\text{ if
}z=qtd_{i}(T_{i},j)\end{dcases}$

######  Definition 0.

Let $M$ be an ST-Model. Given a path $\delta$ of $M$, a stage $t$ on $\delta$
and a formula $\varphi\in\mathcal{L}_{CEDL}$, we say $\varphi$ is true (or
satisfied) at $t$ of $\delta$ under $M$, denoted by
$M,\delta,t\models\varphi$, according to the following definition:

$\begin{array}[]{lllll}M,\delta,t\models
p&&\text{iff}&&p\in\pi_{\Phi}(\delta[t])\\\
M,\delta,t\models\neg\varphi&&\text{iff}&&M,\delta,t\not\models\varphi\\\
M,\delta,t\models\varphi_{1}\land\varphi_{2}&&\text{iff}&&M,\delta,t\models\varphi_{1}\text{
and }M,\delta,t\models\varphi_{2}\\\ M,\delta,t\models
initial&&\text{iff}&&\delta[t]=\bar{w}\\\ M,\delta,t\models
terminal&&\text{iff}&&\delta[t]\in T\\\ M,\delta,t\models
legal_{i}(a)&&\text{iff}&&a\in L(\delta[t],i)\\\ M,\delta,t\models
does_{i}(a)&&\text{iff}&&\theta_{i}(\delta,t)=a\\\
M,\delta,t\models\bigcirc\varphi&&\text{iff}&&M,\delta,t+1\models\varphi\\\
M,\delta,t\models
z_{1}>z_{2}&&\text{iff}&&f(z_{1},\delta[t])>f(z_{2},\delta[t])\\\
M,\delta,t\models
z_{1}<z_{2}&&\text{iff}&&f(z_{1},\delta[t])<f(z_{2},\delta[t])\\\
M,\delta,t\models
z_{1}=z_{2}&&\text{iff}&&f(z_{1},\delta[t])=f(z_{2},\delta[t])\\\
M,\delta,t\models rest_{i}(buyer,a)&&\text{iff}&&\forall\beta\in
Node(a),v_{i}(\beta)\geq 0\text{ and }\\\ &&&&\forall l\in Leaf(a),\exists
j\in G,q_{i}(l,j)\geq 0\\\ M,\delta,t\models
rest_{i}(seller,a)&&\text{iff}&&\forall\beta\in Node(a),v_{i}(\beta)\leq
0\text{ and }\\\ &&&&\forall l\in Leaf(a),\exists j\in G,q_{i}(l,j)\leq 0\\\
M,\delta,t\models rest_{i}(good,a)&&\text{iff}&&Child(a)=\\{\\}\\\
M,\delta,t\models rest_{i}(unit,a)&&\text{iff}&&\forall\beta\in
Leaf(a),\exists j\in G,q_{i}(\beta,j)\in\\{-1,1\\}\end{array}$

A formula $\varphi$ is globally true through $\delta$, denoted by
$M,\delta\models\varphi$, if $M,\delta,t\models\varphi$ for any stage $t$ of
$\delta$. A formula $\varphi$ is globally true in an ST-Model $M$, written
$M\models\varphi$, if $M,\delta\models\varphi$ for all paths $\delta$ in $M$.
Finally, let $\Sigma$ be a set of formulas in $\mathcal{L}_{CEDL}$, then $M$
is a model of $\Sigma$ if $M\models\varphi$ for all $\varphi\in\Sigma$.

The following propositions show that if a player bids at a stage in a path,
then (i) she does not bid anything else at the same stage and (ii) the bid is
legal. Additionally, the value of the bid-tree $noop$ is zero. Notice that an
agent bidding $noop$ does not imply her payment will be zero (_e.g_ , there
may be fees for participating).

######  Proposition 0.

For each agent $i\in N$ and each bid-tree $\beta\in\mathcal{A}$,

  1. (1)

$M\models does_{i}(\beta)\rightarrow\neg does_{i}(\beta^{\prime})$, for any
$\beta^{\prime}\in\mathcal{A}$ such that $\beta^{\prime}\neq\beta$

  2. (2)

$M\models does_{i}(\beta)\rightarrow legal_{i}(\beta)$

###### Proof.

For Statement 1, assume $M,\delta,t\models does_{i}(\beta)$ iff
$\theta_{r}(\delta,t)=\beta$. Then for any
$\beta^{\prime}\neq\beta\in\mathcal{A}_{ce}$,
$\theta_{r}(\delta,t)=\beta^{\prime}$ and $M,\delta,t\models\neg
does_{i}(\beta^{\prime})$.

Let us verify Statement 2. Assume $M,\delta,t\models does_{i}(\beta)$, then
$\theta_{r}(\delta,t)=\beta$ and by the definition of $\delta$, $\beta\in
L(\delta[t],i)$ and $M,\delta,t\models legal_{i}(\beta)$. ∎

######  Lemma 0.

For each agent $i\in N$, each bid-tree $\beta\in\mathcal{A}$ and each
$\bar{z}\in I^{m}$, $M\models value_{i}(noop)=0\land
value_{i}(noop,\bar{z})=0$.

###### Proof.

We consider Statement 1. Remind $noop$ denotes a leaf bid $\langle
0,g,0\rangle$, where $g\in M$. Thus, $v_{i}(noop)=0$,
$f(value_{i}(noop),\delta[t])=0$ and $M,\delta,t\models value_{i}(noop)=0$.
Let $\bar{z}\in I^{m}$. The value of $\bar{z}$ given $noop$, i.e.,
$v_{i}(noop,\bar{z})$, is the maximal sum of $v_{i}(\beta)sat_{i}(\beta)$ in a
solution $sat_{i}$, for all $\beta\in Node(noop)$. Since
$Node(noop)=\\{noop\\}$ and $value_{i}(noop)=0$, for any solution $sat_{i}$,
$v_{i}(noop,\bar{z})=0$ and $M,\delta,t\models value_{i}(noop,\bar{z})=0$. ∎

##  5\. Representing Mechanism Properties and Auction-based Protocols

Let us first show how to represent some classical but important properties
from Mechanism Design, namely budget-balance, no-deficit and individual
rationality conditions.

##### Budget-Balanced Mechanisms

A mechanism is Budget-Balanced (BB) if the cumulative payment among the
bidders is zero, for every valuations they may have Mishra and Sharma (2018).
Given an ST-model $M$, this condition is denoted by the validity of the
following formula: $BB=_{def}add(payment_{1},\dots,payment_{n})=0$.

##### No-deficit Mechanisms

A mechanism where only the designer can earn revenue satisfies no-deficit
Mishra and Sharma (2018). The no-deficit condition is a relaxation from BB,
where the cumulative payment among the bidders cannot be negative. In CEDL, an
ST-model $M$ satisfies the no-deficit condition according to the validity of
the following formula: $noDeficit=_{def}add(payment_{1},\dots,payment_{n})\geq
0$.

##### Individual Rationality

A mechanism is individually rational if agents can always achieve at least as
much utility as from participating as without participating Parkes and Ungar
(2001). To represent such condition, we assume each agent $i\in N$ has a
private valuation in $I$ for each individual trade $\lambda_{i}\in I^{m}$,
denoted $\vartheta_{i}(\lambda_{i})$. As Lubin et al. (2008), we also assume
the agents have monotonic valuation, so that
$\vartheta_{i}(\lambda_{i}^{\prime})\geq\vartheta_{i}(\lambda_{i})$, for any
trade $\lambda_{i}^{\prime}\geq\lambda_{i}$ (_i.e_ ,
$\vartheta_{i,j}(\lambda_{i,j}^{\prime})\geq\vartheta_{i,j}(\lambda_{i,j}$),
for each $j$). The agent’s utility is quasi-linear, denoted
$u_{i}(\lambda_{i},p_{i})=\vartheta_{i}(\lambda_{i})-p_{i}$, where $p_{i}$
denotes $i$’s payment. Rephrased in terms of ST-model, we say a model $M$ is
Individual Rational $IR$ if it is Individual Rational $IR_{i}$ for each agent
$i\in N$ in each path $\delta$ in $M$ and stages $t$ in $\delta$.

A stage $t$ of $\delta$ is $IR_{i}$, written $M,\delta,t\models IR_{i}$ if
there is a path $\delta^{\prime}$ in $M$ such that
$\delta[0,t]=\delta^{\prime}[0,t]$,
$\theta_{r}(\delta,t)=\theta_{r}(\delta^{\prime},t)$, for all $r\in
N\setminus\\{i\\}$, and $M,\delta^{\prime},t\models
utility_{i}(trade_{i},payment_{i})=x\rightarrow\bigcirc
utility_{i}(trade_{i},payment_{i})\geq x$, for each $x\in I$. In other words,
IR requires meta-reasoning as choices among paths have to be considered.

Let us now represent in CEDL two types of auction-based markets: a One-Shot
Combinatorial Exchange and a Simultaneous Ascending Auction. For both of them,
we detail the rules representation, the semantic representation and we revisit
the Mechanism Design conditions.

###  5.1. Representing a Combinatorial Exchange

To represent a One-Shot Combinatorial Exchange with multiple units of
$\mathsf{m}$ goods and $\mathsf{n}$ players, we first describe the auction
signature, written
$\mathcal{S}_{ce}=(N_{ce},G_{ce},\mathcal{A}_{ce},\Phi_{ce},Y_{ce},I_{ce})$,
where $N_{ce}=\\{1,\dots,\mathsf{n}\\}$, $G_{ce}=\\{1,\dots,\mathsf{m}\\}$,
$\mathcal{A}_{ce}\subseteq\mathcal{L}_{TBBLf}$, $\Phi_{ce}=\\{bidRound\\}$,
$Y_{ce}=\\{alloc_{i,j},trade_{i,j}$, $payment_{i}:i\in N_{ce},j\in G_{ce}\\}$,
and $I_{ce}\subset\mathbb{Z}$.

Each instance of a One-Shot Combinatorial Exchange is specific and is defined
with respect to $\mathcal{A}_{ce}$, $I_{ce}$ and the constant values
$\mathsf{n,m}\in I_{ce,+}\setminus\\{0\\}$ (the size of $N_{ce}$ and $G_{ce}$,
resp.), and $\mathsf{x}_{i,j}\in I_{ce,+}$, for each $i\in N_{ce}$ and $j\in
G_{ce}$. Each constant $\mathsf{x}_{i,j}$ represents the quantity of units of
$j$ initially held by agent $i$. The rules of a One-Shot Combinatorial
Exchange are represented by CEDL-formulas as shown in Figure 2.

(1) $initial\rightarrow bidRound\land\bigwedge_{i\in N_{ce}}(payment_{i}=0$
$\land$ $\bigwedge_{j\in G_{ce}}trade_{i,j}=0)$ (2)
$terminal\leftrightarrow\neg initial$ (3) $terminal\rightarrow
legal_{i}(noop)$, for each $i\in N_{ce}$ (4) $initial\rightarrow
legal_{i}(\beta)$, for each $i\in N_{ce}$, $\beta\in\mathcal{A}_{ce}$ (5)
$does(T_{1},\dots,T_{\mathsf{n}})\land
initial\rightarrow\bigcirc(\bigwedge_{i\in
N_{ce}}trade_{i}=win_{i}(T_{1},\dots,T_{\mathsf{n}},\mathsf{x}_{1,1},\dots,\mathsf{x}_{\mathsf{n,m}}))$,
for each $(T_{1}$, $\dots$, $T_{\mathsf{n}})\in\mathcal{A}^{\mathsf{n}}_{ce}$
(6) $does_{i}(\beta)\land initial\rightarrow\bigcirc
payment_{i}=value_{i}(\beta$, $trade_{i})$, for each $i\in N_{ce}$,
$\beta\in\mathcal{A}_{ce}$ (7) $terminal\land y=x\rightarrow\bigcirc y=x$, for
each $y\in Y_{ce}$, $x\in I_{ce}$ (8)
$alloc_{i,j}=add(\mathsf{x}_{i,j},trade_{i,j})$, for each $i\in N_{ce}$, $j\in
G_{ce}$ (9) $\bigcirc\neg bidRound$

Figure 2. A Combinatorial Exchange represented by $\Sigma_{ce}$

In the initial state, the trade and payment are zero for every agent and good
(Rule 1). Any state that is not initial is terminal (Rule 2). The proposition
$bidRound$ helps to distinguish the initial state from the terminal state
where no trade or payment were assigned to any agent (_e.g_ , when all agents
bid $noop$). Once in a terminal state, players can only do $noop$. Otherwise,
they can bid any bid-tree $\beta\in\mathcal{A}_{ce}$ (Rules 3 and 4). If a
list of bid-trees is the joint action performed in the initial sate, then in
the next state each agent receives an individual trade, which is assigned by
the WD over the initial allocations and the bid-trees (Rule 5). After
performing a bid in the initial state, the payment for an agent will be the
value of her trade given her bid (Rule 6). No numerical variable has its value
changed after reaching a terminal state (Rule 7). The allocation for an agent
is the quantity of goods she initially held plus her trade (Rule 8). Finally,
the proposition $bidRound$ is always false in the next state (Rule 9).

##### Representing as a model

Next, we address the model representation. Let $\mathscr{M}_{ce}$ be the set
of ST-models $M_{ce}$ defined for any
$\mathcal{A}_{ce}\subseteq\mathcal{L}_{TBBLf}$, $I_{ce}\subset\mathbb{Z}$, and
the constants $\mathsf{m},\mathsf{n}\in I_{ce,+}\setminus\\{0\\}$ and
$\mathsf{x}_{i,j}\in I_{ce,+}$, for each $i\in N_{ce}$ and $j\in G_{ce}$.

Each $M_{ce}$ is defined as:

  * •

$W_{ce}=\\{\langle
b,x_{1,1},\dots,x_{\mathsf{n,m}},\lambda_{1,1},\dots,\lambda_{\mathsf{n,m}},p_{1},\dots,p_{\mathsf{n}}\rangle:b\in\\{0$,
$1\\},x_{i,j}\in I_{ce,+}$ & $p_{i},\lambda_{i,j}\in I_{ce}$ & $i\in N_{ce}$ &
$j\in G_{ce}\\}$;

  * •

$\bar{w}_{ce}=\langle
1,\mathsf{x}_{1,1},\dots,\mathsf{x}_{\mathsf{n,m}},0,\dots,0,0,\dots,0\rangle$;

  * •

$T_{ce}=\\{w:w\in W_{ce}$ & $w\neq\bar{w}_{ce}\\}$;

  * •

$L_{ce}=\\{(w,i,noop):i\in N_{ce}$ & $w\in T_{ce}\\}\cup\\{(\bar{w}_{ce},i,$
$\beta):\beta\in\mathcal{A}_{ce}$ & $i\in N_{ce}\\}$;

  * •

$U_{ce}$ is defined as follows: for all $w=\langle
b,x_{1,1},\dots,x_{\mathsf{n,m}},\lambda_{1,1},\dots,$
$\lambda_{\mathsf{n,m}},p_{1},\dots,p_{\mathsf{n}}\rangle\in W_{ce}$ and for
all $d\in\mathcal{A}^{\mathsf{n}}_{ce}$:

    * –

If $w=\bar{w}_{ce}$, then $U_{ce}(w,d)=\langle
0,x_{1,1}^{\prime},\dots,x_{\mathsf{n,m}}^{\prime},\lambda_{1,1}^{\prime},\dots$,
$\lambda_{\mathsf{n,m}}^{\prime},p_{1}^{\prime},\dots,p_{\mathsf{n}}^{\prime}\rangle$,
where
$\lambda_{i,j}^{\prime}=\lambda_{i,j}(d,\mathsf{x}_{1,1},\dots,\mathsf{x}_{\mathsf{n,m}})$;
$x_{i,j}^{\prime}=\mathsf{x}_{i,j}+\lambda_{i,j}^{\prime}$; and
$p_{i}^{\prime}=v_{i}(d(i),\lambda_{i,1}^{\prime},\dots,\lambda_{i,\mathsf{m}}^{\prime})$,
for each $i\in N_{ce}$ and $j\in G_{ce}$;

    * –

Otherwise, $U_{ce}(w,d)=w$.

  * •

For each $w\in W_{ce}$, $i\in N_{ce}$ and $j\in G_{ce}$, $\pi_{Y,ce}(w$,
$trade_{i,j})=\lambda_{i,j}$; $\pi_{Y,ce}(w,alloc_{i,j})=x_{i,j}$;
$\pi_{Y,ce}(w,payment_{i})=p_{i}$; and $\pi_{\Phi,ce}(w)=\\{bidRound:b=1\\}$.

Hereafter, we assume an instance of $M_{ce}\in\mathscr{M}_{ce}$ and
$\Sigma_{ce}$ for some $\mathcal{A}_{ce}\subseteq\mathcal{L}_{TBBLf}$,
$I_{ce}\subset\mathbb{Z}$, $\mathsf{m},\mathsf{n}\in I_{ce,+}\setminus\\{0\\}$
and $\mathsf{x}_{i,j}\in I_{ce,+}$, where $i\in N_{ce}$, $j\in G_{ce}$.

######  Example 0.

Let $M_{ce}\in\mathscr{M}_{ce}$, where (i) $\mathsf{n}=2$ and the agents are
denoted by $r1$ and $r2$, (ii) $\mathsf{m}=2$ and the good types are denoted
by $\mathsf{a}$ and $\mathsf{b}$, and (iii) $\mathsf{x}_{r1,\mathsf{a}}=0$,
$\mathsf{x}_{r1,\mathsf{b}}=1$, $\mathsf{x}_{r2,\mathsf{a}}=2$ and
$\mathsf{x}_{r2,\mathsf{b}}=0$, _i.e_ , at the beginning of the auction, agent
$r1$ has $1$ unit of $\mathsf{b}$ and agent $r2$ has $2$ units of
$\mathsf{a}$. Figure 3 illustrates a path in $M_{ce}$, where the agents
perform the bids previously introduced in Figure 1. In state $w_{0}$, all the
payments and trades are zero. Their joint bid leads to state $w_{1}$, where
the joint trade obtained by the winner determination is $(2,-1,-2,1)$. The
tie-breaking ensures that the joint trade is unique. Given the joint trade,
the allocation for agent $r1$ is $2$ units of $\mathsf{a}$ and the allocation
for agent $r2$ is $1$ unit of $\mathsf{b}$. Since $w_{1}$ is terminal, the
agents can only bid $noop$ and the state that succeeds $w_{1}$ is $w_{1}$
itself.

Figure 3. A Path in $M_{ce}$, with 2 bidders and $2$ goods

Let us now evaluate the protocol. First, Proposition 5.1 shows that $M_{ce}$
is a sound representation of $\Sigma_{ce}$ .

######  Proposition 0.

$M_{ce}$ is an ST-model and it is a model of $\Sigma_{ce}$.

###### Proof.

_(Sketch)_ It is routine to check that $M_{ce}$ is actually an ST-model. Given
a path $\delta$ in $M_{ce}$ and a stage $t$ of $\delta$, we need to show that
$M_{ce},\delta,t\models\varphi$, for each $\varphi\in\Sigma_{ce}$.

Let us verify Rule 1. Assume $M_{ce},\delta,t\models initial$, then
$\delta[t]=\bar{w}_{ce}$, i.e., $\delta[t]=\langle
1,\mathsf{x}_{1,1},\dots,\mathsf{x}_{\mathsf{n,m}},0,\dots,0,0,\dots,0\rangle$.
By the definitions of $\pi_{Y,ce}$ and $\pi_{\Phi,ce}$,
$\pi_{\Phi,ce}(\bar{w}_{ce})=\\{bidRound\\}$,
$\pi_{Y,ce}(\bar{w}_{ce},payment_{i})=0$ and
$\pi_{Y,ce}(\bar{w}_{ce},trade_{i,j})=0$ for all $i\in N_{ce}$ and $j\in
G_{ce}$. Thus, $M_{ce},\delta,t\models bidRound\land\bigwedge_{i\in
N_{ce}}payment_{i}=0\land\bigwedge_{j\in G_{ce}}trade_{i,j}=0$.

Now we verify Rule 4. Assume $M_{ce},\delta,t\models initial$, then
$\delta[t]=\bar{w}_{ce}$ and for all $i\in N_{ce}$ and
$\beta\in\mathcal{A}_{ce}$, $(\bar{w}_{ce},i,\beta)\in L_{ce}$. Thus,
$M_{ce},\delta,t\models legal_{i}(\beta)$.

Then we consider Rule 5. $M_{ce},\delta,t\models
does(T_{1},\dots,T_{\mathsf{n}})\land initial$, for
$(T_{1},\dots,T_{\mathsf{n}})\in\mathcal{A}^{\mathsf{n}}_{ce}$, i.e.,
$M_{ce},\delta,t\models\bigwedge_{i\in N_{ce}}does(T_{i})$ and
$M_{ce},\delta,t\models initial$. Thus, $\theta_{i}(\delta,t)=T_{i}$ and
$\delta[t]=w_{ce}$, for all $i\in N_{ce}$. The update function $U_{ce}$
defines $\delta[t+1]$ such that
$\pi_{Y,ce}(\delta[t+1],trade_{i,j})=\lambda_{i,j}(T_{1},\dots,T_{\mathsf{n}},\mathsf{x}_{1,1},\dots,\mathsf{x}_{\mathsf{n,m}})$,
for each $i\in N_{ce}$ and $j\in G_{ce}$. Thus,
$M_{ce},\delta,t+1\models\bigwedge_{i\in N_{ce},j\in
G_{ce}}trade_{i,j}=win_{i,j}(T_{1},\dots$,
$T_{\mathsf{n}},\mathsf{x}_{1,1},\dots$, $\mathsf{x}_{\mathsf{n,m}})$ and also
$M_{ce},\delta,t\models\bigcirc(\bigwedge_{i\in N_{ce},j\in
G_{ce}}trade_{i,j}=win_{i,j}(T_{1},\dots$, $T_{\mathsf{n}}$,
$\mathsf{x}_{1,1},\dots,\mathsf{x}_{\mathsf{n,m}}))$. Using the abbreviation
for individual trades, $M_{ce},\delta$, $t\models\bigcirc(\bigwedge_{i\in
N_{ce}}trade_{i}=win_{i}(T_{1},\dots,T_{\mathsf{n}},\mathsf{x}_{1,1},\dots$,
$\mathsf{x}_{\mathsf{n,m}}))$.

Finally, we consider Rule 8. Let $i\in N_{ce}$ and $j\in G_{ce}$. If $t=0$,
then $\delta[t]=\bar{w}_{ce}$. By the valuation function $\pi_{Y,ce}$,
$\pi_{Y,ce}(\bar{w}_{ce},alloc_{i,j})=\mathsf{x}_{i,j}$ and
$\pi_{Y,ce}(\bar{w}_{ce},trade_{i,j})=0$. If $t=1$, then by the path
definition we have $\delta[t]=U_{ce}(\bar{w_{ce}},d)$, for some
$d\in\mathcal{A}_{ce}^{\mathsf{n}}$. The update function $U_{ce}$ defines
$\pi_{Y,ce}(\bar{w}_{ce},alloc_{i,j})=\mathsf{x}_{i,j}+trade_{i,j}$.
Otherwise, for any $t>1$, $\delta[t]\in T_{ce}$ (see Rule 7 and path
definition). Thereby, $U_{ce}(\delta[t],d)=\delta[t]$, for some joint action
$d$. Thus, $M_{ce},\delta,t\models
alloc_{i,j}=add(\mathsf{x}_{i,j},trade_{i,j})$.

The remaining rules are verified in a similar way. ∎

Next, we focus on general protocol properties: termination and playability.
Each state succeeding the initial is terminal. Thus, $M_{ce}$ satisfies the
termination condition from General Game Playing (GGP) Zhang (2018), that is,
each path in $M_{ce}$ reaches a terminal state. It follows that agents can
only bid once (except by $noop$).

######  Proposition 0.

For each agent $i\in N_{ce}$ and bid-tree $\beta^{\prime}$,

  1. (1)

$M_{ce}\models initial\rightarrow\bigcirc terminal$

  2. (2)

$M_{ce}\models legal_{i}(\beta)\rightarrow\bigcirc\neg
legal_{i}(\beta^{\prime})$, for any $\beta^{\prime}\in\mathcal{A}_{ce}$ such
that $\beta^{\prime}\neq noop$

###### Proof.

Given a path $\delta$ in $M_{ce}$ and a stage $t$ of $\delta$. Let us verify
Statement 1. Assume $M_{ce},\delta,t\models initial$. Then,
$\delta[t]=\bar{w}_{ce}$. By the path definition, for any $j\geq 1$,
$\delta[j]\neq\bar{w}_{ce}$. By the construction of $T_{ce}$, we have
$T_{ce}=W_{ce}\setminus\\{\bar{w}_{ce}\\}$. Thus, $M_{ce},\delta,t+1\models
terminal$ and $M_{ce},\delta,t\models\bigcirc terminal$.

Now we verify Statement 2. Assume $M_{ce},\delta,t\models legal_{i}(\beta)$.
From Statement 1 and since the path construction defines a loop in any
terminal state (i.e, if $\delta[t]\in T_{ce}$ then $\delta[t]=\delta[t+1]$),
we have that $\delta[t+1]\in T_{ce}$. Thus, $L_{ce}(\delta[t+1],i)=\\{noop\\}$
and $M_{ce},\delta,t+1\models\neg legal(\beta^{\prime})$, for any
$\beta^{\prime}\in\mathcal{A}_{ce}$ such that $\beta^{\prime}\neq noop$. ∎

$M_{ce}$ satisfies the playability condition from GGP Zhang (2018), _i.e_ ,
there is always at least one legal action for each agent in any non-terminal
stage of a path.

######  Proposition 0.

For each agent $i\in N_{ce}$,
$M_{ce}\models\bigvee_{a\in\mathcal{A}_{ce}}legal_{i}(a)$.

###### Proof.

Straightforward from Rules 3 and 4 from $\Sigma_{ce}$. ∎

The next lemma shows that if an agent bids $noop$ in an initial state, her
payment will be zero. Furthermore, if the payment is zero in a terminal state,
it will be zero in the succeeding state.

######  Lemma 0.

For each agent $i\in N_{ce}$,

  1. (1)

$M_{ce}\models initial\land does_{i}(noop)\rightarrow\bigcirc payment_{i}=0$

  2. (2)

$M_{ce}\models terminal\land payment_{i}=0\rightarrow\bigcirc payment_{i}=0$

###### Proof.

Straightforward from Corollary 4.3 and Rules 6 and 7 from $\Sigma_{ce}$. ∎

We then focus on budget balance, non-deficit and individual rationality
conditions.

######  Theorem 1.

$M_{ce}\not\models BB$ and $M_{ce}\models noDeficit$.

###### Proof.

Let $\delta$ be a path in $M_{ce}$ and $t$ be a stage in $\delta$.

If $\delta[t]=\bar{w}_{ce}$, then $M_{ce},\delta,t\models\bigwedge_{i\in
N_{ce}}payment_{i}=0$. Thus, $M_{ce},\delta,t\models BB\land noDeficit$.

Otherwise, by the path definition,
$\delta[t]=U_{ce}(\delta[t-1],\theta(\delta,t-1))$. Since $M_{ce}\models
initial\rightarrow\bigcirc terminal$ and given that $\delta[t-1]=\delta[t]$
whenever $\delta[t-1]\in T_{ce}$, we focus on the case where
$\delta[t-1]=\bar{w}_{ce}$ and the remaining cases follow by consequence.

Let us denote $T_{i}=\theta_{i}(\delta,t-1)$, for each $i\in N_{ce}$. By Rules
5 and 6 from $\Sigma_{ce}$, we have $M_{ce},\delta,t\models\bigwedge_{i\in
N_{ce}}(trade_{i}=win_{i}(T_{i},\dots,T_{\mathsf{n}}$,
$\mathsf{x}_{1,1},\dots$, $\mathsf{x}_{\mathsf{n,m}})\land
payment_{i}=value(T_{i},trade_{i}))$. The solution $WD(T_{i}$,
$\dots,T_{\mathsf{n}},\mathsf{x}_{1,1}$,
$\dots,\mathsf{x}_{\mathsf{n,m}})=(\Lambda,sat)$ satisfies Constraints C1-C4
and maximizes $\sum_{i\in N_{ce}}\sum_{\beta\in
Node(T_{i})}v_{i}(\beta)sat_{i}(\beta)$, that is, it maximizes $\sum_{i\in
N_{ce}}v_{i}(T_{i},\lambda_{i})$. We define the pair
$(\Lambda^{\prime},sat^{\prime})$, such that $\Lambda^{\prime}=(0,\dots,0)$ is
an empty joint trade and $sat^{\prime}=(sat_{1},\dots,sat_{\mathsf{n}})$,
where $sat_{i}^{\prime}=\\{\\}$, for all $i\in N_{ce}$. Notice
$sat_{i}^{\prime}$ is valid for $T_{i}$ and $\lambda_{i}^{\prime}$ (i.e,
$sat_{i}^{\prime}\in valid(T_{i},\lambda_{i}^{\prime})$) and $\sum_{\beta\in
Node(T_{i})}v_{i}(\beta)sat_{i}^{\prime}(\beta)=0$. Remind that the value of a
trade $\lambda_{i}^{\prime}$ given a bid-tree $T_{i}$ maximizes the value of
the satisfied nodes in a valid solution. Thus,
$v_{i}(T_{i},\lambda_{i}^{\prime})\geq 0$ (i.e., it is at least equal to
$\sum_{\beta\in Node(T_{i})}v_{i}(\beta)sat_{i}^{\prime}(\beta)$).

Since the pair $(\Lambda^{\prime},sat^{\prime})$ satisfies the Constraints
C1-C4, a solution $(\Lambda,sat)$ for WD should have at least the same
cumulative trade value, that is, $\sum_{i\in
N_{ce}v_{i}(T_{i},\lambda_{i})}\geq\sum_{i\in
N_{ce}v_{i}(T_{i},\lambda_{i}^{\prime})}$. Thus, $\sum_{i\in
N_{ce}}v_{i}(T_{i}$, $\lambda_{i})\geq 0$. Since
$M_{ce},\delta,t\models\bigwedge_{i\in
N_{ce}}payment_{i}=value(T_{i},trade_{i})$, we have $M_{ce},\delta,t\models
add(payment_{1},\dots,payment_{\mathsf{n}})\geq 0$. Thereby,
$M_{ce},\delta,t\models noDeficit$.

However, if $\sum_{i\in N_{ce}}v_{i}(T_{i},\lambda_{i})>0$, then
$M_{ce},\delta,t\models add(payment_{1}$, $\dots,payment_{\mathsf{n}})>0$ and
$M_{ce},\delta,t\not\models BB$. ∎

######  Theorem 2.

For each $i\in N_{ce}$ and some monotonic valuation $\vartheta_{i}$ over
individual trades, $M_{ce}\models IR_{i}$.

###### Proof.

Given a path $\delta$ in $M_{ce}$, a stage $t$ in $\delta$, an agent $i\in
N_{sa}$, and a monotonic valuation $\vartheta_{i}(\lambda_{i})\in I_{ce}$ for
each individual trade $\lambda_{i}\in I^{\mathsf{m}}_{ce}$, let us consider
the case where $\delta[t]=\bar{w}_{sa}$. We have $M_{sa},\delta,t\models
payment_{i}=0\land\bigwedge trade_{i,j}=0$. Then the utility of $i$ is simply
$\vartheta_{i}(0,\dots,0)$. Let $\delta^{\prime}$ be a path such that
$\delta[0,t]=\delta^{\prime}[0,t]$, $\theta_{i}(\delta,t)=noop$, and
$\theta_{r}(\delta,t)=\theta_{r}(\delta^{\prime},t)$, for all $r\in
N_{ce}\setminus\\{i\\}$. Since $noop\in L_{ce}(\delta[j],i)$, there is such
path in $M_{ce}$. From Lemma 5.1, we have $M_{ce},\delta^{\prime},t+1\models
payment_{i}=0$. Constraint C3 (from the winner determination) and Rule R2
(from the valid solution definition) ensure that the quantity of each item
across the leaves of $noop$ is no greater than the total number of units
traded. For each $j\in G_{sa}$, since $q_{i}(noop,j)=0$ , then
$M_{ce},\delta^{\prime},t+1\models trade_{i,j}\geq 0$. Since $i$’s valuation
is monotonic, it follows that $M_{ce},\delta^{\prime},t+1\models
utility_{i}(trade_{i},payment_{i})\geq\vartheta_{i}(0,\dots,0)$.

Now, let us assume $\delta[t]\neq\bar{w}_{sa}$. Let $x\in I_{sa}$ such that
$M_{ce},\delta,t\models utility_{i}(trade_{i},payment_{i})=x$. From the path
definition, $\delta[t]=\delta[t+1]$ and thus $M_{ce},\delta,t+1\models
utility_{i}(trade_{i},payment_{i})=x$. ∎

####  5.1.1. Vickrey–Clarke–Groves payment

A Vickrey-Clarke-Groves (VCG) mechanism computes a discount for each winner’s
payment, such as she has an incentive to be truthful: the bidder is willing to
reveal her private value. Remind that this work focuses on the auction
definition and not on the bidder’s behavior, the reader may refer to Krishna
(2009) for this strategic aspect.

Let us show how to express VCG payments for an agent $i\in N_{ce}$. Given the
bid-trees $T=(T_{1},\dots,T_{\mathsf{x}})$ and the initial joint allocation
$\mathsf{X}\in I^{\mathsf{nm}}_{ce}$, let
$T^{\prime}=(T_{1}^{\prime},\dots,T_{n}^{\prime})$ be defined as follows:
$T_{i}^{\prime}=noop$ and $T_{r}^{\prime}=T_{r}$, for all $r\in
N_{ce}\setminus\\{i\\}$. Similarly, let
$\mathsf{X}^{\prime}=(x_{1,1}^{\prime},\dots,\mathsf{x}_{\mathsf{n,m}}^{\prime})$
be defined as follows: $\mathsf{x}_{i,j}^{\prime}=0$ and
$\mathsf{x}_{r,j}^{\prime}=x_{r,j}^{\prime}$, for all $r\in
N_{ce}\setminus\\{i\\}$ and all $j\in G_{ce}$. Remind
$\lambda_{i}(T,\mathsf{X})$ denotes the individual trade of agent $i$ in the
solution for $WD(T,\mathsf{X})$.

The VCG payment for agent $i$ is the value of the bid-tree $T_{i}$ given the
individual trade $\lambda_{i}(T,\mathsf{X})$ discounted by the difference
between the cumulative values from the joint trade $\Lambda(T,\mathsf{X})$ and
the trade resulting from removing the bid and allocation of $i$. Formally,

$p_{vcg,i}=v_{i}(T_{i},\lambda_{i}(T,\mathsf{X}))-\sum_{r\in
N_{ce}}(v_{r}(T_{r},\lambda_{r}(T,\mathsf{X}))-v_{r}(T_{r}^{\prime},\lambda_{r}(T^{\prime},\mathsf{X}^{\prime})))$

To construct a combinatorial exchange with VCG payments, we can define
$\Sigma_{vcg}$ such that it is defined exactly as $\Sigma_{ce}$, except by
Rule 6, which is replaced by the following:

$does(T)\land\neg terminal\land
p_{i}=sub(value_{i}(T_{i},win_{i}(T,\mathsf{X})),\\\
add(sub(value_{1}(T_{1},win_{1}(T,\mathsf{X})),value_{1}(T_{1}^{\prime},win_{1}(T^{\prime},\mathsf{X}^{\prime}))),\dots,\\\
sub(value_{\mathsf{n}}(T_{\mathsf{n}},win_{\mathsf{n}}(T,\mathsf{X})),value_{\mathsf{n}}(T_{\mathsf{n}}^{\prime},win_{\mathsf{n}}(T^{\prime},\mathsf{X}^{\prime})))))\\\
\rightarrow\bigcirc payment_{i}=p_{i}$

for each $p_{i}\in I_{ce}$, $T\in\mathcal{A}^{\mathsf{n}}_{ce}$ and $i\in
N_{ce}$.

Let $M_{vcg}$ be an ST-model defined as $M_{ce}$, except by the definition of
$\pi_{Y,vcg}(w,payment_{i})$, for all $i$, which are defined by according to
the VCG price $p_{vcg,i}$ in a state $w\in W_{vcg}$. Unsurprisingly, $BB$ and
$noDeficit$ are not valid in $M_{vcg}$.

######  Proposition 0.

$M_{vcg}\not\models BB$ and $M_{vcg}\not\models noDeficit$.

###### Proof.

Let us prove it by showing a counterexample. Assume $\mathsf{n}=2$,
$\mathsf{m}=1$, $\mathsf{x}_{1,1}=0$ and $\mathsf{x}_{2,1}=1$ i.e., there are
two agents, one good type and the second agent initially holds one copy of the
good. Let $T_{1}=\langle 1,1,2\rangle$ and $T_{2}=\langle-1,1,-1\rangle$ Given
a path $\delta$ in $M_{vcg}$, let $t$ in $\delta$ be a stage such that
$M_{vcg},\delta,t\models initial\land does_{1}(T_{1})\land does_{2}(T_{2})$.
That is, in the initial state, agent $1$ bids for buying the good at the price
$2$ and agent $2$ bids for selling the good at the price $-1$. By WD, we have
$\Lambda(T_{1},T_{2},0,1)=(1,-1)$. Thus, $v_{1}(T_{1},1)=2$ and
$v_{2}(T_{2},-1)=-1$. By the update function, we have
$M_{vcg},\delta,t+1\models trade_{1,1}=1\land trade_{2,1}=-1$. Note no trade
is performed when any of the agents does not participate, i.e.,
$\Lambda(noop,T_{2},0,1)=\Lambda(T_{1},noop,0,0)=(0,0)$. We also have
$v_{i}(T_{i},0)=v_{i}(noop,0)=0$, for each $i\in N_{vcg}$. By the VCG payment
rule, $M_{vcg},\delta,t+1\models
payment_{1}=sub(2,add(add(2,-1),add(0,0)))\land
payment_{2}=sub(-1,add(add(2,-1),add(0,0)))$. That is,
$M_{vcg},\delta,t+1\models payment_{1}=1\land payment_{2}=-2$. Thus, we have a
budget deficit of $-1$, i.e., $M_{vcg},\delta,t+1\models
add(payment_{1},payment_{2})=-1$. Thereby, $M_{vcg}\not\models BB$ and
$M_{vcg}\not\models noDeficit$. ∎

###  5.2. Representing a Simultaneous Ascending Auction

Let us now consider a new type of auction: the Simultaneous Ascending Auction
(SAA) is a single-side and single-unit auction similar to the traditional
English Auction, except that several goods are sold at the same time, and that
the bidders simultaneously bid for any number of goods they want Cramton
(2011). To represent a SAA with $\mathsf{m}$ good types and $\mathsf{n}$
agents, we first describe the auction signature, written
$\mathcal{S}_{sa}=(N_{sa},G_{sa},\mathcal{A}_{sa},\Phi_{sa},Y_{sa},I_{sa})$,
where $N_{ce}=\\{1,\dots,\mathsf{n}\\}$, $G_{sa}=\\{1,\dots,\mathsf{m}\\}$,
$\mathcal{A}_{sa}\subseteq\mathcal{L}_{TBBLf}$,
$\Phi_{sa}=\\{sold_{j},bid_{i,j}:$ $j\in G_{sa}$ & $i\in N_{sa}\\}$ and
$Y_{sa}=\\{price,price_{j},$ $trade_{i,j},alloc_{i,j},payment_{i}:j\in G_{sa}$
& $i\in N_{sa}\\}$. The propositions $sold_{j}$ and $bid_{i,j}$ represent
whether the good $j$ was sold and whether $i$ is bidding for $j$, resp. The
variables $price$ and $price_{j}$ specify the current price for any unsold
good and the selling price for $j$, resp.

Each instance of a SAA is specific and defined with respect to
$\mathcal{A}_{sa}$, $I_{sa}$ and the constant values
$\mathsf{inc},\mathsf{n},\mathsf{m}\in I_{sa,+}\setminus\\{0\\}$ and
$\mathsf{start}\in I_{sa,+}$, representing the quantity of agents and goods,
the increment, and the starting price, respectively. Let $\mathsf{max}_{sa}$
denote the largest value in $I_{sa}$. Then, the rules of an SAA are formulated
by CEDL-formulas as shown in Figure 4.

Given $p_{1},\dots,p_{\mathsf{m}}\in I_{sa,+}$, let
$or_{p_{1},\dots,p_{\mathsf{m}}}=_{def}OR((\langle 1,1,p_{1}\rangle$,
$\dots,\langle 1,1,p_{\mathsf{m}}\rangle),0)$, (1) $initial\leftrightarrow
price=\mathsf{start}$ $\land\bigwedge_{j\in
G_{sa}}\big{(}price_{j}=\mathsf{start}$ $\land$ $\bigwedge_{i\in N_{sa}}(\neg
bid_{i,j}\land trade_{i,j}=0)\big{)}$ (2)
$sold_{j}\leftrightarrow\bigvee_{i\in N_{sa}}trade_{i,j}=1$, for each $j\in
G_{sa}$ (3) $terminal\leftrightarrow$ $\neg initial\land\bigwedge_{j\in
G_{sa}}(sold_{j}$ $\lor$ $\bigwedge_{i\in N_{sa}}\neg bid_{i,j})$ (4)
$\bigcirc(trade_{i,j}=1\leftrightarrow bid_{i,j}$ $\land$ $\bigwedge_{r\in
N_{sa}\setminus\\{i\\}}\neg bid_{r,j})$, for each $i\in N_{sa}$, $j\in G_{sa}$
(5) $\bigcirc(trade_{i,j}=0\leftrightarrow\neg(bid_{i,j}$ $\land$
$\bigwedge_{r\in N_{sa}\setminus\\{i\\}}\neg bid_{r,j}))$, for each $i\in
N_{sa}$, $j\in G_{sa}$ (6)
$legal_{i}(or_{p_{1},\dots,p_{\mathsf{m}}})\leftrightarrow$ $\bigwedge_{j\in
G_{sa}}\big{(}(p_{j}=0$ $\land$ $trade_{i,j}=0)$ $\lor$ $(p_{j}=price\land\neg
sold_{j})$ $\lor$ $(p_{j}=price_{j}\land trade_{i,j}=1)\big{)}$, for each
$i\in N_{sa}$, $p_{1},\dots,p_{\mathsf{m}}\in\\{x:0\leq
x<\mathsf{max}_{sa}-\mathsf{inc}\\}$ (7) $\neg terminal\land
price=x\rightarrow\bigcirc price=add(x,\mathsf{inc})$, for each $x\in
I_{sa,+}$ (8) $\neg terminal\land
price_{j}=x\rightarrow\bigcirc((price_{j}=x\land
sold_{j})\lor(price_{j}=add(x,\mathsf{inc})\land\neg sold_{j}))$, for each
$j\in G_{sa}$, $x\in I_{sa,+}$ (9) $\neg terminal\rightarrow alloc_{i,j}=0$,
for each $i\in N_{sa}$, $j\in G_{sa}$ (10) $\bigcirc bid_{i,j}\leftrightarrow$
$(does_{i}(or_{p_{1},\dots,p_{\mathsf{m}}})$ $\land$ $p_{j}\neq 0)$ $\lor$
$(bid_{i,j}\land terminal)$, for each $i\in N_{sa}$, $j\in G_{sa}$ and some
$p_{1},\dots,p_{m}\in I_{sa,+}$ (11) $terminal\rightarrow
alloc_{i,j}=trade_{i,j}$, for each $i\in N_{sa}$, $j\in G_{sa}$ (12)
$payment_{i}=add(times(price_{1},trade_{i,1})$, $\dots$,
$times(price_{\mathsf{m}},trade_{i,\mathsf{m}}))$, for each $i\in N_{sa}$ (13)
$terminal\land y=x\rightarrow\bigcirc y=x$, for each $y\in Y$, $x\in I_{sa}$

Figure 4. Simult. Ascending Auction represented by $\Sigma_{sa}$

In the initial state, no agent is bidding, no trade is performed and the
prices have the value $\mathsf{start}$ (Rule 1). A good is sold if there is a
trade for some agent (Rule 2). In a terminal state, all the goods are either
sold or no one is bidding for them (Rule 3). A good will be traded to an agent
if she is the only one bidding for it, otherwise there is no trade (Rules
4-5). For each good, an agent can either bid the value 0, the current price
(for unsold goods) or repeat her winning bid for this good (Rule 6). In a non-
terminal state, the propositions and numerical variables are updated as
follows: (i) the current price increases, (ii) the selling price increases for
unsold goods, (iii) there is no allocation, and (iv) the active bidders for
each good are updated w.r.t. their bids (Rules 7-10). The allocations are
assigned in terminal states w.r.t. trades (Rule 11). The payment for an agent
is the cumulative value of the selling price for her traded goods (Rule 12).
Finally, after a terminal state, a numerical variable cannot change (Rule 13).
Let $\Sigma_{sa}$ be the set of Rules 1-13.

##### Representing as a model

Next, we address the model representation of the Simultaneous Ascending
Auction (SAA). Let $\mathscr{M}_{sa}$ be the set of ST-models $M_{sa}$ defined
for any $\mathcal{A}_{sa}\subseteq\mathcal{L}_{TBBLf}$,
$I_{sa}\subset\mathbb{Z}$, and the constant values
$\mathsf{inc},\mathsf{start}\in I_{sa,+}$ and $\mathsf{m},\mathsf{n}\in
I_{sa,+}\setminus\\{0\\}$. Let $\mathsf{max}_{sa}$ denote the largest value in
$I_{sa}$. Each $M_{sa}$ is defined as follows:

  * •

$W_{sa}=\\{\langle
b_{1,1},\dots,b_{\mathsf{n,m}},t_{1,1},\dots,t_{\mathsf{n,m}},p,p_{1},\dots,$
$p_{\mathsf{m}}\rangle:b_{i,j},t_{i,j}\in\\{0,1\\}$ & $p,p_{j}\in I_{sa,+}$ &
$i\in N_{sa}$ & $j\in G_{sa}\\}$;

  * •

$\bar{w}_{sa}=\langle
0,\dots,0,0,\dots,0,\mathsf{start},\mathsf{start},\dots,\mathsf{start}\rangle$;

  * •

$T_{sa}=\\{w:w=\langle
b_{1,1},\dots,b_{\mathsf{n,m}},t_{1,1},\dots,t_{\mathsf{n,m}}$, $p,p_{1}$,
$\dots,p_{\mathsf{m}}\rangle\in W_{sa}\setminus\\{\bar{w}_{sa}\\}$ & for all
$j\in G_{sa}$, either (i) $t_{i,j}=1$ for some $i\in N_{sa}$ or (ii)
$bid_{i,j}=0$, for all $i\in N_{sa}\\}$;

  * •

$L_{sa}=\\{(w,i,OR((\langle 1,1,pr_{1}\rangle$, $\dots,\langle
1,1,pr_{\mathsf{m}}\rangle),0)):$ $i\in N_{sa}$ & $w=\langle b_{1,1},$
$\dots,$ $b_{\mathsf{n,m}},t_{1,1},$ $\dots,$ $t_{\mathsf{n,m}},p,p_{1},$
$\dots,$ $p_{\mathsf{m}}\rangle\in W_{sa}$ & for all $j\in G_{sa}$, and all
$0\leq pr_{j}<\mathsf{max}_{sa}-\mathsf{inc}$ such that either (i) $pr_{j}=0$
& $t_{i,j}=0$ or (ii) $pr_{j}=p$ & $t_{i^{\prime},j}\neq 1$, for all
$i^{\prime}\in N_{sa}$ or (iii) $pr_{j}=p_{j}$ & $t_{i,j}=1\\}$;

  * •

$U_{sa}$ is defined as: for all $w=\langle
b_{1,1},\dots,b_{\mathsf{n,m}},t_{1,1}$, $\dots$, $t_{\mathsf{n,m}},p,p_{1}$,
$\dots,p_{\mathsf{m}}\rangle\in W_{sa}$ and all
$d\in\mathcal{A}^{\mathsf{n}}_{sa}$:

    * –

If $w\not\in T_{sa}$, then: $U_{sa}(w,d)=\langle b_{1,1}^{\prime}$,
$\dots,b_{\mathsf{n,m}}^{\prime},t_{1,1}^{\prime},\dots$,
$t_{\mathsf{n,m}}^{\prime}$,
$p^{\prime},p_{1}^{\prime},\dots,p_{\mathsf{m}}^{\prime}\rangle$, where for
every $i\in N_{sa}$ and $j\in G_{sa}$, (i) $b_{i,j}^{\prime}=1$ iff
$d(i)=OR((\langle 1,1,pr_{1}\rangle$, $\dots,\langle
1,1,pr_{\mathsf{m}}\rangle),0)$ and $pr_{j}\neq 0$; and $b_{i,j}^{\prime}=0$
otherwise; (ii) $t_{i,j}^{\prime}=1$ iff $b_{i,j}^{\prime}=1$ and for all
$r\in N_{sa}\setminus\\{i\\},b_{i,j}^{\prime}\neq 1$; and $t_{i,j}^{\prime}=0$
otherwise; (iii) $p^{\prime}=p+\mathsf{inc}$; (iv)
$p_{j}^{\prime}=p_{j}+\mathsf{inc}$ iff $t_{r,j}^{\prime}=0$ for all $r\in
N_{sa}$; and $p_{j}^{\prime}=p_{j}$ otherwise.

    * –

Otherwise, $U_{sa}(w,d)=w$.

  * •

For each $w\in W_{sa}$, $i\in N_{sa}$ and $j\in G_{sa}$, (i)
$\pi_{Y,sa}(w,trade_{i,j})=t_{i,j}$; (ii) $\pi_{Y,sa}(w,price)=p$; (iii)
$\pi_{Y,sa}(w,price_{j})=p_{j}$; (iv) $\pi_{Y,sa}(w,alloc_{i,j})=0$ iff
$w\not\in T_{sa}$, and $\pi_{Y,sa}(w$, $alloc_{i,j})=t_{i,j}$ otherwise; (v)
$\pi_{Y,sa}(w,payment_{i})=\sum_{j\in G_{sa}}(p_{j}\pi_{Y,sa}(w$,
$trade_{i,j}))$.

  * •

For each $w\in W_{sa}$, $\pi_{\Phi,sa}(w)=\\{sold_{j}:t_{i,j}=1$ & $j\in
G_{sa}$ & $i\in N_{sa}\\}\cup\\{bid_{i,j}:b_{i,j}=1$ & $j\in G_{sa}$ & $i\in
N_{sa}\\}$.

Hereafter, we assume an instance of $M_{sa}\in\mathscr{M}_{sa}$ and
$\Sigma_{sa}$ for some $\mathcal{A}_{sa}\subseteq\mathcal{L}_{TBBLf}$,
$I_{sa}\subset\mathbb{Z}$, $\mathsf{start}\in I_{sa,+}$ and
$\mathsf{inc},\mathsf{m},\mathsf{n}\in I_{sa,+}\setminus\\{0\\}$.

######  Example 0.

Let $M_{sa}\in\mathscr{M}_{sa}$, where $\mathsf{start}=2$, $\mathsf{inc}=1$
and the agents and good sets are the same from Example 5.1. Figure 5
illustrates a path in $M_{sa}$. In state $w_{0}$, agents $r1$ and $r2$ bid for
good $\mathsf{a}$, but only agent $r1$ bid for good $\mathsf{b}$. In state
$w_{1}$, since $r1$ is the only bidder for $\mathsf{b}$, $\mathsf{b}$ is sold
to her. Agent $r1$ needs to keep her bid for $\mathsf{b}$ and $r2$ can no
longer bid for it. In $w_{1}$, agent $r2$ increases its bid for good
$\mathsf{a}$ and agent $r1$ do not bid for $\mathsf{a}$. In state $w_{2}$,
since $r2$ is the only bidder for $\mathsf{a}$, she buys the good. Since all
the goods were sold, this state is terminal.

Figure 5. A Path in $M_{sa}$, with 2 bidders and $2$ goods

Let us now evaluate the protocol. First, we show that $\Sigma_{sa}$ is a sound
representation of $M_{sa}$.

######  Proposition 0.

$M_{sa}$ is an ST-model and it is a model of $\Sigma_{sa}$.

###### Proof.

_(Sketch)_ It is routine to check that $M_{sa}$ is actually an ST-model. Given
a path $\delta$, any stage $t$ of $\delta$ in $M_{sa}$, we need to show that
$M_{sa},\delta,t\models\varphi$, for each $\varphi\in\Sigma_{sa}$. Let us
verify Rule 1. Assume $M_{sa},\delta,t\models initial$ iff
$\delta[t]=\bar{w}_{sa}$. By the definition of $\bar{w}_{sa}$, $\pi_{\Phi,sa}$
and $\pi_{Y,sa}$, we have $\pi_{Y,sa}(\bar{w}_{sa},price)=\mathsf{start}$,
$\pi_{Y,sa}(\bar{w}_{sa},price_{j})=\mathsf{start}$,
$bid_{i,j}\not\in\pi_{\Phi,sa}(\bar{w}_{sa})$ and $trade_{i,j}=0$, for all
$i\in N_{sa}$ and $j\in G_{sa}$. Thus, $M_{sa},\delta,t\models initial$ iff
$M_{sa},\delta,t\models price=\mathsf{start}$ $\land\bigwedge_{j\in
G_{sa}}(price_{j}=$ $\mathsf{start}\land\bigwedge_{i\in N}(\neg bid_{i,j}\land
trade_{i,j}=0))$.

Now we verify Rule 2. Let $j\in G_{sa}$ be a good type. Assume
$M_{sa},\delta,t\models sold_{j}$ iff $sold_{j}\in\pi_{\Phi,sa}(\delta[t])$
iff $\pi_{Y,sa}(\delta[t],trade_{i,j})=1$ for some $j\in G_{sa}$ iff
$M_{sa},\delta,t\models\bigvee_{i\in N_{sa}}trade_{i,j}=1$.

Next, we consider Rule 3. Assume $M_{sa},\delta,t\models terminal$ iff
$\delta[t]\neq\bar{w}_{sa}$ and for all $j\in G_{sa}$, either
$M_{sa},\delta,t\models trade_{r,j}=1$ for some $r\in N_{sa}$ or
$M_{sa},\delta,t\models\neg bid_{i,j}$ for all $i\in N_{sa}$. By Rule 2,
$M_{sa},\delta,t\models terminal$ iff $M_{sa},\delta,t\models\neg
initial\land\bigwedge_{j\in G_{sa}}(sold_{j}\lor\bigwedge_{j\in G_{sa}}\neg
bid_{i,j})$.

Now we verify Rule 10. Let $i\in N_{sa}$ and $j\in G_{sa}$. Assume
$M_{sa},\delta,t\models(does_{i}(OR((\langle 1,1,p_{1}\rangle,\dots,\langle
1,\mathsf{m},p_{\mathsf{m}}\rangle),0))\land p_{j}\neq 0)\lor(bid_{i,j}\land
terminal)$, for some $p_{1},\dots,p_{\mathsf{m}}\in I_{sa,+}$. We next prove
for the two cases. First, assume $M_{sa},\delta,t\models bid_{i,j}\land
terminal$. Then $bid_{i,j}\in\pi_{\Phi,sa}(\delta[t])$ and $\delta[t]\in
T_{sa}$. By the update function, $\delta[t+1]=\delta[t]$ and
$M_{sa},\delta,t+1\models bid_{i,j}$, i.e., $M_{sa},\delta,t\models\bigcirc
bid_{i,j}$. In the second case, assume $does_{i}(OR((\langle
1,1,p_{1}\rangle,\dots,\langle 1,\mathsf{m},p_{\mathsf{m}}\rangle),0))\land
p_{j}\neq 0$. By the update function, $bid_{i,j}\in\pi_{\Phi,sa}(\delta[t+1])$
and thus $M_{sa},\delta,t\models\bigcirc bid_{i,j}$.

The remaining rules are verified in a similar way. ∎

Next, we show that no good can be bought by two different agents, _i.e_ ,
given any two agents and a good, one of them will have her trade equal zero.

######  Proposition 0.

For each $j\in G_{sa}$ and each $i,i^{\prime}\in N_{sa}$ such that $i\neq
i^{\prime}$, $M_{sa}\models trade_{i,j}=0\lor trade_{i^{\prime},j}=0$.

###### Proof.

Given a path $\delta$ in $M_{sa}$, any stage $t$ of $\delta$ and a good type
$j\in G_{sa}$, let $i,i^{\prime}\in N_{sa}$, such that $i\neq i^{\prime}$. If
$\delta[t]=\bar{w}_{sa}$, then $M_{sa},\delta,t\models trade_{i,j}=0\land
trade_{i^{\prime},j}=0$ (see Rule 1). Otherwise, by the path definition,
$\delta[j]=U_{sa}(\delta[t-1],\theta(\delta,t-1))$. Let us suppose for the
sake of contradiction that $M_{sa},\delta,t\not\models trade_{i,j}=0\lor
trade_{i^{\prime},j}=0$. Since $W_{sa}$ construction defines
$trade_{i,j},trade_{i^{\prime},j}\in\\{0,1\\}$, we have
$M_{sa},\delta,t\models trade_{i,j}=1\land trade_{i^{\prime},j}=1$. Thus,
$M_{sa},\delta,t-1\models\bigcirc trade_{i,j}$. By Rule 4,
$M_{sa},\delta,t-1\models\bigcirc(bid_{i,j}\land\bigwedge_{r\in
N_{sa}\setminus\\{i\\}}\neg bid_{r,j})$. Thereby,
$M_{sa},\delta,t-1\not\models\bigcirc(bid_{i^{\prime},j}\land\bigwedge_{r\in
N_{sa}\setminus\\{i^{\prime}\\}}\neg bid_{r,j})$ and $M_{sa},\delta$,
$t-1\not\models\bigcirc trade_{i^{\prime},j=1}$. Thus,
$M_{sa},\delta,t\not\models trade_{i^{\prime},j}=1$, which is a
contradiction.. ∎

The legal bids in a state respect the $buyer$ and $unit$ restrictions. It
means that agents cannot bid for negative prices and can only ask for one unit
of each good.

######  Proposition 0.

For each $i\in N_{sa}$ and each $a\in\mathcal{A}_{sa}$, $M_{sa}\models
legal_{i}(a)\rightarrow rest_{i}(buyer,a)\land rest_{i}(unit,a)$.

###### Proof.

Let $\delta$ be a path in $M_{sa}$ and $t$ a stage of $\delta$. Assume
$M_{sa}\models legal_{i}(a)$ iff $a\in L_{sa}(\delta[t],i)$. By $L_{sa}$
construction, $a=OR((\langle 1,1,p_{1}\rangle$, $\dots$, $\langle
1,\mathsf{m},p_{\mathsf{m}}\rangle),0)$, for $p_{1},\dots,p_{\mathsf{m}}\in
I_{sa,+}$. The set of leaves and nodes of $a$ are $Leaf(a)=\\{\langle
1,1,p_{1}\rangle,\dots,\langle 1,\mathsf{m}$, $p_{\mathsf{m}}\rangle\\}$ and
$Node(a)=\\{OR((\langle 1,1,p_{1}\rangle$, $\dots$, $\langle
1,\mathsf{m},p_{\mathsf{m}}\rangle),0)\\}\cup Leaf(a)$, resp. Thus, for all
$\beta\in Node(a)$, $v_{i}(\beta)\geq 0$ and for all $\beta^{\prime}\in
Leaf(a)$, $q_{i}(\beta^{\prime},j)=1$ for some $j\in G_{sa}$. Thereby,
$M_{sa},\delta,t\models rest_{i}(buyer,a)\land rest_{i}(unit,a)$. ∎

The next proposition shows $M_{sa}$ satisfies playability, that is, there is
always a legal action for each agent to take.

######  Proposition 0.

For each agent $i\in N_{ce}$,
$M_{sa}\models\bigvee_{a\in\mathcal{A}_{ce}}legal_{i}(a)$.

###### Proof.

Given a path $\delta$ in $M_{sa}$ and a stage $t$ in $\delta$, we show that
there is a legal action for agent $i$ in $\delta[t]$. For each $j\in G_{sa}$,
let $p_{j}=0$ if $\pi_{Y,sa}(\delta[t],trade_{i,j})=1$. Otherwise, let
$p_{j}=\pi_{Y,sa}(\delta[t],price_{j})$. By the definition of $L_{sa}$, we
have $OR((\langle 1,1,p_{1}\rangle,\dots,\langle 1$,
$\mathsf{m},p_{\mathsf{m}}\rangle),0)\in L_{sa}(\delta[t],\allowbreak i)$.
Thus, $M_{sa},\delta,t\models\bigvee_{a\in\mathcal{A}_{sa}}legal_{i}(a)$. ∎

Each path in $M_{sa}$ reaches a terminal state, and thus the protocol
satisfies the termination condition from GGP.

######  Proposition 0.

For each path $\delta$ in $M_{sa}$, $\delta$ is complete.

###### Proof.

Remind $\mathsf{start}\in I_{sa,+}$ and $\mathsf{inc}\in
I_{sa,+}\setminus\\{0\\}$. Let $\delta$ be a path in $M_{sa}$. In $\delta[0]$,
$\pi_{Y,sa}(\delta[0],price)=\mathsf{start}$. By the update function, for any
stage $t$, if $\delta[t]\not\in T_{sa}$, then
$\pi_{Y,sa}(\delta[t+1],price)=\pi_{Y,sa}(\delta[t],price)+\mathsf{inc}$.

For the sake of contradiction, let us assume $\delta$ is not complete. Let
$i\in N_{sa}$ be any agent. By the definition of $L_{sa}$,
$legal_{i}(OR((\langle 1,1,p_{1}\rangle$, $\dots,\langle
1,\mathsf{m},p_{\mathsf{m}}\rangle),0))\in L(\delta[t],i)$, for all $0\leq
p_{j}<\mathsf{max}_{sa}-\mathsf{inc}$ and $j\in G_{sa}$, such that either (i)
$p_{j}=0$ & $\pi_{Y,sa}(\delta[t]$, $trade_{i,j})=0$, or (ii) $p_{j}=price$ &
$\pi_{Y,sa}(\delta[t],trade_{r,j})=0$ for all $r\in N_{sa}$, or (iii)
$p_{j}=price_{j}$ & $\pi_{Y,sa}(\delta[t],trade_{r,j})=0$. Since
$\pi_{Y,sa}(\delta[t+1],price)>\pi_{Y,sa}(\delta[t],price)$, there will be a
stage $e\geq 0$ in $\delta$, where the condition (ii) will not be true for any
$0\leq p_{j}<\mathsf{max}_{sa}-\mathsf{inc}$.

Thus, for each good $j$, it will be the case that $i$ bids $0$ for it or the
good was assigned to her (i.e., $\pi_{Y,sa}(\delta[e],trade_{i,j})=1$). From
Rules 3 and 10 in $\Sigma_{sa}$, it follows that $\delta[e+1]\in T_{sa}$.
Thus, $\delta$ is a complete path, which is a contradiction. ∎

From being a single-side auction where all agents are buyers, it follows that
there is no-deficit in $M_{sa}$, but it is not budget-balanced.

######  Proposition 0.

$M_{sa}\not\models BB$ and $M_{sa}\models noDeficit$.

###### Proof.

_(Sketch)_ Given a path $\delta$ in $M_{sa}$ and a stage $t$ in $\delta$, let
us show a counterexample. Note that each allocation can be either 0 or 1 and
the good price is at least 0, i.e.,
$\pi_{Y,sa}(\delta[t],alloc_{i,j})\\{0,1\\}$ and
$\pi_{Y,sa}(\delta[t],price_{j})\in I_{sa,+}$. Assume
$\pi_{Y,sa}(\delta[t],alloc_{i^{\prime},j^{\prime}})=1$ and
$\pi_{Y,sa}(\delta[t],price_{j^{\prime}})>0$, for some $j^{\prime}\in G_{sa}$
and some $i^{\prime}\in N_{sa}$. It follows from Rule 12 that
$M_{sa},\delta,t\models payment_{i^{\prime}}>0$ and $M_{sa},\delta,t\models
add(payment_{1},\dots,payment_{\mathsf{n}})>0$. Thus, $M_{sa}\not\models BB$
and $M_{sa}\models noDeficit$. ∎

Finally, the agents can always ensure that their utility will be at least as
good in the next state as it was in the current, _i.e_ , $IR_{i}$ is valid in
$M_{sa}$, for each $i$.

######  Theorem 3.

For each $i\in N_{sa}$ and some valuation $\vartheta_{i}$ over individual
trades, $M_{sa}\models IR_{i}$.

###### Proof.

Given a path $\delta$ in $M_{sa}$ and a stage $t$, let $T_{i}=OR((\langle
1,1,p_{1}\rangle$, $\dots,\langle 1,\mathsf{m},p_{\mathsf{m}}\rangle),0)$,
where $p_{j}=0$ if $\pi_{Y,sa}(\delta[t],trade_{i,j})=0$; otherwise
$p_{j}=\pi_{Y,sa}(\delta[t]$, $price_{j})$, for each $j\in G_{sa}$. Since
$T_{i}\in L_{sa}(\delta[t],i)$, we can construct a path $\delta^{\prime}$,
such that $\delta^{\prime}[0,t]=\delta[0,t]$,
$\theta_{i}(\delta^{\prime},t)=T_{i}$, and
$\theta_{r}(\delta^{\prime},t)=\theta_{r}(\delta,t)$, for all $r\in
N_{sa}\setminus\\{i\\}$. Thus, $M_{ce},\delta^{\prime},t\models
utility_{i}(trade_{i}$, $payment_{i})=x\rightarrow\bigcirc
utility_{i}(trade_{i}$, $payment_{i})=x$, for $x\in I_{sa}$ and
$M_{ce},\delta,t\models IR_{r}$. ∎

##  6\. Discussion and Conclusion

In this paper, we have presented a unified framework for representing auction
protocols. Our work is at the frontier of auction theory and knowledge
representation.

##### Related work

Our work is rooted in the key contributions on Combinatorial Auctions Nisan
(2000, 2004); Xia et al. (2005); Parkes et al. (2005). All these works adopt a
mechanism design perspective: they focus on the properties of a given protocol
and bidding language. Our work has a different purpose. The CEDL language
includes the bidding part of a protocol, but also the protocol itself. Such a
language can be used to automatically derive properties for these protocols.
CEDL can also be used as a framework for testing new auction protocols.

To the best of our knowledge, almost all contributions on the computational
representation of auction-based markets focus on the implementation of the
winner determination problem. For instance, Baral and Ulyan (2001) show how a
specific auction, namely combinatorial auctions, can be encoded in a logic
program. A hybrid approach mixing linear programming and logic programming has
been proposed by Lee and Lee (1997): they focus on sealed-bid auctions and
show how qualitative reasoning helps to refine the optimal quantitative
solutions. Giovannucci et al. (2010) explore a graphical formalism to
compactly represent the winner determination problem for Multi-Unit
Combinatorial Auctions. The closest contributions to ours are the _Market
Specification Language_ (MSL) Thielscher and Zhang (2010) and ADL Mittelmann
and Perrussel (2020), also based on GDL. They both focus on representing
single good auction through a set of rules and then interpreting an auction-
instance with the help of a state-based semantics. MSL is limited to single
agent perspective while ADL is not. However, the main limit of both approaches
is the absence of a bidding language.

##### Going Further

First direction is Computational complexity. Although the model-checking (MC)
problem in ADL is PTIME Mittelmann and Perrussel (2020), the winner
determination in Combinatorial Auctions (and thus also in Combinatorial
Exchange) is known to be NP-complete Rothkopf et al. (1998). We aim to explore
how the MC problem in CEDL is affected by these results. Clearly, the fragment
of CEDL without formulas referring to the WD mixed-integer program is still
PTIME. For instance, the Simultaneous Ascending Auction protocol described in
this paper avoids such formulas.

CEDL definitely puts the emphasis on the auctioneer and auction designer. Our
second direction is to design a CEDL-based General Auction Player (GAP) that
can interpret and reason about the rules of an auction-based market. The key
difference, when the players’ perspective is considered, is the epistemic and
strategic aspects: players have to reason about other players’ behavior. The
epistemic component will allow an agent to bid according to her beliefs about
other agents’ private values. Our future GAP should then be based on the
epistemic extensions of GDL such as GDL-III Thielscher (2016) and Epistemic
GDL Jiang et al. (2016).

This research is supported by the ANR project AGAPE ANR-18-CE23-0013.

## References

  * (1)
  * Baral and Uyan (2001) Chitta Baral and Cenk Uyan. 2001.  Declarative Specification and Solution of Combinatorial Auctions Using Logic Programming. In _Logic Programming and Nonmotonic Reasoning_ , Thomas Eiter, Wolfgang Faber, and Miros law Truszczyński (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 186–199.
  * Boutilier and Hoos (2001) Craig Boutilier and Holger H. Hoos. 2001.  Bidding Languages for Combinatorial Auctions. In _Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI-01)_ , Bernhard Nebel (Ed.). Morgan Kaufmann, Seattle, Washington, USA, 1211–1217.
  * Cavallo et al. (2005) Ruggiero Cavallo, David C Parkes, Adam I Juda, Adam Kirsch, Alex Kulesza, Sébastien Lahaie, Benjamin Lubin, Loizos Michael, and Jeffery Shneidman. 2005.  TBBL: A tree-based bidding language for iterative combinatorial exchanges. In _Multidisciplinary Workshop on Advances in Preference Handling_. Edinburgh.
  * Cramton (2011) Peter Cramton. 2011\.  _Simultaneous Ascending Auctions_.  American Cancer Society.  https://doi.org/10.1002/9780470400531.eorms0783
  * Genesereth and Thielscher (2014) Michael Genesereth and Michael Thielscher. 2014.  _General game playing_.  Morgan & Claypool Publishers.
  * Giovannucci et al. (2010) Andrea Giovannucci, Jesús Cerquides, Ulle Endriss, and Juan A Rodríguez-Aguilar. 2010\.  A graphical formalism for mixed multi-unit combinatorial auctions.  _Autonomous Agents and Multi-Agent Systems_ 20, 3 (2010), 342–368.  https://doi.org/10.1007/s10458-009-9085-x
  * Jiang et al. (2016) Guifei Jiang, Dongmo Zhang, Laurent Perrussel, and Heng Zhang. 2016.  Epistemic GDL: A logic for representing and reasoning about imperfect information games. In _IJCAI International Joint Conference on Artificial Intelligence_.
  * Klemperer (1999) Paul Klemperer. 1999\.  Auction Theory: A Guide to the Literature.  _Journal of Economic Surveys_ 13, 3 (1999), 227–286.  https://doi.org/10.1111/1467-6419.00083 arXiv:https://onlinelibrary.wiley.com/doi/pdf/10.1111/1467-6419.00083
  * Krishna (2009) Vijay Krishna. 2009\.  _Auction Theory_.  Academic Press.  https://doi.org/10.1192/bjp.111.479.1009-a
  * Lee and Lee (1997) H. Geun Lee and R. Lee. 1997.  A hybrid approach of linear programming and logic modeling for the market core of sealed bid auctions.  _Annals of Operations Research_ 75 (1997).
  * Lubin et al. (2008) Benjamin Lubin, Adam I Juda, Ruggiero Cavallo, Sébastien Lahaie, Jeffrey Shneidman, and David C Parkes. 2008.  ICE: An expressive iterative combinatorial exchange.  _Journal of Artificial Intelligence Research_ 33 (2008), 33–77.
  * Mishra and Sharma (2018) Debasis Mishra and Tridib Sharma. 2018.  A simple budget-balanced mechanism.  _Social Choice and Welfare_ 50, 1 (2018), 147–170.
  * Mittelmann and Perrussel (2020) Munyque Mittelmann and Laurent Perrussel. 2020.  Auction Description Language (ADL): a General Framework for Representing Auction-based Markets. In _ECAI 2020_ , G. de Giacomo (Ed.). IOS Press, Santiago de Compostela.
  * Nisan (2000) Noam Nisan. 2000\.  Bidding and Allocation in Combinatorial Auctions. In _ACM Conference on Electronic Commerce_. 1–12.
  * Nisan (2004) Noam Nisan. 2004\.  Bidding languages.  _Combinatorial Auctions_ (2004), 1–19.  https://doi.org/10.1109/CEC.2009.42
  * Parkes et al. (2005) David C Parkes, Ruggiero Cavallo, Nick Elprin, Adam Juda, Sébastien Lahaie, Benjamin Lubin, Loizos Michael, Jeffrey Shneidman, and Hassan Sultan. 2005.  ICE: An Iterative Combinatorial Exchange. In _Proceedings of the 6th ACM Conference on Electronic Commerce_ _(EC ’05)_. Association for Computing Machinery, New York, NY, USA, 249–258.  https://doi.org/10.1145/1064009.1064036
  * Parkes and Ungar (2001) David Christopher Parkes and Lyle H Ungar. 2001.  _Iterative combinatorial auctions: Achieving economic and computational efficiency_.  University of Pennsylvania Philadelphia, PA.
  * Rothkopf et al. (1998) Michael H Rothkopf, Aleksandar Pekeč, and Ronald M Harstad. 1998.  Computationally manageable combinational auctions.  _Management science_ 44, 8 (1998), 1131–1147.
  * Thielscher (2016) Michael Thielscher. 2016\.  GDL-III: A proposal to extend the game description language to general epistemic games. In _Proc. the European Conference on Artificial Intelligence (ECAI)_ , Vol. 285. Hague, 1630–1631.  https://doi.org/10.3233/978-1-61499-672-9-1630
  * Thielscher and Zhang (2010) Michael Thielscher and Dongmo Zhang. 2010.  _From General Game Descriptions to a Market Specification Language for General Trading Agents_.  Springer Berlin Heidelberg, 259–274.
  * Voorneveld (2003) Mark Voorneveld. 2003\.  Characterization of Pareto dominance.  _Operations Research Letters_ 31, 1 (2003), 7 – 11.  https://doi.org/10.1016/S0167-6377(02)00189-X
  * Xia et al. (2005) Mu Xia, Jan Stallaert, and Andrew B. Whinston. 2005.  Solving the combinatorial double auction problem.  _European Journal of Operational Research_ 164, 1 (2005), 239–251.  https://doi.org/10.1016/j.ejor.2003.11.018
  * Zhang (2018) Dongmo Zhang. 2018\.  A Logic for Reasoning About Game Descriptions. In _AI 2018: Advances in Artificial Intelligence_ , Tanja Mitrovic, Bing Xue, and Xiaodong Li (Eds.). Springer International Publishing, Cham, 38–50.