A Semantic Approach to Decidability in Epistemic Planning (Extended Version)

要約

マルチエージェント計画における動的認識論理 (DEL) の使用により、非決定性、部分的な可観測性、および任意の知識の入れ子を処理できるアクション形式主義が広く採用されるようになりました。
このような表現力は決定不可能性を犠牲にして得られるため、主にアクション形式主義の構文上の制限に基づいて、いくつかの決定可能な断片が分離されてきました。
この論文では、決定可能性を達成するための新しい意味論的アプローチを追求します。
つまり、意味論的アプローチは、構文上の制約を課すのではなく、認識論的計画のための論理の公理に焦点を当てます。
具体的には、知識 S5$_n$ の論理と、(知識) 可換性と呼ばれる相互作用公理を拡張します。これは、エージェントが他のエージェントの知識に基づいて無制限に推論する能力を制御します。
その後、3倍の寄付を提供します。
まず、結果として生じる認識論的計画問題が決定可能であることを示します。
そうすることで、私たちのフレームワークが、独立した利益をもたらす共通知識の有限の非固定点の特徴付けを許容することを証明します。
第二に、DEL のより表現力豊かな断片の決定可能性を取得することを目的として、可換性公理のさまざまな一般化を研究します。
最後に、アクション テンプレートに基づく 2 つのよく知られた認識計画システムが、知識の設定の下で解釈された場合、可換性の公理に準拠することを示し、したがってそれらの決定可能性を証明します。

要約(オリジナル)

The use of Dynamic Epistemic Logic (DEL) in multi-agent planning has led to a widely adopted action formalism that can handle nondeterminism, partial observability and arbitrary knowledge nesting. As such expressive power comes at the cost of undecidability, several decidable fragments have been isolated, mainly based on syntactic restrictions of the action formalism. In this paper, we pursue a novel semantic approach to achieve decidability. Namely, rather than imposing syntactical constraints, the semantic approach focuses on the axioms of the logic for epistemic planning. Specifically, we augment the logic of knowledge S5$_n$ and with an interaction axiom called (knowledge) commutativity, which controls the ability of agents to unboundedly reason on the knowledge of other agents. We then provide a threefold contribution. First, we show that the resulting epistemic planning problem is decidable. In doing so, we prove that our framework admits a finitary non-fixpoint characterization of common knowledge, which is of independent interest. Second, we study different generalizations of the commutativity axiom, with the goal of obtaining decidability for more expressive fragments of DEL. Finally, we show that two well-known epistemic planning systems based on action templates, when interpreted under the setting of knowledge, conform to the commutativity axiom, hence proving their decidability.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google