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

15 November 2022, Valencia, Spain

Tutorial at PRIMA 2022
Lecturers: Wojtek Jamroga and Wojtek Penczek

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.

  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 are available here.

STrategic Verifier (STV):


Contact
Prof. Dr. Wojciech Jamroga
University of Luxembourg and Polish Academy of Sciences
E-Mail: wojciech dot jamroga at uni dot lu		 Prof. Dr. Wojciech Penczek
Polish Academy of Sciences
E-Mail: wojciech dot penczek at ipipan dot waw dot pl