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.  

1.  Introduction to formal verification

   • Linear and branching-time temporal logics

   • Decision problems: model checking and satisfiability
     
     

2. Logics for Multi-Agent Systems

   • Concurrent game structures

   • Alternating-Time Temporal Logic (ATL*)

   • Strategy Logic (SL)

   • Model checking ATL* and SL
     
     

3. Quantitative verification 

   • Quantitative Semantics for ATL* and SL

   • Temporal discounting

   • Complexity results for model checking

4. Going further

3. • Research directions on logics for MAS

   • Discussion of existing model-checkers (MCMAS, Vitamin, STV)

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.

• 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.