cs.LO · 2604.22736 Copy arXiv ID · Apr 24, 2026 Save An Undecidability Proof for the Plan Existence Problem Authors: Antonis Achilleos
Organizations: Department of Computer Science, Reykjavik University, Iceland
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.
Explore similar work Feb 5, 2024 · Till Hofmann, Stefan Schupp, Gerhard Lakemeyer Computable Clocks
Jul 12, 2026 · Christoph Benzmüller, Daniel Kirchner Modal Logic Theorem
Jul 28, 2026 · Martha Del Toro, Raquel Fuentetaja, Angel García-Olaya Classical Planning Mixed-Integer Programming
Feb 5, 2024 · cs.AI J/K move · Enter open · S save
Till Hofmann, Stefan Schupp, Gerhard Lakemeyer
Representing time is crucial for cyber-physical systems and has been studied extensively in the situation calculus. The most commonly used approach represents time by adding a real-valued function
t i m e ( a ) \mathit{time}(a) time ( a ) that attaches a time point to each action and consequently to each situation. We show that in this approach, checking whether there is a reachable situation that satisfies a given formula is undecidable, even when the domain contains only finitely many objects. We present an alternative approach based on well-established results from timed automata theory by introducing clocks as real-valued fluents with restricted successor state axioms and comparison operators. With this restriction, we can show that the reachability problem for finite-domain basic action theories is decidable. Finally, we apply our results to Golog program realization by presenting a decidable procedure for determining an action sequence that is a successful execution of a given program.