A Semantic Approach to Decidability in Epistemic Planning

Dynamic Epistemic Logic (DEL) provides a very rich planning formalism that can handle nondeterminism, partial observability and arbitrary knowledge nesting. The general framework is notoriously undecidable. In this paper, we pursue a novel semantic approach to achieve decidability, by focussing on the logic for epistemic planning, rather then to limit the syntax of the accepted modal formulae. Specifically, we augment the logic S5n by introducing a new interaction axiom that we call knowledge alignment, in order to control the ability of agents to unboundedly reason on the knowledge of other agents. We show that the resulting epistemic planning problem is decidable. In doing so, we prove that this framework admits a finitary non-fixpoint characterization of common knowledge, which is of independent interest.