Representing and reasoning about auctions

Abstract

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 $\mathcal {F}_{\mathcal {B}}$ (ADL $[\mathcal {F}_{\mathcal {B}}]$). ADL $[\mathcal {F}_{\mathcal {B}}]$ 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 $[\mathcal {F}_{\mathcal {B}}]$, with complexity in PTIME when the functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in polynomial time.

1 Introduction

Auction-based markets are widely used for automated business transactions. There are numerous variants depending on the parameters considered, including the number of distinct items¹ and their copies and the number of sellers and buyers [35, 36]. For a fixed set of parameters, the protocol, i.e., the bidding, payment and allocation 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. In this setting, the auction designer should at first describe the rules governing the auction and second allow participants to express their preferences. The aim of this paper is to propose a language with clear semantics for enabling the representation of auctions as well as the reasoning about its rules and properties. More precisely, such a language should address the six auction dimensions introduced by Parkes and Kalagnanam [33]:

• 1. Resources: the auction protocol may involve a single item or multiple items, with single or multiple units of each item. The type of the item may also be considered, i.e., the item may be a multi-attribute commodity;

• 2. Market structure: the auction may differ on whether it has single or multiple buyers and/or sellers. In single-sided auctions, there is either a single seller selling resources to multiple buyers (i.e., forward auctions), or a single buyer sourcing resources from multiple suppliers (i.e., reverse auctions). In a double auction, there are multiple suppliers selling resources to multiple buyers. Finally, an exchange is a generalization of double auctions, where the participants trade items;

• 3. Preference structure: the participants’ preferences define their utilities over different outcomes (e.g., marginal utility, quasi-linear utility);

• 4. Bid structure: it refers to the flexibility with which participants can express their preferences. The bid structure ranges from simple statements of willingness to accept a given selling price to complex bids that state prices, quantities, bundles, and logical connectives. In single-dimensional auctions, only one attribute is considered in the bid (e.g., the price offered for a good). On the other hand, multi-dimensional auctions handle a number of attributes in the bid (e.g., quality, delivery date) [55];

• 5. Market clearing: in relation to the method for matching the supply to demand, an auction may be single-sourcing (i.e., matching pairs of buyers and sellers) or multi-sourcing (i.e., matching multiple sellers with a single buyer, or vice-versa);

• 6. Information feedback: auctions may also differ on whether they are direct (i.e., one-stage protocols without information feedback) or indirect mechanisms (i.e., protocols where agents can adjust their bids in response to information feedback).

In the spirit of the General Game Playing (GGP) [21] where games are described with the help of Game Description Language (GDL), we previously introduced a logical language for describing auctions, denoted Auction Description Language (ADL) [45, 46].

In this paper, we go further and present a new version of ADL, named ADL $[\mathcal {F}_{\mathcal {B}}]$, which is described as Auction Description Language with a set of functions $\mathcal {F}_{\mathcal {B}}$. ADL $[\mathcal {F}_{\mathcal {B}}]$ builds upon bidding languages, and hence provides a natural way to represent a wide range of protocols, ranging from single-units auctions to iterative combinatorial exchanges [53]. As for GDL and ADL, we propose a precise semantics based on state-transition models, that gives a clear meaning to the auction rules. Different bidding languages can be used with ADL $[\mathcal {F}_{\mathcal {B}}]$, including the Tree-Based Bidding Language [53], which generalizes known languages such as XOR/OR [50] to combinatorial exchange. To the best of our knowledge, ADL $[\mathcal {F}_{\mathcal {B}}]$ is the first framework offering a unified perspective on an auction mechanism and it 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.

Our motivation for proposing ADL $[\mathcal {F}_{\mathcal {B}}]$ is twofold. First, to enable automated reasoning about properties and features of an auction. These include determining whether the protocol is well-formed, in terms of termination and playability, as well as properties related to the mechanism itself, such as individual rationality and efficiency. Second, inspired by General Game Playing, our goal is to implement general players and an auction server to evaluate their adaptability among different protocols and their ability to learn from other agents’ behavior. Just like for the GGP, ADL $[\mathcal {F}_{\mathcal {B}}]$ provides the ground for testing auction players and creating market-based competitions.

1.1 Contributions

Our main contribution is to provide a general framework for representing auctions. For discussing the generality of ADL $[\mathcal {F}_{\mathcal {B}}]$, we refer again to the six dimensions of auctions [33]:

• 1. Resources as from ADL, we can represent variants with single and multiple units. ADL $[\mathcal {F}_{\mathcal {B}}]$ also considers multiple types of goods;

• 2. Market structure while ADL is restricted to single-sided auctions, ADL $[\mathcal {F}_{\mathcal {B}}]$ also represents double auctions and exchange protocols. However, we cannot represent dynamic sets of agents and goods;

• 3. Preference structure as we are concerned with the general representation of auctions, we focus on how agents can express their preferences rather than on the underlying structures of their utility functions. Following the literature on mechanism design [54], we consider agents with quasi-linear utilities. In such a case, the agents’ utilities are based on a preference function over the outcomes and her payment. For a discussion on the hierarchy of preference functions, the reader may refer to Feige et al. [19];

• 4. Bid structure ADL $[\mathcal {F}_{\mathcal {B}}]$ can be used alongside different bidding languages. We define requirements for the bidding set and we illustrate how to employ two languages with different expressiveness in ADL $[\mathcal {F}_{\mathcal {B}}]$. This aspect was not previously explored with ADL;

• 5. Market clearing as for ADL, we can model single-sourcing auctions. ADL $[\mathcal {F}_{\mathcal {B}}]$ can also encode multi-sourcing auctions;

• 6. Information feedback in ADL $[\mathcal {F}_{\mathcal {B}}]$, direct mechanisms are described by a one-stage protocol and indirect mechanisms are represented by iterative protocols.

Hence, ADL $[\mathcal {F}_{\mathcal {B}}]$ addresses all these dimensions and is general enough to represent most settings. Notice that, similar to GDL (Game Description Language), ADL $[\mathcal {F}_{\mathcal {B}}]$ focuses on deterministic and perfect information protocols. GDL-II is an extension for handling imperfect information [64] and may be considered for auctions such as iterative sealed-bid auctions. These are however less common.

Beyond the auction setting, ADL $[\mathcal {F}_{\mathcal {B}}]$ is also able to represent several kinds of resource allocation problems: as noticed by Chevaleyre et al. [15], auctions can be seen as a subdivision of allocation mechanisms. The main characteristics of an auction are (i) central authority (the auctioneer), (ii) monetary transfer among participants, and (iii) agents’ preferences expressed through bids. All these key features are expressible in ADL $[\mathcal {F}_{\mathcal {B}}]$.

We also show how ADL $[\mathcal {F}_{\mathcal {B}}]$ can be used for the automated verification of mechanism design properties and for automatically checking whether descriptions written in $\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$ are well-formed. We illustrate the generality of ADL $[\mathcal {F}_{\mathcal {B}}]$ by focusing on two auction types: simultaneous ascending auction (SAA) and combinatorial exchange as we believe they are representative to demonstrate the expressive power of ADL $[\mathcal {F}_{\mathcal {B}}]$. Combinatorial exchange is a generalization of combinatorial and double-sided auctions, and SAA generalizes the English auction to multiple items. We evaluate these protocols in terms of the aforementioned properties. Finally, we show that if functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in polynomial time, then the model-checking problem for a $\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$-formula belongs to PTIME, that is, that it can be solved in polynomial time using a deterministic Turing machine.

The paper is organized as follows: in Sect. 2 we discuss the related work. In Sect. 3 we detail the semantics and syntax of ADL $[\mathcal {F}_{\mathcal {B}}]$. In Section 4 we introduce general properties for evaluating ADL $[\mathcal {F}_{\mathcal {B}}]$-based protocols. In Sects. 5 and 6, we show how to represent auctions in ADL $[\mathcal {F}_{\mathcal {B}}]$ and we demonstrate how to derive properties from their description. In Sect. 7, we explore the complexity of deciding whether an ADL $[\mathcal {F}_{\mathcal {B}}]$-formula is true with respect to a model and an execution of such model. Finally, Sect. 8 concludes the paper and discusses future work. The proofs omitted in the main text are presented in the appendix.

2 Related work

Our work is rooted in the key contributions on Auction Theory [36, 50, 51, 72]. All these works adopt a mechanism design perspective: they focus on designing and evaluating protocols and bidding languages. Our work has a different purpose. The ADL $[\mathcal {F}_{\mathcal {B}}]$ language is intended to represent the auction protocols and to allow a modular definition of actions sets, which may be characterized by a subset of a bidding language. ADL $[\mathcal {F}_{\mathcal {B}}]$ can be used to automatically derive properties for these protocols. ADL $[\mathcal {F}_{\mathcal {B}}]$ is also a tool for mechanism design, since it is a well suited framework for testing new auctions.

2.1 Auction representation

To the best of our knowledge, almost all contributions on the computational representation of auctions focus on the implementation of the winner determination problem. For instance, Baral and Ulyan [4] 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 [38]: they focus on sealed-bid auctions and show how qualitative reasoning helps to refine the optimal quantitative solutions. Giovannucci et al. [22] explore a graphical formalism to compactly represent the winner determination problem for multi-unit combinatorial auctions. Linear Logic has also been used [57] for modeling combinatorial auctions. The authors explore the representation of bids and the winner determination. However, there is no temporal operator to allow reasoning on iterative auctions.

The descriptive auction language [59] allows a formal specification of auctions. Agents can only bid through XOR combinations of items. Although the XOR language is widely used, the specification approach is more flexible when the bidding language is not fixed for all protocols. In fact, as stated by Nisan [51], the choice of a bidding language should aim to find a balance between expressivity (i.e., being able to express every preference function) and simplicity (i.e., being intuitive and computationally efficient). There are numerous auction protocols that do not require the expressive power of the XOR language and can be implemented with simpler bidding languages. For instance, in a Dutch auction, agents may simply say whether they accept the current selling price or not. Our proposal is intended to be more flexible, as one may use different bidding languages with ADL $[\mathcal {F}_{\mathcal {B}}]$ for defining distinct protocols.

A rule-based scripting language for representing single-dimensional auctions have been proposed by Lochner et al. [39]. Since it is single-dimensional, bids are composed exclusively by prices. On the other hand, the framework Multiple criteria English Reverse Auctions (MERA) [7, 8] characterizes bids with vectors of attributes and criteria. MERA allows to represent English reverse auctions that differ in relation to the aggregation model of bidders’ preferences and the information feedback provided to the participants.

2.2 Representation of negotiation protocols

A related problem to auction specification is the one of representing negotiation protocols. As noted by Meyer et al. [43] negotiation is investigated from different perspectives, such as economics, psychology, computer science and others. Consequently, there is no agreement in relation to its definition and the distinction between negotiation and auctions may be vague. Although some authors consider auctions as types of negotiation protocols, in this work we consider them related, but rather distinct, types of allocation procedures.

Following the definition from Chevaleyre et al. [15], by auctions we refer to centralized mechanisms that specify trades of items and payments based on the bidders’ reported preferences. On the other hand, we consider that in negotiation protocols, allocations emerge as the result of a sequence of local negotiation steps. That is, they describe the negotiation over resources in a distributed setting. Another important difference is that negotiation protocols for exchanging goods may not be dependant on monetary transfer.

In their paper [3], Bădică et al. discuss how rule-based approaches can be used to automated negotiation. The paper focuses on experimental results for concurrent negotiation and do not address the generality of their approach. Huder et al. [25] propose a framework to enable negotiations according to bilateral and multilateral negotiation protocols using a meta-language to define protocols based on a set of attributes and parameters. In a subsequent work [24], the authors propose a language based on Extensible Markup Language (XML) for meta-negotiating the choice of negotiation protocols and for instantiating and parameterizing the system used for conducting the chosen protocol. Similarly, rule-markup languages have also been used for the declarative representation of negotiations [18].

Due to the lack of a precise semantics, the approaches considered up to here are too poor to enable reasoning. This limitation motivates the use of logic-based languages. In two papers [70, 71], Wooldridge and Parsons briefly compare the use of different languages for negotiation, including propositional logic, a language for electronic commerce and a negotiation meta-language. The problems considered involve simple protocols with multi-attribute negotiation of single goods. Even in this setting, the problems of determining if agreement has been reached and determining if a particular protocol will terminate are computationally hard. A basic logical framework for negotiation has also been proposed by Meyer et al. [43]. In the two agents setting, the work explores modes of negotiation from which an agreement over an outcome can be reached when the participants are rational, cooperative and truthful.

2.3 GDL-based approaches

The Game Description Language (GDL) is the official language used for the General Game Playing (GGP) competition [21]. Due to its initial limitations, several extensions and variants have been successfully proposed, including GDL with imperfect information (GDL-II) [64] and introspection (GDL-III) [65] for specifying epistemic games. GDL has also been extend for defining, comparing and combining strategies in [77, 78]. This extension includes the dual connectives prioritised disjunction and prioritised conjunction for expressing preferences when combining strategies.

The use of GDL-based languages for describing market-based protocols have also been studied. De Jonge and Zhang [31] discuss the use of GDL for modeling negotiation. The main advantage is being able to apply the existing domain-independent techniques from GGP. For instance, the Monte Carlo Tree Search algorithm has been adapted for negotiations in non-zero-sum games [32]. In another paper [30], they propose the use of GDL as a unifying language for defining general and complex negotiation domains.

The closest contributions to ours are the Market Specification Language (MSL) [66] and ADL [45, 46], also based on GDL. Both works focus on representing single item auctions 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 lack of a clear link between the language, the mechanism formalization and the agents’ preferences, which prevents the evaluation of GDL-based specifications as mechanisms. In this paper, we extend ADL [46] for enabling the integration with bidding language and going further on the representation of quantitative aspects.

2.4 Formal verification of auctions

To some extent, our work is also related to the literature of formal verification of auctions. Some works explore computed-aided verification [5, 12, 34], where the process is only assisted by a reasoner. There are also works that focus on a particular variant of an auction. For instance, model-checking approaches have been proposed for verifying suspect behaviors of bidders in concurrent online auctions [73, 74]. Based on Artifact Systems techniques, Belardinelli [6] explores the model checking of properties concerning the evolution of the bidding process in simultaneous ascending auctions. A similar approach investigates the verification of agent-based English auctions using temporal logic [2]. A more general concept has also been introduced [56, 69], where the authors advocate the use of Alternating-time Temporal Logic [1] to reason about economic mechanisms. Strategy Logic (SL) [14, 47] allows for explicit representation of strategies, which enables capturing solution concepts from Game Theory [52]. In [42], the authors investigate a quantitative version of SL with imperfect information for the automated verification of indirect mechanisms. However, as SL and ATL cannot model the internal structures of strategies, these languages are not fitted for reasoning about the actions that were actually executed in a moment of the game, which is an important feature to be considered for General Game Playing.

In this paper, we show how ADL $[\mathcal {F}_{\mathcal {B}}]$ is suitable for the automated verification of direct revelation mechanisms. We encode individual rationality, efficiency and budget-balance as ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae. Verifying such properties amounts to model-checking ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae, which can be done in PTIME, when functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in PTIME. Other properties can be analyzed via meta-reasoning and we exemplify this case with strategyproofness.

3 Auction description language with a set of functions $\mathcal {F}_\mathcal {B}$

The Auction Description Language with a set of functions $\mathcal {F}_\mathcal {B}$ (ADL $[\mathcal {F}_{\mathcal {B}}]$) is a framework for specification of auction-based markets and it is composed by a state-transition model and a logical language. To encode an auction, we first define its signature, which specifies the participants (the agents), the goods being traded and the propositions and variables describing each state of the auction:

Definition 1

An auction signature $\mathcal {S}$ is a tuple $(\text {N}, \text {G}, \mathcal {B}, {\Upphi }, \text {Y}, \text {I}, \mathcal {F}_{\mathcal {B}})$, where:

• $\text {N}= \{1, \ldots , \mathsf {n}\}$ is a nonempty finite set of agents (or bidders);

• $\text {G}= \{1, \ldots , \mathsf {m}\}$ is a finite set of good types;

• $\mathcal {B}$ is a nonempty finite set of bids (or actions);

• ${\Upphi }$ is a finite set of atomic propositions specifying features of a state;

• $\text {Y}$ is a finite set of numerical variables specifying numerical features of a state;

• $\text {I}\subset \mathbb {Z}$ is an interval of integer numbers, denoting the value range for any countable component of the framework. We assume $\text {I}$ is equipped with a partial order²$\preceq _\text {I}$, capturing the standard less-than-or-equal relation over its elements. We let $z_{\text {min}}, z_{\text {max}}\in \mathbb Z$ denote the minimum and maximum values in $\text {I}$, that is, $z_{\text {min}}\preceq _\text {I}z$ and $z \preceq _\text {I}z_{\text {max}}$ for each $z \in \text {I}$. By convenience, we assume $0\in \text {I}$ and denote $\text {I}_{\succeq 0}= [0,z_{\text {max}}]$ and $\text {I}_{\succ 0}= (0, z_{\text {max}}]$ as the non-negative and positive parts of $\text {I}$, respectively. Similarly, $\text {I}_{\preceq 0}= [z_{\text {min}},0]$ and $\text {I}_{\prec 0}= [z_{\text {min}}, 0)$ denote the non-positive and negative parts of $\text {I}$.

• $\mathcal {F}_{\mathcal {B}}\subseteq \{f: \mathcal {B}^\mathsf {a}\times \text {I}^\mathsf {b}\rightarrow \text {I}\mid \mathsf {a}, \mathsf {b}\in \text {I}_{\succeq 0}\}$ is a set of state-independent functions of possibly different arities.

Hereafter, we will fix an auction signature $\mathcal {S}$ and all concepts will be based on this signature, except if stated otherwise. Note that $z_{\text {min}}$ and $z_{\text {max}}$, in the definition of $\text {I}$, should be large enough to represent the total supply of goods being traded as well as the cumulative available money among agents. Through the rest of this paper, we assume that is the case. Any function value outside $\text {I}$ is rounded to the nearest value $z_{\text {min}}$ or $z_{\text {max}}$. We assume that $\mathcal {F}_{\mathcal {B}}$ contains the functions $\text {sum}(z_1,z_2) = z_1+z_2$, $\text {sub}(z_1,z_2) = z_1-z_2$, $\text {times}(z_1,z_2) = z_1 \cdot z_2$, denoting the addition, subtraction and multiplication of two integers $z_1, z_2 \in \text {I}$, respectively. Similarly, we also assume $\mathcal {F}_{\mathcal {B}}$ contains the functions

