Automated Synthesis of Mechanisms

1 Introduction

Mechanism Design is focused on the designing of games, that is, mechanisms, that aggregate agents' preferences towards a single joint decision. When participants act rationally (in the game theoretical sense), such games should ensure a preferable behavior of the players (e.g. truthfullness) as well as desirable features of the decision (e.g. social welfare maximization) [Nisan et al., 2007]. Traditionally, mechanisms have been formulated by human specialists, who use their knowledge and experience for defining the game rules. Conitzer and Sandholm (2003) introduced Automated Mechanism Design (AMD), whose goal is to automatically create mechanisms for solving a specific preference aggregation problem.

AMD is usually tackled from an optimization and/or datadriven point of view. For instance, neural networks have been used to learn mechanisms that optimize a given parameter, such as revenue [Shen et al., 2019; D¨utting et al., 2019]. Statistical machine learning techniques have also been considered in domains without money [Narasimhan et al., 2016]. [Vorobeychik et al., 2007] proposes a black-box optimization algorithm for evaluating candidate mechanisms. Evolutionary search methods have also been used to optimize double auctions [Niu et al., 2012], and [Asselin et al., 2006] addresses AMD through linear programming and optimization.

In the spirit of the long-established logical approach to systems verification [Clarke et al., 2018] and synthesis [David and Kroening, 2017], in this work we propose a new approach to Automated Mechanism Design, which consists in automatically synthesizing mechanisms from a partial or complete specification expressed in a high-level logical language.

∗Contact Author

A related topic is normative systems [ ˚Agotnes et al., 2007], which define constraints (or obligations) on the behaviour of agents. [Bulling and Dastani, 2016] investigates how concepts from mechanism design can be used to analyse the enforcement of norms with preferences modelled using Lineartime Temporal Logic (LTL).

Concerning the choice of specification language, Auction Description Language [Mittelmann and Perrussel, 2020] is general enough to represent many kinds of protocols, but lacks a strategic dimension and cannot be used to reason about equilibria. [Okada et al., 2019] uses Boolean Satisfiability, but their approach is restricted to one type of mechanism and does not handle strategic, temporal and quantitative specifications. [Gutierrez et al., 2019] considers system specifications given in LTL, and studies the implementation of a mechanism to ensure temporal properties in equilibrium. [Pauly and Wooldridge, 2003; Wooldridge et al., 2007] first advocated the use of strategic logics to reason about mechanisms. They consider Alternating-time Temporal Logic (ATL) [Alur et al., 2002], but observe that it lacks the ability to reason about quantitative aspects such as preferences, as well as game-theoretic concepts such as equilibria. Such features are key for modelling and evaluating mechanisms, specially the ones with monetary transfers.

We consider Quantitative Strategy Logic (SL[F]) [Bouyer et al., 2019], a logic that has recently been shown to be a great candidate to formally reason about mechanisms [Maubert et al., 2021]. Indeed SL[F], which subsumes ATL, is expressive enough to express complex solution concepts such as Nash equilibrium and properties about quantities. This language thus allows for specifications that contain constraints on mechanism properties (for instance, in Auction Design, the efficiency and budget-balance). Its quantitative semantics, with satisfaction values that reflect how well a model satisfies a formula, also allows us to investigate the constructions of mechanisms that approximate such properties, which is not possible with standard Strategy Logic (SL) [Chatterjee et al., 2010; Mogavero et al., 2014].

Contribution. In this work we propose a novel perspective on the design of mechanisms. Our approach enables automatically generating optimal mechanisms from a quantitative logical specification, which may include not only game rules but also requirements over the strategic behaviour of participants and quality of the outcome. We rephrase the AMD problem in terms of synthesis from SL[F] specifications. To solve this synthesis problem we investigate the related satisfiability problem for SL[F], which had not been studied so far. Finally, we illustrate the relevance of mechanism synthesis with examples based on Auction Design.

