Overview of the tutorial
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. We conclude by a presentation of the demo tool for verification of strategic ability, developed recently at PAS.
Type: Tutorial
Prerequisites: The tutorial is addressed to all researchers in multi-agent systems. 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.
Program
The tutorial starts with a lightweight introduction to logic-based verification methods for multi-agent systems. Then, we proceed to more advanced topics (complexity results, state of the art algorithms for approximate and partial verification, semantic equivalences, and model reductions). It is important to note that the advanced concepts will not be presented in-depth. Instead, we will use examples and hands-on experience with tools to convey the intuitions, and provide the background for those participants who may want to study the subject further.
The tutorial consists of the following parts:
Gentle introduction to model checking for multi-agent systems.
- Formal verification: why, when, and what.
- Modeling MAS.
- Specification of properties: temporal, epistemic, and strategic logic.
- Motivating example: voting, coercion, and coercion-resistance.
Verification of strategic properties.
- Modal logic meets game theory: alternating-time temporal logics ATL and ATL*. Standard fixpoint model checking algorithm for ATL.
- Abilities under imperfect information: problems with strategies. Imperfect information ATL.
- Complexity of model checking for semantic variants of ATL.
Practical model checking algorithms.
- Practical complexity: state-space, transition-space, and strategy-space explosion.
- How to overcome the complexity: approximate and incomplete verification.
- Fixpoint approximation of strategic ability.
- Strategy synthesis based on strategic dominance.
Model reductions.
- Factors of complexity: models vs. formulas.
- How to overcome the complexity, pt. II: model reductions.
- Bisimulation-based reduction for ATL with imperfect information.
- Partial-order reduction.
Tools and examples.
- Tools for model checking: UPPAAL, MCMAS, STV.
- Hands-on exercises: simple voting and coercion.
- Case study: verification of the SELENE voting protocol.