$$\begin{aligned} \max (z_1,z_2) = \left\{ \begin{array}{ll} z_1 &{} \text { if } z_2 \preceq _\text {I}z_1\\ z_2 &{} \text { otherwise } \end{array}\right. \end{aligned}$$

and

$$\begin{aligned} \min (z_1,z_2) = \left\{ \begin{array}{ll} z_1 &{} \text { if } z_1 \preceq _\text {I}z_2\\ z_2 &{} \text { otherwise } \end{array}\right. \end{aligned}$$

capturing the maximum and minimum among two integers $z_1, z_2 \in \text {I}$.

Given a list integers $(z_{\mathsf {i}})_{\mathsf {i}\in \text {N}} \in \text {I}^\mathsf {n}$ and a 2-ary function $f \in \mathcal {F}_{\mathcal {B}}$ such that $f:\text {I}\times \text {I}\rightarrow \text {I}$, we will use the following shortcut:

$$\begin{aligned}f_{\mathsf {i}\in \text {N}}(z_\mathsf {i}) = f(z_1, f(z_2, f(\ldots, f(z_{\mathsf {n}-1}, z_{\mathsf {n}}) )) )\end{aligned}$$

A trade is a tuple $(\uplambda _{\mathsf {i}, j})_{j\in \text {G}, \mathsf {i}\in \text {N}} \in \text {I}^{\mathsf {n}\mathsf {m}}$, where $\uplambda _{\mathsf {i}, j}$ denotes the number of units $j$ being traded by agent $\mathsf {i}$. A trade specifies which items each agent is selling and/or buying. A positive trade expresses how many units of a good type are purchased and a negative trade represents how many units are sold. Similarly, a positive payment denotes how much a buyer will pay and a negative payment expresses how much a seller will receive.

A tuple of objects indexed by agents in $\text {N}$ is called a profile. In a profile, we may omit the index set and we write it in bold, e.g., $\varvec{\uplambda }$ for $(\uplambda _{\mathsf {i}})_{\mathsf {i}\in \text {N}}$ and $\varvec{(\uplambda _{j})}_{j\in \text {G}}$ for $(\uplambda _{\mathsf {i}, j})_{j\in \text {G}, \mathsf {i}\in \text {N}}$. Given a profile $\varvec{o}$, we let $o_\mathsf {r}$ be the component of agent $\mathsf {r}$ and $o_{-\mathsf {r}}$ be $(o_\mathsf {i})_{\mathsf {i}\ne \mathsf {r}}$.

Let us now present the model and the language’s syntax and semantics.

3.1 Syntax

Let $\mathcal {L}_{z}$ be the set of numerical terms, with each $z\in \mathcal {L}_{z}$ defined as follows:

$$\begin{aligned} z::=x \mid \text {y}\mid f(\upbeta , \ldots , \upbeta , z, \ldots , z) \end{aligned}$$

where $\upbeta \in \mathcal {B}$ is an action, $x \in \text {I}$ is an integer, $\text {y}\in \text {Y}$ is a numerical variable and $f\in \mathcal {F}_{\mathcal {B}}$ is a function³.

The logical language for ADL $[\mathcal {F}_{\mathcal {B}}]$ is denoted by $\mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$ and a formula $\varphi$ in $\mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$ is defined by the following Backus-Naur Form grammar:

$$\begin{aligned} \varphi ::=p\mid initial\mid terminal\mid legal_\mathsf {i}(\upbeta ) \mid does_\mathsf {i}(\upbeta ) \mid \lnot \varphi \mid \varphi \wedge \varphi \mid \bigcirc \varphi \mid z\ \le \ z\end{aligned}$$

where $p\in {\Upphi }$ is a proposition, $\mathsf {i}\in \text {N}$ is an agent, $\upbeta \in \mathcal {B}$ is an action and $z\in \mathcal {L}_{z}$ is a numerical term.

Intuitively, $initial$ and $terminal$ specify the initial terminal states, resp.; $legal_\mathsf {i}(\upbeta )$ asserts that agent $\mathsf {i}$ is allowed to take action $\upbeta$ at the current state and $does_\mathsf {i}(\upbeta )$ asserts that agent $\mathsf {i}$ takes action $\upbeta$ at the current state. The formula $\bigcirc \varphi$ means “$\varphi$ holds at the next state”. The formula $z_1 \le z_2$ means that the numerical term $z_1$ is smaller or equal to the numerical term $z_2$.

We use the standard abbreviations from propositional logic, such as $\varphi \vee \psi$ for $\lnot (\lnot \varphi \wedge \lnot \psi )$, $\varphi \rightarrow \psi$ for $\lnot \varphi \vee \psi$, and $\varphi \leftrightarrow \psi$ for $(\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \varphi )$. We take $\top$ to be an abbreviation for some fixed propositional tautology such as $p \vee \lnot p$, and let $\bot$ be an abbreviation of $\lnot \top$. We also use abbreviations for comparison operators, such as $z_1 = z_2$ for $z_1 \le z_2 \wedge z_2 \le z_1$, $z_1 < z_2$ for $z_1 \le z_2 \wedge \lnot (z_1=z_2)$, $z_1 \ne z_2$ for $\lnot (z_1 = z_2)$, $z_1 \ge z_2$ for $z_2 \le z_1$ and $z_1 > z_2$ for $z_1 \ge z_2 \wedge z_1 \ne z_2$. The extension of the comparison operators to multiple arguments is straightforward.

Assume the bids $\varvec{\upbeta } = (\upbeta _\mathsf {i})_{\mathsf {i}\in \text {N}}$, where $\upbeta _\mathsf {i}\in \mathcal {B}$ is a bid associated to the agent $\mathsf {i}\in \text {N}$. The formula $does(\varvec{\upbeta }) =_{\text {def}}\bigwedge _{\mathsf {i}\in \text {N}} does_\mathsf {i}(\upbeta _\mathsf {i})$ represents that the agents in $\text {N}$ perform the joint action $\varvec{\upbeta }$.

3.2 Semantics

The semantics of ADL $[\mathcal {F}_{\mathcal {B}}]$ are based on state-transition models, which allows us to represent the key aspects of an auction, at first the legal bids and the transitions among states.

Definition 2

A state-transition-model (ST-model for short) $\text {M}$ is a tuple $(\text {W}, \bar{\text {w}}, \text {T}, \text {L}, \text {U}, \uppi _{{\Upphi }}, \uppi _{\text {Y}})$, where:

• $\text {W}$ is a nonempty set of states;

• $\bar{\text {w}}\in \text {W}$ is the initial state;

• $\text {T}\subseteq \text {W}$ is a set of terminal states;

• $\text {L}\subseteq \text {W}\times \text {N}\times \mathcal {B}$ is a legality relation, describing the legal actions at each state, we let $\text {L}(\text {w}, \mathsf {i}) = \{a \in \mathcal {B}\mid (\text {w},\mathsf {i},a) \in \text {L}\}$ be the set of all legal actions for agent $\mathsf {i}$ at state $\text {w}$;

• $\text {U}: \text {W}\times \mathcal {B}^\mathsf {n}\rightarrow \text {W}$ is an update function, given $\varvec{\varvec{d}}\in \mathcal {B}^\mathsf {n}$, let $d_\mathsf {i}$ be the individual action for agent $\mathsf {i}$ in the joint action $\varvec{d}$;

• $\uppi _{{\Upphi }}: \text {W}\rightarrow 2^{\Upphi }$ is the valuation function for the state propositions;

• $\uppi _{\text {Y}}: \text {W}\times \text {Y}\rightarrow \text {I}$, is the valuation function for the numerical variables.

A path represents a run or execution of an auction protocol. Formally,

Definition 3

Given an ST-model $\text {M}= (\text {W}, \bar{\text {w}}, \text {T}, \text {L}, \text {U}, \uppi _{{\Upphi }}, \uppi _{\text {Y}})$, a path is a sequence of states and joint actions $\text {w}_0 \mathop {\rightarrow }\limits ^{\varvec{d}^1} \text {w}_1 \mathop {\rightarrow }\limits ^{\varvec{d}^2}\dots \mathop {\rightarrow }\limits ^{\varvec{d}^{t}} \text {w}_{t} \mathop {\rightarrow }\limits ^{\varvec{d}^{t+1}} \dots$ such that for any $t\ge 1$: (i) $\text {w}_0 = \bar{\text {w}}$; (ii) $\text {w}_{t} \ne \text {w}_0$; (iii) $d_\mathsf {i}^{t} \in \text {L}(\text {w}_{t-1}, \mathsf {i})$ for any $\mathsf {i}\in \text {N}$, (iv) $\text {w}_{t} = \text {U}(\text {w}_{t-1}, \varvec{d}^t)$; and (v) if $\text {w}_{t-1} \in \text {T}$, then $\text {w}_{t-1} = \text {w}_{t}$.

For any path $\updelta$, let $\updelta [t]$ denote the $t$-th state of $\updelta$, $\uptheta (\updelta , t)$ denote the joint action performed at stage $t$ of $\updelta$, $\uptheta _{\mathsf {i}} (\updelta , t)$ denote the action of agent $\mathsf {i}$ performed at stage $t$ of $\updelta$, and $\updelta [0,t]$ denote the finite prefix $\bar{\text {w}}\mathop {\rightarrow }\limits ^{\varvec{d}^1} \text {w}_1 \mathop {\rightarrow }\limits ^{\varvec{d}^2} \ldots \mathop {\rightarrow }\limits ^{\varvec{d}^t} \text {w}_{t}$. A path $\updelta$ is complete if $\updelta [e] \in \text {T}$, for some $e> 0$. After reaching a terminal state $\updelta [e]$, for any $e' > e$, $\updelta [e'] = \updelta [e]$. Finally, for a given model $\text {M}$, any state $\text {w}$ such that there exists a complete path $\updelta$ of $\text {M}$ such that $\text {w}\in \updelta$ will be called a reachable state of $\text {M}$.

The semantics for ADL $[\mathcal {F}_{\mathcal {B}}]$ is given in two steps. First, we define function $f_z$ to compute the meaning of numerical terms $z\in \mathcal {L}_{z}$ in some specific state. Next, a formula $\varphi \in \mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$ is interpreted with respect to a stage in a path.

Definition 4

Given an ST-model $\text {M}$, we define function $f_z: \mathcal {L}_{z}\times \text {W}\rightarrow \text {I}$, assigning any $z\in \mathcal {L}_{z}$ and state $\text {w}\in \text {W}$ to a number in $\text {I}$:

$$\begin{aligned} f_z(z, \text {w}) = {\left\{ \begin{array}{ll} \uppi _{\text {Y}}(\text {w}, z) &{} \text { if } z\in \text {Y}\\ f(\upbeta _1, \ldots , \upbeta _n, f_z(z_1, \text {w}), \ldots , f_z(z_m, \text {w})) &{} \text { if } z= f(\upbeta _1, \ldots , \upbeta _n, z_1, \ldots , z_m)\\ z&{} \text { if } z\in \text {I}\end{array}\right. }\end{aligned}$$

where $n,m\in \text {I}_{\succeq 0}$.

Definition 5

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

$$\begin{aligned} \begin{array}{lllll} \text {M}, \updelta , t\models p&{} &{} \text {iff} &{} &{} p\in \uppi _{{\Upphi }}(\updelta [t]) \\ \text {M}, \updelta , t\models \lnot \varphi &{} &{}\text {iff} &{}&{} \text {M}, \updelta , t\not \models \varphi \\ \text {M}, \updelta , t\models \varphi _1 \wedge \varphi _2 &{} &{}\text {iff} &{}&{} \text {M}, \updelta , t\models \varphi _1 \text { and } \text {M}, \updelta , t\models \varphi _2 \\ \text {M}, \updelta , t\models initial&{} &{}\text {iff} &{}&{} \updelta [t]= \bar{\text {w}}\\ \text {M}, \updelta , t\models terminal&{} &{}\text {iff} &{}&{} \updelta [t]\in \text {T}\\ \text {M}, \updelta , t\models legal_\mathsf {i}(\upbeta ) &{} &{}\text {iff} &{}&{} \upbeta \in \text {L}(\updelta [t], \mathsf {i}) \\ \text {M}, \updelta , t\models does_\mathsf {i}(\upbeta ) &{} &{}\text {iff} &{}&{} \uptheta _{\mathsf {i}} (\updelta , t) = \upbeta \\ \text {M}, \updelta , t\models \bigcirc \varphi &{} &{}\text {iff} &{}&{} \text {M}, \updelta , t+1 \models \varphi \\ \text {M}, \updelta , t\models z_1 \ \le \ z_2 &{} &{} \text {iff} &{} &{} f_z(z_1, \updelta [t]) \ \preceq _\text {I}\ f_z(z_2, \updelta [t]) \end{array}\end{aligned}$$

A formula $\varphi$ is globally true through $\updelta$, denoted by $\text {M}, \updelta \models \varphi$, if $\text {M}, \updelta , t\models \varphi$ for any stage $t$ of $\updelta$. A formula $\varphi$ is globally true in an ST-model $\text {M}$, written $\text {M}\models \varphi$, if $\text {M}, \updelta \models \varphi$ for all paths $\updelta$ in $\text {M}$. Finally, let $\Sigma$ be a set of formulae in $\mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$, then $\text {M}$ is a model of $\Sigma$ if $\text {M}\models \varphi$ for all $\varphi \in \Sigma$.

Similar to Epistemic GDL [29], the following propositions hold:

Proposition 1

Let $\text {M}$ be an ST-model, for each agent $\mathsf {i}\in \text {N}$ and each action $\upbeta \in \mathcal {B}$,

• 1. $\text {M}\models does_\mathsf {i}(\upbeta ) \rightarrow \lnot does_\mathsf {i}(\upbeta ')$, for any $\upbeta ' \in \mathcal {B}$ such that $\upbeta ' \ne \upbeta$

• 2. $\text {M}\models \bigvee _{\upbeta ' \in \mathcal {B}} does_\mathsf {i}(\upbeta ')$

• 3. $\text {M}\models does_\mathsf {i}(\upbeta ) \rightarrow legal_\mathsf {i}(\upbeta )$

• 4. $\text {M}\models \lnot \bigcirc initial$

• 5. $\text {M}\models terminal\wedge \varphi \rightarrow \bigcirc \varphi$, for any $\varphi \in \mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$

• 6. $\text {M}\models initial\rightarrow \lnot terminal$

Statements 1 and 2 specify an agent performs exactly one action in each state. Furthermore, if she does an action, then it must be legal (Statement 3). As a consequence from the path construction, we have that no state can be followed by the initial one (Statement 4) and any formula that holds in a terminal state also holds in the subsequent state (Statement 5). Finally, if a state is the initial one then it is not a terminal state (Statement 6).

We also have tautologies related to the partial order $\preceq _\text {I}$:

Observation. Let $\text {M}$ be an ST-model, $\mathsf {i}\in \text {N}$ be an agent, $z = (z_1, z_2, \dots , z_n)$ be a list of numerical terms (i.e., $z \in \mathcal {L}_{z}^n$) and $f \in \mathcal {F}_{\mathcal {B}}$ be any function such that $f:\text {I}^n \rightarrow \text {I}$, for some $n\in \text {I}_{\succ 0}$,

• 1. $\text {M}\models z_1 \ \mathfrak {R}\ z_1$, for $\mathfrak {R}\in \{\le , \ge , =\}$

• 2. $\text {M}\models z_1 \ \mathfrak {R}\ z_2 \wedge z_2 \ \mathfrak {R}\ z_1 \rightarrow z_1 = z_2$, for $\mathfrak {R}\in \{\le , \ge , =\}$

• 3. $\text {M}\models z_1 \ \mathfrak {R}\ z_2 \wedge z_2 \ \mathfrak {R}\ z_3 \rightarrow z_1 \ \mathfrak {R}\ z_3$, for $\mathfrak {R}\in \{\le , \ge , =\}$

• 4. $\text {M}\models z_i = z_j \leftrightarrow f(z_i, z_{-i}) = f(z_j, z_{-i})$, for any $1\le i \le n$

• 5. $\text {M}\models z_1 = z_2 \leftrightarrow z_2 = z_1$

• 6. $\text {M}\models z_1 \ \mathfrak {R}\ z_2 \rightarrow \lnot (z_2 \ \mathfrak {R}\ z_1)$, for $\mathfrak {R}\in \{<,>\}$

Statements 1, 2 and 3 are a consequence from $\preceq _\text {I}$ being reflexive, antisymmetric and transitive, respectively. Ceteris paribus, two numerical terms are equal if and only if the value obtained after applying f is equal for both terms (Statement 4). Statement 5 says that the equality operator is symmetric and Statement 6 states that the operators representing the relations smaller-than and greater-than are asymmetric.

Requirements for representing verifiable auctions For verifying a protocol expressed in ADL $[\mathcal {F}_{\mathcal {B}}]$ with respect to properties from mechanism design, its signature $\mathcal {S}= (\text {N}, \text {G}, \mathcal {B}, {\Upphi }, \text {Y}, \text {I}, \mathcal {F}_{\mathcal {B}})$ must comply with the following requirements:

• $\mathcal {F}_{\mathcal {B}}$ should include a function $v_\mathsf {i}: \mathcal {B}\times \text {I}^{\mathsf {n}\mathsf {m}} \rightarrow \text {I}$ for each agent $\mathsf {i}\in \text {N}$, where $v_\mathsf {i}(\upbeta , \varvec{\uplambda })$ denotes the value of $\upbeta$ given a joint trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$, i.e., $v_\mathsf {i}(\upbeta , \varvec{\uplambda })$ represents the value reported for trade $\varvec{\uplambda }$ under $\mathsf {i}$’s bid $\upbeta$;

• There are no duplicate bids in $\mathcal {B}$, that is, there are no two bids $\upbeta , \upbeta ' \in \mathcal {B}$, such that $\upbeta \ne \upbeta '$ and $v_\mathsf {i}(\upbeta , \varvec{\uplambda }) = v_\mathsf {i}(\upbeta ', \varvec{\uplambda })$, for any trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$ and any agent $\mathsf {i}$;

• Each payment and trade should be represented as a numerical variable, that is, $\{payment_{\mathsf {i}},$ $trade_{\mathsf {i},j} : \mathsf {i}\in \text {N}, j\in \text {G}\} \subseteq \text {Y}$. The variables $payment_{\mathsf {i}}$ and $trade_{\mathsf {i},j}$ denote the value in a state of agent $\mathsf {i}$’s payment and her trade for the good $j$, respectively.

Other functions may as well be included in $\mathcal {F}_{\mathcal {B}}$. For instance, for indirectly representing market clearing with ADL $[\mathcal {F}_{\mathcal {B}}]$, one may encode a winner determination function, such that it assigns bids and allocations to trades. Such function is not a compulsory requirement for the bidding language, since we can also directly represent the market clearing through $\mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$-rules.⁴

4 Evaluating auction-based protocols

In this section, we explore the general evaluation of auction-based protocols. First, we recall concepts from mechanism design and present their formulation in ADL $[\mathcal {F}_{\mathcal {B}}]$. As for GDL, we then define well-formulated protocol descriptions.

4.1 Mechanism design

A mechanism aggregates agents’ preferences and decides for an outcome (e.g., an allocation of goods, a result of an election, etc) [16]. Auctions are a type of mechanism, in which the outcome is described in terms of trades and monetary transfers among the participants. According to a given objective, the goal of Mechanism Design (MD) is to design a game (i.e., the mechanism) such that an outcome with desirable features is reached, despite the agents’ self interests [62]. The objective of a mechanism can include, for instance, truthfulness of agents (i.e., strategyproofness), maximization of social welfare (i.e., efficiency), voluntary participation (i.e., individual rationality), and so on.

Let us recall concepts from MD and show how to represent some classical but important objectives (hereafter called properties) in ADL $[\mathcal {F}_{\mathcal {B}}]$, namely budget-balance, efficiency, individual rationality and strategyproofness. As we focus on auctions, we denote the mechanism outcome as a pair $(\varvec{\uplambda }, \mathbf{p} )$, where $\varvec{\uplambda }= \varvec{(\uplambda _{j})}_{j\in \text {G}}$ is a trade and $\text {p}_\mathsf {i}$ is the payment for agent $\mathsf {i}$.

The preference of an agent $\mathsf {i}$ in $\text {N}$ over a trade $\varvec{\uplambda }$ is modeled by a preference function $\vartheta _\mathsf {i}: \text {I}^{\mathsf {n}\mathsf {m}} \rightarrow \text {I}$, where $\vartheta _\mathsf {i}\in V_\mathsf {i}$ and $V_\mathsf {i}$ is a finite set of possible preference functions for $\mathsf {i}$. We call $V_\mathsf {i}$ the preference space of $\mathsf {i}$. We classically assume that the utility of agent $\mathsf {i}$ over an outcome $(\varvec{\uplambda }, \mathbf{p} )$ is quasi-linear (i.e., the utility’s dependence on the payment is separable and linear)⁵, defined as $\vartheta _\mathsf {i}(\varvec{\uplambda }) - \text {p}_\mathsf {i}$.

Since different action sets may have different expressiveness and syntactical structures, we use the value reported in a bid for a given trade to assess whether the bid represents the agent’s preference function.

Definition 6

Let $\mathcal {B}$ be an action set and $V_\mathsf {i}$ be the preference space of agent $\mathsf {i}\in \text {N}$. A bid $\upbeta \in \mathcal {B}$ represents a preference function $\vartheta _\mathsf {i}\in V_\mathsf {i}$, denoted by $\upbeta \sim _{\mathsf {i}} \vartheta _\mathsf {i}$, iff $v_{\mathsf {i}}(\upbeta , \varvec{\uplambda }) = \vartheta _\mathsf {i}(\varvec{\uplambda })$, for all trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$.

Similarly, an action set may represent a preference space. In this case, exactly one bid in the action set should represent a preference function.

Definition 7

Given a set of actions $\mathcal {B}$ and a preference space $V_\mathsf {i}$ of agent $\mathsf {i}\in \text {N}$, we say $\mathcal {B}$ represents $V_\mathsf {i}$, denoted by $\mathcal {B}\approx _\mathsf {i}V_\mathsf {i}$ iff for each $\vartheta _\mathsf {i}\in V_\mathsf {i}$ there exists a unique bid $\upbeta \in \mathcal {B}$ such that $\upbeta \sim _\mathsf {i}\vartheta _\mathsf {i}$ and for each bid $\upbeta \in \mathcal {B}$ there exists a preference function $\vartheta _\mathsf {i}\in V_\mathsf {i}$ such that $\upbeta \sim _\mathsf {i}\vartheta _\mathsf {i}$.

If $\mathcal {B}\approx _\mathsf {i}V_\mathsf {i}$, for each $\vartheta _\mathsf {i}\in V_\mathsf {i}$ we let $\upbeta _{\vartheta _\mathsf {i}}$ denote the bid $\upbeta \in \mathcal {B}$ such that $\upbeta \sim _\mathsf {i}\vartheta _\mathsf {i}$, that is, $\upbeta _{\vartheta _\mathsf {i}}$ is the bid that represents $\vartheta _\mathsf {i}$. Given a preference profile $\varvec{\vartheta }$, let $\varvec{\upbeta _{\vartheta }} = (\upbeta _{\vartheta _{\mathsf {i}}})_{\mathsf {i}\in \text {N}}$ denote the profile of bids representing $\varvec{\vartheta }$.

Notice not all elements of $\text {I}$ are feasible values for trades, for instance in a traditional English auction, the trade for each agent should be either 0 or 1 while the interval $\text {I}$ could include greater values for encoding the payments. In the following, the possible choices considered for trades in the mechanism are denoted $\Uplambda \subseteq \text {I}^{\mathsf {n}\mathsf {m}}$.

An indirect mechanism describes the available actions for each agent and an outcome function that maps vectors of actions (also know as strategies) into outcomes. In a direct mechanism, each agent’s available action consists on reporting preferences from her preference space [26]. Formally, a direct mechanism is defined as follows [52]:

Definition 8

A direct mechanism $(\mathsf {s}, \varvec{\mathsf {p}})$ specifies a social choice function $\mathsf {s}: \prod _{\mathsf {i}\in \text {N}} V_\mathsf {i}\rightarrow \Uplambda$ and a profile of payment functions $\varvec{\mathsf {p}}$, where $\mathsf {p}_\mathsf {i}: \prod _{\mathsf {i}\in \text {N}} V_\mathsf {i}\rightarrow \text {I}$ denotes the amount agent $\mathsf {i}$ pays (or receives).

Regardless whether a protocol is multi- or single-stage, we view each step $\text {w}_e \mathop {\rightarrow }\limits ^{\varvec{d}^{e+1}} \text {w}_{e+1}$ of a path $\text {w}_0 \mathop {\rightarrow }\limits ^{\varvec{d}^1} \text {w}_1 \mathop {\rightarrow }\limits ^{\varvec{d}^2}\dots \mathop {\rightarrow }\limits ^{\varvec{d}^{t}} \text {w}_{t} \mathop {\rightarrow }\limits ^{\varvec{d}^{t+1}} \dots$ in an ST-model $\text {M}$ as a direct mechanism, where $e\ge 0$ and the social choice and payments are encoded by the update and valuation functions in $\text {M}$. Formally,

Definition 9

Given a preference space profile $\varvec{V}$, an ST-model $\text {M}$ and a state $\text {w}\in \text {W}$ such that $\text {L}(\text {w}, \mathsf {i}) \approx _\mathsf {i}V_\mathsf {i}$ for each $\mathsf {i}\in \text {N}$, and let the set of possible trades be defined as $\Uplambda = \{(\uppi _{\text {Y}}(\text {w}', trade_{\mathsf {i}, j}))_{\mathsf {i}\in \text {N}, j\in \text {G}}: \text {w}' = \text {U}(\text {w}, \varvec{\upbeta _{\vartheta }})$ & $\varvec{\vartheta }\in \prod _{\mathsf {i}\in \text {N}} V_\mathsf {i}\}$. Then state $\text {w}$ is a direct mechanism $(\mathsf {s}, \varvec{\mathsf {p}})$, where for each $\varvec{\vartheta }\in \prod _{\mathsf {i}\in \text {N}} V_\mathsf {i}$, the outcome is denoted by the valuation of the numerical variables regarding trades and payments in the state $\text {w}' = \text {U}(\text {w}, \varvec{\upbeta _{\vartheta }})$. The social choice function is

$$\begin{aligned}\mathsf {s}(\varvec{\vartheta }) = \varvec{(\uplambda _{j})}_{j\in \text {G}} \end{aligned}$$

where $\uplambda _{\mathsf {i}, j} = \uppi _{\text {Y}}(\text {w}', trade_{\mathsf {i}, j})$ for each agent $\mathsf {i}$ and good $j$. The payment function for agent $\mathsf {i}$ is

$$\begin{aligned}\mathsf {p}_\mathsf {i}(\varvec{\vartheta }) = \uppi _{\text {Y}}(\text {w}', payment_{\mathsf {i}})\end{aligned}$$

The state $\text {w}' = \text {U}(\text {w}, \varvec{\upbeta _{\vartheta }})$ in the above definition is called an outcome state. Any reachable state in an ST-model is an outcome state, except the initial state. For the next subsections, we fix an ST-Model $\text {M}$ and a preference space profile $\varvec{V}$ such that $\text {L}(\text {w}, \mathsf {i}) \approx _\mathsf {i}V_\mathsf {i}$ for each agent $\mathsf {i}$ and state $\text {w}\in \text {W}$.

4.1.1 Budget-balanced mechanisms

A mechanism is strongly budget-balanced (SBB) if the cumulative payment among the bidders is zero, for every preference they may have [44]. A mechanism where there is no monetary deficit, that is, where only the designer can earn revenue, is called weakly budget-balanced (WBB) [44]. This condition is a relaxation from SBB, where the cumulative payment among the bidders cannot be negative.

Definition 10

A direct mechanism $(\mathsf {s}, \varvec{\mathsf {p}})$ is strongly budget-balanced (resp. weakly budget-balanced) if for each $\varvec{\vartheta } \in \prod _{\mathsf {i}\in \text {N}} V_\mathsf {i}$,

$$\begin{aligned}\sum _{\mathsf {i}\in \text {N}}\mathsf {p}_\mathsf {i}(\varvec{\vartheta }) = 0 \text { (resp. }\sum _{\mathsf {i}\in \text {N}}\mathsf {p}_\mathsf {i}(\varvec{\vartheta }) \ge 0\text {)}\end{aligned}$$

We denote the condition of a state being SBB by the following ADL $[\mathcal {F}_{\mathcal {B}}]$-formula:

$$\begin{aligned}sbb=_{\text {def}}\text {sum}_{\mathsf {i}\in \text {N}}(payment_\mathsf {i}) =0\end{aligned}$$

The formula $wbb$ is defined similarly, with $\ge$ instead of $=$. Remind we consider that each stage in $\text {M}$ represents a direct mechanism. The ST-model $\text {M}$ is SBB (resp. WBB) if that is the case for all outcome states of all paths in $\text {M}$, that is, if $\text {M}\models \bigcirc sbb$ (resp. $\text {M}\models \bigcirc wbb$).

Similarly, we could represent conditions for the balance of trades. Balance of supply-demand requires the cumulative of trades for each good to be exactly zero [37]. Mechanisms with free disposal allow trades to sell more items than are purchased [54], that is, the cumulative of trades for each good must be at most zero.

4.1.2 Strategyproof mechanisms

A mechanism is strategyproof (SP), or incentive compatible, if each agent $\mathsf {i}$ prefers reporting her real preference $\vartheta _\mathsf {i}$ than reporting any other preference $\vartheta _\mathsf {i}'$, since $\vartheta _\mathsf {i}$ gives her at least the same utility [52].

Definition 11

A direct mechanism $(\mathsf {s}, \varvec{\mathsf {p}})$ is strategyproof if for every agent $\mathsf {i}\in \text {N}$, every preference profile $\varvec{\vartheta }$ and every $\vartheta _\mathsf {i}' \in V_\mathsf {i}$,

$$\begin{aligned}\vartheta _\mathsf {i}(\mathsf {s}(\varvec{\vartheta })) - \mathsf {p}_\mathsf {i}(\varvec{\vartheta }) \ge \vartheta _\mathsf {i}(\mathsf {s}(\vartheta _\mathsf {i}', \vartheta _{-\mathsf {i}})) - \mathsf {p}_\mathsf {i}(\vartheta _\mathsf {i}', \vartheta _{-\mathsf {i}}) \end{aligned}$$

Now we reformulate this condition in terms of states from an ST-model. Let $V_\mathsf {i}$ denote the preference space for each agent $\mathsf {i}$.

Given the ST-model $\text {M}$, a path $\delta$ in $\text {M}$ and a stage $t\ge 0$ in $\delta$, such that $\text {L}(\delta [t], \mathsf {i}) \approx _\mathsf {i}V_\mathsf {i}$ for each $\mathsf {i}$. For any preference profile $\varvec{\vartheta }$, let $\delta _{\varvec{\vartheta }}$ denote a path such that $\delta [0,t] = \delta _{\varvec{\vartheta }}[0,t]$ and $\theta (\delta _{\varvec{\vartheta }}, t) = \varvec{\upbeta _\vartheta }$ (i.e., $\text {M}, \delta _{\varvec{\vartheta }}, t\models does(\varvec{\upbeta _\vartheta })$). In other words, $\delta _{\varvec{\vartheta }}$ is a path with the same prefix as $\delta$, but one in which agents report the preferences $\varvec{\vartheta }$ in $\delta _{\varvec{\vartheta }}[t]$ instead of the actions they perform in $\delta [t]$.

We say that $\delta [t]$ is strategyproof if for every $\mathsf {i}\in \text {N}$, every preference profile $\varvec{\vartheta }$ and every $\vartheta _\mathsf {i}' \in V_\mathsf {i}$, we have that, for some $x\in \text {I}$,

$$\begin{aligned}\text {M},\delta _{\varvec{\vartheta }}, t\models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {i}) = x\end{aligned}$$

and

$$\begin{aligned}\text {M},\delta _{(\vartheta _\mathsf {i}', \vartheta _{-\mathsf {i}})}, t\models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {i}) \le x\end{aligned}$$

$\text {M}$ is strategyproof if each stage $t\ge 0$ of each path $\delta$ in $\text {M}$ is strategyproof.

4.1.3 Efficient mechanisms

A mechanism is efficient (EF) if the social choice function maximizes the (utilitarian) social welfare [54], i.e., the cumulative preference among the agents.

Definition 12

A direct mechanism $(\mathsf {s}, \varvec{\mathsf {p}})$ is efficient if for every preference profile $\varvec{\vartheta }$,

$$\begin{aligned}\sum _{\mathsf {i}\in \text {N}} \vartheta _\mathsf {i}(\mathsf {s}(\varvec{\vartheta })) = \max _{\varvec{\uplambda }\in \Uplambda } \sum _{\mathsf {i}\in \text {N}} \vartheta _{\mathsf {i}}(\varvec{\uplambda }) \end{aligned}$$

Let us express this condition in terms of an ST-model $\text {M}$. The following formula determines whether the current trade maximizes the social welfare:

$$\begin{aligned}e\textit{f}(\varvec{\upbeta }) =_{\text {def}}\left( \text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{(trade_{j})}_{j\in \text {G}})) = \max _{\varvec{\uplambda }\in \Uplambda }(\text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda })))\right) \end{aligned}$$

We say $\text {M}$ is EF if, after performing a joint action, the trade in the outcome state maximizes agents’ preferences, that is $\text {M}\models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$, for every $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$.

4.1.4 Individually rational mechanisms

A mechanism is (ex-post) individually rational (IR), if agents always get non-negative utility [52]. Given a reported preference, in an IR mechanism, the agent’s utility when participating is at least as good as if she did not participate (assuming the utility of non-participation is zero). Individual rationality is also known as voluntary participation since it expresses the idea that agents are not forced to participate in the mechanism [54].

Definition 13

A direct mechanism $(\mathsf {s}, \varvec{\mathsf {p}})$ is individually rational if for every agent $\mathsf {i}\in \text {N}$, every $\varvec{\vartheta } \in \prod _{\mathsf {r}\in \text {N}} V_\mathsf {r}$,

$$\begin{aligned}\vartheta _\mathsf {i}(\mathsf {s}(\varvec{\vartheta })) - \mathsf {p}(\varvec{\vartheta }) \ge 0\end{aligned}$$

We use the following ADL $[\mathcal {F}_{\mathcal {B}}]$-formula to denote whether an state is IR:

$$\begin{aligned}ir(\varvec{\upbeta }) =_{\text {def}}\bigwedge _{\mathsf {i}\in \text {N}} \text {sub}(v_{\mathsf {i}}(\upbeta _\mathsf {i}, \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {i})\ge 0\end{aligned}$$

The ST-model $\text {M}$ is IR if performing a joint action leads to an individually rational state, that is, $\text {M}\models does(\varvec{\upbeta }) \rightarrow \bigcirc ir(\varvec{\upbeta })$, for every $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$.

The properties described in this section are classical in mechanism design, since they describe desirable features of the outcome. The objective of a mechanism may include a combination of different properties. However, well-known impossibility results restrict the feasible combination of such properties: no mechanism can be efficient, strongly budget-balanced and individual-rational [49] and no mechanism can be efficient, incentive compatible and strongly budget-balanced [23].

In this paper, we verify ST-models by considering that each stage is a direct mechanism, that is, an iterative protocol is treated as a sequence of (independent) direct mechanisms. The revelation principle [52] states that any indirect mechanism that implements a function in dominant strategies can be converted into a strategyproof direct mechanism. For this reason, considering direct mechanisms is of first interest.

If we want to verify an ST-model $\text {M}$ as an (unique) indirect mechanism, we need to evaluate properties considering the final outcome, that is, on the terminal states of each path. The classical approach in mechanism design requires properties to hold in strategic equilibrium rather than for all possible outcomes. As ADL $[\mathcal {F}_{\mathcal {B}}]$ does not involve quantification over strategies, we need meta-reasoning to capture the strategic equilibrium for a given solution concept (such as Nash or dominant strategy equilibrium). The reader may refer to [52] for a discussion on the problem of finding strategic equilibria.

In the next subsection, we will focus on properties that ensure well-formed descriptions in $\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$. This properties are not related to the mechanism outcome but require protocols to be playable and eventually end.

4.2 Characterizing well-formed protocols

Love et al. [40] introduced constraints for games used in General Game Playing. This constraints constitute desirable features of games described in GDL by ensuring their descriptions to be meaningful (or well-formed), in the sense that games are playable, eventually terminate and are weakly winnable by any player.

We rephrase the constraints for termination and playability in terms of ST-models. First, termination refers to whether each path from an ST-model reaches a terminal state.

Definition 14

An ST-model $\text {M}$ terminates if each path $\delta$ in $\text {M}$ is complete, that is, $\delta [t] \in \text {T}$, for some $t>0$.

Playability means there is a legal action for each agent to take in each moment of the auction.

Definition 15

An ST-model $\text {M}$ is playable if $\text {L}(\text {w}, \mathsf {i}) \ne \emptyset$ for each reachable state $\text {w}\in \text {W}$ and agent $\mathsf {i}\in \text {N}$.

Weak winnability means that, for each agent, there is a sequence of joint actions that leads to a terminal state where the goal value is maximal. In the logical formulations of GDL, weak winnability means that every player has a chance to win [60, 75], that is, there exists a path to a winning state. In ADL $[\mathcal {F}_{\mathcal {B}}]$, weak winnability follows from our assumption that each stage represents a direct mechanism. Since we understand the agent’s preferences as represented by legal actions, there exists a joint action in each stage leading to a state that maximizes her utility among the possible outcomes. Hence, we do not focus on weak winnability for determining whether a protocol is well-formed.

A well-formed protocol is a set of rules in ADL $[\mathcal {F}_{\mathcal {B}}]$ whose model is an ST-model that satisfies both termination and playability.

Definition 16

Given an ST-Model $\text {M}$ and a finite set of ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae $\Sigma \subset \mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$, $\Sigma$ is a well-formed protocol over $\text {M}$ if $\text {M}$ is a model of $\Sigma$, $\text {M}$ terminates and it is playable.

It is possible to have different descriptions that are well-formed with respect to the same model (e.g., due to redundancy). In fact, a given auction description may also be sound in respect to several models. Investigating minimal descriptions is an interesting non trivial open question. A potential path is to characterize the minimum equivalent of an original ST-model, that is, the canonical model. This problem was explored for GDL [27], where they use the notion of bisimulation equivalence between ST-models. In a recent paper, Zhang [76] investigates the equivalence of two GDL-descriptions when they describe games behaviourally the same.

Similar to ADL $[\mathcal {F}_{\mathcal {B}}]$, the semantics of GDL is based on fixed paths. Thus, the constraints for well-formed descriptions cannot be encoded through formulae using the standard formulation of GDL. Zhang [75] proposes a GDL-based modal logic to enable reasoning over game descriptions, with which one can express conditions such as playability, termination and winnability. However, the work does not investigate the complexity of verifying formulae in this modal logic. Ruan et al. [60] use ATL [1] to reason about GDL-specified games. They prove that the problem of interpreting ATL formulae over propositional GDL descriptions is EXPTIME-complete and show how to use ATL for the verification of well-formedness conditions, which might or might not hold on various games. Deciding whether a GDL description [40] is well-formed is undecidable in general, since deciding whether a description leads to games that always terminates would solve the halting problem for a Turing machine [61].

$\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$ is useful for representing the rules of an auction as well as for verifying a number of properties. As we discussed above, we can encode different properties of direct mechanisms as $\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$-formulae (e.g., individual rationality and budget balance). Although we cannot represent strategyproofness and the constraints for well-formed descriptions entirely as $\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$-formulae, we are still able to infer them by meta-reasoning over the model specification.

Other logical languages are suitable for encoding properties. Termination and playability, for instance, can be written as ATL-formulae [1]. As SL [14] includes quantification over strategies, it allows the evaluation of games in strategic equilibria. Therefore, it can be used to encode properties for indirect mechanisms as logical formulae, as proposed in [42]. However, the expressivity of such languages brings a computational cost. The model-checking problem for ATL* with perfect information is in PSPACE in the memoryless case and deterministic double exponential time with perfect recall [63]. As for SL, the model-checking is Non Elementary with respect to the size of the specification. More specifically, it is k-EXPSPACE-hard in the alternation number k of quantifications in the specification [48]. As we shall see in Sect. 7, the model-checking for $\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$ is in PTIME in the size of the formula. For this reason, we believe $\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$ provides a reasonable cost-benefit for expressing and evaluating general auctions. As a drawback for ATL, SL and ADL $[\mathcal {F}_{\mathcal {B}}]$, representing auctions as concurrent game structures or state-transition models may require exponential size.

In the next sections, we illustrate the use of ADL $[\mathcal {F}_{\mathcal {B}}]$ for specification of different although representative types of auctions: a simultaneous ascending auction, a Vickrey–Clarke–Groves mechanism and an iterative combinatorial exchange.

5 Representing a simultaneous ascending auction

Let us now consider the simultaneous ascending auction (SAA), which 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 participants simultaneously bid for any number of goods they want. According to Cramton [17]:

“The simultaneous ascending auction (and its variants) will remain the best method for auctioning many related items in a wide range of circumstances, even settings where some of the goods are complements for some bidders.”

To represent a SAA with $\mathsf {n}$ types of goods and $\mathsf {m}$ agents, we first describe the auction signature, written $\mathcal {S}_{sa} = (\text {N}, \text {G}, \mathcal {B}, {\Upphi }, \text {Y}, \text {I}, \mathcal {F}_{\mathcal {B}})$, where $\text {N}= \{1, \ldots , \mathsf {m}\}$, $\text {G}= \{1, \ldots , \mathsf {n}\}$, ${\Upphi }= \{sold_j, bid_{\mathsf {i},j} :$ $j\in \text {G}$ & $\mathsf {i}\in \text {N}\}$, $\text {Y}= \{price, price_j,$ $trade_{\mathsf {i},j},$ $payment_{i}: j\in \text {G}$ & $\mathsf {i}\in \text {N}\}$ and $\text {I}\subset \mathbb {N}$. The propositions $sold_j$ and $bid_{\mathsf {i},j}$ represent whether the good $j$ was sold and whether $\mathsf {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. Agents may specify the value they are willing to pay for each good in a given state. The action set is defined as follows: $\mathcal {B}= \{(p_1, \ldots , p_\mathsf {m}): p_j\in \text {I}_{\succeq 0}, 1 \le j \le \mathsf {m}\}$, where $p_j$ denotes the price for good $j$.

$\mathcal {F}_{\mathcal {B}}$ includes the functions previously introduced (e.g., $\text {sum}(z_1,z_2)$, $\max (z_1, z_2)$). It also contains the function $v_\mathsf {i}: \mathcal {B}\times \text {I}^{\mathsf {n}\mathsf {m}} \rightarrow \text {I}$, for each agent $\mathsf {i}\in \text {N}$. This function is defined as follows:

$$\begin{aligned}v_\mathsf {i}((p_1, \ldots , p_\mathsf {m}), \varvec{\uplambda }) = \sum _{j\in \text {G}} \uplambda _{\mathsf {i}, j} \cdot p_j\end{aligned}$$

for a trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$ and a bid $(p_1, \ldots , p_\mathsf {m}) \in \mathcal {B}$.

Each instance of a SAA is specific and defined with respect to $\mathcal {B}$, $\text {I}$ and the constant values $\mathsf {inc}, \mathsf {m}, \mathsf {n}\in \text {I}_{\succ 0}$ and $\mathsf {start} \in \text {I}_{\succeq 0}$, representing the quantity of agents and types of goods, the bid increment, and the starting price, respectively. Then, the rules of an SAA are formulated by ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae as shown in Fig. 1.

Fig. 1

Simultaneous 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 it is traded to 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 in the next state if she is currently the only active bidder for this item, otherwise there is no trade (Rules 4–5). For each good, an agent can either bid the value 0, an increment on 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, and (iii) the active bidders for each good are updated with respect to their bids (Rules 7–9). The payment for an agent is the cumulative value of the selling price for her traded goods (Rule 10). Let $\Sigma _{sa}$ be the set of Rules 1–10.

5.1 Representing as a model

Next, we address the model representation of SAA. Let $\mathscr {M}_{sa}$ be the set of ST-models $\text {M}_{sa}$ defined for any constant values $\mathsf {start} \in \text {I}_{\succeq 0}$ and $\mathsf {inc}, \mathsf {n}, \mathsf {m}\in \text {I}_{\succ 0}$. Each $\text {M}_{sa}$ is defined as follows:

• $\text {W}= \{\langle \varvec{(b_{j})}_{j\in \text {G}}, \varvec{(\uplambda _{j})}_{j\in \text {G}}, p, (p_j)_{j\in \text {G}} \rangle : b_{\mathsf {i},j}, \uplambda _{\mathsf {i}, j} \in \{0,1\}$ & $p, p_j\in \text {I}_{\succeq 0}$ & $\mathsf {i}\in \text {N}$ & $j\in \text {G}\}$, where $b_{\mathsf {i},j}$ denotes whether agent $\mathsf {i}$ is bidding for good $j$, $\uplambda _{\mathsf {i}, j}$ specifies the number of goods with type $j$ traded for agent $\mathsf {i}$, p denotes the current price and $p_j$ represents the selling price for $j$;

• $\bar{\text {w}}= \langle 0,\ldots , 0, 0,\ldots , 0, \mathsf {start}, \mathsf {start}, \ldots , \mathsf {start} \rangle$, in the initial state, there is no trade or active agent and the prices are $\mathsf {start}$;

• $\text {T}= \{\text {w}: \text {w}= \langle \varvec{(b_{j})}_{j\in \text {G}}, \varvec{(\uplambda _{j})}_{j\in \text {G}}$, $p, (p_j)_{j\in \text {G}} \rangle \in \text {W}{\setminus } \{\bar{\text {w}}\}$ & for all $j\in \text {G}$, either (i) $\uplambda _{\mathsf {i}, j} =1$ for some $\mathsf {i}\in \text {N}$ or (ii) $bid_{\mathsf {i},j} = 0$, for all $\mathsf {i}\in \text {N}\}$, the terminal states are the ones where every good was sold or there is no bidder interested on purchasing it;

• $\text {L}= \{(\text {w}, \mathsf {i}, (pr_j)_{j\in \text {G}}):$ $\mathsf {i}\in \text {N}$ & $\text {w}= \langle \varvec{(b_{j})}_{j\in \text {G}}, \varvec{(\uplambda _{j})}_{j\in \text {G}}, p, (p_j)_{j\in \text {G}} \rangle \in \text {W}$ & for all $j\in \text {G}$, and all $0\le pr_j< z_{\text {max}}-\mathsf {inc}$ such that either (i) $pr_j = 0$ & $\uplambda _{\mathsf {i}, j}=0$ or (ii) $pr_j =p+\mathsf {inc}$ & $\uplambda _{\mathsf {r}, j} \ne 1$, for all $\mathsf {r}\in \text {N}$ or (iii) $pr_j = p_j$ & $\uplambda _{\mathsf {i}, j} =1\}$, that is, agents can choose to raise their bid or to give up of unsold goods, if an agent bought a good, she must keep her bid for it;

• For every $\text {w}= \langle \varvec{(b_{j})}_{j\in \text {G}},\varvec{(\uplambda _{j})}_{j\in \text {G}}, p,(p_j)_{j\in \text {G}}\rangle$ in $\text {W}$ and all $\varvec{d} \in \mathcal {B}^\mathsf {m}$, $\text {U}$ is defined as follows: if $\text {w}\in \text {T}$ then $\text {U}(\text {w},\varvec{d}) = \text {w}$. Otherwise, $\text {U}(\text {w}, \varvec{d}) = \langle \varvec{(b'_{j})}_{j\in \text {G}}, \varvec{(\uplambda '_{j})}_{j\in \text {G}}$, $p', \varvec{(\uplambda _{j})}_{j\in \text {G}} \rangle$, where for every $\mathsf {i}\in \text {N}$ and $j\in \text {G}$ each component is updated as follows,

  • (i) $b_{\mathsf {i},j}' = 1$ iff $d_i \ne 0$; and $b_{\mathsf {i},j}' = 0$ otherwise;

  • (ii) $\uplambda _{\mathsf {i}, j}' = 1$ iff $b_{\mathsf {i},j}' = 1$ and for all $\mathsf {r}\in \text {N}{\setminus }\{i\}, b_{\mathsf {i},j}' \ne 1$; and $\uplambda _{\mathsf {i}, j}' = 0$ otherwise;

  • (iii) $p' = p+\mathsf {inc}$;

  • (iv) $p_j' = p_j+\mathsf {inc}$ iff $\uplambda _{r,j}' = 0$ for all $\mathsf {r}\in \text {N}$; and $p_j' = p_j$ otherwise.

• For each $\text {w}= \langle \varvec{(b_{j})}_{j\in \text {G}},\varvec{(\uplambda _{j})}_{j\in \text {G}}, p,(p_j)_{j\in \text {G}}\rangle$ in $\text {W}$, $\mathsf {i}\in \text {N}$ and $j\in \text {G}$,

  • (i) $\uppi _{\text {Y}}(\text {w}, trade_{\mathsf {i},j}) = \uplambda _{\mathsf {i}, j}$;

  • (ii) $\uppi _{\text {Y}}(\text {w}, price) = p$;

  • (iii) $\uppi _{\text {Y}}(\text {w}, price_{j}) = p_j$;

  • (iv) $\uppi _{\text {Y}}(\text {w}, payment_{\mathsf {i}}) = \sum _{j\in \text {G}} p_j\cdot \uplambda _{\mathsf {i}, j}$

• For each $\text {w}\in \text {W}$, $\uppi _{{\Upphi }}(\text {w}) = \{sold_j : \uplambda _{\mathsf {i}, j} =1$ & $j\in \text {G}$ & $\mathsf {i}\in \text {N}\} \cup \{ bid_{\mathsf {i},j} : b_{\mathsf {i},j} =1$ & $j\in \text {G}$ & $\mathsf {i}\in \text {N}\}$.

Hereafter, we assume an instance of $\text {M}_{sa}\in \mathscr {M}_{sa}$ and $\Sigma _{sa}$ for some $\mathsf {start} \in \text {I}_{\succeq 0}$ and $\mathsf {inc}, \mathsf {n}, \mathsf {m}\in \text {I}_{\succ 0}$.

Example 1

Let $\text {M}_{sa}\in \mathscr {M}_{sa}$, such that $\mathsf {start} = 1$ and $\mathsf {inc} = 1$. We assume there are two agents in $\text {N}$, denoted by $\mathsf {i}$ and $\mathsf {s}$, and two types of goods in $\text {G}$, denoted by $\mathsf {a}$ and $\mathsf {b}$. Figure 2 illustrates a path in $\text {M}_{sa}$, showing the value of the numerical variables and the propositions that hold in each state. For convenience, we omit the numerical variables when their value is 0. In state $\text {w}_0$, agents $\mathsf {r}$ and $\mathsf {s}$ bid for good $\mathsf {a}$, but only agent $\mathsf {r}$ bids for good $\mathsf {b}$. In state $\text {w}_1$, since $\mathsf {r}$ is the only bidder for $\mathsf {b}$, it is sold to her. Agent $\mathsf {r}$ cannot change her bid for $\mathsf {b}$ and $\mathsf {s}$ can no longer bid for it. In $\text {w}_1$, only agent $\mathsf {s}$ accepts to increase her bid for $\mathsf {a}$. In state $\text {w}_2$, $\mathsf {a}$ is sold to $\mathsf {s}$. Since all the goods were sold, this state is terminal.

Fig. 2

A Path in $\text {M}_{sa}$, with 2 bidders and 2 goods

5.2 Evaluating the protocol

Let us now evaluate the protocol. First, we show that $\Sigma _{sa}$ is a sound representation of $\text {M}_{sa}$.

Lemma 1

$\text {M}_{sa}$ is an ST-model and it is a model of $\Sigma _{sa}$.

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 to zero. When a good is sold, it will still be sold in the next state.

Proposition 2

For each $j\in \text {G}$ and each $\mathsf {i}, \mathsf {r}\in \text {N}$ such that $\mathsf {i}\ne \mathsf {r}$,

• 1. $\text {M}_{sa}\models trade_{\mathsf {i},j} = 0 \vee trade_{\mathsf {r},j} = 0$

• 2. $\text {M}_{sa}\models sold_j\rightarrow \bigcirc sold_j$

• 3. $\text {M}_{sa}\models \lnot sold_j\rightarrow price = price_j$

Each path in $\text {M}_{sa}$ reaches a terminal state, and thus the protocol satisfies the termination condition. Furthermore, $\text {M}_{sa}$ satisfies playability, that is, there is always a legal action for each agent to take. Thus, $\Sigma _{sa}$ is well-formed over $\text {M}_{sa}$.

Theorem 1

$\Sigma _{sa}$ is a well-formed protocol over the ST-model $\text {M}_{sa}$.

Proof

Since $\text {M}_{sa}$ is a model of $\Sigma _{sa}$ (see Lemma 1), we have to show that for each path $\updelta$ in $\text {M}_{sa}$ and each agent $\mathsf {i}\in \text {N}$,

• 1. $\updelta$ is a complete path;

• 2. $\text {M}_{sa}\models \bigvee _{a \in \mathcal {B}}legal_\mathsf {i}(a)$.

Let us start by verifying Statement 1. Remind $\mathsf {start} \in \text {I}_{\succeq 0}$ and $\mathsf {inc}\in \text {I}_{\succ 0}$. Let $\updelta$ be a path in $\text {M}_{sa}$. In $\updelta [0]$, $\uppi _{\text {Y}}(\updelta [0], price) = \mathsf {start}$. By the update function, for any stage $t$, if $\updelta [t]\not \in \text {T}$, then $\uppi _{\text {Y}}(\updelta [t+1], price) = \uppi _{\text {Y}}(\updelta [t], price)+\mathsf {inc}$.

For the sake of contradiction, let us assume $\updelta$ is not complete. Let $\mathsf {i}\in \text {N}$ be an agent. By the definition of $\text {L}$, $(p_1, \ldots , p_\mathsf {m}) \in \text {L}(\updelta [t], \mathsf {i})$, for all $0 \le p_j< z_{\text {max}}-\mathsf {inc}$ and $j\in \text {G}$, such that either (i) $p_j= 0$ & $\uppi _{\text {Y}}(\updelta [t]$, $trade_{\mathsf {i},j}) = 0$, or (ii) $p_j= price+\mathsf {inc}$ & $\uppi _{\text {Y}}(\updelta [t], trade_{r,j}) = 0$ for all $r\in \text {N}$, or (iii) $p_j= price_j$ & $\uppi _{\text {Y}}(\updelta [t], trade_{r,j}) = 0$. Since $\uppi _{\text {Y}}(\updelta [t+1], price)>\uppi _{\text {Y}}(\updelta [t], price)$, there will be a stage $e\ge 0$ in $\updelta$, where the condition (ii) will not be true for any $0\le p_j< z_{\text {max}}-\mathsf {inc}$. Thus, for each good $j$, it will be the case that $\mathsf {i}$ bids 0 for it or the good was assigned to her (i.e., $\uppi _{\text {Y}}(\updelta [e], trade_{\mathsf {i},j})= 1$). From Rules 3 and 9 in $\Sigma _{sa}$, it follows that $\updelta [e+1]\in \text {T}$. Thus, $\updelta$ is a complete path, which is a contradiction.

We now consider Statement 2. Given a path $\updelta$ in $\text {M}_{sa}$ and a stage $t$ in $\updelta$, we show that there is a legal action for agent $\mathsf {i}$ in $\updelta [t]$. For each $j\in \text {G}$, let $p_j= 0$ if $\uppi _{\text {Y}}(\updelta [t], trade_{\mathsf {i},j}) = 1$. Otherwise, let $p_j= \uppi _{\text {Y}}(\updelta [t], price_j)$. By $\text {L}$ definition, we have $(p_1, \ldots ,p_\mathsf {m}) \in \text {L}(\updelta [t], \mathsf {i})$. Thus, $\text {M}_{sa}, \updelta , t\models \bigvee _{a \in \mathcal {B}}legal_\mathsf {i}(a)$.

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

Proposition 3

$\text {M}_{sa}\models \bigcirc wbb$ and $\text {M}_{sa}\not \models \bigcirc sbb$

The simultaneous ascending auction is only efficient on states preceding the terminal one.

Proposition 4

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$,

• 1. $\text {M}_{sa} \not \models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$

• 2. $\text {M}_{sa} \models does(\varvec{\upbeta }) \rightarrow \bigcirc (terminal\rightarrow e\textit{f}(\varvec{\upbeta }))$

The auction described by $\text {M}_{sa}$ is individually rational, since agents pay at most their bids.

Theorem 2

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, $\text {M}_{sa} \models does(\varvec{\upbeta }) \rightarrow \bigcirc ir(\varvec{\upbeta })$

Proof

Given a path $\updelta$ in $\text {M}_{sa}$ and a stage $t$, assume $\text {M}_{sa}, \updelta , t\models does(\varvec{\upbeta })$ for some $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$. We consider first the case where $\updelta [t] \not \in \text {T}$. Let $\mathsf {i}\in \text {N}$ be an agent and $(p_1, \dots , p_\mathsf {m})$ denote the bid of $\mathsf {i}$ in the joint action $\varvec{\upbeta }$. Let us consider the good $j\in \text {G}$. We denote by $pr_j= \uppi _{\text {Y}}(\delta [t+1], price_{ j})$ the price of good $j$ in $\delta [t+1]$ and by $\varvec{\uplambda }= (\uppi _{\text {Y}}(\delta [t+1], trade_{\mathsf {s}, j'}))_{j' \in \text {G}, \mathsf {s}\in \text {N}}$ the trade in $\delta [t+1]$. Recall function $v_\mathsf {i}((p_1, \dots , p_\mathsf {m}), \varvec{\uplambda }) = \sum _{j\in \text {G}} \uplambda _{\mathsf {i}, j} \cdot p_j$. Similarly, by Rule 10, we have that the payment for agent $\mathsf {i}$ in $\delta [t+1]$ is $\uppi _{\text {Y}}(\delta [t+1], payment_\mathsf {i}) = \sum _{j\in \text {G}} pr_j\cdot \uplambda _{\mathsf {i}, j}$.

We have $\theta _\mathsf {i}(\updelta , t) = (p_1, \dots , p_\mathsf {m})$. Notice $\mathsf {inc}, p_j\in \text {I}_{\succeq 0}$ by the definition of $\mathcal {S}_{sa}$. According with the action legality (Rule 6), the value of $p_j$ can be either zero, the price of $j$ in $\delta [t]$ or the current price incremented by $\mathsf {inc}$. For each of the three cases, we show that the part of $\mathsf {i}$’s payment corresponding to $j$ is equal to the part of $v_\mathsf {i}((p_1, \dots , p_\mathsf {m}), \varvec{\uplambda })$ corresponding to $j$:

• If $p_j= 0$, agent $\mathsf {i}$ chosen to not bid for good $j$. By Rules 5 and 9, $\text {M}_{sa}, \delta , t+1 \models \lnot bid_{\mathsf {i}, j} \wedge trade_{\mathsf {i}, j}=0$. Thus, we have $\uplambda _{\mathsf {i}, j} \cdot p_j= pr_j\cdot \uplambda _{\mathsf {i}, j} = 0$.

• If $p_j= \uppi _{\text {Y}}(\delta [t],price_j)$, by the definition of $\text {L}$, it must be the case that the good was already sold to agent $\mathsf {i}$, that is $\text {M}_{sa}, \delta , t\models trade_{\mathsf {i}, j} = 1 \wedge sold_j$. Since good $j$ is sold, Rule 6 ensure other agents can only bid the value 0 for $j$, and thus, $\text {M}_{sa}, \delta , t+1 \models \bigwedge _{r\in \text {N}{\setminus }\{\mathsf {i}\} } \lnot bid_{r, j}$. By Rules 4 and 9, we have $\text {M}_{sa}, \delta , t+1\models bid_{\mathsf {i}, j} \wedge trade_{\mathsf {i}, j}=1$. Since good $j$ is sold, its price in $\delta [t]$ is the same as in $\delta [t]$ (Rule 8), that is $\text {M}_{sa}, \delta , t\models price_j= p_j$. Thus, we have $\uplambda _{\mathsf {i}, j} \cdot p_j= pr_j\cdot \uplambda _{\mathsf {i}, j} = pr_j$.

• Let $prevprice = \uppi _{\text {Y}}(\delta [t], price)$. If $p_j= prevprice + \mathsf {inc}$, then $\text {M}_{sa}, \delta , t+1\models bid_{\mathsf {i}, j}$. From the legality definition, it should be the case that $j$ is not sold, that is $\text {M}_{sa}, \delta , t\models \lnot sold_j\wedge price_j= \text {sum}(prevprice_j, \mathsf {inc})$. From Statement 3 of Proposition 2, we have $\text {M}_{sa}, \delta , t\models price = price_j$. The value of $trade_{\mathsf {i}, j}$ depends on the actions of other agents in $\delta [t]$. From Rules 5 and 4, we have $\text {M}_{sa}, \delta , t+1\models trade_{\mathsf {i}, j} = 0 \vee trade_{\mathsf {i}, j} = 1$. In the first case, $\uplambda _{\mathsf {i}, j} \cdot p_j= pr_j\cdot \uplambda _{\mathsf {i}, j} = 0$. Otherwise, the trade has the value 1 and $\uplambda _{\mathsf {i}, j} \cdot p_j= pr_j\cdot \uplambda _{\mathsf {i}, j} = pr_j$, since $p_j= pr_j= prevprice+\mathsf {inc}$.

It follows that $\text {M}_{sa}, \delta , t+1 \models v_{\mathsf {r}}(\upbeta , \varvec{(trade_{j})}_{j\in \text {G}}) = payment_\mathsf {r}$ and $\text {M}_{sa}, \delta , t+1 \models \text {sub}(v_{\mathsf {r}}(\upbeta , \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {r})\ge 0$. Thus, $\text {M}_{sa}, \delta , t\models \bigcirc ir(\varvec{\upbeta })$.

If $\updelta [t] \in \text {T}$, the loop in the path definition ensures $\text {M}_{sa}, \delta , t\models \bigcirc ir(\varvec{\upbeta })$ if and only if $\text {M}_{sa}, \delta , t\models ir(\varvec{\upbeta })$.

Under the assumption that each stage in $\text {M}_{sa}$ is a (direct) mechanism for which the legality set represents the agents’ preference spaces, the $\text {M}_{sa}$ is strategyproof. As it is only legal to accept or decline to raise the current price for unsold goods (represented by bidding the value 0 or $price+\mathsf {inc}$), there is no utility improvement if the agent accepts when she would prefer to decline (and vice-versa). When a good is sold for an agent, there is only one value that is legal to bid for the good bought, and thus the agent cannot strategize.

Proposition 5

$\text {M}_{sa}$ is strategyproof.

We conclude the section by discussing variants of non-combinatorial auctions. When the number of good types is one (that is, $|\text {G}|=1$), $\Sigma _{sa}$ corresponds to the Japanese-English auction. For representing the standard variant of the English auction, one should define the legality rule such that agents are also allowed to bid any price above the current price. Furthermore, the price in the next state should be updated according to the highest bid in the current one. The Dutch auction is also similar to $\Sigma _{sa}$. The key difference is that in the Dutch auction the bidding value should be decreased at each round until at least one agent accepts to pay the current price. As we saw in this section, with the ADL $[\mathcal {F}_{\mathcal {B}}]$ description of a given auction, we are able to formally analyze it, both in relation to domain-specific properties, well-formedness of its protocol and from a mechanism design perspective.

6 Representing combinatorial exchange

We now consider two protocols for combinatorial exchange: a one-shot protocol and a multi-stage variant. We consider the setting with multiple goods and multiple copies of each good. Agents hold an initial allocation of goods and can trade items with each other. Remind a trade denotes the number of goods being exchanged among the agents in a state. With allocation we refer to the number of goods the agents initially have.

Both protocols use the Tree-Based Bidding Language (TBBL) for defining its action set. TBBL [41, 53] 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. TBBL is general enough to represent any kind of utility function (full expressivity), like OR-like bidding languages [9]. It is even more expressive in the sense that it is able to mix preferences for buying and selling bundles in the same framework. In relation to which kind of utility functions this framework is able to represent concisely, [13] compares TBBL with XOR and OR* bidding languages with this respect, and shows that TBBL is more compact, in the sense that there are valuation functions that admit an exponentially larger representation in these latter languages than in TBBL.

6.1 Tree-based bidding language

The bidding language we present in this section, denoted $\mathcal {L}_{\textsf {{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 $\text {I}$.

Definition 17

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

$$\begin{aligned} \upbeta ::= \langle z, j, z \rangle \mid \text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta }, z) \end{aligned}$$

where $\bar{\upbeta }::= \bar{\upbeta }, \upbeta \mid \upbeta$ is a nonempty bid list, $j\in \text {G}$, $z\in \text {I}$, $\text {y}\le \text {x}$ and $\text {y},\text {x}\in \text {I}_{\succeq 0}$.

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

For instance, in Fig. 3, agent $\mathsf {i}$ reports her willingness to buy 1 unit of $\mathsf {a}$ paying 2€ or 2 units of $\mathsf {a}$ for 5€ or to sell 1 unit of $\mathsf {b}$ receiving 2€. Agent $\mathsf {s}$ 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 the condition (ii) has an additional value of 1.

Fig. 3

Examples of tree-bids $\upbeta _{\mathsf {i}}$ and $\upbeta _\mathsf {s}$ reported by agents $\mathsf {i}$ and $\mathsf {s}$, resp

Hereafter, we introduce some extra notations to characterize solutions and winners. Let $\upbeta _\mathsf {i}\in \mathcal {L}_{\textsf {{TBBL}}}$ be a bid-tree from bidder $\mathsf {i}$, the set $\text {Node}(\upbeta _\mathsf {i})$ denotes all nodes in the tree $\upbeta _\mathsf {i}$, that is, all its inner bids, including $\upbeta _\mathsf {i}$ itself. Formally, if $\upbeta _\mathsf {i}$ is in the form $\langle \mathsf {q}, j, \mathsf {v} \rangle$, then $\text {Node}(\upbeta _\mathsf {i}) = \{\upbeta _\mathsf {i}\}$. Otherwise, $\upbeta _\mathsf {i}$ is in the form $\text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta },\mathsf {v}')$ and $\text {Node}(\upbeta _\mathsf {i}) = \{\upbeta _\mathsf {i}\}\cup \text {Node}(\bar{\upbeta }_1)\cup \cdots \cup \text {Node}(\bar{\upbeta }_{\mathsf {z}})$, where $\mathsf {z}=|\bar{\upbeta }|$ and $\bar{\upbeta }_k$ is the k-th element of $\bar{\upbeta }$.

Let $\upalpha \in \text {Node}(\upbeta _\mathsf {i})$, the set $\text {Child}(\upalpha ) \subset \text {Node}(\upbeta _\mathsf {i})$ denotes the children of node $\upalpha$. If $\upalpha$ is in the form $\text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta }, \mathsf {v})$, then $\text {Child}(\upalpha ) = \{\bar{\upbeta }_1, \ldots , \bar{\upbeta }_\mathsf {z}\}$, where $\mathsf {z}=|\bar{\upbeta }|$. Otherwise, $\text {Child}(\upalpha ) = \{\}$. The leaves of a bid-tree $\upbeta _\mathsf {i}$ are denoted by $\text {Leaf}(\upbeta _\mathsf {i}) = \{\langle \mathsf {q}, j, \mathsf {v} \rangle \in \text {Node}(\upbeta _\mathsf {i}): \mathsf {q}\in \text {I}, \mathsf {v}\in \text {I}$ & $j\in \text {G}\}$. The value specified at node $\upalpha$ is denoted by $b_\mathsf {i}(\upalpha ) \in \text {I}$. If $\upalpha$ is in the form $\langle \mathsf {q}, j, \mathsf {v} \rangle$, then $b_\mathsf {i}(\upalpha ) = \mathsf {v}$. Otherwise, $\upalpha$ is in the form $\text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta },\mathsf {v}')$ and $b_\mathsf {i}(\upalpha ) = \mathsf {v}'$. Finally, the quantity of units of the good $j$ specified at a leaf $\upalpha = \langle \mathsf {q}, j, \mathsf {v} \rangle$ is denoted by $q(\upalpha , j) = \mathsf {q}$. For any other $j' \ne j\in \text {G}$, $q(\upbeta , j') = 0$. For any node $\upalpha \not \in \text {Leaf}(\upbeta _\mathsf {i})$ and $j\in \text {G}$, $q(\upalpha , j) = 0$. If $\upalpha$ is not a leaf (i.e., $\upalpha \in \text {Node}(\upbeta _\mathsf {i}){\setminus } \text {Leaf}(\upbeta _\mathsf {i})$), then it is in the form $\text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta })$ and we denote by $\text {x}_\upbeta$ and $\text {y}_\upbeta$ the interval-choose constraints $\text {x}$ and $\text {y}$, respec.

6.1.1 Trade value and valid solutions

Given a bid-tree $\upbeta _\mathsf {i}$ from agent $\mathsf {i}$, the value of a trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {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 $\text {sat}_\mathsf {i}(\upalpha ) \in \{0,1\}$ denote whether a node $\upalpha \in \text {Node}(\upbeta _\mathsf {i})$ is satisfied and $\text {sat}_\mathsf {i}= \{\upalpha : \text {sat}_\mathsf {i}(\upalpha ) = 1,$ for all $\upalpha \in \text {Node}(\upbeta _\mathsf {i})\}$ denote the nodes satisfied in a solution.

A solution $\text {sat}_\mathsf {i}$ is valid for a tree $\upbeta _\mathsf {i}$ and trade $\uplambda _\mathsf {i}$, written $\text {sat}_\mathsf {i}\in \text {valid}(\upbeta _\mathsf {i}, \uplambda _\mathsf {i})$ if the following rules R1 and R2 hold [41]:

$$\begin{aligned}&\text {x}_\upbeta \text {sat}_\mathsf {i}(\upalpha ) \le \sum _{\upgamma \in \text {Child}(\upalpha )} \text {sat}_\mathsf {i}(\upgamma ) \le \text {y}_\upbeta \text {sat}_\mathsf {i}(\upalpha ) \\&\quad \forall \upalpha \in \text {Node}(\upbeta _\mathsf {i}){\setminus } \text {Leaf}(\upbeta _\mathsf {i}) \end{aligned}$$

(R1)

$$\begin{aligned}&\sum _{\upalpha \in \text {Leaf}(\upbeta _\mathsf {i})} q_\mathsf {i}(\upalpha , j) \text {sat}_\mathsf {i}(\upalpha ) \le \uplambda _{\mathsf {i},j}, \forall j\in \text {G}\end{aligned}$$

(R2)

Rule R1 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 trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$ for agent $\mathsf {i}$, given her bid $\upbeta _\mathsf {i}$, is defined as the solution to the following problem:

$$\begin{aligned}&v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda }) = \mathop {\max }_{\text {sat}_\mathsf {i}} \sum _{\upbeta \in \text {Node}(\upbeta _\mathsf {i})} b_\mathsf {i}(\upbeta ) \cdot \text {sat}_\mathsf {i}(\upbeta ) \\&\quad \text {s.t. rules } R1, R2 \text { hold} \end{aligned}$$

6.1.2 Winner determination

Given an auction signature, the bid-trees $\varvec{\upbeta }= (\upbeta _\mathsf {i})_{\mathsf {i}\in \text {N}}$ and an allocation $X= (x_{\mathsf {i}, j})_{j\in \text {G}, \mathsf {i}\in \text {N}}$, where $\upbeta _\mathsf {i}\in \mathcal {L}_{\textsf {{TBBL}}}$ denotes the bid from agent $\mathsf {i}\in \text {N}$ and $x_{\mathsf {i},j} \in \text {I}_{\succeq 0}$ represents how many copies of $j$ agent $\mathsf {i}$ initially holds.

Definition 18

The winner determination (WD) defines a pair $(\varvec{\uplambda }, sat)$ obtained by the solution to the following mixed-integer program [41]:

$$\begin{aligned} \text {WD}(\varvec{\upbeta }, X): \mathop {\max }_{\varvec{\uplambda }, \text {sat}} \sum _{\mathsf {i}\in \text {N}} \sum _{\upbeta \in \text {Node}(\upbeta _\mathsf {i})} b_\mathsf {i}(\upbeta ) \cdot \text {sat}_\mathsf {i}(\upbeta ) \\ \end{aligned}$$

(C1)

$$\begin{aligned} \text {s.t. } \uplambda _{\mathsf {i}, j} + x_{\mathsf {i},j} \ge 0, \forall \mathsf {i}\in \text {N}, j\in \text {G}\\ \sum _{\mathsf {i}\in \text {N}} \uplambda _{\mathsf {i},j} \le 0, \forall j\in \text {G}\\ \end{aligned}$$

(C2)

$$\begin{aligned} \text {sat}_\mathsf {i}\in \text {valid}(\upbeta _\mathsf {i}, \uplambda _\mathsf {i}), \forall \mathsf {i}\in \text {N}\\ \end{aligned}$$

(C3)

$$\begin{aligned} \text {sat}_\mathsf {i}(\upbeta ) \in \{0,1\}, \uplambda _{\mathsf {i}, j} \in \text {I}\end{aligned}$$

(C4)

where $\text {sat}= (\text {sat}_\mathsf {i})_{\mathsf {i}\in \text {N}}$. Constraint C1 ensures that the trade $\varvec{\uplambda }$ is feasible given $X$, that is, no agent sells more items then she initially hold. Constraint C2 provides free disposal and allows trades to sell more items than are purchased (but not vice-versa). Constraint C3 ensures that each trade for an agent $\mathsf {i}$ is valid given her bid-tree. Constraint C4 defines the range for trades and node satisfaction. We denote by $\text {WD}_{\varvec{\uplambda }}(\varvec{\upbeta }, X)$ a function that obtains the trade $\varvec{\uplambda }$ in the solution $\text {WD}(\varvec{\upbeta },X)= (\varvec{\uplambda }, \text {sat})$. Similarly, $\text {WD}_{\uplambda _{\mathsf {i},j}}(\varvec{\upbeta }, X)$ captures the number of units of $j$ traded by agent $\mathsf {i}$ in $\text {WD}_{\varvec{\uplambda }}(\varvec{\upbeta }, X)$.

If there are two or more solutions for $\text {WD}(\varvec{\upbeta }, X)$, the trade $\text {WD}_{\varvec{\uplambda }}(\varvec{\upbeta }, X)$ will be chosen w.r.t. some total order among the elements of $\text {I}^{\mathsf {n}\mathsf {m}}$. This tie-breaking order is omitted to avoid overloading the notation. In the examples, we assume this order is compatible with the Pareto dominance relation [67].

We denote $\text {noop}=_{\text {def}}\langle 0, j, 0 \rangle$ as the action of not bidding, for some arbitrary $j\in \text {G}$.

Lemma 2

For each agent $\mathsf {i}\in \text {N}$, each bid-tree $\upbeta \in \mathcal {L}_{\textsf {{TBBL}}}$ and each $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$, $v_\mathsf {i}(\text {noop}, \varvec{\uplambda }) = 0$.

Next, we illustrate how to represent protocols with TBBL in ADL $[\mathcal {F}_{\mathcal {B}}]$.

6.2 Vickrey–Clarke–Groves mechanism

Using TBBL to determinate the action set, let us now represent the Vickrey–Clarke–Groves (VCG) mechanism in ADL $[\mathcal {F}_{\mathcal {B}}]$. This mechanism chooses the outcome maximizing the reported preferences [36]. Each agent’s payment corresponds to the damage she causes the other players, that is, the difference in the social welfare of others with and without her participation [52]. We detail the rules specification and the semantic representation. Then, we revisit the conditions from MD and evaluate whether the protocol is well-formed.

To represent a VCG mechanism in the combinatorial exchange setting, we first describe its signature, written $\mathcal {S}_{vcg} = (\text {N},\text {G}, \mathcal {B}, {\Upphi }, \text {Y}, \text {I}, \mathcal {F}_{\mathcal {B}})$, where $\text {N}= \{1, \ldots , \mathsf {n}\}$, $\text {G}= \{1, \ldots , \mathsf {m}\}$, $\mathcal {B}\subseteq \mathcal {L}_{\textsf {{TBBL}}}$, ${\Upphi }= \{bidRound\}$, $\text {Y}= \{trade_{\mathsf {i},j}$, $payment_\mathsf {i}: \mathsf {i}\in \text {N}, j\in \text {G}\}$, and $\text {I}\subset \mathbb Z$. Finally, $\mathcal {F}_{\mathcal {B}}$ contains the functions $v_\mathsf {i}(\upbeta , \varvec{\uplambda })$, $\text {WD}_{\varvec{\uplambda }}(\varvec{\upbeta }, X)$ and $\text {WD}_{\uplambda _{\mathsf {i},j}}(\varvec{\upbeta }, X)$ described in the previous section as well as the functions denoting basic mathematical operations (e.g., $\text {sum}(z_1, z_2)$). We also assume $\mathcal {F}_{\mathcal {B}}$ contains the function $\text {WD}_{\varvec{\uplambda }}^{-\mathsf {r}}: \mathcal {B}^{\mathsf {n}} \times \text {I}^{\mathsf {n}\mathsf {m}} \rightarrow \text {I}^{\mathsf {n}\mathsf {m}}$ for any two agents $\mathsf {i}$ and $\mathsf {r}$. $\text {WD}_{\varvec{\uplambda }}^{-\mathsf {r}}$ is defined exactly like $\text {WD}_{\varvec{\uplambda }}$ except that the set $\text {N}$ in the winner determination (see Def. 18) is replaced by $\text {N}{\setminus } \{\mathsf {r}\}$ and that the resulting trade for agent $\mathsf {r}$ and each good $j$ is equal to zero.

Each instance of a VCG is specific and is defined with respect to $\mathcal {B}$, $\text {I}$ and the constant values $\mathsf {n}, \mathsf {m}\in \text {I}_{\succ 0}$ (the size of $\text {N}$ and $\text {G}$, resp.), and $\mathsf {X}= \varvec{(\mathsf {x}_{j})}_{j\in \text {G}}$, where $\mathsf {x}_{\mathsf {i},j}\in \text {I}_{\succeq 0}$, for each $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. Each constant $\mathsf {x}_{\mathsf {i},j}$ represents the number of units of $j$ initially held by agent $\mathsf {i}$. The rules of VCG are represented by ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae as shown in Fig. 4.

Fig. 4

Vickrey–Clarke–Groves mechanism represented by $\Sigma _{vcg}$

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 $\text {noop}$). Once in a terminal state, players can only do $\text {noop}$. Otherwise, they can bid any $\upbeta \in \mathcal {B}$ (Rules 3 and 4). After performing a joint bid, in the next state each agent receives a trade for each good, which is assigned by the winner determination over the initial allocation and their bids (Rule 5). After a joint bid in the initial state, the payment for agent $\mathsf {i}$ will be the difference in the others’ welfare with and without her participation (Rule 6). Finally, the proposition $bidRound$ is always false in the next state (Rule 7).

Notice we could as well represent winner determination explicitly in ADL $[\mathcal {F}_{\mathcal {B}}]$ by capturing the trade maximizing the social welfare among all trades that satisfy constraints C1–C4. For instance, constraint C1 can be written in $\mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$ as $\textit{feasible}(\varvec{(\uplambda _{j})}_{j\in \text {G}}) =_{\text {def}}\bigwedge _{\mathsf {i}\in \text {N}, j\in \text {G}} \text {sum}(\uplambda _{\mathsf {i},j}, x_{\mathsf {i}, j})\ge 0$. We illustrate VCG with an indirect representation of the winner determination for succincteness and clarity of $\Sigma _{vcg}$.

6.2.1 Representing as a model

Next, we address the model representation. Let $\mathscr {M}_{vcg}$ be the set of ST-models $\text {M}_{vcg}$ defined for any $\mathcal {B}\subseteq \mathcal {L}_{\textsf {{TBBL}}}$, $\text {I}\subset \mathbb Z$, and the constants $\mathsf {n}, \mathsf {m}\in \text {I}_{\succ 0}$ and $\mathsf {X}= \varvec{(\mathsf {x}_{j})}_{j\in \text {G}}$, where $\mathsf {x}_{\mathsf {i},j}\in \text {I}_{\succeq 0}$, for each $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. Each $\text {M}_{vcg}$ is defined as follows:

• $\text {W}= \{\langle b, \varvec{(\uplambda _{j})}_{j\in \text {G}}, \varvec{\text {p}}\rangle : b \in \{0$, $1\}$ & $\text {p}_\mathsf {i}, \uplambda _{\mathsf {i},j} \in \text {I}$ & $\mathsf {i}\in \text {N}$ & $j\in \text {G}\}$;

• $\bar{\text {w}}= \langle 1, 0, \ldots , 0, 0,\ldots , 0\rangle$;

• $\text {T}= \text {W}{\setminus } \{\bar{\text {w}}\}$;

• $\text {L}= \{(\text {w}, \mathsf {i}, \text {noop}): \mathsf {i}\in \text {N}$ & $\text {w}\in \text {T}\} \cup \{ ( \bar{\text {w}}, \mathsf {i},$ $\upbeta ) : \upbeta \in \mathcal {B}$ & $\mathsf {i}\in \text {N}\}$;

• $\text {U}$ is defined as follows: for all $\text {w}= \langle b, \varvec{(\uplambda _{j})}_{j\in \text {G}}, \varvec{\text {p}}\rangle \in \text {W}$ and for all $\varvec{d} \in \mathcal {B}^\mathsf {m}$:

  • If $\text {w}= \bar{\text {w}}$, then $\text {U}(\text {w}, \varvec{d}) = \langle 0, \varvec{(\uplambda '_{j})}_{j\in \text {G}}, \varvec{\text {p}'}\rangle \rangle$, where each component is updated as follows, for each $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. The number of units $j$ traded for agent $\mathsf {i}$ is given by the winner determination: $\uplambda _{\mathsf {i},j}' = \text {WD}_{\uplambda _{\mathsf {i},j}}(\varvec{d}, \mathsf {X} )$. The payment for $\mathsf {i}$ is the difference between the social welfare of others with and without $\mathsf {i}$’s participation:

    $$\begin{aligned}\text {p}_\mathsf {i}' = \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(d_\mathsf {r}, \text {WD}_{\varvec{\uplambda }}^{-\mathsf {i}}(\varvec{d}, \mathsf {X})) - \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(d_\mathsf {r}, \text {WD}_{\varvec{\uplambda }}(\varvec{d}, \mathsf {X})) \end{aligned}$$

  • Otherwise, $\text {U}(\text {w},\varvec{d}) = \text {w}$.

• For each $\text {w}\in \text {W}$, $\mathsf {i}\in \text {N}$ and $j\in \text {G}$, $\uppi _{\text {Y}}(\text {w}$, $trade_{\mathsf {i},j}) = \uplambda _{\mathsf {i},j}$; $\uppi _{\text {Y}}(\text {w}, payment_\mathsf {i}) = \text {p}_\mathsf {i}$; and $\uppi _{{\Upphi }}(\text {w}) = \{bidRound: b = 1\}$.

Hereafter, we assume an instance of $\text {M}_{vcg}\in \mathscr {M}_{vcg}$ and $\Sigma _{vcg}$ for some $\mathcal {B}\subseteq \mathcal {L}_{\textsf {{TBBL}}}$, $\text {I}\subset \mathbb Z$, $\mathsf {n}, \mathsf {m}\in \text {I}_{\succ 0}$ and $\mathsf {x}_{\mathsf {i},j} \in \text {I}_{\succeq 0}$, where $\mathsf {i}\in \text {N}$, $j\in \text {G}$.

Example 2

Let $\text {M}_{vcg}\in \mathscr {M}_{vcg}$ such that the sets of agents and goods are the same from Example 1 and the initial allocation is as follows: $\mathsf {x}_{\mathsf {i},\mathsf {a}} =0$, $\mathsf {x}_{\mathsf {i},\mathsf {b}} =1$, $\mathsf {x}_{\mathsf {s},\mathsf {a}} =2$ and $\mathsf {x}_{\mathsf {s},\mathsf {b}} =0$ (i.e., at the beginning of the auction, agent $\mathsf {i}$ has 1 unit of $\mathsf {b}$ and agent $\mathsf {s}$ has 2 units of $\mathsf {a}$). Figure 5 illustrates a path in $\text {M}_{vcg}$, where the agents perform the bids previously introduced in Fig. 3. In state $\text {w}_0$, all the payments and trades are zero. Their joint bid leads to state $\text {w}_1$, where the trade obtained by the winner determination is $(2, -1,-2,1)$. The tie-breaking ensures that the trade is unique. Thus, in $\text {w}_1$ agent $\mathsf {i}$ has 2 units of $\mathsf {a}$ and agent $\mathsf {s}$ has 1 unit of $\mathsf {b}$. Since $\text {w}_1$ is terminal, the agents can only bid $\text {noop}$.

Fig. 5

A Path in $\text {M}_{vcg}$, with 2 bidders and 2 goods

6.2.2 Evaluating the protocol

Let us now evaluate the protocol representing a VCG mechanism. First, Lemma 3 shows that $\text {M}_{vcg}$ is a sound representation of $\Sigma _{vcg}$.

Lemma 3

$\text {M}_{vcg}$ is an ST-model and it is a model of $\Sigma _{vcg}$.

Next, we show $\Sigma _{vcg}$ is a well-formed protocol, that is, each path in $\text {M}_{vcg}$ reaches a terminal state and there is a legal action for each agent in all reachable states.

Theorem 3

$\Sigma _{vcg}$ is a well-formed protocol over the ST-model $\text {M}_{vcg}$.

Proof

Since $\text {M}_{vcg}$ is a model of $\Sigma _{vcg}$ (see Lemma 3), we have to show that for each path $\updelta$ in $\text {M}_{vcg}$ and each agent $\mathsf {i}\in \text {N}$,

• 1. $\updelta$ is a complete path;

• 2. $\text {M}_{vcg}\models \bigvee _{a \in \mathcal {B}}legal_\mathsf {i}(a)$.

Given a path $\updelta$ in $\text {M}_{vcg}$ and a stage $t$ of $\updelta$. Let us verify Statement 1. We show that $\text {M}_{vcg}\models initial \rightarrow \bigcirc terminal$. Assume $\text {M}_{vcg}, \updelta , t \models initial$. Then, $\updelta [t]= \bar{\text {w}}$. By the path definition, for any $j\ge 1$, $\updelta [j] \ne \bar{\text {w}}$. By the construction of $\text {T}$, we have $\text {T}= \text {W}{\setminus } \{\bar{\text {w}}\}$. Thus, $\text {M}_{vcg}, \updelta , t+1 \models terminal$ and $\text {M}_{vcg}, \updelta , t \models \bigcirc terminal$.

Statement 2 is straightforward from Rules 3 and 4 from $\Sigma _{vcg}$.

The next lemma shows that if an agent bids $\text {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 4

For each agent $\mathsf {i}\in \text {N}$, $\text {M}_{vcg} \models initial \wedge does_\mathsf {i}(\text {noop}) \rightarrow \bigcirc payment_\mathsf {i}= 0 \wedge \bigwedge _{j\in \text {G}} trade_{\mathsf {i}, j} \ge 0$

We then focus on properties from Mechanism Design, that is budget balance, individual rationality, efficiency and strategyprofness. These results for VCG have already been proved [36, 52] and here we show how they are rephrased and verified with ADL $[\mathcal {F}_{\mathcal {B}}]$. First, due to the VCG payments, $\text {M}_{vcg}$ is not budget balanced.

Proposition 6

$\text {M}_{vcg} \not \models \bigcirc sbb$ and $\text {M}_{vcg} \not \models \bigcirc wbb$.

After the agents report their preferences, $\text {M}_{vcg}$ chooses the trade maximizing the social welfare (i.e., the cumulative of values for the trade given the agents’ bids).

Proposition 7

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, $\text {M}_{vcg} \models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$

The VCG mechanism is individually rational when the agents’ preferences over trades are non-negative [52].

Proposition 8

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, if $\vartheta _\mathsf {i}(\varvec{\uplambda }) \ge 0$ for all $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$, $\vartheta _\mathsf {i}\in V_\mathsf {i}$ and $\mathsf {i}\in \text {N}$, then $\text {M}_{vcg} \models does(\varvec{\upbeta }) \rightarrow \bigcirc ir(\varvec{\upbeta })$.

The VCG mechanism is also strategyproof [52], because the bid of an agent does not influence her payment.

Theorem 4

$\text {M}_{vcg}$ is strategyproof.

Proof

Given a path $\delta$ in $\text {M}_{vcg}$ and a stage $t\ge 0$ in $\delta$, such that $\text {L}(\delta [t], \mathsf {i}) \approx _\mathsf {i}V_\mathsf {i}$. Since $\text {M}_{vcg} \models initial \rightarrow \bigcirc terminal$ and $\updelta [t+1] = \updelta [t]$ whenever $\updelta [t]\in \text {T}$, it suffices to show consider the case where $t=0$.

Let $\varvec{\vartheta } \in \prod _{\mathsf {i}\in \text {N}}V_\mathsf {i}$ be a preference profile and $\delta _{\varvec{\vartheta }}$ denote a path such that $\delta [0] = \delta _{\varvec{\vartheta }}[0]$ and $\theta (\delta _{\varvec{\vartheta }}, 0) = \varvec{\upbeta _\vartheta }$. We let $\vartheta '_{\mathsf {i}} \in V_\mathsf {i}$ denote a preference of agent $\mathsf {i}$, $\varvec{\vartheta '} = (\vartheta _\mathsf {i}', \vartheta _{-\mathsf {i}})$ and $\delta _{\varvec{\vartheta '}}$ be a path such that $\delta [0] = \delta _{\varvec{\vartheta '}}[0]$, $\theta _\mathsf {i}(\delta _{\varvec{\vartheta '}}, 0) = \upbeta _{\vartheta '_\mathsf {i}}$ and $\theta _\mathsf {r}(\delta _{\varvec{\vartheta '}}, 0) = \upbeta _{\vartheta _\mathsf {r}}$ for each agent $\mathsf {r}\ne \mathsf {i}$. That is, $\text {M}_{vcg}, \delta _{\varvec{\vartheta }}, 0 \models does(\varvec{\upbeta _\vartheta })$ and $\text {M}_{vcg}, \delta _{\varvec{\vartheta '}},0 \models does_\mathsf {i}(\upbeta _{\vartheta _\mathsf {r}'}) \wedge \bigwedge _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} does_\mathsf {r}(\upbeta _{\vartheta _\mathsf {r}})$.

