Automated Verification of Multi-Agent Systems:
From Theory to Practice, Made Easy

In this tutorial, we present a brief introduction to the topic, and mention relevant properties that one might like to verify this way. Then, we describe some very recent results on incomplete model checking algorithms and model reductions, which can potentially lead to practical solutions for the notoriously hard problem. In the last part of the tutorial, we present the experimental tool for verification of strategic ability, being developed by our research group at the Polish Academy of Sciences. In particular, we show how the tool can be used to verify simplified versions of two interesting use cases: multi-agent learning and secure voting in an election.

Level: Intermediate.

Target audience & prerequisites: The tutorial is addressed to all researchers in AI. It will be accessible to the general audience; no special knowledge is required. The concepts being presented are pretty involved mathematically, but we will present them by means of simple examples, and avoid exposition of the detailed mathematical machinery.

The slides are available here.

Prof. Jamroga obtained his PhD from the University of Twente, Netherlands in 2004, and completed his habilitation at the Clausthal University of Technology, Germany in 2009. He has coauthored around 150 refereed publications, and has been a Program Committee member of most important conferences and workshops in AI and multi-agent systems. According to Google Scholar, his papers have been cited over 3100 times, and his H-index is 29. The research track of Prof. Jamroga includes the Best Paper Award at the main conference on electronic voting (E-VOTE-ID) in 2016, and a Best Paper Nomination at the main multi-agent systems conference (AAMAS) in 2018.

His teaching record includes numerous courses at ESSLLI (European Summer School in Logic, Language and Information), EASSS (European Agent Systems Summer School), and ESSAI (European Summer School on AI), several courses at doctoral schools, and tutorials at top conferences in AI and multi-agent systems -- all of them on formal methods for multi-agent systems.

Wojciech Penczek is a full professor and the Director of the Institute of Computer Science, Polish Academy of Sciences (PAS), and the chair of the Committee on Informatics of PAS. He has coauthored more than 220 refereed scientific papers on Petri nets, distributed systems, timed systems, model checking, temporal, epistemic and strategic logics, verification of security properties, and web services. According to Google Scholar, his papers have been cited over 3700 times, and his H-index is 34. Among other awards, he received the Best Paper Award at AAMAS in 2004 and a Best Paper Nomination at AAMAS in 2018. His teaching record includes lectures at Advanced Course on Petri Nets 2010, ESSLI 2010, and EASSS in 2006, 2007, and 2017.

Prof. Penczek has been a project leader of the EC-founded project CRIT-2, and played a main role in several national projects. He was a conference chair of ICATPN '10, TIME '18, and ACSD '19, and served as a PC member of over 90 conferences in Computer Science. He is an editor of Fundamenta Informaticae, and the LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC). His scientific activities include also membership in the working group WG2.2 IFIP (International Federation of Information Processing) since 2002. His achievements have been recognized at the national level in Poland. In 2005, the President of Poland awarded him with the Silver Cross of Merit, one of the highest Polish distinctions for his outstanding academic service.

Damian Kurpiewski is a researcher at the Polish Academy of Sciences. His research interests include modelling, specification and verification of strategic interaction between agents in various systems. Currently he is finishing his PhD under the supervision of Prof. Jamroga, with the focus on logic-based verification of voting protocols. Mr. Kurpiewski has played a vital role in recent algorithmic advances for model checking of alternating-time logic with imperfect information. He also leads the development of the STV model checker.