An Undecidability Proof for the Plan Existence Problem
This result establishes a fundamental undecidability boundary for epistemic planning, which is important for AI and multi-agent systems researchers.
The paper proves that the plan existence problem in epistemic planning is undecidable, even when action preconditions have modal depth at most 1 and there are no postconditions, resolving a previously open question.
The plan existence problem asks, given a goal in the form of a formula in modal logic, an initial epistemic state (a pointed Kripke model), and a set of epistemic actions, whether there exists a sequence of actions that can be applied to reach the goal. We prove that even in the case where the preconditions of the epistemic actions have modal depth at most 1, and there are no postconditions, the plan existence problem is undecidable. The (un)decidability of this problem was previously unknown.