Let $u_{\vartheta _{\mathsf {i}}}\in \text {I}$ such that $\text {M}_{vcg},\delta _{\varvec{\vartheta }}, 0 \models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}})$, $payment_\mathsf {i}) = u_{\vartheta _{\mathsf {i}}}$ holds. As we saw in the proof of Proposition 8, agent $\mathsf {i}$’s utility in $\delta _{\varvec{\vartheta }}[1]$ is simply

$$\begin{aligned}u_{\vartheta _{\mathsf {i}}} = \sum _{\mathsf {r}\in \text {N}} v_\mathsf {r}(\upbeta _{\vartheta _\mathsf {r}}, \varvec{\uplambda }) - \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _{\vartheta _\mathsf {r}} , \varvec{\uplambda }^{-\mathsf {i}}) \end{aligned}$$

where $\varvec{\uplambda }= \varvec{(\uplambda _{j})}_{j\in \text {G}}$ denote the trade performed in $\delta _{\varvec{\vartheta }}[1]$ with $\uplambda _{\mathsf {i}, j} = \uppi _{\text {Y}}(\delta _{\varvec{\vartheta }}[1]$, $trade) = \text {WD}_{\uplambda _{\mathsf {i}, j}}(\varvec{\upbeta }, \mathsf {X})$ for each good $j$ and agent $\mathsf {i}$, and $\varvec{\uplambda }^{-\mathsf {i}} = \text {WD}_{\varvec{\uplambda }}^{-\mathsf {i}}(\varvec{\upbeta }, \mathsf {X})$ is the trade that would happen if $\mathsf {i}$ did not participate in the auction.

