Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic

TL;DR

This paper demonstrates that using Zero-suppressed Decision Diagrams (ZDDs) instead of Binary Decision Diagrams (BDDs) can significantly reduce memory consumption in symbolic model checking of multi-agent systems modeled with Dynamic Epistemic Logic.

Contribution

The paper introduces the application of ZDDs for encoding Kripke models in Dynamic Epistemic Logic, showing memory efficiency improvements over traditional BDDs.

Findings

ZDD variants reduce memory usage compared to BDDs

Application to well-known puzzles demonstrates practical benefits

Implementation based on SMCDEL and CUDD library confirms effectiveness

Abstract

Binary decision diagrams (BDDs) are widely used to mitigate the state-explosion problem in model checking. A variation of BDDs are Zero-suppressed Decision Diagrams (ZDDs) which omit variables that must be false, instead of omitting variables that do not matter. We use ZDDs to symbolically encode Kripke models used in Dynamic Epistemic Logic, a framework to reason about knowledge and information dynamics in multi-agent systems. We compare the memory usage of different ZDD variants for three well-known examples from the literature: the Muddy Children, the Sum and Product puzzle and the Dining Cryptographers. Our implementation is based on the existing model checker SMCDEL and the CUDD library. Our results show that replacing BDDs with the right variant of ZDDs can significantly reduce memory usage. This suggests that ZDDs are a useful tool for model checking multi-agent systems.