=Paper=
{{Paper
|id=Vol-2678/paper11
|storemode=property
|title=An Epistemic Logic for Reasoning about Strategies in General Auctions
|pdfUrl=https://ceur-ws.org/Vol-2678/paper11.pdf
|volume=Vol-2678
|authors=Munyque Mittelmann,Laurent Perrussel
|dblpUrl=https://dblp.org/rec/conf/iclp/MittelmannP20
}}
==An Epistemic Logic for Reasoning about Strategies in General Auctions==
https://ceur-ws.org/Vol-2678/paper11.pdf
An Epistemic Logic for Reasoning about
Strategies in General Auctions?
Munyque Mittelmann and Laurent Perrussel
Université de Toulouse - IRIT, France {munyque.mittelmann,
laurent.perrussel}@irit.fr
Abstract. In this paper, we present the Epistemic Auction Descrip-
tion Language (E-ADL), a language for epistemic and strategic rea-
soning in auctions from the player’s perspective. An automated auc-
tion player faces the challenge of understanding and processing several
different auction-based markets. With E-ADL, an agent can evaluate
the mechanism with well-known properties of economic theory, such as
strategy-proofness and efficiency. Moreover, with the epistemic compo-
nent, the agent can reason about other agents’ private valuation and
their awareness of the protocol properties.
Keywords: Logics for Multi-agents · Game Description Language · Gen-
eral Game Playing · Auction-based Markets.
1 Introduction
Auctions are well-defined environments that provide a valuable testing-ground
for economic theory. They are important for understanding methods of price
formation and negotiations in which both buyers and sellers are actively involved
in determining the price [9]. Typically, an auction-based market is described by
a set of rules stating how the participants bid, how the winners are determined,
and what should be their payment. Any autonomous auction agent will face the
challenge of understanding and processing a number of different auction-based
markets. There are variants that differ on the participants’ type (e.g. only buyers,
both buyers and sellers, ...), the kind and amount of goods been auctioned, the
bidding protocol, and the allocation and payment rules [10].
The great variety of auction protocols prevents any autonomous agent to eas-
ily switch between different auction-based markets. Building intelligent agents
that can switch between different auctions and process their rules is a key issue
for designing automated auction-based market places. For this reason, we previ-
ously proposed a general language to describe auction-based markets from the
auctioneer perspective [11]. Auction Description Language (ADL) is based on
the Game Description Language (GDL), which is a logic programming language
for representing and reasoning about game rules [6].
?
Copyright © 2020 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
2 Mittelmann and Perrussel
In the players’ perspective, the agents may be able to process the protocol
to collect the definition of its main components: the bid legality, the payment,
and allocation rules. With respect to these components, the bidder evaluates the
auction market: the impact of her participation (individual rationality), the ob-
jectives of the auctioneer (to maximize revenue or efficiency), and the possibility
of manipulation (strategy-proofness). Finally, the bidder may use her knowledge
about other agents’ private valuations and awareness of the auction properties.
In this paper, we focus on the epistemic and strategic reasoning of such
auction players. We extend ADL with knowledge operators from the Epistemic
GDL [8] and the action modality from the GDL variant proposed in [18]. Our
goal is to provide the ground for the design of General Auction Players: (i)
such player should be able to evaluate the mechanism and its strategy-proofness
dimension and (ii) if not, she should then consider her knowledge about other
players in order to define her action.
1.1 Related Work
To the best of our knowledge, there is no contribution that focuses on the strate-
gic dimension of auctions through a logical perspective. However, numerous con-
tributions are defining logical systems for Strategic Reasoning. The Alternating
time Temporal Logic (ATL) [1] provides a logic-based analysis of strategic de-
cisions. For representing games, the Propositional Logic of Games (GPL) [13]
specifies the effects of game playing by using inference mechanisms from propo-
sitional dynamic logic (PDL). A more practical approach to specify a game is to
use the Game Description Language (GDL) [6]. The Auction Description Lan-
guage (ADL) [11] extends GDL by handling numerical variables, a key feature
for representing the allocation and payment rules.
To represent strategies, the Strategy Logic (SL) uses first-order quantifica-
tions over strategies in turn-based (i.e. asynchronous) games [2]. This approach
cannot model the internal structures of strategies, which prevents to easily de-
sign strategies aiming to achieve a goal state. [14] introduces a logic for reasoning
about composite strategies in extensive form turn-based games: strategies are
treated as programs that are combined by PDL-like connectives to ensure an
outcome. Zhang and Thielscher [19] present a variant of GDL to describe game
strategies, where formulas can be understood as move recommendations for a
player. However, their work can only model turn-based games.
To incorporate imperfect information games, GDL has been extended to
GDL-II [16] and GDL-III [17]. As purely descriptive languages, 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 to be implemented in realistically in an artificial agent.
Jiang et al. [8] propose an epistemic extension of GDL (EGDL) to represent and
reason about imperfect information games. The language allows representing the
rules of an imperfect information game.
Epistemic Logic for Reasoning in Auctions 3
Structure of the paper Due to the space limitation, we omitted the Propo-
sitions proofs. All the proofs are available at https://epistemicadl.page.link/
EELP2020. The remainder of the paper proceeds as follows. In Section 2, we de-
fine the base terminology and describe the State Transition structures that are
used to evaluate E-ADL semantics. In Section 3, we present the language syntax
and semantics and illustrate our approach by describing and deriving properties
about a standard type of auction, a First-Price Blind protocol. In Section 4, we
define strategy rules, which are formulas in E-ADL assigning a unique action to
be taken in each state. In Section 5, we show how to verify classic properties of
mechanism design in E-ADL auctions, such as efficiency and strategy-proofness.
Finally, Section 6 concludes the paper.
2 State Transition Auctions
In this section, we introduce a logical framework for reasoning in general auction
protocols. The framework is based on ADL [11] and Epistemic GDL [7]. We call
the framework Epistemic Auction Description Language, denoted E-ADL. We
restrict our definition to single-unit and single-good auctions.
Definition 1. An auction signature S is a tuple (N, V, A, Φ, Y ), where: (i) N =
{1, 2, · · · , n} is a nonempty finite set of agents; (ii) V ⊂ N is a finite subset of
naturalSnumbers representing the range of valuations, bids and payments; (iii)
A = r∈N Ar , where Ar = {bidr (x) : x ∈ V } consists of a nonempty set
of actions (or bids) performed by agent r ∈ N and Ar ∩ Ai = ∅ if r 6= i.
For convenience, we occasionally write ar for denoting an action in Ar ; (iv)
Φ = {p, q, · · · } is a finite set of atomic propositions for specifying individual
features of a state; and (v) Y = {y1 , y2 , · · · } is a finite set of numerical variables
for specifying numerical features of a state.
Through the rest of the paper, we will fix an auction signature S and all
concepts will be based on this auction signature, except if stated otherwise. In
this paper, we adopt a semantics based on state-transition models which is more
suitable for describing the dynamics as the one based on stable models initially
considered for GDL and General Game Playing [6].
Definition 2. A state transition ST-model M is a tuple (W, I, T, {Rr }r∈N , L, U ,
πΦ , πY ), where: (i) W is a finite nonempty set of states; (ii) I ⊆ W is a set of
initial states; (iii) T ⊆ W \ I is a set of terminal states; (iv) Rr ⊆ W × W is an
equivalence relation for agent r, indicating the states that are indistinguishable
for r; (v) L ⊆ W ×Q A is a legality relation, describing the legal actions at each
state; (vi) U : W × r∈N Ar → W is an update function, specifying the transi-
tions for each combination of joint actions; (vii) πΦ : W → 2Φ is the valuation
function for the state propositions; and (viii) πY : W × Y → V is the valuation
function for the numerical variables.
Given d ∈ r∈N Ar , let d(r) be the individual action for agent r in the joint
Q
action d. Let L(w) = {a ∈ A | (w, a) ∈ L} be the set of all legal actions at state
4 Mittelmann and Perrussel
w. Let Rr (w) denote the set of all states that agent r cannot distinguish from
w, i.e. Rr (w) = {u ∈ W : wRQ r u}.
For any w ∈ W and d ∈ r∈N Ar , we call (w, d) a move. It is a legal move
if (w, d(r)) ∈ L, for all r ∈ N . WeQuse the notation (w, d(r), d(−r)) when it is
more convenient, where d(−r) ∈ i6=r∈N Ai denotes the actions of all agents
except Qby r in the joint action d. Any set Sr ⊆ {(w, d) : d(r) ∈ L(w) & w ∈ W
& d ∈ i∈N Ai } of moves is a strategy of a player r ∈ N . Our notion of move
and strategy is based on the asynchronous definition from [18] and [19].
Definition 3. Two moves (w, d), (w0 , d0 ) are imperfect recall equivalent for agent
r, written (w, d) ≈r (w0 , d0 ), iff wRr w0 and d(r) = d(r)0 .
An agent with imperfect recall is only aware of the present state but forgets
everything that happened [7]. We only consider imperfect recall because differ-
ently from the standard GDL, our semantics is based on moves instead of paths.
This semantics 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). Since a GDL path is a sequence of
states and (legal) joint actions, the set of complete paths for a model M can have
exponential size. For a formal definition of reachable states and complete paths
in GDL, please refer to [8]. In E-ADL, we define the action execution modality
in synchronous games1 . The idea of move-based semantics and action modalities
comes from [18]. Their approach is restricted to synchronous games, where only
one action can be performed at a given state.
Given an agent r ∈ N , a strategy Sr is complete if there is a move (w, d) ∈ Sr
unless L(w) ∩ Ar = ∅, for each state w ∈ W . In other words, the strategy Sr
always provides at least one action to be taken in any state, except if there
is no legal action. A strategy Sr is deterministic if (w, d(r), d(−r)) ∈ Sr and
(w, d(r)0 , d(−r)0 ) ∈ Sr , then d(r) = d(r)0 , for any w ∈ W . Finally, a strategy Sr
is functional if it is complete and deterministic. Intuitively, a functional strategy
provides a unique action to be taken by r in any state.
A run in an E-ADL model is a finite sequence of legal moves (w0 , d0 ), (w1 , d1 ),
· · · , (we , de ), such that w0 ∈ I and wi+1 = U (wi , di ), for any 0 ≤ i < e. Although
the agents evaluate the semantics based on moves, a run represents an execution
of an auction protocol.
3 Epistemic Auction Description Language
The Epistemic Auction Description Language (E-ADL) is a framework to allow
epistemic reasoning for auction players. Let z ∈ Lz be a numerical term defined
as follows: z ::= z 0 | add(z, z) | sub(z, z) | min(z, z) | max(z, z) | times(z, z) | y |
maxbid, where z 0 ∈ N, y ∈ Y , a ∈ A.
The numerical terms add(z1 , z2 ), sub(z1 , z2 ) and times(z1 , z2 ) specify the
value obtained by adding, subtracting and multiplying z2 from z1 , respectively.
1
Asynchronous games can be simulated as synchronous games in GDL by turn-based
legality. An example of how to simulate asynchronous games is given at [8].
Epistemic Logic for Reasoning in Auctions 5
The terms min(z1 , z2 ) and max(z1 , z2 ) specify the minimum and maximum value
between z1 and z2 , resp. The numerical term maxbid represents the highest bid
in a move. Finally, y denotes the value of the variable y ∈ Y in the current state.
The Epistemic Auction Description language is denoted by LE−ADL and a
formula ϕ in LE−ADL is defined by the following BNF grammar:
ϕ ::= p | initial | terminal | legal(ar ) | does(ar ) | Kr ϕ | Cϕ | [ ar ]ϕ |
¬ϕ | ϕ ∧ ϕ | z < z | z > z | z = z | r ≺ r
where p ∈ Φ, r ∈ N , ar ∈ A and z ∈ Lz .
Other connectives ∨, →, ↔, > and ⊥ are defined by ¬ and ∧ in the standard
way. The comparison operators ≤, ≥ and 6= are defined by ∨, >, < and =. The
extension of the comparison operators >, <, =, ≤, ≥, 6= and numerical terms
max(z1 , z2 ), min(z1 , z2 ), add(z1 , z2 ) to multiple arguments is straightforward.
We use set notation to compactly represent numerical terms with two or
more arguments. For instance, max({ϑi : i ∈ N }) is a representation of the
numerical term max(ϑ1 , ϑ2 , · · · , ϑn ), i.e. the maximum private value among the
agents. Note that this notation also includes conditions over elements of a set.
As an example, assume z1 , z2 , bound and maxset are natural numbers, then
the formula maxset = max({v1 , v2 : v1 < bound & v2 < bound}) is a compact
representation of the E-ADL formula (v1 < bound ∧ v2 < bound ∧ maxset =
max(v1 , v2 )) ∨ (v1 < bound ∧ maxset = v1 ) ∨ (v2 < bound ∧ maxset = v2 ), i.e.
maxset is the maximum between two values complying with a logical condition.
Intuitively, initial and terminal specify the initial and the terminal states,
respectively; does(ar ) asserts that agent r takes action ar at the current move;
legal(ar ) asserts that agent r is allowed to take action ar the current state. Given
an agent r ∈ N , we denote does(bidr (ϑr )) to represent that r did the action
of bidding its own value. Similarly, legal(bidr (ϑr )) denotes that this action is
legal. The epistemic operators Kr and C are taken from the Modal Epistemic
Logic [5]. The formulas Kr ϕ and Cϕ are read as “agent r knows ϕ” and “ϕ is
common knowledge among all the agents in N ” (i.e. every agent knows ϕ, knows
that every other agent knows ϕ, and so on), respectively. The action execution
operator comes from the GDL variant with action modalities [18] and a formula
[ ar ]ϕ means that if action ar is executed at the current state, ϕ will be true in
the next state. The formulas z1 > z2 , z1 < z2 , z1 = z2 means that a numerical
term z1 is greater, less and equal to a numerical term z2 , respectively. The tie-
breaking priority is represented by the formula r1 ≺ r2 , i.e. agent r1 precedes r2
in the lexicographical order.
Instead of using the temporal operator from GDL, we use the action
modality to define an abbreviation with similar meaning [18]:
^ _
ϕ =def (does(ar ) ∧ [ ar ]ϕ)
r∈N ar ∈Ar
The formula ϕ means “ϕ holds at the next state”. We also use the fol-
b r ϕ =def ¬Kr ¬ϕ and
lowing abbreviations from the Modal Epistemic Logic: K
6 Mittelmann and Perrussel
V
Eϕ =def r∈N Kr ϕ, where Kb r ϕ represents that “ϕ is compatible with agent r’s
knowledge”. The formula Eϕ represents that “every agent in N knows ϕ”.
3.1 Semantics
The semantics for the ADL language is given in two steps. First, we define
function f to define the meaning of numerical terms z ∈ Lz . Next, a formula
ϕ ∈ LE−ADL is interpreted with respect to a move.
Through the rest of this paper, the function maximum(a, b, · · · ) returns the
maximum value between a finite sequence a, b, · · · ∈ Z. Let Y + = Y ∪ {maxbid}.
Numerical terms z ∈ Lz \ Y + have a constant evaluation, independently from a
move. Their valuation can be simply assigned by function fZ (Definition 4). In
Definition 5, we specify the more general function f to evaluate any z ∈ Lz .
Definition 4. . Define Function fZ : Lz \ Y + → Z, assigning any formula
z ∈ Lz \ Y + to a number in Z:
If z is in the form add(z 0 , z 00 ), sub(z 0 , z 00 ), min(z 0 , z 00 ), max(z 0 , z 00 ), times(z 0 ,
z ) or mod(z 0 ), then fZ (z) is defined through the application of the corresponding
00
mathematical operators and functions. Otherwise, fZ (z) = z if z ∈ Z.
f : W × r∈N Ar × Lz → Z, assigning any state
Q
Definition 5. Define Function
w ∈ W , joint action d ∈ r∈N Ar , and formula z ∈ Lz to a number in Z:
Q
if z ∈ Z \ Y +
fZ (z)
f (w, d, z) = πY (w, z) if z ∈ Y
maximum({x : d(r) = bidr (x) & r ∈ N })
if z = maxbid
Definition 6. Let M be an ST-Model. Given a move (w, d), where w ∈ W and
d ∈ r∈N Ar , and a formula ϕ ∈ LADL , we say ϕ is true (or satisfied) in the
Q
move (w, d) under M , denoted by M |=(w,d) ϕ, according with the following:
M |=(w,d) p iff p ∈ πΦ (w)
M |=(w,d) ¬ϕ iff M 6|=(w,d) ϕ
M |=(w,d) ϕ1 ∧ ϕ2 iff M |=(w,d) ϕ1 and M |=(w,d) ϕ2
M |=(w,d) initial iff w∈I
M |=(w,d) terminal iff w∈T
M |=(w,d) r1 ≺ r2 iff r1 ≺Lex r2
M |=(w,d) legal(ar ) iff ar ∈ L(w)
M |=(w,d) does(ar ) iff d(r) = ar
M |=(w,d) z1 cp z2 iff f (w, d, z1 ) cp f (w, d, z2 ), where cp ∈ {>, <, =}
for any w0 ∈ W & d0 ∈ i∈N Ai , if (w, d) ≈r (w0 , d0 ),
Q
M |=(w,d) Kr ϕ iff
then M |=(w0 ,d0 ) ϕ
for any w0 ∈ W & d0 ∈ i∈N Ai , if (w, d) ≈N (w0 , d0 ),
Q
M |=(w,d) Cϕ iff
then M |=(w0 ,d0 ) ϕ
Epistemic Logic for Reasoning in Auctions 7
M |=(w,d) [ ar ]ϕ iff M |=(U (w,d0 ),c) ϕ, where d0 = (ar , d(−r)),
for all c ∈ i∈N Ai
Q
S
where ≈N is the transitive closure of r∈N ≈r and ≺Lex is a relation denoting
the lexicographical order among agents in N .
In the semantics of Cϕ, note (w, d) ≈N (w0 , d0 ) represents the transitive
closure of the equivalence relation between states as the joint actions d and d0
are the same.
A formula ϕ is globallyQtrue in an ST-Model M , written M |= ϕ, if M |=(w,d)
ϕ for all w ∈ W and d ∈ r∈N Ar . Finally, let Σ be a set of formulas in LADL ,
then M is a model of Σ if M |= ϕ for all ϕ ∈ Σ.
Given an ST-model M , the Epistemic Properties (Prop. 1) express when a
formula is globally known by one agent and when it is globally common knowl-
edge.
Proposition 1. Let M be an ST-Model, r ∈ N be an agent and ϕ ∈ LE−GDL
be a formula, then
1. M |= ϕ → Kr ϕ if and only if for all w, w0 ∈ W and all d, d0 ∈ i∈N Ai such
Q
that (w, d) ≈r (w0 , d0 ), M |=(w,d) ϕ iff M |=(w0 ,d0 ) ϕ
2. M |= ϕ → Cϕ if and only if for all w, w0 ∈ W and all d, d0 ∈ i∈N Ai such
Q
that (w, d) ≈N (w0 , d0 ), M |=(w,d) ϕ iff M |=(w0 ,d0 ) ϕ
3.2 Running Example: a First-Price Blind Auction
In this section, we illustrate how to describe an auction in E-ADL. First, we
present the protocol from the auctioneer perspective. This protocol describes
strictly the rules of the auction. Next, we present additional epistemic rules for
allowing the agents’ reasoning.
Auctioneer Perspective To describe a First-Price Blind Auction, we first
define the auction signature, written Sbli = {N, V, A, Φbli , Ybli }, where Φbli = {},
Ybli = {paymentr , allocr , ϑi : r ∈ N }. The numerical variables paymentr , allocr
and ϑr specify the payment, the allocation and the private value for an agent r.
The rules of a First-Price Blind Auction are formulated by E-ADL-formulas as
shown in Figure 1.
In an initial state, all agents have the payment and allocation equal to 0
(Rule 1). We are in a terminal state iff we are not in an initial state (Rule 2).
Rule 3 specifies that it is legal, for all agents, to bid any value between 0 and
V if we are not in the terminal state. In the terminal state, the agents can only
bid 0. Rules 4 and 5 specify how the payment and allocation are updated. The
formula winsr,x represents the condition of whether agent r bids x and for all
other agent i, either i does not bid x or r wins the tie-breaking with i. If it is
an initial state, winsr,x for an agent r and x is the highest bid, then in the next
state she will get the good and pay her bid price. Otherwise, she will not get the
good and the payment will be 0. Rule 6 states that after the terminal state, the
numerical variables cannot change (self-loop). Let Σbli be the set of Rules 1-6.
8 Mittelmann and Perrussel
r V i
V does(bid (x)) ∧ i6=r∈N (¬does(bid (x)) ∨ r ≺ i) and r ∈ N ,
Let winsr,x =def
1. initial ↔ i∈N paymenti = 0 ∧ alloci = 0
2. terminal ↔ ¬initial
3. Wx∈V (legal(bidr (x)) ↔ ¬terminal ∨ (terminal ∧ x = 0))
V
4. Vx∈V (initial ∧ maxbid = x ∧ winsr,x ↔ (allocr = 1 ∧ paymentr = x))
5. Wx∈V (initial ∧ ¬winsr,x → (allocr = 0 ∧ paymentr = 0))
6. x∈V,y∈{0,1} terminal ∧ allocr = y ∧ paymentr = x → (allocr = y ∧
paymentr = x)
Fig. 1. First-Price Blind Auction represented by Σbli (Auctioneer Protocol)
Agent’s perspective Now let us focus on the agents’ perspective. The following
E-ADL rules says that each agent is aware of its own valuation, each agent has
a private in V , and each agent knows her own action, respectively:
Let rV∈ N ,
1. Wx∈V (ϑr = x → Kr (ϑr = x))
2. Vx∈V ϑr = x
3. x∈V (does(bidr (x)) → Kr does(bidr (x)))
Fig. 2. First-Price Blind Auction represented by Σbli,N (Agent’s Protocol)
Let Σbli be the set of Rules 1-3. We assume that each agent knows the agent’s
protocol, i.e. EΣbli,N and the Auctioneer Protocol is common knowledge, i.e.
CΣbli .
Model Representation Given Sbli = (N, V, A, Φbli , Ybli ), the state transition
ST-model Mbli = (Wbli , Ibli , Tbli , {Rr,bli }r∈N , Lbli , Ubli , πΦ,bli , πY,bli ) is the model
representation of the First-Price Blind Auction. By space limitation, we omit
its construction, which is available at https://epistemicadl.page.link/EELP2020.
Figure 3 illustrates a run in Mbli , where N = {a, b, c}. In state w0 , the joint
action d0 states the agents’ bids. In state w1 , the good is allocated the agent
with highest bid and she pays her bid.
In the next section, we derive properties from the blind auction model Mbli
and the protocols represented by the set of rules Σbli and Σbli,N .
Protocol Valuation The next proposition shows that soundness does hold, i.e.
the framework provides a sound description for Σbli and Σbli,N .
Proposition 2. Mbli is an ST-Model and it is a model of Σbli and Σbli,N .
Epistemic Logic for Reasoning in Auctions 9
Fig. 3. A run (w0 , d0 ), (w1 , d1 ) in Mbli
Proposition 3 shows that Σbli (and resp. Σbli,N ) represents a one-shot pro-
tocol.
Proposition 3. Mbli |= initial → terminal
If the auctioneer protocol Σbli entails a formula, then this formula is commom
knowledge. Similarly, if the agents’ perspective protocol Σbli,N entails a formula,
then every agent knows the formula (Proposition 4).
Proposition 4. Given ϕ ∈ LE−GDL ,
1. If Mbli |= Σbli → ϕ, then Cϕ
2. If Mbli |= Σbli,N → ϕ, then Eϕ
Up to now, we focus on the protocol definition and semantics. Next, we
address how an agent can use LE−ADL to choose her actions during an auction.
In other words, we describe strategy rules: E-ADL formulas which assign a unique
action to be taken in each state.
4 Strategy rules
For any state-transition model M and a formula ϕ ∈ LE−ADL , let S(ϕ) =
{(w, d) : M |=(w,d) ϕ}. S(ϕ) denotes all moves under which ϕ is valid.
Definition 7. Given a model M and a strategy S r for agent r ∈ N , a formula
ϕ ∈ LE−ADL is a representation of S r iff S r = S(ϕ). If S(ϕ) is a representation
of a functional strategy, then ϕ is a strategy rule.
10 Mittelmann and Perrussel
In the following example, we illustrate a strategy rule in the Blind Auction
represented by Mbli .
Example 1. Given the blind auction represented in the running example by Mbli
and an agent r ∈ N , the formula
_
outbidr =def does(bidr (v)) ∧
v∈V
v = min {ϑr , x : Kr x = add(max({ϑi : i 6= r ∈ N }), 1) & x ∈ V }
is a strategy rule where the agent outbids the higher private value of her op-
ponents or bids its own value if she knows the other agents’ private values are
greater then her value.
Let us assume the agent a ∈ N has the equivalence relation Ra illustrated
by Figure 4. Agent a knows the other agents, b and c, evaluate the good at
most 2 while a evaluates the good at 5. Since it is a first-price auction, we can
see that b and c would not maximize their utility by bidding above their pri-
vate value. Thereby, the strategy outbida consists of outbidding the adversaries
private value, that is to bid 3.
Fig. 4. Indistinguishable states for agent a
The action of bida (3) was taken at the run illustrated by Figure 3. In this
case, agent a gets the good and pays 3, which leads to a positive utility.
Proposition 5. Given an agent r, the formula outbidr is a strategy rule.
In the next section, we describe how to verify classic properties of mechanism
design, such as efficiency, strategy-proofness and individual rationality. For the
game-theoretic definition of mechanism design and its properties, please refer to
[12], [4] and [15].
Epistemic Logic for Reasoning in Auctions 11
5 Representing Classical Properties of Auctions
Assuming the agents have private valuations ϑ1 , · · · , ϑn in V . Given an agent
r ∈ N , let us denote the numerical term utility(ϑr , r) =def sub(times(ϑr ,
allocr ), paymentr ) as the utility of r given the private value ϑr . Next, we show
how to represent strategy-proofness, efficiency and individual rationality prop-
erties in E-ADL.
We assume an agent is rational by the standard utility maximization defini-
tion: a rational agent has a private valuation and tries to maximize her payoff.
Following [3], we consider a weak notion of rationality. An agent r is said to
be weakly rational if she does a legal action ar such that, for every other legal
action br , there exists some state of the world that r considers possible, where
ar performs as well as br . That is if r knows that by bidding ar it is possible to
get a utility at least as good as by doing br .
Formally, agent r ∈ N is weakly rational in the move (w, d) if
^ ^
M |=(w,d) (does(ar ) ∧ legal(ar ) → (¬legal(br )∨
ar ∈Ar br 6=ar ∈Ar
_
(K̂r ([a ]utility(ϑr , r) = x ∧ [br ]utility(ϑr , r) = x0 ∧ x ≥ x0 ))))
r
x,x0 ∈V
We denote rat(w) as the set of joint actions d ∈ r∈N Ar such that (w, d)
Q
is a move where all the agents are weakly rational. Notice that this notion of
rationality requires an epistemic reasoning for the agents about the possible
consequences of their actions.
Strategy-proofness A mechanism is strategy-proof if the agents would prefer
to truthfully report their valuation rather than bidding any other possible value
[15]. We say that a state w ∈ W is strategy-proof for an agent r ∈ N , if bidding
her private values leads to a Q better (or equal) utility than bidding any other
value, for any joint action d ∈ i∈N Ai . In E-ADL, we express this condition by
using the action execution operator as follows:
_
SPr =def ([bidr (ϑr )]utility(ϑr , r) = x
x∈V
^
∧ [bidr (v)]utility(ϑr , r) ≤ x)
v6=ϑr ∈V
The formula SPr means that agent r gets the utility x when bidding her
own private value and for any other value v, her utility is bellow or equal to
x. In this formula, the value of the numerical term utility(ϑr , r) depends on
the valuation of the numerical variables in the state resulting from applying
the action execution operator. An auction is strategy-proof in a state when it
is
V strategy-proof in that state for all agents and joint actions, i.e. SPN =def
r∈N SPr .
12 Mittelmann and Perrussel
For verifying whether an auction is strategy-proof, we do not make any as-
sumption about the agents’ rationality. In the blind auction described by Mbli ,
the winner pays her bid. Thereby, the agents do not have an incentive to be
truthful (i.e. bid their private value).
Proposition 6. For any w ∈ Ibli , d ∈ r∈N Ar and r ∈ N , Mbli 6|= SPr , and
Q
consequently, Mbli 6|= SPN .
Example 2. We can construct a strategy-proof blind auction by changing the
payment rule from Σbli . Let us define a Vickrey Auction Σvic , such that it is
exactly the same as Σbli , except by Rule 4, which is replaced by the following
Rule 40 :
_
initial ∧ maxbid = f irst ∧ winsr,f irst ∧
second,f irst,x1 ,··· ,xn ∈V
second = max({0, xr : xr 6= maxbid & does(bidr (xr ) & r ∈ N )}) →
(allocr = 1 ∧ paymentr = second)
The model Mvic is constructed in a similar way than Mbli , except the update
function, which assigns the second highest bid as the winner’s payment.
Proposition 7. For any w ∈ Ivic , d ∈ r∈N Ar and r ∈ N , Mvic |=(w,d) SPr ,
Q
and consequently, Mvic |=(w,d) SPN .
Efficiency We say that a mechanism is efficient if it maximizes the social
welfare [4]. In a single-good and single-unit auction, it means that the good
should be allocated to the agent who valuates it the most, i.e. the agent with the
highest private value. Here, we make an assumption about the agents’ behavior:
we assume they are weakly rational and only consider moves according to this
assumption. Without this restriction, agents could perform random actions, and
thus it would not be possible to ensure that the winning agent has the highest
valuation. Efficiency (EF ) in a state w ∈ W , is defined by the validity of the
following E-ADL formula for any joint action d ∈ rat(w):
^
EF =def allocr = 1 → ϑr = max({ϑi : i ∈ N })
r∈N
Efficiency is an epistemic property: to check if an auction is efficient, an
agent should reason about the knowledge of all the agents about the possible
consequences of their own actions.
Proposition 8. Given the ST-models Mbli and Mvic , then for any w ∈ Wbli ,
w0 ∈ Wvic and for all d ∈ rat(w), d0 ∈ rat(w0 ), (i) Mbli 6|=(w,d) EF and (ii)
Mvic |=(w0 ,d0 ) EF .
If we did not assume weakly rationality of the agents, the auction represented
by Mvic would not be efficient. Even if it is strategy-proof, we still need to link
this property to the assumption they will behave rationally.
Epistemic Logic for Reasoning in Auctions 13
Individual Rationality A mechanism is individual-rational if an agent can
always achieve as much utility as from participating as without participating
[12]. We consider that if an agent does not participate in the auction than she
would neither have the good allocated or a payment assigned and her utility is
zero. The auction is individual-rational in a state w ∈ W for an agent r if by
participating she can achieve a utility greater or equal to zero, for any joint action
d ∈ i∈N Ai . The individual-rationality constraint is defined by the following
Q
E-ADL formula:
_
IRr =def [ar ]utility(ϑr , r) ≥ 0
a∈Ar
Similarly, we can verify whether the action V is individual-rational for every
agent in N by the following formula: IRN =def r∈N IRr .
The individual-rationality property consists of checking whether an agent has
a reason to participate in the auction. It does not make any assumptions about
her committing to a rational behavior once the auction starts. The following
proposition shows Mbli and Mvic are individual-rational.
Proposition 9. For any w0 ∈ Wbli , w ∈ Wvic , d ∈ r∈N Ar and r ∈ N , (i)
Q
Mbli |=(w,d) IRr , and consequently, Mbli |=(w,d) IRN ; (ii) Mvic |=(w,d) IRr , and
consequently, Mvic |=(w,d) IRN .
Note that even if an auction has a property (such as strategy-proofness,
efficiency, or individual rationality), it does not mean that the agents are indi-
vidually or collectively aware of these properties. This knowledge may come from
reasoning with previous background knowledge. Let us now discuss how knowing
some classical auction properties can be meaningful for defining strategies.
5.1 Knowledge about auction properties
Agents can have different levels of knowledge over auction properties, by com-
bining the C and Kr operators and properties formulas. For instance, Kr SPr
represents the agent knows the auction is strategy-proof. When that is the case,
the agent can avoid any additional reasoning about her strategies and other
agents’ behavior: she knows that she cannot increase her utility by bidding any
value different from her private value. If a weakly rational agent knows an auction
is strategy-proof, then she will bid her own private value (Proposition 10).
Proposition 10. Given an ST-model M , a state w ∈ W , a joint action d ∈
i
Q
r∈N A and an agent r ∈ N , if r weakly rational then
M |=(w,d) Kr SPr ∧ legal(bidr (ϑr )) → does(bidr (ϑr ))
Corollary 1. Given r ∈ N , the formula does(bidr (ϑr )) is a strategy rule.
To check whether the auction is strategy-proof, i.e. M |=(w,d) Kr SPr , there is no
epistemic requirement about the other agents. The agent can derive Proposition
10 by simply reasoning about the possible outcomes from her actions.
14 Mittelmann and Perrussel
If an agent r knows that an auction is efficient and that she is not the
agent with the highest valuation, then she knows she will not win the auction
(Proposition 11). In this situation, assuming the payment for losing agents is
zero, bidding any value below her private value will lead to the same payoff.
This information about efficiency may be useful if the agent needs to choose to
participate in different auctions.
Proposition 11. Assuming the agents are weakly rational, given an ST-model
M , a state w ∈ W and any joint action in d ∈ rat(w),
_
CEF ∧ Kr ϑi > ϑr → Kr allocr = 0
i∈N
If it is not IRr , any agent with utility maximization rationality would not
participate. Furthermore, if for some utility maximization rational agent i, agent
r knows agent i knows it is not IRi , then r knows i should not participate and
r does not have to reason about i’s bid.
E-ADL can provide an interplay between properties and agents’ strategies, as
illustrated by Proposition 10. When the reasoning about the classical properties
is not enough to decide their strategy, agents can use the epistemic component
to choose between different weakly rational actions. For instance, the First-Price
Blind Auction denoted by Mbli is neither strategy-proof nor efficient and there
may be several actions complying with the weakly rationality condition. This is
a trade-off situation: the less the agent bids, the higher her utility, but the lower
her chance of winning (in terms of the outcomes in the possible worlds). The
strategy rule outbidr presented in Example 1 illustrates how an agent can decide
among different actions in the blind auction.
6 Conclusion
In this paper, we present E-ADL, a language to allow epistemic and strategic
reasoning in single-unit and single-good auctions. The language enables an agent
to evaluate the auction through well-known properties from the economic theory:
strategy-proofness, efficiency, and individual rationality. With E-ADL an agent
can choose her bid with respect to the auction properties and her knowledge
about the other players’ private valuation and awareness of these properties.
For future work, we intend to generalize the definitions for describing other
types of auctions, from multi-units auctions to combinatorial exchange. We also
intend to investigate the complexity of the model-checking problem for E-ADL
formulas, that is the problem of determining whether an E-ADL formula holds
at a move under an ST-model. Promising starting points are the results of ADL
and EGDL. The model checking complexity is in PTIME-complete [11] for ADL
formulas and in ∆p2 -complete for EGDL [8]. These complexity results are rea-
sonable when compared to other languages for strategic reasoning, such as ATL
and its variants. The main difference between the model-checking for E-ADL
and EGDL is the action modality, whose truth condition refers to every possible
Epistemic Logic for Reasoning in Auctions 15
joint action. Finally, an interesting line of work is to explore orders of rationality
[3]: how a rational agent would strategically bid when she knows the other agents
are rational, and how should she behave when they are aware of her rationality.
Acknowledgments
This research is supported by the ANR project AGAPE ANR-18-CE23-0013.
References
1. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Jour-
nal of the ACM (JACM) 49(5), 672–713 (2002)
2. Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Information and
Computation 208(6), 677–693 (2010)
3. Chen, J., Micali, S., Pass, R.: Tight revenue bounds with possibilistic beliefs and
level-k rationality. Econometrica 83(4), 1619–1639 (2015)
4. De Vries, S., Vohra, R.V.: Combinatorial auctions: A survey. INFORMS Journal
on Computing 15(3), 284–309 (2003). https://doi.org/10.1287/ijoc.15.3.284.16077
5. Fagin, R., Moses, Y., Halpern, J.Y., Vardi, M.Y.: Reasoning about knowledge. MIT
press (2003)
6. Genesereth, M., Thielscher, M.: General game playing. Synthesis Lectures on Ar-
tificial Intelligence and Machine Learning, Morgan & Claypool Publishers (2014)
7. Jiang, G., Perrussel, L., Zhang, D.: On axiomatization of epistemic gdl. In: Baltag,
A., Seligman, J., Yamada, T. (eds.) International Workshop on Logic, Rationality
and Interaction. pp. 598–613. Springer, Berlin, Heidelberg (2017)
8. Jiang, G., Zhang, D., Perrussel, L., Zhang, H.: Epistemic GDL: A logic for repre-
senting and reasoning about imperfect information games. In: Proc. of IJCAI-2016
(2016)
9. Klemperer, P.: Auction Theory: A Guide to the Literature. Journal of Economic
Surveys (1999). https://doi.org/10.1111/1467-6419.00083
10. Krishna, V.: Auction Theory. Academic Press (2009)
11. Mittelmann, M., Perrussel, L.: Auction description language (ADL): a general
framework for representing auction-based markets. In: de Giacomo, G. (ed.) ECAI
2020. IOS Press, Santiago de Compostela (2020)
12. Parkes, D.C., Ungar, L.H.: Iterative combinatorial auctions: Achieving economic
and computational efficiency. University of Pennsylvania Philadelphia, PA (2001)
13. Pauly, M., Parikh, R.: Game logic-an overview. Studia Logica 75(2), 165–182
(2003)
14. Ramanujam, R., Simon, S.: Dynamic logic on games with structured strategies. In:
Proc. of KR-2008. p. 49–58. AAAI Press (2008)
15. Roughgarden, T.: Algorithmic game theory. Communications of the ACM 53(7),
78–86 (2010)
16. Thielscher, M.: A general game description language for incomplete information
games. Proc. of AAAI-10 pp. 994–999 (2010)
17. Thielscher, M.: GDL-III: A description language for epistemic general game play-
ing. Proceeding of IJCAI-2017 pp. 1276–1282 (2017)
18. Zhang, D., Thielscher, M.: A logic for reasoning about game strategies. In: Proc.
of AAAI-2015. p. 1671–1677. AAAI Press (2015)
19. Zhang, D., Thielscher, M.: Representing and Reasoning about Game Strategies.
Journal of Philosophical Logic 44(2), 203–236 (2015)