Tableaux like model checking on-the-fly for ATL+

TL;DR

This paper introduces an on-the-fly tableau-inspired model checking algorithm for ATL+ that efficiently verifies multi-agent system properties by generating states dynamically during the proof process.

Contribution

It presents a novel on-the-fly model checking approach for ATL+ using a tableau-like inference system, enabling efficient verification of multi-agent systems.

Findings

Efficient on-the-fly state generation during model checking

Successful verification of ATL+ properties in multi-agent systems

Proof-of-concept implementation demonstrating practical viability

Abstract

We propose a model checking algorithm to test properties of systems that are expressed in the multi-agent temporal logic ATL+. The specificities of this algorithm are: it is on-the-fly, generating states only when they are needed, and it works by constructing a candidate formal proof in an inference system inspired by tableau proof systems.