Notice that the bid of $\mathsf {i}$ has no impact in $\sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}})$ by the definition of $\text {WD}_{\varvec{\uplambda }}^{-\mathsf {i}}$. Thus, it means that the bid maximizing $\mathsf {i}$’s utility is the one that maximize

$$\begin{aligned}\sum _{\mathsf {r}\in \text {N}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }) \end{aligned}$$

which, by definition, is the case when she bids truthfully. That is, $u_{\vartheta _{\mathsf {i}}}$ is the maximum utility $\mathsf {i}$ obtains in the succeeding stages of all paths starting in $\delta [0]$. Thus, $\text {M}_{vcg},\delta _{\varvec{\vartheta }},0 \models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}})$, $payment_\mathsf {i}) = u_{\vartheta _{\mathsf {i}}}$ and for any $\vartheta '$, $\text {M}_{vcg},\delta _{\varvec{\vartheta '}}, 0 \models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {i}) \le u_{\vartheta _{\mathsf {i}}}$.

We conclude the section by discussing variants of combinatorial exchange. In combinatorial auctions, there are two types of participants: buyers and sellers. The main difference to a combinatorial exchange is that buyers can only demand for non-negative quantities and prices while sellers can only ask for non-positive quantities and prices. These restrictions can be easily encoded in ADL $[\mathcal {F}_{\mathcal {B}}]$ by including a proposition for denoting the participants’ types and defining legality rules based on their types. In Sect. 5, we exemplify the representation of a single-sided auction. Restricting the number of participants with the type buyer (or similarly seller) to one is an alternative way of encoding single-sided auctions. Multi-unit auctions with single items can be represented for different market structures (e.g., the single-sided setting) by restricting the number of good types to one (that is, $|\text {G}| = 1$). In the next section, we show how to represent an iterative protocol in ADL $[\mathcal {F}_{\mathcal {B}}]$ using a slightly different version of TBBL.

