OVERLAY Formally Reasoning about Strategies in Mechanisms Munyque Mittelmann 0 Università degli Studi di Napoli Federico II , Italy 2022 4

In this paper, we present recently published work that proposes a new approach for Mechanism Design, the problem of designing games for aggregating preferences into social decisions. This approach is based on formal methods and logics for strategic reasoning in Multi-Agent Systems.

 eol>Strategic Reasoning Formal Methods Multi-Agent Systems Mechanism Design 1. Introduction

When considering settings with multiple agents, two main possible situations arise. The first is when all agents can be assumed to share a common purpose. For instance, teams of cooperating agents have been considered in a wide range of applications including operations for search and rescue, surveillance, and space exploration [ 1 ]. However, a second scenario happens when some (or all) agents in the environment have their own, possibly conflicting, goals and preferences [ 2 ]. This is the case, for instance, when considering voting systems: agents may not share the same preference over the candidates. Moreover, some agents may even try to manipulate the results of an election through bribing and coercion to convince others to change their votes.

Much progress has been done in the development of logics for strategic reasoning in MultiAgent Systems, including the formulation of Alternating-Time Temporal Logic (ATL) [ 3 ], Strategy Logic (SL) [ 4, 5 ] and its extensions to imperfect information [ 6, 7, 8 ], and quantitative semantics (denoted SL[ℱ ]) [ 9 ]. On the other side, research in economics has been concerned with the design of games (aka mechanisms) for aggregating individual preferences, while motivating agents to behave well (e.g., being truthful) and ensuring the quality of social decisions (e.g., allocative eficiency) [ 10 ]. The real-world applications of designing and verifying mechanisms for social choice are manifold, including the classic problems on auctions, markets, and government policies. Furthermore, new and trending applications include fair division protocols [ 11 ], secure voting [ 12 ], and even the formulation of human rights for economical development [ 13 ]. The problem of formally reasoning about mechanisms is, however, nontrivial: it requires considering quantitative information (e.g., utilities and payments), non-determinism, incomplete (e.g., Bayesian) and imperfect information about the participant’s preferences, and complex strategic concepts (such as strategy dominance and equilibria).

In this paper, we present recently published work [ 14, 15, 16 ] that proposes a new approach for Mechanism Design (MD) based on the logics developed for strategic reasoning in MAS. By enhancing the connection between diferent research communities, we aim to facilitate the adoption of techniques from each field (for instance, the synthesis of game arenas from the algorithms for solving satisfiability). The logical formalization of MD may provide an inherently diferent view of social choice problems from the classical characterizations.

We start by presenting the base logic on which this approach of mechanism design is built, namely the Quantitative Strategy Logic, SL[ℱ ]. Next, we summarize some recent results in extending and applying such logic for reasoning about mechanisms. Finally, we conclude with a short discussion and directions for future work.

 2. Quantitative Strategy Logic Let us first present SL[ℱ ] [9] syntax and semantics.

Definition 1.

 The syntax of SL[ℱ ] is defined by the grammar

::= | ∃. | (i, ) | (, ..., ) | X | U where ∈ AP is an atomic proposition, ∈ Var is a strategy variable, i ∈ N is an agent, and ∈ ℱ is a function in [ − 1, 1 ].

The intuitive reading is: ∃. 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, resp., 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 → [ − 1, 1 ] is a weight function assigning a value in [ − 1, 1 ] to each atomic proposition in each position.

In a position ∈ , each player i chooses an action i ∈ ℬ, and the game proceeds to position (, ) where = (i)i∈N is the action profile (i.e., , a tuple with an action for each agent). 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’ 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. 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.

Definition 3. (Partial, see complete def. in [ 9 ]) Let be a wCGS, and an assignment. The satisfaction value (ℎ) ∈ [ − 1, 1 ] of an SL[ℱ ] formula in a history ℎ is defined as follows: J K (ℎ) = ℓ(last(ℎ), )

J K

J∃. K(ℎ) = m∈SatxrJ K[↦→ ](ℎ)

J(i, ) K(ℎ) = J K[i↦→()](ℎ)

 3. Reasoning about Mechanisms We now briefly describe recent work at extending and applying SL[ℱ ] to MD. 3.1. Verification of Mechanisms under Imperfect Information

In [ 14 ] we propose an epistemic extension of SL[ℱ ], denoted SLK[ℱ ], for considering imperfect information about agents’ preferences (or types). We show how SLK[ℱ ] can express solution concepts (such as Nash equilibria) and fundamental properties from mechanisms, including budget-balance, individual rationality, strategyproofness and Pareto optimality. We prove that our encoding of such properties is correct w.r.t. the classical definitions from economics.

