R-CHECK: A Model Checker for Verifying Reconfigurable MAS

TL;DR

R-CHECK is a model checker designed for verifying reconfigurable multi-agent systems, enabling analysis of individual and collective behaviors, interaction protocols, and dynamic reconfiguration features.

Contribution

It introduces a high-level input language with symbolic semantics for modeling complex interaction features in reconfigurable multi-agent systems.

Findings

Supports reasoning about reconfiguration and coalition formation

Allows analysis of joint missions and self-organization

Facilitates verification of multi-agent system behaviors

Abstract

Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.