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

要約

我々は、信念ベースを利用した信念のみをもつマルチエージェント言語の新しいセマンティクスを提示し、この言語とプライベート信念展開演算子による動的拡張の公式を自動的にチェックするためにそれを使用する方法を示します。
QBF への還元に依存するモデル チェック用の PSPACE アルゴリズムと、状態空間の探索に依存する代替の専用アルゴリズムを提供します。
QBF ベースのアルゴリズムの実装と、具体的な例での計算時間に関するいくつかの実験結果を示します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google