# formal_verification_of_bayesian_mechanisms__4f29c125.pdf

Formal Verification of Bayesian Mechanisms

Munyque Mittelmann1, Bastien Maubert1, Aniello Murano1, Laurent Perrussel2

1 Universit a degli Studi di Napoli Federico II , Italy 2 IRIT - Universit e Toulouse Capitole, France {munyque.mittelmann, laurent.perrussel}@ut-capitole.fr, {bastien.maubert, nello.murano}@gmail.com

In this paper, for the first time, we study the formal verification of Bayesian mechanisms through strategic reasoning. We rely on the framework of Probabilistic Strategy Logic (PSL), which is well-suited for representing and verifying multi-agent systems with incomplete information. We take advantage of the recent results on the decidability of PSL model checking under memoryless strategies, and reduce the problem of formally verifying Bayesian mechanisms to PSL model checking. We show how to encode Bayesian-Nash equilibrium and economical properties, and illustrate our approach with different kinds of mechanisms.

Introduction The design of mechanisms for aggregating preferences while achieving a socially desirable outcome is a central problem in Multi-Agent Systems (MAS). For example, an auction is a mechanism that combines bids into a choice of allocation and payments (Klemperer 1999). In recent years, there has been a growing effort at designing novel mechanisms for a wide variety of problems and settings, including peer selection (Aziz et al. 2019), hedonic coalition formation games (Bil o et al. 2018; Flammini, Kodric, and Varricchio 2022), sponsored search auctions (Gatti et al. 2015), and diffusion auctions (Li et al. 2022). The advantages of automating the development and/or analysis of mechanisms are numerous (Okada, Todo, and Yokoo 2019), as these tasks require deep knowledge of mathematics and game theory. Furthermore, the automated approach can yield better mechanisms (in terms of the designing criteria) because it capitalizes on the particulars of the setting, e.g. the probabilistic (or other) information that the designer has about the agents preferences (Sandholm 2003). Automated Mechanism Design (AMD) was introduced by Conitzer and Sandholm (2002). In this field, designing mechanisms is usually modelled as a computational optimization problem. Different techniques may be used such as neural networks (Shen, Tang, and Zuo 2019), statistical machine learning (Narasimhan, Agarwal, and Parkes 2016), black-box optimization algorithms (Vorobeychik, Reeves, and Wellman 2007), as well as evolutionary search methods (Niu et al. 2012). All these techniques treat AMD by

Copyright 2022, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

solving it for a specific setting: no general perspective is considered and consequently typical properties are always defined in terms of the specific problem. In line with the well established logical approach to system verification (Clarke et al. 2018), the work presented in (Wooldridge et al. 2007) advocates the use of Alternatingtime Temporal Logic (ATL) (Alur, Henzinger, and Kupferman 2002) to reason about mechanism design. Due to ATL s limitations regarding the expression of solution concepts (such as Nash equilibria) as well as handling quantitative aspects, recent works proposed the use of variants of Quantitative Strategy Logic (SL[F]) (Bouyer et al. 2019) for reasoning about mechanisms. In (Maubert et al. 2021; Mittelmann 2022), the authors demonstrate how to represent and verify knowledge-based benchmarks and properties such as efficiency and strategyproofness in Epistemic SL[F]. Similarly, SL[F] with natural strategies have been considered for reasoning with bounded recall (Belardinelli et al. 2022). Finally, the automated design of deterministic mechanisms was reduced to SL[F]-synthesis in (Mittelmann et al. 2022). However, SL[F] semantics is deterministic and thus the logic is unable to express probabilistic features, which are essential when considering Bayesian and randomized mechanisms. This paper shows the potential of using the probabilistic version of Strategy Logic (Probabilistic Strategy Logic, PSL) (Aminof et al. 2019) for AMD. Model-Checking PSL-formulas is decidable in 3-EXPSPACE in the context of memoryless strategy, a common assumption in Mechanism Design. As illustrated by recent work on the subject (Feldman et al. 2022; Varloot and Laraki 2022), randomness and imperfect information are foundational and must be addressed by any formal verification technique for Bayesian mechanisms. Generalizing from the deterministic to the probabilistic setting is challenging due to several aspects. First, the wide and heterogeneous range of settings considered in the literature obscures the path for a general and formal approach to verification. The setting may consider deterministic or randomized mechanisms, incomplete information about agents types (Bayesian mechanisms), mixed or pure strategies, and direct or indirect mechanisms (iterative protocols). Second, considering Bayesian mechanisms brings out different methods for evaluating a mechanism according to the time-line for revealing the incomplete

The Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23)

information as the mechanism is executed. We consider a very general Bayesian framework for mechanism design and show how to capture it with PSL. This allows for automatic verification of a wide class of Bayesian mechanisms through PSL model checking, and motivates further research on applications of logic-based approaches for AMD.

Related Work Logic-based approaches have been widely and successfully applied for probabilistic verification of MAS. For instance, probabilistic model-checking techniques have been used for verifying and analysing a drone swarm system (Lomuscio and Pirovano 2020), negotiation games (Ballarini, Fisher, and Wooldridge 2009), team formation protocols (Chen et al. 2011), and stochastic behaviours in dispersion games (Hao et al. 2012), to name a few. (Gutierrez et al. 2021) investigates rational verification for both non-cooperative games and cooperative games in the qualitative probabilistic setting. (Kwiatkowska et al. 2022) details how verification techniques can be developed for concurrent stochastic games and next implemented in PRISM-games model checker.

