On the Complexity of Dynamic Epistemic Logic

TL;DR

This paper investigates the computational complexity of Dynamic Epistemic Logic (DEL), establishing that model-checking is PSPACE-complete and satisfiability is NEXPTIME-complete, using a new tableau method.

Contribution

It proves the complexity of DEL with event models and introduces a tableau method for satisfiability, filling a significant knowledge gap.

Findings

Model-checking in DEL is PSPACE-complete.

Satisfiability in DEL is NEXPTIME-complete.

A sound and complete tableau method for satisfiability.

Abstract

Although Dynamic Epistemic Logic (DEL) is an influential logical framework for representing and reasoning about information change, little is known about the computational complexity of its associated decision problems. In fact, we only know that for public announcement logic, a fragment of DEL, the satisfiability problem and the model-checking problem are respectively PSPACE-complete and in P. We contribute to fill this gap by proving that for the DEL language with event models, the model-checking problem is, surprisingly, PSPACE-complete. Also, we prove that the satisfiability problem is NEXPTIME-complete. In doing so, we provide a sound and complete tableau method deciding the satisfiability problem.