Epistemic Reasoning About Rationality and Bids in Auctions

Abstract

In this paper, we investigate strategic reasoning in the context of auctions. More precisely, we establish an explicit link between bidding actions and bounded rationality. To do so, we extend the Auction Description Language with an epistemic operator and an action choice operator and use it to represent a classical auction where agents have imperfect information about other agents’ valuations. We formalize bounded rationality concepts in iterative protocols and show how to use them to reason about the players’ actions. Finally, we provide a model checking algorithm.

This research is supported by the ANR project AGAPE ANR-18-CE23-0013 and by the EU project TAILOR (EU Horizon 2020 program, GA No 952215).

1 Introduction

Building a General Auction Player is similar to the General Game Playing (GGP) challenge [9], it aims at designing an agent that can participate in an auction while discovering the rules governing it. As for games, there is a wide variety of auction-based markets. Auctions may differ in the participants’ type (e.g., only buyers, both buyers and sellers, ...), the kind and amount of goods being auctioned, the bidding protocol, and the allocation and payment rules [13].

Inspired by the Game Description Language (GDL), which is a logic programming language for representing and reasoning about game rules [9], we defined a general language to describe auction-based markets from the auctioneer perspective [15]: Auction Description Language (ADL). In this paper, we consider the player’s perspective and our goal is to show how an agent may reason about the rules governing an auction and also about their knowledge of other agents’ valuations for eliciting her bid. More precisely, we show that computing a rational bid requires to assume that other agents are also bidding rationally. Following [2], we understand ‘rational’ as ‘not playing dominated actions’.

Our contribution is twofold. We first extend ADL with knowledge operators from Epistemic GDL [12] and the action modality from the GDL variant proposed in [21]. This extension aims at providing the ground for the design of General Auction Players. Second, we characterize rationality along two dimensions: (i) the impact of the level of higher-order knowledge about other agents and (ii) the impact of looking-ahead beyond the next action to be executed. We also explore the complexity of model-checking for evaluating rationality.

Related Work. To the best of our knowledge, there is no contribution that focuses on the strategic dimension of auctions through a logical perspective. However, numerous contributions define logical systems for representing games and representing strategic reasoning. GGP uses the Game Description Language (GDL) [9] for representing games. The Auction Description Language (ADL) [15] extends GDL by handling numerical variables, a key feature for representing an auction mechanism with its allocation and payment rules.

Alternating-time Temporal Logic (ATL) [1] provides a logic-based analysis of strategic decisions. Strategy Logic (SL) generalizes ATL with first-order quantifications over strategies [4]. These approaches cannot model the internal structures of strategies, which makes it difficult to easily design strategies aiming to achieve a goal state. A logic for reasoning about composite strategies in turn-based games is introduced in [17], where strategies are treated as programs that are combined by PDL-like connectives. Zhang and Thielscher [22] present a variant of GDL to describe game strategies, where strategies can be understood as moves for a player. However, their work can only model turn-based games.

To incorporate imperfect information games, GDL has been extended to GDL-II [18] and GDL-III [19]. GDL-II and GDL-III aim at describing the rules of an imperfect information game, but do not provide tools for reasoning about how a player infers information based on these rules. All these logics face decidability and tractability issues: their expressive power prevents them from being implemented realistically in an artificial agent. Jiang et al. [12] propose an epistemic extension of GDL (EGDL) to represent and reason about imperfect information games. Their language allows us to represent the rules in the imperfect information setting. A key characteristic of EGDL is that it manages the balance between expressiveness and computational complexity of model checking ($\varDelta ^P_2$).

Epistemic Game Theory (EGT) considers strategic reasoning with uncertain information and is about the interplay between knowledge, belief and rationality [3, 14]. More precisely, EGT shows how dominated strategies may be eliminated in an iterative manner [2]. These contributions however require perfect reasoners, who can reason about higher-order knowledge at arbitrary depth, which is unrealistic. In [5], the authors abandon this hypothesis but do not propose a full logic detailing the impact of bounded rationality.

Structure of the Paper. The remainder of the paper proceeds as follows. In Sect. 2, we define the models of E-ADL in terms of State-Transition structures. In Sect. 3 we present the language and its semantics and illustrate our approach by describing a Dutch auction. In Sect. 4 we show how to express bounded rationality with higher-order knowledge. In Sect. 5 we present the model-checking algorithm. Section 6 concludes the paper.

2 Auctions as State-Transition Models

In this section, we introduce a logical framework for reasoning about auction protocols while considering imperfect information. The framework is based on ADL [15] and Epistemic GDL [11]. We call the framework Epistemic Auction Description Language, denoted by E-ADL.

Definition 1

An auction signature $\mathcal {S}$ is a tuple $(\mathrm{N}, \mathrm{V}, \mathcal {A}, \varPhi , \mathrm{Y})$, where: (i) $\mathrm{N}= \{1, 2, \cdots$, $n\}$ is a nonempty finite set of agents; (ii) $\mathrm{V}\subset \mathbb Z$ is a finite subset of integer numbers representing the range of valuations, bids and payments; (iii) $\mathcal {A}= \bigcup _{r\in \mathrm{N}} \mathrm{A}^{r}$, where each $\mathrm{A}^{r}$ consists of a nonempty finite set of actions performed by agent $r\in \mathrm{N}$ and $\mathrm{A}^{r} \cap \mathrm{A}^{s} = \emptyset$ if $r\ne s$. For convenience, we may write $a^{r}$ for denoting an action in $\mathrm{A}^{r}$; (iv) $\varPhi = \{p, q, \cdots \}$ is a finite set of atomic propositions for specifying individual features of a state; (v) $\mathrm{Y}= \{ y_1, y_2, \cdots \}$ is a finite set of numerical variables for specifying numerical features of a state.