6.3 Iterative combinatorial exchange

We conclude the section on combinatorial exchange by considering an iterative protocol, denoted ICE. The protocol is a simplified and first-price version of the mechanism presented in [53]. In this auction, bidders report an interval of prices they are willing to pay (or receive) for a trade. For ensuring termination, agents need to refine their bids, that is, to shrink the value interval reported in their previous bid. For expressing such conditions, we consider the TBBL extension with value bounds, denoted $\mathcal {L}_{\textsf {{TBBL}} +}$. In this variant proposed by Lubin et al. [41], agents report a pair of valuation bounds in each node of their bid. The syntax of $\mathcal {L}_{\textsf {{TBBL}} +}$ is obtained by replacing the value $\mathsf {v}$ of a leaf node $\langle \mathsf {q},j, \mathsf {v} \rangle$ by the lower bound $\underline{\mathsf {v}} \in \text {I}$ and upper bound $\overline{\mathsf {v}} \in \text {I}$ with $\underline{\mathsf {v}} \le \overline{\mathsf {v}}$. The bounds $\underline{\mathsf {v}}$ and $\overline{\mathsf {v}}$ denote the minimum and maximum price the bidder considers acceptable to pay (or receive) for $\mathsf {q}$ units of $j$, respectively. Bid nodes with IC operators are similarly updated to include value bounds.

Given an agent $\mathsf {i}\in \text {N}$, a bid $\upbeta \in \mathcal {L}_{\textsf {{TBBL}} +}$ and a trade $\uplambda \in \text {I}^{\mathsf {n}\mathsf {m}}$, the functions $\underline{v}_\mathsf {i}(\upbeta , \uplambda )$, $\overline{v}_\mathsf {i}(\upbeta , \uplambda )$, $\underline{b}_\mathsf {i}(\upbeta )$, $\overline{b}_\mathsf {i}(\upbeta )$ are defined with the same semantics from the functions $v_\mathsf {i}$ and $b_\mathsf {i}$ introduced in Sect. 6. Since the lower bound is no greater than the upper bound, we have that $\underline{b}_\mathsf {i}(\upbeta ) \le \overline{b}_\mathsf {i}(\upbeta )$ and $\underline{v}_\mathsf {i}(\upbeta , \uplambda ) \le \overline{v}_\mathsf {i}(\upbeta , \uplambda )$. For representing this ICE protocol with $\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$, we first fix a constant $\varepsilon \in [0,1]$ for estimating the weight of the bounds in the value of a bid given a trade (i.e., function $v_\mathsf {i}$). If $\varepsilon = 1$, the bid value is based only on its lower bounds. Likewise, the upper bounds determinate the bid value when $\varepsilon = 0$. Next, we describe the auction signature, written $\mathcal {S}_{ice} = (\text {N},\text {G}, \mathcal {B}, \{\}, \text {Y}, \text {I}, \mathcal {F}_{\mathcal {B}})$, where $\text {N}= \{1, \ldots , \mathsf {n}\}$, $\text {G}= \{1, \ldots , \mathsf {m}\}$, $\mathcal {B}\subseteq \mathcal {L}_{\textsf {{TBBL}} +}$, $\text {Y}= \{ trade_{\mathsf {i},j}$, $payment_\mathsf {i}: \mathsf {i}\in \text {N}, j\in \text {G}\}$, and $\text {I}\subset \mathbb Z$. If $\langle \mathsf {q},j, \underline{\mathsf {v}}, \overline{\mathsf {v}} \rangle$ is a bid in $\mathcal {B}$, we assume $\langle \mathsf {q},j, \underline{\mathsf {v}}', \overline{\mathsf {v}}' \rangle \in \mathcal {B}$ for any $\underline{\mathsf {v}}'\ge \underline{\mathsf {v}}$ and $\overline{\mathsf {v}}' \le \overline{\mathsf {v}}$ such that $\underline{\mathsf {v}}'\le \overline{\mathsf {v}}'$. Similarly, if $\text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta },\underline{\mathsf {v}}, \overline{\mathsf {v}}) \in \mathcal {B}$, we assume $\text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta },\underline{\mathsf {v}}', \overline{\mathsf {v}}') \in \mathcal {B}$ for any $\underline{\mathsf {v}}'\ge \underline{\mathsf {v}}$ and $\overline{\mathsf {v}}' \le \overline{\mathsf {v}}$ such that $\underline{\mathsf {v}}'\le \overline{\mathsf {v}}'$. $\mathcal {F}_{\mathcal {B}}$ contains the basic mathematical operations as well as the following functions: $v_\mathsf {i}: \mathcal {B}\times \text {I}^{\mathsf {n}\mathsf {m}} \rightarrow \text {I}$, $\text {WD}_{\uplambda _{\mathsf {i},j}}^\varepsilon : \mathcal {B}^\mathsf {n}\times \text {I}^{\mathsf {n}\mathsf {m}} \rightarrow \text {I}$, $\text {eq}: \mathcal {B}\times \mathcal {B}\rightarrow [0,1]$ and $\text {uncert}: \mathcal {B}\rightarrow \text {I}$. We next describe each of those functions.

Given an agent $\mathsf {i}$, the value of bid $\upbeta \in \mathcal {L}_{\textsf {{TBBL}} +}$ given a trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$ is defined as follows:

$$\begin{aligned} v_\mathsf {i}(\upbeta , \varvec{\uplambda }) = \left\lceil \varepsilon \cdot \underline{v}_\mathsf {i}(\upbeta , \varvec{\uplambda }) \right\rceil + \left\lfloor (1-\varepsilon )\cdot \overline{v}_\mathsf {i}(\upbeta , \varvec{\uplambda }) \right\rfloor \end{aligned}$$

Notice the rounding of the terms⁶ ensure the result will not be smaller than the lower bound neither greater than the upper bound.

Assuming a joint bid $\varvec{\upbeta }\in \mathcal {L}_{\textsf {{TBBL}} +}^\mathsf {n}$ and an initial allocation $X\in \text {I}_{\succeq 0}^{\mathsf {n}\mathsf {m}}$, function $\text {WD}_{\uplambda _{\mathsf {i},j}}^\varepsilon (\varvec{\upbeta }, X)$ is defined exactly as function $\text {WD}_{\uplambda _{\mathsf {i},j}}(\varvec{\upbeta }, X)$ defined in Sect. 6.1.2, except that the winner determination is replaced by the following:

$$\begin{aligned} \text {WD}^\varepsilon (\varvec{\upbeta }, X): \mathop {{{\,\mathrm{argmax}\,}}}_{\varvec{\uplambda }, \text {sat}} \sum _{\mathsf {i}\in \text {N}} \sum _{\upbeta \in \text {Node}(\upbeta _\mathsf {i})} (\left\lceil \varepsilon \underline{b}_\mathsf {i}(\upbeta ) \cdot \text {sat}_\mathsf {i}(\upbeta ) \right\rceil + \left\lfloor (1-\varepsilon ) \overline{b}_\mathsf {i}(\upbeta ) \cdot \text {sat}_\mathsf {i}(\upbeta ) \right\rfloor ) \\ \text {s.t. Constraints } C1-C4 \text { hold (see Def. 18)} \end{aligned}$$

Given two bids $\upbeta , \upgamma \in \mathcal {L}_{\textsf {{TBBL}} +}$, $\text {eq}(\upbeta , \upgamma )$ denotes whether they are equivalent on structure, in the sense of differing only on their valuation bounds, and it is defined as follows:

• If $\upbeta$ is in the form $\langle \mathsf {q}, j, \underline{\mathsf {v}}, \overline{\mathsf {v}}\rangle$ and $\upgamma = \langle \mathsf {q}, j, \underline{\mathsf {v}}', \overline{\mathsf {v}}' \rangle$ for some $\underline{\mathsf {v}}', \overline{\mathsf {v}}' \in \text {I}$, then $\text {eq}(\upbeta , \upgamma )= 1$;

• If $\upbeta$ is in the form $\text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta },\underline{\mathsf {v}}, \overline{\mathsf {v}})$, $\upgamma = \text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta }',\underline{\mathsf {v}}', \overline{\mathsf {v}}')$ for some $\underline{\mathsf {v}}', \overline{\mathsf {v}}'\in \text {I}$ and each $\bar{\upbeta }_k \backsim \bar{\upbeta }'_k$, for each $0 < k_i \le |\bar{\upbeta }|$, then $\text {eq}(\upbeta , \upgamma )= 1$;

• Otherwise, $\text {eq}(\upbeta , \upgamma )= 0$.

The difference among the bounds of a node represents its uncertainty. That is, the higher the bound difference, the less precise the node is about the agents’ preference. The actual willingness-to-pay (or receive), is unknown except when the lower and upper bounds are the same [53]. We define function $\text {uncert}(\langle \mathsf {q}, j, \underline{\mathsf {v}}, \overline{\mathsf {v}}\rangle ) = \overline{\mathsf {v}}-\underline{\mathsf {v}}$ and $\text {uncert}(\text {IC}_{\text {y}}^{\text {x}}(\bar{\upbeta },\underline{\mathsf {v}}, \overline{\mathsf {v}})) = \overline{\mathsf {v}}-\underline{\mathsf {v}} + \sum _{0 < k \le |\bar{\upbeta }|}\text {uncert}(\bar{\upbeta }_k)$ for capturing the uncertainty of bid in $\mathcal {L}_{\textsf {{TBBL}} +}$.

Each instance of ICE is specific and is defined with respect to $\mathcal {B}$, $\text {I}$ and the constant values $\varepsilon \in [0,1]$, $\mathsf {n}, \mathsf {m}\in \text {I}_{\succ 0}$ (the size of $\text {N}$ and $\text {G}$, resp.), and $\mathsf {X}= \varvec{(\mathsf {x}_{j})}_{j\in \text {G}}$, where $\mathsf {x}_{\mathsf {i},j}\in \text {I}_{\succeq 0}$, for each $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. The rules of a ICE are represented by ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae as shown in Fig. 6.

Fig. 6

An Iterative Combinatorial Exchange represented by $\Sigma$

