Automated Verification of Multi-Agent Systems. Why, What, and Especially: How?

Automated verification of discrete-state systems has been a hot topic in computer science for over 40 years. The idea found its way into AI and multi-agent systems in early 2000'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.

In this talk, I present a brief introduction to the topic, and mention relevant properties that one might like to verify this way. Then, I describe some very recent results which can potentially lead  to practical solutions. I conclude by a presentation of the experimental tool for verification of strategic ability, being developed by our research group at the Polish Academy of Sciences.