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 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. In this tutorial, we present a lightweight 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 and model reductions, which can lead to practical solutions for the notoriously hard problem. We conclude by a presentation of the experimental tool for verification of strategic ability, being developed at the Polish Academy of Sciences.

1. Gentle introduction to model checking for multi-agent systems.
   1. Formal verification: why, when, and what.
   2. Modeling MAS.
   3. Specification of properties: temporal, epistemic, and strategic logic.
   4. Motivating example: voting, coercion, and coercion-resistance.

2. Verification of strategic properties.
   1. Modal logic meets game theory: standard fixpoint model checking algorithm for perfect information games.
   2. Abilities under imperfect information: problems with strategies. Imperfect information ATL.
   3. Complexity of model checking for semantic variants of ATL.

3. Practical model checking algorithms.
   1. Practical complexity: state-space, transition-space, and strategy-space explosion.
   2. How to overcome the complexity, pt. I: approximate and incomplete verification.
   3. Fixpoint approximation of strategic ability.
   4. Incomplete brute-force search and optimizations based on strategic dominance.
   5. Experimental results.

4. Model reductions.
   1. Factors of complexity: models vs. formulas.
   2. How to overcome the complexity, pt. II: model reductions.
   3. Bisimulation-based reduction for ATL with imperfect information.
   4. Partial-order reduction.

5. Tools and examples.
   1. Tools for model checking: STV.
   2. Case study: verification of the SELENE voting protocol.

Materials

The lecture slides are available here.