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

25 July 2022 (morning sessions), Vienna, Austria

Tutorial at IJCAI-ECAI 2022
Lecturers: Catalin Dima and Wojtek Jamroga

Overview

Program and materials

Contact


Overview of the course

The course offers an introduction to some recent advances in formal verification of intelligent agents and multi-agent systems. The focus is on accessible presentation and simple examples, without going too deep into the involved mathematical machinery.

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.




Program of the course

The tutorial consists of the following parts. Parts 1-2 will be presented before the coffee break; parts 3-5 after the break.

  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 following book can be used as introductory material for the interested students.

The lecture slides is available here.




Contact

Prof. Dr. Wojciech Jamroga
University of Luxembourg and Polish Academy of Sciences
E-Mail: wojciech.jamroga--aat--uni.lu
Prof. Dr. Catalin Dima
Universite Paris-Est Creteil
E-Mail: dima at univ-paris12 dot fr