Base-based Model Checking for Multi-Agent Only Believing (long version)
This work addresses the challenge of model checking for multi-agent belief systems, which is incremental as it builds on existing semantics with new algorithmic approaches.
The paper tackles the problem of automatically checking formulas in multi-agent only believing and its dynamic extension by introducing a novel semantics based on belief bases, resulting in a PSPACE algorithm with experimental computation time results.
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.