Formal Aspects of Strategic Reasoning in Multi-Agent Systems
Tutorial @ KR 2024
Presenters: Aniello Murano and Munyque Mittelmann, from the University of Naples Federico II
Contact: munyque.mittelmann[at]unina.it
Brief Description
This tutorial aims to give an overview of the most recent logics introduced in the field of strategic reasoning in MAS. Specifically, starting from the background on verification of MAS, we will introduce the logics ATL* and SL and discuss their main features.
In particular, the tutorial will focus on logics for strategic reasoning and the related model checking and satisfiability problems. We will introduce automata-theoretic techniques to solve the related decision problems. We will then discuss other facets of quantitative verification of logics for MAS and introduce recent work in the field.
Schedule
Introduction to formal verification
Linear and branching-time temporal logics
Decision problems: model checking and satisfiability
Logics for Multi-Agent Systems
Concurrent game structures
Alternating-Time Temporal Logic (ATL*)
Strategy Logic (SL)
Model checking ATL* and SL
Quantitative verification
Quantitative Semantics for ATL* and SL
Temporal discounting
Complexity results for model checking
4. Going further
Research directions on logics for MAS
Discussion of existing model-checkers (MCMAS, Vitamin, STV)
Target Audience and Learning Goals
The tutorial will assume some basic knowledge of propositional, modal, or temporal logic. Basic knowledge of Automata Theory is desirable but not mandatory.
The tutorial introduces a topic that involves different aspects relevant to the KR community. In particular, the target audience consists of researchers working on multi-agent systems, strategic reasoning, formal verification, and logics.
The learning goals are, first, to learn the fundamentals of logics for strategic reasoning. Second, the understanding of how formal methods can be applied to the verification of MAS. Third, to learn about recent developments on quantitative verification and visualize research directions.
Main References
Alur, R.; Henzinger, T. A.; and Kupferman, O. Alternating-time temporal logic. Journal of the ACM 49(5):672–713, 2002.
Bouyer, P.; Kupferman, O.; Markey, N.; Maubert, B.; Murano, A.; and Perelli, G. Reasoning about quality and fuzziness of strategic behaviours. Proc. of IJCAI 2019.
Chatterjee, K.; Henzinger, T. A.; and Piterman, N. Strategy logic. Information and Computation 208(6):677–693, 2010.
Jamroga, W.; Mittelmann, M.; Murano, A.; and Perelli, G. Playing Quantitative Games Against an Authority: On the Module Checking Problem. Proc. of AAMAS 2024.
Clarke, E. M.; Henzinger, T. A.; Veith, H.; Bloem, R. Handbook of Model Checking. Springer, 2018.
Maubert, B.; Mittelmann, M.; Murano, A.; and Perrussel, L. Strategic reasoning in automated mechanism design. In Proc. of KR 2021.
Mittelmann, M.; Murano, A.; and Perrussel, L. Discounting in Strategy Logic. Proc. of IJCAI 2023.
Mogavero, F.; Murano, A.; Perelli, G.; and Vardi, M. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log. 15(4), 2014.
Vardi, M. Y., Wolper, P. An automata-theoretic approach to automatic program verification. Proc. of LICS 1986.