An Undecidability Proof for the Plan Existence Problem
Logic in Computer Science
2026-04-27 v1 Artificial Intelligence
Abstract
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.
Keywords
Cite
@article{arxiv.2604.22736,
title = {An Undecidability Proof for the Plan Existence Problem},
author = {Antonis Achilleos},
journal= {arXiv preprint arXiv:2604.22736},
year = {2026}
}