An Epistemic Logic for Reasoning about Strategies in General Auctions?

Abstract

In this paper, we present the Epistemic Auction Description Language (E-ADL), a language for epistemic and strategic reasoning in auctions from the player's perspective. An automated auction player faces the challenge of understanding and processing several di erent auction-based markets. With E-ADL, an agent can evaluate the mechanism with well-known properties of economic theory, such as strategy-proofness and e ciency. Moreover, with the epistemic component, the agent can reason about other agents' private valuation and their awareness of the protocol properties.

Keywords

• Logics for Multi-agents
• Game Description Language
• General Game Playing
• Auction-based Markets

Introduction

Auctions are well-de ned 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 di erent auction-based markets. There are variants that di er 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 easily switch between di erent auction-based markets. Building intelligent agents that can switch between di erent auctions and process their rules is a key issue for designing automated auction-based market places. For this reason, we previously 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).

In the players' perspective, the agents may be able to process the protocol to collect the de nition 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 objectives of the auctioneer (to maximize revenue or e ciency), 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 de ne her action. 1.1

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 are de ning logical systems for Strategic Reasoning. The Alternating time Temporal Logic (ATL) [ 1 ] provides a logic-based analysis of strategic decisions. For representing games, the Propositional Logic of Games (GPL) [ 13 ] speci es the e ects of game playing by using inference mechanisms from propositional dynamic logic (PDL). A more practical approach to specify a game is to use the Game Description Language (GDL) [ 6 ]. The Auction Description Language (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 rst-order quanti cations over strategies in turn-based (i.e. asynchronous ) games [ 2 ]. This approach cannot model the internal structures of strategies, which prevents to easily design 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 arti cial 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. Structure of the paper Due to the space limitation, we omitted the Propositions proofs. All the proofs are available at https://epistemicadl.page.link/ EELP2020. The remainder of the paper proceeds as follows. In Section 2, we dene 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 de ne 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 e ciency 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 de nition to single-unit and single-good auctions.

De nition 1. An auction signature S is a tuple (N; V; A; ; Y ), where: (i) N = f1; 2; , ng is a nonempty nite set of agents; (ii) V N is a nite subset of natural numbers representing the range of valuations, bids and payments; (iii) A = Sr2N Ar, where Ar = fbidr(x) : x 2 V g consists of a nonempty set of actions (or bids) performed by agent r 2 N and Ar \ Ai = ; if r 6= i. For convenience, we occasionally write ar for denoting an action in Ar; (iv) = fp; q; g is a nite set of atomic propositions for specifying individual features of a state; and (v) Y = fy1; y2; g is a nite set of numerical variables for specifying numerical features of a state.

Through the rest of the paper, we will x 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 ].

De nition 2. A state transition ST-model M is a tuple (W; I; T; fRrgr2N ; L; U , ; Y ), where: (i) W is a nite nonempty set of states; (ii) I W is a set of initial states; (iii) T W n 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 A is a legality relation, describing the legal actions at each state; (vi) U : W Qr2N Ar ! W is an update function, specifying the transitions 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 2 Qr2N Ar, let d(r) be the individual action for agent r in the joint action d. Let L(w) = fa 2 A j (w; a) 2 Lg be the set of all legal actions at state w. Let Rr(w) denote the set of all states that agent r cannot distinguish from w, i.e. Rr(w) = fu 2 W : wRrug.

