Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems

TL;DR

This paper proposes a hybrid verification approach combining model checking and runtime verification to verify multi-agent systems, addressing the challenge of their complexity and undecidability issues.

Contribution

It introduces a novel method that integrates model checking of decidable fragments with runtime verification for the undecidable parts of MAS models.

Findings

The combined approach effectively verifies complex MAS models.

Experimental results demonstrate the practicality of the method.

The technique improves verification coverage for complex systems.

Abstract

Multi-Agent Systems (MAS) are notoriously complex and hard to verify. In fact, it is not trivial to model a MAS, and even when a model is built, it is not always possible to verify, in a formal way, that it is actually behaving as we expect. Usually, it is relevant to know whether an agent is capable of fulfilling its own goals. One possible way to check this is through Model Checking. Specifically, by verifying Alternating-time Temporal Logic (ATL) properties, where the notion of strategies for achieving goals can be described. Unfortunately, the resulting model checking problem is not decidable in general. In this paper, we present a verification procedure based on combining Model Checking and Runtime Verification, where sub-models of the MAS model belonging to decidable fragments are verified by a model checker, and runtime monitors are used to verify the rest. Furthermore, we implement our technique and show experimental results.