Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Comparing State-Representations for DEL Model Checking

Gregor Behnke, Malvin Gattinger, Avijeet Ghosh, Haitian Wang

TL;DR

The paper investigates scalable model checking for Dynamic Epistemic Logic by comparing two compact representations: symbolic structures based on Binary Decision Diagrams and succinct models encoded by mental programs. It proves that PAL-S5 and DEL-K model checking remain PSPACE-complete on symbolic structures, and develops explicit, but exponentially sized, translations between BDDs and mental programs, including a no-small-translation result in one direction. It extends the analysis to DEL with belief structures and transformers, establishing PSPACE-completeness across representations. The work clarifies trade-offs between representations, highlights the necessity of direct formalization in a chosen representation, and reports on implementation efforts and future benchmarking within the SMCDEL framework.

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.

Comparing State-Representations for DEL Model Checking

TL;DR

The paper investigates scalable model checking for Dynamic Epistemic Logic by comparing two compact representations: symbolic structures based on Binary Decision Diagrams and succinct models encoded by mental programs. It proves that PAL-S5 and DEL-K model checking remain PSPACE-complete on symbolic structures, and develops explicit, but exponentially sized, translations between BDDs and mental programs, including a no-small-translation result in one direction. It extends the analysis to DEL with belief structures and transformers, establishing PSPACE-completeness across representations. The work clarifies trade-offs between representations, highlights the necessity of direct formalization in a chosen representation, and reports on implementation efforts and future benchmarking within the SMCDEL framework.

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.

Paper Structure

This paper contains 10 sections, 20 theorems, 17 equations, 4 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Symbolic Structures with BDDs
  3. Symbolic Model Checking $\mathsf{PAL}$-S5
  4. Symbolic Model Checking $\mathsf{DEL}$-K
  5. Succinct Models with Mental Programs
  6. Comparison and Translations
  7. Translating Mental Programs to BDDs
  8. Translating BDDs to Mental Programs
  9. Conclusions and Future Work
  10. Proofs

Key Result

Theorem 2.8

Model checking $\mathcal{L}_\mathsf{EL}\xspace$ on knowledge structures is PSPACE-hard.

Figures (4)

  • Figure 1: Node $p_i$ in $\beta$'s $\mathsf{BDD}$.
  • Figure 2: Node $p_i$ in $\beta \land \bigwedge_{p \in V} (p \leftrightarrow p')$'s $\mathsf{BDD}$.
  • Figure 3: The BDD after $p_0$ is added.
  • Figure 4: The corresponding Kripke model.

Theorems & Definitions (50)

  • Example 1.1
  • Definition 1.2
  • Definition 1.3
  • Definition 1.4
  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • ...and 40 more