Automated verification of discrete-state systems has been a hot topic in computer science for
over 35 years. The idea found its way into AI and multi-agent systems in late 1990’s, and techniques for verification of such systems have been in constant development since then. Model checking of temporal, epistemic, and strategic properties is one of the most prominent and most successful approaches here.
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.
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.
Wojciech Jamroga is a full professor at the Polish Academy of Sciences and a research scientist at the University of Luxembourg. His research focuses on modeling, specification and verification of interaction between autonomous agents. 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 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. 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, ESSLLI 2010, and EASSS in 2006, 2007, and 2017.