For any w 2 W and d 2 Qr2N Ar, we call (w; d) a move. It is a legal move if (w; d(r)) 2 L, for all r 2 N . We use the notation (w; d(r); d( r)) when it is more convenient, where d( r) 2 Qi6=r2N Ai denotes the actions of all agents except by r in the joint action d. Any set Sr f(w; d) : d(r) 2 L(w) & w 2 W & d 2 Qi2N Aig of moves is a strategy of a player r 2 N . Our notion of move and strategy is based on the asynchronous de nition from [ 18 ] and [ 19 ]. De nition 3. Two moves (w; d); (w0; d0) are imperfect recall equivalent for agent r, written (w; d) r (w0; d0), i wRrw0 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 di erently from the standard GDL, our semantics is based on moves instead of paths. This semantics allows the agent to reason about the e ects 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 de nition of reachable states and complete paths in GDL, please refer to [ 8 ]. In E-ADL, we de ne 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 2 N , a strategy Sr is complete if there is a move (w; d) 2 Sr unless L(w) \ Ar = ;, for each state w 2 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)) 2 Sr and (w; d(r)0; d( r)0) 2 Sr, then d(r) = d(r)0, for any w 2 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 nite sequence of legal moves (w0; d0); (w1; d1), ; (we; de), such that w0 2 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 2 Lz be a numerical term de ned as follows: z ::= z0 j add(z; z) j sub(z; z) j min(z; z) j max(z; z) j times(z; z) j y j maxbid, where z0 2 N; y 2 Y , a 2 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 ]. 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 2 Y in the current state.

The Epistemic Auction Description language is denoted by LE ADL and a formula ' in LE ADL is de ned by the following BNF grammar: ' ::= p j initial j terminal j legal(ar) j does(ar) j Kr' j C' j [ ar ]' j :' j ' ^ ' j z < z j z > z j z = z j r r where p 2 , r 2 N , ar 2 A and z 2 Lz .

