Undecidability in Epistemic Planning
Guillaume Aucher, Thomas Bolander, Guillaume Aucher, Thomas Bol, Guillaume Aucher, Thomas Bolander · Technical University of Denmark, DTU Orbit (Technical University of Denmark, DTU) · 2013
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).