We assume a total order among the agents in $\mathrm{N}$, denoted by $\prec$, where $r \prec i$ means that agent $r$ precedes agent i in $\prec$; it will be used to break ties in winner determination. Throughout the rest of the paper, we fix an auction signature $\mathcal {S}$ and all concepts will be based on this signature, except if stated otherwise. We adopt a semantics based on state-transition models. This is more suitable for describing the dynamics than stable models that were initially considered for GDL and GGP [9].

Definition 2

A state transition ST-model $\mathrm{M}$ is a tuple $(\mathrm{W}, \mathrm{I}, \mathrm{T}, \{\mathrm{R}_{r}\}_{r\in \mathrm{N}}, \mathrm{U}, \pi _{\varPhi }, \pi _{\mathrm{Y}})$, where: (i) $\mathrm{W}$ is a finite nonempty set of states; (ii) $\mathrm{I}\subseteq \mathrm{W}$ is a set of initial states; (iii) $\mathrm{T}\subseteq \mathrm{W}\setminus \mathrm{I}$ is a set of terminal states; (iv) $\mathrm{R}_{r} \subseteq \mathrm{W}\times \mathrm{W}$ is an equivalence relation for agent $r$, indicating the states that are indistinguishable for $r$; (v) $\mathrm{U}: \mathrm{W}\times (\prod _{r \in \mathrm{N}} \mathrm{A}^{r} ) \rightarrow \mathrm{W}$ is an update function, specifying the transitions for each combination of joint actions; (vi) $\pi _{\varPhi }: \mathrm{W}\rightarrow 2^\varPhi$ is the valuation function for the state propositions; and (vii) $\pi _{\mathrm{Y}}: \mathrm{W}\times \mathrm{Y}\rightarrow \mathrm{V}$ is the valuation function for the numerical variables.

For a group of agents ${G}\in 2^{\mathrm{N}}\setminus \{\emptyset \}$, we write $d^{{G}} \in \prod _{r\in {G}} \mathrm{A}^{r}$ to denote a joint action of the agents in ${G}$. We denote by $d^{r}$ the individual action for agent $r\in {G}$ in the joint action $d^{{G}}$. When ${G}= \mathrm{N}$ then we omit $\mathrm{N}$ and simply write $d$ instead of $d^{\mathrm{N}}$. Let $\mathrm{R}_{r}(w)$ denote the set of all states that agent $r$ cannot distinguish from $w$, i.e., $\mathrm{R}_{r}(w) = \{u\in \mathrm{W}: w\mathrm{R}_{r} u\}$.

For every $w\in \mathrm{W}$ and $d\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$, we call $(w, d)$ a move. Given a group of agents ${G}\in 2^{\mathrm{N}}\setminus \{\emptyset \}$, we write $(w, \langle d^{{G}}, d^{\text {-}{G}}\rangle )$ instead of $(w, d)$ when we want to talk about ${G}$’s part in $(w, d)$, where $d^{\text {-}{G}} \in \prod _{s\in \mathrm{N}\setminus {G}} \mathrm{A}^{s}$ denotes the actions of all the agents except those in ${G}$ in the joint action $d$. Our notion of move resembles the turn-based definition proposed in [21] and [22].

Definition 3

Two moves $(w, d)$ and $(u, e)$ are equivalent for agent $r$, written $(w, d) \approx _r(u, e)$, iff $w\mathrm{R}_{r} u$ and $d^{r} = e^{r}$.

Clearly relation $\approx _r$ is reflexive, transitive and symmetric. Differently from standard GDL, our semantics is based on moves instead of paths. This allows the agent to reason about the effects of actions without exploring all ways the game could proceed (i.e., all the reachable states in each complete path where she takes this action). In E-ADL, we define the action execution modality in games with synchronous moves. The idea of move-based semantics and action modalities stems from [21]. Their approach is restricted to turn-based games, where only one action can be performed at a given state.

3 Epistemic Auction Description Language

The Epistemic Auction Description Language (E-ADL) is a framework to allow epistemic reasoning for auction players. First, we introduce the syntax.

3.1 Syntax

Let $z \in \mathcal {L}_{z}$ be a numerical term defined as follows: $z\,{::=}\,t \mid add(z, z) \mid sub(z,z) \mid min(z,z) \mid max(z,z) \mid times(z,z) \mid y$, where $t \in \mathrm{V}$, $y\in Y$. The meaning of numerical terms is the natural one; for instance, the term $min(z_1$, $z_2)$ specifies the minimum value between $z_1$ and $z_2$. Finally, y denotes the value of the variable $y \in \mathrm{Y}$ in the current state.

A formula in E-ADL, denoted $\varphi \in \mathcal {L}_{\text {E-ADL}}$, is defined by the following BNF:

$$\begin{aligned} \varphi \,{::=}\,p \mid z \otimes z \mid r \prec r \mid initial\mid terminal\mid does(a^{r}) \mid \lnot \varphi \mid \varphi \wedge \varphi \mid \mathsf {K}_{r} \varphi \mid [\,d^{{G}}\,]\varphi \end{aligned}$$