Outline. In Section 2 we recall the logic SL[F]. In Section 3 we address the satisfiability and synthesis for this logic. In Section 4, we address the problem of AMD using SL[F]. Finally, Section 5 concludes the paper.

2 Quantitative Strategy Logic

For the remainder of the paper, we fix a set of atomic propositions AP, a set of agents Ag and a set of strategy variables Var, except when stated otherwise. We let n be the number of agents in Ag. We also let F ⊆ {f : [-1, 1]m → [-1, 1] | m ∈ N} be a set of functions over [-1, 1] of possibly different arities, that will parameterise the logics we consider.

Definition 1. The syntax of SL[F] is defined by the grammar

The intuitive reading of the operators is as follows: ∃s. φ means that there exists a strategy such that φ holds; (a, s)φ means that when strategy s is assigned to agent a, φ holds; X and U are the usual temporal operators "next" and "until". The meaning of f(φ1, ..., φn) depends on the function f . We use ⊤, ∨, and ¬ to denote, respectively, function 1, function x, y ↦→ max(x, y) and function x ↦→ -x.

Remark 1. While [Bouyer et al., 2019] considers values in [0,1], we follow [Maubert et al., 2021] and use interval [-1,1] instead, which is more adapted to model some mechanisms of interest, such as double-sided auctions.

A variable is free in formula φ if it is bound to an agent without being quantified upon, and an agent a is free in φ if φ contains a temporal operator (X or U) not in the scope of any binding for a. The set of free variables and agents in φ is written free(φ), and a formula φ is a sentence if free(φ) = ∅.

Definition 2. A weighted concurrent game structure (wCGS) is a tuple G = (Ac, V, vι, δ, ℓ) where (i) Ac is a finite set of actions; (ii) V is a finite set of positions; (iii) vι ⊆ V is an initial position; (iv) δ : V × Ac Ag → V is a transition function; (v) ℓ : V ×AP → [-1, 1] is a weight function.

Remark 2. Because we are interested in synthesizing mechanisms of finite size, we restrict attention to finite models.

In a position v ∈ V , each player a chooses an action ca ∈ Ac, and the game proceeds to position δ(v, c) where c is an action profile (ca)a∈Ag.

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

A play π = v1v2... is an infinite sequence of positions such that for every i ≥ 1 there exists an action profile c such that

δ(vi, c) = vi+1. We write πi = vi for the position at index i in play π. A history h is a finite prefix of a play, last(h) is the last position of history h, |h| is the length of h and Hist is the set of histories.

A strategy is a function σ : Hist → Ac that maps each history to an action. We let Str be the set of strategies.

Remark 3. Unlike [Maubert et al., 2021], which considers strategies without memory, we consider strategies with perfect recall, as in [Bouyer et al., 2019]. The main reason is that for memoryless strategies satisfiability, and thus synthesis, is undecidable already for SL, even for bounded actions or turnbased systems [Laroussinie and Markey, 2015]. Considering perfect recall strategies means that the systems we synthesize satisfy the strategic aspects of the specification assuming that agents' actions can depend on the past.

An assignment A : Ag ∪ Var → Str is a function from players and variables to strategies. For an assignment A, an agent a and a strategy σ for a, A[a ↦→ σ] is the assignment that maps a to σ and is otherwise equal to A, and A[s ↦→ σ] is defined similarly, where s is a variable.

For an assignment A and a history h, we let Out(A, h) be the unique play that continues h following the strategies assigned by A. Formally, Out(A, h) is the play hv0v1... such that for all i ≥ 0, vi = δ(vi-1, c) where for all a ∈ Ag, ca = A(a)(hv0...vi-1), and v-1 = last(h).

Definition 3. Let G = (Ac, V, δ, ℓ, Vι) be a wCGS, and A an assignment. The satisfaction value �φ�GA(h) ∈ [-1, 1] of an SL[F] formula φ in a history h is defined as follows, where π denotes Out(A, h):

