Comparing State-Representations for DEL Model Checking

TL;DR

This paper compares symbolic BDD-based and mental program-based representations for DEL model checking, establishing their computational complexity and providing translations between them, thus advancing understanding of their theoretical limits.

Contribution

It proves that model checking DEL with BDD-based symbolic structures is PSPACE-complete and relates it to mental program models, including exponential translation bounds.

Findings

Model checking DEL with BDDs is PSPACE-complete.

Translations between BDDs and mental programs are exponential.

No small translation exists from mental programs to BDDs.

Abstract

Model checking with the standard Kripke models used in (Dynamic) Epistemic Logic leads to scalability issues. Hence alternative representations have been developed, in particular symbolic structures based on Binary Decision Diagrams (BDDs) and succinct models based on mental programs. While symbolic structures have been shown to perform well in practice, their theoretical complexity was not known so far. On the other hand, for succinct models model checking is known to be PSPACE-complete, but no implementations are available. We close this gap and directly relate the two representations. We show that model checking DEL on symbolic structures encoded with BDDs is also PSPACE-complete. In fact, already model checking Epistemic Logic without dynamics is PSPACE-complete on symbolic structures. We also provide direct translations between BDDs and mental programs. Both translations yield exponential outputs. For the translation from mental programs to BDDs we show that no small translation exists. For the other direction we conjecture the same.