where $p \in \varPhi$, $r\in \mathrm{N}$, $\otimes \in \{>,<,=\}$, $a^{r} \in \mathcal {A}$, ${G}\in 2^{\mathrm{N}}\setminus \{\emptyset \}$, $d^{{G}}\in \prod _{r\in {G}} \mathrm{A}^{r}$ and $z \in \mathcal {L}_{z}$. Other connectives $\vee , \rightarrow , \leftrightarrow , \top$ and $\bot$ are defined by $\lnot$ and $\wedge$ in the standard way. The comparison operators $\le$, $\ge$ and $\ne$ are defined by $\vee , >, <$ and $=$. The extension of the operators $>,<$ and $=$ and numerical terms $max(z_1, z_2), min(z_1, z_2)$, $add(z_1, z_2)$ to multiple arguments is straightforward. The formula $r_1 \prec r_2$ denotes the tie-breaking priority of $r_1$ over $r_2$.

Intuitively, $initial$ and $terminal$ specify the initial and the terminal states, respectively; $does(a^{r})$ asserts that agent $r$ takes action $a^{r}$ at the current move. The epistemic operator $\mathsf {K}_{r}$ is taken from the Epistemic Logic [7]. The formula $\mathsf {K}_{r} \varphi$ is read as “agent $r$ knows that $\varphi$”. The action execution operator comes from the GDL variant with action modalities [21] and the formula $[\,d^{{G}}\,]\varphi$ means that if joint action $d^{{G}}$ is executed, $\varphi$ will be true next. The abbreviation $does(d^{{G}})$ specifies that each agent in ${G}$ performs her respective action in $d^{{G}}$, that is, . As in [21], we use the action modality to define the temporal operator $\bigcirc$:

$$\begin{aligned} \bigcirc \varphi =_{def} \bigvee _{d\in \prod _{r\in \mathrm{N}}\mathrm{A}^{r}} \left( does(d) \wedge [\,d\,]\varphi \right) \end{aligned}$$

The formula $\bigcirc \varphi$ reads “$\varphi$ will be true next”. We also use the following abbreviation from Epistemic Logic: $\widehat{\mathsf {K}}_{r} \varphi =_{def} \lnot \mathsf {K}_{r} \lnot \varphi$ where $\widehat{\mathsf {K}}_{r} \varphi$ represents that “$\varphi$ is compatible with agent $r$’s knowledge”. Given $j>0$ and ${G}\in 2^\mathrm{N}\setminus \{\emptyset \}$, we write $\sigma ^{{G}} = (\prod _{r\in {G}} \mathrm{A}^{r})^{j}$ for a sequence of joint actions for ${G}$. The i-th joint action in $\sigma ^{{G}}$ is noted $\sigma ^{{G}}_i$. Finally, define $[\,\sigma ^{{G}}\,]^{j}\, \varphi$, for $|\sigma ^{{G}}| = j$ by induction of $j$:

The formula $[\,\sigma ^{{G}}\,]^{j}\, \varphi$ means that if the group ${G}$ followed the sequence of joint actions described by $\sigma ^{{G}}$ for the next $j$ stages, then $\varphi$ would hold.

3.2 Semantics

The semantics for E-ADL is given in two steps. First, function f interprets the meaning of numerical terms $z \in \mathcal {L}_{z}$. Next, a formula $\varphi \in \mathcal {L}_{\text {E-ADL}}$ is interpreted with respect to a move. In Definition 4, we specify function f to evaluate the meaning of any $z \in \mathcal {L}_{z}$ in a move.

Definition 4

Let $\mathrm{M}$ be an ST-Model. Define Function $f: W \times (\prod _{r \in \mathrm{N}} \mathrm{A}^{r} ) \times \mathcal {L}_{z}\rightarrow \mathbb Z$, assigning any $w\in \mathrm{W}$, $d\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$, and $z \in \mathcal {L}_{z}$ to a number in $\mathbb Z$:

If z is on the form $add(z', z'')$, $sub(z', z'')$, $min(z', z'')$, $max(z', z'')$ or $times(z'$, $z'')$, then $f(w, d, z)$ is defined through the application of the corresponding mathematical operators and functions over $f(w, d, z')$ and $f(w, d, z'')$. Otherwise, $f(w, d, z) = z$ if $z\in \mathrm{V}$ and $f(w, d, z) = \pi _{Y}(w, z)$ if $z \in Y$.

Definition 5

Let $\mathrm{M}$ be an ST-Model. Given a move $(w, d)$, where $w\in \mathrm{W}$ and $d\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$, and a formula $\varphi \in \mathcal {L}_{ADL}$, we say that $\varphi$ is true in the move $(w, d)$ under M, denoted by $M \models _{(w, d)} \varphi$, according to the following rules:

A formula $\varphi$ is globally true in an ST-Model $\mathrm{M}$, written $\mathrm{M}\models \varphi$, if $\mathrm{M}\models _{(w, d)}\varphi$ for all $w\in \mathrm{W}$ and $d\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$. Finally, let $\varSigma$ be a set of formulas in $\mathcal {L}_{\text {E-ADL}}$, then M is a model of $\varSigma$ if $M \models \varphi$ for all $\varphi \in \varSigma$.

Each $\mathsf {K}_{r}$ is a normal modal operator. It satisfies that if all $r$-accessible worlds agree on $\varphi$ then $r$ knows either $\varphi$ or $\lnot \varphi$. If $\varphi$ is true then $r$ knows that $\varphi$.

Proposition 1

Let $\mathrm{M}$ be an ST-Model, $r\in \mathrm{N}$ be an agent and $\varphi \in \mathcal {L}_{\text {E-ADL}}$ be a formula, then $\mathrm{M}\models \varphi \rightarrow \mathsf {K}_{r} \varphi$ if and only if for all $w, u\in \mathrm{W}$ and all $d, e\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$ such that $(w, d) \approx _r(u, e)$, $\mathrm{M}\models _{(w, d)}\varphi$ iff $\mathrm{M}\models _{(u, e)}\varphi$.

