In this paper, I summarize the results obtained in my thesis, whose aim was to investigate the use of formal methods for the specification, design, and evaluation of mechanisms, with a focus on auctions. We address such challenges by introducing logic-based approaches for representing and designing auctionbased markets with strategic players. Firstly, for providing a foundation for general and automated auction playing in MAS, we propose a framework for representing auctions, denoted Auction Description Language (ADL). ADL addresses important dimensions of auction-based markets and is general enough to represent most auction settings. Second, we propose a novel approach for reasoning and designing new auctions (and, in general, mechanisms) based on formal methods. Such an approach for Automated Mechanism Design aims to automatically generate mechanisms from their specifications and verify them in relation to target economical properties. We demonstrate how this approach can express key concepts from Economic Theory (including Nash equilibrium and strategyproofness) and how it enables automatically generating optimal mechanisms from a quantitative logical specification.
An auction is a popular mechanism that aggregates participants’ bids into a social decision, usually expressed in terms of allocations and payments. Automated agents are widely used in auction-based markets but software agents are usually designed to act on a specific context, which prevents them from switching between diferent kinds of markets. For doing so, they should be able to “understand” the auction rules and reason about their own valuations and also about other players private information valuations. This limitation inspires the development of a lightweight logic-based language for representing the rules of an auction market.
More than describing, the design and evaluation of new auctions (and, more generally,
mechanisms) is a central problem in multiagent settings [
My thesis [6] addressed such challenges by introducing logic-based approaches for representing and designing auction-based markets with strategic players. Our motivation is two fold: first, we aim to provide a foundation for general and automated auction playing in MAS, by establishing a logical framework to create a good balance between expressive power and computational eficiency. Second, we propose a novel approach based on formal methods for (i) reasoning about auctions under strategic behavior and (ii) Automated Mechanism Design. Such approach aims to automatically generate auctions from their specifications and verify them in relation to target economical properties.
Representation of Auctions There are numerous variants of auctions depending on
the parameters considered, including the number of distinct items and copies as well
as the number of sellers and buyers [7, 8]. For a fixed set of parameters, the protocol,
i.e., the bidding, payment and allocation rules, may also difer. Building intelligent
agents that can switch between diferent auctions and process their rules is a key issue
for building automated auction-based marketplaces. In this scenario, the auctioneer
should at first allow participants to express their preferences and second describe the
rules governing the market. In relation to the formal representation of auction rules,
we recall the descriptive auction language [9], which allows the specification of auctions
by allowing players to bid using the XOR language. Rule-based approaches have also
being used for representing single-dimensional auctions [10] and negotiation protocols
[11]. Similarly, negotiation protocols have being handled with meta-languages [12], the
Extensible Markup Language [13] and rule-markup languages [14]. Since the above
languages lack a precise semantics, Wooldridge and Parsons (2000, 2000) motivate and
compare the use of diferent logical languages for specifying negotiation protocols. In
the context of General Game Playing (GGP), the Game Description Language (GDL)
was designed for specifying game rules while maintaining a tractable complexity [17].
This language has been extended to deal with integer values [18] and epistemic operators
[19]. The use of languages inspired on GDL for describing market-based protocols have
been studied in the context of negotiation [20, 21] and single-item markets [22]. Such
approaches lack a clear link between the language, the mechanism formalization and the
agents’ preferences, which is a key aspect for enabling reasoning about auctions.
Automated Mechanism Design Designing an auction in such manner to ensure features
of the outcome alongside with a desirable behavior of the participants is a key challenge
in Economics. In fact, this problem is known as Mechanism Design: the formulation
of game-like systems whose equilibria satisfy some desired properties, usually expressed
in terms of incentive, utility or social welfare. Traditionally, mechanisms have been
formulated and verified by human specialists, who use their knowledge and experience
for defining the game rules. Creating and verifying mechanisms which will be played
by strategic agents can be a very dificult and time-consuming task. Sandholm (2003)
introduced Automated Mechanism Design (AMD), whose goal is to automatically create
mechanisms for solving a specific preference aggregation problem. AMD is usually
handled as an optimization and domain-oriented problem. Most solutions used on the
literature are based on machine learning, which include, for instance, neural networks
[24, 25] and statistical techniques [26]. A number of works explore computed-aided
verification of auctions [ 27, 28, 29], where the process is assisted by a reasoner. In the
context of fully-automatic verification, Pauly and Wooldridge (2003 ) and Wooldridge
et al. (2007 ) advocate the use of Alternating-time Temporal Logic (ATL) [32] to reason
about mechanisms. The main limitation in these works is the purely qualitative setting
and the impossibility of expressing key strategic concepts such as dominance in the logic.
Logics for Strategic Reasoning This work is also related to the long-established logical
approach to systems verification [
We addressed the problem of modeling and analyzing auction mechanisms for MAS using logics and strategic reasoning. First, we provided a framework for representing auctions, denoted Auction Description Language (ADL) [39, 40, 41]. ADL addresses important dimensions of auction-based markets and is general enough to represent most auction settings. We illustrated the generality of ADL by modeling a number of representative auctions. We demonstrated how this language can be used for the automated verification of direct mechanisms and for automatically checking well-formedness of auction descriptions. We then extended ADL with knowledge operators and an action modality [42, 43] (denoted Epistemic ADL, or simply ADLK) for providing a ground for the design of general auction players and characterizing their rational behavior when reasoning about the efect of actions and other players rationality. We show that the model-checking problem for ADL-formulas belongs to Ptime when it involves functions that be computed in polynomial time. By the other hand, we show that the model-checking problem for ADLK is in Exptime.
In relation to Automated Mechanism Design, we investigate logical frameworks for strategic reasoning about mechanisms. We first propose a new variant of Strategy Logic with quantitative features, imperfect information and epistemic operators, denoted SLK[ℱ ] [44]. We demonstrated how SLK[ℱ ] can express the implementation of social choice functions and be used for automatically verifying a number of important concepts and properties often required in auctions, or more generally in mechanism design. We also show how we can express properties relating agents’ revenues with respect to their beliefs about other agents’ preferences. We showed that verifying a mechanism in relation to classical properties boils-down to model checking a SLK[ℱ ] formula and we prove it can be done in Pspace for memoryless strategies.
We then introduced a quantitative semantics for SL with natural strategies and imperfect information (denoted NatSL[ℱ]) [45], which provides a new perspective for formal verification and design of novel mechanisms based on the complexity of strategies. We show how to model popular strategies for repeated keyword auctions using NatSL[ℱ] and prove properties pertaining to this game; We proved that the modelchecking problem for NatSL[ℱ] is Pspace-complete and that NatSL[ℱ] has incomparable distinguishing and expressive power to SL[ℱ ]. Finally, we ofered a novel perspective on the design of mechanisms by rephrasing the AMD problem in terms of synthesis from SL[ℱ ] specifications [ 46, 47]. This approach enables automatically generating optimal mechanisms from a quantitative logical specification, which may include not only game rules but also requirements over the strategic behavior of participants and quality of the outcome. We solved the synthesis problem for SL[ℱ ] by investigating the related satisfiability problem in two cases: action-bounded and turn-based mechanisms.
In a recent work [48], we considered the use of the probabilistic extension of SL [49] to handle stochastic features often present in auctions. Going from deterministic setting to a more general and probabilistic one is challenging due to several aspects. First, the wide and heterogeneous range of settings considered in the literature obscures the path for a general and formal approach to verification. The setting may consider deterministic or randomized mechanisms, incomplete information about agents’ types (Bayesian mechanisms), mixed or pure strategies and iterative protocols (indirect mechanisms). Second, considering Bayesian mechanisms brings out diferent methods for evaluating a mechanism according to the time-line for revealing the incomplete information as the game is run.
We studied the verification of mechanisms under memoryless combinatorial strategies and Natural Strategies with bounded recall. This setting is enough to capture many kinds of auctions (such as one-shot or English auctions) where memoryless strategies are suficient to represent the bidders behaviour since all the relevant information can be encoded in a state. However, when participating in repeated auctions, agents could gather information from other agents behaviour and act based on what happened in previous instances of the game. An interesting direction is, then, to investigate the use of strategies with recall for learning other players’ valuations based on their behavior. For such situations we can study the model-checking problem for SLK[ℱ ] with memoryful strategies. In the qualitative setting already, imperfect information yields undecidability, but known decidable cases exist [37, 36], which should be considered also in the quantitative case.
We believe the automated synthesis of mechanisms is a promising and powerful tool for AMD. However, the high expressiveness of SL[ℱ ] 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[ℱ ]-fragments, inspired from the SL-fragments One-Goal SL [50, 51] and Simple-Goal SL [52], 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. On a related vein, we can study the translation of ADL to SL[ℱ ]-formulae, so as to include the auction description in the mechanism specification. In this setting, SL[ℱ ] formulae can be used to express requirements of well-formed auction descriptions.
The problems contemplated in my thesis are also worth investigating from an empirical perspective. One direction is to explore the interplay between agents’ bounded rationality and the auctioneer revenue so as to understand the impact of bounded rationality on mechanism design. An implementation of a model checker for NatSL[ℱ] would enable the empirical evaluation of natural strategies and auctions played by participants with restricted memory. Finally, experimental results could be used to assess the practical relevance of our proposed approaches, especially in relation to mechanism synthesis from SL[ℱ ] specification due to the high theoretical complexity of the problem.
I am very grateful to my co-authors Laurent Perrussel, Aniello Murano, Bastien Maubert, Francesco Belardinelli, Wojtek Jamroga, Vadim Malvone, Andreas Herzig, and Sylvain Bouveret. This research is supported by the ANR project AGAPE ANR-18-CE23-0013 and the PRIN project RIPER (No. 20203FFYLK). [4] C. David, D. Kroening, Program synthesis: challenges and opportunities,
Philosophical Transactions of the Royal Society A 375 (2017) 20150403. [5] M. Pauly, M. Wooldridge, Logic for mechanism design–a manifesto, in: Workshop on Game Theory and Decision Theory in Agent Systems (GTDT), 2003. [6] M. Mittelmann, Logics for Representation and Design of Auctions, Ph.D. thesis,
Universitè de Toulouse, 2022. [7] P. Klemperer, Auction theory: A guide to the literature, Journal of Economic
Surveys 13 (1999) 227–286. [8] V. Krishna, Auction Theory, Academic Press, 2009. [9] D. Rolli, S. Luckner, H. Gimpel, C. Weinhardt, A Descriptive Auction Language,
Electronic Markets 16 (2006) 51–62. [10] K. M. Lochner, M. P. Wellman, Rule-based specification of auction mechanisms, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004) 2 (2004) 818–825. [11] C. Bădică, M. Ganzha, M. Paprzycki, Rule-based automated price negotiation: Overview and experiment, in: Artificial Intelligence and Soft Computing (ICAISC 2006), Springer Berlin Heidelberg, Berlin, Heidelberg, 2006, pp. 1050–1059. [12] S. Hudert, H. Ludwig, G. Wirtz, Negotiating SLAs-An approach for a generic negotiation framework for WS-agreement, Journal of Grid Computing 7 (2009) 225–246. [13] S. Hudert, T. Eymann, H. Ludwig, G. Wirtz, A negotiation protocol description language for automated service level agreement negotiations, 2009 IEEE Conference on Commerce and Enterprise Computing (CEC 2009) (2009) 162–169. [14] A. Dobriceanu, L. Biscu, C. Badica, Adding a declarative representation of negotiation mechanisms to an agent-based negotiation service, in: 2007 IEEE/WIC/ACM International Conferences on Web Intelligence and Intelligent Agent Technology - Workshops, 2007, pp. 471–474. [15] M. Wooldridge, S. Parsons, Languages for negotiation, in: Proceedings of the 14th
European Conference on Artificial Intelligence (ECAI 2000), IOS Press, NLD, 2000. [16] M. Wooldridge, S. Parsons, On the use of logic in negotiation, in: Proceedings of the Autonomous Agents Workshop on Agent Communication Languages and Conversation Protocols, 2000. [17] M. Genesereth, M. Thielscher, General game playing, Synthesis Lectures on Artificial
Intelligence and Machine Learning, Morgan & Claypool Publishers, 2014. [18] M. Mittelmann, L. Perrussel, Game description logic with integers: A GDL numerical extension, in: Proceedings of the International Symposium on Foundations of Information and Knowledge Systems (FoIKS 2020), 2020. [19] G. Jiang, D. Zhang, L. Perrussel, H. Zhang, Epistemic GDL: A logic for representing and reasoning about imperfect information games, in: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2016), 2016. [20] D. d. Jonge, D. Zhang, Using GDL to represent domain knowledge for automated negotiations, in: Proc. of Autonomous Agents and Multi-Agent Systems Workshops, AAMAS 2016 Workshops, 2016, pp. 134–153. [21] D. de Jonge, D. Zhang, GDL as a unifying domain description language for declarative automated negotiation, Autonomous Agents and Multi-Agent Systems 35 (2021) 13. [22] M. Thielscher, D. Zhang, From General Game Descriptions to a Market Specification
Language for General Trading Agents, Springer Berlin Heidelberg, 2010, pp. 259–274. [23] 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. [24] W. Shen, P. Tang, S. Zuo, Automated mechanism design via neural networks, in: Proceedings of the International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2019), 2019. [25] P. Dütting, Z. Feng, H. Narasimhan, D. Parkes, S. S. Ravindranath, Optimal auctions through deep learning, in: Proceedings of the International Conference on Machine Learning (ICML 2019), 2019. [26] H. Narasimhan, S. B. Agarwal, D. C. Parkes, Automated mechanism design without money via machine learning, in: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2016), 2016. [27] M. Caminati, M. Kerber, C. Lange, C. Rowat, Sound auction specification and implementation, in: ACM Conference on Economics and Computation, 2015. [28] G. Barthe, M. Gaboardi, E. Arias, J. Hsu, A. Roth, P.-Y. Strub, Computer-aided verification for mechanism design, in: Conf. on Web and Internet Economics, 2016. [29] M. Kerber, C. Lange, C. Rowat, An introduction to mechanized reasoning, Journal of Mathematical Economics 66 (2016) 26 – 39. [30] M. Pauly, R. Parikh, Game logic-an overview, Studia Logica 75 (2003) 165–182. [31] M. Wooldridge, T. Ågotnes, P. Dunne, W. Van der Hoek, Logic for automated mechanism design-a progress report, in: Proceedings of AAAI Conference on Artificial Intelligence (AAAI 2007), 2007. [32] R. Alur, T. A. Henzinger, O. Kupferman, Alternating-time temporal logic, Journal of the ACM 49 (2002) 672–713. [33] K. Chatterjee, T. A. Henzinger, N. Piterman, Strategy logic, Information and
Computation 208 (2010) 677–693. [34] 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. [35] 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. [36] F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin, Verification of multi-agent systems with public actions against strategy logic, Artificial Intelligence 285 (2020). [37] R. Berthon, B. Maubert, A. Murano, S. Rubin, M. Vardi, Strategy logic with imperfect information, ACM Transactions on Computational Logic 22 (2021). [38] P. Cermák, A. Lomuscio, F. Mogavero, A. Murano, Practical verification of multiagent systems against SLK specifications, Information and Computation 261 (2018) 588–614. [39] M. Mittelmann, L. Perrussel, Auction description language (ADL): general framework for representing auction-based markets, in: Proceedings of the European Conference on Artificial Intelligence (ECAI 2020), volume 325, IOS Press, 2020, pp. 825–832. [40] M. Mittelmann, S. Bouveret, L. Perrussel, A general framework for the logical representation of combinatorial exchange protocols, in: Proceedings of the International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2021), ACM, 2021, pp. 1602–1604. [41] M. Mittelmann, S. Bouveret, L. Perrussel, Representing and reasoning about auctions, Autonomous Agents and Multi-Agent Systems 36 (2022) 20. URL: https: //doi.org/10.1007/s10458-022-09547-9. doi:1 0 . 1 0 0 7 / s 1 0 4 5 8 - 0 2 2 - 0 9 5 4 7 - 9 . [42] M. Mittelmann, L. Perrussel, An epistemic logic for reasoning about strategies in general auctions, in: Proceedings of the Workshops of the International Conference on Logic Programming, volume 2678, 2020. [43] M. Mittelmann, A. Herzig, L. Perrussel, Epistemic reasoning about rationality and bids in auctions, in: Proceedings of the European Conference on Logics in Artificial Intelligence (JELIA 2021), volume 12678, Springer, 2021, pp. 116–130. [44] B. Maubert, M. Mittelmann, A. Murano, L. Perrussel, Strategic reasoning in automated mechanism design, in: Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR 2021), 2021, pp. 487–496. [45] 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 MultiAgent Systems (AAMAS 2022), IFAAMAS, 2022, pp. 1602–1604. [46] 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. [47] M. Mittelmann, B. Maubert, A. Murano, L. Perrussel, Synthesis of mechanisms with strategy logic, in: ICTCS, volume 3284 of CEUR Workshop Proceedings, CEUR-WS.org, 2022, pp. 47–52. [48] M. Mittelmann, B. Maubert, A. Murano, L. Perrussel, Formal verification of bayesian mechanisms, in: Proc. of the AAAI Conference on Artificial Intelligence, AAAI 2023, AAAI Press, 2023. [49] B. Aminof, M. Kwiatkowska, B. Maubert, A. Murano, S. Rubin, Probabilistic strategy logic, in: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI 2019), 2019. [50] F. Mogavero, A. Murano, G. Perelli, M. Y. Vardi, Reasoning about strategies: on the satisfiability problem, Logical Methods in Computer Science 13 (2017). [51] 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. [52] 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.