For instance, a strategy profile is a Nash equlibrium (NE) if no agent can increase her utility with a unilateral change of strategy [ 17 ]. Which is expressed with the SLK[ℱ ]-formula: NE() =def ⋀︁ ∀. [︀ (N− i, − i)(i, )Futili ≤ (N, )Futili]︀

i∈N where = (i)i∈N is a profile of strategy variables (for details, see [ 14 ]).

Similarly, individual rationality (IR) is a property of mechanisms in which each agent can ensure to always get nonnegative utility [18], which is encoded with our approach by evaluating the formula IR =def ⋀︀i∈N 0 ≤ utili in strategic equilibrium.

We then consider epistemic aspects and show how, thanks to the epistemic operators in SLK[ℱ ], we can express properties relating agents’ revenues with their knowledge about other agents’ preferences. Verifying that a mechanism satisfies a property then consists in model checking an SLK[ℱ ]formula, which we show can be done in Pspace for memoryless strategies.

 3.2. Mechanisms with Natural Strategies

A Natural Strategy [19, 20] is a list of condition-action pairs, denoting the action the agent will take in case the condition is met. In [ 15 ] we have extended SL[ℱ ] to handle this type of strategies. The resulting language, denoted NatSL[ℱ ], provides a tool for reasoning about mechanisms in relation to strategies with bounded complexity. We demonstrated the usefulness of our approach by modeling and evaluating strategies for repeated keyword auctions. In terms of technical results, we proved that the model checking problem for NatSL[ℱ ] is Pspace-complete, that is, no harder than model checking for the much less expressive language of quantitative LTL (LTL[ℱ ]). We also showed that NatSL[ℱ ] has incomparable distinguishing and expressive power to SL[ℱ ]. This means that the characterizations based on simple bounded strategies ofer an inherently diferent view of mechanisms from characterizations using combinatorial strategies of arbitrary complexity.

3.3. Mechanism Synthesis

In [ 16 ], we rephrased the problem of designing new mechanisms in terms of synthesis from SL[ℱ ]-specifications. Such specifications may include not only game rules but also requirements over the strategic behavior of participants and quality of the outcome. While mechanism synthesis from SL[ℱ ]formulas is undecidable, we solve it in two cases: when the number of actions is bounded, and when agents play in turn. These two restrictions still preserve enough expressiveness to model relevant scenarios of mechanism synthesis, which we illustrate with examples based on auctions. The quantitative semantics of SL[ℱ ] makes it possible to synthesize mechanisms that approximate a specification (satisfy it as much as possible), or maximize some value (such as social welfare in an equilibrium), which is not possible with SL.

4. Discussion

In this paper, we discuss a novel approach for Automated Mechanism Design in which mechanisms can be automatically (i) verified with respect to epistemic and quantitative properties (ii) verified with respect to natural strategies, and (ii) generated (or synthesized) from partial or complete specifications in a rich logical language. An advantage of our approach lies in the high expressivity and generality of logics for strategic reasoning. Moreover, by relying on precise semantics, formal methods provide tools for rigorously analyzing the correctness of systems, which is important to improve trust in mechanisms (fully or partially) created by machines. The ability of SL to naturally express key strategic concepts such as Nash Equilibria, and the possibility to extend it with quantitative aspects and epistemic operators, as we do with SLK[ℱ ], make it a perfect candidate to become a standard logic for verifying mechanisms.

The present setting is enough to capture many kinds of mechanisms where memoryless strategies are suficient to represent the agents’ behavior, such as one-shot or English auctions. However, when participating in sequential auctions, agents could gather information from other agents’ behavior and act based on what happened in previous steps of the game [21]. For such situations we plan to study further the model-checking problem for SLK[ℱ ] with perfect recall. In the qualitative setting already, imperfect information yields undecidability, but known decidable cases exist [ 7, 6 ]. We will investigate them in the quantitative case. Yet another interesting direction for future work is to study the complexity of synthesizing from SL[ℱ ]-fragments, inspired from the SL-fragments One-Goal SL [22, 23] and Simple-Goal SL [24], 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.

Acknowledgments

I am very grateful to my co-authors Laurent Perrussel, Aniello Murano, Bastien Maubert, Francesco Belardinelli, Wojtek Jamroga, Vadim Malvone. This research is supported by the ANR project AGAPE ANR-18-CE23-0013 and the PRIN project RIPER (No. 20203FFYLK). computational eficiency, University of Pennsylvania Philadelphia, PA, 2001. [18] N. Nisan, T. Roughgarden, É. Tardos, V. Vazirani, Algorithmic Game Theory, Cambridge