If φ is a sentence, its satisfaction value does not depend on the assignment, and we write �φ�G (h) for �φ�GA(h) where A is any assignment. We also let �φ�G = �φ�G (vι).

We can define the following classic abbreviations: ⊥:= ¬⊤, φ∧φ′ := ¬(¬φ∨¬φ′ ), φ→φ′ := ¬φ∨φ′ , Fψ := ⊤Uψ, Gψ := ¬F¬ψ and ∀s. φ := ¬∃s. ¬φ. We also use Aφ as a shorthand for a universal quantification on strategies and bindings for all agents, followed by φ; this simulates the universal path quantifier of CTL∗ .

3 Satisfiability and Synthesis of SL[F]

We investigate the following satisfiability problem for SL[F]. Definition 4. The satisfiability problem for SL[F] takes a sentence φ ∈ SL[F] and a threshold ϑ > -1, and decides

whether there exists a wCGS G s.t. �φ�G ≥ ϑ.

The satisfiability problem for SL was proved undecidable in [Mogavero et al., 2017], but the proof there considers models with infinitely many actions. However it is also known to be undecidable when considering finite models, i.e., models with both finitely many states and finitely many actions, as we do. Indeed, it is shown in [Troquard and Walther, 2012; Laroussinie and Markey, 2015] that satisfiability of ATL with strategy context (ATLsc) is undecidable for finite models. Since ATLsc can be expressed in SL [Laroussinie and Markey, 2015] and SL in SL[F], by taking F = {⊤, ∨, ¬} [Bouyer et al., 2019], we obtain the following result.

Proposition 1. The satisfiability problem for SL[F] is undecidable as soon as F contains ⊤, ∨ and ¬.

However satisfiability of SL is known to be decidable when restricted to turn-based systems or systems with a bounded number of actions [Laroussinie and Markey, 2015]. We show that in these cases satisfiability is decidable for SL[F] as well. To do so we first recall Booleanly-quantified CTL∗ (BQCTL∗ [F]) and solve its satisfiability problem, and we then show that for bounded actions or turn based systems satisfiability of SL[F] reduces to that of BQCTL∗ [F].

3.1 Booleanly-Quantified CTL∗ [F]

The logic BQCTL∗ [F] [Bouyer et al., 2019], a quantitative extension of QCTL∗ [Laroussinie and Markey, 2014], itself an extension of CTL∗ with quantifiers on atomic proposition. In BQCTL∗ [F] the semantics is quantitative, but the quantifiers on propositions consider only Boolean values. To be consistent with SL[F] we consider [-1,1] as range of values instead of [0,1] as in [Bouyer et al., 2019]. This changes nothing to the results presented there.

The syntax of BQCTL∗ [F] is defined by:

where p ranges over AP and f over F.

Eψ is the quantitative counterpart to the path quantifier of CTL∗ , and it maximizes the value of ψ over all branches. Formulas of type φ are called state formulas, those of type ψ are called path formulas, and BQCTL∗ [F] consists of all the state formulas defined by the grammar. We again use ⊤, ∨, and ¬ to denote functions 1, max and -x, as well as classic abbreviations already introduced for SL[F].

Definition 5. A weighted Kripke structure (wKS) is a tuple S = (S, sι,R, ℓ) where S is a set of states, sι ∈ S is an initial state, R ⊆ S ×S is a left-total 1 transition relation, and ℓ : S → [-1, 1]AP is a weight function.

A path in S is an infinite word λ = s0s1... over S such that s0 = sι and (si, si+1) ∈ R for all i. Finite prefixes of paths are histories, and we let HistS be the set of all histories in S. We also let ValS = {ℓ(s)(p) | s ∈ S and p ∈ AP} be the finite set of values appearing in S.