In the initial state, there is no payment or trade for any agent (Rule 1) and agents can report any bid (Rule 2). After performing a bid, an agent is allowed to report any bid that has the same structure and less uncertainty than her last bid. When the bid has no uncertainty (i.e., for each node, its lower and upper bounds are the same), the agent must repeat her bid in the next turn (Rules 3 and 4). When there is no uncertainty in all bids performed in a state, the next state is terminal (Rule 5). The agents pay their reported values according to their trade in a given state (Rule 6). Finally, the agents’ trades are computed in each round using the winner determination given their bids and their initial allocation (Rule 7).

6.3.1 Representing as a model

Next, we address the model representation. Let $\mathscr {M}_{ice}$ be the set of ST-models $\text {M}_{ice}$ defined for any $\mathcal {B}\subseteq \mathcal {L}_{\textsf {{TBBL}} +}$, $\text {I}\subset \mathbb Z$, and the constants $\mathsf {n}, \mathsf {m}\in \text {I}_{\succ 0}$ and $\mathsf {X}= \varvec{(\mathsf {x}_{j})}_{j\in \text {G}}$, where $\mathsf {x}_{\mathsf {i},j}\in \text {I}_{\succeq 0}$, for each $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. Each $\text {M}_{ice}$ is defined as follows:

• $\text {W}= \{\langle \varvec{(\uplambda _{j})}_{j\in \text {G}}, \varvec{\text {p}}, \varvec{lastbid}\rangle : lastbid_\mathsf {i}\in \mathcal {B}$ & $\text {p}_\mathsf {i}, \uplambda _{\mathsf {i},j} \in \text {I}$ & $\mathsf {i}\in \text {N}$ & $j\in \text {G}\}$;

• $\bar{\text {w}}= \langle 0, \ldots , 0, 0,\ldots , 0, \text {noop}, \ldots , \text {noop}\rangle$;

• $\text {T}= \{\langle \varvec{(\uplambda _{j})}_{j\in \text {G}}, \varvec{\text {p}}, \varvec{lastbid}\rangle : \text {uncert}(lastbid_\mathsf {i}) = 0$ & $lastbid_\mathsf {i}\in \mathcal {B}$ & $\text {p}_\mathsf {i}, \uplambda _{\mathsf {i},j} \in \text {I}$ & $\mathsf {i}\in \text {N}$ & $j\in \text {G}\} \}$;

• $\text {L}= \{(\bar{\text {w}}, \mathsf {i}, \upbeta ): \mathsf {i}\in \text {N}$ & $\upbeta \in \mathcal {B}\} \cup \{ ( \langle \varvec{(\uplambda _{j})}_{j\in \text {G}}, \varvec{\text {p}}, \varvec{lastbid}\rangle , \mathsf {i},$ $\upbeta ) : \text {eq}(\upbeta , lastbid_\mathsf {i})$ & $\text {uncert}(\upbeta )<\text {uncert}(lastbid_\mathsf {i})$ & $\upbeta , lastbid_\mathsf {r}\in \mathcal {B}$ & $\text {p}_\mathsf {r}, \uplambda _{\mathsf {r},j} \in \text {I}$ & $\mathsf {r}, \mathsf {i}\in \text {N}$ & $j\in \text {G}\}$;

• $\text {U}$ is defined as follows: for all $\text {w}= \langle \varvec{(\uplambda _{j})}_{j\in \text {G}}, \varvec{\text {p}}, \varvec{lastbid}\rangle \in \text {W}$ and for all $\varvec{d} \in \mathcal {B}^\mathsf {m}$:

  • If $\text {w}\not \in \text {T}$, then $\text {U}(\text {w}, \varvec{d}) = \langle \varvec{(\uplambda '_{j})}_{j\in \text {G}}, \varvec{\text {p}'}, \varvec{d}\rangle \rangle$, where each component is updated as follows, for each $\mathsf {i}\in \text {N}$ and $j\in \text {G}$: $\uplambda _{\mathsf {i},j}' = \text {WD}_{\uplambda _{\mathsf {i},j}}^\varepsilon (\varvec{d}, \mathsf {X} )$ and $\text {p}_\mathsf {i}' = v_\mathsf {i}(d_\mathsf {i}, \varvec{(\uplambda '_{j})}_{j\in \text {G}})$.

  • Otherwise, $\text {U}(\text {w},\varvec{d}) = \text {w}$.

• For each $\text {w}\in \text {W}$, $\mathsf {i}\in \text {N}$ and $j\in \text {G}$, the valuation of numerical variables is as follows: $\uppi _{\text {Y}}(\text {w}$, $trade_{\mathsf {i},j}) = \uplambda _{\mathsf {i},j}$ and $\uppi _{\text {Y}}(\text {w}, payment_\mathsf {i}) = \text {p}_\mathsf {i}$.

Hereafter, we assume an instance of $\text {M}_{ice}\in \mathscr {M}_{ice}$ and $\Sigma _{ice}$ for some $\mathcal {B}\subseteq \mathcal {L}_{\textsf {{TBBL}} +}$, $\text {I}\subset \mathbb Z$, $\mathsf {n}, \mathsf {m}\in \text {I}_{\succ 0}$ and $\mathsf {x}_{\mathsf {i},j} \in \text {I}_{\succeq 0}$, where $\mathsf {i}\in \text {N}$, $j\in \text {G}$.

Example 3

Let $\text {M}_{ice}\in \mathscr {M}_{ice}$, where (i) there are only two agents, denoted by $\mathsf {r}$ and $\mathsf {s}$, (ii) there is only one good type, denoted by $\mathsf {a}$, and (iii) $\mathsf {x}_{\mathsf {r},\mathsf {a}} =1$ and $\mathsf {x}_{\mathsf {s},\mathsf {a}} =0$, i.e, agent $\mathsf {r}$ holds 1 unit of $\mathsf {a}$ and agent $\mathsf {s}$ has none. Figure 5 illustrates a path in $\text {M}_{ice}$. In the initial state $\text {w}_0$, agent $\mathsf {r}$ says she wants to sell $\mathsf {a}$ for a price between 10€ and 20€ and agent $\mathsf {s}$ reports her willingness to buy it for a price between 15€ and 25€. In state $\text {w}_1$, the agents are informed of the provisional trade and payments. Agent $\mathsf {s}$ changes her bid to specify she is willing to receive exactly 15€ for selling $\mathsf {a}$. By her turn, agent $\mathsf {r}$ specifies a value range 18€ to 20€ for buying $\mathsf {a}$. In $\text {w}_2$, only $\mathsf {s}$ can change her bid, since there is no uncertainty in $\mathsf {r}$’s bid. Then, $\mathsf {s}$ reports her willingness to pay exactly 18€. State $\text {w}_3$ is terminal because there was no uncertainty in the bids reported on $\text {w}_2$. The good is traded and the agents pay (and receive) their asking prices.

Fig. 7

A path in $\text {M}_{ice}$ where two agents trade a good

6.3.2 Evaluating the protocol

Now we focus on the evaluation of $\Sigma _{ice}$ and $\text {M}_{ice}$. First, Lemma 5 shows the soundness of $\Sigma _{ice}$ over $\text {M}_{ice}$.

Lemma 5

$\text {M}_{ice}$ is an ST-model and it is a model of $\Sigma$.

Since $\text {M}_{ice}$ is playable and terminates, $\Sigma _{ice}$ is well-formed.

Theorem 5

$\Sigma _{ice}$ is a well-formed protocol over $\text {M}_{ice}$.

Proof

Since $\text {M}_{ice}$ is a model of $\Sigma _{ice}$, we show that for each path $\updelta$ in $\text {M}_{ice}$, each stage $t\ge 0$ in $\delta$ and each agent $\mathsf {i}\in \text {N}$,

• 1. $\updelta$ is a complete path;

• 2. $\text {M}_{ice}, \delta , t\models \bigvee _{\upbeta \in \mathcal {B}}legal_\mathsf {i}(\upbeta )$.

First, we consider Statement 2. By the definition of $\mathcal {L}_{\textsf {{TBBL}} +}$, $\text {uncert}(\upbeta ) \ge 0$ for each bid $\upbeta \in \mathcal {B}$. According to the legality definition, $\text {uncert}(\theta _\mathsf {i}(\delta , t)) < \text {uncert}(\theta _\mathsf {i}(\delta , t-1))$ or $\text {uncert}(\theta _\mathsf {i}(\delta , t)) = 0$. That is, either the bid reported by $\mathsf {i}$ in $\delta [t]$ has less uncertainty than the one she reported in $\delta [t-1]$ or it has no uncertainty. In the case of no uncertainty, $\theta _\mathsf {i}(\delta , t) = \theta _\mathsf {i}(\delta ,e)$ for each $e\ge t$. Since the uncertainty decreases in each turn until being equal to zero, there exists a stage $e\ge 0$ such that $\text {M}_{ice},\delta , e\models does_\mathsf {i}(\upbeta ) \wedge \text {uncert}(\upbeta ) = 0$ for each agent $\mathsf {i}$. By Rule 5, it follows that the next stage in $\delta$ is terminal, that is, $\text {M}_{ice}, \delta , e\models \bigcirc terminal$.

We now verify Statement 2. If $\delta [t] = \bar{\text {w}}$, then $\text {M}_{ice}, \delta , t\models legal_\mathsf {i}(\upbeta )$ for each $\upbeta \in \mathcal {B}$ (Rule 2). Otherwise, $t>0$ and $\text {M}_{ice}, \delta , t-1 \models does_\mathsf {i}(\upbeta )$ for some $\upbeta \in \mathcal {B}$. By the definition of $\mathcal {L}_{\textsf {{TBBL}} +}$, $\text {uncert}(\upbeta ) \ge 0$. If $\text {uncert}(\upbeta ) = 0$, then $\text {M}_{ice}, \delta , t\models legal_\mathsf {i}(\upbeta )$ (Rule 4). Finally, if $\text {uncert}(\upbeta ) <0$, by the definition of $\mathcal {B}$, there must exist a bid $\upgamma$ such that $\text {eq}(\upbeta , \upgamma )$ and $\text {uncert}(\upgamma )<\text {uncert}(\upbeta )$. According to Rule 3 of $\Sigma _{ice}$, $\text {M}_{ice}, \delta , t\models legal_\mathsf {i}(\upgamma )$.

The cumulative of payments cannot be smaller than zero. However the auction may have positive transfers.

Proposition 9

$\text {M}_{ice}\not \models \bigcirc sbb$ and $\text {M}_{ice} \models \bigcirc wbb$.

ICE is individually rational, since agents pay their reported preferences.

Proposition 10

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, $\text {M}_{ice}\models does(\varvec{\upbeta }) \rightarrow \bigcirc ir(\varvec{\upbeta })$.

The protocol is efficient since the winner determination maximizes the social welfare given the reported bids.

Proposition 11

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, $\text {M}_{ice}\models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$

Since the players’ bids influence their payments, they can manipulate the price and the auction is not strategyproof.

Proposition 12

$\text {M}_{ice}$ is not strategyproof.

The automated verification of strategyproofness and termination requires meta-reasoning over the possible paths of a ST-Model. However, for a number properties (such as efficiency and individual rationality), the problem of analysing a stage as a direct mechanism boils down to model-checking ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae.

7 Model checking

Now we examine the complexity of the problem of deciding whether an ADL $[\mathcal {F}_{\mathcal {B}}]$ formula is true with respect to a model, a path and a stage in the path.

Definition 19

The model checking problem for ADL $[\mathcal {F}_{\mathcal {B}}]$ is the following: Given an ST-Model $\text {M}$, a path $\updelta$ in $\text {M}$, a stage $t\ge 0$ in $\updelta$ and a formula $\varphi \in \textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]$, determine whether $\text {M}, \updelta , t\models \varphi$ or not.

In the next sections, we show that the model checking problem for ADL $[\mathcal {F}_{\mathcal {B}}]$ is decidable in polynomial-time deterministic Turing machine (PTIME) when functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in polynomial time.

7.1 Upper bound

Let $\varphi \in$ be a formula and $\text {M}$ be an ST-Model over $\mathcal {S}$. We say that $\psi$ is a subformula of $\varphi$ if either (i) $\psi = \varphi$; (ii) $\varphi$ is of the form $\lnot \phi$, or $\bigcirc \psi$ and $\psi$ is a subformula of $\phi$; or (iii) $\varphi$ is of the form $\phi \wedge \phi '$ and $\psi$ is a subformula of either $\phi$ or $\phi '$. We denote $Subformula (\varphi )$ as the set of all subformulae of $\varphi$.

Theorem 6

Assuming that functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in polynomial time, the model checking problem for ADL $[\mathcal {F}_{\mathcal {B}}]$ is in PTIME.

Proof

Assume the functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in polynomial time. Algorithm modelCheck works in the following way: first it gets all subformulae of $\varphi$ and orders them in a vector S by ascending length. Thus, $S(|\varphi |) = \varphi$, i.e., the position $|\varphi |$ in S corresponds to the formula $\varphi$ itself, and if $\phi _i$ is a subformula of $\phi _j$ then $i < j$. An induction on S labels each subformula $\phi _i$ depending on whether or not $\phi _i$ is true in $\delta [j]$ under $\text {M}$. Since functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in polynomial time, if $\phi _i$ does not have any subformula, its truth value is obtained directly from the model. Since S is ordered by formulae length, if $\phi _i$ is either of the form $\phi ' \wedge \phi ''$ or $\lnot \phi '$ the algorithm labels $\phi _i$ according to the label assigned to $\phi '$ and/or $\phi ''$. If $\phi _i$ is of the form $\bigcirc \phi '$ then its label is recursively defined according to $\phi '$ truth value in the stage $t+1$. As Algorithm modelCheck visits each subformula at most once, and the number of subformulas is not greater than the size of $\varphi$, the algorithm can clearly be implemented in a polynomial-time deterministic Turing machine with PTIME.

7.2 Lower bound

Now let us characterize a lower bound of the complexity of model-checking ADL $[\mathcal {F}_{\mathcal {B}}]$. To do so, we reduce the model checking problem for GDL, which is known to be PTIME (consequence of Lemma 2 by Jiang et al. [29]).

Theorem 7

The model checking problem for ADL $[\mathcal {F}_{\mathcal {B}}]$ is PTIME.

Proof

First, we recall GDL definitions. By convenience, we refer to the GDL formalization presented in [27]. Let $\mathcal {S}_{\text {GDL}} = (\text {N}, \mathcal {B}, {\Upphi })$ be a game signature, where ${\Upphi }$ is a propositional set, $\text {N}$ is a set of agents, and $\mathcal {B}$ is the action set. Let $\text {M}_{\text {GDL}}= (\text {W}, \bar{\text {w}}, \text {T}, \text {L}, \text {U}, g, \uppi _{{\Upphi }})$ be a GDL model over $\mathcal {S}_{\text {GDL}}$, where $\text {W}$, $\bar{\text {w}}$, $\text {T}$, $\text {L}$ and $\uppi _{{\Upphi }}$ are defined in the same way as in a ADL $[\mathcal {F}_{\mathcal {B}}]$ model (see Definition 2), $\text {U}: \text {W}\times \mathcal {B}^{|\text {N}|} \rightarrow \text {W}{\setminus } \{\bar{\text {w}}\}$ is the update function and $g : \text {N}\rightarrow 2^\text {W}$ is the goal function.

A path $\updelta$ in $\text {M}_{\text {GDL}}$ is an infinite sequence of states and joint actions, defined in the same way as Definition 3. Let $\updelta$ be a path in $\text {M}_{\text {GDL}}$, a formula $\varphi$ in $\mathcal {L}_{\text {GDL}}$ is defined by the following BNF:

$$\begin{aligned}\varphi ::= p \mid initial\mid terminal\mid legal_{\mathsf {r}}(a) \mid wins(\mathsf {r}) \mid does_{\mathsf {r}}(a) \mid \lnot \varphi \mid \varphi \wedge \varphi \mid \bigcirc \varphi \end{aligned}$$

where $p \in {\Upphi }$, $\mathsf {r}\in \text {N}$ and $a \in \mathcal {B}$.

For any stage $t\ge 0$ and formula $\varphi \in \mathcal {L}_{\text {GDL}}$, the semantics of $\mathcal {L}_{\text {GDL}}$ are similar to Definition 5, except by the following case: $\text {M}_{\text {GDL}}, \updelta , t\models wins(\mathsf {r}) \text { iff } \updelta [t] \in g(\mathsf {r})$.

Given a stage $t>0$ and a formula $\varphi \in \mathcal {L}_{\text {GDL}}$, we show how to construct an ADL $[\mathcal {F}_{\mathcal {B}}]$ model $\text {M}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$, such that $\text {M}, \delta , t\models \varphi$ iff $\text {M}_{\text {GDL}}, \updelta , t\models \varphi$.

Let $\mathcal {S}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]} = (\text {N}, \emptyset , \mathcal {A}, {\Upphi }', \emptyset , [0,0], \emptyset )$ be the auction signature, where ${\Upphi }' = {\Upphi }\cup \{wins(\mathsf {r}) : \mathsf {r}\in \text {N}\}$. We define the ADL $[\mathcal {F}_{\mathcal {B}}]$ model $\text {M}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]} = (\text {W}, \bar{\text {w}}, \text {T}, \text {L}, \text {U}, \uppi _{{\Upphi }}', \emptyset )$, where $\text {W}, \bar{\text {w}}, \text {T}$ and $\text {U}$ are the same as in $\text {M}_{\text {GDL}}$. The valuation function for state propositions is defined as follows: $\uppi _{{\Upphi }}'(\text {w}) = \uppi _{{\Upphi }}(\text {w}) \cup \{wins(\mathsf {r}): \text {w}\in g(\mathsf {r})$ & $\mathsf {r}\in \text {N}\}$, for each $\text {w}\in \text {W}$.

Since $\text {U}(\text {w}, \varvec{d}) \in \text {W}$, for each $\text {w}\in \text {W}$ and $\varvec{d}\in \mathcal {B}^{|\text {N}|}$, we have that $\text {U}$ is an update function in accordance with Definition 2. Furthermore, if $\updelta$ is a path in $\text {M}_{\text {GDL}}$ then it is a path in $\text {M}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$. Since $\{wins(\mathsf {r}): \mathsf {r}\in \text {N}\} \subseteq {\Upphi }'$, we have that $\mathcal {L}_{\text {GDL}}\subseteq \mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$.

Given $\varphi \in \mathcal {L}_{\text {GDL}}$, if $\varphi$ is not in the form $wins(\mathsf {r})$, then it is straightforward that $\text {M}_{\text {GDL}}, \delta , t\models \varphi$ iff $\text {M}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}, \delta , t\models \varphi$. Now we consider the case were $\varphi \in \mathcal {L}_{\text {GDL}}$ is in the form $wins(\mathsf {r})$, for some $\mathsf {r}\in \text {N}$. Assume $\text {M}_{\text {GDL}}, \delta , t\models wins(\mathsf {r})$ iff $\delta [t] \in g(\mathsf {r})$ iff $wins(\mathsf {r}) \in {\Upphi }'(\delta [t])$ iff $\text {M}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}, \delta , t\models wins(\mathsf {r})$.

Theorem 7 shows that Algorithm modelCheck is optimal when the functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in polynomial time. As for GDL, the ST-model may have exponential size.

Since Algorithm modelCheck calls the functions in $\mathcal {F}_{\mathcal {B}}$ in a polynomial number of times (according to on the formula length), the complexity of computing functions in $\mathcal {F}_{\mathcal {B}}$ will affect its complexity. For instance, the winner determination problem for combinatorial auctions is NP-hard, which is then the complexity of computing the winner determination functions for TBBL [41]. In that case, the model checking problem for ADL $[\mathcal {F}_{\mathcal {B}}]$ is in $\Delta _2^P$, since modelCheck consults a NP-oracle a polynomial number of times.

8 Conclusion

In this paper, we have presented ADL $[\mathcal {F}_{\mathcal {B}}]$, a unified framework for representing auction protocols. Our work is at the frontier of auction theory and knowledge representation. We illustrated the usefulness of our approach by showing how to represent a number of representative auctions, which include features from single and multi-stage protocols, multiple items, multiple copies of those items and exchange protocols (which generalize double-sided auctions).

ADL $[\mathcal {F}_{\mathcal {B}}]$ provides tools for automated verification of properties from mechanism design. We showed how stages in an ADL $[\mathcal {F}_{\mathcal {B}}]$ ST-model may represent direct mechanisms and be evaluated as such. The majority of properties that we considered (noting that at the evaluating a stage in an ST-model essentially comes down to model-checking ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae) can be checked in PTIME when the functions in $\mathcal {F}_{\mathcal {B}}$ can be computed in polynomial time. Thus, ADL $[\mathcal {F}_{\mathcal {B}}]$ enables reasoning about important aspects for designing and playing auctions, while having a reasonable complexity cost.

The main limitation of ADL $[\mathcal {F}_{\mathcal {B}}]$ is due to having a semantics based on fixed paths, that is, non-alternating executions of an auction. This means it is not possible to encode through ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae conditions that compare the effect of different strategic behaviour. An example of such condition is strategyproofness, where one should contrast the agents’ utility after truthfully reporting her preference and after lying. Here, we demonstrated the use of meta-reasoning over the state-transition model for comparing alternative executions of an auction. Furthermore, evaluating indirect mechanisms requires capturing the terminal outcomes (that is, the final trades and payments) in strategic equilibrium. Complex solution concepts, such as Nash and dominant strategy equilibrium, cannot be encoded through ADL $[\mathcal {F}_{\mathcal {B}}]$-formulae. Logics focused on strategic reasoning are more suitable for considering this problem (e.g., ATL with Strategy Contexts [10] and Strategy Logic (SL) [14]). Finding a balance between expressivity and complexity is an open question, as such expressive languages face decidability issues and high complexity for model-checking (e.g., the satisfiability problem of SL is undecidable and its complexity for model-checking is Non Elementary).

ADL $[\mathcal {F}_{\mathcal {B}}]$ definitely puts the emphasis on the auctioneer and mechanism designer. Our next direction is to design a ADL $[\mathcal {F}_{\mathcal {B}}]$-based General Auction Player (GAP) that can interpret and reason about the rules of an auction-based market. The key difference, when the player perspective is considered, is the epistemic and strategic aspects: players have to reason about other players’ behavior and may have imperfect information. Additionally, search optimization techniques used for GGP (see, for instance [20, 68]) may be adapted for considering utility optimization in auctions. Another future direction is to explore the synthesis of state-transition models based on a ADL $[\mathcal {F}_{\mathcal {B}}]$-description of an auction. This problem entails considering the satisfiability problem for the language.

Last but not least, we intend to develop the axiomatic system for ADL $[\mathcal {F}_{\mathcal {B}}]$ and prove its soundness and completeness with respect to the semantics based on the state transition model. It would require a combination of techniques used for Epistemic GDL [28], first-order logic with dependent types [58] and finite algebras [11].

Appendix A: Technical Proof

Proposition 1

Let $\text {M}$ be an ST-model, for each agent $\mathsf {i}\in \text {N}$ and each action $\upbeta \in \mathcal {B}$,

• 1. $\text {M}\models does_\mathsf {i}(\upbeta ) \rightarrow \lnot does_\mathsf {i}(\upbeta ')$, for any $\upbeta ' \in \mathcal {B}$ such that $\upbeta ' \ne \upbeta$

• 2. $\text {M}\models \bigvee _{\upbeta ' \in \mathcal {B}} does_\mathsf {i}(\upbeta ')$

• 3. $\text {M}\models does_\mathsf {i}(\upbeta ) \rightarrow legal_\mathsf {i}(\upbeta )$

• 4. $\text {M}\models \lnot \bigcirc initial$

• 5. $\text {M}\models terminal\wedge \varphi \rightarrow \bigcirc \varphi$, for any $\varphi \in \mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$

• 6. $\text {M}\models initial\rightarrow \lnot terminal$

Proof

Let $\text {M}$ be an ST-model, $\updelta$ be a path, $t\ge 0$ be an stage in $\updelta$, $\mathsf {i}\in \text {N}$ be an agent and $\upbeta \in \mathcal {B}$ be an action. For Statement 1, assume $\text {M}, \updelta , t\models does_\mathsf {i}(\upbeta )$ iff $\uptheta _{\mathsf {i}} (\updelta , t) = \upbeta$. Then for any $\upbeta ' \in \mathcal {B}$ such that $\upbeta ' \ne \upbeta$, $\uptheta _{\mathsf {i}} (\updelta , t) \ne \upbeta '$ and $\text {M}, \updelta , t\models \lnot does_\mathsf {i}(\upbeta ')$.