Outline The paper is organized as follows; first, we recall PSL. Next, we show how to represent a general notion of Bayesian mechanism as a stochastic transition system. Then, we show how to represent and verify different concepts of equilibrium. Next, we show how classical properties of Bayesian mechanism can be encoded in PSL and verified via model checking.

Preliminaries Throughout this paper, we fix finite non-empty sets of agents Ag, atomic propositions AP and strategy variables Var. We write o for a tuple of objects (oa)a Ag, one for each agent, and such tuples are called profiles. Given a profile o and a Ag, we let oa be agent a s component, and o a is (ob)b =a. Similarly, we let Ag a = Ag \ {a}.

Distributions Let X be a finite non-empty set. A distribution over X is a function d : X [0, 1] such that P x X d(x) = 1, and Dist(X) is the set of distributions over X. We write x d for d(x) > 0. If d(x) = 1 for some element x X, then d is a point distribution. If, for i I, di is a distribution over Xi, then, writing X = Q i I Xi, the product distribution of the di is the distribution d : X [0, 1] defined by d(x) = Q i I di(xi).

Markov Chains A Markov chain M is a tuple (Q, p) where Q is a set of states and p Dist(Q Q) is a distribution. The values p(s, t) are called transition probabilities of M. A path is an infinite sequence of states.

Systems We now introduce the formal models we use to represent Bayesian mechanisms. Definition 1. A multi-agent stochastic transition system (or simply system) G is a tuple (Ac, V, v , δ, ℓ, L) where (i) Ac is a finite non-empty set of actions, (ii) V is a finite non-empty set of states, (iii) v V is an initial state, (iv) δ : V Ac Ag Dist(V ) is a transition function, (v) ℓ: V 2AP is a labelling function, and (vi) L : V 2Ac is a legality function defining the available actions in each state.

A joint-action c is an element of Ac Ag. We say that G is deterministic (instead of stochastic) if every δ(v, c) is a point distribution.

Plays A play in a system G is an infinite sequence π = v0v1 of states such that there exists a sequence c0c1 of joint-actions such that ci L(vi)Ag and vi+1 δ(vi, ci) for every i. We write πi for vi.

Strategies A (memoryless) strategy is a function σ : V Dist(Ac). Let Str denote the set of all strategies. A strategy profile is a tuple σ of strategies, one for each agent. We write σa for the strategy of agent a in the strategy profile σ. Next we recall Probabilistic Strategy Logic (PSL), introduced by Aminof et al. (2019).

PSL Syntax The syntax of PSL is defined by the following grammar:

φ ::= p | φ | φ φ | s.φ | τ τ

τ ::= c | τ 1 | τ τ | τ + τ | τ τ | Ps(ψ) ψ ::= φ | ψ | ψ ψ | Xψ | ψUψ

where p AP, s Var, c Q and s Var Ag. As usual we write φ φ for φ φ , and τ = τ for τ τ τ τ .

PSL Semantics Formulas of PSL are interpreted over multi-agent stochastic transition systems. Temporal operators next (X) and until (U) have their usual meaning, and strategy quantification x.φ means that there exists a strategy such that φ holds, as usual in Strategy Logic (Mogavero et al. 2014). The characteristic feature of PSL consists in terms of the form Ps(ψ), whose intuitive meaning is that if each agent a uses the strategy assigned to sa then property ψ holds with probability Ps(ψ) in the resulting behaviour of the system.

Probability Space on Outcomes An outcome of a strategy profile σ and a state v is a play π that starts with v and is extended by σ, i.e., π0 = v, and for every k 0 there exists ck σ(πk) such that πk+1 δ(πk, ck). The set of outcomes of a strategy profile σ and state v is denoted out(σ, v). A given system G, strategy profile σ, and state v induce an infinite-state Markov chain Mσ,v whose states are the finite prefixes of plays in out(σ, v). Such finite prefixes of plays are called histories and written h, and we let last(h) denote the last state in h. Transition probabilities in Mσ,v are defined as p(h, hv ) = P c Ac Ag σ(h)(c) δ(last(h), c)(v ). The Markov chain Mσ,v induces a canonical probability space on its set of infinite paths (Kemeny, Snell, and Knapp 1976), which can be identified with the set of plays in out(σ, v). The corresponding measure is denoted µσ,v.1

Assignments An assignment is a partial function A : Var Str. A binding is a function β : Ag Var that maps agents to strategies. If the image of a binding β is contained in the domain of A, then A β : Ag Str is a joint strategy. For an assignment A, variable s and strategy σ, A[s 7 σ] is

1This is a classic construction, see (Berthon et al. 2020).

the assignment that maps s to σ and is otherwise equal to A. Notation A[s 7 σ] is defined similarly for a variable profile s = (sa)a Ag and a strategy profile σ = (σa)a Ag. A variable s is free in a formula if it has a subformula of the form Ps(ψ) where s appears in s but Ps(ψ) is not in the scope of any s. A state formula with no free variables is called a sentence.

PSL Semantics PSL state formulas are interpreted in a transition system G, an assignment A : Var Str whose domain contains the free variables of the formula, and a state v G. We only give the inductive cases for strategy quantification and comparison of expected outcomes, and refer to (Aminof et al. 2019) for the other standard cases.

G, A, v |= p if p ℓ(v) G, A, v |= s.φ if σ Str. G, A[s 7 σ], v |= φ G, A, v |= τ1 τ2 if val A,v(τ1) val A,v(τ2)

where val A,v(c) = c and val A,v(τ 1) = (val A,v(τ)) 1