Given finite nonempty sets X of directions and V ⊆ [-1, 1] of possible values, a V AP -labeled X-tree, (or (V AP ,X)-tree for short, or V AP -tree when directions are understood), is a pair t = (τ, ℓ) where τ ⊆ X+ is closed under non-empty prefixes, all nodes u ∈ τ start with the same direction r, called the root, and have at least one child u · d ∈ τ , and ℓ : τ → V AP is a weight function. We let Valt ⊆ V be the image of ℓ on τ. A branch λ = u0u1... is an infinite sequence of nodes such that for all i ≥ 0, ui+1 is a child of ui. For i ≥ 0, λ≥i denotes the suffix of λ that starts at node ui, and we let Br(u) be the set of branches that start in node u.

1 i.e., for all s ∈ S, there exists s′ such that (s, s′ ) ∈ R.

A binary tree is a X-tree where |X| = 2. A tree is regular if it is the unfolding of some finite Kripke structure.

Let p ∈ AP. A p-labeling for a V-tree t = (τ, ℓ) is a mapping ℓp : τ → {-1, 1}. The composition of t with ℓp is the (V ∪ {-1, 1})AP -tree defined as t ⊗ ℓp := (τ, ℓ′ ), where ℓ′ (u)(p) = ℓp(u) and ℓ′ (u)(q) = ℓ(u)(q) for q ̸= p.

Finally, the tree unfolding of a weighted Kripke structure S with state set S is the Val AP S -labeled S-tree tS = (HistS, ℓ′ ), where ℓ′ (u) = ℓ(last(u)) for every u ∈ HistS .

Different semantics exist for QCTL∗ , which differ on how proposition quantification is interpreted (see [Laroussinie and Markey, 2014] for more on the different semantics for QCTL∗ ). In this paper we focus on the tree semantics, which allows capturing perfect-recall strategies.

Definition 6 (Semantics). Consider a finite set V ⊆ [-1, 1] of possible values. The satisfaction value �φ�t (u) of a BQCTL∗ [F] state formula φ in a node u of a V AP -tree t = (τ, ℓ), and the satisfaction value �ψ�t (λ) of a path formula ψ along some branch λ of t, are defined inductively as follows:

For a tree t with root r we write �φ�t for �φ�t (r), for a weighted Kripke structure S we write �φ�S for �φ�tS .

3.2 Deciding BQCTL∗ [F] Satisfiability

As for SL[F], we define the quantitative satisfiability problem for BQCTL∗ [F] as follows.

Definition 7. The satisfiability problem for BQCTL∗ [F] takes a formula φ ∈ BQCTL∗ [F] and a threshold ϑ > -1, and decides whether there exists a wKS S s.t. �φ�tS ≥ ϑ.

Satisfiability for QCTL∗ with structure semantics is undecidable [French, 2003], but decidable for the tree semantics [Laroussinie and Markey, 2014] which we consider in this paper. Relying on the automata construction developed in [Bouyer et al., 2019] to model check BQCTL∗ [F], we show that satisfiability is also decidable for BQCTL∗ [F].

Theorem 1. Satisfiability of BQCTL∗ [F] is decidable.

The lower bounds are inherited from the satisfiability problem for QCTL∗ [Laroussinie and Markey, 2014]. The reduction is direct with threshold ϑ = 1. For the upper bounds, the first step is to show that one can restrict attention to structures with binary branching, i.e., where each state has at most two successor states.

Given a finite wKS S, by adding dummy nodes labeled with proposition pint one can build a wKS ˜ S with binary branching that simulates S; given a BQCTL∗ [F] formula φ, one can then define a formula ˜ φ that ignores these dummy nodes and has same satisfaction value on ˜ S as φ on S.

Let Φ be a BQCTL∗ [F] formula and ϑ > -1 a threshold. Let also ˜Φ be the corresponding formula on structures with binary branching, and φ2 = ¬pint ∧ AGF¬pint. Consider also function Bool such that Bool(x) = 1 if x ∈ {-1, 1}, and -1 otherwise, which we use to check that propositions take only Boolean values -1 or 1. We can prove the following:

