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.
First, we demonstrated how to represent and verify knowledge-based benchmarks and properties
(such as eficiency and strategyproofness) in the newly proposed Epistemic SL[ℱ ] (SLK[ℱ ]) [
In a second stage, we considered SL[ℱ ] with Natural Strategies [
Finally, we reduced the design of deterministic mechanisms to SL[ℱ ]-synthesis [
Definition 1.
::= | ∃. | (i, ) | (, ..., ) | X | U
where ∈ AP is an atomic proposition, ∈ Var is a strategy variable, i ∈ N is an agent, and
∈ ℱ is a function over [
The intuitive reading of the operators is as follows: ∃. means that there exists a strategy such that holds; (i, ) means that when strategy is assigned to agent i, holds; X and U are the usual temporal operators “next” and “until”. The meaning of ( 1, ..., ) depends on the function . We use ⊤, ∨, and ¬ to denote, respectively, function 1, function , ↦→ max(, ) and function ↦→ − .
Definition 2. A weighted concurrent game structure (wCGS) is a tuple = (ℬ, , , , ℓ ) where
(i) ℬ is a finite set of actions; (ii) is a finite set of positions; (iii) ⊆ is an initial position;
(iv) : × ℬ N → is a transition function; (v) ℓ : × AP → [
In a position ∈ , each player i chooses an action i ∈ ℬ, and the game proceeds to position (, ) where is the action profile (i)i∈N. We write for a tuple of objects (i)i∈N, one for each agent, and such tuples are called profiles . Given a profile and i ∈ N, we let i be agent i’s component, and − i is (r)r̸=i. Similarly, we let N− i = N ∖ {i}.
A play = 12... is an infinite sequence of positions such that for every ≥ 1 there exists
an action profile such that (, ) = +1. We write = for the position at index in
play . A history ℎ is a finite prefix of a play. A strategy is a function : Hist → ℬ that maps
each history to an action. We let Str be the set of strategies. An assignment : N ∪ Var → Str
is a function from players and variables to strategies. For an assignment , an agent i and a
strategy for i, [ ↦→ ] is the assignment that maps to and is otherwise equal to , and
[ ↦→ ] is defined similarly, where is a variable. For an assignment and a history ℎ, we
let Out(, ℎ) be the unique play that continues ℎ following the strategies assigned by .
Definition 3. (Partial, see complete definition in [
J K
J∃. K(ℎ) = m∈SatxrJ K[↦→ ](ℎ)
J(i, ) K(ℎ) = J K[i↦→()](ℎ)
We write J K (ℎ) when the satisfaction value of does not depend on the
assignment. We also let J K = J K ( ). We can define the classic abbreviations:
⊥=def ¬⊤, ∧ ′ =def ¬(¬ ∨ ¬ ′), → ′ =def ¬ ∨ ′, F =def ⊤U , G =def ¬F¬
and ∀. =def ¬∃. ¬ . We also use A as a shorthand for a universal quantification on
strategies and bindings for all agents.
3. Satisfiability and Synthesis of SL[ℱ ]
The satisfiability of SL is undecidable in general [
The algorithm for SL[ℱ ] 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 note that the algorithm for the satisfiability problem of SL[ℱ ] can actually return a
satisfying wCGS when one exists. Second, it is proved in [
Algorithm 1 synthesizes a wCGS that maximizes the satisfaction value of the given SL[ℱ ] specification, in all cases where the satisfiability problem for SL[ℱ ] can be solved and a witness produced. We now show how this can be used to solve automated mechanism design. Algorithm 1 ℎ(Φ , )
Input: a SL[ℱ ]-formula Φ and a set of possible values for atomic propositions .
Output: a wCGS such that JΦ K is maximal 1: Compute Ṽa︁lΦ, 2: Let 1, ..., be a decreasing enumeration of Ṽa︁lΦ, 3: for ← 1 to do 4: Solve -satisfiability for Φ and = 5: if there exists such that JΦ K ≥ then
return
We first recall basic concepts used to formalize mechanisms, which determine how to choose one
option among several alternatives, based on agents’ strategies. We assume that each alternative
is a tuple (, p) where ∈ is a choice from a finite set of choices ⊂ [
SL[ℱ ] can express a variety of important notions in mechanism design, such as
strategyproofness, individual rationality, and eficiency [
First the agent’s utility is denoted by the SL[ℱ ] formula utili( i) =def vi(choice, i) − payi.
Eficiency can be expressed as follows: EF( ) =def ∑︀i∈N vi(choice, i) = maxv , where maxv = max∈ ∑︀i∈N vi(, i) is a constant in ℱ .
We also recall the SL[ℱ ]-formula that characterizes Nash equilibria:
NE(, ) =def ⋀︁ ∀. [︀ (N− i, − i)(i, )F(term ∧ utili( i)) ≤ (N, )F(term ∧ utili( i))]︀ i∈N where = (i)i∈N is a profile of strategy variables.
We now illustrate the mechanism synthesis problem by considering rules based on the Japanese auction. We let winsi ∈ (− 1, 1] be a constant value denoting the choice in which the agent i is the winner, with winsi ̸= winsr for any r ̸= i. We consider the choice set = {winsi : i ∈ N} ∪ {− 1}, where − 1 specifies the case where there is no winner at the end of the game.
Example 1. In the Japanese auction, the price is repeatedly raised by the auctioneer
until only one bidder remains. The remaining bidder wins the item at the final price [
J1. AG((initial → price = 0 ∧ ¬sold ∧ ¬term) ∧ (XG¬initial ∧ F term)) J2. AG(sold ↔ choice ̸= − 1) J3. AG((¬sold ∧ price + inc ≤ 1) → (price + inc = Xprice ∧ ¬Xterm)) J4. AG((sold ∨ price + inc > 1) → (price = Xprice ∧ Xterm)) J5. AG(choice = winsi ↔ bidi ∧ ⋀︀r̸=i ¬bidi) J6. AG(choice = − 1 ↔ ¬(⋁︀i∈N(bidi ∧ ⋀︀r̸=i ¬bidi))) J7. AG(︀ ⋀︀i∈N(choice = winsi → payi = price))︀ J8. AG(︀ ⋀︀i∈N(choice ̸= winsi → payi = 0))︀ J9. ⋀︀ ∈Θ(∃. NE(, ) ∧ F(term ∧ 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 eficient for some Nash equilibrium, for all type
profiles [
We present a novel approach for AMD based on Strategy Logic and formal methods, which builds an important bridge between logics for strategic reasoning in MAS and economic theory (in particular, computational social choice and mechanisms design). In the results presented here, in which mechanisms can be automatically generated from partial or complete specifications in a rich logical language. The great expressiveness of the specification language SL[ℱ ] makes our approach of automated synthesis very general, unlike previous proposals. Another advantage is the use of formal methods, which are developed to guarantee their correctness by construction. While mechanism synthesis from SL[ℱ ] specifications is undecidable, we solve it when the number of actions is bounded.
This work is part of a paper accepted at IJCAI-ECAI 22. This research is supported by the ANR project AGAPE ANR-18-CE23-0013, the PRIN project RIPER (No. 20203FFYLK), and the EU ICT-48 2020 project TAILOR (No. 952215).