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

TL;DR

This paper introduces a semantic method for ensuring decidability in epistemic planning by augmenting the logic of knowledge with an interaction axiom, enabling analysis of more expressive multi-agent planning systems.

Contribution

It proposes a semantic approach to decidability in epistemic planning by adding the commutativity axiom to the logic of knowledge, moving beyond syntactic restrictions.

Findings

Decidability of the epistemic planning problem under the new framework.

Finitary non-fixpoint characterization of common knowledge.

Existing epistemic planning systems conform to the commutativity axiom, ensuring their decidability.

Abstract

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.