It follows from the equivalence relation $\approx _r$ that agent $r$ knows the actions she performs. This is similar to the uniform strategies in Alternating-time Temporal Epistemic Logic [10] and Dynamic Epistemic Logic [20].

Proposition 2

For any agent $r\in \mathrm{N}$, action $a^{r} \in \mathrm{A}^{r}$, formula $\varphi \in \mathcal {L}_{\text {E-ADL}}$, number of steps $j>0$, group of agents ${G}\in 2^{\mathrm{N}}\setminus \{\emptyset \}$ and $\sigma ^{r} \in (\prod _{r\in {G}} \mathrm{A}^{r})^{j}$:

• 1. $\mathrm{M}\models does(a^{r})\rightarrow \mathsf {K}_{r} does(a^{r})$

• 2. If $\mathrm{M}\models [\,\sigma ^{{G}}\,]^{j}\,\varphi$ then $\mathrm{M}\models \mathsf {K}_{r} [\,\sigma ^{{G}}\,]^{j}\,\varphi$

• 3. If $\mathrm{M}\models [\,\sigma ^{{G}}\,]^{j} \mathsf {K}_{r} \varphi$ then $\mathrm{M}\models \mathsf {K}_{r} [\,\sigma ^{{G}}\,]^{j} \varphi$

Let us now illustrate how to represent an auction-based protocol in E-ADL, namely, a Dutch auction. First, we show the syntactical representation through E-ADL-formulas. Later, we address the semantical representation.

3.3 Running Example: Dutch Auction

In a Dutch auction, the auctioneer starts by proposing a high asking price. The price is decreased until it reaches a predefined reserve price or some bidder shows interest at purchasing the good. The auction then ends and the object is sold at the given price to the bidder who signaled her interest [13].

Let $\mathcal {S}_{\text {dut}}$ be an auction signature and $\mathsf {starting}, \mathsf {reserve}\in \mathbb N$, $\mathsf {dec}, \mathsf {n}\in \mathbb N\setminus \{0\}$ be constant values. The constants $\mathsf {starting}, \mathsf {reserve}$, $\mathsf {dec}, \mathsf {n}$ represent the starting and reserve prices, the decrement in each round and the number of agents, respectively. The auction signature is defined as follows: $\mathcal {S}_{\text {dut}}= (\mathrm{N}_{\text {dut}}, \mathrm{V}_{\text {dut}}, \mathcal {A}_{\text {dut}}, \varPhi _{\text {dut}}, \mathrm{Y}_{\text {dut}})$, where $\mathrm{N}_{\text {dut}}= \{1, \dots , \mathsf {n}\}$, $\mathrm{V}_{\text {dut}} = \{0, \dots , \mathsf {starting}\}$, $\mathcal {A}_{\text {dut}}= \{\text {bid}_{r}, \text {wait}_{r}: r\in \mathrm{N}_{\text {dut}}\}$, $\varPhi _{\text {dut}}= \{winner_{r} : r\in \mathrm{N}\}$ and $\mathrm{Y}_{\text {dut}}= \{\text {payment}_{r}, \vartheta _r: r\in \mathrm{N}\}$. The numerical variables $\text {payment}_{r}$ and $\vartheta _r$ specify the payment and the private valuation for an agent $r$.

Syntactical Representation. The rules of the Dutch auction are formulated by E-ADL-formulas as shown in Fig. 1.

Fig. 1.

Dutch auction represented by $\varSigma _{\text {dut}}$

In an initial state, the price starts at $\mathsf {starting}$ and there is no winner (Rule 1). If an agent is a winner, she pays the current price. Otherwise, she does not pay anything (Rules 2 and 3). The terminal state is reached when it is not possible to decrease the price anymore or there is a winner (Rule 4). While not in the terminal state, the price either decreases if no agent bids or the price is settled if some agent accepted to purchase the good (Rules 5 and 6). If only one agent accepts, she is marked as the winner. In case two or more agents bid, the winner is assigned according to the tie-breaking rule. Rules 7 and 8 ensure no proposition or numerical variable change its value after a terminal state. Finally, Rule 9 specifies that each agent is aware of how much she valuates the good. Let $\varSigma _{\text {dut}}$ be the set of Rules 1–9.

Model Representation. Let us address the model representation of the Dutch auction. Let us define $\mathcal {M}_{\text {dut}}$ as the class of models $\mathrm{M}_{\text {dut}}$ defined for a signature $\mathcal {S}_{\text {dut}}$ and the constants $\mathsf {starting}, \mathsf {reserve}, \mathsf {dec}$ and $\mathsf {n}$. Each $\mathrm{M}_{\text {dut}}= (\mathrm{W}_{\text {dut}}, \mathrm{I}_{\text {dut}}, \mathrm{T}_{\text {dut}}, \{\mathrm{R}_{r, \text {dut}}\}_{r\in \mathrm{N}}, \mathrm{U}_{\text {dut}}, \pi _{\varPhi , \text {dut}}, \pi _{\mathrm{Y}, \text {dut}})$ is defined as follows:

• $\mathrm{W}_{\text {dut}}= \{\langle \text {pr}, \text {buyer}, \text {val}_{1}, \dots , \text {val}_{\mathsf {n}}\rangle :0 \le \text {pr}\le \mathsf {starting}$ & $\text {buyer}\in \mathrm{N}_{\text {dut}}\cup \{none\}$ & $0 \le \text {val}_{r} \le \mathsf {starting}$ for each $r\in \mathrm{N}_{\text {dut}}\}$;