val A,v(τ τ ) = val A,v(τ) val A,v(τ ) for { , +, } val A,v(Ps(ψ)) = µA β,v({π : G, A, π, 0 |= ψ}), where β is the binding such that β(a) = sa for each a Ag2. If φ is a sentence, the truth of G, A, v |= φ does not depend on A. Thus, as usual, we write G, v |= φ to mean that G, A, v |= φ for some (equivalently all) A.

Model Checking Model Checking problem consists of deciding whether G, A, v |= φ. It is decidable in the memoryless context (Aminof et al. 2019); as usual, perfect recall strategy is not decidable. More precisely, computational complexity is 3-EXPSPACE, w.r.t. the size of the φ and EXPSPACE w.r.t. the size of G.

Bayesian Mechanism Design with PSL Next, we recall mechanisms and we show how to model them as stochastic systems with the purpose of enabling the verification of properties under incomplete information.

Bayesian Mechanism Design A mechanism is a game that maps agents strategies to a collective choice from a finite set of alternatives Alt (Nisan et al. 2007). In the case of randomized mechanisms, strategies are mapped to probability distributions over Alt. As monetary transfers are often a central feature of the decision, we follow (Parkes 2001) and write each alternative as a tuple (x, p) where x is a choice and pa Z is the payment for agent a3. Each agent a has a type θa Θa that specifies how she values each possible choice, where Θa is a (finite) set of possible types for agent a. The value an agent a with type θa attributes to a choice x is defined by the valuation function va(x, θa) Z. We assume agents have quasi-linear utility, so that agent a s utility for an alternative α = (x, p) is

2G, A, π, 0 |= ψ evaluates path formula ψ in π0. 3Notice that mechanisms without monetary transfers can be handled by setting all agents payments to zero.

ua(θa, α) = va(x, θa) pa. We let Θ = Q a Ag Θa, and we write θ = (θa)a Ag Θ for a type profile, which assigns a type θa to each agent a. In Bayesian mechanisms we consider incomplete information over the agents types (Hartline 2012). The type θa of agent a is drawn from a publicly known distribution d Dist(Θa), d(θa) is the a priori probability that agent a has type θa.

Agents strategies They depend on their type, we let σθ a Stra denote a strategy of agent a with type θ, and we also write σa = (σθ1 a , ..., σθn a ) for a tuple containing one strategy for each possible type of a, where Θa = {θ1, ..., θn}. A strategy σa for an agent a is thus a tuple (σθ1 a , ..., σθn a ). Given a strategy profile σ = (σa)a Ag, we let σ(θ) = (σθa a )a Ag denote strategies for all agents when they have types θ, and d(θ) (resp. d(θ a|θa) ) denote the probability that θ is drawn (resp. θ a is drawn given that a has type θa).

Social Choice Function In the probabilistic setting, a social choice function maps each possible agents type profile to a probability distribution over the alternatives.

Definition 2. A (randomized) social choice function (SCF) f : Θ Dist(Alt) is a function that maps type profiles to probability distributions over the set of alternatives.

Given a type profile θ, we may write df,θ instead of f(θ) for the probability distribution assigned by f to θ.

Mechanism They are similar in spirit to SCFs except that instead of type profiles they map strategy profiles to probability distributions over the set of alternatives.

Definition 3. A (randomized) mechanism is a function M : Q a Ag Stra Dist(Alt).

Given a strategy profile σ, we may write d M,σ instead of M(σ). A direct mechanism is a mechanism where the strategy sets are the agents sets of possible types. A direct mechanism is thus also an SCF (Narahari 2014). In those mechanisms, a strategy of particular interest is the truth-revelation strategy, in which the agent reports its real type: given type θa for each agent a, the truth-revelation strategy ˆθa for agent a is the strategy such that ˆθa(v) = θa, for any position v. A deterministic mechanism chooses an alternative for each strategy profile. This is the case when, for every strategy profile σ, the mechanism assigns a point distribution, e.g., d M,σ(α) = 1 for some alternative α. Deterministic SCFs are captured similarly. Example 1 (BIN-TAC auction). We give an informal description of the Buy-It-Now or Take-a-Chance (BIN-TAC) auction (Celis et al. 2014), a randomized mechanism. In this auction, a good is auctioned with a buy-it-now price r, set relatively high. If a single bidder chooses buy-it now (BIN), she gets the good for price r. If more than one bidder takes the BIN option, a new bidding round is held between those bidders with reserve price4 r. Then, the winner is the highest bidder and her payment is the second-highest bid. If no one

4The reserve price denotes the minimum price that the seller is willing to accept.

chooses to BIN, a take-a-chance (TAC) auction is held between all bidders, with a TAC-reserve price r (0 r r). The TAC auction proceeds by choosing the top h bidders uniformly at random, and if her bid exceeds the reserve r , she wins the auction and pay the maximum of the reserve and the (h + 1)-th bid (if it exists). Ties among the h-highest bidders are broken randomly prior to the random allocation. In our approach, mechanisms are represented by stochastic transition systems which define the possible actions and strategies of the agents and their outcomes: such transition systems should encode agents choice and payment. Definition 4 (Mechanism as a system). Assume that AP contains {ter, choicex, paypa a | (x, p) Alt, a Ag} where ter specifies whether a state is terminal, choicex denotes that the choice x was selected, and paypa a denotes that pa is the payment chosen for agent a. Given a system G = (Ac, V, v , δ, ℓ, L) over the atomic propositions AP, we say that G is the system representation of the mechanism M : Q a Ag Stra Dist(Alt) if it satisfies the following: i every play eventually reaches a terminal position, i.e., a sink5 where proposition ter has value true and alα holds for exactly one α Alt; ii in all non-terminal positions, ter has value false; iii for every α Alt and σ Q a Ag Stra,

