# automated_synthesis_of_mechanisms__209060f6.pdf Automated Synthesis of Mechanisms Munyque Mittelmann1 , Bastien Maubert2 , Aniello Murano2 and Laurent Perrussel1 1IRIT - Universit e Toulouse 1 Capitole, France 2Universit a degli Studi di Napoli Federico II , Italy {munyque.mittelmann,laurent.perrussel}@ut-capitole.fr, {bastien.maubert,nello.murano}@gmail.com Mechanism Design aims to design a game so that a desirable outcome is reached regardless of agents self-interests. In this paper, we show how this problem can be rephrased as a synthesis problem, where mechanisms are automatically synthesized from a partial or complete specification in a high-level logical language. We show that Quantitative Strategy Logic is a perfect candidate for specifying mechanisms as it can express complex strategic and quantitative properties. We solve automated mechanism design in two cases: when the number of actions is bounded, and when agents play in turn. 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 Contact Author to Automated Mechanism Design, which consists in automatically synthesizing mechanisms from a partial or complete specification expressed in a high-level logical language. 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 Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) 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 φ ::= p | s. φ | (a, s)φ | f(φ, ..., φ) | Xφ | φUφ where p AP, s Var, a Ag, and f F. 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 7 max(x, y) and function x 7 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 (w CGS) 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 7 σ] is the assignment that maps a to σ and is otherwise equal to A, and A[s 7 σ] 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 w CGS, and A an assignment. The satisfaction value JφKG A(h) [ 1, 1] of an SL[F] formula φ in a history h is defined as follows, where π denotes Out(A, h): Jp KG A(h) = ℓ(last(h), p) J s. φKG A(h) = max σ Str JφKG A[s7 σ](h) J(a, s)φKG A(h) = JφKG A[a7 A(s)](h) Jf(φ1,..., φm)KG A(h) = f(Jφ1KG A(h), ..., Jφm KG A(h)) JXφKG A(h) = JφKG A(π|h|+1) Jφ1Uφ2KG A(h) = sup i 0 min Jφ2KG A(π|h|+i), min 0 j 1, and decides whether there exists a w CGS G s.t. JφKG ϑ. Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) 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: φ ::= p | p. φ | Eψ | f(φ, ..., φ) ψ ::= φ | Xψ | ψUψ | f(ψ, ..., ψ) 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 (w KS) 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-total1 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 Hist S be the set of all histories in S. We also let Val S = {ℓ(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 VAP-labeled X-tree, (or (VAP, X)-tree for short, or VAP-tree when directions are understood), is a pair t = (τ, ℓ) where τ X+ is closed under 1i.e., for all s S, there exists s such that (s, s ) R. non-empty prefixes, all nodes u τ start with the same direction r, called the root, and have at least one child u d τ, and ℓ: τ VAP 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. 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 t S = (Hist S, ℓ ), where ℓ (u) = ℓ(last(u)) for every u Hist S. 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 JφKt(u) of a BQCTL [F] state formula φ in a node u of a VAP-tree t = (τ, ℓ), and the satisfaction value JψKt(λ) of a path formula ψ along some branch λ of t, are defined inductively as follows: Jp Kt(u) = ℓ(u)(p) J p. φKt(u) = sup ℓp : τ { 1,1} JφKt ℓp(u) JEψKt(u) = sup λ Br(u) JψKt(λ) Jf(φ1, ..., φn)Kt(u) = f(Jφ1Kt(u), ..., Jφn Kt(u)) JφKt(λ) = JφKt(λ0) JXψKt(λ) = JψKt(λ 1) Jψ1Uψ2Kt(λ) = sup i 0 min(Jψ2Kt(λ i), min 0 j 1, and decides whether there exists a w KS S s.t. JφKt S ϑ. 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]. Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) 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 w KS S, by adding dummy nodes labeled with proposition pint one can build a w KS e S with binary branching that simulates S; given a BQCTL [F] formula φ, one can then define a formula eφ that ignores these dummy nodes and has same satisfaction value on e S as φ on S. Lemma 1. For every BQCTL [F] formula φ and every finite w KS S, JφKS = JeφK e S. Let Φ be a BQCTL [F] formula and ϑ > 1 a threshold. Let also eΦ 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) w KS S such that JΦKS ϑ if and only if there exists a regular binary tree t such that JAGBool(pint) φ2 eΦKt ϑ. 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 eΦ 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 w KS S such that JΦKt ϑ. 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 Acw CGS a w CGS whose set of actions is Ac. Concerning turnbased systems, intuitively a w CGS 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 w CGS 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 w CGS a w CGS 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 w CGS. 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-w CGS is decidable. Theorem 3. Let V be a finite set of values. Then Vsatisfiability of SL[F] over turn-based w CGS 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 w CGS 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 w CGS. 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 w CGS, 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 = {JφKG | G is a V-weighted w CGS} is finite, and one can compute a set f Valφ,V of size at most |V||φ| such that Valφ,V f Valφ,V. Algorithm 1: Optimal mechanism synthesis Data: A SL[F] specification Φ and a set of possible values for atomic propositions V Result: A w CGS G such that JΦKG is maximal Compute f ValΦ,V; Let ν1, ..., νn be a decreasing enumeration of f ValΦ,V; for i=1...n do Solve V-satisfiability for Φ and ϑ = νi; if there exists G such that JΦKG νi then return G; end end Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) Consider now Algorithm 1. This algorithm synthesizes a w CGS 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 Automated Mechanism Design 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 Θ = Q 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 P, 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 w CGS 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 w CGS over the atomic propositions AP that satisfies the following: (i) every play eventually reaches a terminal position, i.e., a sink2 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. 2A 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(θ) := V 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(θ) := P a Ag va(choice, θa) = maxvθ, where maxvθ = maxx X P 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: NE(s, θ) := a Ag t. (Ag a, s a)(a, t)F(ter utila(θa)) (Ag, s)F(ter utila(θa)) 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: Max-Nash(φ, θ) := s. NE(s, θ) F(ter φ) 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-Bounded Mechanisms 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. Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) 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 V b =a bida) J6. AG(choice = 1 (W a Ag(bida V b =a bida))) J7. AG V a Ag(choice = winsa paya = price) J8. AG V a Ag(choice = winsa paya = 0) J9. V θ Θ Max-Nash(IR(θ) EF(θ), θ) We denote by Σjpn the conjunction of Rules J1-J9. Algorithm 1 constructs a w CGS 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 w CGS-mechanism Gjpn such that JΣjpn KGjpn = 1. Such an optimal mechanism is produced by Algorithm 1. 4.3 Turn-Based Mechanisms 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 V a Ag(bida = 0)) E2. AG(price = max(bida1, bida2)) E3. AG ter V a Ag(tua Xtua tua Xtua) E4. AG ter V a Ag(bid a < Xbida tua Xchoice = winsa) E5. AG ter V a Ag(bid a Xbida tua X(choice = wins a) ter) E6. AG V a Ag(bida = 1 tua X(choice = winsa) ter) E7. Max-Nash(P a Ag va(choice, θa), θ) 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 w CGS-mechanism Geng such that JΣeng(θ)KGeng = maxx X P a Ag va(x, θa), for each type profile θ Θ. As a result, Algorithm 1 applied to V θ Θ Σ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). Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) [ Agotnes et al., 2007] T. Agotnes, W. Van Der Hoek, J. A. Rodr ıguez-Aguilar, C. Sierra, and M. J. Wooldridge. On the logic of normative systems. In IJCAI, 2007. [Alur et al., 2002] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672 713, 2002. [Asselin et al., 2006] F. Asselin, B. Jaumard, and A. Nongaillard. A technique for large automated mechanism design problems. In IAT, 2006. [Belardinelli et al., 2019] F. Belardinelli, W. Jamroga, D. Kurpiewski, V. Malvone, and A. Murano. Strategy logic with simple goals: Tractable reasoning about strategies. In IJCAI, 2019. [Bouyer et al., 2019] P.Bouyer, O.Kupferman, N.Markey, B. Maubert, A.Murano, and G.Perelli. Reasoning about quality and fuzziness of strategic behaviours. In IJCAI, 2019. [Bulling and Dastani, 2016] N. Bulling and M. Dastani. Norm-based mechanism design. Artificial Intelligence, 239:97 142, 2016. [Cerm ak et al., 2015] P. Cerm ak, A. Lomuscio, and A. Murano. Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In AAAI, 2015. [Chatterjee et al., 2010] K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy Logic. Inf. Comput., 208(6):677 693, 2010. [Clarke et al., 2018] E.M.Clarke, O.Grumberg, D.Kroening, D. Peled, and H. Veith. Model checking. MIT press, 2018. [David and Kroening, 2017] C. David and D. Kroening. Program synthesis: challenges and opportunities. Phil. Trans. Royal Society A, 375(2104):20150403, 2017. [D utting et al., 2019] P. D utting, Z. Feng, H. Narasimhan, D. Parkes, and S. S. Ravindranath. Optimal auctions through deep learning. In ICML, 2019. [French, 2003] T. French. Quantified propositional temporal logic with repeating states. In TIME, 2003. [Green and Laffont, 1979] J. R. Green and J. J. Laffont. Incentives in Public Decision Making. North-Holland, Amsterdam, 1979. [Gutierrez et al., 2019] J. Gutierrez, M. Najib, G. Perelli, and M. J. Wooldridge. Equilibrium design for concurrent games. In CONCUR, 2019. [Klemperer, 1999] P. Klemperer. Auction theory: A guide to the literature. Journal of Economic Surveys, 13(3):227 286, 1999. [Laroussinie and Markey, 2014] F. Laroussinie and N. Markey. Quantified CTL: expressiveness and complexity. Log. Methods Comput. Sci., 10(4), 2014. [Laroussinie and Markey, 2015] F. Laroussinie and N. Markey. Augmenting ATL with strategy contexts. Inf. Comput., 245:98 123, 2015. [Maubert et al., 2021] B. Maubert, M. Mittelmann, A. Murano, and L. Perrussel. Strategic reasoning in automated mechanism design. In KR, 2021. [Mittelmann and Perrussel, 2020] M. Mittelmann and L. Perrussel. Auction description language (ADL): a general framework for representing auction-based markets. In ECAI, 2020. [Mogavero et al., 2014] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log., 15(4), 2014. [Mogavero et al., 2017] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: on the satisfiability problem. Log. Methods Comput. Sci., 13(1), 2017. [Myerson and Satterthwaite, 1983] R. B. Myerson and M. A. Satterthwaite. Efficient mechanisms for bilateral trading. Journal of Economic Theory, 29(2):265 281, 1983. [Narasimhan et al., 2016] H. Narasimhan, S. B. Agarwal, and D. C. Parkes. Automated mechanism design without money via machine learning. In IJCAI, 2016. [Nisan et al., 2007] N. Nisan, T. Roughgarden, E. Tardos, and V. Vazirani. Algorithmic Game Theory. Cambridge University Press, 2007. [Niu et al., 2012] J. Niu, K. Cai, S. Parsons, M. Fasli, and X. Yao. A grey-box approach to automated mechanism design. Elec. Com. Research and App., 11(1):24 35, 2012. [Okada et al., 2019] N. Okada, T. Todo, and M. Yokoo. Satbased automated mechanism design for false-name-proof facility location. In PRIMA, 2019. [Parkes, 2001] D. Parkes. Iterative combinatorial auctions: Achieving economic and computational efficiency. Univ. of Pennsylvania Philadelphia, 2001. [Pauly and Wooldridge, 2003] M. Pauly and M. Wooldridge. Logic for mechanism design a manifesto. In Workshop on Game Theory and Decision Theory in Agent Syst., 2003. [Pin, 2021] Jean Eric Pin. Handbook of Automata Theory. European Math. Society Publis. House, Zuerich, 2021. [Pnueli and Rosner, 1989] A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, 1989. [Sandholm, 2003] T. Sandholm. Automated mechanism design: A new application area for search algorithms. In CP, 2003. [Shen et al., 2019] W. Shen, P. Tang, and S. Zuo. Automated mechanism design via neural networks. In AAMAS, 2019. [Troquard and Walther, 2012] N. Troquard and D. Walther. On satisfiability in ATL with strategy contexts. In JELIA, 2012. [Vorobeychik et al., 2007] Y. Vorobeychik, D. M. Reeves, and M. P. Wellman. Constrained automated mechanism design for infinite games of incomplete information. In UAI, 2007. [Wooldridge et al., 2007] M. Wooldridge, T. Agotnes, P. Dunne, and W. Van der Hoek. Logic for automated mechanism design-a progress report. In AAAI, 2007. Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)