Lemma 2. There exists a (finite) wKS S such that �Φ�S ≥ ϑ if and only if there exists a regular binary tree t such that �AGBool(pint) ∧ φ2 ∧ ˜Φ�t ≥ ϑ.

It is shown in [Bouyer et al., 2019] that we can build an automaton A that accepts binary trees t on which the satisfaction value of AGBool(pint) ∧φ2 ∧ ˜Φ belongs to [ϑ, 1] (we refer to [Pin, 2021, Ch. 8] for standard definitions and results on tree automata). The number of states of the automaton is (k + 1)-exponential in the nesting depth of the formula, and its index k-exponential. From Lemma 2 and the fact that every regular tree language contains a regular tree it follows that A is nonempty if and only if there exists a finite wKS S such that �Φ�t ≥ ϑ. The emptiness of A can be tested in time polynomial in the number of states and exponential in the index. The overall complexity is thus (k + 1)-exponential in time.

3.3 Decidable Cases for SL[F] Satisfiability

In the qualitative setting, satisfiability of ATL with strategy context and SL are known to be decidable in two cases: when the number of possible actions is bounded, and when agents play in turns. With respect to bounded actions, we call AcwCGS a wCGS whose set of actions is Ac. Concerning turnbased systems, intuitively a wCGS is turn-based when in every position there is a unique agent who can determine the next position by the choice of its action. Formally, a wCGS G = (Ac, V, vι, δ, ℓ) is turn-based if for every position v ∈ V there exists a unique agent a such that for every successor v′ ∈ {δ(v, c) | c ∈ Ac Ag} there is an action c such that δ(v, c) = v′ for all joint actions c where ca = c. We call owner of a position the agent that can choose the successor.

We show that, as for SL, the satisfiability problem for SL[F] is decidable when the number of actions is bounded (a priori) or systems are turn-based, if in addition we restrict to models in which atomic propositions take values in a given finite set of possible values. Given a set V ⊆ [-1, 1] of possible values with {-1, 1} ⊆ V, we call V-weighted wCGS a wCGS whose weight function takes values in V.

Definition 8. Given a finite set V ⊂ [-1, 1] such that {-1, 1} ⊆ V, the V-satisfiability problem for SL[F] is the restriction of the satisfiability problem to V-weighted wCGS.

We establish the following results (proofs are in appendix).

Theorem 2. Let V be a finite set of values and Ac a finite set of actions. Then V-satisfiability of SL[F] over Ac-wCGS is decidable.

Theorem 3. Let V be a finite set of values. Then Vsatisfiability of SL[F] over turn-based wCGS is decidable.

Concerning complexity, for Theorems 1, 2 and 3 the problems are (k + 1)-EXPTIME-complete where k is the maximal number of nested quantifiers on propositions (for BQCTL∗ [F]) or strategies (for SL[F]). Blocks of successive quantifiers can be counted as one if they are all existential or all universal, so that an existential quantification on a strategy profile for all agents just adds one exponential for instance.

3.4 Automated Synthesis of Optimal Mechanism

We describe how we can use our algorithm for SL[F] satisfiability to synthesize mechanisms that optimally satisfy the specification, in the sense that they achieve the best possible satisfaction value for the specification.

First, we observe that the algorithms developed in the previous section for the satisfiability problem of SL[F] in the case of bounded actions or turn-based systems can be tweaked to actually return a satisfying wCGS when one exists. Indeed classic algorithms to solve emptiness of parity tree automata can produce a witness regular tree accepted by the automaton (see [Pnueli and Rosner, 1989]), and from such a tree in our setting we can infer a witness wCGS.

Second, it is proved in [Bouyer et al., 2019] that given a finite set V of possible values for atomic propositions and a formula φ ∈ SL[F] there is only a finite number of possible satisfaction values φ can take in any wCGS, and we can compute an over-approximation of this set.

