Practical Abstraction for Model Checking of Multi-Agent Systems

TL;DR

This paper introduces an intuitive, agent-based abstraction method for model checking multi-agent systems that simplifies the state space without requiring a full global model, making verification more accessible and efficient.

Contribution

It presents a novel variable-removal abstraction scheme that is easy to understand, formally proven correct, and effective in reducing model complexity for multi-agent systems.

Findings

Significant reduction in model size demonstrated

Method is easy for domain experts to apply

Experimental results on postal voting models show efficiency gains

Abstract

Model checking of multi-agent systems (MAS) is known to be hard, both theoretically and in practice. A smart abstraction of the state space may significantly reduce the model, and facilitate the verification. In this paper, we propose and study an intuitive agent-based abstraction scheme, based on the removal of variables in the representation of a MAS. This allows to do the reduction without generating the global model of the system. Moreover, the process is easy to understand and control even for domain experts with little knowledge of computer science. We formally prove the correctness of the approach, and evaluate the gains experimentally on models of a postal voting procedure.