Click here to flash read.
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.