Lemma 3 ([Bouyer et al., 2019]). Let V ⊂ [-1, 1] be a finite set of values with {-1, 1} ⊆ V and let φ be an SL[F] sentence. The set Valφ,V = {�φ�G | G is a V-weighted wCGS} is finite, and one can compute a set ˜ Valφ,V of size at most |V||φ| such that Valφ,V ⊆ ˜ Valφ,V .

Algorithm 1: Optimal mechanism synthesis

Data: A SL[F] specification Φ and a set of possible values for atomic propositions V Result: A wCGS G such that �Φ�G is maximal Compute ˜ ValΦ,V ; Let ν1, ..., νn be a decreasing enumeration of ˜ ValΦ,V ; for i=1...n do Solve V-satisfiability for Φ and ϑ = νi; if there exists G such that �Φ�G ≥ νi then return G; end end

Consider now Algorithm 1. This algorithm synthesizes a wCGS that maximizes the satisfaction value of the given SL[F] specification, in all cases where the satisfiability problem for SL[F] can be solved and a witness produced. In particular, it works in the case of bounded actions and the case of turn-based systems. We now show how this can be used to solve automated mechanism design.

4 AutomatedMechanismDesign

This section aims to motivate the use of synthesis of SL[F] for mechanism design. We first recall basic concepts used to formalize mechanisms, which determine how to choose one option among several alternatives, based on agents' strategies. Since many mechanisms describe monetary transfers, we assume that each alternative is a tuple (x, p) where x ∈ X is a choice from a finite set of choices X ⊂ [-1, 1], and pa ∈ [-1, 1] is the payment for agent a. For each agent a ∈ Ag, let also Θa ⊂ [-1, 1] be a finite set of possible types for a. We let Θ = ∏a∈Ag Θa, and we note θ = (θa)a∈Ag ∈ Θ for a type profile, which assigns a type θa to each agent a. The type θa of an agent a determines how she values each choice x ∈ X; this is represented by a valuation function va : X × Θa → [-1, 1].

In this section we assume that F contains the constant θa and the function va for each agent a and type θa ∈ Θa. We also assume that F contains the difference function -, the n-ary sum function ∑, the equality function = and the comparison functions ≤, >, < and ̸=. For readability we use the infix notation x-y. These functions are defined with the standard meaning. Finally, we assume that types, payments and valuations are normalized so that all values remain in [-1, 1].

A mechanism consists of a description of the agents' possible strategies, and a description of the alternatives that result from them. As described in [Maubert et al., 2021], we can represent mechanisms as wCGS and verify their equilibrium outcome in relation to a number of economic properties.

Definition 9. Let AP ⊇ {choice, paya , ter : a ∈ Ag}, where choice and paya denote respectively the choice elected by the mechanism, and the payment of agent a. The proposition ter specifies whether a position is terminal. A mechanism G is a wCGS over the atomic propositions AP that satisfies the following: (i) every play eventually reaches a terminal position, i.e., a sink 2 where proposition ter has value 1; (ii) in all non-terminal positions, ter has value -1.

4.1 Characterizing Properties With SL[F]

SL[F] can express a variety of important notions in mechanism design, such as strategy proofness, individual rationality, efficiency, budget-balance, Pareto optimality, and different kinds of game-theoretic equilibria [Maubert et al., 2021]. We recall the formulas for some of these notions. Let θ = (θa)a∈Ag be a type profile in Θ.

First define utila(θa) := va(choice, θa) - paya . This is an SL[F] formula, whose value in a terminal position is equal to the agent's utility, which she tries to maximize.

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

Individual rationality (IR) expresses the idea that an agent has an incentive to participate [Parkes, 2001], that is, she can ensure to always get nonnegative utility. In SL[F] we encode (ex-post) individual rationality [Nisan et al., 2007] through the formula IR(θ) := ∧a∈Ag 0 ≤ utila(θa).