• $\mathrm{I}_{\text {dut}}= \{\langle \mathsf {starting}, none, \text {val}_{1}, \dots , \text {val}_{\mathsf {n}}\rangle : 0\le \text {val}_{r} \le \mathsf {starting}$ for each $r\in \mathrm{N}_{\text {dut}}\}$;

• $\mathrm{T}_{\text {dut}}= \{\langle \text {pr}, \text {buyer}, \text {val}_{1}, \dots , \text {val}_{\mathsf {n}}\rangle :0 \le \text {pr}\le \mathsf {starting}$ & $\text {buyer}\in \mathrm{N}_{\text {dut}}$ & $0 \le \text {val}_{r} \le \mathsf {starting}$ for each $r\in \mathrm{N}_{\text {dut}}\} \cup \{\langle \text {pr}, \text {buyer}, \text {val}_{1}, \dots , \text {val}_{\mathsf {n}}\rangle :\text {pr}-\mathsf {dec}<\mathsf {reserve}$ & $\text {buyer}\in \mathrm{N}_{\text {dut}}\cup \{none\}$ & $0 \le \text {val}_{r} \le \mathsf {starting}$ for each $r\in \mathrm{N}_{\text {dut}}\}$;

• For each agent $r\in \mathrm{N}_{\text {dut}}$ and for any two states $w= \langle \text {pr}, \text {buyer}, \text {val}_{1}, \dots , \text {val}_{\mathsf {n}}\rangle$ and $u= \langle \text {pr}', \text {buyer}', \text {val}_{1}', \dots , \text {val}_{\mathsf {n}}' \rangle$ in $\mathrm{W}_{\text {dut}}$, the relation $\mathrm{R}_{r, \text {dut}}$ is defined as follows: $w\mathrm{R}_{r, \text {dut}} u$ iff (i) $\text {pr}= \text {pr}'$; (ii) $\text {buyer}= \text {buyer}'$; and (iii) $\text {val}_{r} = \text {val}_{r}'$.

• For all states $w= \langle \text {pr}, \text {buyer}, \text {val}_{1}, \dots , \text {val}_{\mathsf {n}}\rangle$ and all joint actions $d= (a^{r})_{r\in \mathrm{N}_{\text {dut}}}$, such that $w\in \mathrm{W}_{\text {dut}}$ and $a^{r} \in \{\text {bid}_{r}, \text {wait}_{r}\}$, we define $\mathrm{U}_{\text {dut}}$ as follows:

  • If $w\not \in \mathrm{T}_{\text {dut}}$, then $\mathrm{U}_{\text {dut}}(w, d) = \langle \text {pr}', \text {buyer}', \text {val}_{1}, \dots , \text {val}_{\mathsf {n}}\rangle$, such that the components $\text {pr}'$ and $\text {buyer}'$ are defined as follows: (i) $\text {pr}' = \text {pr}-\mathsf {dec}$ if $a^{r} = \text {wait}_{r}$, for all $r\in \mathrm{N}_{\text {dut}}$; otherwise $\text {pr}' = \text {pr}$; (ii) $\text {buyer}' = r$ if $a^{r} = \text {bid}_{r}$ for some $r\in \mathrm{N}$ and for all $s\in \mathrm{N}_{\text {dut}}$ such that $s\ne r$, either $a^{s}= \text {wait}_{s}$ or $r \prec s$; otherwise, $\text {buyer}' = none$;

  • Otherwise, $\mathrm{U}_{\text {dut}}(w, d) = w$.

• Finally, for each state $w= \langle \text {pr}, \text {buyer}, \text {val}_{1}, \dots , \text {val}_{\mathsf {n}}\rangle$, such that $w\in \mathrm{W}_{\text {dut}}$, let $\pi _{\varPhi , \text {dut}}(w) = \{winner_{r}: \text {buyer}= r$ & $r\in \mathrm{N}_{\text {dut}}\}$; $\pi _{\mathrm{Y}, \text {dut}}(w, \text {price}) = \text {pr}$. For each agent $r\in \mathrm{N}_{\text {dut}}$, let $\pi _{\mathrm{Y}, \text {dut}}(w, \vartheta _{r}) = \text {val}_{r}$ and $\pi _{\mathrm{Y}, \text {dut}}(w, \text {payment}_{r}) = \text {pr}$ if $\text {buyer}= r$. Otherwise, $\pi _{\mathrm{Y}, \text {dut}}(w, \text {payment}_{r}) = 0$.

Let us assume a model $\mathrm{M}_{\text {dut}}\in \mathcal {M}_{\text {dut}}$ and $\varSigma _{\text {dut}}$ for some $\mathcal {S}_{\text {dut}}$ and the constants $\mathsf {starting}, \mathsf {reserve}\in \mathbb N$, $\mathsf {dec}, \mathsf {n}\in \mathbb N\setminus \{0\}$.

Proposition 3

$\mathrm{M}_{\text {dut}}$ is an ST-Model and $\mathrm{M}_{\text {dut}}\models \varSigma _{\text {dut}}$, i.e., $\mathrm{M}_{\text {dut}}$ is a model of $\varSigma _{\text {dut}}$.

That is, $\mathrm{M}_{\text {dut}}$ is a sound representation of $\varSigma _{\text {dut}}$. Notice that as $\mathrm{M}_{\text {dut}}$ is not the unique model for $\varSigma _{\text {dut}}$, thereby, the completeness does not hold. It follows from Proposition 1 and 3 that each agent knows the auction rules denoted by $\varSigma _{\text {dut}}$, that is, $\mathrm{M}_{\text {dut}}\models \bigwedge _{r\in \mathrm{N}} (\mathsf {K}_{r} \varSigma _{\text {dut}})$. In the next section, we define rationality in E-ADL.