G, A[s 7 σ], v |= Ps(F(ter alα)) = d M,σ(α)

where alα := choicex V a Ag paypa a is a shortcut denoting that an alternative α = (x, p) was chosen. Example 2 (BIN-TAC auction (cont.)). We now resume the BIN-TAC auction example and show how to represent it as a system. Let w be an upper bound for values used in the mechanism. For simplicity, we consider the lower bound to be 0. Assume the type of each bidder is drawn identically and independently from a distribution over Θ [0, w]. We let r (0, w) denote the BIN price, r [0, r] be the TAC reserve price, and h [1, n] be the randomization parameter. The set of alternatives is Alt BIN-TAC = {(xa, (pa)a Ag) : a Ag {none} & pa [0, w]}, where pa is the payment for a and xa denotes the winner of the item (or none ). Define the mechanism GBIN-TAC = (Ac, V, v , δ, ℓ, L) over AP = {price, choicex, paypa a , ter : a Ag & (x, p) Alt}, where: Ac = {BIN, TAC, bidx : x Θ}; v V for each v = win, p, mode, (acta)a Ag , where win Ag {none} denotes the winner, mode {init, BIN, TAC, t}, p [0, w], and acta Ac {noop} denotes agent a s last action; The initial position is v = none, r, init, (noop)a Ag . For each position v = win, p, mode, (acta)a Ag , the legality function is as follows: c L(v) if either (i) mode = init and c {TAC, BIN}, or (ii) mode {BIN, TAC} and c Ac \ {BIN, TAC}, or (iii) mode = t. For each position v = win, p, mode, (acta)a Ag and joint action c = (ca)a Ag, transition δ(v, c) is as follows:

5A sink is a position that loops for all action profiles.

Initial TAC

choice = x1st pay1st = x2nd pay 1st = 0

choice = xa paya = r pay a = 0

choice = xa1 paya1 = x(h+1)th pay a1 = 0

choice = xah payah = x(h+1)th pay ah = 0

c0,a = BIN and c0, a = TAC

c0,a = c0,b = BIN, for a = b

c1,a = bidxa, for each a Ag

c1,a = bidxa, for each a Ag

c1,a = bidxa, for each a Ag

Figure 1: System representation of the BIN-TAC Auction. Red nodes represent terminal positions and specify the alternative chosen. Edges are transitions, with the label specifying the joint actions c0 and c1 performed in each stage. Continuous lines are transitions with probability 1 and dashed lines are transitions with probability 1

h. For simplicity, we omit the nodes in which there is no winner (that is, when the highest bid is below the reserve price).

Let Ag BIN = {a : a Ag & acta = BIN}. If mode = BIN, ca is in the form bidxa for each a Ag BIN, and xb r for some b then, δ(v, c) = win, p , t, (ca)a Ag with probability 1, where win = a if xa = maxb Ag(xb) (ties are broken according to a predefined order) and p = max(r, maxb Ag BIN\{a:xa=maxa Ag(xa )}(xb));