A mechanism is efficient (EF) if it chooses the alternative maximizing the social welfare, i.e.the cumulative of the agent's valuations over the assigned choice [Parkes, 2001]. In SL[F], we can write this condition with the formula EF(θ) := ∑a∈Ag va(choice, θa) = maxvθ, where maxvθ = maxx∈X ∑a∈Ag va(x, θa) is a constant in F. In a terminal position, it means that the social welfare is maximal.

To express that a mechanism satisfies a property we need to capture its equilibria. A strategy profile σ = (σa)a∈Ag is a Nash equlibrium (NE) if no agent can increase her utility with a unilateral change of strategy [Parkes, 2001]. The following SL[F]-formula characterizes Nash equilibria:

where s = (sa)a∈Ag is a profile of strategy variables.

The following formula maximizes the value of φ in the terminal positions of all Nash equilibria:

We now use these formulas to illustrate our approach to mechanism synthesis. To avoid detailing tie-breaking rules, in the examples we assume agents have distinct types, that is θa ̸= θb for any b ̸= a and θ ∈ Θ. Given an agent a, we let winsa ∈ (-1, 1] be a constant value denoting the choice in which a is the winner, with winsa ̸= winsb for any b ̸= a. We consider the choice set X = {winsa : a ∈ Ag}∪{-1}, where -1 specifies the case where there is no winner at the end of the game. In the examples we let each valuation function va be defined as va(θa, x) = θa if x = winsa, and va(θa, x) = 0 otherwise. That is, the valuation of an agent depends only on her type and whether she won.

4.2 Action-BoundedMechanisms

Action-bounded mechanisms are of great interest since the amount of resources available is often limited. For instance, the actions in a market could consist in bids representing discrete monetary values bounded by the participants' budget. In this section, we illustrate the synthesis problem with such restriction by considering rules based on the Japanese auction.

Example 1. The Japanese auction is an ascending protocol in which the price is repeatedly raised by the auctioneer until only one bidder remains. The remaining bidder wins the item at the final price [Klemperer, 1999]. Let us fix a price increment inc > 0. There are only two possible actions, accept (acc) or decline (dec), so that the set Ac = {acc, dec} is indeed bounded. Furthermore, we let AP = {price, sold, init, choice, bida, paya , ter : a ∈ Ag}, where price denotes the current price, init denotes whether the position is the initial one, sold specifies whether the item was sold, and bida specifies whether a is an active bidder.

The following SL[F]-formulae are a partial description of a mechanism, inspired by the Japanese auction. The meaning of Rules J1-J8 is intuitive. Similar rules for encoding auctions through a logic-based language can be seen in [Mittelmann and Perrussel, 2020]. Rule J9 specifies that for all type profiles there should exist a NE whose outcome is IR and EF.

• J1. AG((init → price = 0 ∧ ¬ter) ∧ (XG¬init ∧ F ter))
• J2. AG(sold ↔ choice ̸= -1)
• J3. AG((¬sold ∧ price + inc ≤ 1) → (price + inc = Xprice ∧ ¬Xter))
• J4. AG((sold ∨ price + inc > 1) → (price = Xprice ∧ Xter))
• J5. AG(choice = winsa ↔ bida ∧ ∧b̸=a ¬bida)
• J6. AG(choice = -1 ↔ ¬(∨a∈Ag (bida ∧ ∧b̸=a ¬bida)))
• J7. AG(∧a∈Ag (choice = winsa → paya = price))
• J8. AG(∧a∈Ag (choice ̸= winsa → paya = 0))
• J9. ∧θ∈Θ Max-Nash(IR(θ) ∧EF(θ), θ)

We denote by Σjpn the conjunction of Rules J1-J9. Algorithm 1 constructs a wCGS that maximizes the satisfaction value of Σjpn. We show that this value is 1, meaning that there exists a mechanism that is individually rational and efficient for some Nash equilibrium, for all type profiles.