Statement 2 follows from the definition of $\updelta$, since $\theta _\mathsf {i}(\updelta , t) \in \text {L}(\delta [t], \mathsf {i})$ and $\text {L}(\delta [t], \mathsf {i}) \subseteq \mathcal {B}$, we have $\text {M}, \delta , t\models \bigvee _{\upbeta ' \in \mathcal {B}} does_\mathsf {i}(\upbeta ')$.

Let us verify Statement 3. Assume $\text {M}, \updelta , t\models does_\mathsf {i}(\upbeta )$, then $\uptheta _{\mathsf {i}} (\updelta , t) = \upbeta$ and by the definition of $\updelta$, $\upbeta \in \text {L}(\updelta [t], \mathsf {i})$ and $\text {M}, \updelta , t\models legal_\mathsf {i}(\upbeta )$.

We consider Statement 4. By the path definition, for all $t> 0$, $\delta [t] \ne \bar{\text {w}}$. Thus, $\delta [t+1] \ne \bar{\text {w}}$ and $\text {M}, \delta , t+1 \models \lnot initial$. It follows that $\text {M}, \delta , t\models \lnot \bigcirc initial$.

We now verify Statement 5. Assume $\text {M}\models terminal\wedge \varphi$, for some $\varphi \in \mathcal {L}_{\textsf {{ADL}}[\mathcal {F}_{\mathcal {B}}]}$. Then $\updelta [t] \in \text {T}$ and $\delta [t+1] = \delta [t]$. Thus, $\text {M}, \delta , t+1 \models \varphi$ and $\text {M}, \delta , t\models \bigcirc \varphi$.

Finally, we consider Statement 6. Assume for the sake of contradiction that $\text {M}, \updelta , t\models initial\wedge terminal$. Then, $\updelta [t] = \bar{\text {w}}$ and $\updelta [t] \in \text {T}$. By the path definition, it should be the case that $t= 0$. Due to the loop on terminal states, it follows that $\text {w}_{0} = \text {w}_{1}$, which is a contradiction with the path requirement $\text {w}_{t'} \ne \text {w}_0$, for any $t' \ge 1$.

Lemma 1

$\text {M}_{sa}$ is an ST-model and it is a model of $\Sigma _{sa}$.

Proof

(Sketch) It is routine to check that $\text {M}_{sa}$ is actually an ST-model. Given a path $\updelta$, any stage $t$ of $\updelta$ in $\text {M}_{sa}$, we need to show that $\text {M}_{sa},\updelta , t \models \varphi$, for each $\varphi \in \Sigma _{sa}$. Let us verify Rule 1. Assume $\text {M}_{sa}, \updelta , t\models initial$ iff $\updelta [t]= \bar{\text {w}}$. By the definition of $\bar{\text {w}}$, $\uppi _{{\Upphi }}$ and $\uppi _{\text {Y}}$, we have $\uppi _{\text {Y}}(\bar{\text {w}}, price) = \mathsf {start}$, $\uppi _{\text {Y}}(\bar{\text {w}}, price_j) = \mathsf {start}$, $bid_{\mathsf {i},j} \not \in \uppi _{{\Upphi }}(\bar{\text {w}})$ and $trade_{\mathsf {i},j} = 0$, for all $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. Thus, $\text {M}_{sa}, \updelta , t\models initial$ iff $\text {M}_{sa}, \updelta , t\models price = \mathsf {start}$ $\wedge \bigwedge _{j\in \text {G}} ( price_j=$ $\mathsf {start} \wedge \bigwedge _{\mathsf {i}\in \text {N}} (\lnot bid_{\mathsf {i},j} \wedge trade_{\mathsf {i},j} = 0))$.

Now we verify Rule 2. Let $j\in \text {G}$ be a good type. Assume $\text {M}_{sa}, \updelta , t\models sold_j$ iff $sold_j \in \uppi _{{\Upphi }}(\updelta [t])$ iff $\uppi _{\text {Y}}(\updelta [t], trade_{\mathsf {i},j}) = 1$ for some $j\in \text {G}$ iff $\text {M}_{sa}, \updelta , t\models \bigvee _{\mathsf {i}\in \text {N}} trade_{\mathsf {i},j} = 1$.

Next, we consider Rule 3. Assume $\text {M}_{sa}, \updelta , t\models terminal$ iff $\updelta [t]\ne \bar{\text {w}}$ and for all $j\in \text {G}$, either $\text {M}_{sa}, \updelta , t\models trade_{r,j} = 1$ for some $\mathsf {r}\in \text {N}$ or $\text {M}_{sa}, \updelta , t\models \lnot bid_{\mathsf {i},j}$ for all $\mathsf {i}\in \text {N}$. By Rule 2, $\text {M}_{sa}, \updelta , t\models terminal$ iff $\text {M}_{sa}, \updelta , t\models \lnot initial \wedge \bigwedge _{j\in \text {G}} (sold_j \vee \bigwedge _{j\in \text {G}} \lnot bid_{\mathsf {i},j})$.

Now we verify Rule 9. Let $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. Assume $\text {M}_{sa}, \updelta , t\models (does_\mathsf {i}(p_1, \ldots , p_\mathsf {m}) \wedge p_j\ne 0) \vee (bid_{\mathsf {i},j} \wedge terminal)$, for some $p_1, \ldots , p_\mathsf {m}\in \text {I}_{\succeq 0}$. We next prove for the two cases. First, assume $\text {M}_{sa}, \updelta , t\models bid_{\mathsf {i},j} \wedge terminal$. Then $bid_{\mathsf {i},j} \in \uppi _{{\Upphi }}(\updelta [t])$ and $\updelta [t]\in \text {T}$. By the update function, $\updelta [t+1] = \updelta [t]$ and $\text {M}_{sa}, \updelta , t+1 \models bid_{\mathsf {i},j}$, i.e., $\text {M}_{sa}, \updelta , t\models \bigcirc bid_{\mathsf {i},j}$. In the second case, assume $does_\mathsf {i}(p_1, \ldots ,p_\mathsf {m}) \wedge p_j\ne 0$. By the update function, $bid_{\mathsf {i},j}\in \uppi _{{\Upphi }}(\updelta [t+1])$ and thus $\text {M}_{sa}, \updelta , t\models \bigcirc bid_{\mathsf {i},j}$.

The remaining rules are verified in a similar way.

Proposition 2

For each $j\in \text {G}$ and each $\mathsf {i}, \mathsf {r}\in \text {N}$ such that $\mathsf {i}\ne \mathsf {r}$,

• 1. $\text {M}_{sa}\models trade_{\mathsf {i},j} = 0 \vee trade_{\mathsf {r},j} = 0$

• 2. $\text {M}_{sa}\models sold_j\rightarrow \bigcirc sold_j$

• 3. $\text {M}_{sa}\models \lnot sold_j\rightarrow price = price_j$

Proof

Given a path $\updelta$ in $\text {M}_{sa}$, any stage $t$ of $\updelta$ and a good type $j\in \text {G}$, let $\mathsf {i}, \mathsf {r}\in \text {N}$, such that $\mathsf {i}\ne \mathsf {r}$. Let us consider Statement 1. If $\updelta [t]= \bar{\text {w}}$, then $\text {M}_{sa}, \updelta , t\models trade_{\mathsf {i},j} =0 \wedge trade_{\mathsf {r},j} =0$ (see Rule 1). Otherwise, by the path definition, $\updelta [j] = \text {U}(\updelta [t-1], \uptheta (\updelta , t-1))$. Let us suppose for the sake of contradiction that $\text {M}_{sa}, \updelta , t\not \models trade_{\mathsf {i},j} = 0 \vee trade_{\mathsf {r}, j} = 0$. Since $\text {W}$ construction defines $trade_{\mathsf {i},j}, trade_{\mathsf {r}, j} \in \{0,1\}$, we have $\text {M}_{sa}, \updelta , t\models trade_{\mathsf {i},j} = 1 \wedge trade_{\mathsf {r}, j} = 1$. Thus, $\text {M}_{sa}, \updelta , t-1 \models \bigcirc trade_{\mathsf {i},j}$. By Rule 4, $\text {M}_{sa}, \updelta , t-1 \models \bigcirc (bid_{\mathsf {i},j} \wedge \bigwedge _{\mathsf {s}\in \text {N}{\setminus } \{\mathsf {i}\}} \lnot bid_{\mathsf {s},j})$. Thereby, $\text {M}_{sa}, \updelta , t-1 \not \models \bigcirc (bid_{\mathsf {r}, j} \wedge \bigwedge _{\mathsf {s}\in \text {N}{\setminus } \{\mathsf {r}\}} \lnot bid_{\mathsf {s},j})$ and $\text {M}_{sa}, \updelta$, $t-1 \not \models \bigcirc trade_{\mathsf {r}, j=1}$. Thus, $\text {M}_{sa}, \updelta , t\not \models trade_{\mathsf {r}, j} = 1$, which is a contradiction.

For Statement 2. Assume $\text {M}_{sa}, \delta , t\models sold_j$. Then, $\text {M}_{sa}, \delta , t\models trade_{\mathsf {i}, j} = 1$ for some agent $\mathsf {i}\in \text {N}$. From Rule 6, $\theta _\mathsf {i}(\delta , t) = (p_1, \dots , p_\mathsf {m})$ with $p_j= \uppi _{\text {Y}}(\delta [t], price_j)$ and $\theta _\mathsf {r}(\delta , t) = (p_1', \dots , p_\mathsf {m}')$ with $p_j' = 0$, for all agent $\mathsf {r}\ne \mathsf {i}$. By Rule 9, we have $\text {M}_{sa}, \delta , t\models bid_{\mathsf {i}, j} \wedge \bigwedge _{\mathsf {r}\in \text {N}{\setminus } \{\mathsf {i}\}} \lnot bid_{\mathsf {r},j}$. Thus, it follows from Rules 2 and 4 that $\text {M}_{sa}, \delta , t\models \bigcirc trade_{\mathsf {i}, j} = 1$ and $\text {M}_{sa}, \delta , t\models \bigcirc sold_j$.

For Statement 3, notice all prices in the initial state have the same value (Rule 1) and the current price and the price for unsold items are increased by the same amount in each turn (Rule 7 and 8). Assume $\text {M}_{sa}, \delta , t\models \lnot sold_j$. Since $\text {M}_{sa} \models sold_j\rightarrow \bigcirc sold_j$, there is no stage $t'<t$ such that $\text {M}_{sa}, \delta , t' \models sold_j$ and thus $\text {M}_{sa}, \delta , t\models price = price_j$.

Proposition 3

$\text {M}_{sa}\models \bigcirc wbb$ and $\text {M}_{sa}\not \models \bigcirc sbb$

Proof

Suppose a path $\updelta$ in $\text {M}_{sa}$ and a stage $t$ in $\updelta$. Note that each trade can be either 0 or 1 and the price for a good is at least 0, i.e., $\uppi _{\text {Y}}(\updelta [t], trade_{\mathsf {i},j}) \in \{0, 1\}$ and $\uppi _{\text {Y}}(\updelta [t], price_j) \in \text {I}_{\succeq 0}$. It follows from Rule 10 that $\text {M}_{sa}, \updelta , t\models payment_{\mathsf {i}} \ge 0$ for each agent $\mathsf {i}$ and $\text {M}_{sa}, \updelta , t\models \text {sum}_{\mathsf {i}\in \text {N}}(payment_\mathsf {i}) \ge 0$. Thus, $\text {M}_{sa} \models \bigcirc wbb$.

We will prove $\text {M}_{sa}$ is not strongly budget-balanced with a counter-example. Given an agent $\mathsf {i}$, let $\updelta$ be a path in $\text {M}_{sa}$ such that $\theta _\mathsf {i}(\updelta , 0) = (\mathsf {start}, 0, \dots , 0)$ and $\theta _\mathsf {s}(\updelta , 0) = (0, \dots , 0)$ for each agent $\mathsf {s}\ne \mathsf {i}$. Since $(\mathsf {start}, 0, \dots , 0) \in \text {L}(\updelta [0], \mathsf {i})$ and $(0, \dots , 0) \in \text {L}(\text {w}, \mathsf {s})$, there exists such path in $\text {M}_{sa}$. Since $\updelta [0] \not \in \text {T}$, $\uppi _{\text {Y}}(\updelta [0], price) = \uppi _{\text {Y}}(\updelta [0], price_j) = \mathsf {start}$ and $sold_j\not \in \uppi _{{\Upphi }}(\updelta [0])$ for each $j$, it follows from Rules 7 and 8, that all prices are increased by the constant $\mathsf {inc}>0$, that is $\text {M}_{sa}, \updelta , 1 \models price = \text {sum}(\mathsf {start}, \mathsf {inc}) \wedge \bigwedge _{j\in \text {G}} price_j= \text {sum}(\mathsf {start}, \mathsf {inc})$. By Rule 9, we have that agent $\mathsf {i}$ is only bidding for the good 1, that is, $\text {M}_{sa}, \updelta , 1 \models bid_{\mathsf {i},1} \wedge \bigwedge _{j\in \text {G}{\setminus }\{1\}} \lnot bid_{\mathsf {i}, j}$. All other agents are not bidding for any good, i.e., $\text {M}_{sa}, \updelta , 1 \models \bigwedge _{j\in \text {G}} \lnot bid_{\mathsf {s}, j}$, for each $\mathsf {s}\ne \mathsf {i}$. From Rules 4 and 10, we have $\text {M}_{sa}, \updelta , 1 \models trade_{\mathsf {i}, 1} =1 \wedge payment_\mathsf {i}= price_1 \wedge \bigwedge _{\mathsf {s}\in \text {N}{\setminus }\{\mathsf {i}\}}\text {p}_\mathsf {s}=0$. Since $\uppi _{\text {Y}}(\updelta [1], price_1) >0$, we have $\text {M}_{sa}, \updelta , 1 \not \models \text {sum}_{\mathsf {s}\in \text {N}}(payment_\mathsf {s}) =0$ and $\text {M}_{sa}\not \models \bigcirc sbb$.

Proposition 4

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$,

• 1. $\text {M}_{sa} \not \models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$

• 2. $\text {M}_{sa} \models does(\varvec{\upbeta }) \rightarrow \bigcirc (terminal\rightarrow e\textit{f}(\varvec{\upbeta }))$

Proof

Given a path $\delta$ in $\text {M}_{sa}$, we first consider Statement 1. We prove $\text {M}_{sa}$ is not efficient with a counter-example. Our purpose is to show that there exists a joint action $\varvec{\upbeta }$ such that $\text {M}_{sa}, \delta , 0 \models does(\varvec{\upbeta }) \wedge \lnot \bigcirc e\textit{f}(\varvec{\upbeta })$. That is, $\text {M}_{sa}, \delta , 0 \models does(\varvec{\upbeta }) \wedge \lnot \bigcirc \text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{(trade_{j})}_{j\in \text {G}})) = \max _{\varvec{\uplambda }\in \Uplambda }(\text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda })))$.

As we consider the initial state of $\delta$, $\text {M}_{sa}, \delta , 0 \models price = \mathsf {start} \wedge \bigwedge _{j\in \text {G}} price_j= \mathsf {start} \wedge \bigwedge _{\mathsf {i}\in \text {N}} (\lnot bid_{\mathsf {i}, j} \wedge trade_{\mathsf {i}, j} = 0)$. Thus, no good was sold, that is, $\text {M}_{sa}, \delta , 0 \models \bigwedge _{j\in \text {G}}\lnot sold_j$. Let $\mathsf {i}$ and $\mathsf {r}$ be two distinct agents in $\text {N}$ with $\mathsf {i}\ne \mathsf {r}$. From the definition of $\text {L}$, $\text {L}(\delta [0], \mathsf {i})= \text {L}(\delta [0], \mathsf {r})$ and $(p_1, \dots , p_\mathsf {m}) \in \text {L}(\delta [0], \mathsf {i})$ if $p_j= 0$ or $p_j= \text {sum}(\mathsf {start},\mathsf {inc})$ for each good $j$.

Let us assume $\text {M}_{sa}, \delta , 0 \models does(\varvec{\upbeta })$ for $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$ such that $\upbeta _\mathsf {i}=\upbeta _\mathsf {r}= (\mathsf {start}+\mathsf {inc}, 0, \dots , 0)$ and $\upbeta _\mathsf {s}=(0, \dots , 0)$ for each $\mathsf {s}\in \text {N}{\setminus }\{\mathsf {i}, \mathsf {r}\}$. Since $\upbeta _\mathsf {i}\in \text {L}(\delta [0], \mathsf {i})$, $\upbeta _\mathsf {r}\in \text {L}(\delta [0], \mathsf {r})$ and $\upbeta _\mathsf {s}\in \text {L}(\delta [0], \mathsf {s})$, there exists such path in $\text {M}_{sa}$. Thus, $\text {M}_{sa}, \delta , 1 \models bid_{\mathsf {i}, 1} \wedge bid_{\mathsf {r}, 1}$. Notice $bid_{\mathsf {i}', j}$ does not hold in $\delta [1]$ for any other pair $(\mathsf {i}', j) \ne (\mathsf {i}, 1)$ and $(\mathsf {i}', j) \ne (\mathsf {s}, 1)$. From Rules 4 and 5, we have $\text {M}_{sa}, \delta , 1 \models \bigwedge _{\mathsf {i}' \in \text {N}, j\in \text {G}} trade_{\mathsf {i}', j} = 0$.

Recall the valuation of each agent $\mathsf {i}'$ is $v_\mathsf {i}' ((p_1, \ldots , p_\mathsf {m}), \varvec{\uplambda }) = \sum _{j\in \text {G}} \uplambda _{\mathsf {i}', j} \cdot p_j$ for a trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$ and a bid $(p_1, \ldots , p_\mathsf {m}) \in \mathcal {B}$. Since each trade has the value 0 in $\delta [1]$, it follows that $\text {M}_{sa}, \delta , 1 \models \text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{(trade_{j})}_{j\in \text {G}})) =0$.

However, let $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$ be a trade such that $\uplambda _{\mathsf {i}, 1}=1$ and $\uplambda _{\mathsf {i}', j}=0$ for all other pair $(\mathsf {i}', j) \ne (\mathsf {i},1)$. It is easy to see that $\varvec{\uplambda }\in \Uplambda$. The value of this trade for $\mathsf {i}$ is $v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda }) = \mathsf {start}+\mathsf {inc}$ and $v_\mathsf {i}'(\upbeta _\mathsf {i}', \varvec{\uplambda }) = 0$ for each $\mathsf {i}'\ne \mathsf {i}$. Thus, we have $\sum _{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda })) = \mathsf {start}+\mathsf {inc}$, $\text {M}_{sa}, \delta , 1 \models \lnot \text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{(trade_{j})}_{j\in \text {G}})) =\max _{\varvec{\uplambda }\in \Uplambda }(\text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}$, $\varvec{\uplambda })))$ and $\text {M}_{sa}, \delta , 0 \models \lnot \bigcirc e\textit{f}(\varvec{\upbeta })$.

For Statement 2, let $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$ be a joint action and $t\ge 0$ be a stage of $\delta$. From the definition of $\text {M}_{sa}$ we have that each trade can be only 0 or 1. That is, if $\varvec{\uplambda }\in \Uplambda$ then $\uplambda _{\mathsf {i}, j} \in \{0,1\}$ for each agent $\mathsf {i}$ and good $j$. Assume $\text {M}_{sa} \models does(\varvec{\upbeta })$ and $\text {M}_{sa}, \delta , t\models \bigcirc terminal$. We intend to show that $\text {M}_{sa} \models \bigcirc e\textit{f}(\varvec{\upbeta })$, i.e., $\text {M}_{sa}, \delta , t\models \bigcirc \text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{(trade_{j})}_{j\in \text {G}})) = \max _{\varvec{\uplambda }\in \Uplambda }(\text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda }))))$.

We focus on the case where $\delta [t] \not \in \text {T}$. Let $\mathsf {i}$ be an agent in $\text {N}$ and let $(p_1, \dots , p_\mathsf {m})$ denote $\mathsf {i}$’s action in $\varvec{\upbeta }$. Recall function $v_{\mathsf {i}}((p_1, \dots , p_\mathsf {m}), \varvec{\uplambda }) = \sum _{j\in \text {G}} p_j\cdot \uplambda _{\mathsf {i}, j}$, for a trade $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$. Since the value for each good in $v_\mathsf {i}$ depends only on its reported value in $\mathsf {i}$’s bid and its trade for $\mathsf {i}$, we show that the part of $v_{\mathsf {i}}((p_1, \dots , p_\mathsf {m}), \varvec{\uplambda })$ corresponding to each good $j$ (i.e., $p_j\cdot \uplambda _{\mathsf {i},j}$) is maximized when $\uplambda _{\mathsf {i}, j} = \uppi _{\text {Y}}(\delta [t], trade_{\mathsf {i}, j})$.

From the definition of $\mathcal {B}$, we have that the reported value for $j$ in $\mathsf {i}$’s bid is at least zero, i.e., $p_j\ge 0$. We check for two cases:

• 1. If $p_j= 0$, then $\uplambda _{\mathsf {i}j}\cdot p_j= 0$, for any trade $\varvec{\uplambda }\in \Uplambda$. Thus, $\text {M}_{sa}, \delta , t+1 \models \text {times}(p_j, trade_{\mathsf {i}, j}) = \max ( \text {times}(p_j, 0), \text {times}(p_j, 1) )$;

• 2. If $p_j> 0$, then $\text {M}_{sa}, \delta , t+1 \models bid_{\mathsf {i}, j}$. Since $\delta [t+1]\in \text {T}$, it should be the case that $\text {M}_{sa}, \delta , t+1 \models sold_j$. From Rule 2, we know the trade for good $j$ is one for some agent, i.e., $\text {M}_{sa}, \delta , t+1 \models \bigvee _{\mathsf {r}\in \text {N}} trade_{\mathsf {r}, j} = 1$. Because $\text {M}_{sa}, \delta , t+1 \models bid_{\mathsf {i}, j}$, it should be the case that the agent who have a trade for $j$ is $\mathsf {i}$ (see Rules 4 and 5), that is, $\text {M}_{sa}, \delta , t+1 \models trade_{\mathsf {i}, j}=1$. Hence, $\text {M}_{sa}, \delta , t+1 \models \text {times}(p_j, 1) = \max (\text {times}(p_j, 0), \text {times}(p_j, 1))$.

It follows that

$$\begin{aligned}\text {M}_{sa}, \delta , t+1 \models \text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{(trade_{j})}_{j\in \text {G}})) = \max _{\varvec{\uplambda }\in \Uplambda }(\text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda }))))\end{aligned}$$

or simply, $\text {M}_{sa}, \delta , t\models \bigcirc ef(\varvec{\upbeta })$.

The case where $\delta [t] \in \text {T}$, follows from the loop on the path definition.

Proposition 5

$\text {M}_{sa}$ is strategyproof.

Proof

Given a path $\delta$ in $\text {M}_{sa}$ and a stage $t\ge 0$ in $\delta$, such that $\text {L}(\delta [t], \mathsf {i}) \approx _\mathsf {i}V_\mathsf {i}$. Let $\varvec{\vartheta } \in \prod _{\mathsf {i}\in \text {N}}V_\mathsf {i}$ be a preference profile and $\delta _{\varvec{\vartheta }}$ denote a path such that $\delta [0,t] = \delta _{\varvec{\vartheta }}[0,t]$ and $\theta (\delta _{\varvec{\vartheta }}, t) = \varvec{\upbeta _\vartheta }$. We let $\vartheta '_{\mathsf {i}} \in V_\mathsf {i}$ denote a preference of agent $\mathsf {i}$, $\varvec{\vartheta '} = (\vartheta _\mathsf {i}', \vartheta _{-\mathsf {i}})$ and $\delta _{\varvec{\vartheta '}}$ be a path such that $\delta [0,t] = \delta _{\varvec{\vartheta '}}[0,t]$, $\theta _\mathsf {i}(\delta _{\varvec{\vartheta '}}, t) = \upbeta _{\vartheta '_\mathsf {i}}$ and $\theta _\mathsf {r}(\delta _{\varvec{\vartheta '}}, t) = \upbeta _{\vartheta _\mathsf {r}}$ for each agent $\mathsf {r}\ne \mathsf {i}$.

