An Undecidability Proof for the Plan Existence Problem

AIPR assessment

This is a hard, specialized theory problem in an active subfield, where the relevant baseline is a chain of prior decidability and undecidability results rather than empirical benchmarks. The main strengths reinforce each other: the open-problem resolution, the carefully engineered reduction, and the multiple frame-condition extensions all point to a substantial formal contribution. The main weakness is limited downstream directness, since the result is a negative boundary theorem rather than a

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.

Score Breakdown

More from this week

• Agentic World Modeling: Foundations, Capabilities, Laws, and Beyond
• How Hard is it to Decide if a Fact is Relevant to a Query?
• Railway Artificial Intelligence Learning Benchmark (RAIL-BENCH): A Benchmark Suite for Perception in the Railway Domain
• On first-order model checking parameterized by the number of variables
• Entrywise Low-Rank Approximation and Matrix \(p \rightarrow q\) Norms via Global Correlation Rounding

More in Logic

• Univalence without function extensionality
• Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes
• An algebraic characterisation of Eve-positional languages
• On first-order model checking parameterized by the number of variables