Base-based Model Checking for Multi-Agent Only Believing (long version)

TL;DR

This paper introduces a new semantics for multi-agent only believing using belief bases, along with algorithms for automatic model checking, including a practical implementation and experimental evaluation.

Contribution

It proposes a novel belief base semantics for multi-agent only believing and develops efficient model checking algorithms, including a QBF-based approach.

Findings

QBF-based model checking algorithm operates within PSPACE

Implementation demonstrates practical feasibility

Experimental results show computation time benefits

Abstract

We present a novel semantics for the language of multi-agent only believing exploiting belief bases, and show how to use it for automatically checking formulas of this language and of its dynamic extension with private belief expansion operators. We provide a PSPACE algorithm for model checking relying on a reduction to QBF and alternative dedicated algorithm relying on the exploration of the state space. We present an implementation of the QBF-based algorithm and some experimental results on computation time in a concrete example.