Undecidability in Epistemic Planning

Dynamic epistemic logic (DEL) provides a very expressive framework for multi-agent planning that can deal with nondeterminism, partial observability, sensing actions, and arbitrary nesting of beliefs about other agents' beliefs. However, as we show in this paper, this expressiveness comes at a price. The planning framework is undecidable, even if we allow only purely epistemic actions (actions that change only beliefs, not ontic facts). Undecidability holds already in the S5 setting with at least 2 agents, and even with 1 agent in S4. It shows that multi-agent planning is robustly undecidable if we assume that agents can reason with an arbitrary nesting of beliefs about beliefs. We also prove a corollary showing undecidability of the DEL model checking problem with the star operator on actions (iteration).

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/hal-00824653
Author Aucher, Guillaume, Bolander, Thomas
Maintainer CCSD
Last Updated May 11, 2026, 01:45 (UTC)
Created May 11, 2026, 01:45 (UTC)
Identifier Report N°: RR-8310
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor System synthesis and supervision, scenarios (S4) ; Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Centre Inria de l'Université de Rennes ; Institut National de Recherche en Informatique et en Automatique (Inria)
creator Aucher, Guillaume
date 2013-05-22T00:00:00
harvest_object_id b698c86e-fa8c-4c2e-b2f3-a1984de1c673
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-03-28T00:00:00
set_spec type:REPORT