The design of mechanisms for aggregating preferences while achieving a socially desirable outcome is a central problem in Multi-Agent Systems. In this paper, we motivate a recent approach [1] for formally verifying Bayesian mechanisms using a logic for strategic reasoning, namely Probabilistic Strategy Logic. This approach has been used to encode classic notions from Mechanism Design, including, BayesianNash equilibrium and incentive compatibility.
and properties such as eficiency and strategyproofness in Epistemic SL[ℱ ]. Similarly, SL[ℱ ] with natural strategies have been considered for reasoning with bounded recall [18]. Finally, the automated design of deterministic mechanisms was reduced to SL[ℱ ]-synthesis in [19]. However, SL[ℱ ] semantics is deterministic and thus the logic is unable to express probabilistic features, which are essential when considering Bayesian and randomized mechanisms. Related Work In probabilistic model checking, specifications are given in probabilistic logics, and their validity is evaluated w.r.t. a system. For instance, the problem has been considered for Probabilistic ATL Chen and Lu [20], Probabilistic Alternating-Time -Calculus [21], and Probabilistic Strategy Logic [22]. Probabilistic ATL has been also studied in the setting of imperfect information and memoryless strategies [23], and with accumulated costs/rewards [24]. In algorithmic mechanism design, probabilistic verification refers to the use of statistical tests to evaluate mechanisms [25]. It has been considered, for instance, in the standard mechanism design setting Ball and Kattwinkel [26] and for obviously strategy-proof mechanisms [27].
The approach recently proposed in [
Unlike previous proposals, the automated verification of Bayesian mechanisms using Probabilistic Strategy Logic (PSL) is able to take into account a wide range of settings (e.g. randomized, indirect, and Bayesian mechanisms). Furthermore, thanks to the great expressiveness of the specification language, PSL, the verification ex ante, interim and ex post of complex solution concepts and properties is fully automated through model checking of logical formulas.
This research has been supported by the PRIN project RIPER (No. 20203FFYLK), the ANR project AGAPE ANR-18-CE23-0013, and the EU H2020 Marie Sklodowska-Curie project with grant agreement No 101105549. This abstract is based on the AAAI 2023 paper “Formal Verification of Bayesian Mechanisms”. quality and fuzziness of strategic behaviours, in: Proc. of IJCAI 2019, 2019. [17] B. Maubert, M. Mittelmann, A. Murano, L. Perrussel, Strategic reasoning in automated mechanism design, in: KR-21, 2021. [18] F. Belardinelli, W. Jamroga, V. Malvone, M. Mittelmann, A. Murano, L. Perrussel, Reasoning about human-friendly strategies in repeated keyword auctions, in: AAMAS-22, 2022. [19] M. Mittelmann, B. Maubert, A. Murano, L. Perrussel, Automated synthesis of mechanisms, in: IJCAI-22, 2022. [20] T. Chen, J. Lu, Probabilistic alternating-time temporal logic and model checking algorithm, in: Proc. of FSKD, 2007, pp. 35–39. [21] F. Song, Y. Zhang, T. Chen, Y. Tang, Z. Xu, Probabilistic alternating-time -calculus, in:
Proc. of AAAI 2019, 2019, pp. 6179–6186. [22] B. Aminof, M. Kwiatkowska, B. Maubert, A. Murano, S. Rubin, Probabilistic strategy logic, in: Proc. of IJCAI-19, 2019. [23] F. Belardinelli, W. Jamroga, M. Mittelmann, A. Murano, Strategic abilities of forgetful agents in stochastic environments, in: Proc. of KR-23, 2023. [24] T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, A. Simaitis, Automatic verification of competitive stochastic systems, Formal Methods in System Design 43 (2013) 61–92. [25] I. Caragiannis, E. Elkind, M. Szegedy, L. Yu, Mechanism design: From partial to probabilistic verification, in: Proceedings of the 13th ACM Conference on Electronic Commerce, EC ’12, Association for Computing Machinery, New York, NY, USA, 2012, p. 266–283. URL: https://doi.org/10.1145/2229012.2229035. doi:10.1145/2229012.2229035. [26] I. Ball, D. Kattwinkel, Probabilistic verification in mechanism design, in: Proceedings of the 2019 ACM Conference on Economics and Computation, EC ’19, Association for Computing Machinery, New York, NY, USA, 2019, p. 389–390. URL: https://doi.org/10.1145/ 3328526.3329657. doi:10.1145/3328526.3329657. [27] D. Ferraioli, C. Ventre, Probabilistic verification for obviously strategyproof mechanisms, in: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS ’18, 2018, p. 1930–1932.