Let Ag TAC = {a : a Ag & acta = TAC}. If mode = TAC, ca is in the form bidxa for each a Ag TAC and xb r for some b, let Ag TACh = {a : xa is one of the h-highest values in {xa : a Ag TAC}. Then, let δ(v, c) = a, p , t, (ca)a Ag with probability 1 h for each a Ag TACh, where p = max(r , x) and x is the (h + 1)-highest bid in {xa : a Ag TACh}. If mode = BIN (resp., mode = TAC), ca is in the form bidxa with xa < r (resp., xa < r ) for each a Ag BIN, then, δ(v, c) = none, 0, t, (ca)a Ag with probability 1; The transitions when mode = init are shown in Figure 1. Other cases are sinks, i.e., δ(v, c) = v with prob. 1. For each v = win, p, mode, (acta)a Ag and each a Ag, the labeling is defined as follows: choicex ℓ(v) if x = win, payp a ℓ(v) if a = win, pay0 a ℓ(v) if a = win, and ter ℓ(v) if mode = t.

Bayesian Mechanism Time-Line The concepts of ex ante, interim, and ex post properties provide a way to consider the nuances between various mechanisms. These terms refer to the time-line of the game (see Figure 2), in relation to the incomplete information about types (Chawla and Sivan 2014). Initially, agents have incomplete information about all agents type (ex ante). Then, each agent realizes her own type, while remaining uncertain

interim ex post ex ante

Figure 2: The information disclosure time-line of a mechanism. Ex ante properties are evaluated based on the type profile distribution, interim properties are calculated using the distributions of type profiles given one agent s type, and ex post properties are evaluated given a fixed type profile.

about others (interim). Finally, all types are known to all (ex post). In other words, in ex ante no type is known, and we thus consider the expectation over all type profiles; in interim each agent knows her own type, and we consider the expectation over other agents types; finally in ex post, all types are known, and we only consider the actual types6. We now show how to use PSL for evaluating a mechanism in relation to ex ante, interim and ex post properties. First we define the corresponding notions of expected utility.

Expected utility We recall the definition of expected utilities for Bayesian games, adapted from (Leyton-Brown and Shoham 2008) to our setting. The expected utility for agent a induced by the mechanism M given the strategies σ and type profile θ in ex post is computed as follows: Ee.p. a (M, σ, θ) := P α Alt d M,σ(θ)(α) ua(θa, α). Given a type θa for agent a, her interim expected utility is Ee.i. a (M, σ, θa) := P θ a Θ a d(θ a|θa) Ee.p. a (M, σ, (θ a, θa)). Finally, the ex ante expected utility for a is Ee.a. a (M, σ) := P θ Θ d(θ) Ee.p. a (M, σ, θ). The ex post, interim and ex ante expected utilities induced by a social choice function are defined analogously and denoted Ee.p. a (f, θ), Ee.i. a (f, θa), and Ee.a. a (f), resp. Let s(θ) := (sθ a)a Ag. We write the following PSLarithmetic terms to capture the ex ante, interim and ex post expected utilities of agent a, respectively, where s is a tuple of strategy variables for each agent:

Ee.p. a (s, θ) := X

α Alt ua(θa, α) Ps(θ)(F(ter alα))

Ee.i. a (s, θa) := X

θ a Θ a d(θ a|θa) Ee.p. a (s, (θ a, θa))

Ee.a. a (s) := X

θ Θ d(θ) Ee.p. a (s, θ)

The following result is important as it will lead to define equilibrium in terms of PSL-formulas.

6Note that in our setting with probabilistic transitions and strategies, fixing types does not determine a unique outcome, as it does in deterministic mechanisms with pure strategies.

Theorem 1. Let G be a system representing a mechanism M, θ a type profile, σ a strategy profile, s a variable profile, and A an assignment such that for all a, A(sa) = σa. Then for all agents a it holds that

G, A, v |= Ee.a. a (s, θ) = Ee.a. a (M, σ, θ)

Ee.i. a (s, θa) = Ee.i. a (M, σ, θa) Ee.p. a (s) = Ee.p. a (M, σ)

Best Response Equilibrium A strategy profile σ is an ex ante best response equilibrium (BREe.a.) if for every type profile θ no agent can increase her expected utility with a unilateral change of strategy given the distributional information about all agents types. That is, for each agent a, playing her strategy σa is the ex-ante best response to the others playing σ a. Let s = (sa)a Ag be a profile of strategy variables. First, the fact that the strategies represented by s form an ex ante best response equilibrium (BREe.a.) can be expressed in PSL with the formula

BREe.a.(s) :=

a Ag ta. Ee.a. a ((s a, ta)) Ee.a. a (s)

A strategy profile σ is a Nash equilibrium (NE) if for every θ no agent can increase her expected utility with a unilateral change of strategy (Nisan et al. 2007). We let

a Ag ta. Ee.p. a ((s a, ta), θ) Ee.p. a (s, θ)

Finally, a strategy profile σ is a Bayesian-Nash equilibrium (BNE) if for every player a and every θa, σ is the best response that a has to σ a when her type is θa, in expectation over the other types θ a (Nisan et al. 2007). The following formula expresses that strategy profile s is a BNE:

a Ag,θa Θa ta. Ee.i. a ((s a, ta), θa) Ee.i. a (s, θa)

The key difference between BNE and NE is that in BNE an agent s strategy must be a best-response given distributional information about the preferences of other agents, while in NE an agent s strategy must be a bestresponse to the actual strategies of the other agents (Parkes 2001). Through the rest of this paper, we let E {BREe.a., BNE, NE} denote an equilibrium concept. The following theorem shows that checking the existence of such complex equilibria can be rephrased in terms of model checking of PSL-formulas. Theorem 2. Let G be a system representing a mechanism M, σ a strategy profile, s a variable profile, and A an assignment such that for all a, A(sa) = σa. Then it holds that

G, A, v |= E(s) iff σ is a E in M

Example 3 (BIN-TAC auction (cont.)). Now we resume Example 2 and we focus on characterizing equilibrium strategies under BIN-TAC, based on the results of (Celis et al. 2014). If multiple agents choose to BIN, it is weakly dominant for agents to bid their valuations. Truth-telling is also

weakly dominant in the TAC auction. Taking these auction strategies as given, we turn to the decision whether to buyit-now or take-a-chance. Following (Celis et al. 2014), in a symmetric equilibrium, the BIN decision takes a threshold form: for some threshold θ, agent a with type θa > θ elect to BIN, and the rest do not. Let the random variable Xj be the j-th highest draw in an independent sample of size n 1 from a distribution d (the j-th highest rival valuation) and X be the maximum of Xh and the TAC reserve price r .

Proposition 1 ((Celis et al. 2014)). There exists a unique symmetric pure strategy Bayes-Nash equilibrium7, characterized by a threshold θ (0, w]. Let σa be a strategy for agent a such that σa(v) = bidˆθa(v) for each v = v and h > 1 be a constant. Now, we characterize the action assigned in v . If w p < 1 h E[ w X |X1 < w] then θ = w and σa(v ) = TAC. Otherwise, θ is the solution of θ = p + 1

h E[ w X |X1 < θ]. Then, σa(v ) = BIN if θ θ and σa(v ) = TAC otherwise. We then have: GBIN-TAC, A[s σ], v |= BNE(σ).

The intuition is that since strategies have a threshold form, the choice is relevant only when there are no highervaluation bidders, since these bidders will BIN and win.

Verifying Mechanism Properties As we are now able to represent mechanisms as stochastic systems and complex Bayesian solution concepts as PSLformulas, we are in a position for investigating classical Bayesian Mechanism Design properties: we show how evaluating such properties boils down to model checking.

Implementation of an SCF Given an SCF f, the mechanism design problem consists in defining game rules (the mechanism) to implement f despite agents individual interests. Game-theoretic concepts are used for analysing the outcome of the mechanism. In the deterministic setting, a mechanism implements an SCF f if the alternative chosen when agents follow equilibrium strategies is the alternative chosen by f for all possible agent preferences. Different equilibrium concepts may be used to define implementation, including Bayesian-Nash and dominant strategies (Parkes 2001). We generalize to our setting the definitions of implementation of SCFs from (Parkes 2001; Conitzer and Sandholm 2002). We center this definition on the equilibrium notions introduced above, but the implementation may be defined using some other concept (Parkes 2001).

Definition 5. A mechanism E-implements an SCF f if there exists a strategy profile σ(θ) that is an E-equilibrium in the mechanism and d M,σ(θ)(α) = df,θ(α) for each alternative α Alt and θ.

In the deterministic setting, Definition 5 corresponds to the mechanism implementation from (Parkes 2001). We generalize the definition to take into account randomized

7A symmetric equilibrium is an equilibrium where all players use the same strategy.

mechanisms inline with (Conitzer and Sandholm 2002). To do so, we first introduce the following macros:

sa := sθ1 a ... sθn a , sa := sθ1 a ... sθn a , s := sa1... san

where Θa = {θ1, ..., θn}. Let φf,s be a formula denoting that f assigns the same probability distribution as the mechanism under strategies s, for any types:

θ Θ,α Alt Ps(θ)(Fter alα) = df,θ(α)

Theorem 3. Let G be a system representing a mechanism M. Given an equilibrium concept E {BREe.a., NE, BNE}, assume that M E-implements an SCF f. Then it holds that:

G, v |= s. E(s) φf,s

Example 4 (Dutch auction). In a Dutch auction, the price of a good starts at a high value and is gradually lowered until a bidder accepts the going price. Then she gets the good and the auction ends. The choices in the α include the option of selecting either agent as the winner or not selling the item (in such case the winner is none ). In each alternative, an agent s payment may be either 0 or the reserve price minus dec times the number of rounds and at most one agent may pay more than 0. The Dutch auction is represented by the mechanism Gdut, defined similarly to Example 2. This auction is a BNE-implementation of the first price auction (Narahari 2014): Proposition 2. Let ffirst : Θ Altdut be a deterministic SCF defined as follows: ffirst(θ) = (x, p) where x = a for the agent such that va(a, θa) = maxa Ag va (a , θa ) (ties are broken based on the order ), pa = va(a, θa) if x = a, and pa = 0 otherwise. We have that: Gdut BNEimplements ffirst, or, equivalently, Gdut, v |= s. BNE(s) V θ Θ,α Alt Ps(θ)(Fter alα) = dffirst,θ(α).

That is, BNE implementation requires that there exists an (interim) best response equilibrium from which, with probability 1, the alternative assigned by the mechanism is the same as the one chosen by the SCF. Similarly, NE implementation requires that there exists an (ex post) best response equilibrium from which, with probability 1, the alternative assigned by the mechanism is the same as the one chosen by the SCF. We are now able to evaluate mechanisms in relation to classical economic properties in ex ante, interim and ex post equilibrium.

Mechanism Properties Mechanisms are designed with the goal of achieving desirable properties. We illustrate a number of those properties and use them for characterizing a classical mechanism. According to the modeled problem and target properties, different stages of information disclosure in the mechanism may be relevant. For instance, individual rationality (IR) captures the idea that an agent can decide whether or not to participate, in the sense that her expected utility induced by the

game is no worse then her utility outside the mechanism. The most natural definition of IR is interim (Parkes 2001), as it expresses the case that the agent has incentive for participating when she considers her own preferences and has only distributional information about others. An SCF f is (interim) individually rational if for every θ Θ, Ee.i. a (f, θa) 0 for each agent a. The following formula rephrases individual rationality with respect to some strategy variable s and type profile θ:

IR(s, θ) :=

a Ag 0 Ee.i. a (s, θa)

Theorem 4. Let G be a system representing a mechanism M. The SCF f E-implemented by M is (interim) individual rational iff G, v |= s. E(s) F(ter φf,s V θ Θ IR(s, θ)). In order to collect truthful preferences, the mechanism can be designed to incentivize the agents to tell the truth. In Dominant Strategy Incentive Compatible (DSIC), truth revelation is the best strategy for each agent irrespective of what is reported by the other agents. As DSIC is a strong requirement, a useful relaxation is when truth revelation is the agents best response in expectation of the types of others (Bayesian Incentive Compatible, BIC) (Narahari 2014). Let Ac = a AgΘa. A direct mechanism M is Bayesian Incentive Compatible if the truth-revealing strategy profile (ˆθa)a Ag is a BNE in M for any θ Θ. In other words, BIC holds if the corresponding PSL definition of BNE holds: Proposition 3. Let G be a system representing a mechanism M. M is Bayesian Incentive Compatible iff for any θ Θ: G, A[s (ˆθa)a Ag], v |= BNE(s). We illustrate these properties with a classical example: Example 5. In the d AGVA mechanism (d Aspremont and G erard-Varet 1979; Arrow 1979) the allocation rules assigns the choice that maximizes the cumulative of the agents valuations for the (possibly untruthful) reported types, which defines a discount for agent s payment (for her bid ϑa) based on the expected total value of the other agents when she bids ϑa and other are truthful. Let Altd AGVA be defined over a finite set of choices C and a finite set of payments in [w, w] analogously to Example 2. Define the mechanism Gd AGVA = (Ac, V, v , δ, ℓ, L) over AP = {price, choicex, paypa a , ter : a Ag & (x, p) Altd AGVA}, where: Ac = {θ Θ}, where Θ = a AgΘa; v V for each v = win, p , where win C {none} denotes the winning allocation, and pa [w, w] {0} is the payment for a. The initial position is v = none, (0, ..., 0) V . L(v) = Ac for any position v V . For each position v = win, p and joint action c = (ca)a Ag, let x (c) = argmaxx C vb(x , cb) denote the alternative maximizing the reported types 8. Also let SW a(ca) = Eθ a(P b =a vb(x (ca, θ a), θb)) where

8We assume function argmax breaks ties according to a predefined order over the set of choices.

the term Ec a(.) is the expected total value for agents b = a when agent a announces θa and others tell the truth. The transition δ(v, c) is defined as follows:

If win = none, define δ(v, c) = win , p with probability 1, where, for each a,

win = argmaxx C( X

b Ag vb(x, cb))

P b =a SW b(cb)

n 1 SW a(ca)

Other cases are sinks, i.e., δ(v, c) = v with prob. 1.

The labelling function ℓis as for the other examples.

The d AGVA auction is BIC, however, it is not interim IR. Formally, let θ be a type profile, we have that Gd AGVA, A[s (ˆθa)a Ag], v |= BNE(s) and Gd AGVA, A, v |= s. BNE(s) F(ter V θ Θ IR(s, θ)). Notice that the d AGVA auction is a direct mechanism and, as pointed before, it is an SCF. Thus, the simplification in relation to the complete formula in Theorem 4. Similarly to IR, we can represent the conditions for other properties from mechanism design, such as efficiency or budget-balance. The above d AGVA auction illustrates how expected social welfare may be encoded, paving the way for going further in checking such new properties.

This works addresses the gap between the economics approach to mechanism design and the well-established techniques for formal reasoning in MAS. We propose the automated verification of Bayesian mechanisms using Probabilistic Strategy Logic (PSL). Unlike previous proposals, we introduce a general approach for evaluating mechanisms, which is able to take into account a wide range of settings (e.g. randomized, indirect and Bayesian mechanisms). Furthermore, thanks to the great expressiveness of the specification language, PSL, the verification ex ante, interim and ex post of complex solution concepts and properties is fullyautomated through model checking of logical formulas. The possibilities for future work are many. Although memoryless strategies are sufficient for most mechanisms, memory can be considered, e.g. for modeling mechanism design with information acquisition (Bikhchandani and Obara 2017). Since model checking PSL with perfect recall is undecidable (Aminof et al. 2019), one possibility is to study the case with bounded memory. As quantitative aspects (such as payments and utilities) are key features of mechanisms, we intend to investigate an extension of PSL with weighted semantics and its application to AMD. A quantitative approach is particularly appealing for considering approximation in Mechanism Design and the assessment of expected optimality (e.g. in relation to efficiency and revenue). Yet another line of research is the automated construction (or synthesis) of Bayesian mechanisms from PSLspecifications.

Acknowledgments

This research is partially supported by the ANR project AGAPE ANR-18-CE23-0013, the PRIN project RIPER (No. 20203FFYLK), the JPMorgan AI Faculty Research Award Resilience-based Generalized Planning and Strategic Reasoning , and the EU ICT-48 2020 project TAILOR (No. 952215).

References Alur, R.; Henzinger, T.; and Kupferman, O. 2002. Alternating-time temporal logic. J. ACM, 49(5): 672 713. Aminof, B.; Kwiatkowska, M.; Maubert, B.; Murano, A.; and Rubin, S. 2019. Probabilistic Strategy Logic. In Proc. of IJCAI-19. Arrow, K. J. 1979. The Property Rights Doctrine and Demand Revelation under Incomplete Information. In Economics and Human Welfare, 23 39. Academic Press. Aziz, H.; Lev, O.; Mattei, N.; Rosenschein, J. S.; and Walsh, T. 2019. Strategyproof peer selection using randomization, partitioning, and apportionment. Artificial Intelligence, 275: 295 309. Ballarini, P.; Fisher, M.; and Wooldridge, M. 2009. Uncertain Agent Verification through Probabilistic Model Checking. In Safety and Security in Multiagent Systems. Belardinelli, F.; Jamroga, W.; Malvone, V.; Mittelmann, M.; Murano, A.; and Perrussel, L. 2022. Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions. In AAMAS-22. Berthon, R.; Fijalkow, N.; Filiot, E.; Guha, S.; Maubert, B.; Murano, A.; Pinault, L.; Pinchinat, S.; Rubin, S.; and Serre, O. 2020. Alternating Tree Automata with Qualitative Semantics. ACM TOCL, 22(1): 1 24. Bikhchandani, S.; and Obara, I. 2017. Mechanism design with information acquisition. Econ. Theory, 63(3): 783 812. Bil o, V.; Fanelli, A.; Flammini, M.; Monaco, G.; and Moscardelli, L. 2018. Nash Stable Outcomes in Fractional Hedonic Games: Existence, Efficiency and Computation. J. Artif. Int. Res., 62(1): 315 371. Bouyer, P.; Kupferman, O.; Markey, N.; Maubert, B.; Murano, A.; and Perelli, G. 2019. Reasoning about Quality and Fuzziness of Strategic Behaviours. In Proc. of IJCAI 2019. Celis, L. E.; Lewis, G.; Mobius, M. M.; and Nazerzadeh, H. 2014. Buy-It-Now or Take-a-Chance: Price Discrimination Through Randomized Auctions. Manag. Sci., 60(12): 2927 2948. Chawla, S.; and Sivan, B. 2014. Bayesian Algorithmic Mechanism Design. SIGecom Exch., 13(1): 5 49. Chen, T.; Kwiatkowska, M.; Parker, D.; and Simaitis, A. 2011. Verifying team formation protocols with probabilistic model checking. In Int. Workshop on Comp. Logic in MAS. Clarke, E.; Grumberg, O.; Kroening, D.; Peled, D.; and Veith, H. 2018. Model checking. MIT press. Conitzer, V.; and Sandholm, T. 2002. Complexity of mechanism design. In Proc. of Uncertainty in AI - 02.

d Aspremont, C.; and G erard-Varet, L.-A. 1979. Incentives and incomplete information. Journal of Public Economics, 11(1): 25 45. Feldman, M.; Gkatzelis, V.; Gravin, N.; and Schoepflin, D. 2022. Bayesian and Randomized Clock Auctions. In EC 22, 820 845. ACM. Flammini, M.; Kodric, B.; and Varricchio, G. 2022. Strategyproof mechanisms for Friends and Enemies Games. Artificial Intelligence, 302: 103610. Gatti, N.; Lazaric, A.; Rocco, M.; and Trov o, F. 2015. Truthful learning mechanisms for multi-slot sponsored search auctions with externalities. Artificial Intelligence, 227: 93 139. Gutierrez, J.; Hammond, L.; Lin, A. W.; Najib, M.; and Wooldridge, M. 2021. Rational Verification for Probabilistic Systems. In Proc. of KR-21, 312 322. Hao, J.; Song, S.; Liu, Y.; Sun, J.; Gui, L.; Dong, J. S.; and Leung, H.-f. 2012. Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction. In Proc. of PRIMA-12. Hartline, J. D. 2012. Bayesian mechanism design. Theoretical Computer Science, 8(3): 143 263. Kemeny, J. G.; Snell, J. L.; and Knapp, A. W. 1976. Stochastic Processes. In Denumerable Markov Chains, 40 57. Springer. Klemperer, P. 1999. Auction theory: A guide to the literature. Journal of economic surveys, 13(3). Kwiatkowska, M.; Norman, G.; Parker, D.; Santos, G.; and Yan, R. 2022. Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges. In Proc. of MFCS 2022, 4 22. Leyton-Brown, K.; and Shoham, Y. 2008. Essentials of Game Theory: A Concise Multidisciplinary Introduction. Synthesis Lectures on AI and Machine Learning. Morgan & Claypool Publishers. Li, B.; Hao, D.; Gao, H.; and Zhao, D. 2022. Diffusion auction design. Artificial Intelligence, 303: 103631. Lomuscio, A.; and Pirovano, E. 2020. Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems. In Proc. of AAMAS-20, 762 770. Maubert, B.; Mittelmann, M.; Murano, A.; and Perrussel, L. 2021. Strategic Reasoning in Automated Mechanism Design. In KR-21. Mittelmann, M. 2022. Formally Reasoning about Strategies in Mechanisms. In OVERLAY@AI*IA, volume 3311 of CEUR Workshop Proceedings, 21 26. CEUR-WS.org. Mittelmann, M.; Maubert, B.; Murano, A.; and Perrussel, L. 2022. Automated Synthesis of Mechanisms. In IJCAI-22. Mogavero, F.; Murano, A.; Perelli, G.; and Vardi, M. Y. 2014. Reasoning About Strategies: On the Model-Checking Problem. ACM Trans. Comput. Log., 15(4). Narahari, Y. 2014. Game Theory and Mechanism Design. World Scientific. Narasimhan, H.; Agarwal, S. B.; and Parkes, D. C. 2016. Automated mechanism design without money via machine learning. In IJCAI-16.

Nisan, N.; Roughgarden, T.; Tardos, E.; and Vazirani, V. 2007. Algorithmic Game Theory. Cambridge Univ. Press. Niu, J.; Cai, K.; Parsons, S.; Fasli, M.; and Yao, X. 2012. A grey-box approach to automated mechanism design. Electronic Commerce Research and Applications, 11(1): 24 35. Okada, N.; Todo, T.; and Yokoo, M. 2019. SAT-Based Automated Mechanism Design for False-Name-Proof Facility Location. In PRIMA 2019. Parkes, D. 2001. Iterative combinatorial auctions: Achieving economic and computational efficiency. Univ. of Pennsylvania Philadel. Sandholm, T. 2003. Automated mechanism design: A new application area for search algorithms. In Proc. of CP-03. Shen, W.; Tang, P.; and Zuo, S. 2019. Automated Mechanism Design via Neural Networks. In AAMAS-19. Varloot, E. M.; and Laraki, R. 2022. Level-strategyproof Belief Aggregation Mechanisms. In EC-22, 335 369. ACM. Vorobeychik, Y.; Reeves, D. M.; and Wellman, M. P. 2007. Constrained Automated Mechanism Design for Infinite Games of Incomplete Information. In Conf. on Uncertainty in AI - 07. Wooldridge, M.; Agotnes, T.; Dunne, P.; and Van der Hoek, W. 2007. Logic for automated mechanism design-a progress report. In AAAI-07.