Proposition 2. There exists a wCGS-mechanism Gjpn such that �Σjpn�Gjpn = 1.

Such an optimal mechanism is produced by Algorithm 1.

4.3 Turn-BasedMechanisms

In a number of mechanisms, such as picking sequences, agents play in turns. Hereby, we exemplify the synthesis of a turned-based mechanism. In this example we also show how Algorithm 1 can be used to maximize the social welfare.

Example 2. The English auction is an ascending auction in which the participants are allowed to outbid the last bidder by proposing a highest price. The auction ends when no agent is willing to raise the last bid. The highest bidder wins the item at her proposed price [Nisan et al., 2007].

In this specification, let us consider two agents, with Ag = {a1, a2}. We let -a denote the opponent of a ∈ Ag. Furthermore, we let AP = {price, init, choicea, bida, tua, paya , ter : a ∈ Ag}, where price denotes the current price, init denotes whether the position is the initial one, tua specifies whether it is a's turn and bida specifies the value of a's bid.

The following SL[F]-formulae are a partial description of a two-player turned-based variant of the English auction.

• E1. AG(init → tua1 ∧ ¬tua2 ∧ ¬ter ∧ ∧a∈Ag (bida = 0))
• E2. AG(price = max(bida1 , bida2 ))
• E3. AG(¬ter→ ∧a∈Ag (tua→¬Xtua ∧¬tua→Xtua))
• E4. AG(¬ter → ∧a∈Ag (bid-a < Xbida ∧ tua → Xchoice = winsa))

The value of formula E7 is the social welfare in the best NE for type profile θ. Letting Σeng(θ) be the conjunction of Rules E1-E7 alongside with the payment rules in Σjpn (Rules J7-J8), we have:

Proposition 3. There exists a wCGS-mechanism Geng such that �Σeng(θ)�Geng = maxx∈X ∑a∈Ag va(x, θa), for each type profile θ ∈ Θ.

As a result, Algorithm 1 applied to ∧θ∈Θ Σeng(θ) returns a mechanism that satisfies all the rules E1-E7 and J7-J8, and in which the minimal social welfare in all possible type profiles is as high as possible.

Complexity. The synthesis problem in these examples can be solved in 3-EXPTIME. The complexity is dominated by Rules J9 and E7, which express the existence of NE. Without them the complexity would be in 2-EXPTIME. Most importantly, the complexity is only in the size of the formula, which is typically rather small.

Approximate mechanisms. The well-known results of Green and Laffont (1979) and Myerson and Satterthwaite (1983) show the impossibility of defining mechanisms whose equilibrium is efficient while having strict balance of monetary transfers. The quantitative semantics of SL[F] and Algorithm 1 enable synthesizing mechanisms that approximate efficiency by maximizing social welfare.

5 Conclusion

We propose a novel approach for AMD in which mechanisms can be automatically generated (or synthesized) from partial or complete specifications in a rich logical language. The great expressiveness of the specification language SL[F] makes our approach of automated synthesis very general, unlike previous proposals. While mechanism synthesis from SL[F] specifications is undecidable, we solve it in two cases: when the number of actions is bounded, and when agents play in turn. We achieve this thanks to reductions to the satisfiability problem for BQCTL∗ [F], which we prove to be decidable.

The high expressiveness of SL[F] may not always be needed for simple classes of mechanisms, and one may consider fragments of it to achieve better complexity. Therefore, an interesting direction for future work is to study the complexity of synthesizing from SL[F]-fragments, inspired from the SL-fragments One-Goal SL [Mogavero et al., 2017; Cerm´ak et al., 2015] and Simple-Goal SL [Belardinelli et al., 2019], for instance. These fragments are usually computationally easier than full SL, and we can hope that similar results can be established in the quantitative setting.

Acknowledgements

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