4 Rationality in Auctions

To characterize rationality of auction players, we assume $\{ \vartheta _{r}, payment_{r}: r\in \mathrm{N}\} \subseteq Y$ and $\{winner_{r}: r\in \mathrm{N}\} \subseteq \varPhi$, where $\vartheta _{r}, payment_{r}$ and $winner_{r}$ specify the agents valuation, payment and whether she won the auction, resp. Let $ut \in \mathrm{V}$, we denote whether the utility of agent $r\in \mathrm{N}$ is equal to ut in a single good and unit auction according to the truth value of the following formula:

Note that we can extend the notion of utility to multiple units and goods by including numerical variables representing the agents’ allocations and their valuations for such allocations. In this work, we focus on epistemic reasoning about action choice and rationality of auction players. For a discussion on expressivity and hierarchy of valuations functions, the reader may refer to Feige et al. [8].

Similar to the strong strategy dominance (see [14]), we say an action $a^{r}$ of an agent $r$ is a strongly dominated action if and only if, there exists another action $b^{r}$ of $r$ such that, for all actions $a^{-r}$ of the other agents, playing $b^{r}$ while others play $a^{-r}$ leads to a better utility than playing $a^{r}$ while others play $a^{-r}$. In E-ADL, the agents’ utility is captured in a move of a model and the action choice operator allows us to compare what would have happened if a group of agents took a given joint action.

4.1 Rationality

We adapt the weak rationality formalization from [14] to E-ADL formulas. Different from his approach, we consider levels of rationality instead of common knowledge. Our notion of $k$-order rationality is based on [6]: an agent is $k$-order rational if she is weakly rational and knows all agents are $(k-1)$-order rational.

GDL-based languages explicit the stages of a game execution through paths (or runs). The game starts from an initial state and the succeeding states are defined according to the agents’ joint actions. Since GDL agents choose “on-the-fly strategies” during the game, the players should be able to evaluate the current state of the game and to decide which action they will execute.

Adopting these features from GDL in E-ADL allows us to explicitly model information feedback, which is a key feature in the design of iterative auctions [16]. For instance, in E-ADL, we can describe auctions where the agents are assigned to allocations and payments at any stage, which may be different from their final assignments in the terminal state. For this reason, instead of defining utilities as a function to strategy profiles as in ATL [1], we model the agents’ utility as being dependent on the current state of the auction.

We refrase the rationality notions from [6, 14] by, at first, considering $k$-order of knowledge and, second, by taking into account state-based utilities and exploring bounded sequences of actions. A rational agent plays according to her utility after performing an action. When reasoning about iterative auctions, the agent considers her utility after playing according to a sequence of j actions. Since most auction-based markets are finite (in the sense that the auction finishes eventually), it is reasonable to assume the agents only need to include in their reasoning which actions may occur in the next j steps. Given a fixed number of steps $j >0$, we inductively define that an agent is $k$-order rational, for $k\le j$. The base case is that any agent is 0-order rational, that is, . For all $k> 0$, we define:

That is, an agent is $(k+1)$-order rational if she is weakly rational when looking $j$ stages ahead and knows every other agent is k rational. Weak rationality is defined by:

where