In the stage $t$ of $\delta _{{\varvec{\vartheta }}}$, the agents report their (truthful) preferences $\varvec{\vartheta }$, i.e., $\text {M}_{sa}, \delta _{\varvec{\vartheta }}, t\models does(\varvec{\upbeta _\vartheta })$. On the other hand, in the stage $t$ of $\delta _{\varvec{\vartheta '}}$, the agent $\mathsf {i}$ reports her (untruthful) preference $\vartheta '_\mathsf {i}$ and each agent $\mathsf {r}\ne \mathsf {i}$ reports $\vartheta _\mathsf {r}$, i.e., $\text {M}_{sa}, \delta _{\varvec{\vartheta '}}, t\models does_\mathsf {i}(\upbeta _{\vartheta _\mathsf {r}'}) \wedge \bigwedge _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} does_\mathsf {r}(\upbeta _{\vartheta _\mathsf {r}})$.

For some $x\in \text {I}$, we have to show $\text {M}_{sa},\delta _{\varvec{\vartheta }}, t\models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}})$, $payment_\mathsf {i}) = x$ and $\text {M}_{sa},\delta _{\varvec{\vartheta '}}, t\models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {i}) \le x$.

That is, agent $\mathsf {i}$’s utility in $\delta _{\varvec{\vartheta '}}$ is not better than in $\delta _{\varvec{\vartheta }}$. Remind the legal actions in $\delta [t]$ represent her preference space, i.e., $\text {L}(\delta [t], \mathsf {i}) \approx _\mathsf {i}V_\mathsf {i}$. Notice the value of a bid $(p_1, \ldots , p_\mathsf {m})$ given a trade $\varvec{\uplambda }$ is $v_\mathsf {i}((p_1, \ldots , p_\mathsf {m}), \varvec{\uplambda }) = \sum _{j\in \text {G}} \uplambda _{\mathsf {i}, j} \cdot p_j$. Similarly, the payment in $\delta [t]$ is $\uppi _{\text {Y}}(\delta [t], payment_\mathsf {i}) = \sum _{j\in \text {G}} \uppi _{\text {Y}}(\delta [t], trade_{\mathsf {i}, j}) \cdot \uppi _{\text {Y}}(\delta [t], price_j)$. Since there is no dependence among goods in $v_\mathsf {i}$ and in $\mathsf {i}$’s payment, we consider the part of $\mathsf {i}$’s utility corresponding to $j$ in $\delta _{\varvec{\vartheta }}$ and $\delta _{\varvec{\vartheta '}}$. Thus, we need to show that

• (i) $\text {M}_{sa}, \delta _{\varvec{\vartheta }}, t\models \bigcirc \text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j), \text {times}(trade_{\mathsf {i}, j}, price_j)) = x_j$

• (ii) $\text {M}_{sa}, \delta _{\varvec{\vartheta '}}, t\models \bigcirc \text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j), \text {times}(trade_{\mathsf {i}, j}, price_j)) \le x_j$

for some $x_j\in \text {I}$ and each good $j\in \text {G}$.

We denote $\upbeta _{\vartheta _{\mathsf {i}}} = (p_1, \dots , p_\mathsf {m})$ and $\upbeta _{\vartheta '_{\mathsf {i}}} = (p_1', \dots , p_\mathsf {m}')$. According to the legality definition, the values of $p_j$ and $p_j'$ can be either the price of $j$ in $\delta [t]$, zero, or the price in $\delta [t]$ incremented by $\mathsf {inc}>0$. Let us consider each case:

• Assume $p_j= \uppi _{\text {Y}}(\delta [t],price_j)$ iff $\text {M}_{sa}, \delta , t\models trade_{\mathsf {i}, j} = 1$ (w.r.t the definition of $\text {L}$). That is, $p_j= \uppi _{\text {Y}}(\delta [t],price_j)$ when good $j$ was already bought by agent $\mathsf {i}$. Thus, it is not legal for $\mathsf {i}$ to bid any other value for $j$, i.e., $(p_1', \dots , p_j') \in \text {L}(\delta [t], \mathsf {i})$ iff $p_j= p_j'$. Thereby, it is easy to see that $\text {M}_{sa}, \delta _{\varvec{\vartheta }}, t\models \bigcirc \text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j), \text {times}(trade_{\mathsf {i}, j}, price_j)) = p_j$ and also $\text {M}_{sa}, \delta _{\varvec{\vartheta '}}, t\models \bigcirc \text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j), \text {times}(trade_{\mathsf {i}, j}, price_j))= p_j$.

• Assume agent $\mathsf {i}$ declines to raise her bid for good $j$, that is, $p_j= 0$. By Rules 5 and 9, we have $\text {M}_{sa}, \delta _{\varvec{\vartheta }}, t\models \bigcirc trade_{\mathsf {i}, j} = 0$ and $\text {M}_{sa}, \delta _{\varvec{\vartheta }}, t\models \bigcirc \text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j), \text {times}(trade_{\mathsf {i}, j}, price_j))= 0$. By the legality definition, it should be the case that $\text {M}_{sa}, \delta , t\models \lnot trade_{\mathsf {i}, j}=0$ and $p_j'$ is either 0 or $\uppi _{{\Upphi }}(\delta [t], price)+\mathsf {inc}$. If $p_j'=0$, then $\text {M}_{sa}, \delta _{\varvec{\vartheta '}}, t\models \bigcirc \text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j)$, $\text {times}(trade_{\mathsf {i}, j}, price_j))= 0$. Otherwise, the value of $trade_{\mathsf {i}, j}$ in $\delta _{\varvec{\vartheta '}}[t+1]$ will be either 0 or 1, depending on the joint bid $\varvec{\upbeta _{\vartheta '}}$.

  • If $\text {M}_{sa}, \delta _{\varvec{\vartheta '}}, t\models \bigcirc trade_{\mathsf {i}, j} = 1$, then $\text {M}_{sa}, \delta _{\varvec{\vartheta '}}, t\models \bigcirc \text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j)$, $\text {times}(trade_{\mathsf {i}, j}, price_j))= \text {sub}(0, price_j)$. Since $\uppi _{\text {Y}}(\delta _{\varvec{\vartheta '}}[t+1], price_j)\ge 0$, we have $\text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j)$, $\text {times}(trade_{\mathsf {i}, j}, price_j))\le 0$.

  • Otherwise, the trade for good $j$ is zero (i.e., $\text {M}_{sa}, \delta _{\varvec{\vartheta '}}, t\models \bigcirc trade_{\mathsf {i}, j} = 0$) and $\text {M}_{sa}, \delta _{\varvec{\vartheta '}}, t\models \bigcirc \text {sub}(\text {times}(trade_{\mathsf {i}, j}, p_j), \text {times}(trade_{\mathsf {i}, j}, price_j))= 0$.

• The proof for the case $p_j= \uppi _{\text {Y}}(\delta [t], price)+\mathsf {inc}$ is similar to the previous case.

It follows that $\text {M}_{sa},\delta _{\varvec{\vartheta }}, t\models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}})$, $payment_\mathsf {i}) = x$ and $\text {M}_{sa},\delta _{\varvec{\vartheta '}}, t\models \bigcirc \text {sub}(v_{\mathsf {i}}(\upbeta _{\vartheta _\mathsf {i}}, \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {i}) \le x$, where $x\in \text {I}$.

Lemma 2

For each agent $\mathsf {i}\in \text {N}$, each bid-tree $\upbeta \in \mathcal {L}_{\textsf {{TBBL}}}$ and each $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$, $v_\mathsf {i}(\text {noop}, \varvec{\uplambda }) = 0$.

Proof

Remind $\text {noop}$ denotes a leaf bid $\langle 0,j,0\rangle$, where $j\in \text {G}$. Thus, $b_\mathsf {i}(\text {noop}) = 0$. Let $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$. The value of $\varvec{\uplambda }$ given $\text {noop}$, i.e., $v_\mathsf {i}(\text {noop}, \varvec{\uplambda })$, is the maximal sum of $b_\mathsf {i}(\upbeta )\cdot \text {sat}_\mathsf {i}(\upbeta )$ in a solution $\text {sat}_\mathsf {i}$, for all $\upbeta \in \text {Node}(\text {noop})$. Since $\text {Node}(\text {noop}) = \{\text {noop}\}$ and $b_\mathsf {i}(\text {noop})=0$, for any solution $\text {sat}_\mathsf {i}$, $v_\mathsf {i}(\text {noop}, \varvec{\uplambda }) = 0$.

Lemma 3

$\text {M}_{vcg}$ is an ST-model and it is a model of $\Sigma _{vcg}$.

Proof

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

Let us verify Rule 1. Assume $\text {M}_{vcg}, \updelta , t \models initial$, then $\updelta [t]= \bar{\text {w}}$, i.e., $\updelta [t]= \langle 1, 0, \ldots , 0, 0, \ldots , 0 \rangle$. By the definitions of $\uppi _{\text {Y}}$ and $\uppi _{{\Upphi }}$, $\uppi _{{\Upphi }}(\bar{\text {w}}) = \{bidRound\}$, $\uppi _{\text {Y}}(\bar{\text {w}}, payment_\mathsf {i}) = 0$ and $\uppi _{\text {Y}}(\bar{\text {w}}, trade_{\mathsf {i},j}) = 0$ for all $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. Thus, $\text {M}_{vcg}, \updelta , t \models bidRound\wedge \bigwedge _{\mathsf {i}\in \text {N}} payment_\mathsf {i}= 0 \wedge \bigwedge _{j\in \text {G}} trade_{\mathsf {i},j} = 0$.

Now we verify Rule 4. Assume $\text {M}_{vcg}, \updelta , t \models initial$, then $\updelta [t]= \bar{\text {w}}$ and for all $\mathsf {i}\in \text {N}$ and $\upbeta \in \mathcal {B}$, $(\bar{\text {w}}, i, \upbeta ) \in \text {L}$. Thus, $\text {M}_{vcg}, \updelta , t \models legal_\mathsf {i}(\upbeta )$.

Then we consider Rule 5. $\text {M}_{vcg}, \updelta , t \models does(\varvec{\upbeta }) \wedge initial$, for $\varvec{\upbeta } \in \mathcal {B}^\mathsf {m}$, i.e., $\text {M}_{vcg}, \updelta , t \models \bigwedge _{\mathsf {i}\in \text {N}} does(\upbeta _\mathsf {i})$ and $\text {M}_{vcg}, \updelta , t \models initial$. Thus, $\uptheta _{\mathsf {i}} (\updelta , t) = \upbeta _\mathsf {i}$ for all $\mathsf {i}\in \text {N}$. The update function $\text {U}$ defines $\updelta [t+1]$ such that $\uppi _{\text {Y}}(\updelta [t+1], trade_{\mathsf {i},j}) = \text {WD}_{\uplambda _{\mathsf {i},j}}(\varvec{\upbeta }, \mathsf {X})$, for each $\mathsf {i}\in \text {N}$ and $j\in \text {G}$. Thus, $\text {M}_{vcg}, \updelta , t+1 \models \bigwedge _{\mathsf {i}\in \text {N}, j\in \text {G}} trade_{\mathsf {i},j} = \text {WD}_{\uplambda _{\mathsf {i},j}}(\varvec{\upbeta }, \mathsf {X})$ and also $\text {M}_{vcg}, \updelta , t \models \bigcirc (\bigwedge _{\mathsf {i}\in \text {N}, j\in \text {G}} trade_{\mathsf {i},j} = \text {WD}_{\uplambda _{\mathsf {i},j}}(\varvec{\upbeta }, \mathsf {X} ))$. Using the abbreviation, $\text {M}_{vcg}, \updelta$, $t \models \bigcirc (\bigwedge _{\mathsf {i}\in \text {N}} trade_\mathsf {i}= \text {WD}_{\uplambda _{\mathsf {i}}}(\varvec{\upbeta }$, $\mathsf {X} ))$.

The remaining rules are verified in a similar way.

Lemma 4

For each agent $\mathsf {i}\in \text {N}$, $\text {M}_{vcg} \models initial \wedge does_\mathsf {i}(\text {noop}) \rightarrow \bigcirc payment_\mathsf {i}= 0 \wedge \bigwedge _{j\in \text {G}} trade_{\mathsf {i}, j} \ge 0$

Proof

Straightforward from Lemma 2, Rule 6 from $\Sigma _{vcg}$ and Rule R2 from the definition of $b_\mathsf {i}$.

Proposition 6

$\text {M}_{vcg} \not \models \bigcirc sbb$ and $\text {M}_{vcg} \not \models \bigcirc wbb$.

Proof

We show $\text {M}_{vcg} \not \models \bigcirc wbb$ and $\text {M}_{vcg} \not \models \bigcirc sbb$ by showing a counter example. Given two distinct agents $\mathsf {i}, \mathsf {r}$ in $\text {N}$ and a good $j$ in $\text {G}$, let $\updelta$ be a path in $\text {M}_{vcg}$ such that $\theta _{\mathsf {i}}(\delta , 0) = \langle 1, j, 5 \rangle$ and $\theta _{\mathsf {r}}(\delta , 0) = \langle -1, j, -3 \rangle$. For any other agent $\mathsf {s}\in \text {N}{\setminus }\{\mathsf {i}, \mathsf {r}\}$, $\theta _{\mathsf {s}}(\delta , 0) = noop$. Since this actions are legal in the initial state $\delta [0]$, there exists such path.

By Rule 5 and the definition of function $\text {WD}_{\varvec{\uplambda }}$, we have that $\text {M}_{vcg}, \delta , 1 \models (trade_{\mathsf {i}, j} = 1 \wedge trade_{\mathsf {r}, j} = -1)$ and $\text {M}_{vcg}, \delta , 1 \models trade_{\mathsf {s}, j'} = 0$ for all pairs $(\mathsf {s}, j') \ne (\mathsf {i}, j)$ and $(\mathsf {s}, j') \ne (\mathsf {r}, j)$. That is, the good $j$ is sold by $\mathsf {r}$ and bought by $\mathsf {i}$. The social welfare of all agents other than $\mathsf {i}$ is $-3$ and the social welfare of all agents other than $\mathsf {r}$ is 5. If either $\mathsf {i}$ or $\mathsf {r}$ did not participate, there would be no trade and the social welfare would be zero. Thus, by Rule 6, the payments for $\mathsf {i}$ and $\mathsf {r}$ are 3 and $-5$, resp., that is, $\text {M}_{vcg}, \delta , 1 \models payment_{\mathsf {i}} = 3 \wedge payment_{\mathsf {r}} = -5$. The other agents’ do not have payments on $\delta [1]$, i.e., $\text {M}_{vcg}, \delta , 1 \models \bigwedge _{\mathsf {s}\in \text {N}{\setminus }\{\mathsf {i}, \mathsf {r}\}}payment_{\mathsf {s}} = 0$. Then, $\text {M}_{vcg}, \delta , 1 \models \text {sum}_{\mathsf {i}\in \text {N}}(payment_\mathsf {i}) <0$. Thus we have that $\text {M}_{vcg}, \delta , 0 \not \models \bigcirc sbb$ and $\text {M}_{vcg}, \delta , 0 \not \models \bigcirc wbb$.

Proposition 7

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, $\text {M}_{vcg} \models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$

Proof

(Sketch) Since $\text {M}_{vcg} \models initial \rightarrow \bigcirc terminal$ and $\updelta [t+1] = \updelta [t]$ whenever $\updelta [t]\in \text {T}$, it suffices to show that $\text {M}_{vcg}, \delta , 0 \models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$, for any joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$. Assume $\text {M}_{vcg}, \delta , 0 \models does(\varvec{\upbeta })$, by Rule 5 we have that $\text {M}_{vcg}, \delta , 1 \models \bigwedge _{\mathsf {i}\in \text {N}, j\in \text {G}} trade_{\mathsf {i}, j} = \text {WD}_{\uplambda _{\mathsf {i}, j}}( \varvec{\upbeta }, \mathsf {X})$. By the definition of the winner determination function $\text {WD}_{\varvec{\uplambda }}(\varvec{\upbeta },\mathsf {X})$ (and consequently function $\text {WD}_{\uplambda _{\mathsf {i}, j}}$ for each agent $\mathsf {i}$ and good $j$), we have that the trade $(\uppi _{\text {Y}}(\delta [1], trade_{\mathsf {i}, j}))_{j\in \text {G}, \mathsf {i}\in \text {N}}$ maximizes the cumulative value among the agents. That is, $\text {M}_{vcg}, \delta , 1 \models \text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}$, $\varvec{(trade_{j})}_{j\in \text {G}})) = \max _{\varvec{\uplambda }\in \Uplambda }(\text {sum}_{\mathsf {i}\in \text {N}}(v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda })))$ and $\text {M}_{vcg}, \delta , 0 \models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$.

Proposition 8

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, if $\vartheta _\mathsf {i}(\varvec{\uplambda }) \ge 0$ for all $\varvec{\uplambda }\in \text {I}^{\mathsf {n}\mathsf {m}}$, $\vartheta _\mathsf {i}\in V_\mathsf {i}$ and $\mathsf {i}\in \text {N}$, then $\text {M}_{vcg} \models does(\varvec{\upbeta }) \rightarrow \bigcirc ir(\varvec{\upbeta })$.

Proof

Let $\varvec{\upbeta }\in \mathcal {B}^\mathsf {n}$ be a joint action and $\delta$ be a path in $\text {M}_{vcg}$. Since $\text {M}_{vcg} \models initial \rightarrow \bigcirc terminal$ and $\updelta [t+1] = \updelta [t]$ whenever $\updelta [t]\in \text {T}$, it suffices to show that $\text {M}_{vcg}, \delta , 0 \models does(\varvec{\upbeta }) \rightarrow \bigcirc ir(\varvec{\upbeta })$. Assume $\text {M}_{vcg}, \delta , 0 \models does(\varvec{\upbeta })$ and that the preferences represented by $\text {L}(\delta [1], \mathsf {i})$ are non-negative for every agent and possible trade. That is, $v_{\mathsf {i}}(\upbeta , \varvec{\uplambda }) \ge 0$ for any bid $\upbeta$, trade $\varvec{\uplambda }$ and agent $\mathsf {i}$.

Let $\varvec{\uplambda }= \varvec{(\uplambda _{j})}_{j\in \text {G}}$ denote the trade performed after the agents report $\varvec{\upbeta }$, where $\uplambda _{\mathsf {i}, j} = \uppi _{\text {Y}}(\delta [1], trade_{\mathsf {i}, j}) = \text {WD}_{\uplambda _{\mathsf {i}, j}}(\varvec{\upbeta }, \mathsf {X})$ for each good $j$ and agent $\mathsf {i}$. We denote by $\varvec{\uplambda }^{-\mathsf {i}} = \text {WD}_{\varvec{\uplambda }}^{-\mathsf {i}}(\varvec{\upbeta }, \mathsf {X})$ the trade that would happen if $\mathsf {i}$ did not participate.

The utility of agent $\mathsf {i}$ in $\delta [1]$ is $u_\mathsf {i}= v(\upbeta _\mathsf {i}, \varvec{\uplambda })- \uppi _{\text {Y}}(\delta [1],payment_\mathsf {i})$. According to the payment definition (Rule 6), agent $\mathsf {i}$’s utility in $\delta [1]$ is

$$\begin{aligned}u_\mathsf {i}= v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda })- \big ( \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}}) - \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda })\big )\end{aligned}$$

or

$$\begin{aligned}u_\mathsf {i}= v_\mathsf {i}(\upbeta _\mathsf {i}, \varvec{\uplambda })- \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}}) + \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }) \end{aligned}$$

or simply

$$\begin{aligned}u_\mathsf {i}= \sum _{\mathsf {r}\in \text {N}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }) - \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}}) \end{aligned}$$

Thus, agent $\mathsf {i}$’s utility is non-negative if

$$\begin{aligned}\sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }) \ge \sum _{\mathsf {r}\in \text {N}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}}) \end{aligned}$$

Assume for contradiction that this is not the case, that is,

$$\begin{aligned}\sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}}) > \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda })\end{aligned}$$

Since $v_{\mathsf {r}}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}})\ge 0$, then we have

$$\begin{aligned}\sum _{\mathsf {r}\in \text {N}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}}) \ge \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda }^{-\mathsf {i}}) > \sum _{\mathsf {r}\in \text {N}{\setminus }\{\mathsf {i}\}} v_\mathsf {r}(\upbeta _\mathsf {r}, \varvec{\uplambda })\end{aligned}$$

which is a contradiction since $\varvec{\uplambda }$ is the efficient trade (see Proposition 7). Thus, $\text {M}_{vcg}, \delta , 1 \models \bigwedge _{\mathsf {r}\in \text {N}} \text {sub}(v_{\mathsf {r}}(\upbeta _\mathsf {r}, \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {r})\ge 0$ and $\text {M}_{vcg}, \delta , 0 \models \bigcirc ir(\varvec{\upbeta })$.

Lemma 5

$\text {M}_{ice}$ is an ST-model and it is a model of $\Sigma$.

Proof

The proof is similar to those for Lemmas 1 and 3.

Proposition 9

$\text {M}_{ice}\not \models \bigcirc sbb$ and $\text {M}_{ice} \models \bigcirc wbb$.

Proof

(Sketch) Considering strong budget-balance, notice the path $\delta$ illustrated at Fig. 7 is a counterexample. For instance, in the last stage we have $\text {M}_{ice}, \delta , 3 \models \text {sum}_{\mathsf {i}\in \text {N}} (payment_\mathsf {i})= 3$ and thus $\text {M}_{ice} \not \models \bigcirc \text {sum}_{\mathsf {i}\in \text {N}}(payment_\mathsf {i}) = 0$ and $\text {M}_{ice} \not \models \bigcirc sbb$.

Now we consider weak budget-balance. Let $\delta$ be a path in $\text {M}_{ice}$, $t\ge 0$ a stage in $\delta$ and $\mathsf {i}\in \text {N}$. By the definition of $v_\mathsf {i}$, we have that an empty trade is valuated zero, i.e., $v_\mathsf {i}(\theta _\mathsf {i}(\delta , 0), (0, \dots , 0)) = 0$. Thus, $\sum _{\mathsf {r}\in \text {N}}v_\mathsf {r}(\theta _\mathsf {r}(\delta , 0), (0, \dots , 0)) = 0$. Notice the empty trade $(0, \cdots , 0)$ satisfies Constraints C1–C4 from the winner determination. Among the trades satisfying those constraints, $\text {WD}^\varepsilon$ selects the trade $\varvec{(\uplambda _{j})}_{j\in \text {G}}$ that maximizes the cumulative value among all agents, Thus, the cumulative value cannot be smaller than zero. Since the agents’ pay the value of their bids, it follows that $\text {M}_{ice}, \delta , t\models \bigcirc \text {sub}_{\mathsf {i}\in \text {N}}(payment_\mathsf {i}) \ge 0$.

Proposition 10

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, $\text {M}_{ice}\models does(\varvec{\upbeta }) \rightarrow \bigcirc ir(\varvec{\upbeta })$.

Proof

The proof is straightforward since $\text {M}_{ice} \models does_\mathsf {i}(\upbeta _\mathsf {i}) \rightarrow \bigcirc payment_\mathsf {i}= v_\mathsf {i}(\upbeta _\mathsf {i}$, $\varvec{(trade_{j})}_{j\in \text {G}})$, for each $\mathsf {i}\in \text {N}$ and $\upbeta _\mathsf {i}\in \mathcal {B}$.

Proposition 11

Given a joint action $\varvec{\upbeta } \in \mathcal {B}^\mathsf {n}$, $\text {M}_{ice}\models does(\varvec{\upbeta }) \rightarrow \bigcirc e\textit{f}(\varvec{\upbeta })$

Proof

(Sketch) The proof is similar to the proof for Proposition 11.

Proposition 12

$\text {M}_{ice}$ is not strategyproof.

Proof

(Sketch) We show $\text {M}_{ice}$ is not strategyproof with a counterexample. Assume the path $\delta$ illustrated in Fig. 7 and consider stage 2. We have $\theta _\mathsf {s}(\delta , 2) = \langle 1, \mathsf {a}, 18, 18 \rangle$. Since the agents pay their reported valuation, in $\delta [3]$, the utility of agent $\mathsf {s}$ given her bid is zero, i.e., $\text {M}_{ice}, \delta , 3 \models \text {sub}(v_\mathsf {s}(\langle 1, \mathsf {a}, 18, 18 \rangle , \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {s}) = 0$. Let $\delta '$ be a path in $\text {M}_{ice}$ defined exactly like $\delta$, except by the actions performed by $\mathsf {s}$ in each stage $t\ge 2$, which is defined as $\theta _\mathsf {s}(\delta , t) = \langle 1, \mathsf {a}, 16, 16 \rangle$. Then, $\text {M},\delta ', 3 \models \bigcirc \text {sub}(v_{\mathsf {i}}(\langle 1, \mathsf {a}, 18, 18 \rangle , \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {s}) =2$ and $\text {M},\delta ', 3 \not \models \bigcirc \text {sub}(v_{\mathsf {s}}(\langle 1, \mathsf {a}, 18, 18 \rangle , \varvec{(trade_{j})}_{j\in \text {G}}), payment_\mathsf {s}) \le 0$.