University Press, 2007. [19] W. Jamroga, V. Malvone, A. Murano, Natural strategic ability, Artificial Intelligence 277 (2019) 103170. [20] W. Jamroga, V. Malvone, A. Murano, Natural strategic ability under imperfect information, in: Proceedings of the International Conference on Autonomous Agents and MultiAgent Systems (AAMAS 2019), International Foundation for Autonomous Agents and Multiagent Systems, Richland, 2019, p. 962–970. [21] T. D. Jeitschko, Learning in sequential auctions, Southern Economic Journal (1998) 98–112. [22] F. Mogavero, A. Murano, G. Perelli, M. Y. Vardi, Reasoning about strategies: on the satisfiability problem, Logical Methods in Computer Science 13 (2017). URL: https://doi. org/10.23638/LMCS-13(1:9)2017. doi:10.23638/LMCS-13(1:9)2017. [23] P. Cermák, A. Lomuscio, A. Murano, Verifying and synthesising multi-agent systems against one-goal strategy logic specifications, in: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI 2015), 2015. [24] F. Belardinelli, W. Jamroga, D. Kurpiewski, V. Malvone, A. Murano, Strategy logic with simple goals: Tractable reasoning about strategies, in: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2019), 2019.

 [1] Y. Wang , E. Garcia , D. Casbeer , F. Zhang (Eds.), Cooperative Control of MultiAgent Systems , Wiley, 2017 . URL: https://doi.org/10.1002/9781119266235. doi: 10 .1002/ 9781119266235. [2] W. van der Hoek , M. Wooldridge, Chapter 24 multi-agent systems , in: Handbook of Knowledge Representation, Elsevier , 2008 , pp. 887 - 928 . URL: https://doi.org/10.1016/ s1574- 6526 ( 07 ) 03024 - 6 . doi: 10 .1016/s1574- 6526 ( 07 ) 03024 - 6 . [3] R. Alur , T. A. Henzinger , O. Kupferman , Alternating-time temporal logic , Journal of the ACM 49 ( 2002 ) 672 - 713 . [4] K. Chatterjee , T. A. Henzinger , N. Piterman , Strategy logic, Information and Computation 208 ( 2010 ) 677 - 693 . [5] F. Mogavero , A. Murano , G. Perelli, M. Y. Vardi , Reasoning about strategies: On the model-checking problem , ACM Transactions on Computational Logic (TOCL) 15 ( 2014 ) 1 - 47 . [6] F. Belardinelli , A. Lomuscio , A. Murano , S. Rubin , Verification of multi-agent systems with public actions against strategy logic , Artificial Intelligence 285 ( 2020 ). [7] R. Berthon , B. Maubert , A. Murano , S. Rubin , M. Vardi , Strategy logic with imperfect information , ACM Transactions on Computational Logic 22 ( 2021 ). [8] P. Cermák , A. Lomuscio , F. Mogavero , A. Murano , Practical verification of multi-agent systems against SLK specifications , Information and Computation 261 ( 2018 ) 588 - 614 . [9] P. Bouyer , O. Kupferman , N. Markey , B. Maubert , A. Murano , G. Perelli, Reasoning about quality and fuzziness of strategic behaviours , in: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2019 ), 2019 . [10] T. Sandholm , Automated mechanism design: A new application area for search algorithms , in: Principles and Practice of Constraint Programming - CP 2003 , Springer Berlin Heidelberg, Berlin, Heidelberg, 2003 , pp. 19 - 36 . [11] J. Lang , J. Rothe , Fair division of indivisible goods , in: Economics and Computation , Springer, 2016 , pp. 493 - 550 . [12] W. Jamroga , M. Tabatabaei , Preventing coercion in e-voting: Be open and commit , in: Proc. Elect . Voting- 16 , 2016 . [13] D. Mohan , Social choice theory and its application in a human rights based approach to development, Journal of governance & regulation ( 2017 ) 7 - 13 . [14] B. Maubert , M. Mittelmann , A. Murano , L. Perrussel, Strategic reasoning in automated mechanism design , in: Proc. of the Int. Conference on Principles of Knowledge Representation and Reasoning (KR 2021 ), 2021 , pp. 487 - 496 . [15] F. Belardinelli , W. Jamroga , V. Malvone , M. Mittelmann , A. Murano , L. Perrussel , Reasoning about human-friendly strategies in repeated keyword auctions , in: Proceedings of the International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2022 ), ACM, 2022 , pp. 1602 - 1604 . [16] M. Mittelmann , B. Maubert , A. Murano , L. Perrussel, Automated synthesis of mechanisms, in: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2022 ), 2022 . [17] D. C. Parkes , L. H. Ungar , Iterative combinatorial auctions: Achieving economic and