$$\begin{aligned}&\text {WRAction}(r, \sigma ^{r}, j) =_{def} \bigwedge _{\chi ^{r}\in (\mathrm{A}^{r})^j} \Big ( \bigvee _{\sigma ^{\text {-}r} \in (\prod _{s\ne r} \mathrm{A}^{s})^j} \big ( \widehat{\mathsf {K}}_{r} does(\sigma ^{\text {-}r}_1) \, \wedge \\&\quad \,\,\bigvee _{ut, ut' \in \mathrm{V}} ( [\,\chi ^{r}, \sigma ^{\text {-}r}\,]^{j}\, utility_r= ut' \wedge [\,\sigma ^{r}, \sigma ^{\text {-}r}\,]^{j}\, utility_r= ut \wedge ut' \le ut ) \big ) \Big ) \end{aligned}$$

An agent $a^{r}$ is weakly rational when reasoning $j$ stages ahead if when she performs an action $a^{r}$, there exists a sequence of $j$ actions starting by $a^{r}$ that is weakly rational for her to follow over $j$ stages. Finally, it is weakly rational for agent $r$ to follow a sequence of actions $\sigma ^{r}$ for $j$ steps, noted $\text {WRAction}(r, \sigma ^{r}, j)$, if for every other sequence of actions $\chi ^{r}$ there exists a sequence of joint actions $\sigma ^{\text {-}r}$ that $r$ considers possible to be executed such that her utility after following $\sigma ^{r}$ for $j$ steps is at least as good as her utility after following $\chi ^{r}$.

Notice that if $j$ is large enough to reach terminal states, the state-based utilities represent strategy-based utility functions. Our definition of rationality requires to assume that all agents are rational: as soon as one is known to be non-rational, it is no longer possible to be $k$-order rational, for $k>1$. This requirement entails that looking ahead without considering knowledge leads to consider all actions as rational:

Proposition 4

For every ST-Model $\mathrm{M}$, state $w\in \mathrm{W}$, joint action $d\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$, agent $r\in \mathrm{N}$ and $j>0$, it holds that $\mathrm{M}\models _{(w, d)} does(d^r) \wedge \mathrm{Rat}(r, 0, j)$.

Next, considering higher-order knowledge enables us to eliminate strongly dominated actions.

Theorem 1

For any ST-Model $\mathrm{M}$, state $w\in \mathrm{W}$, joint action $d\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$, $k> 0$, $j> 0$, agent $r\in \mathrm{N}$ and action $a^{r} \in \mathrm{A}^{r}$, if $\mathrm{M}\models _{(w, d)}does(a^{r}) \wedge \mathrm{Rat}(r, k, j)$ then $\mathrm{M}\models _{(w, d)}does(a^{r}) \wedge \mathrm{Rat}(r, k- 1, j)$.

Proof

Assume $\mathrm{M}\models _{(w, d)}does(a^{r}) \wedge \mathrm{Rat}(r, k, j)$. Thus, $\mathrm{M}\models _{(w, d)}does(a^{r}) \wedge \text {WR}(r, j) \wedge \mathsf {K}_{r}(\bigwedge _{s\in \mathrm{N}} \mathrm{Rat}(s, k-1, j))$. Since $\mathrm{R}_{r}$ is reflexive, it follows that $\mathrm{M}\models _{(w, d)}does(a^{r}) \wedge \mathrm{Rat}(r, k- 1, j)$.

Note that increasing $j$ may not enable the elimination of actions. The larger $j$, the more stages will be considered. Ideally, $j$ should be large enough to reach terminal states. However, termination may not be ensured in auction protocols and real world players usually have time restrictions to decide their actions.

4.2 Example: Rationality on the Dutch Auction

Let us consider the Dutch auction from Sect. 3.3. Consider a specific instance $\mathrm{M}_{\text {dut}}$ in $\mathcal {M}_{\text {dut}}$, such that there are only two players $r$ and $s$ whose valuation for the good being auctioned is 7 and 4, respectively. The auctioneer starts by proposing the price 10 and in each round the price is decreased by 1. Formally, $\mathrm{N}_{\mathsf {dut}} = \{r, s\}, \mathrm{V}_{\mathsf {dut}} = \{0, \dots , 10\}, \mathcal {A}_{\mathsf {dut}} = \{\text {bid}_{r}, \text {wait}_{r}, \text {bid}_{s}, \text {wait}_{s}\}, \varPhi _{\mathsf {dut}} = \{winner_{r}, winner_{s}\}$ and $\mathrm{Y}_{\mathsf {dut}} = \{payment_{r}, \vartheta _{r}, payment_{s}, \vartheta _{s}\}$. Let $\mathrm{M}_{\mathsf {dut}}$ be the model defined by the signature $\mathcal {S}_{\text {dut}}= (\mathrm{N}_{\text {dut}}, \mathrm{V}_{\text {dut}}, \mathcal {A}_{\text {dut}}, \varPhi _{\text {dut}}, \mathrm{Y}_{\text {dut}})$ and the constants $\mathsf {starting}= 10$, $\mathsf {dec}=1$, $\mathsf {reserve}= 0$ and $\mathsf {n}= 2$. We consider the initial state $w_0 \in \mathrm{I}$, such that $\pi _{\mathrm{Y}}(w_0, \vartheta _{r}) = 7$ and $\pi _{\mathrm{Y}}(w_0, \vartheta _{s}) = 4$.

Fig. 2.

The utilities agents $r$ and $s$ consider possible to obtain when they are 1st-order rational

Due to the starting price and the decrement, the auction is ensured to end after 10 stages. We therefore focus on the case $j = 10$. If the auction reaches a terminal state before 10 stages, the update function ensures a loop in the terminal state. Since the auction ends at the first bid, we write $\text {bidAfter}(r, m)$ as the sequence of actions $\sigma ^{r}$, such that $\sigma ^{r}_i = \text {wait}_{r}$ for $i < m \le j$ and $\sigma ^{r}_i = \text {bid}_{r}$ for $m \le i \le j$. The sequence is read “$r$ bids after m steps”. Let $\text {onlywait}(r)$ be the sequence of $j$ actions $\text {wait}_{r}$. We use a similar notation for expressing agent $s$’s sequence of actions. Let $d$ be a joint action, we will examine which sequences of actions are rational for each agent to follow. We assume the Dutch auction protocol $\varSigma _\text {dut}$ and the tie-breaking ordering are common knowledge among the agents in $\mathrm{N}_{\text {dut}}$.

If the agents are 0-order rational, that is, if $\mathrm{M}_{\mathsf {dut}} \models _{(w_0, d)} \mathrm{Rat}(r, 0, j) \wedge \mathrm{Rat}(s, 0, j)$, then both agents consider possible that any sequence of joint actions will be taken. If we now consider 1st-order rationality for $r$, that is $\mathrm{M}_{\mathsf {dut}} \models _{(w_0, d)} \mathrm{Rat}(r, 1, j)$, then $r$ is not going to follow any sequence of actions that are strongly dominated in j steps. The weakly rational sequences of actions for $r$ are those where she waits until the price is below her private valuation (e.g., $\text {bidAfter}(r,4), \text {bidAfter}(r,5)$, and so on). The sequence of actions $\text {onlywait}(r)$ is not rational for $r$. The weakly rational actions for agent $s$ when $\mathrm{M}_{\mathsf {dut}} \models _{(w_0, d)} \mathrm{Rat}(s, 1, j)$ are defined similarly. Figure 2 illustrates the utilities each agent considers possible to achieve when playing a weakly rational sequence of actions.

Fig. 3.

The utilities agents $r$ and $s$ consider possible to obtain when they are 7th-order rational and $\mathrm{M}_{\text {dut}}\models (2 \le \vartheta _{s} \le \mathsf {starting}) \wedge (2 \le \vartheta _{r} \le \mathsf {starting})$

For $k>1$, which actions a k-order rational agent considers possible her opponents will take depends on her knowledge about their valuations. For instance, let us consider the case where it is common knowledge that $(2 \le \vartheta _{s} \le \mathsf {starting}) \wedge (2 \le \vartheta _{r} \le \mathsf {starting})$, i.e., we have $\mathrm{M}_{\text {dut}}\models (2 \le \vartheta _{s} \le \mathsf {starting}) \wedge (2 \le \vartheta _{r} \le \mathsf {starting})$. By Proposition 1, both agents then know their opponent has a valuation between 2 and the starting price. If the agent $s$ is 2nd-order rational, she will know the sequence of actions $\text {onlywait}(r)$ is not weakly rational for $r$. Due to the tie-breaking rule, if both agents bid at the same stage, agent $r$ wins. Thus, agent $s$ cannot win by waiting for the price to reach zero and it is not weakly rational to perform $\text {bidAfter}(s,10)$. If $r$ is 3rd-order rational, she knows that $s$ knows $\text {onlywait}(r)$ is not rational for her and consequently, that it cannot be the case that $s$ will $\text {bidAfter}(s,10)$. If the agents are 4th-order rational, they will not consider possible that the good is not sold before the price be zero. Thus, a similar reasoning will happen due tie-breaking when the price is 1. Finally, Fig. 3 illustrates the utilities each agent considers possible when she is 7th-order rational. Since agents are uncertain about which value between 2 and $\mathsf {starting}$ represents the valuation of their opponents, raising the order of rationality beyond 7 would not modify the actions they consider possible to be taken by their opponent.

5 Model Checking

Now we examine the upper bound of the complexity of deciding whether an E-ADL formula is true with respect to a model and a move. To prove this bound, we provide a model-checking algorithm and analyze its complexity. Let $\varphi \in \mathcal {L}_{\text {E-ADL}}$ be a formula and $\mathrm{M}= (\mathrm{W}, \mathrm{I}, \mathrm{T}, \{\mathrm{R}_{r}\}_{r\in \mathrm{N}}, \mathrm{U}, \pi _{\varPhi }, \pi _{\mathrm{Y}})$ 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$, $\mathsf {K}_{r}\phi$ or $[\,d^{{G}}\,] \phi$ 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 '$. Denote $Sub(\varphi )$ as the set of all subformulas of $\varphi$.

Theorem 2

The following problem is in $\mathcal {O}(|\mathrm{W}|\times |\mathcal {A}|^{m})$, where $m = |\mathrm{N}|\times |\varphi |$: Given an ST-Model $\mathrm{M}$, a state $w\in \mathrm{W}$, a joint action $d\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$ and a formula $\varphi \in \mathcal {L}_{\text {E-ADL}}$, determine whether $\mathrm{M}\models _{(w, d)}\varphi$ or not.

Proof

Algorithm 1, named modelCheck, works in the following way: first it gets all subformulas 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 $\mathrm{M}$ at the move $(w, d)$. If $\phi _i$ does not have any subformula, its truth value is obtained directly from the model. Since S is ordered by formulas 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 $[\,b^{{G}}\,] \phi '$ then its label is recursively defined according to $\phi '$ truth value in the updated state given the joint action $\langle b^{{G}}, d^{\text {-}{G}}\rangle$, for any joint action to be taken in the next move. Since we compare with every joint action, this is done in an exponential number of steps, based on the size of the set of agents (i.e., according to $|\mathcal {A}|^{n}$, where $n = |\mathrm{N}|$). Finally, the case where $\phi _i$ is in the form $\mathsf {K}_{r} \phi '$ is recursively defined according to the truth value of $\phi '$ in all moves that are equivalent to $(w, d)$. Similar to the previous case, since we compare with all possible moves and all states in $\mathrm{R}_{r}(w) \subseteq \mathrm{W}$, this step is done in an exponential number of steps (i.e., according to $|\mathrm{W}|\times |\mathcal {A}|^{n}$, where $n = |\mathrm{N}|$). 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 $\mathcal {O}(|\mathrm{W}|\times |\mathcal {A}|^{m})$, where $m = |\mathrm{N}|\times |\varphi |$.

It follows that checking agent rationality is exponential in the quantity of agents, the order of rationality and how many rounds are considered.

Corollary 1

Given an ST-model $\mathrm{M}$, a state $w\in \mathrm{W}$, a joint action $d\in \prod _{r \in \mathrm{N}} \mathrm{A}^{r}$, an agent $r$, $j>0$ and $k>0$, the problem of checking whether $\mathrm{M}\models _{(w, d)}\mathrm{Rat}(r, k+1 , j)$ is in $\mathcal {O}(|\mathrm{W}|\times |\mathcal {A}|^{n kj})$, where $n = |\mathrm{N}|$.

6 Conclusion

In this paper, we present Epistemic Auction Description Language (E-ADL), a language to allow reasoning about knowledge and action choice in auctions. E-ADL extends ADL with epistemic operators and action modalities. Our goal is to provide the ground for the design of General Auction Players and the characterization of their rational behavior. As in the GGP competition, real world players may have time restrictions to decide their actions. For those scenarios, we explore bounded rationality in relation to the level of higher-order knowledge about other agents and bounded looking-ahead beyond the next state. For future work, we intend to investigate the interplay between agents’ bounded rationality and the auctioneer revenue and to generalize the definitions to combinatorial auctions.