Other connectives _; !; $; > and ? are de ned by : and ^ in the standard way. The comparison operators , and 6= are de ned 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(f#i : i 2 N g) 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(fv1; v2 : v1 < bound & v2 < boundg) 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 2 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 tiebreaking 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 de ne an abbreviation with similar meaning [ 18 ]: ' =def ^ _ (does(ar) ^ [ ar ]')

r2N ar2Ar

The formula ' means \' holds at the next state". We also use the following abbreviations from the Modal Epistemic Logic: Kbr' =def :Kr:' and E' =def Vr2N Kr', where Kbr' 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 de ne function f to de ne the meaning of numerical terms z 2 Lz. Next, a formula ' 2 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 nite sequence a; b; 2 Z. Let Y + = Y [ fmaxbidg. Numerical terms z 2 Lz n Y + have a constant evaluation, independently from a move. Their valuation can be simply assigned by function fZ (De nition 4). In De nition 5, we specify the more general function f to evaluate any z 2 Lz. De nition 4. . De ne Function fZ : Lz n Y + ! Z, assigning any formula z 2 Lz n Y + to a number in Z:

If z is in the form add(z0; z00), sub(z0; z00), min(z0; z00), max(z0; z00), times(z0, z00) or mod(z0), then fZ(z) is de ned through the application of the corresponding mathematical operators and functions. Otherwise, fZ(z) = z if z 2 Z. De nition 5. De ne Function f : W Qr2N Ar Lz ! Z, assigning any state w 2 W , joint action d 2 Qr2N Ar, and formula z 2 Lz to a number in Z: 8>fZ(z) f (w; d; z) = < Y (w; z)

>:maximum(fx : d(r) = bidr(x) & r 2 N g) De nition 6. Let M be an ST-Model. Given a move (w; d), where w 2 W and d 2 Qr2N Ar, and a formula ' 2 LADL, we say ' is true (or satis ed) in the move (w; d) under M , denoted by M j=(w;d) ', according with the following: if z 2 Z n Y + if z 2 Y if z = maxbid M j=(w;d) p M j=(w;d) :' M j=(w;d) '1 ^ '2 M j=(w;d) initial M j=(w;d) r1 M j=(w;d) terminal i

r2 i M j=(w;d) legal(ar) i M j=(w;d) does(ar) i M j=(w;d) Kr' M j=(w;d) z1 cp z2 i

i M j=(w;d) C' i i i i i p 2 M 6j=(w;d) '

(w) w 2 I w 2 T r1 Lex r2 ar 2 L(w) d(r) = ar M j=(w;d) '1 and M j=(w;d) '2 f (w; d; z1) cp f (w; d; z2); where cp 2 f>; <; =g for any w0 2 W & d0 2 Qi2N Ai, if (w; d) r (w0; d0); then M j=(w0;d0) ' for any w0 2 W & d0 2 Qi2N Ai, if (w; d) N (w0; d0); then M j=(w0;d0) ' for all c 2 Qi2N Ai where N is the transitive closure of Sr2N the lexicographical order among agents in N . r and

Lex is a relation denoting

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 globally true in an ST-Model M , written M j= ', if M j=(w;d) ' for all w 2 W and d 2 Qr2N Ar. Finally, let be a set of formulas in LADL, then M is a model of if M j= ' for all ' 2 .

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 knowledge.

Proposition 1. Let M be an ST-Model, r 2 N be an agent and ' 2 LE GDL be a formula, then 1. M j= ' ! Kr' if and only if for all w; w0 2 W and all d; d0 2 Qi2N Ai such that (w; d) r (w0; d0), M j=(w;d) ' i M j=(w0;d0) ' 2. M j= ' ! C' if and only if for all w; w0 2 W and all d; d0 2 Qi2N Ai such that (w; d) N (w0; d0), M j=(w;d) ' i M j=(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 rst de ne the auction signature, written Sbli = fN; V; A, bli; Yblig, where bli = fg, Ybli = fpaymentr, allocr; #i : r 2 N g. 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 i we are not in an initial state (Rule 2). Rule 3 speci es 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. Let winsr;x =def does(bidr(x)) ^ Vi6=r2N (:does(bidi(x)) _ r i) and r 2 N , 1. initial $ Vi2N paymenti = 0 ^ alloci = 0 2. terminal $ :initial 3. Vx2V (legal(bidr(x)) $ :terminal _ (terminal ^ x = 0)) 4. Wx2V (initial ^ maxbid = x ^ winsr;x $ (allocr = 1 ^ paymentr = x)) 65.. WVx2V (initial ^ :winsr;x ! (allocr = 0 ^ paymentr = 0))

x2V;y2f0;1g terminal ^ allocr = y ^ paymentr = x ! paymentr = x) (allocr = y ^ 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 r 2 N , 1. Vx2V (#r = x ! Kr(#r = x)) 2. W 3. Vx2V #r = x

x2V (does(bidr(x)) ! Krdoes(bidr(x))) 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; fRr;bligr2N ; 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 = fa; b; cg. 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

Proposition 3 shows that tocol.

bli (and resp.

bli;N ) represents a one-shot proProposition 3. Mbli j= 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 ' 2 LE GDL, 1. If Mbli j= 2. If Mbli j= bli ! ', then C' bli;N ! ', then E'

Up to now, we focus on the protocol de nition 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 ' 2 LE ADL, let S(') = f(w; d) : M j=(w;d) 'g. S(') denotes all moves under which ' is valid. De nition 7. Given a model M and a strategy Sr for agent r 2 N , a formula ' 2 LE ADL is a representation of Sr i Sr = S('). If S(') is a representation of a functional strategy, then ' is a strategy rule.

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 2 N , the formula outbidr =def _

does(bidr(v)) ^ v2V v = min f#r; x : Kr x = add(max(f#i : i 6= r 2 N g); 1) & x 2 V g is a strategy rule where the agent outbids the higher private value of her opponents or bids its own value if she knows the other agents' private values are greater then her value.

Let us assume the agent a 2 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 rst-price auction, we can see that b and c would not maximize their utility by bidding above their private value. Thereby, the strategy outbida consists of outbidding the adversaries private value, that is to bid 3.

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 e ciency, strategy-proofness and individual rationality. For the game-theoretic de nition of mechanism design and its properties, please refer to [ 12 ], [ 4 ] and [ 15 ].

Representing Classical Properties of Auctions

Assuming the agents have private valuations #1; ; #n in V . Given an agent r 2 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, e ciency and individual rationality properties in E-ADL.

We assume an agent is rational by the standard utility maximization de nition: a rational agent has a private valuation and tries to maximize her payo . 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 2 N is weakly rational in the move (w; d) if M j=(w;d) ^ (does(ar) ^ legal(ar) ! ^

(:legal(br)_ ar2Ar br6=ar2Ar _ (K^ r([ar]utility(#r; r) = x ^ [br]utility(#r; r) = x0 ^ x x0)))) x;x02V

We denote rat(w) as the set of joint actions d 2 Qr2N Ar such that (w; d) 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 2 W is strategy-proof for an agent r 2 N , if bidding her private values leads to a better (or equal) utility than bidding any other value, for any joint action d 2 Qi2N Ai. In E-ADL, we express this condition by using the action execution operator as follows:

SPr =def _ ([bidr(#r)]utility(#r; r) = x x2V ^

^ v6=#r2V [bidr(v)]utility(#r; r) x)

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 strategy-proof in that state for all agents and joint actions, i.e. SPN =def Vr2N SPr.

For verifying whether an auction is strategy-proof, we do not make any assumption 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 2 Ibli, d 2 Qr2N Ar and r 2 N , Mbli 6j= SPr, and consequently, Mbli 6j= SPN .

Example 2. We can construct a strategy-proof blind auction by changing the payment rule from bli. Let us de ne 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:

_ second;first;x1; ;xn2V

initial ^ maxbid = f irst ^ winsr;first^ second = max(f0; xr : xr 6= maxbid & does(bidr(xr) & r 2 N )g) ! (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 2 Ivic, d 2 Qr2N Ar and r 2 N , Mvic j=(w;d) SPr, and consequently, Mvic j=(w;d) SPN .

E ciency We say that a mechanism is e cient 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. E ciency (EF ) in a state w 2 W , is de ned by the validity of the following E-ADL formula for any joint action d 2 rat(w):

EF =def ^ allocr = 1 ! #r = max(f#i : i 2 N g)

r2N

E ciency is an epistemic property: to check if an auction is e cient, 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 2 Wbli, w0 2 Wvic and for all d 2 rat(w), d0 2 rat(w0), (i) Mbli 6j=(w;d) EF and (ii) Mvic j=(w0;d0) EF .

If we did not assume weakly rationality of the agents, the auction represented by Mvic would not be e cient. Even if it is strategy-proof, we still need to link this property to the assumption they will behave rationally. 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 2 W for an agent r if by participating she can achieve a utility greater or equal to zero, for any joint action d 2 Qi2N Ai. The individual-rationality constraint is de ned by the following E-ADL formula:

IRr =def _ [ar]utility(#r; r) a2Ar 0

Similarly, we can verify whether the action is individual-rational for every agent in N by the following formula: IRN =def Vr2N 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 2 Wbli, w 2 Wvic, d 2 Qr2N Ar and r 2 N , (i) Mbli j=(w;d) IRr, and consequently, Mbli j=(w;d) IRN ; (ii) Mvic j=(w;d) IRr, and consequently, Mvic j=(w;d) IRN .

Note that even if an auction has a property (such as strategy-proofness, e ciency, or individual rationality), it does not mean that the agents are individually 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 de ning strategies. 5.1

Knowledge about auction properties

Agents can have di erent levels of knowledge over auction properties, by combining the C and Kr operators and properties formulas. For instance, KrSPr 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 di erent 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 2 W , a joint action d 2 Qr2N Ai and an agent r 2 N , if r weakly rational then

M j=(w;d) KrSPr ^ legal(bidr(#r)) ! does(bidr(#r)) Corollary 1. Given r 2 N , the formula does(bidr(#r)) is a strategy rule. To check whether the auction is strategy-proof, i.e. M j=(w;d) KrSPr, 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.

If an agent r knows that an auction is e cient 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 payo . This information about e ciency may be useful if the agent needs to choose to participate in di erent auctions.

Proposition 11. Assuming the agents are weakly rational, given an ST-model M , a state w 2 W and any joint action in d 2 rat(w),

CEF ^ Kr _ #i > #r ! Kr i2N allocr = 0

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 di erent weakly rational actions. For instance, the First-Price Blind Auction denoted by Mbli is neither strategy-proof nor e cient and there may be several actions complying with the weakly rationality condition. This is a trade-o 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 di erent 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, e ciency, 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 de nitions 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 2p-complete for EGDL [ 8 ]. These complexity results are reasonable when compared to other languages for strategic reasoning, such as ATL and its variants. The main di erence between the model-checking for E-ADL and EGDL is the action modality, whose truth condition refers to every possible 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 . Journal 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 Arti cial 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 representing 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 e ciency . 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 playing . 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 )