An Undecidability Proof for the Plan Existence Problem

TL;DR

This paper proves that determining the existence of a plan in certain modal logic settings is undecidable, even with simplified preconditions and no postconditions.

Contribution

It establishes the undecidability of the plan existence problem under conditions where it was previously unknown.

Findings

Plan existence problem is undecidable with modal depth at most 1 preconditions.

Undecidability holds even without postconditions.

Addresses a previously unknown aspect of epistemic planning complexity.

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.